1(* Title: FOL/simpdata.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1994 University of Cambridge 4 5Simplification data for FOL. 6*) 7 8(*Make meta-equalities. The operator below is Trueprop*) 9 10fun mk_meta_eq th = 11 (case Thm.concl_of th of 12 _ $ (Const(\<^const_name>\<open>eq\<close>,_)$_$_) => th RS @{thm eq_reflection} 13 | _ $ (Const(\<^const_name>\<open>iff\<close>,_)$_$_) => th RS @{thm iff_reflection} 14 | _ => error "conclusion must be a =-equality or <->"); 15 16fun mk_eq th = 17 (case Thm.concl_of th of 18 Const(\<^const_name>\<open>Pure.eq\<close>,_)$_$_ => th 19 | _ $ (Const(\<^const_name>\<open>eq\<close>,_)$_$_) => mk_meta_eq th 20 | _ $ (Const(\<^const_name>\<open>iff\<close>,_)$_$_) => mk_meta_eq th 21 | _ $ (Const(\<^const_name>\<open>Not\<close>,_)$_) => th RS @{thm iff_reflection_F} 22 | _ => th RS @{thm iff_reflection_T}); 23 24(*Replace premises x=y, X<->Y by X==Y*) 25fun mk_meta_prems ctxt = 26 rule_by_tactic ctxt 27 (REPEAT_FIRST (resolve_tac ctxt [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); 28 29(*Congruence rules for = or <-> (instead of ==)*) 30fun mk_meta_cong ctxt rl = 31 Drule.zero_var_indexes (mk_meta_eq (mk_meta_prems ctxt rl)) 32 handle THM _ => 33 error("Premises and conclusion of congruence rules must use =-equality or <->"); 34 35val mksimps_pairs = 36 [(\<^const_name>\<open>imp\<close>, [@{thm mp}]), (\<^const_name>\<open>conj\<close>, [@{thm conjunct1}, @{thm conjunct2}]), 37 (\<^const_name>\<open>All\<close>, [@{thm spec}]), (\<^const_name>\<open>True\<close>, []), (\<^const_name>\<open>False\<close>, [])]; 38 39fun mk_atomize pairs = 40 let 41 fun atoms th = 42 (case Thm.concl_of th of 43 Const(\<^const_name>\<open>Trueprop\<close>,_) $ p => 44 (case head_of p of 45 Const(a,_) => 46 (case AList.lookup (op =) pairs a of 47 SOME(rls) => maps atoms ([th] RL rls) 48 | NONE => [th]) 49 | _ => [th]) 50 | _ => [th]) 51 in atoms end; 52 53fun mksimps pairs ctxt = map mk_eq o mk_atomize pairs o Variable.gen_all ctxt; 54 55 56(** make simplification procedures for quantifier elimination **) 57structure Quantifier1 = Quantifier1 58( 59 (*abstract syntax*) 60 fun dest_eq (Const (\<^const_name>\<open>eq\<close>, _) $ s $ t) = SOME (s, t) 61 | dest_eq _ = NONE 62 fun dest_conj (Const (\<^const_name>\<open>conj\<close>, _) $ s $ t) = SOME (s, t) 63 | dest_conj _ = NONE 64 fun dest_imp (Const (\<^const_name>\<open>imp\<close>, _) $ s $ t) = SOME (s, t) 65 | dest_imp _ = NONE 66 val conj = FOLogic.conj 67 val imp = FOLogic.imp 68 (*rules*) 69 val iff_reflection = @{thm iff_reflection} 70 val iffI = @{thm iffI} 71 val iff_trans = @{thm iff_trans} 72 val conjI= @{thm conjI} 73 val conjE= @{thm conjE} 74 val impI = @{thm impI} 75 val mp = @{thm mp} 76 val uncurry = @{thm uncurry} 77 val exI = @{thm exI} 78 val exE = @{thm exE} 79 val iff_allI = @{thm iff_allI} 80 val iff_exI = @{thm iff_exI} 81 val all_comm = @{thm all_comm} 82 val ex_comm = @{thm ex_comm} 83); 84 85 86(*** Case splitting ***) 87 88structure Splitter = Splitter 89( 90 val context = \<^context> 91 val mk_eq = mk_eq 92 val meta_eq_to_iff = @{thm meta_eq_to_iff} 93 val iffD = @{thm iffD2} 94 val disjE = @{thm disjE} 95 val conjE = @{thm conjE} 96 val exE = @{thm exE} 97 val contrapos = @{thm contrapos} 98 val contrapos2 = @{thm contrapos2} 99 val notnotD = @{thm notnotD} 100 val safe_tac = Cla.safe_tac 101); 102 103val split_tac = Splitter.split_tac; 104val split_inside_tac = Splitter.split_inside_tac; 105val split_asm_tac = Splitter.split_asm_tac; 106 107 108(*** Standard simpsets ***) 109 110val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}]; 111 112fun unsafe_solver ctxt = 113 FIRST' [resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt), 114 assume_tac ctxt, 115 eresolve_tac ctxt @{thms FalseE}]; 116 117(*No premature instantiation of variables during simplification*) 118fun safe_solver ctxt = 119 FIRST' [match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt), 120 eq_assume_tac, ematch_tac ctxt @{thms FalseE}]; 121 122(*No simprules, but basic infastructure for simplification*) 123val FOL_basic_ss = 124 empty_simpset \<^context> 125 setSSolver (mk_solver "FOL safe" safe_solver) 126 setSolver (mk_solver "FOL unsafe" unsafe_solver) 127 |> Simplifier.set_subgoaler asm_simp_tac 128 |> Simplifier.set_mksimps (mksimps mksimps_pairs) 129 |> Simplifier.set_mkcong mk_meta_cong 130 |> simpset_of; 131 132fun unfold_tac ctxt ths = 133 ALLGOALS (full_simp_tac (clear_simpset (put_simpset FOL_basic_ss ctxt) addsimps ths)); 134 135 136(*** integration of simplifier with classical reasoner ***) 137 138structure Clasimp = Clasimp 139( 140 structure Simplifier = Simplifier 141 and Splitter = Splitter 142 and Classical = Cla 143 and Blast = Blast 144 val iffD1 = @{thm iffD1} 145 val iffD2 = @{thm iffD2} 146 val notE = @{thm notE} 147); 148open Clasimp; 149 150