src/LCF/LCF.ML
 changeset 1461 6bcb44e4d6e5 parent 442 13ac1fd0a14d child 3837 d7f033c74b38
equal inserted replaced
1460:5a6f2aabd538 1461:6bcb44e4d6e5
`     1 (*  Title: 	LCF/lcf.ML`
`     1 (*  Title:      LCF/lcf.ML`
`     2     ID:         \$Id\$`
`     2     ID:         \$Id\$`
`     3     Author: 	Tobias Nipkow`
`     3     Author:     Tobias Nipkow`
`     4     Copyright   1992  University of Cambridge`
`     4     Copyright   1992  University of Cambridge`
`     5 `
`     5 `
`     6 For lcf.thy.  Basic lemmas about LCF`
`     6 For lcf.thy.  Basic lemmas about LCF`
`     7 *)`
`     7 *)`
`     8 `
`     8 `
`    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 `