1(* Title: Subgoal_Methods.thy 2 Author: Daniel Matichuk, NICTA/UNSW 3 4Methods for managing subgoals collectively. 5*) 6 7(* 8 * Copyright 2014, NICTA 9 * 10 * This software may be distributed and modified according to the terms of 11 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 12 * See "LICENSE_BSD2.txt" for details. 13 * 14 * @TAG(NICTA_BSD) 15 *) 16 17theory Subgoal_Methods 18imports Main 19begin 20ML \<open> 21signature SUBGOAL_METHODS = 22sig 23 val fold_subgoals: Proof.context -> bool -> thm -> thm 24 val unfold_subgoals_tac: Proof.context -> tactic 25 val distinct_subgoals: Proof.context -> thm -> thm 26end; 27 28structure Subgoal_Methods: SUBGOAL_METHODS = 29struct 30 31fun max_common_prefix eq (ls :: lss) = 32 let 33 val ls' = tag_list 0 ls; 34 fun all_prefix (i,a) = 35 forall (fn ls' => if length ls' > i then eq (a, nth ls' i) else false) lss 36 val ls'' = take_prefix all_prefix ls' 37 in map snd ls'' end 38 | max_common_prefix _ [] = []; 39 40fun push_outer_params ctxt th = 41 let 42 val ctxt' = ctxt 43 |> Simplifier.empty_simpset 44 |> Simplifier.add_simp Drule.norm_hhf_eq; 45 in 46 Conv.fconv_rule 47 (Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) ctxt') th 48 end; 49 50fun fix_schematics ctxt raw_st = 51 let 52 val ((schematic_types, [st']), ctxt1) = Variable.importT [raw_st] ctxt; 53 val ((_, inst), ctxt2) = 54 Variable.import_inst true [Thm.prop_of st'] ctxt1; 55 56 val schematic_terms = map (apsnd (Thm.cterm_of ctxt2)) inst; 57 val schematics = (schematic_types, schematic_terms); 58 59 in (Thm.instantiate schematics st', ctxt2) end 60 61val strip_params = Term.strip_all_vars; 62val strip_prems = Logic.strip_imp_prems o Term.strip_all_body; 63val strip_concl = Logic.strip_imp_concl o Term.strip_all_body; 64 65 66 67fun fold_subgoals ctxt prefix raw_st = 68 if Thm.nprems_of raw_st < 2 then raw_st 69 else 70 let 71 val (st, inner_ctxt) = fix_schematics ctxt raw_st; 72 73 val subgoals = Thm.prems_of st; 74 val paramss = map strip_params subgoals; 75 val common_params = max_common_prefix (eq_snd (op =)) paramss; 76 77 fun strip_shift subgoal = 78 let 79 val params = strip_params subgoal; 80 val diff = length common_params - length params; 81 val prems = strip_prems subgoal; 82 in map (Term.incr_boundvars diff) prems end; 83 84 val premss = map (strip_shift) subgoals; 85 86 val common_prems = max_common_prefix (op aconv) premss; 87 88 val common_params = if prefix then common_params else []; 89 val common_prems = if prefix then common_prems else []; 90 91 fun mk_concl subgoal = 92 let 93 val params = Term.strip_all_vars subgoal; 94 val local_params = drop (length common_params) params; 95 val prems = strip_prems subgoal; 96 val local_prems = drop (length common_prems) prems; 97 val concl = strip_concl subgoal; 98 in Logic.list_all (local_params, Logic.list_implies (local_prems, concl)) end; 99 100 val goal = 101 Logic.list_all (common_params, 102 (Logic.list_implies (common_prems,Logic.mk_conjunction_list (map mk_concl subgoals)))); 103 104 val chyp = Thm.cterm_of inner_ctxt goal; 105 106 val (common_params',inner_ctxt') = 107 Variable.add_fixes (map fst common_params) inner_ctxt 108 |>> map2 (fn (_, T) => fn x => Thm.cterm_of inner_ctxt (Free (x, T))) common_params; 109 110 fun try_dest rule = 111 try (fn () => (@{thm conjunctionD1} OF [rule], @{thm conjunctionD2} OF [rule])) (); 112 113 fun solve_headgoal rule = 114 let 115 val rule' = rule 116 |> Drule.forall_intr_list common_params' 117 |> push_outer_params inner_ctxt'; 118 in 119 (fn st => Thm.implies_elim st rule') 120 end; 121 122 fun solve_subgoals rule' st = 123 (case try_dest rule' of 124 SOME (this, rest) => solve_subgoals rest (solve_headgoal this st) 125 | NONE => solve_headgoal rule' st); 126 127 val rule = Drule.forall_elim_list common_params' (Thm.assume chyp); 128 in 129 st 130 |> push_outer_params inner_ctxt 131 |> solve_subgoals rule 132 |> Thm.implies_intr chyp 133 |> singleton (Variable.export inner_ctxt' ctxt) 134 end; 135 136fun distinct_subgoals ctxt raw_st = 137 let 138 val (st, inner_ctxt) = fix_schematics ctxt raw_st; 139 val subgoals = Drule.cprems_of st; 140 val atomize = Conv.fconv_rule (Object_Logic.atomize_prems inner_ctxt); 141 142 val rules = 143 map (atomize o Raw_Simplifier.norm_hhf inner_ctxt o Thm.assume) subgoals 144 |> sort (int_ord o apply2 Thm.nprems_of); 145 146 val st' = st 147 |> ALLGOALS (fn i => 148 Object_Logic.atomize_prems_tac inner_ctxt i THEN solve_tac inner_ctxt rules i) 149 |> Seq.hd; 150 151 val subgoals' = subgoals 152 |> inter (op aconvc) (Thm.chyps_of st') 153 |> distinct (op aconvc); 154 in 155 Drule.implies_intr_list subgoals' st' 156 |> singleton (Variable.export inner_ctxt ctxt) 157 end; 158 159(* Variant of filter_prems_tac that recovers premise order *) 160fun filter_prems_tac' ctxt pred = 161 let 162 fun Then NONE tac = SOME tac 163 | Then (SOME tac) tac' = SOME (tac THEN' tac'); 164 fun thins H (tac, n, i) = 165 (if pred H then (tac, n + 1, i) 166 else (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0, i + n)); 167 in 168 SUBGOAL (fn (goal, i) => 169 let val Hs = Logic.strip_assums_hyp goal in 170 (case fold thins Hs (NONE, 0, 0) of 171 (NONE, _, _) => no_tac 172 | (SOME tac, _, n) => tac i THEN rotate_tac (~ n) i) 173 end) 174 end; 175 176fun trim_prems_tac ctxt rules = 177let 178 fun matches (prem,rule) = 179 let 180 val ((_,prem'),ctxt') = Variable.focus NONE prem ctxt; 181 val rule_prop = Thm.prop_of rule; 182 in Unify.matches_list (Context.Proof ctxt') [rule_prop] [prem'] end; 183 184in filter_prems_tac' ctxt (not o member matches rules) end; 185 186val adhoc_conjunction_tac = REPEAT_ALL_NEW 187 (SUBGOAL (fn (goal, i) => 188 if can Logic.dest_conjunction (Logic.strip_imp_concl goal) 189 then resolve0_tac [Conjunction.conjunctionI] i 190 else no_tac)); 191 192fun unfold_subgoals_tac ctxt = 193 TRY (adhoc_conjunction_tac 1) 194 THEN (PRIMITIVE (Raw_Simplifier.norm_hhf ctxt)); 195 196val _ = 197 Theory.setup 198 (Method.setup @{binding fold_subgoals} 199 (Scan.lift (Args.mode "prefix") >> (fn prefix => fn ctxt => 200 SIMPLE_METHOD (PRIMITIVE (fold_subgoals ctxt prefix)))) 201 "lift all subgoals over common premises/params" #> 202 Method.setup @{binding unfold_subgoals} 203 (Scan.succeed (fn ctxt => SIMPLE_METHOD (unfold_subgoals_tac ctxt))) 204 "recover subgoals after folding" #> 205 Method.setup @{binding distinct_subgoals} 206 (Scan.succeed (fn ctxt => SIMPLE_METHOD (PRIMITIVE (distinct_subgoals ctxt)))) 207 "trim all subgoals to be (logically) distinct" #> 208 Method.setup @{binding trim} 209 (Attrib.thms >> (fn thms => fn ctxt => 210 SIMPLE_METHOD (HEADGOAL (trim_prems_tac ctxt thms)))) 211 "trim all premises that match the given rules"); 212 213end; 214\<close> 215 216end 217