# HG changeset patch
# User huffman
# Date 1119654554 -7200
# Node ID 00a3bf006881a301b539f810cfa58141c592a9e2
# Parent  6fc73c9dd5f470cd8d76f0fdfe8b3271085c4d96
cleaned up

diff -r 6fc73c9dd5f4 -r 00a3bf006881 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Sat Jun 25 01:04:01 2005 +0200
+++ b/src/HOLCF/Adm.thy	Sat Jun 25 01:09:14 2005 +0200
@@ -13,29 +13,26 @@
 
 subsection {* Definitions *}
 
-consts
-adm		:: "('a::cpo=>bool)=>bool"
-
-defs
-adm_def:       "adm P == !Y. chain(Y) --> 
-                        (!i. P(Y i)) --> P(lub(range Y))"
+constdefs
+  adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool"
+  "adm P \<equiv> \<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (lub (range Y))"
 
 subsection {* Admissibility and fixed point induction *}
 
 text {* access to definitions *}
 
 lemma admI:
-   "(!!Y. [| chain Y; !i. P (Y i) |] ==> P (lub (range Y))) ==> adm P"
+   "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (lub (range Y))) \<Longrightarrow> adm P"
 apply (unfold adm_def)
 apply blast
 done
 
-lemma triv_admI: "!x. P x ==> adm P"
+lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
 apply (rule admI)
 apply (erule spec)
 done
 
-lemma admD: "[| adm(P); chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))"
+lemma admD: "\<lbrakk>adm P; chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (lub (range Y))"
 apply (unfold adm_def)
 apply blast
 done
@@ -43,13 +40,13 @@
 text {* for chain-finite (easy) types every formula is admissible *}
 
 lemma adm_max_in_chain: 
-"!Y. chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)"
+  "\<forall>Y. chain (Y::nat=>'a) \<longrightarrow> (\<exists>n. max_in_chain n Y) \<Longrightarrow> adm (P::'a=>bool)"
 apply (unfold adm_def)
 apply (intro strip)
-apply (rule exE)
-apply (rule mp)
-apply (erule spec)
+apply (drule spec)
+apply (drule mp)
 apply assumption
+apply (erule exE)
 apply (subst lub_finch1 [THEN thelubI])
 apply assumption
 apply assumption
@@ -61,10 +58,9 @@
 text {* improved admissibility introduction *}
 
 lemma admI2:
- "(!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |] 
-  ==> P(lub (range Y))) ==> adm P"
-apply (unfold adm_def)
-apply (intro strip)
+  "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i); \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> 
+    \<Longrightarrow> P (lub (range Y))) \<Longrightarrow> adm P"
+apply (rule admI)
 apply (erule increasing_chain_adm_lemma)
 apply assumption
 apply fast
@@ -72,74 +68,53 @@
 
 text {* admissibility of special formulae and propagation *}
 
-lemma adm_less [simp]: "[|cont u;cont v|]==> adm(%x. u x << v x)"
-apply (unfold adm_def)
-apply (intro strip)
-apply (frule_tac f = "u" in cont2mono [THEN ch2ch_monofun])
+lemma adm_less [simp]: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
+apply (rule admI)
+apply (simp add: cont2contlub [THEN contlubE])
+apply (rule lub_mono)
+apply (erule (1) cont2mono [THEN ch2ch_monofun])
+apply (erule (1) cont2mono [THEN ch2ch_monofun])
 apply assumption
-apply (frule_tac f = "v" in cont2mono [THEN ch2ch_monofun])
-apply assumption
-apply (erule cont2contlub [THEN contlubE, THEN ssubst])
-apply assumption
-apply (erule cont2contlub [THEN contlubE, THEN ssubst])
-apply assumption
-apply (blast intro: lub_mono)
 done
 
-lemma adm_conj [simp]: "[| adm P; adm Q |] ==> adm(%x. P x & Q x)"
+lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
 by (fast elim: admD intro: admI)
 
-lemma adm_not_free [simp]: "adm(%x. t)"
-apply (unfold adm_def)
-apply fast
-done
+lemma adm_not_free: "adm (\<lambda>x. t)"
+by (rule admI, simp)
 
