51 fun sstac ths = EVERY' (map stac ths); |
51 fun sstac ths = EVERY' (map stac ths); |
52 |
52 |
53 fun strip_tac i = REPEAT(rstac [impI,allI] i); |
53 fun strip_tac i = REPEAT(rstac [impI,allI] i); |
54 |
54 |
55 val eq_imp_less1 = prove_goal thy "x=y ==> x << y" |
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]); |
56 (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]); |
57 |
57 |
58 val eq_imp_less2 = prove_goal thy "x=y ==> y << x" |
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]); |
59 (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]); |
60 |
60 |
61 val less_refl = refl RS eq_imp_less1; |
61 val less_refl = refl RS eq_imp_less1; |
62 |
62 |
63 val less_anti_sym = prove_goal thy "[| x << y; y << x |] ==> x=y" |
63 val less_anti_sym = prove_goal thy "[| x << y; y << x |] ==> x=y" |
64 (fn prems => [rewrite_goals_tac[eq_def], |
64 (fn prems => [rewtac eq_def, |
65 REPEAT(rstac(conjI::prems)1)]); |
65 REPEAT(rstac(conjI::prems)1)]); |
66 |
66 |
67 val ext = prove_goal thy |
67 val ext = prove_goal thy |
68 "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x.f(x))=(%x.g(x))" |
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, |
69 (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI, |
70 prem RS eq_imp_less1, |
70 prem RS eq_imp_less1, |
71 prem RS eq_imp_less2]1)]); |
71 prem RS eq_imp_less2]1)]); |
72 |
72 |
73 val cong = prove_goal thy "[| f=g; x=y |] ==> f(x)=g(y)" |
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, |
74 (fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1, |
75 rtac refl 1]); |
75 rtac refl 1]); |
76 |
76 |
77 val less_ap_term = less_refl RS mono; |
77 val less_ap_term = less_refl RS mono; |
78 val less_ap_thm = less_refl RSN (2,mono); |
78 val less_ap_thm = less_refl RSN (2,mono); |
79 val ap_term = refl RS cong; |
79 val ap_term = refl RS cong; |
80 val ap_thm = refl RSN (2,cong); |
80 val ap_thm = refl RSN (2,cong); |
81 |
81 |
82 val UU_abs = prove_goal thy "(%x::'a::cpo.UU) = UU" |
82 val UU_abs = prove_goal thy "(%x::'a::cpo.UU) = UU" |
83 (fn _ => [rtac less_anti_sym 1, rtac minimal 2, |
83 (fn _ => [rtac less_anti_sym 1, rtac minimal 2, |
84 rtac less_ext 1, rtac allI 1, rtac minimal 1]); |
84 rtac less_ext 1, rtac allI 1, rtac minimal 1]); |
85 |
85 |
86 val UU_app = UU_abs RS sym RS ap_thm; |
86 val UU_app = UU_abs RS sym RS ap_thm; |
87 |
87 |
88 val less_UU = prove_goal thy "x << UU ==> x=UU" |
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]); |
89 (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]); |
90 |
90 |
91 |
91 |
92 val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b.P(b)" |
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, |
93 (fn prems => [rtac allI 1, rtac mp 1, |
94 res_inst_tac[("p","b")]tr_cases 2, |
94 res_inst_tac[("p","b")]tr_cases 2, |
95 fast_tac (FOL_cs addIs prems) 1]); |
95 fast_tac (FOL_cs addIs prems) 1]); |
96 |
96 |
97 |
97 |
98 val Contrapos = prove_goal thy "(A ==> B) ==> (~B ==> ~A)" |
98 val Contrapos = prove_goal thy "(A ==> B) ==> (~B ==> ~A)" |
99 (fn prems => [rtac notI 1, rtac notE 1, rstac prems 1, |
99 (fn prems => [rtac notI 1, rtac notE 1, rstac prems 1, |
100 rstac prems 1, atac 1]); |
100 rstac prems 1, atac 1]); |
101 |
101 |
102 val not_less_imp_not_eq1 = eq_imp_less1 COMP Contrapos; |
102 val not_less_imp_not_eq1 = eq_imp_less1 COMP Contrapos; |
103 val not_less_imp_not_eq2 = eq_imp_less2 COMP Contrapos; |
103 val not_less_imp_not_eq2 = eq_imp_less2 COMP Contrapos; |
104 |
104 |
105 val not_UU_eq_TT = not_TT_less_UU RS not_less_imp_not_eq2; |
105 val not_UU_eq_TT = not_TT_less_UU RS not_less_imp_not_eq2; |
110 val not_FF_eq_TT = not_FF_less_TT RS not_less_imp_not_eq1; |
110 val not_FF_eq_TT = not_FF_less_TT RS not_less_imp_not_eq1; |
111 |
111 |
112 |
112 |
113 val COND_cases_iff = (prove_goal thy |
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))" |
114 "ALL b. P(b=>x|y) <-> (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, |
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, |
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, |
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; |
118 stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)])) RS spec; |
119 |
119 |
120 val lemma = prove_goal thy "A<->B ==> B ==> A" |
120 val lemma = prove_goal thy "A<->B ==> B ==> A" |
121 (fn prems => [cut_facts_tac prems 1, rewrite_goals_tac [iff_def], |
121 (fn prems => [cut_facts_tac prems 1, rewtac iff_def, |
122 fast_tac FOL_cs 1]); |
122 fast_tac FOL_cs 1]); |
123 |
123 |
124 val COND_cases = conjI RSN (2,conjI RS (COND_cases_iff RS lemma)); |
124 val COND_cases = conjI RSN (2,conjI RS (COND_cases_iff RS lemma)); |
125 |
125 |
126 end; |
126 end; |
127 |
127 |