src/HOL/HOLCF/Library/List_Cpo.thy
 changeset 62175 8ffc4d0e652d parent 58880 0baae4311a9f child 67399 eab6ce8368fa
```     1.1 --- a/src/HOL/HOLCF/Library/List_Cpo.thy	Wed Jan 13 23:02:28 2016 +0100
1.2 +++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Wed Jan 13 23:07:06 2016 +0100
1.3 @@ -2,13 +2,13 @@
1.4      Author:     Brian Huffman
1.5  *)
1.6
1.7 -section {* Lists as a complete partial order *}
1.8 +section \<open>Lists as a complete partial order\<close>
1.9
1.10  theory List_Cpo
1.11  imports HOLCF
1.12  begin
1.13
1.14 -subsection {* Lists are a partial order *}
1.15 +subsection \<open>Lists are a partial order\<close>
1.16
1.17  instantiation list :: (po) po
1.18  begin
1.19 @@ -55,7 +55,7 @@
1.20    assumes 1: "P [] []"
1.21    assumes 2: "\<And>x y xs ys. \<lbrakk>x \<sqsubseteq> y; xs \<sqsubseteq> ys; P xs ys\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)"
1.22    shows "P xs ys"
1.23 -using `xs \<sqsubseteq> ys`
1.24 +using \<open>xs \<sqsubseteq> ys\<close>
1.25  proof (induct xs arbitrary: ys)
1.26    case Nil thus ?case by (simp add: 1)
1.27  next
1.28 @@ -100,20 +100,20 @@
1.29    assumes 1: "P (\<lambda>i. [])"
1.30    assumes 2: "\<And>A B. chain A \<Longrightarrow> chain B \<Longrightarrow> P B \<Longrightarrow> P (\<lambda>i. A i # B i)"
1.31    shows "P S"
1.32 -using `chain S`
1.33 +using \<open>chain S\<close>
1.34  proof (induct "S 0" arbitrary: S)
1.35    case Nil
1.36 -  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`])
1.37 +  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF \<open>chain S\<close>])
1.38    with Nil have "\<forall>i. S i = []" by simp
1.39    thus ?case by (simp add: 1)
1.40  next
1.41    case (Cons x xs)
1.42 -  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`])
1.43 +  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF \<open>chain S\<close>])
1.44    hence *: "\<forall>i. S i \<noteq> []" by (rule all_forward, insert Cons) auto
1.45    have "chain (\<lambda>i. hd (S i))" and "chain (\<lambda>i. tl (S i))"
1.46 -    using `chain S` by simp_all
1.47 +    using \<open>chain S\<close> by simp_all
1.48    moreover have "P (\<lambda>i. tl (S i))"
1.49 -    using `chain S` and `x # xs = S 0` [symmetric]
1.50 +    using \<open>chain S\<close> and \<open>x # xs = S 0\<close> [symmetric]
1.52    ultimately have "P (\<lambda>i. hd (S i) # tl (S i))"
1.53      by (rule 2)
1.54 @@ -126,7 +126,7 @@
1.55      A B where "chain A" and "chain B" and "S = (\<lambda>i. A i # B i)"
1.56  using S by (induct rule: list_chain_induct) simp_all
1.57
1.58 -subsection {* Lists are a complete partial order *}
1.59 +subsection \<open>Lists are a complete partial order\<close>
1.60
1.61  lemma is_lub_Cons:
1.62    assumes A: "range A <<| x"
1.63 @@ -147,7 +147,7 @@
1.64    qed
1.65  qed
1.66
1.67 -subsection {* Continuity of list operations *}
1.68 +subsection \<open>Continuity of list operations\<close>
1.69
1.70  lemma cont2cont_Cons [simp, cont2cont]:
1.71    assumes f: "cont (\<lambda>x. f x)"
1.72 @@ -193,8 +193,8 @@
1.73    shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
1.74  using assms by (simp add: cont2cont_case_list prod_cont_iff)
1.75
1.76 -text {* The simple version (due to Joachim Breitner) is needed if the
1.77 -  element type of the list is not a cpo. *}
1.78 +text \<open>The simple version (due to Joachim Breitner) is needed if the
1.79 +  element type of the list is not a cpo.\<close>
1.80
1.81  lemma cont2cont_case_list_simple [simp, cont2cont]:
1.82    assumes "cont (\<lambda>x. f1 x)"
1.83 @@ -202,7 +202,7 @@
1.84    shows "cont (\<lambda>x. case l of [] \<Rightarrow> f1 x | y # ys \<Rightarrow> f2 x y ys)"
1.85  using assms by (cases l) auto
1.86
1.87 -text {* Lemma for proving continuity of recursive list functions: *}
1.88 +text \<open>Lemma for proving continuity of recursive list functions:\<close>
1.89
1.90  lemma list_contI:
1.91    fixes f :: "'a::cpo list \<Rightarrow> 'b::cpo"
1.92 @@ -233,7 +233,7 @@
1.93      done
1.94  qed
1.95
1.96 -text {* Continuity rule for map *}
1.97 +text \<open>Continuity rule for map\<close>
1.98
1.99  lemma cont2cont_map [simp, cont2cont]:
1.100    assumes f: "cont (\<lambda>(x, y). f x y)"
1.101 @@ -246,11 +246,11 @@
1.102  apply (induct_tac y, simp, simp)
1.103  done
1.104
1.105 -text {* There are probably lots of other list operations that also
1.106 +text \<open>There are probably lots of other list operations that also
1.107  deserve to have continuity lemmas.  I'll add more as they are
1.108 -needed. *}
1.109 +needed.\<close>
1.110
1.111 -subsection {* Lists are a discrete cpo *}
1.112 +subsection \<open>Lists are a discrete cpo\<close>
1.113
1.114  instance list :: (discrete_cpo) discrete_cpo
1.115  proof
1.116 @@ -259,7 +259,7 @@
1.117      by (induct xs arbitrary: ys, case_tac [!] ys, simp_all)
1.118  qed
1.119
1.120 -subsection {* Compactness and chain-finiteness *}
1.121 +subsection \<open>Compactness and chain-finiteness\<close>
1.122
1.123  lemma compact_Nil [simp]: "compact []"
1.124  apply (rule compactI2)
1.125 @@ -298,7 +298,7 @@
1.126      by (rule compact_imp_max_in_chain)
1.127  qed
1.128
1.129 -subsection {* Using lists with fixrec *}
1.130 +subsection \<open>Using lists with fixrec\<close>
1.131
1.132  definition
1.133    match_Nil :: "'a::cpo list \<rightarrow> 'b match \<rightarrow> 'b match"
1.134 @@ -320,10 +320,10 @@
1.135    "match_Cons\<cdot>(x # xs)\<cdot>k = k\<cdot>x\<cdot>xs"
1.136  unfolding match_Cons_def by simp_all
1.137
1.138 -setup {*
1.139 +setup \<open>