0

1 
(* Title: FOL/simpdata


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
Simplification data for FOL


7 
*)


8 


9 
(*** Rewrite rules ***)


10 


11 
fun int_prove_fun s =


12 
(writeln s; prove_goal IFOL.thy s


13 
(fn prems => [ (cut_facts_tac prems 1), (Int.fast_tac 1) ]));


14 


15 
val conj_rews = map int_prove_fun


16 
["P & True <> P", "True & P <> P",


17 
"P & False <> False", "False & P <> False",


18 
"P & P <> P",


19 
"P & ~P <> False", "~P & P <> False",


20 
"(P & Q) & R <> P & (Q & R)"];


21 


22 
val disj_rews = map int_prove_fun


23 
["P  True <> True", "True  P <> True",


24 
"P  False <> P", "False  P <> P",


25 
"P  P <> P",


26 
"(P  Q)  R <> P  (Q  R)"];


27 


28 
val not_rews = map int_prove_fun


29 
["~ False <> True", "~ True <> False"];


30 


31 
val imp_rews = map int_prove_fun


32 
["(P > False) <> ~P", "(P > True) <> True",


33 
"(False > P) <> True", "(True > P) <> P",


34 
"(P > P) <> True", "(P > ~P) <> ~P"];


35 


36 
val iff_rews = map int_prove_fun


37 
["(True <> P) <> P", "(P <> True) <> P",


38 
"(P <> P) <> True",


39 
"(False <> P) <> ~P", "(P <> False) <> ~P"];


40 


41 
val quant_rews = map int_prove_fun


42 
["(ALL x.P) <> P", "(EX x.P) <> P"];


43 


44 
(*These are NOT supplied by default!*)


45 
val distrib_rews = map int_prove_fun


46 
["~(PQ) <> ~P & ~Q",


47 
"P & (Q  R) <> P&Q  P&R", "(Q  R) & P <> Q&P  R&P",


48 
"(P  Q > R) <> (P > R) & (Q > R)"];


49 


50 
val P_Imp_P_iff_T = int_prove_fun "P ==> (P <> True)";


51 


52 
fun make_iff_T th = th RS P_Imp_P_iff_T;


53 


54 
val refl_iff_T = make_iff_T refl;


55 


56 
val notFalseI = int_prove_fun "~False";


57 


58 
(* Conversion into rewrite rules *)


59 


60 
val not_P_imp_P_iff_F = int_prove_fun "~P ==> (P <> False)";


61 


62 
fun mk_meta_eq th = case concl_of th of


63 
_ $ (Const("op <>",_)$_$_) => th RS iff_reflection


64 
 _ $ (Const("op =",_)$_$_) => th RS eq_reflection


65 
 _ $ (Const("Not",_)$_) => (th RS not_P_imp_P_iff_F) RS iff_reflection


66 
 _ => (make_iff_T th) RS iff_reflection;


67 


68 
fun atomize th = case concl_of th of (*The operator below is Trueprop*)


69 
_ $ (Const("op >",_) $ _ $ _) => atomize(th RS mp)


70 
 _ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) @


71 
atomize(th RS conjunct2)


72 
 _ $ (Const("All",_) $ _) => atomize(th RS spec)


73 
 _ $ (Const("True",_)) => []


74 
 _ $ (Const("False",_)) => []


75 
 _ => [th];


76 


77 
fun mk_rew_rules th = map mk_meta_eq (atomize th);


78 


79 
structure Induction = InductionFun(struct val spec=IFOL.spec end);


80 


81 
val IFOL_rews =


82 
[refl_iff_T] @ conj_rews @ disj_rews @ not_rews @


83 
imp_rews @ iff_rews @ quant_rews;


84 


85 
open Simplifier Induction;


86 

3

87 
infix addcongs;


88 
fun ss addcongs congs =


89 
ss addeqcongs (congs RL [eq_reflection,iff_reflection]);


90 

0

91 
val IFOL_ss = empty_ss


92 
setmksimps mk_rew_rules


93 
setsolver


94 
(fn prems => resolve_tac (TrueI::refl::iff_refl::notFalseI::prems))


95 
setsubgoaler asm_simp_tac


96 
addsimps IFOL_rews

3

97 
addcongs [imp_cong];

0

98 


99 
(*Classical version...*)


100 
fun prove_fun s =


101 
(writeln s; prove_goal FOL.thy s


102 
(fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOL_cs 1) ]));


103 


104 
val cla_rews = map prove_fun


105 
["P  ~P", "~P  P",


106 
"~ ~ P <> P", "(~P > P) <> P"];


107 


108 
val FOL_ss = IFOL_ss addsimps cla_rews;


109 


110 
(*** case splitting ***)


111 


112 
val split_tac =


113 
let val eq_reflection2 = prove_goal FOL.thy "x==y ==> x=y"


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


115 
val iff_reflection2 = prove_goal FOL.thy "x==y ==> x<>y"


116 
(fn [prem] => [rewtac prem, rtac iff_refl 1])


117 
val [iffD] = [eq_reflection2,iff_reflection2] RL [iffD2]


118 
in fn splits => mk_case_split_tac iffD (map mk_meta_eq splits) end;
