--- a/src/HOLCF/Tr.ML Fri Apr 01 21:04:00 2005 +0200
+++ b/src/HOLCF/Tr.ML Fri Apr 01 23:44:41 2005 +0200
@@ -1,182 +1,34 @@
-(* Title: HOLCF/Tr.ML
- ID: $Id$
- Author: Franz Regensburger
-Introduce infix if_then_else_fi and boolean connectives andalso, orelse
-*)
-
-(* ------------------------------------------------------------------------ *)
-(* Exhaustion and Elimination for type one *)
-(* ------------------------------------------------------------------------ *)
-
-Goalw [FF_def,TT_def] "t=UU | t = TT | t = FF";
-by (induct_tac "t" 1);
-by (fast_tac HOL_cs 1);
-by (fast_tac (HOL_cs addss simpset()) 1);
-qed "Exh_tr";
-
-val prems = Goal "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q";
-by (rtac (Exh_tr RS disjE) 1);
-by (eresolve_tac prems 1);
-by (etac disjE 1);
-by (eresolve_tac prems 1);
-by (eresolve_tac prems 1);
-qed "trE";
-
-(* ------------------------------------------------------------------------ *)
-(* tactic for tr-thms with case split *)
-(* ------------------------------------------------------------------------ *)
-
-bind_thms ("tr_defs", [andalso_def,orelse_def,neg_def,ifte_def,TT_def,FF_def]);
-
-fun prover t = prove_goal thy t
- (fn prems =>
- [
- (res_inst_tac [("p","y")] trE 1),
- (REPEAT(asm_simp_tac (simpset() addsimps
- [o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* distinctness for type tr *)
-(* ------------------------------------------------------------------------ *)
-
-bind_thms ("dist_less_tr", map prover [
- "~TT << UU",
- "~FF << UU",
- "~TT << FF",
- "~FF << TT"
- ]);
-
-val dist_eq_tr = map prover ["TT~=UU","FF~=UU","TT~=FF"];
-bind_thms ("dist_eq_tr", dist_eq_tr @ (map (fn thm => (thm RS not_sym)) dist_eq_tr));
-
-(* ------------------------------------------------------------------------ *)
-(* lemmas about andalso, orelse, neg and if *)
-(* ------------------------------------------------------------------------ *)
-
-bind_thms ("andalso_thms", map prover [
- "(TT andalso y) = y",
- "(FF andalso y) = FF",
- "(UU andalso y) = UU",
- "(y andalso TT) = y",
- "(y andalso y) = y"
- ]);
-
-bind_thms ("orelse_thms", map prover [
- "(TT orelse y) = TT",
- "(FF orelse y) = y",
- "(UU orelse y) = UU",
- "(y orelse FF) = y",
- "(y orelse y) = y"]);
-
-bind_thms ("neg_thms", map prover [
- "neg$TT = FF",
- "neg$FF = TT",
- "neg$UU = UU"
- ]);
-
-bind_thms ("ifte_thms", map prover [
- "If UU then e1 else e2 fi = UU",
- "If FF then e1 else e2 fi = e2",
- "If TT then e1 else e2 fi = e1"]);
-
-Addsimps (dist_less_tr @ dist_eq_tr @ andalso_thms @
- orelse_thms @ neg_thms @ ifte_thms);
+(* legacy ML bindings *)
-(* ------------------------------------------------------------------- *)
-(* split-tac for If via If2 because the constant has to be a constant *)
-(* ------------------------------------------------------------------- *)
-
-Goalw [If2_def]
- "P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))";
-by (res_inst_tac [("p","Q")] trE 1);
-by (REPEAT (Asm_full_simp_tac 1));
-qed"split_If2";
-
-val split_If_tac =
- simp_tac (HOL_basic_ss addsimps [symmetric If2_def]) THEN' (split_tac [split_If2]);
-
-
-
-(* ----------------------------------------------------------------- *)
- section"Rewriting of HOLCF operations to HOL functions";
-(* ----------------------------------------------------------------- *)
-
-
-Goal
-"!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)";
-by (rtac iffI 1);
-by (res_inst_tac [("p","t")] trE 1);
-by Auto_tac;
-by (res_inst_tac [("p","t")] trE 1);
-by Auto_tac;
-qed"andalso_or";
-
-Goal "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
-by (rtac iffI 1);
-by (res_inst_tac [("p","t")] trE 1);
-by Auto_tac;
-by (res_inst_tac [("p","t")] trE 1);
-by Auto_tac;
-qed"andalso_and";
-
-Goal "(Def x ~=FF)= x";
-by (simp_tac (simpset() addsimps [FF_def]) 1);
-qed"Def_bool1";
-
-Goal "(Def x = FF) = (~x)";
-by (simp_tac (simpset() addsimps [FF_def]) 1);
-qed"Def_bool2";
+val TT_def = thm "TT_def";
+val FF_def = thm "FF_def";
+val neg_def = thm "neg_def";
+val ifte_def = thm "ifte_def";
+val andalso_def = thm "andalso_def";
+val orelse_def = thm "orelse_def";
+val If2_def = thm "If2_def";
+val Exh_tr = thm "Exh_tr";
+val trE = thm "trE";
+val tr_defs = thms "tr_defs";
+val dist_less_tr = thms "dist_less_tr";
+val dist_eq_tr = thms "dist_eq_tr";
+val ifte_simp = thm "ifte_simp";
+val ifte_thms = thms "ifte_thms";
+val andalso_thms = thms "andalso_thms";
+val orelse_thms = thms "orelse_thms";
+val neg_thms = thms "neg_thms";
+val split_If2 = thm "split_If2";
+val andalso_or = thm "andalso_or";
+val andalso_and = thm "andalso_and";
+val Def_bool1 = thm "Def_bool1";
+val Def_bool2 = thm "Def_bool2";
+val Def_bool3 = thm "Def_bool3";
+val Def_bool4 = thm "Def_bool4";
+val If_and_if = thm "If_and_if";
+val adm_trick_1 = thm "adm_trick_1";
+val adm_trick_2 = thm "adm_trick_2";
+val adm_tricks = thms "adm_tricks";
+val adm_nTT = thm "adm_nTT";
+val adm_nFF = thm "adm_nFF";
-Goal "(Def x = TT) = x";
-by (simp_tac (simpset() addsimps [TT_def]) 1);
-qed"Def_bool3";
-
-Goal "(Def x ~= TT) = (~x)";
-by (simp_tac (simpset() addsimps [TT_def]) 1);
-qed"Def_bool4";
-
-Goal
- "(If Def P then A else B fi)= (if P then A else B)";
-by (res_inst_tac [("p","Def P")] trE 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps tr_defs@[flift1_def,o_def]) 1);
-by (asm_full_simp_tac (simpset() addsimps tr_defs@[flift1_def,o_def]) 1);
-qed"If_and_if";
-
-Addsimps [Def_bool1,Def_bool2,Def_bool3,Def_bool4];
-
-(* ----------------------------------------------------------------- *)
- section"admissibility";
-(* ----------------------------------------------------------------- *)
-
-
-(* The following rewrite rules for admissibility should in the future be
- replaced by a more general admissibility test that also checks
- chain-finiteness, of which these lemmata are specific examples *)
-
-Goal "(x~=FF) = (x=TT|x=UU)";
-by (res_inst_tac [("p","x")] trE 1);
-by (TRYALL (Asm_full_simp_tac));
-qed"adm_trick_1";
-
-Goal "(x~=TT) = (x=FF|x=UU)";
-by (res_inst_tac [("p","x")] trE 1);
-by (TRYALL (Asm_full_simp_tac));
-qed"adm_trick_2";
-
-bind_thms ("adm_tricks", [adm_trick_1,adm_trick_2]);
-
-
-Goal "cont(f) ==> adm (%x. (f x)~=TT)";
-by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
-by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
-qed"adm_nTT";
-
-Goal "cont(f) ==> adm (%x. (f x)~=FF)";
-by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1);
-by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1));
-qed"adm_nFF";
-
-Addsimps [adm_nTT,adm_nFF];
--- a/src/HOLCF/Tr.thy Fri Apr 01 21:04:00 2005 +0200
+++ b/src/HOLCF/Tr.thy Fri Apr 01 23:44:41 2005 +0200
@@ -1,11 +1,16 @@
(* Title: HOLCF/Tr.thy
ID: $Id$
Author: Franz Regensburger
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Introduce infix if_then_else_fi and boolean connectives andalso, orelse
*)
-Tr = Lift + Fix +
+header {* The type of lifted booleans *}
+
+theory Tr
+imports Lift Fix
+begin
types
tr = "bool lift"
@@ -14,7 +19,8 @@
"tr" <= (type) "bool lift"
consts
- TT,FF :: "tr"
+ TT :: "tr"
+ FF :: "tr"
Icifte :: "tr -> 'c -> 'c -> 'c"
trand :: "tr -> tr -> tr"
tror :: "tr -> tr -> tr"
@@ -30,13 +36,164 @@
"x orelse y" == "tror$x$y"
"If b then e1 else e2 fi" == "Icifte$b$e1$e2"
defs
- TT_def "TT==Def True"
- FF_def "FF==Def False"
- neg_def "neg == flift2 Not"
- ifte_def "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
- andalso_def "trand == (LAM x y. If x then y else FF fi)"
- orelse_def "tror == (LAM x y. If x then TT else y fi)"
- If2_def "If2 Q x y == If Q then x else y fi"
+ TT_def: "TT==Def True"
+ FF_def: "FF==Def False"
+ neg_def: "neg == flift2 Not"
+ ifte_def: "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
+ andalso_def: "trand == (LAM x y. If x then y else FF fi)"
+ orelse_def: "tror == (LAM x y. If x then TT else y fi)"
+ If2_def: "If2 Q x y == If Q then x else y fi"
+
+text {* Exhaustion and Elimination for type @{typ tr} *}
+
+lemma Exh_tr: "t=UU | t = TT | t = FF"
+apply (unfold FF_def TT_def)
+apply (induct_tac "t")
+apply fast
+apply fast
+done
+
+lemma trE: "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
+apply (rule Exh_tr [THEN disjE])
+apply fast
+apply (erule disjE)
+apply fast
+apply fast
+done
+
+text {* tactic for tr-thms with case split *}
+
+lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
+(*
+fun prover t = prove_goal thy t
+ (fn prems =>
+ [
+ (res_inst_tac [("p","y")] trE 1),
+ (REPEAT(asm_simp_tac (simpset() addsimps
+ [o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
+ ])
+*)
+text {* distinctness for type @{typ tr} *}
+
+lemma dist_less_tr [simp]: "~TT << UU" "~FF << UU" "~TT << FF" "~FF << TT"
+by (simp_all add: tr_defs)
+
+lemma dist_eq_tr [simp]: "TT~=UU" "FF~=UU" "TT~=FF" "UU~=TT" "UU~=FF" "FF~=TT"
+by (simp_all add: tr_defs)
+
+text {* lemmas about andalso, orelse, neg and if *}
+
+lemma ifte_simp:
+ "If x then e1 else e2 fi =
+ flift1 (%b. if b then e1 else e2)$x"
+apply (unfold ifte_def TT_def FF_def flift1_def)
+apply (simp add: cont_flift1_arg cont_if)
+done
+
+lemma ifte_thms [simp]:
+ "If UU then e1 else e2 fi = UU"
+ "If FF then e1 else e2 fi = e2"
+ "If TT then e1 else e2 fi = e1"
+by (simp_all add: ifte_simp TT_def FF_def)
+
+lemma andalso_thms [simp]:
+ "(TT andalso y) = y"
+ "(FF andalso y) = FF"
+ "(UU andalso y) = UU"
+ "(y andalso TT) = y"
+ "(y andalso y) = y"
+apply (unfold andalso_def, simp_all)
+apply (rule_tac p=y in trE, simp_all)
+apply (rule_tac p=y in trE, simp_all)
+done
+
+lemma orelse_thms [simp]:
+ "(TT orelse y) = TT"
+ "(FF orelse y) = y"
+ "(UU orelse y) = UU"
+ "(y orelse FF) = y"
+ "(y orelse y) = y"
+apply (unfold orelse_def, simp_all)
+apply (rule_tac p=y in trE, simp_all)
+apply (rule_tac p=y in trE, simp_all)
+done
+
+lemma neg_thms [simp]:
+ "neg$TT = FF"
+ "neg$FF = TT"
+ "neg$UU = UU"
+by (simp_all add: neg_def TT_def FF_def)
+
+text {* split-tac for If via If2 because the constant has to be a constant *}
+
+lemma split_If2:
+ "P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))"
+apply (unfold If2_def)
+apply (rule_tac p = "Q" in trE)
+apply (simp_all)
+done
+
+ML_setup {*
+val split_If_tac =
+ simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")])
+ THEN' (split_tac [thm "split_If2"])
+*}
+
+subsection "Rewriting of HOLCF operations to HOL functions"
+
+lemma andalso_or:
+"!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)"
+apply (rule_tac p = "t" in trE)
+apply simp_all
+done
+
+lemma andalso_and: "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)"
+apply (rule_tac p = "t" in trE)
+apply simp_all
+done
+
+lemma Def_bool1 [simp]: "(Def x ~= FF) = x"
+by (simp add: FF_def)
+
+lemma Def_bool2 [simp]: "(Def x = FF) = (~x)"
+by (simp add: FF_def)
+
+lemma Def_bool3 [simp]: "(Def x = TT) = x"
+by (simp add: TT_def)
+
+lemma Def_bool4 [simp]: "(Def x ~= TT) = (~x)"
+by (simp add: TT_def)
+
+lemma If_and_if:
+ "(If Def P then A else B fi)= (if P then A else B)"
+apply (rule_tac p = "Def P" in trE)
+apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
+done
+
+subsection "admissibility"
+
+text {*
+ The following rewrite rules for admissibility should in the future be
+ replaced by a more general admissibility test that also checks
+ chain-finiteness, of which these lemmata are specific examples
+*}
+
+lemma adm_trick_1: "(x~=FF) = (x=TT|x=UU)"
+apply (rule_tac p = "x" in trE)
+apply (simp_all)
+done
+
+lemma adm_trick_2: "(x~=TT) = (x=FF|x=UU)"
+apply (rule_tac p = "x" in trE)
+apply (simp_all)
+done
+
+lemmas adm_tricks = adm_trick_1 adm_trick_2
+
+lemma adm_nTT [simp]: "cont(f) ==> adm (%x. (f x)~=TT)"
+by (simp add: adm_tricks)
+
+lemma adm_nFF [simp]: "cont(f) ==> adm (%x. (f x)~=FF)"
+by (simp add: adm_tricks)
end
-