0

1 
(* Title: FOL/simpdata


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

282

4 
Copyright 1994 University of Cambridge

0

5 


6 
Simplification data for FOL


7 
*)


8 


9 
(*** Rewrite rules ***)


10 


11 
fun int_prove_fun s =

282

12 
(writeln s;


13 
prove_goal IFOL.thy s


14 
(fn prems => [ (cut_facts_tac prems 1),


15 
(Int.fast_tac 1) ]));

0

16 


17 
val conj_rews = map int_prove_fun

282

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

0

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


20 
"P & P <> P",

282

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

0

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


23 


24 
val disj_rews = map int_prove_fun


25 
["P  True <> True", "True  P <> True",


26 
"P  False <> P", "False  P <> P",


27 
"P  P <> P",


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


29 


30 
val not_rews = map int_prove_fun

282

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


32 
"~ False <> True", "~ True <> False"];

0

33 


34 
val imp_rews = map int_prove_fun


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


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


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


38 


39 
val iff_rews = map int_prove_fun


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


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


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


43 


44 
val quant_rews = map int_prove_fun


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


46 


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


48 
val distrib_rews = map int_prove_fun

282

49 
["P & (Q  R) <> P&Q  P&R",


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

0

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


52 

282

53 
(** Conversion into rewrite rules **)

0

54 

53

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


56 

282

57 
(*Make atomic rewrite rules*)


58 
fun atomize th = case concl_of th of


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


60 
atomize(th RS conjunct2)


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


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


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


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


65 
 _ => [th];


66 


67 
val P_iff_F = int_prove_fun "~P ==> (P <> False)";


68 
val iff_reflection_F = P_iff_F RS iff_reflection;


69 


70 
val P_iff_T = int_prove_fun "P ==> (P <> True)";


71 
val iff_reflection_T = P_iff_T RS iff_reflection;


72 


73 
(*Make metaequalities. The operator below is Trueprop*)


74 
fun mk_meta_eq th = case concl_of th of


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


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


77 
 _ $ (Const("Not",_)$_) => th RS iff_reflection_F


78 
 _ => th RS iff_reflection_T;

0

79 


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


81 


82 
open Simplifier Induction;


83 

3

84 
infix addcongs;


85 
fun ss addcongs congs =

282

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


87 


88 
val IFOL_rews =


89 
[refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @


90 
imp_rews @ iff_rews @ quant_rews;

3

91 

282

92 
val notFalseI = int_prove_fun "~False";


93 
val triv_rls = [TrueI,refl,iff_refl,notFalseI];


94 


95 
val IFOL_ss =


96 
empty_ss


97 
setmksimps (map mk_meta_eq o atomize o gen_all)


98 
setsolver (fn prems => resolve_tac (triv_rls@prems) ORELSE' assume_tac)


99 
setsubgoaler asm_simp_tac


100 
addsimps IFOL_rews


101 
addcongs [imp_cong];

0

102 


103 
(*Classical version...*)


104 
fun prove_fun s =

282

105 
(writeln s;


106 
prove_goal FOL.thy s


107 
(fn prems => [ (cut_facts_tac prems 1),


108 
(Cla.fast_tac FOL_cs 1) ]));

0

109 
val cla_rews = map prove_fun

282

110 
["~(P&Q) <> ~P  ~Q",


111 
"P  ~P", "~P  P",

0

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


113 


114 
val FOL_ss = IFOL_ss addsimps cla_rews;


115 


116 
(*** case splitting ***)


117 

282

118 
val meta_iffD =


119 
prove_goal FOL.thy "[ P==Q; Q ] ==> P"


120 
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])


121 


122 
fun split_tac splits =


123 
mk_case_split_tac meta_iffD (map mk_meta_eq splits);
