# HG changeset patch
# User huffman
# Date 1130973149 -3600
# Node ID b653e18f0a4121de55a7928b67f05d250e77520d
# Parent  f2c8f68a45e64512ff297cd192c36f37bc51c887
cleaned up; removed adm_tricks in favor of compactness theorems

diff -r f2c8f68a45e6 -r b653e18f0a41 src/HOLCF/IOA/meta_theory/Seq.ML
--- a/src/HOLCF/IOA/meta_theory/Seq.ML	Wed Nov 02 23:59:49 2005 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Thu Nov 03 00:12:29 2005 +0100
@@ -363,7 +363,7 @@
 by (simp_tac (simpset() addsimps [sforall_def]) 1);
 by (res_inst_tac[("x","x")] seq.ind 1);
 (* adm *)
-by (simp_tac (simpset() addsimps [adm_trick_1]) 1);
+by (simp_tac (simpset() (*addsimps [adm_trick_1]*)) 1);
 (* base cases *)
 by (Simp_tac 1);
 by (Simp_tac 1);
@@ -375,7 +375,7 @@
 by (simp_tac (simpset() addsimps [sforall_def]) 1);
 by (res_inst_tac[("x","x")] seq.ind 1);
 (* adm *)
-by (simp_tac (simpset() addsimps [adm_trick_1]) 1);
+by (simp_tac (simpset() (*addsimps [adm_trick_1]*)) 1);
 (* base cases *)
 by (Simp_tac 1);
 by (Simp_tac 1);
diff -r f2c8f68a45e6 -r b653e18f0a41 src/HOLCF/Tr.ML
--- a/src/HOLCF/Tr.ML	Wed Nov 02 23:59:49 2005 +0100
+++ b/src/HOLCF/Tr.ML	Thu Nov 03 00:12:29 2005 +0100
@@ -1,15 +1,12 @@
 
 (* legacy ML bindings *)
 
-val adm_nFF = thm "adm_nFF";
-val adm_nTT = thm "adm_nTT";
-val adm_trick_1 = thm "adm_trick_1";
-val adm_trick_2 = thm "adm_trick_2";
-val adm_tricks = thms "adm_tricks";
 val andalso_and = thm "andalso_and";
 val andalso_def = thm "andalso_def";
 val andalso_or = thm "andalso_or";
 val andalso_thms = thms "andalso_thms";
+val compact_FF = thm "compact_FF";
+val compact_TT = thm "compact_TT";
 val Def_bool1 = thm "Def_bool1";
 val Def_bool2 = thm "Def_bool2";
 val Def_bool3 = thm "Def_bool3";
diff -r f2c8f68a45e6 -r b653e18f0a41 src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Wed Nov 02 23:59:49 2005 +0100
+++ b/src/HOLCF/Tr.thy	Thu Nov 03 00:12:29 2005 +0100
@@ -20,22 +20,24 @@
   "tr" <= (type) "bool lift" 
 
 consts
-	TT              :: "tr"
-	FF              :: "tr"
-        Icifte          :: "tr -> 'c -> 'c -> 'c"
-        trand           :: "tr -> tr -> tr"
-        tror            :: "tr -> tr -> tr"
-        neg             :: "tr -> tr"
-        If2             :: "tr=>'c=>'c=>'c"
+  TT     :: "tr"
+  FF     :: "tr"
+  Icifte :: "tr \<rightarrow> 'c \<rightarrow> 'c \<rightarrow> 'c"
+  trand  :: "tr \<rightarrow> tr \<rightarrow> tr"
+  tror   :: "tr \<rightarrow> tr \<rightarrow> tr"
+  neg    :: "tr \<rightarrow> tr"
+  If2    :: "[tr, 'c, 'c] \<Rightarrow> 'c"
 
-syntax  "@cifte"        :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
-        "@andalso"      :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
-        "@orelse"       :: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
+syntax
+  "@cifte"   :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60)
+  "@andalso" :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ andalso _" [36,35] 35)
+  "@orelse"  :: "tr \<Rightarrow> tr \<Rightarrow> tr"     ("_ orelse _"  [31,30] 30)
  
