src/HOL/HOLCF/Adm.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 41959 b460124855b8
child 58880 0baae4311a9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 41430
diff changeset
     1
(*  Title:      HOL/HOLCF/Adm.thy
25895
0eaadfa8889e converted adm_all and adm_ball to rule_format; cleaned up
huffman
parents: 25880
diff changeset
     2
    Author:     Franz Regensburger and Brian Huffman
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     3
*)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     4
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
     5
header {* Admissibility and compactness *}
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     6
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     7
theory Adm
27181
e1e9b210d699 remove unnecessary import of Ffun;
huffman
parents: 26836
diff changeset
     8
imports Cont
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
     9
begin
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    10
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 31076
diff changeset
    11
default_sort cpo
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    12
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    13
subsection {* Definitions *}
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    14
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
    15
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
    16
  adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
    17
  "adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    18
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    19
lemma admI:
16623
f3fcfa388ecb cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents: 16565
diff changeset
    20
   "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
25895
0eaadfa8889e converted adm_all and adm_ball to rule_format; cleaned up
huffman
parents: 25880
diff changeset
    21
unfolding adm_def by fast
0eaadfa8889e converted adm_all and adm_ball to rule_format; cleaned up
huffman
parents: 25880
diff changeset
    22
25925
3dc4acca4388 change lemma admD to rule_format
huffman
parents: 25923
diff changeset
    23
lemma admD: "\<lbrakk>adm P; chain Y; \<And>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
25895
0eaadfa8889e converted adm_all and adm_ball to rule_format; cleaned up
huffman
parents: 25880
diff changeset
    24
unfolding adm_def by fast
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    25
27181
e1e9b210d699 remove unnecessary import of Ffun;
huffman
parents: 26836
diff changeset
    26
lemma admD2: "\<lbrakk>adm (\<lambda>x. \<not> P x); chain Y; P (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. P (Y i)"
e1e9b210d699 remove unnecessary import of Ffun;
huffman
parents: 26836
diff changeset
    27
unfolding adm_def by fast
e1e9b210d699 remove unnecessary import of Ffun;
huffman
parents: 26836
diff changeset
    28
16565
00a3bf006881 cleaned up
huffman
parents: 16207
diff changeset
    29
lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
    30
by (rule admI, erule spec)
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    31
16623
f3fcfa388ecb cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents: 16565
diff changeset
    32
subsection {* Admissibility on chain-finite types *}
f3fcfa388ecb cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents: 16565
diff changeset
    33
40623
dafba3a1dc5b declare adm_chfin [simp]
huffman
parents: 40500
diff changeset
    34
text {* For chain-finite (easy) types every formula is admissible. *}
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    35
40623
dafba3a1dc5b declare adm_chfin [simp]
huffman
parents: 40500
diff changeset
    36
lemma adm_chfin [simp]: "adm (P::'a::chfin \<Rightarrow> bool)"
25921
0ca392ab7f37 change class axiom chfin to rule_format
huffman
parents: 25895
diff changeset
    37
by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    38
16623
f3fcfa388ecb cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents: 16565
diff changeset
    39
subsection {* Admissibility of special formulae and propagation *}
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    40
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    41
lemma adm_const [simp]: "adm (\<lambda>x. t)"
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
    42
by (rule admI, simp)
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    43
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    44
lemma adm_conj [simp]:
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    45
  "\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
25925
3dc4acca4388 change lemma admD to rule_format
huffman
parents: 25923
diff changeset
    46
by (fast intro: admI elim: admD)
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    47
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    48
lemma adm_all [simp]:
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    49
  "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    50
by (fast intro: admI elim: admD)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    51
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    52
lemma adm_ball [simp]:
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    53
  "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
17586
df8b2f0e462e added theorem adm_ball
huffman
parents: 16738
diff changeset
    54
