src/HOL/HOLCF/Adm.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 63040 eb4ddd18d635
child 67312 0d25e02759b7
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@41959
     1
(*  Title:      HOL/HOLCF/Adm.thy
huffman@25895
     2
    Author:     Franz Regensburger and Brian Huffman
huffman@16056
     3
*)
huffman@16056
     4
wenzelm@62175
     5
section \<open>Admissibility and compactness\<close>
huffman@16056
     6
huffman@16056
     7
theory Adm
huffman@27181
     8
imports Cont
huffman@16056
     9
begin
huffman@16056
    10
wenzelm@36452
    11
default_sort cpo
huffman@16056
    12
wenzelm@62175
    13
subsection \<open>Definitions\<close>
huffman@16056
    14
wenzelm@25131
    15
definition
wenzelm@25131
    16
  adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
wenzelm@25131
    17
  "adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
huffman@16056
    18
huffman@16056
    19
lemma admI:
huffman@16623
    20
   "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
huffman@25895
    21
unfolding adm_def by fast
huffman@25895
    22
huffman@25925
    23
lemma admD: "\<lbrakk>adm P; chain Y; \<And>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
huffman@25895
    24
unfolding adm_def by fast
huffman@16056
    25
huffman@27181
    26
lemma admD2: "\<lbrakk>adm (\<lambda>x. \<not> P x); chain Y; P (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. P (Y i)"
huffman@27181
    27
unfolding adm_def by fast
huffman@27181
    28
huffman@16565
    29
lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
huffman@17814
    30
by (rule admI, erule spec)
huffman@16056
    31
wenzelm@62175
    32
subsection \<open>Admissibility on chain-finite types\<close>
huffman@16623
    33
wenzelm@62175
    34
text \<open>For chain-finite (easy) types every formula is admissible.\<close>
huffman@16056
    35
huffman@40623
    36
lemma adm_chfin [simp]: "adm (P::'a::chfin \<Rightarrow> bool)"
huffman@25921
    37
by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
huffman@16056
    38
wenzelm@62175
    39
subsection \<open>Admissibility of special formulae and propagation\<close>
huffman@16056
    40
huffman@40007
    41
lemma adm_const [simp]: "adm (\<lambda>x. t)"
huffman@17814
    42
by (rule admI, simp)
huffman@16056
    43
huffman@40007
    44
lemma adm_conj [simp]:
huffman@40007
    45
  "\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
huffman@25925
    46
by (fast intro: admI elim: admD)
huffman@16056
    47
huffman@40007
    48
lemma adm_all [simp]:
huffman@40007
    49
  "(\<And>y. adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P x y)"
huffman@16056
    50
by (fast intro: admI elim: admD)
huffman@16056
    51
huffman@40007
    52
lemma adm_ball [simp]:
huffman@40007
    53
  "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
huffman@17586
    54
by (fast intro: admI elim: admD)
huffman@17586
    55
wenzelm@62175
    56
text \<open>Admissibility for disjunction is hard to prove. It requires 2 lemmas.\<close>
huffman@17814
    57
huffman@40007
    58
lemma adm_disj_lemma1:
huffman@40007
    59
  assumes adm: "adm P"
huffman@40007
    60
  assumes chain: "chain Y"
huffman@40007
    61
  assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)"
huffman@40007
    62
  shows "P (\<Squnion>i. Y i)"
huffman@40007
    63
proof -
wenzelm@63040
    64
  define f where "f i = (LEAST j. i \<le> j \<and> P (Y j))" for i
huffman@40007
    65
  have chain': "chain (\<lambda>i. Y (f i))"
huffman@40007
    66
    unfolding f_def
huffman@40007
    67
    apply (rule chainI)
huffman@40007
    68
    apply (rule chain_mono [OF chain])
huffman@40007
    69
    apply (rule Least_le)
huffman@40007
    70
    apply (rule LeastI2_ex)
huffman@40007
    71
    apply (simp_all add: P)
huffman@40007
    72
    done
huffman@40007
    73
  have f1: "\<And>i. i \<le> f i" and f2: "\<And>i. P (Y (f i))"
huffman@40007
    74
    using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def)
huffman@40007
    75
  have lub_eq: "(\<Squnion>i. Y i) = (\<Squnion>i. Y (f i))"
huffman@40007
    76
    apply (rule below_antisym)
