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