src/HOL/HOLCF/Adm.thy
changeset 62175 8ffc4d0e652d
parent 58880 0baae4311a9f
child 63040 eb4ddd18d635
     1.1 --- a/src/HOL/HOLCF/Adm.thy	Wed Jan 13 23:02:28 2016 +0100
     1.2 +++ b/src/HOL/HOLCF/Adm.thy	Wed Jan 13 23:07:06 2016 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Franz Regensburger and Brian Huffman
     1.5  *)
     1.6  
     1.7 -section {* Admissibility and compactness *}
     1.8 +section \<open>Admissibility and compactness\<close>
     1.9  
    1.10  theory Adm
    1.11  imports Cont
    1.12 @@ -10,7 +10,7 @@
    1.13  
    1.14  default_sort cpo
    1.15  
    1.16 -subsection {* Definitions *}
    1.17 +subsection \<open>Definitions\<close>
    1.18  
    1.19  definition
    1.20    adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
    1.21 @@ -29,14 +29,14 @@
    1.22  lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
    1.23  by (rule admI, erule spec)
    1.24  
    1.25 -subsection {* Admissibility on chain-finite types *}
    1.26 +subsection \<open>Admissibility on chain-finite types\<close>
    1.27  
    1.28 -text {* For chain-finite (easy) types every formula is admissible. *}
    1.29 +text \<open>For chain-finite (easy) types every formula is admissible.\<close>
    1.30  
    1.31  lemma adm_chfin [simp]: "adm (P::'a::chfin \<Rightarrow> bool)"
    1.32  by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
    1.33  
    1.34 -subsection {* Admissibility of special formulae and propagation *}
    1.35 +subsection \<open>Admissibility of special formulae and propagation\<close>
    1.36  
    1.37  lemma adm_const [simp]: "adm (\<lambda>x. t)"
    1.38  by (rule admI, simp)
    1.39 @@ -53,7 +53,7 @@
    1.40    "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
    1.41  by (fast intro: admI elim: admD)
    1.42  
    1.43 -text {* Admissibility for disjunction is hard to prove. It requires 2 lemmas. *}
    1.44 +text \<open>Admissibility for disjunction is hard to prove. It requires 2 lemmas.\<close>
    1.45  
    1.46  lemma adm_disj_lemma1:
    1.47    assumes adm: "adm P"
    1.48 @@ -108,7 +108,7 @@
    1.49      \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
    1.50  by (subst iff_conv_conj_imp, rule adm_conj)
    1.51  
    1.52 -text {* admissibility and continuity *}
    1.53 +text \<open>admissibility and continuity\<close>
    1.54  
    1.55  lemma adm_below [simp]:
    1.56    "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
    1.57 @@ -124,7 +124,7 @@
    1.58  lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)"
    1.59  by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
    1.60  
    1.61 -subsection {* Compactness *}
    1.62 +subsection \<open>Compactness\<close>
    1.63  
    1.64  definition
    1.65    compact :: "'a::cpo \<Rightarrow> bool" where
    1.66 @@ -161,7 +161,7 @@
    1.67  apply (erule (1) below_trans [OF is_ub_thelub])
    1.68  done
    1.69  
    1.70 -text {* admissibility and compactness *}
    1.71 +text \<open>admissibility and compactness\<close>
    1.72  
    1.73  lemma adm_compact_not_below [simp]:
    1.74    "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)"
    1.75 @@ -178,7 +178,7 @@
    1.76  lemma compact_bottom [simp, intro]: "compact \<bottom>"
    1.77  by (rule compactI, simp)
    1.78  
    1.79 -text {* Any upward-closed predicate is admissible. *}
    1.80 +text \<open>Any upward-closed predicate is admissible.\<close>
    1.81  
    1.82  lemma adm_upward:
    1.83    assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y"