1461
|
1 |
(* Title: LCF/lcf.ML
|
0
|
2 |
ID: $Id$
|
1461
|
3 |
Author: Tobias Nipkow
|
0
|
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"
|
1461
|
56 |
(fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]);
|
0
|
57 |
|
|
58 |
val eq_imp_less2 = prove_goal thy "x=y ==> y << x"
|
1461
|
59 |
(fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]);
|
0
|
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"
|
1461
|
64 |
(fn prems => [rewtac eq_def,
|
|
65 |
REPEAT(rstac(conjI::prems)1)]);
|
0
|
66 |
|
|
67 |
val ext = prove_goal thy
|
3837
|
68 |
"(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))"
|
1461
|
69 |
(fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
|
|
70 |
prem RS eq_imp_less1,
|
|
71 |
prem RS eq_imp_less2]1)]);
|
0
|
72 |
|
|
73 |
val cong = prove_goal thy "[| f=g; x=y |] ==> f(x)=g(y)"
|
1461
|
74 |
(fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1,
|
|
75 |
rtac refl 1]);
|
0
|
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 |
|
3837
|
82 |
val UU_abs = prove_goal thy "(%x::'a::cpo. UU) = UU"
|
1461
|
83 |
(fn _ => [rtac less_anti_sym 1, rtac minimal 2,
|
|
84 |
rtac less_ext 1, rtac allI 1, rtac minimal 1]);
|
0
|
85 |
|
|
86 |
val UU_app = UU_abs RS sym RS ap_thm;
|
|
87 |
|
|
88 |
val less_UU = prove_goal thy "x << UU ==> x=UU"
|
1461
|
89 |
(fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]);
|
0
|
90 |
|
|
91 |
|
3837
|
92 |
val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)"
|
1461
|
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]);
|
0
|
96 |
|
|
97 |
|
|
98 |
val Contrapos = prove_goal thy "(A ==> B) ==> (~B ==> ~A)"
|
1461
|
99 |
(fn prems => [rtac notI 1, rtac notE 1, rstac prems 1,
|
|
100 |
rstac prems 1, atac 1]);
|
0
|
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=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))"
|
1461
|
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;
|
0
|
119 |
|
|
120 |
val lemma = prove_goal thy "A<->B ==> B ==> A"
|
1461
|
121 |
(fn prems => [cut_facts_tac prems 1, rewtac iff_def,
|
|
122 |
fast_tac FOL_cs 1]);
|
0
|
123 |
|
|
124 |
val COND_cases = conjI RSN (2,conjI RS (COND_cases_iff RS lemma));
|
|
125 |
|
|
126 |
end;
|
|
127 |
|
|
128 |
open LCF_Lemmas;
|
|
129 |
|