src/LCF/LCF.ML
changeset 0 a5a9c433f639
child 442 13ac1fd0a14d
equal deleted inserted replaced
-1:000000000000 0:a5a9c433f639
       
     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=>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,
       
   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