40 subsection {* Syntax for continuous lambda abstraction *} |
40 subsection {* Syntax for continuous lambda abstraction *} |
41 |
41 |
42 syntax "_cabs" :: "'a" |
42 syntax "_cabs" :: "'a" |
43 |
43 |
44 parse_translation {* |
44 parse_translation {* |
45 (* rewrites (_cabs x t) --> (Abs_CFun (%x. t)) *) |
45 (* rewrites (_cabs x t) => (Abs_CFun (%x. t)) *) |
46 [mk_binder_tr ("_cabs", "Abs_CFun")]; |
46 [mk_binder_tr ("_cabs", "Abs_CFun")]; |
47 *} |
47 *} |
48 |
48 |
49 text {* To avoid eta-contraction of body: *} |
49 text {* To avoid eta-contraction of body: *} |
50 print_translation {* |
50 typed_print_translation {* |
51 let |
51 let |
52 fun cabs_tr' [Abs abs] = |
52 fun cabs_tr' _ _ [Abs abs] = let |
53 let val (x,t) = atomic_abs_tr' abs |
53 val (x,t) = atomic_abs_tr' abs |
54 in Syntax.const "_cabs" $ x $ t end |
54 in Syntax.const "_cabs" $ x $ t end |
|
55 |
|
56 | cabs_tr' _ T [t] = let |
|
57 val xT = domain_type (domain_type T); |
|
58 val abs' = ("x",xT,(incr_boundvars 1 t)$Bound 0); |
|
59 val (x,t') = atomic_abs_tr' abs'; |
|
60 in Syntax.const "_cabs" $ x $ t' end; |
|
61 |
55 in [("Abs_CFun", cabs_tr')] end; |
62 in [("Abs_CFun", cabs_tr')] end; |
56 *} |
63 *} |
57 |
64 |
58 text {* syntax for nested abstractions *} |
65 text {* Syntax for nested abstractions *} |
59 |
66 |
60 syntax |
67 syntax |
61 "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3LAM _./ _)" [1000, 10] 10) |
68 "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3LAM _./ _)" [1000, 10] 10) |
62 |
69 |
63 syntax (xsymbols) |
70 syntax (xsymbols) |
64 "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda>_./ _)" [1000, 10] 10) |
71 "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda>_./ _)" [1000, 10] 10) |
65 |
72 |
66 parse_ast_translation {* |
73 parse_ast_translation {* |
67 (* rewrites (LAM x y z. t) --> (_cabs x (_cabs y (_cabs z t))) *) |
74 (* rewrites (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *) |
68 (* cf. Syntax.lambda_ast_tr from Syntax/syn_trans.ML *) |
75 (* cf. Syntax.lambda_ast_tr from Syntax/syn_trans.ML *) |
69 let |
76 let |
70 fun Lambda_ast_tr [pats, body] = |
77 fun Lambda_ast_tr [pats, body] = |
71 Syntax.fold_ast_p "_cabs" (Syntax.unfold_ast "_cargs" pats, body) |
78 Syntax.fold_ast_p "_cabs" (Syntax.unfold_ast "_cargs" pats, body) |
72 | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts); |
79 | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts); |
73 in [("_Lambda", Lambda_ast_tr)] end; |
80 in [("_Lambda", Lambda_ast_tr)] end; |
74 *} |
81 *} |
75 |
82 |
76 print_ast_translation {* |
83 print_ast_translation {* |
77 (* rewrites (_cabs x (_cabs y (_cabs z t))) --> (LAM x y z. t) *) |
84 (* rewrites (_cabs x (_cabs y (_cabs z t))) => (LAM x y z. t) *) |
78 (* cf. Syntax.abs_ast_tr' from Syntax/syn_trans.ML *) |
85 (* cf. Syntax.abs_ast_tr' from Syntax/syn_trans.ML *) |
79 let |
86 let |
80 fun cabs_ast_tr' asts = |
87 fun cabs_ast_tr' asts = |
81 (case Syntax.unfold_ast_p "_cabs" |
88 (case Syntax.unfold_ast_p "_cabs" |
82 (Syntax.Appl (Syntax.Constant "_cabs" :: asts)) of |
89 (Syntax.Appl (Syntax.Constant "_cabs" :: asts)) of |
84 | (xs, body) => Syntax.Appl |
91 | (xs, body) => Syntax.Appl |
85 [Syntax.Constant "_Lambda", Syntax.fold_ast "_cargs" xs, body]); |
92 [Syntax.Constant "_Lambda", Syntax.fold_ast "_cargs" xs, body]); |
86 in [("_cabs", cabs_ast_tr')] end; |
93 in [("_cabs", cabs_ast_tr')] end; |
87 *} |
94 *} |
88 |
95 |
|
96 text {* Dummy patterns for continuous abstraction *} |
89 translations |
97 translations |
90 "\<Lambda> _. t" == "Abs_CFun (\<lambda> _. t)" |
98 "\<Lambda> _. t" => "Abs_CFun (\<lambda> _. t)" |
|
99 |
91 |
100 |
92 subsection {* Continuous function space is pointed *} |
101 subsection {* Continuous function space is pointed *} |
93 |
102 |
94 lemma UU_CFun: "\<bottom> \<in> CFun" |
103 lemma UU_CFun: "\<bottom> \<in> CFun" |
95 by (simp add: CFun_def inst_fun_pcpo cont_const) |
104 by (simp add: CFun_def inst_fun_pcpo cont_const) |