src/HOLCF/Tr.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5143 b94cd208f073
child 7654 57c4cea8b137
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/Tr.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for Tr.thy
     7 *)
     8 
     9 open Tr;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* Exhaustion and Elimination for type one                                  *)
    13 (* ------------------------------------------------------------------------ *)
    14 qed_goalw "Exh_tr" thy [FF_def,TT_def] "t=UU | t = TT | t = FF"
    15  (fn prems =>
    16         [
    17 	(lift.induct_tac "t" 1),
    18 	(fast_tac HOL_cs 1),
    19 	(fast_tac (HOL_cs addss simpset()) 1)
    20 	]);
    21 
    22 qed_goal "trE" thy
    23         "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
    24  (fn prems =>
    25         [
    26         (rtac (Exh_tr RS disjE) 1),
    27         (eresolve_tac prems 1),
    28         (etac disjE 1),
    29         (eresolve_tac prems 1),
    30         (eresolve_tac prems 1)
    31         ]);
    32 
    33 (* ------------------------------------------------------------------------ *) 
    34 (* tactic for tr-thms with case split                                       *)
    35 (* ------------------------------------------------------------------------ *)
    36 
    37 val tr_defs = [andalso_def,orelse_def,neg_def,ifte_def,TT_def,FF_def];
    38 
    39 fun prover t =  prove_goal thy t
    40  (fn prems =>
    41         [
    42         (res_inst_tac [("p","y")] trE 1),
    43 	(REPEAT(asm_simp_tac (simpset() addsimps 
    44 		[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
    45 	]);
    46 
    47 (* ------------------------------------------------------------------------ *) 
    48 (* distinctness for type tr                                                 *) 
    49 (* ------------------------------------------------------------------------ *)
    50 
    51 val dist_less_tr = map prover [
    52 			"~TT << UU",
    53 			"~FF << UU",
    54 			"~TT << FF",
    55 			"~FF << TT"
    56                         ];
    57 
    58 val dist_eq_tr = map prover ["TT~=UU","FF~=UU","TT~=FF"];
    59 val dist_eq_tr = dist_eq_tr @ (map (fn thm => (thm RS not_sym)) dist_eq_tr);
    60 
    61 (* ------------------------------------------------------------------------ *) 
    62 (* lemmas about andalso, orelse, neg and if                                 *) 
    63 (* ------------------------------------------------------------------------ *)
    64 
    65 val andalso_thms = map prover [
    66                         "(TT andalso y) = y",
    67                         "(FF andalso y) = FF",
    68                         "(UU andalso y) = UU",
    69 			"(y andalso TT) = y",
    70 		  	"(y andalso y) = y"
    71                         ];
    72 
    73 val orelse_thms = map prover [
    74                         "(TT orelse y) = TT",
    75                         "(FF orelse y) = y",
    76                         "(UU orelse y) = UU",
    77                         "(y orelse FF) = y",
    78 			"(y orelse y) = y"];
    79 
    80 val neg_thms = map prover [
    81                         "neg`TT = FF",
    82                         "neg`FF = TT",
    83                         "neg`UU = UU"
    84                         ];
    85 
    86 val ifte_thms = map prover [
    87                         "If UU then e1 else e2 fi = UU",
    88                         "If FF then e1 else e2 fi = e2",
    89                         "If TT then e1 else e2 fi = e1"];
    90 
    91 Addsimps (dist_less_tr @ dist_eq_tr @ andalso_thms @ 
    92 	  orelse_thms @ neg_thms @ ifte_thms);
    93 
    94 (* ------------------------------------------------------------------- *)
    95 (*  split-tac for If via If2 because the constant has to be a constant *)
    96 (* ------------------------------------------------------------------- *)
    97   
    98 Goalw [If2_def] 
    99   "P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))";
   100 by (res_inst_tac [("p","Q")] trE 1);
   101 by (REPEAT (Asm_full_simp_tac 1));
   102 qed"split_If2";
   103 
   104 val split_If_tac =
   105   simp_tac (HOL_basic_ss addsimps [symmetric If2_def]) THEN' (split_tac [split_If2]);
   106 
   107  
   108 
   109 (* ----------------------------------------------------------------- *)
   110         section"Rewriting of HOLCF operations to HOL functions";
   111 (* ----------------------------------------------------------------- *)
   112 
   113 
   114 Goal
   115 "!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)";
   116 by (rtac iffI 1);
   117 by (res_inst_tac [("p","t")] trE 1);
   118 by Auto_tac;
   119 by (res_inst_tac [("p","t")] trE 1);
   120 by Auto_tac;
   121 qed"andalso_or";
   122 
   123 Goal "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
   124 by (rtac iffI 1);
   125 by (res_inst_tac [("p","t")] trE 1);
   126 by Auto_tac;
   127 by (res_inst_tac [("p","t")] trE 1);
   128 by Auto_tac;
   129 qed"andalso_and";
   130 
   131 Goal "(Def x ~=FF)= x";
   132 by (simp_tac (simpset() addsimps [FF_def]) 1);
   133 qed"Def_bool1";
   134 
   135 Goal "(Def x = FF) = (~x)";
   136 by (simp_tac (simpset() addsimps [FF_def]) 1);
   137 qed"Def_bool2";
   138 
   139 Goal "(Def x = TT) = x";
   140 by (simp_tac (simpset() addsimps [TT_def]) 1);
   141 qed"Def_bool3";
   142 
   143 Goal "(Def x ~= TT) = (~x)";
   144 by (simp_tac (simpset() addsimps [TT_def]) 1);
   145 qed"Def_bool4";
   146 
   147 Goal 
   148   "(If Def P then A else B fi)= (if P then A else B)";
   149 by (res_inst_tac [("p","Def P")]  trE 1);
   150 by (Asm_full_simp_tac 1);
   151 by (asm_full_simp_tac (simpset() addsimps tr_defs@[flift1_def,o_def]) 1);
   152 by (asm_full_simp_tac (simpset() addsimps tr_defs@[flift1_def,o_def]) 1);
   153 qed"If_and_if";
   154 
   155 Addsimps [Def_bool1,Def_bool2,Def_bool3,Def_bool4];
   156 
   157 (* ----------------------------------------------------------------- *)
   158         section"admissibility";
   159 (* ----------------------------------------------------------------- *)
   160 
   161 
   162 (* The following rewrite rules for admissibility should in the future be 
   163    replaced by a more general admissibility test that also checks 
   164    chain-finiteness, of which these lemmata are specific examples *)
   165 
   166 Goal "x~=FF = (x=TT|x=UU)";
   167 by (res_inst_tac [("p","x")] trE 1);
   168 by (TRYALL (Asm_full_simp_tac));
   169 qed"adm_trick_1";
   170 
   171 Goal "x~=TT = (x=FF|x=UU)";
   172 by (res_inst_tac [("p","x")] trE 1);
   173 by (TRYALL (Asm_full_simp_tac));
   174 qed"adm_trick_2";
   175 
   176 val adm_tricks = [adm_trick_1,adm_trick_2];
   177 
   178 
   179 Goal "cont(f) ==> adm (%x. (f x)~=TT)";
   180 by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
   181 by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
   182 qed"adm_nTT";
   183 
   184 Goal "cont(f) ==> adm (%x. (f x)~=FF)";
   185 by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
   186 by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
   187 qed"adm_nFF";
   188 
   189 Addsimps [adm_nTT,adm_nFF];