923

1 
(* Title: HOL/simpdata.ML


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1991 University of Cambridge


5 


6 
Instantiation of the generic simplifier


7 
*)


8 


9 
open Simplifier;


10 


11 
local


12 


13 
fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);


14 


15 
val P_imp_P_iff_True = prover "P > (P = True)" RS mp;


16 
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;


17 


18 
val not_P_imp_P_iff_F = prover "~P > (P = False)" RS mp;


19 
val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection;


20 


21 
fun atomize pairs =


22 
let fun atoms th =


23 
(case concl_of th of


24 
Const("Trueprop",_) $ p =>


25 
(case head_of p of


26 
Const(a,_) =>


27 
(case assoc(pairs,a) of


28 
Some(rls) => flat (map atoms ([th] RL rls))


29 
 None => [th])


30 
 _ => [th])


31 
 _ => [th])


32 
in atoms end;


33 


34 
fun mk_meta_eq r = case concl_of r of


35 
Const("==",_)$_$_ => r


36 
 _$(Const("op =",_)$_$_) => r RS eq_reflection


37 
 _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False


38 
 _ => r RS P_imp_P_eq_True;


39 
(* last 2 lines requires all formulae to be of the from Trueprop(.) *)


40 


41 
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;


42 


43 
val imp_cong = impI RSN


44 
(2, prove_goal HOL.thy "(P=P')> (P'> (Q=Q'))> ((P>Q) = (P'>Q'))"


45 
(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);


46 


47 
val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))"


48 
(fn _ => [rtac refl 1]);


49 


50 
val simp_thms = map prover


51 
[ "(x=x) = True",


52 
"(~True) = False", "(~False) = True", "(~ ~ P) = P",


53 
"(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",


54 
"(True=P) = P", "(P=True) = P",


55 
"(True > P) = P", "(False > P) = True",


56 
"(P > True) = True", "(P > P) = True",


57 
"(P > False) = (~P)", "(P > ~P) = (~P)",


58 
"(P & True) = P", "(True & P) = P",


59 
"(P & False) = False", "(False & P) = False", "(P & P) = P",


60 
"(P  True) = True", "(True  P) = True",


61 
"(P  False) = P", "(False  P) = P", "(P  P) = P",


62 
"(!x.P) = P", "(? x.P) = P", "? x. x=t", "(? x. x=t & P(x)) = P(t)",


63 
"(PQ > R) = ((P>R)&(Q>R))" ];


64 


65 
in


66 


67 
val meta_eq_to_obj_eq = prove_goal HOL.thy "x==y ==> x=y"


68 
(fn [prem] => [rewtac prem, rtac refl 1]);


69 


70 
val eq_sym_conv = prover "(x=y) = (y=x)";


71 


72 
val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";


73 


74 
val if_True = prove_goalw HOL.thy [if_def] "if True x y = x"


75 
(fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);


76 


77 
val if_False = prove_goalw HOL.thy [if_def] "if False x y = y"


78 
(fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);


79 


80 
val if_P = prove_goal HOL.thy "P ==> if P x y = x"


81 
(fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);


82 


83 
val if_not_P = prove_goal HOL.thy "~P ==> if P x y = y"


84 
(fn [prem] => [ stac (prem RS not_P_imp_P_iff_F) 1, rtac if_False 1 ]);


85 


86 
val expand_if = prove_goal HOL.thy


87 
"P(if Q x y) = ((Q > P(x)) & (~Q > P(y)))"


88 
(fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),


89 
rtac (if_P RS ssubst) 2,


90 
rtac (if_not_P RS ssubst) 1,


91 
REPEAT(fast_tac HOL_cs 1) ]);


92 


93 
val if_bool_eq = prove_goal HOL.thy "if P Q R = ((P>Q) & (~P>R))"


94 
(fn _ => [rtac expand_if 1]);


95 


96 
infix addcongs;


97 
fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);


98 


99 
val mksimps_pairs =


100 
[("op >", [mp]), ("op &", [conjunct1,conjunct2]),


101 
("All", [spec]), ("True", []), ("False", []),


102 
("if", [if_bool_eq RS iffD1])];


103 


104 
fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;


105 


106 
val HOL_ss = empty_ss


107 
setmksimps (mksimps mksimps_pairs)


108 
setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac


109 
ORELSE' etac FalseE)


110 
setsubgoaler asm_simp_tac


111 
addsimps ([if_True, if_False, o_apply, conj_assoc] @ simp_thms)


112 
addcongs [imp_cong];


113 


114 
fun split_tac splits =


115 
mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) (map mk_meta_eq splits);


116 


117 
(* eliminiation of existential quantifiers in assumptions *)


118 


119 
val ex_all_equiv =


120 
let val lemma1 = prove_goal HOL.thy


121 
"(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"


122 
(fn prems => [resolve_tac prems 1, etac exI 1]);


123 
val lemma2 = prove_goalw HOL.thy [Ex_def]


124 
"(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"


125 
(fn prems => [REPEAT(resolve_tac prems 1)])


126 
in equal_intr lemma1 lemma2 end;


127 


128 
(* '&' congruence rule: not included by default!


129 
May slow rewrite proofs down by as much as 50% *)


130 


131 
val conj_cong = impI RSN


132 
(2, prove_goal HOL.thy "(P=P')> (P'> (Q=Q'))> ((P&Q) = (P'&Q'))"


133 
(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);


134 


135 
(** 'if' congruence rules: neither included by default! *)


136 


137 
(*Simplifies x assuming c and y assuming ~c*)


138 
val if_cong = prove_goal HOL.thy


139 
"[ b=c; c ==> x=u; ~c ==> y=v ] ==> if b x y = if c u v"


140 
(fn rew::prems =>


141 
[stac rew 1, stac expand_if 1, stac expand_if 1,


142 
fast_tac (HOL_cs addDs prems) 1]);


143 


144 
(*Prevents simplification of x and y: much faster*)


145 
val if_weak_cong = prove_goal HOL.thy


146 
"b=c ==> if b x y = if c x y"


147 
(fn [prem] => [rtac (prem RS arg_cong) 1]);


148 


149 
(*Prevents simplification of t: much faster*)


150 
val let_weak_cong = prove_goal HOL.thy


151 
"a = b ==> (let x=a in t(x)) = (let x=b in t(x))"


152 
(fn [prem] => [rtac (prem RS arg_cong) 1]);


153 


154 
end;


155 


156 
fun prove nm thm = qed_goal nm HOL.thy thm (fn _ => [fast_tac HOL_cs 1]);


157 


158 
prove "conj_commute" "(P&Q) = (Q&P)";


159 
prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";


160 
val conj_comms = [conj_commute, conj_left_commute];


161 


162 
prove "conj_disj_distribL" "(P&(QR)) = (P&Q  P&R)";


163 
prove "conj_disj_distribR" "((PQ)&R) = (P&R  Q&R)";
