author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 19440  b2877e230b07 
child 25131  2c8caac48ade 
permissions  rwrr 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

1 
(* Title: HOLCF/Adm.thy 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

2 
ID: $Id$ 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

3 
Author: Franz Regensburger 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

4 
*) 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

5 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

6 
header {* Admissibility and compactness *} 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

7 

32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

8 
theory Adm 
16079
757e1c4a8081
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
huffman
parents:
16070
diff
changeset

9 
imports Cont 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

10 
begin 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

11 

32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

12 
defaultsort cpo 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

13 

32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

14 
subsection {* Definitions *} 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

15 

16565  16 
constdefs 
17 
adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" 

16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

18 
"adm P \<equiv> \<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

19 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

20 
compact :: "'a::cpo \<Rightarrow> bool" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

21 
"compact k \<equiv> adm (\<lambda>x. \<not> k \<sqsubseteq> x)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

22 

16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

23 
lemma admI: 
16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

24 
"(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P" 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

25 
by (unfold adm_def, fast) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

26 

16565  27 
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

28 
by (rule admI, erule spec) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

29 

16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

30 
lemma admD: "\<lbrakk>adm P; chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)" 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

31 
by (unfold adm_def, fast) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

32 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

33 
lemma compactI: "adm (\<lambda>x. \<not> k \<sqsubseteq> x) \<Longrightarrow> compact k" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

34 
by (unfold compact_def) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

35 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

36 
lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> x)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

37 
by (unfold compact_def) 
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 
text {* improved admissibility introduction *} 
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

40 

f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

41 
lemma admI2: 
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

42 
"(\<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> 
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

43 
\<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P" 
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

44 
apply (rule admI) 
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

45 
apply (erule (1) increasing_chain_adm_lemma) 
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

46 
apply fast 
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

47 
done 
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

48 

f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

49 
subsection {* Admissibility on chainfinite types *} 
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

50 

16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

51 
text {* for chainfinite (easy) types every formula is admissible *} 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

52 

32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

53 
lemma adm_max_in_chain: 
16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

54 
"\<forall>Y. chain (Y::nat \<Rightarrow> 'a) \<longrightarrow> (\<exists>n. max_in_chain n Y) 
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

55 
\<Longrightarrow> adm (P::'a \<Rightarrow> bool)" 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

56 
by (auto simp add: adm_def maxinch_is_thelub) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

57 

32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

58 
lemmas adm_chfin = chfin [THEN adm_max_in_chain, standard] 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

59 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

60 
lemma compact_chfin: "compact (x::'a::chfin)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

61 
by (rule compactI, rule adm_chfin) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

62 

16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

63 
subsection {* Admissibility of special formulae and propagation *} 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

64 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

65 
lemma adm_not_free: "adm (\<lambda>x. t)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

66 
by (rule admI, simp) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

67 

16565  68 
lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)" 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

69 
by (fast elim: admD intro: admI) 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

70 

16565  71 
lemma adm_all: "\<forall>y. adm (P y) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P y x)" 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

72 
by (fast intro: admI elim: admD) 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

73 

17586  74 
lemma adm_ball: "\<forall>y\<in>A. adm (P y) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P y x)" 
75 
by (fast intro: admI elim: admD) 

76 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

77 
lemmas adm_all2 = adm_all [rule_format] 
17586  78 
lemmas adm_ball2 = adm_ball [rule_format] 
79 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

80 
text {* Admissibility for disjunction is hard to prove. It takes 5 Lemmas *} 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

81 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

82 
lemma adm_disj_lemma1: 
16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

83 
"\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

84 
\<Longrightarrow> chain (\<lambda>i. Y (LEAST j. i \<le> j \<and> P (Y j)))" 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

85 
apply (rule chainI) 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

86 
apply (erule chain_mono3) 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

87 
apply (rule Least_le) 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

88 
apply (rule LeastI2_ex) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

89 
apply simp_all 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

90 
done 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

91 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

92 
lemmas adm_disj_lemma2 = LeastI_ex [of "\<lambda>j. i \<le> j \<and> P (Y j)", standard] 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

93 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

94 
lemma adm_disj_lemma3: 
16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

95 
"\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

96 
(\<Squnion>i. Y i) = (\<Squnion>i. Y (LEAST j. i \<le> j \<and> P (Y j)))" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

97 
apply (frule (1) adm_disj_lemma1) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

98 
apply (rule antisym_less) 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

99 
apply (rule lub_mono [rule_format], assumption+) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

100 
apply (erule chain_mono3) 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

101 
apply (simp add: adm_disj_lemma2) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

102 
apply (rule lub_range_mono, fast, assumption+) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

103 
done 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

104 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

105 
lemma adm_disj_lemma4: 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

106 
"\<lbrakk>adm P; chain Y; \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

107 
apply (subst adm_disj_lemma3, assumption+) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

108 
apply (erule admD) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

109 
apply (simp add: adm_disj_lemma1) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

110 
apply (simp add: adm_disj_lemma2) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

111 
done 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

112 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

113 
lemma adm_disj_lemma5: 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

114 
"\<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

115 
apply (erule contrapos_pp) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

116 
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

117 
apply (rule_tac x="max a b" in exI) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

118 
apply (simp add: le_maxI1 le_maxI2) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

119 
done 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

120 

