add case syntax stuff
authorhuffman
Sun Nov 06 01:21:37 2005 +0100 (2005-11-06)
changeset 18097d196d84c306f
parent 18096 574aa0487069
child 18098 227ecb2cfa3d
add case syntax stuff
src/HOLCF/Fixrec.thy
     1.1 --- a/src/HOLCF/Fixrec.thy	Sun Nov 06 00:35:24 2005 +0100
     1.2 +++ b/src/HOLCF/Fixrec.thy	Sun Nov 06 01:21:37 2005 +0100
     1.3 @@ -31,12 +31,14 @@
     1.4  apply (rule_tac p=y in upE, simp, simp)
     1.5  done
     1.6  
     1.7 -subsection {* Monadic bind operator *}
     1.8 +subsubsection {* Monadic bind operator *}
     1.9  
    1.10 -consts
    1.11 -  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" (infixl ">>=" 50)
    1.12 -defs
    1.13 -  bind_def: "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
    1.14 +constdefs
    1.15 +  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
    1.16 +  "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
    1.17 +
    1.18 +syntax ">>=" :: "['a maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'b maybe" (infixl ">>=" 50)
    1.19 +translations "m >>= f" == "bind\<cdot>m\<cdot>f"
    1.20  
    1.21  nonterminals
    1.22    maybebind maybebinds
    1.23 @@ -71,7 +73,7 @@
    1.24   "(do b <- (do a <- m; k\<cdot>a); h\<cdot>b) = (do a <- m; b <- k\<cdot>a; h\<cdot>b)"
    1.25  by (rule_tac p=m in maybeE, simp_all)
    1.26  
    1.27 -subsection {* Run operator *}
    1.28 +subsubsection {* Run operator *}
    1.29  
    1.30  constdefs
    1.31    run:: "'a::pcpo maybe \<rightarrow> 'a"
    1.32 @@ -88,12 +90,14 @@
    1.33  lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"
    1.34  by (simp add: run_def return_def)
    1.35  
    1.36 -subsection {* Monad plus operator *}
    1.37 +subsubsection {* Monad plus operator *}
    1.38  
    1.39 -consts
    1.40 -  mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" (infixr "+++" 65)
    1.41 -defs
    1.42 -  mplus_def: "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
    1.43 +constdefs
    1.44 +  mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
    1.45 +  "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
    1.46 +
    1.47 +syntax "+++" :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65)
    1.48 +translations "m1 +++ m2" == "mplus\<cdot>m1\<cdot>m2"
    1.49  
    1.50  text {* rewrite rules for mplus *}
    1.51  
    1.52 @@ -112,6 +116,193 @@
    1.53  lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
    1.54  by (rule_tac p=x in maybeE, simp_all)
    1.55  
    1.56 +subsubsection {* Fatbar combinator *}
    1.57 +
    1.58 +constdefs
    1.59 +  fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)"
    1.60 +  "fatbar \<equiv> \<Lambda> a b x. a\<cdot>x +++ b\<cdot>x"
    1.61 +
    1.62 +syntax
    1.63 +  "\<parallel>" :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60)
    1.64 +translations
    1.65 +  "m1 \<parallel> m2" == "fatbar\<cdot>m1\<cdot>m2"
    1.66 +
    1.67 +lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>"
    1.68 +by (simp add: fatbar_def)
    1.69 +
    1.70 +lemma fatbar2: "m\<cdot>x = fail \<Longrightarrow> (m \<parallel> ms)\<cdot>x = ms\<cdot>x"
    1.71 +by (simp add: fatbar_def)
    1.72 +
    1.73 +lemma fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> (m \<parallel> ms)\<cdot>x = return\<cdot>y"
    1.74 +by (simp add: fatbar_def)
    1.75 +
    1.76 +lemmas fatbar_simps = fatbar1 fatbar2 fatbar3
    1.77 +
    1.78 +subsection {* Pattern combinators *}
    1.79 +
    1.80 +types ('a,'b,'c) pattern = "'b \<rightarrow> 'a \<rightarrow> 'c maybe"
    1.81 +
    1.82 +constdefs
    1.83 +  wild_pat :: "('a, 'b, 'b) pattern"
    1.84 +  "wild_pat \<equiv> \<Lambda> r a. return\<cdot>r"
    1.85 +
    1.86 +  var_pat :: "('a, 'a \<rightarrow> 'b, 'b) pattern"
    1.87 +  "var_pat \<equiv> \<Lambda> r a. return\<cdot>(r\<cdot>a)"
    1.88 +
    1.89 +  as_pat :: "('a, 'b, 'c) pattern \<Rightarrow> ('a, 'a \<rightarrow> 'b, 'c) pattern"
    1.90 +  "as_pat p \<equiv> \<Lambda> r a. p\<cdot>(r\<cdot>a)\<cdot>a"
    1.91 +
    1.92 +lemma wild_pat [simp]: "wild_pat\<cdot>r\<cdot>a = return\<cdot>r"
    1.93 +by (simp add: wild_pat_def)
    1.94 +
    1.95 +lemma var_pat [simp]: "var_pat\<cdot>r\<cdot>a = return\<cdot>(r\<cdot>a)"
    1.96 +by (simp add: var_pat_def)
    1.97 +
    1.98 +lemma as_pat [simp]: "as_pat p\<cdot>r\<cdot>a = p\<cdot>(r\<cdot>a)\<cdot>a"
    1.99 +by (simp add: as_pat_def)
   1.100 +
   1.101 +subsection {* Case syntax *}
   1.102 +
   1.103 +nonterminals
   1.104 +  Case_syn  Cases_syn
   1.105 +
   1.106 +syntax
   1.107 +  "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
   1.108 +  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ =>/ _)" 10)
   1.109 +  ""            :: "Case_syn => Cases_syn"               ("_")
   1.110 +  "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  ("_/ | _")
   1.111 +  "_as_pattern" :: "[idt, 'a] \<Rightarrow> 'a"                     (infixr "as" 10)
   1.112 +
   1.113 +syntax (xsymbols)
   1.114 +  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
   1.115 +
   1.116 +syntax
   1.117 +  "_match"   :: "'a \<Rightarrow> Case_syn" (* or Cases_syn *)
   1.118 +  "_as"      :: "[pttrn, Case_syn] \<Rightarrow> Case_syn"
   1.119 +  "_matches" :: "['a, Case_syn, 'a list] \<Rightarrow> Case_syn"
   1.120 +  "_cons"    :: "['a, 'a list] \<Rightarrow> 'a list"
   1.121 +  "_nil"     :: "'a list"
   1.122 +
   1.123 +translations
   1.124 +  "_Case_syntax x (_match m)"     == "run\<cdot>(m\<cdot>x)"
   1.125 +  "_Case2 (_match c) (_match cs)" == "_match (c \<parallel> cs)"
   1.126 +  "_Case1 dummy_pattern r"        == "_match (wild_pat\<cdot>r)"
   1.127 +  "_as x (_match (p\<cdot>t))"          == "_match ((as_pat p)\<cdot>(\<Lambda> x. t))"
   1.128 +  "_Case1 (_as_pattern x e) r"    == "_as x (_Case1 e r)"
   1.129 +  "_Case1 x t"                    == "_match (var_pat\<cdot>(\<Lambda> x. t))"
   1.130 +  "_Case1 (f\<cdot>e) r" == "_matches f (_Case1 e r) _nil"
   1.131 +  "_matches (f\<cdot>e) (_match (p\<cdot>r)) ps" == "_matches f (_Case1 e r) (_cons p ps)"
   1.132 +
   1.133 +lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>"
   1.134 +by (simp add: fatbar_def)
   1.135 +
   1.136 +lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)"
   1.137 +by (simp add: fatbar_def)
   1.138 +
   1.139 +lemma run_fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y"
   1.140 +by (simp add: fatbar_def)
   1.141 +
   1.142 +lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
   1.143 +
   1.144 +subsection {* Pattern combinators for built-in types *}
   1.145 +
   1.146 +constdefs
   1.147 +  cpair_pat :: "_"
   1.148 +  "cpair_pat p1 p2 \<equiv> \<Lambda> r1 \<langle>x1,x2\<rangle>. bind\<cdot>(p1\<cdot>r1\<cdot>x1)\<cdot>(\<Lambda> r2. p2\<cdot>r2\<cdot>x2)"
   1.149 +
   1.150 +  spair_pat :: "_"
   1.151 +  "spair_pat p1 p2 \<equiv> \<Lambda> r (:x,y:). cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x,y\<rangle>"
   1.152 +
   1.153 +  sinl_pat :: "_"
   1.154 +  "sinl_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x | sinr\<cdot>y \<Rightarrow> fail"
   1.155 +
   1.156 +  sinr_pat :: "_"
   1.157 +  "sinr_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> fail | sinr\<cdot>y \<Rightarrow> p\<cdot>r\<cdot>y"
   1.158 +
   1.159 +  up_pat :: "_"
   1.160 +  "up_pat p \<equiv> \<Lambda> r a. case a of up\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x"
   1.161 +
   1.162 +  Def_pat :: "'a::type \<Rightarrow> ('a lift, 'b, 'b) pattern"
   1.163 +  "Def_pat x \<equiv> \<Lambda> r. FLIFT y. if x = y then return\<cdot>r else fail"
   1.164 +
   1.165 +  ONE_pat :: "_"
   1.166 +  "ONE_pat \<equiv> \<Lambda> r ONE. return\<cdot>r"
   1.167 +
   1.168 +  TT_pat :: "(tr, _, _) pattern"
   1.169 +  "TT_pat \<equiv> \<Lambda> r b. If b then return\<cdot>r else fail fi"
   1.170 +
   1.171 +  FF_pat :: "(tr, _, _) pattern"
   1.172 +  "FF_pat \<equiv> \<Lambda> r b. If b then fail else return\<cdot>r fi"
   1.173 +
   1.174 +translations
   1.175 +  "_matches cpair (_match (p1\<cdot>r)) (_cons p2 _nil)"
   1.176 +    == "_match ((cpair_pat p1 p2)\<cdot>r)"
   1.177 +
   1.178 +  "_matches spair (_match (p1\<cdot>r)) (_cons p2 _nil)"
   1.179 +    == "_match ((spair_pat p1 p2)\<cdot>r)"
   1.180 +
   1.181 +translations
   1.182 +  "_matches sinl (_match (p1\<cdot>r)) _nil" == "_match ((sinl_pat p1)\<cdot>r)"
   1.183 +  "_matches sinr (_match (p1\<cdot>r)) _nil" == "_match ((sinr_pat p1)\<cdot>r)"
   1.184 +  "_matches up (_match (p1\<cdot>r)) _nil" == "_match ((up_pat p1)\<cdot>r)"
   1.185 +
   1.186 +translations
   1.187 +  "_Case1 (Def x) r" == "_match (Def_pat x\<cdot>r)"
   1.188 +  "_Case1 ONE r" == "_match (ONE_pat\<cdot>r)"
   1.189 +  "_Case1 TT r" == "_match (TT_pat\<cdot>r)"
   1.190 +  "_Case1 FF r" == "_match (FF_pat\<cdot>r)"
   1.191 +
   1.192 +lemma cpair_pat_simps [simp]:
   1.193 +  "p1\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = \<bottom>"
   1.194 +  "p1\<cdot>r\<cdot>x = fail \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = fail"
   1.195 +  "p1\<cdot>r\<cdot>x = return\<cdot>r' \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = p2\<cdot>r'\<cdot>y"
   1.196 +by (simp_all add: cpair_pat_def)
   1.197 +
   1.198 +lemma spair_pat_simps [simp]:
   1.199 +  "spair_pat p1 p2\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.200 +  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> spair_pat p1 p2\<cdot>r\<cdot>(:x, y:) = cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x, y\<rangle>"
   1.201 +by (simp_all add: spair_pat_def)
   1.202 +
   1.203 +lemma sinl_pat_simps [simp]:
   1.204 +  "sinl_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.205 +  "x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = p\<cdot>r\<cdot>x"
   1.206 +  "x \<noteq> \<bottom> \<Longrightarrow> sinl_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = fail"
   1.207 +by (simp_all add: sinl_pat_def)
   1.208 +
   1.209 +lemma sinr_pat_simps [simp]:
   1.210 +  "sinr_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.211 +  "x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinl\<cdot>x) = fail"
   1.212 +  "x \<noteq> \<bottom> \<Longrightarrow> sinr_pat p\<cdot>r\<cdot>(sinr\<cdot>x) = p\<cdot>r\<cdot>x"
   1.213 +by (simp_all add: sinr_pat_def)
   1.214 +
   1.215 +lemma up_pat_simps [simp]:
   1.216 +  "up_pat p\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.217 +  "up_pat p\<cdot>r\<cdot>(up\<cdot>x) = p\<cdot>r\<cdot>x"
   1.218 +by (simp_all add: up_pat_def)
   1.219 +
   1.220 +lemma Def_pat_simps [simp]:
   1.221 +  "Def_pat x\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.222 +  "Def_pat x\<cdot>r\<cdot>(Def x) = return\<cdot>r"
   1.223 +  "x \<noteq> y \<Longrightarrow> Def_pat x\<cdot>r\<cdot>(Def y) = fail"
   1.224 +by (simp_all add: Def_pat_def)
   1.225 +
   1.226 +lemma ONE_pat_simps [simp]:
   1.227 +  "ONE_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.228 +  "ONE_pat\<cdot>r\<cdot>ONE = return\<cdot>r"
   1.229 +by (simp_all add: ONE_pat_def)
   1.230 +
   1.231 +lemma TT_pat_simps [simp]:
   1.232 +  "TT_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.233 +  "TT_pat\<cdot>r\<cdot>TT = return\<cdot>r"
   1.234 +  "TT_pat\<cdot>r\<cdot>FF = fail"
   1.235 +by (simp_all add: TT_pat_def)
   1.236 +
   1.237 +lemma FF_pat_simps [simp]:
   1.238 +  "FF_pat\<cdot>r\<cdot>\<bottom> = \<bottom>"
   1.239 +  "FF_pat\<cdot>r\<cdot>TT = fail"
   1.240 +  "FF_pat\<cdot>r\<cdot>FF = return\<cdot>r"
   1.241 +by (simp_all add: FF_pat_def)
   1.242 +
   1.243  subsection {* Match functions for built-in types *}
   1.244  
   1.245  defaultsort pcpo