# HG changeset patch # User huffman # Date 1120175317 -7200 # Node ID f3fcfa388ecb3d7b0e936adc68dd39436aaebc8e # Parent f90894e13a3e08149ca53a33dd68b8c003a56439 cleaned up; added adm_less to adm_lemmas; added subsection headings diff -r f90894e13a3e -r f3fcfa388ecb src/HOLCF/Adm.thy --- a/src/HOLCF/Adm.thy Thu Jun 30 19:49:41 2005 +0200 +++ b/src/HOLCF/Adm.thy Fri Jul 01 01:48:37 2005 +0200 @@ -15,14 +15,10 @@ constdefs adm :: "('a::cpo \ bool) \ bool" - "adm P \ \Y. chain Y \ (\i. P (Y i)) \ P (lub (range Y))" - -subsection {* Admissibility and fixed point induction *} - -text {* access to definitions *} + "adm P \ \Y. chain Y \ (\i. P (Y i)) \ P (\i. Y i)" lemma admI: - "(\Y. \chain Y; \i. P (Y i)\ \ P (lub (range Y))) \ adm P" + "(\Y. \chain Y; \i. P (Y i)\ \ P (\i. Y i)) \ adm P" apply (unfold adm_def) apply blast done @@ -32,43 +28,42 @@ apply (erule spec) done -lemma admD: "\adm P; chain Y; \i. P (Y i)\ \ P (lub (range Y))" +lemma admD: "\adm P; chain Y; \i. P (Y i)\ \ P (\i. Y i)" apply (unfold adm_def) apply blast done +text {* improved admissibility introduction *} + +lemma admI2: + "(\Y. \chain Y; \i. P (Y i); \i. \j>i. Y i \ Y j \ Y i \ Y j\ + \ P (\i. Y i)) \ adm P" +apply (rule admI) +apply (erule (1) increasing_chain_adm_lemma) +apply fast +done + +subsection {* Admissibility on chain-finite types *} + 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)" + "\Y. chain (Y::nat \ 'a) \ (\n. max_in_chain n Y) + \ adm (P::'a \ bool)" apply (unfold adm_def) apply (intro strip) apply (drule spec) apply (drule mp) apply assumption apply (erule exE) -apply (subst lub_finch1 [THEN thelubI]) -apply assumption -apply assumption -apply (erule spec) +apply (simp add: maxinch_is_thelub) done lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard] -text {* improved admissibility introduction *} +subsection {* Admissibility of special formulae and propagation *} -lemma admI2: - "(\Y. \chain Y; \i. P (Y i); \i. \j>i. Y i \ Y j \ Y i \ Y j\ - \ P (lub (range Y))) \ adm P" -apply (rule admI) -apply (erule increasing_chain_adm_lemma) -apply assumption -apply fast -done - -text {* admissibility of special formulae and propagation *} - -lemma adm_less [simp]: "\cont u; cont v\ \ adm (\x. u x \ v x)" +lemma adm_less: "\cont u; cont v\ \ adm (\x. u x \ v x)" apply (rule admI) apply (simp add: cont2contlub [THEN contlubE]) apply (rule lub_mono) @@ -96,14 +91,13 @@ lemma adm_all: "\y. adm (P y) \ adm (\x. \y. P y x)" by (fast intro: admI elim: admD) -lemmas adm_all2 = allI [THEN adm_all, standard] +lemmas adm_all2 = adm_all [rule_format] lemma adm_subst: "\cont t; adm P\ \ adm (\x. P (t x))" apply (rule admI) apply (simp add: cont2contlub [THEN contlubE]) apply (erule admD) -apply (erule cont2mono [THEN ch2ch_monofun]) -apply assumption +apply (erule (1) cont2mono [THEN ch2ch_monofun]) apply assumption done @@ -114,7 +108,7 @@ 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 adm_conj) +by (simp add: po_eq_conv adm_conj adm_less) text {* admissibility for disjunction is hard to prove. It takes 7 Lemmas *} @@ -131,46 +125,41 @@ done lemma adm_disj_lemma2: - "\adm P; \X. chain X \ (\n. P (X n)) \ - lub (range Y) = lub (range X)\ \ P (lub (range Y))" + "\adm P; \X. chain X \ (\n. P (X n)) \ (\i. Y i) = (\i. X i)\ + \ P (\i. Y i)" by (force elim: admD) lemma adm_disj_lemma3: - "\chain (Y::nat=>'a::cpo); \i. \j\i. P (Y j)\ \ - chain (\m. Y (LEAST j. m \ j \ P (Y j)))" + "\chain (Y::nat \ 'a::cpo); \i. \j\i. P (Y j)\ + \ chain (\m. Y (LEAST j. m \ j \ P (Y j)))" apply (rule chainI) apply (erule chain_mono3) apply (rule Least_le) +apply (drule_tac x="Suc i" in spec) apply (rule conjI) apply (rule Suc_leD) -apply (erule allE) -apply (erule exE) -apply (erule LeastI [THEN conjunct1]) -apply (erule allE) -apply (erule exE) -apply (erule LeastI [THEN conjunct2]) +apply (erule LeastI_ex [THEN conjunct1]) +apply (erule LeastI_ex [THEN conjunct2]) done lemma adm_disj_lemma4: "\\i. \j\i. P (Y j)\ \ \m. P (Y (LEAST j::nat. m \ j \ P (Y j)))" apply (rule allI) -apply (erule allE) -apply (erule exE) -apply (erule LeastI [THEN conjunct2]) +apply (drule_tac x=m in spec) +apply (erule LeastI_ex [THEN conjunct2]) done lemma adm_disj_lemma5: - "\chain (Y::nat=>'a::cpo); \i. \j\i. P(Y j)\ \ - lub (range Y) = (LUB m. Y (LEAST j. m \ j \ P (Y j)))" + "\chain (Y::nat \ 'a::cpo); \i. \j\i. P (Y j)\ \ + (\m. Y m) = (\m. Y (LEAST j. m \ j \ P (Y j)))" apply (rule antisym_less) apply (rule lub_mono) 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 (drule_tac x=k in spec) + apply (erule LeastI_ex [THEN conjunct1]) apply (rule lub_mono3) apply (erule (1) adm_disj_lemma3) apply assumption @@ -180,19 +169,19 @@ done lemma adm_disj_lemma6: - "\chain (Y::nat=>'a::cpo); \i. \j\i. P(Y j)\ \ - \X. chain X \ (\n. P (X n)) \ lub (range Y) = lub (range X)" + "\chain (Y::nat \ 'a::cpo); \i. \j\i. P(Y j)\ \ + \X. chain X \ (\n. P (X n)) \ (\i. Y i) = (\i. X i)" apply (rule_tac x = "\m. Y (LEAST j. m \ j \ 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; \i. \j\i. P (Y j)\ \ P (lub (range Y))" + "\adm P; chain Y; \i. \j\i. P (Y j)\ \ P (\i. Y i)" apply (erule adm_disj_lemma2) apply (erule (1) adm_disj_lemma6) done -lemma adm_disj: "[| adm P; adm Q |] ==> adm(%x. P x | Q x)" +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) @@ -214,7 +203,7 @@ by (subst de_Morgan_conj, rule adm_disj) lemmas adm_lemmas = - adm_conj adm_not_free adm_imp adm_disj adm_eq adm_not_UU + adm_less 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]