change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up

--- a/src/HOLCF/Cfun.thy	Thu Nov 03 01:02:29 2005 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Nov 03 01:11:39 2005 +0100
@@ -39,49 +39,51 @@
 
 subsection {* Syntax for continuous lambda abstraction *}
 
-syntax
-  "_cabs" :: "[pttrn, 'a] \<Rightarrow> logic"
-translations
-  "_cabs x t" == "Abs_CFun (%x. t)"
+syntax "_cabs" :: "'a"
+
+parse_translation {*
+(* rewrites (_cabs x t) --> (Abs_CFun (%x. t)) *)
+  [mk_binder_tr ("_cabs", "Abs_CFun")];
+*}
 
 text {* To avoid eta-contraction of body: *}
 print_translation {*
-let
-  fun cabs_tr' [Abs abs] =
-    let val (x,t) = atomic_abs_tr' abs
-    in Syntax.const "_cabs" $ x $ t end
-in [("Abs_CFun", cabs_tr')] end
+  let
+    fun cabs_tr' [Abs abs] =
+      let val (x,t) = atomic_abs_tr' abs
+      in Syntax.const "_cabs" $ x $ t end
+  in [("Abs_CFun", cabs_tr')] end;
 *}
 
 text {* syntax for nested abstractions *}
 
 syntax
-  "_Lambda" :: "[pttrns, 'a] \<Rightarrow> logic"  ("(3LAM _./ _)" [0, 10] 10)
+  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic"  ("(3LAM _./ _)" [1000, 10] 10)
 
 syntax (xsymbols)
-  "_Lambda" :: "[pttrns, 'a] \<Rightarrow> logic" ("(3\<Lambda>_./ _)" [0, 10] 10)
+  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda>_./ _)" [1000, 10] 10)
 
 parse_ast_translation {*
 (* rewrites (LAM x y z. t) --> (_cabs x (_cabs y (_cabs z t))) *)
-(* c.f. Syntax.lambda_ast_tr from Syntax/syn_trans.ML *)
-let
-  fun Lambda_ast_tr [pats, body] =
-        Syntax.fold_ast_p "_cabs" (Syntax.unfold_ast "_pttrns" pats, body)
-    | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
-in [("_Lambda", Lambda_ast_tr)] end
+(* cf. Syntax.lambda_ast_tr from Syntax/syn_trans.ML *)
+  let
+    fun Lambda_ast_tr [pats, body] =
+          Syntax.fold_ast_p "_cabs" (Syntax.unfold_ast "_cargs" pats, body)
+      | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
+  in [("_Lambda", Lambda_ast_tr)] end;
 *}
 
 print_ast_translation {*
 (* rewrites (_cabs x (_cabs y (_cabs z t))) --> (LAM x y z. t) *)
-(* c.f. Syntax.abs_ast_tr' from Syntax/syn_trans.ML *)
-let
-  fun cabs_ast_tr' asts =
-    (case Syntax.unfold_ast_p "_cabs"
-        (Syntax.Appl (Syntax.Constant "_cabs" :: asts)) of
-      ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
-    | (xs, body) => Syntax.Appl
-        [Syntax.Constant "_Lambda", Syntax.fold_ast "_pttrns" xs, body]);
-in [("_cabs", cabs_ast_tr')] end
+(* cf. Syntax.abs_ast_tr' from Syntax/syn_trans.ML *)
+  let
+    fun cabs_ast_tr' asts =
+      (case Syntax.unfold_ast_p "_cabs"
+          (Syntax.Appl (Syntax.Constant "_cabs" :: asts)) of
+        ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
+      | (xs, body) => Syntax.Appl
+          [Syntax.Constant "_Lambda", Syntax.fold_ast "_cargs" xs, body]);
+  in [("_cabs", cabs_ast_tr')] end;
 *}
 
 subsection {* Continuous function space is pointed *}

--- a/src/HOLCF/Cprod.thy	Thu Nov 03 01:02:29 2005 +0100
+++ b/src/HOLCF/Cprod.thy	Thu Nov 03 01:11:39 2005 +0100
@@ -202,20 +202,11 @@
   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
 
 translations
-  "<x, y, z>" == "<x, <y, z>>"
-  "<x, y>"    == "cpair$x$y"
-
-text {* syntax for @{text "LAM <x,y,z>.e"} *}
-
-syntax
-  "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("<_,/ _>")
-
-syntax (xsymbols)
-  "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("\<langle>_,/ _\<rangle>")
+  "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
+  "\<langle>x, y\<rangle>"    == "cpair\<cdot>x\<cdot>y"
 
 translations
-  "LAM <x,y,zs>. t"       == "csplit$(LAM x <y,zs>. t)"
-  "LAM <x,y>. t"          == "csplit$(LAM x y. t)"
+  "\<Lambda>(cpair\<cdot>x\<cdot>y). t" == "csplit\<cdot>(\<Lambda> x y. t)"
 
 
 subsection {* Convert all lemmas to the continuous versions *}

--- a/src/HOLCF/Fix.thy	Thu Nov 03 01:02:29 2005 +0100
+++ b/src/HOLCF/Fix.thy	Thu Nov 03 01:11:39 2005 +0100
@@ -33,13 +33,13 @@
 subsection {* Binder syntax for @{term fix} *}
 
 syntax
-  "_FIX" :: "[pttrn, 'a] => 'a" ("(3FIX _./ _)" [0, 10] 10)
+  "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3FIX _./ _)" [1000, 10] 10)
 
 syntax (xsymbols)
-  "_FIX" :: "[pttrn, 'a] => 'a" ("(3\<mu>_./ _)" [0, 10] 10)
+  "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu>_./ _)" [1000, 10] 10)
 
 translations
-  "FIX x. t" == "fix$(LAM x. t)"
+  "\<mu> x. t" == "fix\<cdot>(\<Lambda> x. t)"
 
 subsection {* Properties of @{term iterate} *}
 

--- a/src/HOLCF/Sprod.thy	Thu Nov 03 01:02:29 2005 +0100
+++ b/src/HOLCF/Sprod.thy	Thu Nov 03 01:11:39 2005 +0100
@@ -44,11 +44,14 @@
   ssplit_def: "ssplit \<equiv> \<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p))"
 
 syntax  
-  "@stuple"	:: "['a, args] => 'a ** 'b"	("(1'(:_,/ _:'))")
+  "@stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
 
 translations
-        "(:x, y, z:)"   == "(:x, (:y, z:):)"
-        "(:x, y:)"      == "spair$x$y"
+  "(:x, y, z:)" == "(:x, (:y, z:):)"
+  "(:x, y:)"    == "spair\<cdot>x\<cdot>y"
+
+translations
+  "\<Lambda>(spair\<cdot>x\<cdot>y). t" == "ssplit\<cdot>(\<Lambda> x y. t)"
 
 subsection {* Case analysis *}
 
@@ -91,7 +94,7 @@
 
 lemma spair_defined [simp]: 
   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>"
-by (simp add: spair_Abs_Sprod Abs_Sprod_defined cpair_defined_iff Sprod_def)
+by (simp add: spair_Abs_Sprod Abs_Sprod_defined Sprod_def)
 
 lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>"
 by (erule contrapos_pp, simp)

--- a/src/HOLCF/Ssum.thy	Thu Nov 03 01:02:29 2005 +0100
+++ b/src/HOLCF/Ssum.thy	Thu Nov 03 01:11:39 2005 +0100
@@ -112,16 +112,16 @@
 subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
 
 lemma sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl cpair_less)
+by (simp add: less_Ssum_def Rep_Ssum_sinl)
 
 lemma sinr_less [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: less_Ssum_def Rep_Ssum_sinr cpair_less)
+by (simp add: less_Ssum_def Rep_Ssum_sinr)
 
 lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
+by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr eq_UU_iff)
 
 lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
+by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr eq_UU_iff)
 
 lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
 by (simp add: po_eq_conv)
@@ -218,7 +218,11 @@
   "sscase \<equiv> \<Lambda> f g s. Iwhen f g s"
 
 translations
-"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"
+  "case s of sinl\<cdot>x \<Rightarrow> t1 | sinr\<cdot>y \<Rightarrow> t2" == "sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
+
+translations
+  "\<Lambda>(sinl\<cdot>x). t" == "sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
+  "\<Lambda>(sinr\<cdot>y). t" == "sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
 
 text {* continuous versions of lemmas for @{term sscase} *}
 

--- a/src/HOLCF/Up.thy	Thu Nov 03 01:02:29 2005 +0100
+++ b/src/HOLCF/Up.thy	Thu Nov 03 01:11:39 2005 +0100
@@ -189,7 +189,7 @@
 apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
 apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
 apply (simp add: cont_cfun_arg)
-apply (simp add: thelub_const lub_const)
+apply (simp add: lub_const)
 done
 
 subsection {* Continuous versions of constants *}
@@ -202,7 +202,8 @@
   "fup \<equiv> \<Lambda> f p. Ifup f p"
 
 translations
-  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(LAM x. t)\<cdot>l"
+  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(\<Lambda> x. t)\<cdot>l"
+  "\<Lambda>(up\<cdot>x). t" == "fup\<cdot>(\<Lambda> x. t)"
 
 text {* continuous versions of lemmas for @{typ "('a)u"} *}
 
@@ -248,7 +249,7 @@
 apply (erule (1) admD)
 apply (rule allI, drule_tac x="i + j" in spec)
 apply simp
-apply (simp add: thelub_const)
+apply simp
 done
 
 text {* properties of fup *}