# HG changeset patch # User huffman # Date 1130976699 -3600 # Node ID 20e5a644079044d680d8e09f5e37153b44c7c99c # Parent f1f4f951ec8d3656557bfb6e45300ee881b3a77d change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up diff -r f1f4f951ec8d -r 20e5a6440790 src/HOLCF/Cfun.thy --- 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] \ 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] \ logic" ("(3LAM _./ _)" [0, 10] 10) + "_Lambda" :: "[cargs, 'a] \ logic" ("(3LAM _./ _)" [1000, 10] 10) syntax (xsymbols) - "_Lambda" :: "[pttrns, 'a] \ logic" ("(3\_./ _)" [0, 10] 10) + "_Lambda" :: "[cargs, 'a] \ logic" ("(3\_./ _)" [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 *} diff -r f1f4f951ec8d -r 20e5a6440790 src/HOLCF/Cprod.thy --- 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] \ 'a * 'b" ("(1\_,/ _\)") translations - "" == ">" - "" == "cpair$x$y" - -text {* syntax for @{text "LAM .e"} *} - -syntax - "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn" ("<_,/ _>") - -syntax (xsymbols) - "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn" ("\_,/ _\") + "\x, y, z\" == "\x, \y, z\\" + "\x, y\" == "cpair\x\y" translations - "LAM . t" == "csplit$(LAM x . t)" - "LAM . t" == "csplit$(LAM x y. t)" + "\(cpair\x\y). t" == "csplit\(\ x y. t)" subsection {* Convert all lemmas to the continuous versions *} diff -r f1f4f951ec8d -r 20e5a6440790 src/HOLCF/Fix.thy --- 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] \ 'a" ("(3FIX _./ _)" [1000, 10] 10) syntax (xsymbols) - "_FIX" :: "[pttrn, 'a] => 'a" ("(3\_./ _)" [0, 10] 10) + "_FIX" :: "['a, 'a] \ 'a" ("(3\_./ _)" [1000, 10] 10) translations - "FIX x. t" == "fix$(LAM x. t)" + "\ x. t" == "fix\(\ x. t)" subsection {* Properties of @{term iterate} *} diff -r f1f4f951ec8d -r 20e5a6440790 src/HOLCF/Sprod.thy --- 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 \ \ f. strictify\(\ p. f\(sfst\p)\(ssnd\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\x\y" + +translations + "\(spair\x\y). t" == "ssplit\(\ x y. t)" subsection {* Case analysis *} @@ -91,7 +94,7 @@ lemma spair_defined [simp]: "\x \ \; y \ \\ \ (:x, y:) \ \" -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:) = \ \ x = \ \ y = \" by (erule contrapos_pp, simp) diff -r f1f4f951ec8d -r 20e5a6440790 src/HOLCF/Ssum.thy --- 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\x \ sinl\y) = (x \ 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\x \ sinr\y) = (x \ 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\x \ sinr\y) = (x = \)" -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\x \ sinl\y) = (x = \)" -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\x = sinr\y) = (x = \ \ y = \)" by (simp add: po_eq_conv) @@ -218,7 +218,11 @@ "sscase \ \ 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\x \ t1 | sinr\y \ t2" == "sscase\(\ x. t1)\(\ y. t2)\s" + +translations + "\(sinl\x). t" == "sscase\(\ x. t)\\" + "\(sinr\y). t" == "sscase\\\(\ y. t)" text {* continuous versions of lemmas for @{term sscase} *} diff -r f1f4f951ec8d -r 20e5a6440790 src/HOLCF/Up.thy --- 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 \ \ f p. Ifup f p" translations - "case l of up\x \ t" == "fup\(LAM x. t)\l" + "case l of up\x \ t" == "fup\(\ x. t)\l" + "\(up\x). t" == "fup\(\ 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 *}