-lemma adm_not_less: "cont t ==> adm(%x.~ (t x) << u)"
-apply (unfold adm_def)
-apply (intro strip)
-apply (rule contrapos_nn)
-apply (erule spec)
+lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
+apply (rule admI)
+apply (drule_tac x=0 in spec)
+apply (erule contrapos_nn)
 apply (rule trans_less)
 prefer 2 apply (assumption)
 apply (erule cont2mono [THEN monofun_fun_arg])
-apply (rule is_ub_thelub)
-apply assumption
+apply (erule is_ub_thelub)
 done
 
-lemma adm_all: "!y. adm(P y) ==> adm(%x.!y. P y x)"
+lemma adm_all: "\<forall>y. adm (P y) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P y x)"
 by (fast intro: admI elim: admD)
 
 lemmas adm_all2 = allI [THEN adm_all, standard]
 
-lemma adm_subst: "[|cont t; adm P|] ==> adm(%x. P (t x))"
+lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
 apply (rule admI)
-apply (simplesubst cont2contlub [THEN contlubE])
-apply assumption
-apply assumption
+apply (simp add: cont2contlub [THEN contlubE])
 apply (erule admD)
 apply (erule cont2mono [THEN ch2ch_monofun])
 apply assumption
 apply assumption
 done
 
-lemma adm_UU_not_less: "adm(%x.~ UU << t(x))"
-by simp
+lemma adm_UU_not_less: "adm (\<lambda>x. \<not> \<bottom> \<sqsubseteq> t x)"
+by (simp add: adm_not_free)
 
-lemma adm_not_UU: "cont(t)==> adm(%x.~ (t x) = UU)"
-apply (unfold adm_def)
-apply (intro strip)
-apply (rule contrapos_nn)
-apply (erule spec)
-apply (rule chain_UU_I [THEN spec])
-apply (erule cont2mono [THEN ch2ch_monofun])
-apply assumption
-apply (erule cont2contlub [THEN contlubE, THEN subst])
-apply assumption
-apply assumption
-done
+lemma adm_not_UU: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x = \<bottom>)"
+by (simp add: eq_UU_iff adm_not_less)
 
-lemma adm_eq: "[|cont u ; cont v|]==> adm(%x. u x = v x)"
-by (simp add: po_eq_conv)
+lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
+by (simp add: po_eq_conv adm_conj)
 
 text {* admissibility for disjunction is hard to prove. It takes 7 Lemmas *}
 
@@ -155,13 +130,14 @@
 apply (rule le_maxI2)
 done
 
-lemma adm_disj_lemma2: "[| adm P; \<exists>X. chain X & (!n. P(X n)) & 
-      lub(range Y)=lub(range X)|] ==> P(lub(range Y))"
+lemma adm_disj_lemma2:
+  "\<lbrakk>adm P; \<exists>X. chain X \<and> (\<forall>n. P (X n)) \<and> 
+    lub (range Y) = lub (range X)\<rbrakk> \<Longrightarrow> P (lub (range Y))"
 by (force elim: admD)
 
 lemma adm_disj_lemma3: 
-  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j) |] ==> 
-            chain(%m. Y (LEAST j. m\<le>j \<and> P(Y j)))"
+  "\<lbrakk>chain (Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow>
+    chain (\<lambda>m. Y (LEAST j. m \<le> j \<and> P (Y j)))"
 apply (rule chainI)
 apply (erule chain_mono3)
 apply (rule Least_le)
@@ -176,7 +152,7 @@
 done
 
 lemma adm_disj_lemma4: 
-  "[| \<forall>i. \<exists>j\<ge>i. P (Y j) |] ==> ! m. P(Y(LEAST j::nat. m\<le>j & P(Y j)))"
+  "\<lbrakk>\<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> \<forall>m. P (Y (LEAST j::nat. m \<le> j \<and> P (Y j)))"
 apply (rule allI)
 apply (erule allE)
 apply (erule exE)
@@ -184,21 +160,19 @@
 done
 
 lemma adm_disj_lemma5: 
