0

1 
(* Title: LCF/lcf.ML


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1992 University of Cambridge


5 


6 
For lcf.thy. Basic lemmas about LCF


7 
*)


8 


9 
open LCF;


10 


11 
signature LCF_LEMMAS =


12 
sig


13 
val ap_term: thm


14 
val ap_thm: thm


15 
val COND_cases: thm


16 
val COND_cases_iff: thm


17 
val Contrapos: thm


18 
val cong: thm


19 
val ext: thm


20 
val eq_imp_less1: thm


21 
val eq_imp_less2: thm


22 
val less_anti_sym: thm


23 
val less_ap_term: thm


24 
val less_ap_thm: thm


25 
val less_refl: thm


26 
val less_UU: thm


27 
val not_UU_eq_TT: thm


28 
val not_UU_eq_FF: thm


29 
val not_TT_eq_UU: thm


30 
val not_TT_eq_FF: thm


31 
val not_FF_eq_UU: thm


32 
val not_FF_eq_TT: thm


33 
val rstac: thm list > int > tactic


34 
val stac: thm > int > tactic


35 
val sstac: thm list > int > tactic


36 
val strip_tac: int > tactic


37 
val tr_induct: thm


38 
val UU_abs: thm


39 
val UU_app: thm


40 
end;


41 


42 


43 
structure LCF_Lemmas : LCF_LEMMAS =


44 


45 
struct


46 


47 
(* Standard abbreviations *)


48 


49 
val rstac = resolve_tac;


50 
fun stac th = rtac(th RS sym RS subst);


51 
fun sstac ths = EVERY' (map stac ths);


52 


53 
fun strip_tac i = REPEAT(rstac [impI,allI] i);


54 


55 
val eq_imp_less1 = prove_goal thy "x=y ==> x << y"


56 
(fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]);


57 


58 
val eq_imp_less2 = prove_goal thy "x=y ==> y << x"


59 
(fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]);


60 


61 
val less_refl = refl RS eq_imp_less1;


62 


63 
val less_anti_sym = prove_goal thy "[ x << y; y << x ] ==> x=y"


64 
(fn prems => [rewrite_goals_tac[eq_def],


65 
REPEAT(rstac(conjI::prems)1)]);


66 


67 
val ext = prove_goal thy


68 
"(!!x::'a::cpo. f(x)=g(x)::'b::cpo) ==> (%x.f(x))=(%x.g(x))"


69 
(fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,


70 
prem RS eq_imp_less1,


71 
prem RS eq_imp_less2]1)]);


72 


73 
val cong = prove_goal thy "[ f=g; x=y ] ==> f(x)=g(y)"


74 
(fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1,


75 
rtac refl 1]);


76 


77 
val less_ap_term = less_refl RS mono;


78 
val less_ap_thm = less_refl RSN (2,mono);


79 
val ap_term = refl RS cong;


80 
val ap_thm = refl RSN (2,cong);


81 


82 
val UU_abs = prove_goal thy "(%x::'a::cpo.UU) = UU"


83 
(fn _ => [rtac less_anti_sym 1, rtac minimal 2,


84 
rtac less_ext 1, rtac allI 1, rtac minimal 1]);


85 


86 
val UU_app = UU_abs RS sym RS ap_thm;


87 


88 
val less_UU = prove_goal thy "x << UU ==> x=UU"


89 
(fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]);


90 


91 


92 
val tr_induct = prove_goal thy "[ P(UU); P(TT); P(FF) ] ==> ALL b.P(b)"


93 
(fn prems => [rtac allI 1, rtac mp 1,


94 
res_inst_tac[("p","b")]tr_cases 2,


95 
fast_tac (FOL_cs addIs prems) 1]);


96 


97 


98 
val Contrapos = prove_goal thy "(A ==> B) ==> (~B ==> ~A)"


99 
(fn prems => [rtac notI 1, rtac notE 1, rstac prems 1,


100 
rstac prems 1, atac 1]);


101 


102 
val not_less_imp_not_eq1 = eq_imp_less1 COMP Contrapos;


103 
val not_less_imp_not_eq2 = eq_imp_less2 COMP Contrapos;


104 


105 
val not_UU_eq_TT = not_TT_less_UU RS not_less_imp_not_eq2;


106 
val not_UU_eq_FF = not_FF_less_UU RS not_less_imp_not_eq2;


107 
val not_TT_eq_UU = not_TT_less_UU RS not_less_imp_not_eq1;


108 
val not_TT_eq_FF = not_TT_less_FF RS not_less_imp_not_eq1;


109 
val not_FF_eq_UU = not_FF_less_UU RS not_less_imp_not_eq1;


110 
val not_FF_eq_TT = not_FF_less_TT RS not_less_imp_not_eq1;


111 


112 


113 
val COND_cases_iff = (prove_goal thy


114 
"ALL b. P(b=>xy) <> (b=UU>P(UU)) & (b=TT>P(x)) & (b=FF>P(y))"


115 
(fn _ => [cut_facts_tac [not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,


116 
not_TT_eq_FF,not_FF_eq_UU,not_FF_eq_TT]1,


117 
rtac tr_induct 1, stac COND_UU 1, stac COND_TT 2,


118 
stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)])) RS spec;


119 


120 
val lemma = prove_goal thy "A<>B ==> B ==> A"


121 
(fn prems => [cut_facts_tac prems 1, rewrite_goals_tac [iff_def],


122 
fast_tac FOL_cs 1]);


123 


124 
val COND_cases = conjI RSN (2,conjI RS (COND_cases_iff RS lemma));


125 


126 
end;


127 


128 
open LCF_Lemmas;


129 
