src/HOL/HOLCF/Adm.thy

 (*  Title:      HOL/HOLCF/Adm.thy
     Author:     Franz Regensburger and Brian Huffman
 *)
 
-section {* Admissibility and compactness *}
+section \<open>Admissibility and compactness\<close>
 
 theory Adm
 imports Cont
 begin
 
 default_sort cpo
 
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
 
 definition
   adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
   "adm P = (\<forall>Y. chain Y \<longrightarrow> (\<forall>i. P (Y i)) \<longrightarrow> P (\<Squnion>i. Y i))"
 

 unfolding adm_def by fast
 
 lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
 by (rule admI, erule spec)
 
-subsection {* Admissibility on chain-finite types *}
+subsection \<open>Admissibility on chain-finite types\<close>
 
-text {* For chain-finite (easy) types every formula is admissible. *}
+text \<open>For chain-finite (easy) types every formula is admissible.\<close>
 
 lemma adm_chfin [simp]: "adm (P::'a::chfin \<Rightarrow> bool)"
 by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
 
-subsection {* Admissibility of special formulae and propagation *}
+subsection \<open>Admissibility of special formulae and propagation\<close>
 
 lemma adm_const [simp]: "adm (\<lambda>x. t)"
 by (rule admI, simp)
 
 lemma adm_conj [simp]:

 
 lemma adm_ball [simp]:
   "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
 by (fast intro: admI elim: admD)
 
-text {* Admissibility for disjunction is hard to prove. It requires 2 lemmas. *}
+text \<open>Admissibility for disjunction is hard to prove. It requires 2 lemmas.\<close>
 
 lemma adm_disj_lemma1:
   assumes adm: "adm P"
   assumes chain: "chain Y"
   assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)"

 lemma adm_iff [simp]:
   "\<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)
 
-text {* admissibility and continuity *}
+text \<open>admissibility and continuity\<close>
 
 lemma adm_below [simp]:
   "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
 by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont)
 

 by (simp add: adm_def cont2contlubE ch2ch_cont)
 
 lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)"
 by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
 
-subsection {* Compactness *}
+subsection \<open>Compactness\<close>
 
 definition
   compact :: "'a::cpo \<Rightarrow> bool" where
   "compact k = adm (\<lambda>x. k \<notsqsubseteq> x)"
 

 apply (rule below_antisym)
 apply (erule (1) chain_mono)
 apply (erule (1) below_trans [OF is_ub_thelub])
 done
 
-text {* admissibility and compactness *}
+text \<open>admissibility and compactness\<close>
 
 lemma adm_compact_not_below [simp]:
   "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)"
 unfolding compact_def by (rule adm_subst)
 

 by (simp add: po_eq_conv)
 
 lemma compact_bottom [simp, intro]: "compact \<bottom>"
 by (rule compactI, simp)
 
-text {* Any upward-closed predicate is admissible. *}
+text \<open>Any upward-closed predicate is admissible.\<close>
 
 lemma adm_upward:
   assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y"
   shows "adm P"
 by (rule admI, drule spec, erule P, erule is_ub_thelub)