16623
f3fcfa388ecb
cleaned up; added adm_less to adm_lemmas; added subsection headings
huffman
parents:
16565
diff
changeset

121 
lemma adm_disj: "\<lbrakk>adm P; adm Q\<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

122 
apply (rule admI) 
17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

123 
apply (erule adm_disj_lemma5 [THEN disjE]) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

124 
apply (erule (2) adm_disj_lemma4 [THEN disjI1]) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

125 
apply (erule (2) adm_disj_lemma4 [THEN disjI2]) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

126 
done 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

127 

16565  128 
lemma adm_imp: "\<lbrakk>adm (\<lambda>x. \<not> P x); adm Q\<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

129 
by (subst imp_conv_disj, rule adm_disj) 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

130 

16565  131 
lemma adm_iff: 
132 
"\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk> 

133 
\<Longrightarrow> adm (\<lambda>x. P x = Q x)" 

16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

134 
by (subst iff_conv_conj_imp, rule adm_conj) 
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

135 

16565  136 
lemma adm_not_conj: 
137 
"\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. \<not> Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> (P x \<and> Q x))" 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

138 
by (simp add: adm_imp) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

139 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

140 
text {* admissibility and continuity *} 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

141 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

142 
lemma adm_less: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

143 
apply (rule admI) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

144 
apply (simp add: cont2contlubE) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

145 
apply (rule lub_mono) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

146 
apply (erule (1) ch2ch_cont) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

147 
apply (erule (1) ch2ch_cont) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

148 
apply assumption 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

149 
done 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

150 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

151 
lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

152 
by (simp add: po_eq_conv adm_conj adm_less) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

153 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

154 
lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

155 
apply (rule admI) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

156 
apply (simp add: cont2contlubE) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

157 
apply (erule admD) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

158 
apply (erule (1) ch2ch_cont) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

159 
apply assumption 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

160 
done 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

161 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

162 
lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

163 
apply (rule admI) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

164 
apply (drule_tac x=0 in spec) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

165 
apply (erule contrapos_nn) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

166 
apply (erule rev_trans_less) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

167 
apply (erule cont2mono [THEN monofun_fun_arg]) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

168 
apply (erule is_ub_thelub) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

169 
done 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

170 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

171 
text {* admissibility and compactness *} 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

172 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

173 
lemma adm_compact_not_less: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

174 
by (unfold compact_def, erule adm_subst) 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

175 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

176 
lemma adm_neq_compact: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

177 
by (simp add: po_eq_conv adm_imp adm_not_less adm_compact_not_less) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

178 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

179 
lemma adm_compact_neq: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

180 
by (simp add: po_eq_conv adm_imp adm_not_less adm_compact_not_less) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

181 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

182 
lemma compact_UU [simp, intro]: "compact \<bottom>" 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

183 
by (rule compactI, simp add: adm_not_free) 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

184 

19440  185 
lemma adm_not_UU: "cont t \<Longrightarrow> adm (\<lambda>x. t x \<noteq> \<bottom>)" 
186 
by (simp add: adm_neq_compact) 

17814
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

187 

21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

188 
lemmas adm_lemmas [simp] = 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

189 
adm_not_free adm_conj adm_all2 adm_ball2 adm_disj adm_imp adm_iff 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

190 
adm_less adm_eq adm_not_less 
21183d6f62b8
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
huffman
parents:
17586
diff
changeset

191 
adm_compact_not_less adm_compact_neq adm_neq_compact adm_not_UU 
16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

192 

16062
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

193 
(* legacy ML bindings *) 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

194 
ML 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

195 
{* 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

196 
val adm_def = thm "adm_def"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

197 
val admI = thm "admI"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

198 
val triv_admI = thm "triv_admI"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

199 
val admD = thm "admD"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

200 
val adm_max_in_chain = thm "adm_max_in_chain"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

201 
val adm_chfin = thm "adm_chfin"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

202 
val admI2 = thm "admI2"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

203 
val adm_less = thm "adm_less"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

204 
val adm_conj = thm "adm_conj"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

205 
val adm_not_free = thm "adm_not_free"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

206 
val adm_not_less = thm "adm_not_less"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

207 
val adm_all = thm "adm_all"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

208 
val adm_all2 = thm "adm_all2"; 
17586  209 
val adm_ball = thm "adm_ball"; 
210 
val adm_ball2 = thm "adm_ball2"; 

16062
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

211 
val adm_subst = thm "adm_subst"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

212 
val adm_not_UU = thm "adm_not_UU"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

213 
val adm_eq = thm "adm_eq"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

214 
val adm_disj_lemma1 = thm "adm_disj_lemma1"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

215 
val adm_disj_lemma2 = thm "adm_disj_lemma2"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

216 
val adm_disj_lemma3 = thm "adm_disj_lemma3"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

217 
val adm_disj_lemma4 = thm "adm_disj_lemma4"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

218 
val adm_disj_lemma5 = thm "adm_disj_lemma5"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

219 
val adm_disj = thm "adm_disj"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

220 
val adm_imp = thm "adm_imp"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

221 
val adm_iff = thm "adm_iff"; 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

222 
val adm_not_conj = thm "adm_not_conj"; 
16565  223 
val adm_lemmas = thms "adm_lemmas"; 
16062
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

224 
*} 
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
16056
diff
changeset

225 

16056
32c3b7188c28
Moved admissibility definitions and lemmas to a separate theory
huffman
parents:
diff
changeset

226 
end 