1(* Title: HOL/Tools/simpdata.ML 2 Author: Tobias Nipkow 3 Copyright 1991 University of Cambridge 4 5Instantiation of the generic simplifier for HOL. 6*) 7 8(** tools setup **) 9 10structure Quantifier1 = Quantifier1 11( 12 (*abstract syntax*) 13 fun dest_eq (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ s $ t) = SOME (s, t) 14 | dest_eq _ = NONE; 15 fun dest_conj (Const(\<^const_name>\<open>HOL.conj\<close>,_) $ s $ t) = SOME (s, t) 16 | dest_conj _ = NONE; 17 fun dest_imp (Const(\<^const_name>\<open>HOL.implies\<close>,_) $ s $ t) = SOME (s, t) 18 | dest_imp _ = NONE; 19 val conj = HOLogic.conj 20 val imp = HOLogic.imp 21 (*rules*) 22 val iff_reflection = @{thm eq_reflection} 23 val iffI = @{thm iffI} 24 val iff_trans = @{thm trans} 25 val conjI= @{thm conjI} 26 val conjE= @{thm conjE} 27 val impI = @{thm impI} 28 val mp = @{thm mp} 29 val uncurry = @{thm uncurry} 30 val exI = @{thm exI} 31 val exE = @{thm exE} 32 val iff_allI = @{thm iff_allI} 33 val iff_exI = @{thm iff_exI} 34 val all_comm = @{thm all_comm} 35 val ex_comm = @{thm ex_comm} 36); 37 38structure Simpdata = 39struct 40 41fun mk_meta_eq r = r RS @{thm eq_reflection}; 42fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; 43 44fun mk_eq th = 45 (case Thm.concl_of th of 46 (*expects Trueprop if not == *) 47 Const (\<^const_name>\<open>Pure.eq\<close>,_) $ _ $ _ => th 48 | _ $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _) => mk_meta_eq th 49 | _ $ (Const (\<^const_name>\<open>Not\<close>, _) $ _) => th RS @{thm Eq_FalseI} 50 | _ => th RS @{thm Eq_TrueI}) 51 52fun mk_eq_True (_: Proof.context) r = 53 SOME (HOLogic.mk_obj_eq r RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE; 54 55(* Produce theorems of the form 56 (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) 57*) 58 59fun lift_meta_eq_to_obj_eq ctxt i st = 60 let 61 fun count_imp (Const (\<^const_name>\<open>HOL.simp_implies\<close>, _) $ _ $ P) = 1 + count_imp P 62 | count_imp _ = 0; 63 val j = count_imp (Logic.strip_assums_concl (Thm.term_of (Thm.cprem_of st i))) 64 in 65 if j = 0 then @{thm meta_eq_to_obj_eq} 66 else 67 let 68 val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); 69 val mk_simp_implies = fold_rev (fn R => fn S => 70 Const (\<^const_name>\<open>HOL.simp_implies\<close>, propT --> propT --> propT) $ R $ S) Ps; 71 in 72 Goal.prove_global (Proof_Context.theory_of ctxt) [] 73 [mk_simp_implies \<^prop>\<open>(x::'a) == y\<close>] 74 (mk_simp_implies \<^prop>\<open>(x::'a) = y\<close>) 75 (fn {context = ctxt, prems} => EVERY 76 [rewrite_goals_tac ctxt @{thms simp_implies_def}, 77 REPEAT (assume_tac ctxt 1 ORELSE 78 resolve_tac ctxt 79 (@{thm meta_eq_to_obj_eq} :: 80 map (rewrite_rule ctxt @{thms simp_implies_def}) prems) 1)]) 81 end 82 end; 83 84(*Congruence rules for = (instead of ==)*) 85fun mk_meta_cong ctxt rl = 86 let 87 val rl' = Seq.hd (TRYALL (fn i => fn st => 88 resolve_tac ctxt [lift_meta_eq_to_obj_eq ctxt i st] i st) rl) 89 in 90 mk_meta_eq rl' handle THM _ => 91 if can Logic.dest_equals (Thm.concl_of rl') then rl' 92 else error "Conclusion of congruence rules must be =-equality" 93 end |> zero_var_indexes; 94 95fun mk_atomize ctxt pairs = 96 let 97 fun atoms thm = 98 let 99 fun res th = map (fn rl => th RS rl); (*exception THM*) 100 val thm_ctxt = Variable.declare_thm thm ctxt; 101 fun res_fixed rls = 102 if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls 103 else Variable.trade (K (fn [thm'] => res thm' rls)) thm_ctxt [thm]; 104 in 105 case Thm.concl_of thm 106 of Const (\<^const_name>\<open>Trueprop\<close>, _) $ p => (case head_of p 107 of Const (a, _) => (case AList.lookup (op =) pairs a 108 of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm]) 109 | NONE => [thm]) 110 | _ => [thm]) 111 | _ => [thm] 112 end; 113 in atoms end; 114 115fun mksimps pairs ctxt = map_filter (try mk_eq) o mk_atomize ctxt pairs o Variable.gen_all ctxt; 116 117fun unsafe_solver_tac ctxt = 118 let 119 val sol_thms = 120 reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt; 121 fun sol_tac i = 122 FIRST 123 [resolve_tac ctxt sol_thms i, 124 assume_tac ctxt i, 125 eresolve_tac ctxt @{thms FalseE} i] ORELSE 126 (match_tac ctxt [@{thm conjI}] 127 THEN_ALL_NEW sol_tac) i 128 in 129 (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac 130 end; 131 132val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; 133 134 135(*No premature instantiation of variables during simplification*) 136fun safe_solver_tac ctxt = 137 (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' 138 FIRST' [match_tac ctxt (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt), 139 eq_assume_tac, ematch_tac ctxt @{thms FalseE}]; 140 141val safe_solver = mk_solver "HOL safe" safe_solver_tac; 142 143structure Splitter = Splitter 144( 145 val context = \<^context> 146 val mk_eq = mk_eq 147 val meta_eq_to_iff = @{thm meta_eq_to_obj_eq} 148 val iffD = @{thm iffD2} 149 val disjE = @{thm disjE} 150 val conjE = @{thm conjE} 151 val exE = @{thm exE} 152 val contrapos = @{thm contrapos_nn} 153 val contrapos2 = @{thm contrapos_pp} 154 val notnotD = @{thm notnotD} 155 val safe_tac = Classical.safe_tac 156); 157 158val split_tac = Splitter.split_tac; 159val split_inside_tac = Splitter.split_inside_tac; 160 161 162(* integration of simplifier with classical reasoner *) 163 164structure Clasimp = Clasimp 165( 166 structure Simplifier = Simplifier 167 and Splitter = Splitter 168 and Classical = Classical 169 and Blast = Blast 170 val iffD1 = @{thm iffD1} 171 val iffD2 = @{thm iffD2} 172 val notE = @{thm notE} 173); 174open Clasimp; 175 176val mksimps_pairs = 177 [(\<^const_name>\<open>HOL.implies\<close>, [@{thm mp}]), 178 (\<^const_name>\<open>HOL.conj\<close>, [@{thm conjunct1}, @{thm conjunct2}]), 179 (\<^const_name>\<open>All\<close>, [@{thm spec}]), 180 (\<^const_name>\<open>True\<close>, []), 181 (\<^const_name>\<open>False\<close>, []), 182 (\<^const_name>\<open>If\<close>, [@{thm if_bool_eq_conj} RS @{thm iffD1}])]; 183 184val HOL_basic_ss = 185 empty_simpset \<^context> 186 setSSolver safe_solver 187 setSolver unsafe_solver 188 |> Simplifier.set_subgoaler asm_simp_tac 189 |> Simplifier.set_mksimps (mksimps mksimps_pairs) 190 |> Simplifier.set_mkeqTrue mk_eq_True 191 |> Simplifier.set_mkcong mk_meta_cong 192 |> simpset_of; 193 194fun hol_simplify ctxt rews = 195 Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps rews); 196 197fun unfold_tac ctxt ths = 198 ALLGOALS (full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths)); 199 200end; 201 202structure Splitter = Simpdata.Splitter; 203structure Clasimp = Simpdata.Clasimp; 204