src/HOL/HOLCF/ex/Pattern_Match.thy

 (*  Title:      HOL/HOLCF/ex/Pattern_Match.thy
     Author:     Brian Huffman
 *)
 
-section {* An experimental pattern-matching notation *}
+section \<open>An experimental pattern-matching notation\<close>
 
 theory Pattern_Match
 imports HOLCF
 begin
 
 default_sort pcpo
 
-text {* FIXME: Find a proper way to un-hide constants. *}
+text \<open>FIXME: Find a proper way to un-hide constants.\<close>
 
 abbreviation fail :: "'a match"
 where "fail \<equiv> Fixrec.fail"
 
 abbreviation succeed :: "'a \<rightarrow> 'a match"
 where "succeed \<equiv> Fixrec.succeed"
 
 abbreviation run :: "'a match \<rightarrow> 'a"
 where "run \<equiv> Fixrec.run"
 
-subsection {* Fatbar combinator *}
+subsection \<open>Fatbar combinator\<close>
 
 definition
   fatbar :: "('a \<rightarrow> 'b match) \<rightarrow> ('a \<rightarrow> 'b match) \<rightarrow> ('a \<rightarrow> 'b match)" where
   "fatbar = (\<Lambda> a b x. a\<cdot>x +++ b\<cdot>x)"
 

 lemma run_fatbar3: "m\<cdot>x = succeed\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y"
 by (simp add: fatbar_def)
 
 lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
 
-subsection {* Bind operator for match monad *}
+subsection \<open>Bind operator for match monad\<close>
 
 definition match_bind :: "'a match \<rightarrow> ('a \<rightarrow> 'b match) \<rightarrow> 'b match" where
   "match_bind = (\<Lambda> m k. sscase\<cdot>(\<Lambda> _. fail)\<cdot>(fup\<cdot>k)\<cdot>(Rep_match m))"
 
 lemma match_bind_simps [simp]:

   "match_bind\<cdot>(succeed\<cdot>x)\<cdot>k = k\<cdot>x"
 unfolding match_bind_def fail_def succeed_def
 by (simp_all add: cont_Rep_match cont_Abs_match
   Rep_match_strict Abs_match_inverse)
 
-subsection {* Case branch combinator *}
+subsection \<open>Case branch combinator\<close>
 
 definition
   branch :: "('a \<rightarrow> 'b match) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c match)" where
   "branch p \<equiv> \<Lambda> r x. match_bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. succeed\<cdot>(r\<cdot>y))"
 

 by (simp_all add: branch_def)
 
 lemma branch_succeed [simp]: "branch succeed\<cdot>r\<cdot>x = succeed\<cdot>(r\<cdot>x)"
 by (simp add: branch_def)
 
-subsection {* Cases operator *}
+subsection \<open>Cases operator\<close>
 
 definition
   cases :: "'a match \<rightarrow> 'a::pcpo" where
   "cases = Fixrec.run"
 
-text {* rewrite rules for cases *}
+text \<open>rewrite rules for cases\<close>
 
 lemma cases_strict [simp]: "cases\<cdot>\<bottom> = \<bottom>"
 by (simp add: cases_def)
 
 lemma cases_fail [simp]: "cases\<cdot>fail = \<bottom>"
 by (simp add: cases_def)
 
 lemma cases_succeed [simp]: "cases\<cdot>(succeed\<cdot>x) = x"
 by (simp add: cases_def)
 
-subsection {* Case syntax *}
+subsection \<open>Case syntax\<close>
 
 nonterminal Case_pat and Case_syn and Cases_syn
 
 syntax
   "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)

 
 translations
   "_Case_syntax x ms" == "CONST cases\<cdot>(ms\<cdot>x)"
   "_Case2 m ms" == "m \<parallel> ms"
 
-text {* Parsing Case expressions *}
+text \<open>Parsing Case expressions\<close>
 
 syntax
   "_pat" :: "'a"
   "_variable" :: "'a"
   "_noargs" :: "'a"

 translations
   "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_variable p r)"
   "_variable (_args x y) r" => "CONST csplit\<cdot>(_variable x (_variable y r))"
   "_variable _noargs r" => "CONST unit_when\<cdot>r"
 
