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