convert to new-style theory
authorhuffman
Fri Apr 01 23:44:41 2005 +0200 (2005-04-01 ago)
changeset 15649f8345ee4f607
parent 15648 f6da795ee27a
child 15650 b37dc98fbbc5
convert to new-style theory
src/HOLCF/Tr.ML
src/HOLCF/Tr.thy
     1.1 --- a/src/HOLCF/Tr.ML	Fri Apr 01 21:04:00 2005 +0200
     1.2 +++ b/src/HOLCF/Tr.ML	Fri Apr 01 23:44:41 2005 +0200
     1.3 @@ -1,182 +1,34 @@
     1.4 -(*  Title:      HOLCF/Tr.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Franz Regensburger
     1.7  
     1.8 -Introduce infix if_then_else_fi and boolean connectives andalso, orelse
     1.9 -*)
    1.10 -
    1.11 -(* ------------------------------------------------------------------------ *)
    1.12 -(* Exhaustion and Elimination for type one                                  *)
    1.13 -(* ------------------------------------------------------------------------ *)
    1.14 -
    1.15 -Goalw [FF_def,TT_def] "t=UU | t = TT | t = FF";
    1.16 -by (induct_tac "t" 1);
    1.17 -by (fast_tac HOL_cs 1);
    1.18 -by (fast_tac (HOL_cs addss simpset()) 1);
    1.19 -qed "Exh_tr";
    1.20 -
    1.21 -val prems = Goal "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q";
    1.22 -by (rtac (Exh_tr RS disjE) 1);
    1.23 -by (eresolve_tac prems 1);
    1.24 -by (etac disjE 1);
    1.25 -by (eresolve_tac prems 1);
    1.26 -by (eresolve_tac prems 1);
    1.27 -qed "trE";
    1.28 -
    1.29 -(* ------------------------------------------------------------------------ *) 
    1.30 -(* tactic for tr-thms with case split                                       *)
    1.31 -(* ------------------------------------------------------------------------ *)
    1.32 -
    1.33 -bind_thms ("tr_defs", [andalso_def,orelse_def,neg_def,ifte_def,TT_def,FF_def]);
    1.34 -
    1.35 -fun prover t =  prove_goal thy t
    1.36 - (fn prems =>
    1.37 -        [
    1.38 -        (res_inst_tac [("p","y")] trE 1),
    1.39 -	(REPEAT(asm_simp_tac (simpset() addsimps 
    1.40 -		[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
    1.41 -	]);
    1.42 -
    1.43 -(* ------------------------------------------------------------------------ *) 
    1.44 -(* distinctness for type tr                                                 *) 
    1.45 -(* ------------------------------------------------------------------------ *)
    1.46 -
    1.47 -bind_thms ("dist_less_tr", map prover [
    1.48 -			"~TT << UU",
    1.49 -			"~FF << UU",
    1.50 -			"~TT << FF",
    1.51 -			"~FF << TT"
    1.52 -                        ]);
    1.53 -
    1.54 -val dist_eq_tr = map prover ["TT~=UU","FF~=UU","TT~=FF"];
    1.55 -bind_thms ("dist_eq_tr", dist_eq_tr @ (map (fn thm => (thm RS not_sym)) dist_eq_tr));
    1.56 -
    1.57 -(* ------------------------------------------------------------------------ *) 
    1.58 -(* lemmas about andalso, orelse, neg and if                                 *) 
    1.59 -(* ------------------------------------------------------------------------ *)
    1.60 -
    1.61 -bind_thms ("andalso_thms", map prover [
    1.62 -                        "(TT andalso y) = y",
    1.63 -                        "(FF andalso y) = FF",
    1.64 -                        "(UU andalso y) = UU",
    1.65 -			"(y andalso TT) = y",
    1.66 -		  	"(y andalso y) = y"
    1.67 -                        ]);
    1.68 -
    1.69 -bind_thms ("orelse_thms", map prover [
    1.70 -                        "(TT orelse y) = TT",
    1.71 -                        "(FF orelse y) = y",
    1.72 -                        "(UU orelse y) = UU",
    1.73 -                        "(y orelse FF) = y",
    1.74 -			"(y orelse y) = y"]);
    1.75 -
    1.76 -bind_thms ("neg_thms", map prover [
    1.77 -                        "neg$TT = FF",
    1.78 -                        "neg$FF = TT",
    1.79 -                        "neg$UU = UU"
    1.80 -                        ]);
    1.81 -
    1.82 -bind_thms ("ifte_thms", map prover [
    1.83 -                        "If UU then e1 else e2 fi = UU",
    1.84 -                        "If FF then e1 else e2 fi = e2",
    1.85 -                        "If TT then e1 else e2 fi = e1"]);
    1.86 -
    1.87 -Addsimps (dist_less_tr @ dist_eq_tr @ andalso_thms @ 
    1.88 -	  orelse_thms @ neg_thms @ ifte_thms);
    1.89 +(* legacy ML bindings *)
    1.90  
    1.91 -(* ------------------------------------------------------------------- *)
    1.92 -(*  split-tac for If via If2 because the constant has to be a constant *)
    1.93 -(* ------------------------------------------------------------------- *)
    1.94 -  
    1.95 -Goalw [If2_def] 
    1.96 -  "P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))";
    1.97 -by (res_inst_tac [("p","Q")] trE 1);
    1.98 -by (REPEAT (Asm_full_simp_tac 1));
    1.99 -qed"split_If2";
   1.100 -
   1.101 -val split_If_tac =
   1.102 -  simp_tac (HOL_basic_ss addsimps [symmetric If2_def]) THEN' (split_tac [split_If2]);
   1.103 -
   1.104 - 
   1.105 -
   1.106 -(* ----------------------------------------------------------------- *)
   1.107 -        section"Rewriting of HOLCF operations to HOL functions";
   1.108 -(* ----------------------------------------------------------------- *)
   1.109 -
   1.110 -
   1.111 -Goal
   1.112 -"!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)";
   1.113 -by (rtac iffI 1);
   1.114 -by (res_inst_tac [("p","t")] trE 1);
   1.115 -by Auto_tac;
   1.116 -by (res_inst_tac [("p","t")] trE 1);
   1.117 -by Auto_tac;
   1.118 -qed"andalso_or";
   1.119 -
   1.120 -Goal "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
   1.121 -by (rtac iffI 1);
   1.122 -by (res_inst_tac [("p","t")] trE 1);
   1.123 -by Auto_tac;
   1.124 -by (res_inst_tac [("p","t")] trE 1);
   1.125 -by Auto_tac;
   1.126 -qed"andalso_and";
   1.127 -
   1.128 -Goal "(Def x ~=FF)= x";
   1.129 -by (simp_tac (simpset() addsimps [FF_def]) 1);
   1.130 -qed"Def_bool1";
   1.131 -
   1.132 -Goal "(Def x = FF) = (~x)";
   1.133 -by (simp_tac (simpset() addsimps [FF_def]) 1);
   1.134 -qed"Def_bool2";
   1.135 +val TT_def = thm "TT_def";
   1.136 +val FF_def = thm "FF_def";
   1.137 +val neg_def = thm "neg_def";
   1.138 +val ifte_def = thm "ifte_def";
   1.139 +val andalso_def = thm "andalso_def";
   1.140 +val orelse_def = thm "orelse_def";
   1.141 +val If2_def = thm "If2_def";
   1.142 +val Exh_tr = thm "Exh_tr";
   1.143 +val trE = thm "trE";
   1.144 +val tr_defs = thms "tr_defs";
   1.145 +val dist_less_tr = thms "dist_less_tr";
   1.146 +val dist_eq_tr = thms "dist_eq_tr";
   1.147 +val ifte_simp = thm "ifte_simp";
   1.148 +val ifte_thms = thms "ifte_thms";
   1.149 +val andalso_thms = thms "andalso_thms";
   1.150 +val orelse_thms = thms "orelse_thms";
   1.151 +val neg_thms = thms "neg_thms";
   1.152 +val split_If2 = thm "split_If2";
   1.153 +val andalso_or = thm "andalso_or";
   1.154 +val andalso_and = thm "andalso_and";
   1.155 +val Def_bool1 = thm "Def_bool1";
   1.156 +val Def_bool2 = thm "Def_bool2";
   1.157 +val Def_bool3 = thm "Def_bool3";
   1.158 +val Def_bool4 = thm "Def_bool4";
   1.159 +val If_and_if = thm "If_and_if";
   1.160 +val adm_trick_1 = thm "adm_trick_1";
   1.161 +val adm_trick_2 = thm "adm_trick_2";
   1.162 +val adm_tricks = thms "adm_tricks";
   1.163 +val adm_nTT = thm "adm_nTT";
   1.164 +val adm_nFF = thm "adm_nFF";
   1.165  
   1.166 -Goal "(Def x = TT) = x";
   1.167 -by (simp_tac (simpset() addsimps [TT_def]) 1);
   1.168 -qed"Def_bool3";
   1.169 -
   1.170 -Goal "(Def x ~= TT) = (~x)";
   1.171 -by (simp_tac (simpset() addsimps [TT_def]) 1);
   1.172 -qed"Def_bool4";
   1.173 -
   1.174 -Goal 
   1.175 -  "(If Def P then A else B fi)= (if P then A else B)";
   1.176 -by (res_inst_tac [("p","Def P")]  trE 1);
   1.177 -by (Asm_full_simp_tac 1);
   1.178 -by (asm_full_simp_tac (simpset() addsimps tr_defs@[flift1_def,o_def]) 1);
   1.179 -by (asm_full_simp_tac (simpset() addsimps tr_defs@[flift1_def,o_def]) 1);
   1.180 -qed"If_and_if";
   1.181 -
   1.182 -Addsimps [Def_bool1,Def_bool2,Def_bool3,Def_bool4];
   1.183 -
   1.184 -(* ----------------------------------------------------------------- *)
   1.185 -        section"admissibility";
   1.186 -(* ----------------------------------------------------------------- *)
   1.187 -
   1.188 -
   1.189 -(* The following rewrite rules for admissibility should in the future be 
   1.190 -   replaced by a more general admissibility test that also checks 
   1.191 -   chain-finiteness, of which these lemmata are specific examples *)
   1.192 -
   1.193 -Goal "(x~=FF) = (x=TT|x=UU)";
   1.194 -by (res_inst_tac [("p","x")] trE 1);
   1.195 -by (TRYALL (Asm_full_simp_tac));
   1.196 -qed"adm_trick_1";
   1.197 -
   1.198 -Goal "(x~=TT) = (x=FF|x=UU)";
   1.199 -by (res_inst_tac [("p","x")] trE 1);
   1.200 -by (TRYALL (Asm_full_simp_tac));
   1.201 -qed"adm_trick_2";
   1.202 -
   1.203 -bind_thms ("adm_tricks", [adm_trick_1,adm_trick_2]);
   1.204 -
   1.205 -
   1.206 -Goal "cont(f) ==> adm (%x. (f x)~=TT)";
   1.207 -by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
   1.208 -by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
   1.209 -qed"adm_nTT";
   1.210 -
   1.211 -Goal "cont(f) ==> adm (%x. (f x)~=FF)";
   1.212 -by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
   1.213 -by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
   1.214 -qed"adm_nFF";
   1.215 -
   1.216 -Addsimps [adm_nTT,adm_nFF];
     2.1 --- a/src/HOLCF/Tr.thy	Fri Apr 01 21:04:00 2005 +0200
     2.2 +++ b/src/HOLCF/Tr.thy	Fri Apr 01 23:44:41 2005 +0200
     2.3 @@ -1,11 +1,16 @@
     2.4  (*  Title:      HOLCF/Tr.thy
     2.5      ID:         $Id$
     2.6      Author:     Franz Regensburger
     2.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8  
     2.9  Introduce infix if_then_else_fi and boolean connectives andalso, orelse
    2.10  *)
    2.11  
    2.12 -Tr = Lift + Fix +
    2.13 +header {* The type of lifted booleans *}
    2.14 +
    2.15 +theory Tr
    2.16 +imports Lift Fix
    2.17 +begin
    2.18  
    2.19  types
    2.20    tr = "bool lift"
    2.21 @@ -14,7 +19,8 @@
    2.22    "tr" <= (type) "bool lift" 
    2.23  
    2.24  consts
    2.25 -	TT,FF           :: "tr"
    2.26 +	TT              :: "tr"
    2.27 +	FF              :: "tr"
    2.28          Icifte          :: "tr -> 'c -> 'c -> 'c"
    2.29          trand           :: "tr -> tr -> tr"
    2.30          tror            :: "tr -> tr -> tr"
    2.31 @@ -30,13 +36,164 @@
    2.32               "x orelse y"  == "tror$x$y"
    2.33               "If b then e1 else e2 fi" == "Icifte$b$e1$e2"
    2.34  defs
    2.35 -  TT_def      "TT==Def True"
    2.36 -  FF_def      "FF==Def False"
    2.37 -  neg_def     "neg == flift2 Not"
    2.38 -  ifte_def    "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
    2.39 -  andalso_def "trand == (LAM x y. If x then y else FF fi)"
    2.40 -  orelse_def  "tror == (LAM x y. If x then TT else y fi)"
    2.41 -  If2_def     "If2 Q x y == If Q then x else y fi"
    2.42 +  TT_def:      "TT==Def True"
    2.43 +  FF_def:      "FF==Def False"
    2.44 +  neg_def:     "neg == flift2 Not"
    2.45 +  ifte_def:    "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
    2.46 +  andalso_def: "trand == (LAM x y. If x then y else FF fi)"
    2.47 +  orelse_def:  "tror == (LAM x y. If x then TT else y fi)"
    2.48 +  If2_def:     "If2 Q x y == If Q then x else y fi"
    2.49 +
    2.50 +text {* Exhaustion and Elimination for type @{typ tr} *}
    2.51 +
    2.52 +lemma Exh_tr: "t=UU | t = TT | t = FF"
    2.53 +apply (unfold FF_def TT_def)
    2.54 +apply (induct_tac "t")
    2.55 +apply fast
    2.56 +apply fast
    2.57 +done
    2.58 +
    2.59 +lemma trE: "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
    2.60 +apply (rule Exh_tr [THEN disjE])
    2.61 +apply fast
    2.62 +apply (erule disjE)
    2.63 +apply fast
    2.64 +apply fast
    2.65 +done
    2.66 +
    2.67 +text {* tactic for tr-thms with case split *}
    2.68 +
    2.69 +lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
    2.70 +(*
    2.71 +fun prover t =  prove_goal thy t
    2.72 + (fn prems =>
    2.73 +        [
    2.74 +        (res_inst_tac [("p","y")] trE 1),
    2.75 +	(REPEAT(asm_simp_tac (simpset() addsimps 
    2.76 +		[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
    2.77 +	])
    2.78 +*)
    2.79 +text {* distinctness for type @{typ tr} *}
    2.80 +
    2.81 +lemma dist_less_tr [simp]: "~TT << UU" "~FF << UU" "~TT << FF" "~FF << TT"
    2.82 +by (simp_all add: tr_defs)
    2.83 +
    2.84 +lemma dist_eq_tr [simp]: "TT~=UU" "FF~=UU" "TT~=FF" "UU~=TT" "UU~=FF" "FF~=TT"
    2.85 +by (simp_all add: tr_defs)
    2.86 +
    2.87 +text {* lemmas about andalso, orelse, neg and if *}
    2.88 +
    2.89 +lemma ifte_simp:
    2.90 +  "If x then e1 else e2 fi =
    2.91 +    flift1 (%b. if b then e1 else e2)$x"
    2.92 +apply (unfold ifte_def TT_def FF_def flift1_def)
    2.93 +apply (simp add: cont_flift1_arg cont_if)
    2.94 +done
    2.95 +
    2.96 +lemma ifte_thms [simp]:
    2.97 +  "If UU then e1 else e2 fi = UU"
    2.98 +  "If FF then e1 else e2 fi = e2"
    2.99 +  "If TT then e1 else e2 fi = e1"
   2.100 +by (simp_all add: ifte_simp TT_def FF_def)
   2.101 +
   2.102 +lemma andalso_thms [simp]:
   2.103 +  "(TT andalso y) = y"
   2.104 +  "(FF andalso y) = FF"
   2.105 +  "(UU andalso y) = UU"
   2.106 +  "(y andalso TT) = y"
   2.107 +  "(y andalso y) = y"
   2.108 +apply (unfold andalso_def, simp_all)
   2.109 +apply (rule_tac p=y in trE, simp_all)
   2.110 +apply (rule_tac p=y in trE, simp_all)
   2.111 +done
   2.112 +
   2.113 +lemma orelse_thms [simp]:
   2.114 +  "(TT orelse y) = TT"
   2.115 +  "(FF orelse y) = y"
   2.116 +  "(UU orelse y) = UU"
   2.117 +  "(y orelse FF) = y"
   2.118 +  "(y orelse y) = y"
   2.119 +apply (unfold orelse_def, simp_all)
   2.120 +apply (rule_tac p=y in trE, simp_all)
   2.121 +apply (rule_tac p=y in trE, simp_all)
   2.122 +done
   2.123 +
   2.124 +lemma neg_thms [simp]:
   2.125 +  "neg$TT = FF"
   2.126 +  "neg$FF = TT"
   2.127 +  "neg$UU = UU"
   2.128 +by (simp_all add: neg_def TT_def FF_def)
   2.129 +
   2.130 +text {* split-tac for If via If2 because the constant has to be a constant *}
   2.131 +  
   2.132 +lemma split_If2: 
   2.133 +  "P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))"  
   2.134 +apply (unfold If2_def)
   2.135 +apply (rule_tac p = "Q" in trE)
   2.136 +apply (simp_all)
   2.137 +done
   2.138 +
   2.139 +ML_setup {*
   2.140 +val split_If_tac =
   2.141 +  simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")])
   2.142 +    THEN' (split_tac [thm "split_If2"])
   2.143 +*}
   2.144 +
   2.145 +subsection "Rewriting of HOLCF operations to HOL functions"
   2.146 +
   2.147 +lemma andalso_or: 
   2.148 +"!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)"
   2.149 +apply (rule_tac p = "t" in trE)
   2.150 +apply simp_all
   2.151 +done
   2.152 +
   2.153 +lemma andalso_and: "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)"
   2.154 +apply (rule_tac p = "t" in trE)
   2.155 +apply simp_all
   2.156 +done
   2.157 +
   2.158 +lemma Def_bool1 [simp]: "(Def x ~= FF) = x"
   2.159 +by (simp add: FF_def)
   2.160 +
   2.161 +lemma Def_bool2 [simp]: "(Def x = FF) = (~x)"
   2.162 +by (simp add: FF_def)
   2.163 +
   2.164 +lemma Def_bool3 [simp]: "(Def x = TT) = x"
   2.165 +by (simp add: TT_def)
   2.166 +
   2.167 +lemma Def_bool4 [simp]: "(Def x ~= TT) = (~x)"
   2.168 +by (simp add: TT_def)
   2.169 +
   2.170 +lemma If_and_if: 
   2.171 +  "(If Def P then A else B fi)= (if P then A else B)"
   2.172 +apply (rule_tac p = "Def P" in trE)
   2.173 +apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
   2.174 +done
   2.175 +
   2.176 +subsection "admissibility"
   2.177 +
   2.178 +text {*
   2.179 +   The following rewrite rules for admissibility should in the future be 
   2.180 +   replaced by a more general admissibility test that also checks 
   2.181 +   chain-finiteness, of which these lemmata are specific examples
   2.182 +*}
   2.183 +
   2.184 +lemma adm_trick_1: "(x~=FF) = (x=TT|x=UU)"
   2.185 +apply (rule_tac p = "x" in trE)
   2.186 +apply (simp_all)
   2.187 +done
   2.188 +
   2.189 +lemma adm_trick_2: "(x~=TT) = (x=FF|x=UU)"
   2.190 +apply (rule_tac p = "x" in trE)
   2.191 +apply (simp_all)
   2.192 +done
   2.193 +
   2.194 +lemmas adm_tricks = adm_trick_1 adm_trick_2
   2.195 +
   2.196 +lemma adm_nTT [simp]: "cont(f) ==> adm (%x. (f x)~=TT)"
   2.197 +by (simp add: adm_tricks)
   2.198 +
   2.199 +lemma adm_nFF [simp]: "cont(f) ==> adm (%x. (f x)~=FF)"
   2.200 +by (simp add: adm_tricks)
   2.201  
   2.202  end
   2.203 -