| author | Christian Urban <urbanc@in.tum.de> |
| Sun, 17 Jan 2010 02:24:15 +0100 | |
| changeset 899 | 2468c0f2b276 |
| parent 892 | 693aecde755d |
| child 917 | 2cb5745f403e |
| permissions | -rw-r--r-- |
|
872
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Terms |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports Nominal "../QuotMain" "../QuotList" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
atom_decl name |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
899
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
7 |
text {* primrec seems to be genarally faster than fun *}
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
8 |
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
9 |
section {*** lets with binding patterns ***}
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
10 |
|
|
872
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
datatype trm1 = |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
Vr1 "name" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
| Ap1 "trm1" "trm1" |
|
892
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
14 |
| Lm1 "name" "trm1" --"name is bound in trm1" |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
15 |
| Lt1 "bp" "trm1" "trm1" --"all variables in bp are bound in the 2nd trm1" |
|
872
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
and bp = |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
BUnit |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
| BVr "name" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
| BPr "bp" "bp" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
|
|
874
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
21 |
(* to be given by the user *) |
|
899
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
22 |
primrec |
|
874
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
23 |
bv1 |
|
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
24 |
where |
|
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
25 |
"bv1 (BUnit) = {}"
|
|
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
26 |
| "bv1 (BVr x) = {x}"
|
|
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
27 |
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
|
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
28 |
|
|
892
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
29 |
(* needs to be calculated by the package *) |
|
899
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
30 |
primrec |
|
892
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
31 |
fv_trm1 and fv_bp |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
32 |
where |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
33 |
"fv_trm1 (Vr1 x) = {x}"
|
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
34 |
| "fv_trm1 (Ap1 t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2)" |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
35 |
| "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {x}"
|
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
36 |
| "fv_trm1 (Lt1 bp t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2 - bv1 bp)" |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
37 |
| "fv_bp (BUnit) = {}"
|
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
38 |
| "fv_bp (BVr x) = {x}"
|
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
39 |
| "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)" |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
40 |
|
|
899
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
41 |
(* needs to be stated by the package *) |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
42 |
overloading |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
43 |
perm_trm1 \<equiv> "perm :: 'x prm \<Rightarrow> trm1 \<Rightarrow> trm1" (unchecked) |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
44 |
perm_bp \<equiv> "perm :: 'x prm \<Rightarrow> bp \<Rightarrow> bp" (unchecked) |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
45 |
begin |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
46 |
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
47 |
primrec |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
48 |
perm_trm1 and perm_bp |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
49 |
where |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
50 |
"perm_trm1 pi (Vr1 a) = Vr1 (pi \<bullet> a)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
51 |
| "perm_trm1 pi (Ap1 t1 t2) = Ap1 (perm_trm1 pi t1) (perm_trm1 pi t2)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
52 |
| "perm_trm1 pi (Lm1 a t) = Lm1 (pi \<bullet> a) (perm_trm1 pi t)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
53 |
| "perm_trm1 pi (Lt1 bp t1 t2) = Lt1 (perm_bp pi bp) (perm_trm1 pi t1) (perm_trm1 pi t2)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
54 |
| "perm_bp pi (BUnit) = BUnit" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
55 |
| "perm_bp pi (BVr a) = BVr (pi \<bullet> a)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
56 |
| "perm_bp pi (BPr bp1 bp2) = BPr (perm_bp pi bp1) (perm_bp pi bp2)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
57 |
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
58 |
end |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
59 |
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
60 |
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
61 |
section {*** lets with single assignments ***}
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
62 |
|
|
872
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
datatype trm2 = |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
Vr2 "name" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
| Ap2 "trm2" "trm2" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
| Lm2 "name" "trm2" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
| Lt2 "assign" "trm2" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
and assign = |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
As "name" "trm2" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
|
|
874
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
71 |
(* to be given by the user *) |
|
899
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
72 |
primrec |
|
874
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
73 |
bv2 |
|
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
74 |
where |
|
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
75 |
"bv2 (As x t) = {x}"
|
|
872
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
|
|
892
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
77 |
(* needs to be calculated by the package *) |
|
899
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
78 |
primrec |
|
892
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
79 |
fv_trm2 and fv_assign |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
80 |
where |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
81 |
"fv_trm2 (Vr2 x) = {x}"
|
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
82 |
| "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)" |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
83 |
| "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {x}"
|
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
84 |
| "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)" |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
85 |
| "fv_assign (As x t) = (fv_trm2 t)" |
|
874
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
86 |
|
|
899
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
87 |
(* needs to be stated by the package *) |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
88 |
overloading |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
89 |
perm_trm2 \<equiv> "perm :: 'x prm \<Rightarrow> trm2 \<Rightarrow> trm2" (unchecked) |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
90 |
perm_assign \<equiv> "perm :: 'x prm \<Rightarrow> assign \<Rightarrow> assign" (unchecked) |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
91 |
begin |
|
892
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
92 |
|
|
899
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
93 |
primrec |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
94 |
perm_trm2 and perm_assign |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
95 |
where |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
96 |
"perm_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
97 |
| "perm_trm2 pi (Ap2 t1 t2) = Ap2 (perm_trm2 pi t1) (perm_trm2 pi t2)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
98 |
| "perm_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (perm_trm2 pi t)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
99 |
| "perm_trm2 pi (Lt2 as t) = Lt2 (perm_assign pi as) (perm_trm2 pi t)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
100 |
| "perm_assign pi (As a t) = As (pi \<bullet> a) (perm_trm2 pi t)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
101 |
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
102 |
end |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
103 |
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
104 |
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
105 |
section {*** lets with many assignments ***}
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
106 |
|
|
872
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
107 |
datatype trm3 = |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
108 |
Vr3 "name" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
109 |
| Ap3 "trm3" "trm3" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
110 |
| Lm3 "name" "trm3" |
|
892
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
111 |
| Lt3 "assigns" "trm3" |
|
872
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
112 |
and assigns = |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
113 |
ANil |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
114 |
| ACons "name" "trm3" "assigns" |
|
2605ea41bbdd
added 3 calculi with interesting binding structure
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
115 |
|
|
874
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
116 |
(* to be given by the user *) |
|
899
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
117 |
primrec |
|
874
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
118 |
bv3 |
|
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
119 |
where |
|
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
120 |
"bv3 ANil = {}"
|
|
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
121 |
| "bv3 (ACons x t as) = {x} \<union> (bv3 as)"
|
|
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
122 |
|
|
899
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
123 |
primrec |
|
892
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
124 |
fv_trm3 and fv_assigns |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
125 |
where |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
126 |
"fv_trm3 (Vr3 x) = {x}"
|
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
127 |
| "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)" |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
128 |
| "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {x}"
|
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
129 |
| "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)" |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
130 |
| "fv_assigns (ANil) = {}"
|
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
131 |
| "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)" |
|
693aecde755d
added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de>
parents:
874
diff
changeset
|
132 |
|
|
899
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
133 |
(* needs to be stated by the package *) |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
134 |
overloading |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
135 |
perm_trm3 \<equiv> "perm :: 'x prm \<Rightarrow> trm3 \<Rightarrow> trm3" (unchecked) |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
136 |
perm_assigns \<equiv> "perm :: 'x prm \<Rightarrow> assigns \<Rightarrow> assigns" (unchecked) |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
137 |
begin |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
138 |
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
139 |
primrec |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
140 |
perm_trm3 and perm_assigns |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
141 |
where |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
142 |
"perm_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
143 |
| "perm_trm3 pi (Ap3 t1 t2) = Ap3 (perm_trm3 pi t1) (perm_trm3 pi t2)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
144 |
| "perm_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (perm_trm3 pi t)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
145 |
| "perm_trm3 pi (Lt3 as t) = Lt3 (perm_assigns pi as) (perm_trm3 pi t)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
146 |
| "perm_assigns pi (ANil) = ANil" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
147 |
| "perm_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (perm_trm3 pi t) (perm_assigns pi as)" |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
148 |
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
149 |
end |
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
150 |
|
|
2468c0f2b276
added permutation functions for the raw calculi
Christian Urban <urbanc@in.tum.de>
parents:
892
diff
changeset
|
151 |
|
|
874
ab8a58973861
added bound-variable functions to terms
Christian Urban <urbanc@in.tum.de>
parents:
872
diff
changeset
|
152 |
end |