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