huffman@40007
    77
    apply (rule lub_mono [OF chain chain'])
huffman@40007
    78
    apply (rule chain_mono [OF chain f1])
huffman@40007
    79
    apply (rule lub_range_mono [OF _ chain chain'])
huffman@40007
    80
    apply clarsimp
huffman@40007
    81
    done
huffman@40007
    82
  show "P (\<Squnion>i. Y i)"
huffman@40007
    83
    unfolding lub_eq using adm chain' f2 by (rule admD)
huffman@40007
    84
qed
huffman@16056
    85
huffman@40007
    86
lemma adm_disj_lemma2:
huffman@17814
    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)"
huffman@17814
    88
apply (erule contrapos_pp)
huffman@17814
    89
apply (clarsimp, rename_tac a b)
huffman@17814
    90
apply (rule_tac x="max a b" in exI)
huffman@25895
    91
apply simp
huffman@16056
    92
done
huffman@16056
    93
huffman@40007
    94
lemma adm_disj [simp]:
huffman@40007
    95
  "\<lbrakk>adm (\<lambda>x. P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<or> Q x)"
huffman@16056
    96
apply (rule admI)
huffman@40007
    97
apply (erule adm_disj_lemma2 [THEN disjE])
huffman@40007
    98
apply (erule (2) adm_disj_lemma1 [THEN disjI1])
huffman@40007
    99
apply (erule (2) adm_disj_lemma1 [THEN disjI2])
huffman@16056
   100
done
huffman@16056
   101
huffman@40007
   102
lemma adm_imp [simp]:
huffman@40007
   103
  "\<lbrakk>adm (\<lambda>x. \<not> P x); adm (\<lambda>x. Q x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<longrightarrow> Q x)"
huffman@16056
   104
by (subst imp_conv_disj, rule adm_disj)
huffman@16056
   105
huffman@40007
   106
lemma adm_iff [simp]:
huffman@16565
   107
  "\<lbrakk>adm (\<lambda>x. P x \<longrightarrow> Q x); adm (\<lambda>x. Q x \<longrightarrow> P x)\<rbrakk>  
huffman@16565
   108
    \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
huffman@16056
   109
by (subst iff_conv_conj_imp, rule adm_conj)
huffman@16056
   110
wenzelm@62175
   111
text \<open>admissibility and continuity\<close>
huffman@17814
   112
huffman@40007
   113
lemma adm_below [simp]:
huffman@40007
   114
  "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
huffman@40435
   115
by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont)
huffman@17814
   116
huffman@40007
   117
lemma adm_eq [simp]:
huffman@40007
   118
  "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
huffman@40007
   119
by (simp add: po_eq_conv)
huffman@17814
   120
huffman@40007
   121
lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
huffman@40435
   122
by (simp add: adm_def cont2contlubE ch2ch_cont)
huffman@16056
   123
huffman@41182
   124
lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)"
huffman@40007
   125
by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
huffman@17814
   126
wenzelm@62175
   127
subsection \<open>Compactness\<close>
huffman@25880
   128
huffman@25880
   129
definition
huffman@25880
   130
  compact :: "'a::cpo \<Rightarrow> bool" where
huffman@41182
   131
  "compact k = adm (\<lambda>x. k \<notsqsubseteq> x)"
huffman@25880
   132
huffman@41182
   133
lemma compactI: "adm (\<lambda>x. k \<notsqsubseteq> x) \<Longrightarrow> compact k"
huffman@25880
   134
unfolding compact_def .
huffman@25880
   135
huffman@41182
   136
lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> x)"
huffman@25880
   137
unfolding compact_def .
huffman@25880
   138
huffman@25880
   139
lemma compactI2:
huffman@27413
   140
  "(\<And>Y. \<lbrakk>chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i) \<Longrightarrow> compact x"
huffman@25880
   141
unfolding compact_def adm_def by fast
huffman@25880
   142
huffman@25880
   143
lemma compactD2:
huffman@27413
   144
  "\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i"
huffman@25880
   145
unfolding compact_def adm_def by fast
huffman@25880
   146
huffman@39969
   147
lemma compact_below_lub_iff:
huffman@39969
   148
  "\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
huffman@40500
   149
by (fast intro: compactD2 elim: below_lub)
huffman@39969
   150
huffman@25880
   151
lemma compact_chfin [simp]: "compact (x::'a::chfin)"
huffman@25880
   152
by (rule compactI [OF adm_chfin])
huffman@25880
   153
huffman@25880
   154
lemma compact_imp_max_in_chain:
huffman@25880
   155
  "\<lbrakk>chain Y; compact (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. max_in_chain i Y"
huffman@25880
   156
apply (drule (1) compactD2, simp)
huffman@25880
   157
apply (erule exE, rule_tac x=i in exI)
huffman@25880
   158
apply (rule max_in_chainI)
huffman@31076
   159
apply (rule below_antisym)
huffman@25922
   160
apply (erule (1) chain_mono)
huffman@31076
   161
apply (erule (1) below_trans [OF is_ub_thelub])
huffman@25880
   162
done
huffman@25880
   163
wenzelm@62175
   164
text \<open>admissibility and compactness\<close>
huffman@17814
   165
huffman@40007
   166
lemma adm_compact_not_below [simp]:
huffman@41182
   167
  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)"
huffman@25880
   168
unfolding compact_def by (rule adm_subst)
huffman@16056
   169
huffman@40007
   170
lemma adm_neq_compact [simp]:
huffman@40007
   171
  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
huffman@40007
   172
by (simp add: po_eq_conv)
huffman@17814
   173
huffman@40007
   174
lemma adm_compact_neq [simp]:
huffman@40007
   175
  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
huffman@40007
   176
by (simp add: po_eq_conv)
huffman@17814
   177
huffman@41430
   178
lemma compact_bottom [simp, intro]: "compact \<bottom>"
huffman@40007
   179
by (rule compactI, simp)
huffman@17814
   180
wenzelm@62175
   181
text \<open>Any upward-closed predicate is admissible.\<close>
huffman@25802
   182
huffman@25802
   183
lemma adm_upward:
huffman@25802
   184
  assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y"
huffman@25802
   185
  shows "adm P"
huffman@25802
   186
by (rule admI, drule spec, erule P, erule is_ub_thelub)
huffman@25802
   187
huffman@40007
   188
lemmas adm_lemmas =
huffman@40007
   189
  adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
huffman@31076
   190
  adm_below adm_eq adm_not_below
huffman@40007
   191
  adm_compact_not_below adm_compact_neq adm_neq_compact
huffman@16056
   192
huffman@16056
   193
end