-parse_translation {*
+parse_translation \<open>
 (* rewrite (_pat x) => (succeed) *)
 (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
  [(@{syntax_const "_pat"}, fn _ => fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
   Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
-*}
-
-text {* Printing Case expressions *}
+\<close>
+
+text \<open>Printing Case expressions\<close>
 
 syntax
   "_match" :: "'a"
 
-print_translation {*
+print_translation \<open>
   let
     fun dest_LAM (Const (@{const_syntax Rep_cfun},_) $ Const (@{const_syntax unit_when},_) $ t) =
           (Syntax.const @{syntax_const "_noargs"}, t)
     |   dest_LAM (Const (@{const_syntax Rep_cfun},_) $ Const (@{const_syntax csplit},_) $ t) =
           let

             Syntax.const @{syntax_const "_Case1"} $
               (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
           end;
 
   in [(@{const_syntax Rep_cfun}, K Case1_tr')] end;
-*}
+\<close>
 
 translations
   "x" <= "_match (CONST succeed) (_variable x)"
 
 
-subsection {* Pattern combinators for data constructors *}
+subsection \<open>Pattern combinators for data constructors\<close>
 
 type_synonym ('a, 'b) pat = "'a \<rightarrow> 'b match"
 
 definition
   cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where

 
 definition
   ONE_pat :: "(one, unit) pat" where
   "ONE_pat = (\<Lambda> ONE. succeed\<cdot>())"
 
-text {* Parse translations (patterns) *}
+text \<open>Parse translations (patterns)\<close>
 translations
   "_pat (XCONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
   "_pat (XCONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
   "_pat (XCONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
   "_pat (XCONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
   "_pat (XCONST up\<cdot>x)" => "CONST up_pat (_pat x)"
   "_pat (XCONST TT)" => "CONST TT_pat"
   "_pat (XCONST FF)" => "CONST FF_pat"
   "_pat (XCONST ONE)" => "CONST ONE_pat"
 
-text {* CONST version is also needed for constructors with special syntax *}
+text \<open>CONST version is also needed for constructors with special syntax\<close>
 translations
   "_pat (CONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
   "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
 
-text {* Parse translations (variables) *}
+text \<open>Parse translations (variables)\<close>
 translations
   "_variable (XCONST Pair x y) r" => "_variable (_args x y) r"
   "_variable (XCONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
   "_variable (XCONST sinl\<cdot>x) r" => "_variable x r"
   "_variable (XCONST sinr\<cdot>x) r" => "_variable x r"

 
 translations
   "_variable (CONST Pair x y) r" => "_variable (_args x y) r"
   "_variable (CONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
 
-text {* Print translations *}
+text \<open>Print translations\<close>
 translations
   "CONST Pair (_match p1 v1) (_match p2 v2)"
       <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)"
   "CONST spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
       <= "_match (CONST spair_pat p1 p2) (_args v1 v2)"

   "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
   "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>ONE = succeed\<cdot>r"
 by (simp_all add: branch_def ONE_pat_def)
 
 
-subsection {* Wildcards, as-patterns, and lazy patterns *}
+subsection \<open>Wildcards, as-patterns, and lazy patterns\<close>
 
 definition
   wild_pat :: "'a \<rightarrow> unit match" where
   "wild_pat = (\<Lambda> x. succeed\<cdot>())"
 

 
 definition
   lazy_pat :: "('a \<rightarrow> 'b::pcpo match) \<Rightarrow> ('a \<rightarrow> 'b match)" where
   "lazy_pat p = (\<Lambda> x. succeed\<cdot>(cases\<cdot>(p\<cdot>x)))"
 
-text {* Parse translations (patterns) *}
+text \<open>Parse translations (patterns)\<close>
 translations
   "_pat _" => "CONST wild_pat"
 
-text {* Parse translations (variables) *}
+text \<open>Parse translations (variables)\<close>
 translations
   "_variable _ r" => "_variable _noargs r"
 
-text {* Print translations *}
+text \<open>Print translations\<close>
 translations
   "_" <= "_match (CONST wild_pat) _noargs"
 
 lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = succeed\<cdot>r"
 by (simp add: branch_def wild_pat_def)

   "branch p\<cdot>r\<cdot>x = succeed\<cdot>s \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = succeed\<cdot>s"
 apply (simp_all add: branch_def lazy_pat_def)
 apply (cases "p\<cdot>x", simp_all)+
 done
 
-subsection {* Examples *}
+subsection \<open>Examples\<close>
 
 term "Case t of (:up\<cdot>(sinl\<cdot>x), sinr\<cdot>y:) \<Rightarrow> (x, y)"
 
 term "\<Lambda> t. Case t of up\<cdot>(sinl\<cdot>a) \<Rightarrow> a | up\<cdot>(sinr\<cdot>b) \<Rightarrow> b"
 
 term "\<Lambda> t. Case t of (:up\<cdot>(sinl\<cdot>_), sinr\<cdot>x:) \<Rightarrow> x"
 
-subsection {* ML code for generating definitions *}
-
-ML {*
+subsection \<open>ML code for generating definitions\<close>
+
+ML \<open>
 local open HOLCF_Library in
 
 infixr 6 ->>;
 infix 9 ` ;
 

   in
     (pat_stricts @ pat_apps, thy)
   end
 
 end
-*}
+\<close>
 
 (*
 Cut from HOLCF/Tools/domain_constructors.ML
 in function add_domain_constructors: