change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
authorhuffman
Thu Nov 03 01:11:39 2005 +0100 (2005-11-03)
changeset 1807820e5a6440790
parent 18077 f1f4f951ec8d
child 18079 9d4d70b175fd
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
src/HOLCF/Cfun.thy
src/HOLCF/Cprod.thy
src/HOLCF/Fix.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Thu Nov 03 01:02:29 2005 +0100
     1.2 +++ b/src/HOLCF/Cfun.thy	Thu Nov 03 01:11:39 2005 +0100
     1.3 @@ -39,49 +39,51 @@
     1.4  
     1.5  subsection {* Syntax for continuous lambda abstraction *}
     1.6  
     1.7 -syntax
     1.8 -  "_cabs" :: "[pttrn, 'a] \<Rightarrow> logic"
     1.9 -translations
    1.10 -  "_cabs x t" == "Abs_CFun (%x. t)"
    1.11 +syntax "_cabs" :: "'a"
    1.12 +
    1.13 +parse_translation {*
    1.14 +(* rewrites (_cabs x t) --> (Abs_CFun (%x. t)) *)
    1.15 +  [mk_binder_tr ("_cabs", "Abs_CFun")];
    1.16 +*}
    1.17  
    1.18  text {* To avoid eta-contraction of body: *}
    1.19  print_translation {*
    1.20 -let
    1.21 -  fun cabs_tr' [Abs abs] =
    1.22 -    let val (x,t) = atomic_abs_tr' abs
    1.23 -    in Syntax.const "_cabs" $ x $ t end
    1.24 -in [("Abs_CFun", cabs_tr')] end
    1.25 +  let
    1.26 +    fun cabs_tr' [Abs abs] =
    1.27 +      let val (x,t) = atomic_abs_tr' abs
    1.28 +      in Syntax.const "_cabs" $ x $ t end
    1.29 +  in [("Abs_CFun", cabs_tr')] end;
    1.30  *}
    1.31  
    1.32  text {* syntax for nested abstractions *}
    1.33  
    1.34  syntax
    1.35 -  "_Lambda" :: "[pttrns, 'a] \<Rightarrow> logic"  ("(3LAM _./ _)" [0, 10] 10)
    1.36 +  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic"  ("(3LAM _./ _)" [1000, 10] 10)
    1.37  
    1.38  syntax (xsymbols)
    1.39 -  "_Lambda" :: "[pttrns, 'a] \<Rightarrow> logic" ("(3\<Lambda>_./ _)" [0, 10] 10)
    1.40 +  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda>_./ _)" [1000, 10] 10)
    1.41  
    1.42  parse_ast_translation {*
    1.43  (* rewrites (LAM x y z. t) --> (_cabs x (_cabs y (_cabs z t))) *)
    1.44 -(* c.f. Syntax.lambda_ast_tr from Syntax/syn_trans.ML *)
    1.45 -let
    1.46 -  fun Lambda_ast_tr [pats, body] =
    1.47 -        Syntax.fold_ast_p "_cabs" (Syntax.unfold_ast "_pttrns" pats, body)
    1.48 -    | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
    1.49 -in [("_Lambda", Lambda_ast_tr)] end
    1.50 +(* cf. Syntax.lambda_ast_tr from Syntax/syn_trans.ML *)
    1.51 +  let
    1.52 +    fun Lambda_ast_tr [pats, body] =
    1.53 +          Syntax.fold_ast_p "_cabs" (Syntax.unfold_ast "_cargs" pats, body)
    1.54 +      | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
    1.55 +  in [("_Lambda", Lambda_ast_tr)] end;
    1.56  *}
    1.57  
    1.58  print_ast_translation {*
    1.59  (* rewrites (_cabs x (_cabs y (_cabs z t))) --> (LAM x y z. t) *)
    1.60 -(* c.f. Syntax.abs_ast_tr' from Syntax/syn_trans.ML *)
    1.61 -let
    1.62 -  fun cabs_ast_tr' asts =
    1.63 -    (case Syntax.unfold_ast_p "_cabs"
    1.64 -        (Syntax.Appl (Syntax.Constant "_cabs" :: asts)) of
    1.65 -      ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
    1.66 -    | (xs, body) => Syntax.Appl
    1.67 -        [Syntax.Constant "_Lambda", Syntax.fold_ast "_pttrns" xs, body]);
    1.68 -in [("_cabs", cabs_ast_tr')] end
    1.69 +(* cf. Syntax.abs_ast_tr' from Syntax/syn_trans.ML *)
    1.70 +  let
    1.71 +    fun cabs_ast_tr' asts =
    1.72 +      (case Syntax.unfold_ast_p "_cabs"
    1.73 +          (Syntax.Appl (Syntax.Constant "_cabs" :: asts)) of
    1.74 +        ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
    1.75 +      | (xs, body) => Syntax.Appl
    1.76 +          [Syntax.Constant "_Lambda", Syntax.fold_ast "_cargs" xs, body]);
    1.77 +  in [("_cabs", cabs_ast_tr')] end;
    1.78  *}
    1.79  
    1.80  subsection {* Continuous function space is pointed *}
     2.1 --- a/src/HOLCF/Cprod.thy	Thu Nov 03 01:02:29 2005 +0100
     2.2 +++ b/src/HOLCF/Cprod.thy	Thu Nov 03 01:11:39 2005 +0100
     2.3 @@ -202,20 +202,11 @@
     2.4    "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
     2.5  
     2.6  translations
     2.7 -  "<x, y, z>" == "<x, <y, z>>"
     2.8 -  "<x, y>"    == "cpair$x$y"
     2.9 -
    2.10 -text {* syntax for @{text "LAM <x,y,z>.e"} *}
    2.11 -
    2.12 -syntax
    2.13 -  "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("<_,/ _>")
    2.14 -
    2.15 -syntax (xsymbols)
    2.16 -  "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("\<langle>_,/ _\<rangle>")
    2.17 +  "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
    2.18 +  "\<langle>x, y\<rangle>"    == "cpair\<cdot>x\<cdot>y"
    2.19  
    2.20  translations
    2.21 -  "LAM <x,y,zs>. t"       == "csplit$(LAM x <y,zs>. t)"
    2.22 -  "LAM <x,y>. t"          == "csplit$(LAM x y. t)"
    2.23 +  "\<Lambda>(cpair\<cdot>x\<cdot>y). t" == "csplit\<cdot>(\<Lambda> x y. t)"
    2.24  
    2.25  
    2.26  subsection {* Convert all lemmas to the continuous versions *}
     3.1 --- a/src/HOLCF/Fix.thy	Thu Nov 03 01:02:29 2005 +0100
     3.2 +++ b/src/HOLCF/Fix.thy	Thu Nov 03 01:11:39 2005 +0100
     3.3 @@ -33,13 +33,13 @@
     3.4  subsection {* Binder syntax for @{term fix} *}
     3.5  
     3.6  syntax
     3.7 -  "_FIX" :: "[pttrn, 'a] => 'a" ("(3FIX _./ _)" [0, 10] 10)
     3.8 +  "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3FIX _./ _)" [1000, 10] 10)
     3.9  
    3.10  syntax (xsymbols)
    3.11 -  "_FIX" :: "[pttrn, 'a] => 'a" ("(3\<mu>_./ _)" [0, 10] 10)
    3.12 +  "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu>_./ _)" [1000, 10] 10)
    3.13  
    3.14  translations
    3.15 -  "FIX x. t" == "fix$(LAM x. t)"
    3.16 +  "\<mu> x. t" == "fix\<cdot>(\<Lambda> x. t)"
    3.17  
    3.18  subsection {* Properties of @{term iterate} *}
    3.19  
     4.1 --- a/src/HOLCF/Sprod.thy	Thu Nov 03 01:02:29 2005 +0100
     4.2 +++ b/src/HOLCF/Sprod.thy	Thu Nov 03 01:11:39 2005 +0100
     4.3 @@ -44,11 +44,14 @@
     4.4    ssplit_def: "ssplit \<equiv> \<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p))"
     4.5  
     4.6  syntax  
     4.7 -  "@stuple"	:: "['a, args] => 'a ** 'b"	("(1'(:_,/ _:'))")
     4.8 +  "@stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
     4.9  
    4.10  translations
    4.11 -        "(:x, y, z:)"   == "(:x, (:y, z:):)"
    4.12 -        "(:x, y:)"      == "spair$x$y"
    4.13 +  "(:x, y, z:)" == "(:x, (:y, z:):)"
    4.14 +  "(:x, y:)"    == "spair\<cdot>x\<cdot>y"
    4.15 +
    4.16 +translations
    4.17 +  "\<Lambda>(spair\<cdot>x\<cdot>y). t" == "ssplit\<cdot>(\<Lambda> x y. t)"
    4.18  
    4.19  subsection {* Case analysis *}
    4.20  
    4.21 @@ -91,7 +94,7 @@
    4.22  
    4.23  lemma spair_defined [simp]: 
    4.24    "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>"
    4.25 -by (simp add: spair_Abs_Sprod Abs_Sprod_defined cpair_defined_iff Sprod_def)
    4.26 +by (simp add: spair_Abs_Sprod Abs_Sprod_defined Sprod_def)
    4.27  
    4.28  lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>"
    4.29  by (erule contrapos_pp, simp)
     5.1 --- a/src/HOLCF/Ssum.thy	Thu Nov 03 01:02:29 2005 +0100
     5.2 +++ b/src/HOLCF/Ssum.thy	Thu Nov 03 01:11:39 2005 +0100
     5.3 @@ -112,16 +112,16 @@
     5.4  subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
     5.5  
     5.6  lemma sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
     5.7 -by (simp add: less_Ssum_def Rep_Ssum_sinl cpair_less)
     5.8 +by (simp add: less_Ssum_def Rep_Ssum_sinl)
     5.9  
    5.10  lemma sinr_less [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
    5.11 -by (simp add: less_Ssum_def Rep_Ssum_sinr cpair_less)
    5.12 +by (simp add: less_Ssum_def Rep_Ssum_sinr)
    5.13  
    5.14  lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
    5.15 -by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
    5.16 +by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr eq_UU_iff)
    5.17  
    5.18  lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
    5.19 -by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
    5.20 +by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr eq_UU_iff)
    5.21  
    5.22  lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
    5.23  by (simp add: po_eq_conv)
    5.24 @@ -218,7 +218,11 @@
    5.25    "sscase \<equiv> \<Lambda> f g s. Iwhen f g s"
    5.26  
    5.27  translations
    5.28 -"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"
    5.29 +  "case s of sinl\<cdot>x \<Rightarrow> t1 | sinr\<cdot>y \<Rightarrow> t2" == "sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
    5.30 +
    5.31 +translations
    5.32 +  "\<Lambda>(sinl\<cdot>x). t" == "sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
    5.33 +  "\<Lambda>(sinr\<cdot>y). t" == "sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
    5.34  
    5.35  text {* continuous versions of lemmas for @{term sscase} *}
    5.36  
     6.1 --- a/src/HOLCF/Up.thy	Thu Nov 03 01:02:29 2005 +0100
     6.2 +++ b/src/HOLCF/Up.thy	Thu Nov 03 01:11:39 2005 +0100
     6.3 @@ -189,7 +189,7 @@
     6.4  apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
     6.5  apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
     6.6  apply (simp add: cont_cfun_arg)
     6.7 -apply (simp add: thelub_const lub_const)
     6.8 +apply (simp add: lub_const)
     6.9  done
    6.10  
    6.11  subsection {* Continuous versions of constants *}
    6.12 @@ -202,7 +202,8 @@
    6.13    "fup \<equiv> \<Lambda> f p. Ifup f p"
    6.14  
    6.15  translations
    6.16 -  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(LAM x. t)\<cdot>l"
    6.17 +  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(\<Lambda> x. t)\<cdot>l"
    6.18 +  "\<Lambda>(up\<cdot>x). t" == "fup\<cdot>(\<Lambda> x. t)"
    6.19  
    6.20  text {* continuous versions of lemmas for @{typ "('a)u"} *}
    6.21  
    6.22 @@ -248,7 +249,7 @@
    6.23  apply (erule (1) admD)
    6.24  apply (rule allI, drule_tac x="i + j" in spec)
    6.25  apply simp
    6.26 -apply (simp add: thelub_const)
    6.27 +apply simp
    6.28  done
    6.29  
    6.30  text {* properties of fup *}