--- a/src/HOLCF/Cfun.thy Mon Oct 10 04:38:26 2005 +0200
+++ b/src/HOLCF/Cfun.thy Mon Oct 10 05:30:02 2005 +0200
@@ -25,20 +25,56 @@
cpodef (CFun) ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}"
by (simp add: Ex_cont adm_cont)
+syntax (xsymbols)
+ "->" :: "[type, type] => type" ("(_ \<rightarrow>/ _)" [1,0]0)
+
syntax
- Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("_$_" [999,1000] 999)
- (* application *)
- Abs_CFun :: "('a => 'b) => ('a -> 'b)" (binder "LAM " 10)
- (* abstraction *)
+ Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("_$_" [999,1000] 999)
+ "_Lambda" :: "[pttrns, 'a] \<Rightarrow> logic" ("(3LAM _./ _)" [0, 10] 10)
syntax (xsymbols)
- "->" :: "[type, type] => type" ("(_ \<rightarrow>/ _)" [1,0]0)
- "LAM " :: "[idts, 'a => 'b] => ('a -> 'b)"
- ("(3\<Lambda>_./ _)" [0, 10] 10)
- Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("(_\<cdot>_)" [999,1000] 999)
+ "_Lambda" :: "[pttrns, 'a] \<Rightarrow> logic" ("(3\<Lambda>_./ _)" [0, 10] 10)
+ Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>_)" [999,1000] 999)
syntax (HTML output)
- Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("(_\<cdot>_)" [999,1000] 999)
+ Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>_)" [999,1000] 999)
+
+syntax
+ "_cabs" :: "[pttrn, 'a] \<Rightarrow> logic"
+translations
+ "_cabs x t" == "Abs_CFun (%x. t)"
+
+(* 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
+*}
+
+parse_ast_translation {*
+(* rewrites (LAM x y z. t) --> (LAM x. LAM y. LAM 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
+*}
+
+print_ast_translation {*
+(* rewrites (LAM x. LAM y. LAM 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 ("abs_ast_tr'", asts)
+ | (xs, body) => Syntax.Appl
+ [Syntax.Constant "_Lambda", Syntax.fold_ast "_pttrns" xs, body]);
+in [("_cabs", cabs_ast_tr')] end
+*}
subsection {* Class instances *}
@@ -448,4 +484,17 @@
lemma strictify2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strictify\<cdot>f\<cdot>x = f\<cdot>x"
by (simp add: strictify_conv_if)
+subsection {* Continuous let-bindings *}
+
+constdefs
+ CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b"
+ "CLet \<equiv> \<Lambda> s f. f\<cdot>s"
+
+syntax
+ "_CLet" :: "[letbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
+
+translations
+ "_CLet (_binds b bs) e" == "_CLet b (_CLet bs e)"
+ "Let x = a in e" == "CLet$a$(LAM x. e)"
+
end
--- a/src/HOLCF/Cprod.thy Mon Oct 10 04:38:26 2005 +0200
+++ b/src/HOLCF/Cprod.thy Mon Oct 10 05:30:02 2005 +0200
@@ -195,49 +195,19 @@
"<x, y, z>" == "<x, <y, z>>"
"<x, y>" == "cpair$x$y"
+syntax
+ "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn" ("<_,/ _>")
+
+translations
+ "LAM <x,y,zs>. t" == "csplit$(LAM x <y,zs>. t)"
+ "LAM <x,y>. t" == "csplit$(LAM x y. t)"
+
defs
cpair_def: "cpair \<equiv> (\<Lambda> x y. (x, y))"
cfst_def: "cfst \<equiv> (\<Lambda> p. fst p)"
csnd_def: "csnd \<equiv> (\<Lambda> p. snd p)"
csplit_def: "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
-subsection {* Syntax *}
-
-text {* syntax for @{text "LAM <x,y,z>.e"} *}
-
-syntax
- "_LAM" :: "[patterns, 'a \<Rightarrow> 'b] \<Rightarrow> ('a \<rightarrow> 'b)" ("(3LAM <_>./ _)" [0, 10] 10)
-
-translations
- "LAM <x,y,zs>. b" == "csplit$(LAM x. LAM <y,zs>. b)"
- "LAM <x,y>. LAM zs. b" <= "csplit$(LAM x y zs. b)"
- "LAM <x,y>.b" == "csplit$(LAM x y. b)"
-
-syntax (xsymbols)
- "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
-
-text {* syntax for Let *}
-
-constdefs
- CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b"
- "CLet \<equiv> \<Lambda> s f. f\<cdot>s"
-
-nonterminals
- Cletbinds Cletbind
-
-syntax
- "_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10)
- "_Cbindp" :: "[patterns, 'a] => Cletbind" ("(2<_> =/ _)" 10)
- "" :: "Cletbind => Cletbinds" ("_")
- "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _")
- "_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
-
-translations
- "_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)"
- "Let x = a in LAM ys. e" == "CLet$a$(LAM x ys. e)"
- "Let x = a in e" == "CLet$a$(LAM x. e)"
- "Let <xs> = a in e" == "CLet$a$(LAM <xs>. e)"
-
subsection {* Convert all lemmas to the continuous versions *}
lemma cpair_eq_pair: "<x, y> = (x, y)"
--- a/src/HOLCF/Fix.thy Mon Oct 10 04:38:26 2005 +0200
+++ b/src/HOLCF/Fix.thy Mon Oct 10 05:30:02 2005 +0200
@@ -35,17 +35,13 @@
subsection {* Binder syntax for @{term fix} *}
syntax
- "@FIX" :: "('a => 'a) => 'a" (binder "FIX " 10)
- "@FIXP" :: "[patterns, 'a] => 'a" ("(3FIX <_>./ _)" [0, 10] 10)
+ "_FIX" :: "[pttrn, 'a] => 'a" ("(3FIX _./ _)" [0, 10] 10)
syntax (xsymbols)
- "FIX " :: "[idt, 'a] => 'a" ("(3\<mu>_./ _)" [0, 10] 10)
- "@FIXP" :: "[patterns, 'a] => 'a" ("(3\<mu>()<_>./ _)" [0, 10] 10)
+ "_FIX" :: "[pttrn, 'a] => 'a" ("(3\<mu>_./ _)" [0, 10] 10)
translations
- "FIX x. LAM y. t" == "fix\<cdot>(LAM x y. t)"
- "FIX x. t" == "fix\<cdot>(LAM x. t)"
- "FIX <xs>. t" == "fix\<cdot>(LAM <xs>. t)"
+ "FIX x. t" == "fix$(LAM x. t)"
subsection {* Properties of @{term iterate} and @{term fix} *}
--- a/src/HOLCF/domain/syntax.ML Mon Oct 10 04:38:26 2005 +0200
+++ b/src/HOLCF/domain/syntax.ML Mon Oct 10 05:30:02 2005 +0200
@@ -75,9 +75,8 @@
fun case1 n (con,mx,args) = mk_appl (Constant "_case1")
[Library.foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)),
expvar n];
- fun arg1 n (con,_,args) = if args = [] then expvar n
- else mk_appl (Constant "LAM ")
- [foldr1 (app "_idts") (mapn (argvar n) 1 args) , expvar n];
+ fun cabs (x,t) = mk_appl (Constant "_cabs") [x,t];
+ fun arg1 n (con,_,args) = foldr cabs (expvar n) (mapn (argvar n) 1 args);
in
ParsePrintRule
(mk_appl (Constant "_case_syntax") [Variable "x", foldr1