-  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j) |] ==> 
-            lub(range(Y)) = (LUB m. Y(LEAST j. m\<le>j & P(Y j)))"
+  "\<lbrakk>chain (Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j)\<rbrakk> \<Longrightarrow> 
+    lub (range Y) = (LUB m. Y (LEAST j. m \<le> j \<and> P (Y j)))"
  apply (rule antisym_less)
   apply (rule lub_mono)
     apply assumption
-   apply (erule adm_disj_lemma3)
-   apply assumption
+   apply (erule (1) adm_disj_lemma3)
   apply (rule allI)
   apply (erule chain_mono3)
   apply (erule allE)
   apply (erule exE)
   apply (erule LeastI [THEN conjunct1])
  apply (rule lub_mono3)
-   apply (erule adm_disj_lemma3)
-   apply assumption
+   apply (erule (1) adm_disj_lemma3)
   apply assumption
  apply (rule allI)
  apply (rule exI)
@@ -206,44 +180,42 @@
 done
 
 lemma adm_disj_lemma6:
-  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j) |] ==> 
-            \<exists>X. chain X & (\<forall>n. P(X n)) & lub(range Y) = lub(range X)"
-apply (rule_tac x = "%m. Y (LEAST j. m\<le>j & P (Y j))" in exI)
+  "\<lbrakk>chain (Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j)\<rbrakk> \<Longrightarrow>
+    \<exists>X. chain X \<and> (\<forall>n. P (X n)) \<and> lub (range Y) = lub (range X)"
+apply (rule_tac x = "\<lambda>m. Y (LEAST j. m \<le> j \<and> P (Y j))" in exI)
 apply (fast intro!: adm_disj_lemma3 adm_disj_lemma4 adm_disj_lemma5)
 done
 
 lemma adm_disj_lemma7:
-"[| adm(P); chain(Y); \<forall>i. \<exists>j\<ge>i. P(Y j) |]==>P(lub(range(Y)))"
+  "\<lbrakk>adm P; chain Y; \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> P (lub (range Y))"
 apply (erule adm_disj_lemma2)
-apply (erule adm_disj_lemma6)
-apply assumption
+apply (erule (1) adm_disj_lemma6)
 done
 
 lemma adm_disj: "[| adm P; adm Q |] ==> adm(%x. P x | Q x)"
 apply (rule admI)
 apply (erule adm_disj_lemma1 [THEN disjE])
 apply (rule disjI1)
-apply (erule adm_disj_lemma7)
-apply assumption
-apply assumption
+apply (erule (2) adm_disj_lemma7)
 apply (rule disjI2)
-apply (erule adm_disj_lemma7)
-apply assumption
-apply assumption
+apply (erule (2) adm_disj_lemma7)
 done
 
-lemma adm_imp: "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)"
+lemma adm_imp: "\<lbrakk>adm (\<lambda>x. \<not> P x); adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
 by (subst imp_conv_disj, rule adm_disj)
 
-lemma adm_iff: "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |]  
-            ==> adm (%x. P x = Q x)"
+lemma adm_iff:
+  "\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk>  
+    \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
 by (subst iff_conv_conj_imp, rule adm_conj)
 
-lemma adm_not_conj: "[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"
+lemma adm_not_conj:
+  "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. \<not> Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> (P x \<and> Q x))"
 by (subst de_Morgan_conj, rule adm_disj)
 
-lemmas adm_lemmas = adm_not_free adm_imp adm_disj adm_eq adm_not_UU
-        adm_UU_not_less adm_all2 adm_not_less adm_not_conj adm_iff
+lemmas adm_lemmas =
+  adm_conj adm_not_free adm_imp adm_disj adm_eq adm_not_UU
+  adm_UU_not_less adm_all2 adm_not_less adm_not_conj adm_iff
 
 declare adm_lemmas [simp]
 
@@ -278,8 +250,7 @@
 val adm_imp = thm "adm_imp";
 val adm_iff = thm "adm_iff";
 val adm_not_conj = thm "adm_not_conj";
-val adm_lemmas = [adm_not_free, adm_imp, adm_disj, adm_eq, adm_not_UU,
-        adm_UU_not_less, adm_all2, adm_not_less, adm_not_conj, adm_iff]
+val adm_lemmas = thms "adm_lemmas";
 *}
 
 end