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.51      by (simp add: Cons(1))
    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>
   1.140    Fixrec.add_matchers
   1.141      [ (@{const_name Nil}, @{const_name match_Nil}),
   1.142        (@{const_name Cons}, @{const_name match_Cons}) ]
   1.143 -*}
   1.144 +\<close>
   1.145  
   1.146  end