by (fast intro: admI elim: admD)
df8b2f0e462e added theorem adm_ball
huffman
parents: 16738
diff changeset
    55
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    56
text {* Admissibility for disjunction is hard to prove. It requires 2 lemmas. *}
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
    57
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    58
lemma adm_disj_lemma1:
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    59
  assumes adm: "adm P"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    60
  assumes chain: "chain Y"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    61
  assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    62
  shows "P (\<Squnion>i. Y i)"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    63
proof -
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    64
  def f \<equiv> "\<lambda>i. LEAST j. i \<le> j \<and> P (Y j)"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    65
  have chain': "chain (\<lambda>i. Y (f i))"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    66
    unfolding f_def
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    67
    apply (rule chainI)
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    68
    apply (rule chain_mono [OF chain])
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    69
    apply (rule Least_le)
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    70
    apply (rule LeastI2_ex)
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    71
    apply (simp_all add: P)
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    72
    done
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    73
  have f1: "\<And>i. i \<le> f i" and f2: "\<And>i. P (Y (f i))"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    74
    using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def)
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    75
  have lub_eq: "(\<Squnion>i. Y i) = (\<Squnion>i. Y (f i))"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    76
    apply (rule below_antisym)
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    77
    apply (rule lub_mono [OF chain chain'])
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    78
    apply (rule chain_mono [OF chain f1])
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    79
    apply (rule lub_range_mono [OF _ chain chain'])
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    80
    apply clarsimp
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    81
    done
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    82
  show "P (\<Squnion>i. Y i)"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    83
    unfolding lub_eq using adm chain' f2 by (rule admD)
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    84
qed
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    85
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    86
lemma adm_disj_lemma2:
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
    87
  "\<forall>n::nat. P n \<or> Q n \<Longrightarrow> (\<forall>i. \<exists>j\<ge>i. P j) \<or> (\<forall>i. \<exists>j\<ge>i. Q j)"
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
    88
apply (erule contrapos_pp)
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
    89
apply (clarsimp, rename_tac a b)
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
    90
apply (rule_tac x="max a b" in exI)
25895
0eaadfa8889e converted adm_all and adm_ball to rule_format; cleaned up
huffman
parents: 25880
diff changeset
    91
apply simp
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    92
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    93
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    94
lemma adm_disj [simp]:
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    95
  "\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)"
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
    96
apply (rule admI)
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    97
apply (erule adm_disj_lemma2 [THEN disjE])
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    98
apply (erule (2) adm_disj_lemma1 [THEN disjI1])
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
    99
apply (erule (2) adm_disj_lemma1 [THEN disjI2])
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   100
done
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   101
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   102
lemma adm_imp [simp]:
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   103
  "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   104
by (subst imp_conv_disj, rule adm_disj)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   105
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   106
lemma adm_iff [simp]:
16565
00a3bf006881 cleaned up
huffman
parents: 16207
diff changeset
   107
  "\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk>  
00a3bf006881 cleaned up
huffman
parents: 16207
diff changeset
   108
    \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   109
by (subst iff_conv_conj_imp, rule adm_conj)
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   110
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
   111
text {* admissibility and continuity *}
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
   112
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   113
lemma adm_below [simp]:
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   114
  "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
40435
a26503ac7c87 simplify some proofs
huffman
parents: 40430
diff changeset
   115
by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont)
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
   116
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   117
lemma adm_eq [simp]:
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   118
  "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   119
by (simp add: po_eq_conv)
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
   120
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   121
lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
40435
a26503ac7c87 simplify some proofs
huffman
parents: 40430
diff changeset
   122
by (simp add: adm_def cont2contlubE ch2ch_cont)
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   123
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40774
diff changeset
   124
lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)"
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   125
by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
   126
25880
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   127
subsection {* Compactness *}
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   128
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   129
definition
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   130
  compact :: "'a::cpo \<Rightarrow> bool" where
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40774
diff changeset
   131
  "compact k = adm (\<lambda>x. k \<notsqsubseteq> x)"
25880
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   132
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40774
diff changeset
   133
lemma compactI: "adm (\<lambda>x. k \<notsqsubseteq> x) \<Longrightarrow> compact k"
25880
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   134
unfolding compact_def .
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   135
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40774
diff changeset
   136
lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> x)"
25880
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   137
unfolding compact_def .
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   138
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   139
lemma compactI2:
27413
3154f3765cc7 replace lub (range Y) with (LUB i. Y i)
huffman
parents: 27290
diff changeset
   140
  "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
25880
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   141
unfolding compact_def adm_def by fast
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   142
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   143
lemma compactD2:
27413
3154f3765cc7 replace lub (range Y) with (LUB i. Y i)
huffman
parents: 27290
diff changeset
   144
  "\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
25880
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   145
unfolding compact_def adm_def by fast
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   146
39969
0b8e19f588a4 new lemmas about lub
huffman
parents: 36452
diff changeset
   147
lemma compact_below_lub_iff:
0b8e19f588a4 new lemmas about lub
huffman
parents: 36452
diff changeset
   148
  "\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
40500
ee9c8d36318e add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents: 40435
diff changeset
   149
by (fast intro: compactD2 elim: below_lub)
39969
0b8e19f588a4 new lemmas about lub
huffman
parents: 36452
diff changeset
   150
25880
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   151
lemma compact_chfin [simp]: "compact (x::'a::chfin)"
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   152
by (rule compactI [OF adm_chfin])
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   153
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   154
lemma compact_imp_max_in_chain:
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   155
  "\<lbrakk>chain Y; compact (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. max_in_chain i Y"
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   156
apply (drule (1) compactD2, simp)
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   157
apply (erule exE, rule_tac x=i in exI)
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   158
apply (rule max_in_chainI)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
   159
apply (rule below_antisym)
25922
cb04d05e95fb rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents: 25921
diff changeset
   160
apply (erule (1) chain_mono)
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
   161
apply (erule (1) below_trans [OF is_ub_thelub])
25880
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   162
done
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   163
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
   164
text {* admissibility and compactness *}
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
   165
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   166
lemma adm_compact_not_below [simp]:
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40774
diff changeset
   167
  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)"
