1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11theory Rule_By_Method
12imports
13  Main
14  "HOL-Eisbach.Eisbach_Tools"
15begin
16
17ML \<open>
18signature RULE_BY_METHOD =
19sig
20  val rule_by_tac: Proof.context -> {vars : bool, prop: bool} ->
21    (Proof.context -> tactic) -> (Proof.context -> tactic) list -> Position.T -> thm
22end;
23
24
25fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt);
26
27fun fix_schematics ctxt raw_st =
28  let
29    val ((schematic_types, [st']), ctxt1) = Variable.importT [raw_st] ctxt;
30    fun certify_inst ctxt inst = map (apsnd (Thm.cterm_of ctxt)) (#2 inst)
31    val (schematic_terms, ctxt2) =
32      Variable.import_inst true [Thm.prop_of st'] ctxt1
33      |>> certify_inst ctxt1;
34    val schematics = (schematic_types, schematic_terms);
35  in (Thm.instantiate schematics st', ctxt2) end
36
37fun curry_asm ctxt st = if Thm.nprems_of st = 0 then Seq.empty else
38let
39
40  val prems = Thm.cprem_of st 1 |> Thm.term_of |> Logic.strip_imp_prems;
41
42  val (thesis :: xs,ctxt') = Variable.variant_fixes ("thesis" :: replicate (length prems) "P") ctxt;
43
44  val rl =
45    xs
46    |> map (fn x => Thm.cterm_of ctxt' (Free (x, propT)))
47    |> Conjunction.mk_conjunction_balanced
48    |> (fn xs => Thm.apply (Thm.apply @{cterm "Pure.imp"} xs) (Thm.cterm_of ctxt' (Free (thesis,propT))))
49    |> Thm.assume
50    |> Conjunction.curry_balanced (length prems)
51    |> Drule.implies_intr_hyps
52
53  val rl' = singleton (Variable.export ctxt' ctxt) rl;
54
55  in Thm.bicompose (SOME ctxt) {flatten = false, match = false, incremented = false}
56              (false, rl', 1) 1 st end;
57
58val drop_trivial_imp =
59let
60  val asm =
61    Thm.assume (Drule.protect @{cprop "(PROP A \<Longrightarrow> PROP A) \<Longrightarrow> PROP A"})
62    |> Goal.conclude;
63
64in
65  Thm.implies_elim  asm (Thm.trivial @{cprop "PROP A"})
66  |> Drule.implies_intr_hyps
67  |> Thm.generalize ([],["A"]) 1
68  |> Drule.zero_var_indexes
69 end
70
71val drop_trivial_imp' =
72let
73  val asm =
74    Thm.assume (Drule.protect @{cprop "(PROP P \<Longrightarrow> A) \<Longrightarrow> A"})
75    |> Goal.conclude;
76
77  val asm' = Thm.assume @{cprop "PROP P == Trueprop A"}
78
79in
80  Thm.implies_elim asm (asm' COMP Drule.equal_elim_rule1)
81  |> Thm.implies_elim (asm' COMP Drule.equal_elim_rule2)
82  |> Drule.implies_intr_hyps
83  |> Thm.permute_prems 0 ~1
84  |> Thm.generalize ([],["A","P"]) 1
85  |> Drule.zero_var_indexes
86 end
87
88fun atomize_equiv_tac ctxt i =
89  Object_Logic.full_atomize_tac ctxt i
90  THEN PRIMITIVE (fn st'  =>
91  let val (_,[A,_]) = Drule.strip_comb (Thm.cprem_of st' i) in
92  if Object_Logic.is_judgment ctxt (Thm.term_of A) then st'
93  else error ("Failed to fully atomize result:\n" ^ (Syntax.string_of_term ctxt (Thm.term_of A))) end)
94
95
96structure Data = Proof_Data
97(
98  type T = thm list * bool;
99  fun init _ = ([],false);
100);
101
102val empty_rule_prems = Data.map (K ([],true));
103
104fun add_rule_prem thm = Data.map (apfst (Thm.add_thm thm));
105
106fun with_rule_prems enabled parse =
107  Scan.state :|-- (fn context =>
108  let
109    val context' = Context.proof_of context |> Data.map (K ([Drule.free_dummy_thm],enabled))
110                   |> Context.Proof
111  in Scan.lift (Scan.pass context' parse) end)
112
113
114fun get_rule_prems ctxt =
115  let
116    val (thms,b) = Data.get ctxt
117  in if (not b) then [] else thms end
118
119
120fun zip_subgoal assume tac (ctxt,st : thm) = if Thm.nprems_of st = 0 then Seq.single (ctxt,st) else
121let
122  fun bind_prems st' =
123  let
124    val prems = Drule.cprems_of st';
125    val (asms, ctxt') = Assumption.add_assumes prems ctxt;
126    val ctxt'' = fold add_rule_prem asms ctxt';
127    val st'' = Goal.conclude (Drule.implies_elim_list st' (map Thm.assume prems));
128  in (ctxt'',st'') end
129
130  fun defer_prems st' =
131  let
132    val nprems = Thm.nprems_of st';
133    val st'' = Thm.permute_prems 0 nprems (Goal.conclude st');
134  in (ctxt,st'') end;
135
136
137in
138  tac ctxt (Goal.protect 1 st)
139  |> Seq.map (if assume then bind_prems else defer_prems)  end
140
141
142fun zip_subgoals assume tacs pos ctxt st =
143let
144  val nprems = Thm.nprems_of st;
145  val _ = nprems < length tacs andalso error ("More tactics than rule assumptions" ^ Position.here pos);
146  val tacs' = map (zip_subgoal assume) (tacs @ (replicate (nprems - length tacs) (K all_tac)));
147  val ctxt' = empty_rule_prems ctxt;
148in Seq.EVERY tacs' (ctxt',st) end;
149
150fun rule_by_tac' ctxt {vars,prop} tac asm_tacs pos raw_st =
151  let
152    val (st,ctxt1) = if vars then (raw_st,ctxt) else fix_schematics ctxt raw_st;
153
154    val ([x],ctxt2) = Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN,NONE, NoSyn)] ctxt1;
155
156    val thesis = if prop then Free (x,propT) else Object_Logic.fixed_judgment ctxt2 x;
157
158    val cthesis = Thm.cterm_of ctxt thesis;
159
160    val revcut_rl' = Thm.instantiate' [] ([NONE,SOME cthesis]) @{thm revcut_rl};
161
162    fun is_thesis t = Logic.strip_assums_concl t aconv thesis;
163
164    fun err thm str = error (str ^ Position.here pos ^ "\n" ^
165      (Pretty.string_of (Goal_Display.pretty_goal ctxt thm)));
166
167    fun pop_thesis st =
168    let
169      val prems = Thm.prems_of st |> tag_list 0;
170      val (i,_) = (case filter (is_thesis o snd) prems of
171        [] => err st "Lost thesis"
172        | [x] => x
173        | _ => err st "More than one result obtained");
174     in st |> Thm.permute_prems 0 i  end
175
176    val asm_st =
177    (revcut_rl' OF [st])
178    |> (fn st => Goal.protect (Thm.nprems_of st - 1) st)
179
180
181    val (ctxt3,concl_st) = case Seq.pull (zip_subgoals (not vars) asm_tacs pos ctxt2 asm_st) of
182      SOME (x,_) => x
183    | NONE => error ("Failed to apply tactics to rule assumptions. " ^ (Position.here pos));
184
185    val concl_st_prepped =
186      concl_st
187      |> Goal.conclude
188      |> (fn st => Goal.protect (Thm.nprems_of st) st |> Thm.permute_prems 0 ~1 |> Goal.protect 1)
189
190    val concl_st_result = concl_st_prepped
191      |> (tac ctxt3
192          THEN (PRIMITIVE pop_thesis)
193          THEN curry_asm ctxt
194          THEN PRIMITIVE (Goal.conclude #> Thm.permute_prems 0 1 #> Goal.conclude))
195
196    val result = (case Seq.pull concl_st_result of
197      SOME (result,_) => singleton (Proof_Context.export ctxt3 ctxt) result
198      | NONE => err concl_st_prepped "Failed to apply tactic to rule conclusion:")
199
200    val drop_rule = if prop then drop_trivial_imp else drop_trivial_imp'
201
202    val result' = ((Goal.protect (Thm.nprems_of result -1) result) RS drop_rule)
203    |> (if prop then all_tac else
204       (atomize_equiv_tac ctxt (Thm.nprems_of result)
205       THEN resolve_tac ctxt @{thms Pure.reflexive} (Thm.nprems_of result)))
206    |> Seq.hd
207    |> Raw_Simplifier.norm_hhf ctxt
208
209  in Drule.zero_var_indexes result' end;
210
211fun rule_by_tac is_closed ctxt args tac asm_tacs pos raw_st =
212 let val f = rule_by_tac' ctxt args tac asm_tacs pos
213  in
214   if is_closed orelse Context_Position.is_really_visible ctxt then SOME (f raw_st)
215   else try f raw_st
216 end
217
218fun pos_closure (scan : 'a context_parser) :
219  (('a * (Position.T * bool)) context_parser) = (fn (context,toks) =>
220  let
221    val (((context',x),tr_toks),toks') = Scan.trace (Scan.pass context (Scan.state -- scan)) toks;
222    val pos = Token.range_of tr_toks;
223    val is_closed = exists (fn t => is_some (Token.get_value t)) tr_toks
224  in ((x,(Position.range_position pos, is_closed)),(context',toks')) end)
225
226val parse_flags = Args.mode "schematic" -- Args.mode "raw_prop" >> (fn (b,b') => {vars = b, prop = b'})
227
228fun tac m ctxt =
229  Method.NO_CONTEXT_TACTIC ctxt
230    (Method.evaluate_runtime m ctxt []);
231
232(* Declare as a mixed attribute to avoid any partial evaluation *)
233
234fun handle_dummy f (context, thm) =
235  case (f context thm) of SOME thm' => (NONE, SOME thm')
236  | NONE => (SOME context, SOME Drule.free_dummy_thm)
237
238val (rule_prems_by_method : attribute context_parser) = Scan.lift parse_flags :-- (fn flags =>
239  pos_closure (Scan.repeat1
240    (with_rule_prems (not (#vars flags)) Method.text_closure ||
241      Scan.lift (Args.$$$ "_" >> (K Method.succeed_text))))) >>
242        (fn (flags,(ms,(pos, is_closed))) => handle_dummy (fn context =>
243          rule_by_tac is_closed (Context.proof_of context) flags (K all_tac) (map tac ms) pos))
244
245val (rule_concl_by_method : attribute context_parser) = Scan.lift parse_flags :-- (fn flags =>
246  pos_closure (with_rule_prems (not (#vars flags)) Method.text_closure)) >>
247    (fn (flags,(m,(pos, is_closed))) => handle_dummy (fn context =>
248      rule_by_tac is_closed (Context.proof_of context) flags (tac m) [] pos))
249
250val _ = Theory.setup
251  (Global_Theory.add_thms_dynamic (@{binding "rule_prems"},
252    (fn context => get_rule_prems (Context.proof_of context))) #>
253   Attrib.setup @{binding "#"} rule_prems_by_method
254    "transform rule premises with method" #>
255   Attrib.setup @{binding "@"} rule_concl_by_method
256    "transform rule conclusion with method" #>
257   Attrib.setup @{binding atomized}
258    (Scan.succeed (Thm.rule_attribute []
259      (fn context => fn thm =>
260        Conv.fconv_rule (Object_Logic.atomize (Context.proof_of context)) thm
261          |> Drule.zero_var_indexes)))
262    "atomize rule")
263\<close>
264
265experiment begin
266
267ML \<open>
268  val [att] = @{attributes [@\<open>erule thin_rl, cut_tac TrueI, fail\<close>]}
269  val k = Attrib.attribute @{context} att
270  val _ = case (try k (Context.Proof @{context}, Drule.dummy_thm)) of
271    SOME _ => error "Should fail"
272    | _ => ()
273  \<close>
274
275lemmas baz = [[@\<open>erule thin_rl, rule revcut_rl[of "P \<longrightarrow> P \<and> P"], simp\<close>]] for P
276
277lemmas bazz[THEN impE] = TrueI[@\<open>erule thin_rl, rule revcut_rl[of "P \<longrightarrow> P \<and> P"], simp\<close>] for P
278
279lemma "Q \<longrightarrow> Q \<and> Q" by (rule baz)
280
281method silly_rule for P :: bool uses rule =
282  (rule [[@\<open>erule thin_rl, cut_tac rule, drule asm_rl[of P]\<close>]])
283
284lemma assumes A shows A by (silly_rule A rule: \<open>A\<close>)
285
286lemma assumes A[simp]: "A" shows A
287  apply (match conclusion in P for P \<Rightarrow>
288       \<open>rule [[@\<open>erule thin_rl, rule revcut_rl[of "P"], simp\<close>]]\<close>)
289  done
290
291end
292
293end
294