-translations 
-	     "x andalso y" == "trand$x$y"
-             "x orelse y"  == "tror$x$y"
-             "If b then e1 else e2 fi" == "Icifte$b$e1$e2"
+translations
+  "x andalso y" == "trand\<cdot>x\<cdot>y"
+  "x orelse y"  == "tror\<cdot>x\<cdot>y"
+  "If b then e1 else e2 fi" == "Icifte\<cdot>b\<cdot>e1\<cdot>e2"
+
 defs
   TT_def:      "TT==Def True"
   FF_def:      "FF==Def False"
@@ -47,14 +49,14 @@
 
 text {* Exhaustion and Elimination for type @{typ tr} *}
 
-lemma Exh_tr: "t=UU | t = TT | t = FF"
+lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> 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"
+lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 apply (rule Exh_tr [THEN disjE])
 apply fast
 apply (erule disjE)
@@ -76,16 +78,18 @@
 *)
 text {* distinctness for type @{typ tr} *}
 
-lemma dist_less_tr [simp]: "~TT << UU" "~FF << UU" "~TT << FF" "~FF << TT"
+lemma dist_less_tr [simp]:
+  "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
 by (simp_all add: tr_defs)
 
-lemma dist_eq_tr [simp]: "TT~=UU" "FF~=UU" "TT~=FF" "UU~=TT" "UU~=FF" "FF~=TT"
+lemma dist_eq_tr [simp]:
+  "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
 by (simp_all add: tr_defs)
 
 text {* lemmas about andalso, orelse, neg and if *}
 
 lemma ifte_thms [simp]:
-  "If UU then e1 else e2 fi = UU"
+  "If \<bottom> then e1 else e2 fi = \<bottom>"
   "If FF then e1 else e2 fi = e2"
   "If TT then e1 else e2 fi = e1"
 by (simp_all add: ifte_def TT_def FF_def)
@@ -93,7 +97,7 @@
 lemma andalso_thms [simp]:
   "(TT andalso y) = y"
   "(FF andalso y) = FF"
-  "(UU andalso y) = UU"
+  "(\<bottom> andalso y) = \<bottom>"
   "(y andalso TT) = y"
   "(y andalso y) = y"
 apply (unfold andalso_def, simp_all)
@@ -104,7 +108,7 @@
 lemma orelse_thms [simp]:
   "(TT orelse y) = TT"
   "(FF orelse y) = y"
-  "(UU orelse y) = UU"
+  "(\<bottom> orelse y) = \<bottom>"
   "(y orelse FF) = y"
   "(y orelse y) = y"
 apply (unfold orelse_def, simp_all)
@@ -113,15 +117,15 @@
 done
 
 lemma neg_thms [simp]:
-  "neg$TT = FF"
-  "neg$FF = TT"
-  "neg$UU = UU"
+  "neg\<cdot>TT = FF"
+  "neg\<cdot>FF = TT"
+  "neg\<cdot>\<bottom> = \<bottom>"
 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))"  
+  "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
 apply (unfold If2_def)
 apply (rule_tac p = "Q" in trE)
 apply (simp_all)
@@ -136,58 +140,41 @@
 subsection "Rewriting of HOLCF operations to HOL functions"
 
 lemma andalso_or: 
-"!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)"
+  "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> 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)"
+lemma andalso_and:
+  "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)"
 apply (rule_tac p = "t" in trE)
 apply simp_all
 done
 
-lemma Def_bool1 [simp]: "(Def x ~= FF) = x"
+lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x"
 by (simp add: FF_def)
 
-lemma Def_bool2 [simp]: "(Def x = FF) = (~x)"
+lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> 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)"
+lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)"
 by (simp add: TT_def)
 
 lemma If_and_if: 
-  "(If Def P then A else B fi)= (if P then A else B)"
+  "(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
+subsection {* Compactness *}
 
-lemma adm_trick_2: "(x~=TT) = (x=FF|x=UU)"
-apply (rule_tac p = "x" in trE)
-apply (simp_all)
-done
+lemma compact_TT [simp]: "compact TT"
+by (rule compact_chfin)
 
-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)
+lemma compact_FF [simp]: "compact FF"
+by (rule compact_chfin)
 
 end