25880
2c6cabe7a47c Compactness subsection with some new lemmas
huffman
parents: 25806
diff changeset
   168
unfolding compact_def by (rule adm_subst)
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   169
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   170
lemma adm_neq_compact [simp]:
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   171
  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   172
by (simp add: po_eq_conv)
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
   173
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   174
lemma adm_compact_neq [simp]:
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   175
  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   176
by (simp add: po_eq_conv)
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
   177
41430
1aa23e9f2c87 change some lemma names containing 'UU' to 'bottom'
huffman
parents: 41182
diff changeset
   178
lemma compact_bottom [simp, intro]: "compact \<bottom>"
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   179
by (rule compactI, simp)
17814
21183d6f62b8 added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents: 17586
diff changeset
   180
25802
8aea40e25aa8 new lemma adm_upward
huffman
parents: 25786
diff changeset
   181
text {* Any upward-closed predicate is admissible. *}
8aea40e25aa8 new lemma adm_upward
huffman
parents: 25786
diff changeset
   182
8aea40e25aa8 new lemma adm_upward
huffman
parents: 25786
diff changeset
   183
lemma adm_upward:
8aea40e25aa8 new lemma adm_upward
huffman
parents: 25786
diff changeset
   184
  assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y"
8aea40e25aa8 new lemma adm_upward
huffman
parents: 25786
diff changeset
   185
  shows "adm P"
8aea40e25aa8 new lemma adm_upward
huffman
parents: 25786
diff changeset
   186
by (rule admI, drule spec, erule P, erule is_ub_thelub)
8aea40e25aa8 new lemma adm_upward
huffman
parents: 25786
diff changeset
   187
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   188
lemmas adm_lemmas =
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   189
  adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
   190
  adm_below adm_eq adm_not_below
40007
bb04a995bbd3 cleaned up Adm.thy
huffman
parents: 39969
diff changeset
   191
  adm_compact_not_below adm_compact_neq adm_neq_compact
16056
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   192
32c3b7188c28 Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff changeset
   193
end