src/HOL/HOLCF/Fixrec.thy
changeset 62175 8ffc4d0e652d
parent 58880 0baae4311a9f
child 65380 ae93953746fc
     1.1 --- a/src/HOL/HOLCF/Fixrec.thy	Wed Jan 13 23:02:28 2016 +0100
     1.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Wed Jan 13 23:07:06 2016 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  keywords "fixrec" :: thy_decl
     1.5  begin
     1.6  
     1.7 -subsection {* Pattern-match monad *}
     1.8 +subsection \<open>Pattern-match monad\<close>
     1.9  
    1.10  default_sort cpo
    1.11  
    1.12 @@ -46,13 +46,13 @@
    1.13    "succeed\<cdot>x \<noteq> fail" "fail \<noteq> succeed\<cdot>x"
    1.14  by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject)
    1.15  
    1.16 -subsubsection {* Run operator *}
    1.17 +subsubsection \<open>Run operator\<close>
    1.18  
    1.19  definition
    1.20    run :: "'a match \<rightarrow> 'a::pcpo" where
    1.21    "run = (\<Lambda> m. sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)\<cdot>(Rep_match m))"
    1.22  
    1.23 -text {* rewrite rules for run *}
    1.24 +text \<open>rewrite rules for run\<close>
    1.25  
    1.26  lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
    1.27  unfolding run_def
    1.28 @@ -66,7 +66,7 @@
    1.29  unfolding run_def succeed_def
    1.30  by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)
    1.31  
    1.32 -subsubsection {* Monad plus operator *}
    1.33 +subsubsection \<open>Monad plus operator\<close>
    1.34  
    1.35  definition
    1.36    mplus :: "'a match \<rightarrow> 'a match \<rightarrow> 'a match" where
    1.37 @@ -76,7 +76,7 @@
    1.38    mplus_syn :: "['a match, 'a match] \<Rightarrow> 'a match"  (infixr "+++" 65)  where
    1.39    "m1 +++ m2 == mplus\<cdot>m1\<cdot>m2"
    1.40  
    1.41 -text {* rewrite rules for mplus *}
    1.42 +text \<open>rewrite rules for mplus\<close>
    1.43  
    1.44  lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
    1.45  unfolding mplus_def
    1.46 @@ -96,7 +96,7 @@
    1.47  lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
    1.48  by (cases x, simp_all)
    1.49  
    1.50 -subsection {* Match functions for built-in types *}
    1.51 +subsection \<open>Match functions for built-in types\<close>
    1.52  
    1.53  default_sort pcpo
    1.54  
    1.55 @@ -192,12 +192,12 @@
    1.56    "match_FF\<cdot>\<bottom>\<cdot>k = \<bottom>"
    1.57  by (simp_all add: match_FF_def)
    1.58  
    1.59 -subsection {* Mutual recursion *}
    1.60 +subsection \<open>Mutual recursion\<close>
    1.61  
    1.62 -text {*
    1.63 +text \<open>
    1.64    The following rules are used to prove unfolding theorems from
    1.65    fixed-point definitions of mutually recursive functions.
    1.66 -*}
    1.67 +\<close>
    1.68  
    1.69  lemma Pair_equalI: "\<lbrakk>x \<equiv> fst p; y \<equiv> snd p\<rbrakk> \<Longrightarrow> (x, y) \<equiv> p"
    1.70  by simp
    1.71 @@ -216,22 +216,22 @@
    1.72    "\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f"
    1.73  by (simp add: fix_ind)
    1.74  
    1.75 -text {* lemma for proving rewrite rules *}
    1.76 +text \<open>lemma for proving rewrite rules\<close>
    1.77  
    1.78  lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
    1.79  by simp
    1.80  
    1.81  
    1.82 -subsection {* Initializing the fixrec package *}
    1.83 +subsection \<open>Initializing the fixrec package\<close>
    1.84  
    1.85  ML_file "Tools/holcf_library.ML"
    1.86  ML_file "Tools/fixrec.ML"
    1.87  
    1.88 -method_setup fixrec_simp = {*
    1.89 +method_setup fixrec_simp = \<open>
    1.90    Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)
    1.91 -*} "pattern prover for fixrec constants"
    1.92 +\<close> "pattern prover for fixrec constants"
    1.93  
    1.94 -setup {*
    1.95 +setup \<open>
    1.96    Fixrec.add_matchers
    1.97      [ (@{const_name up}, @{const_name match_up}),
    1.98        (@{const_name sinl}, @{const_name match_sinl}),
    1.99 @@ -242,7 +242,7 @@
   1.100        (@{const_name TT}, @{const_name match_TT}),
   1.101        (@{const_name FF}, @{const_name match_FF}),
   1.102        (@{const_name bottom}, @{const_name match_bottom}) ]
   1.103 -*}
   1.104 +\<close>
   1.105  
   1.106  hide_const (open) succeed fail run
   1.107