19171
|
1 |
(* $Id$ *)
|
|
2 |
|
|
3 |
theory Recursion
|
|
4 |
imports "Iteration"
|
|
5 |
begin
|
|
6 |
|
|
7 |
types 'a f1_ty' = "name\<Rightarrow>('a::pt_name)"
|
|
8 |
'a f2_ty' = "lam\<Rightarrow>lam\<Rightarrow>'a\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
|
|
9 |
'a f3_ty' = "lam\<Rightarrow>name\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
|
|
10 |
|
|
11 |
constdefs
|
|
12 |
rfun' :: "'a f1_ty' \<Rightarrow> 'a f2_ty' \<Rightarrow> 'a f3_ty' \<Rightarrow> lam \<Rightarrow> (lam\<times>'a::pt_name)"
|
|
13 |
"rfun' f1 f2 f3 t \<equiv>
|
|
14 |
(itfun
|
|
15 |
(\<lambda>a. (Var a,f1 a))
|
|
16 |
(\<lambda>r1 r2. (App (fst r1) (fst r2), f2 (fst r1) (fst r2) (snd r1) (snd r2)))
|
|
17 |
(\<lambda>a r. (Lam [a].(fst r),f3 (fst r) a (snd r)))
|
|
18 |
t)"
|
|
19 |
|
|
20 |
rfun :: "'a f1_ty' \<Rightarrow> 'a f2_ty' \<Rightarrow> 'a f3_ty' \<Rightarrow> lam \<Rightarrow> 'a::pt_name"
|
|
21 |
"rfun f1 f2 f3 t \<equiv> snd (rfun' f1 f2 f3 t)"
|
|
22 |
|
|
23 |
lemma fcb':
|
|
24 |
fixes f3::"('a::pt_name) f3_ty'"
|
|
25 |
assumes f: "finite ((supp (f1,f2,f3))::name set)"
|
|
26 |
and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
|
|
27 |
shows "\<exists>a. a \<sharp> (\<lambda>a r. (Lam [a].fst r, f3 (fst r) a (snd r))) \<and>
|
|
28 |
(\<forall>y. a \<sharp> (Lam [a].fst y, f3 (fst y) a (snd y)))"
|
|
29 |
using c f
|
|
30 |
apply(auto)
|
|
31 |
apply(rule_tac x="a" in exI)
|
|
32 |
apply(auto simp add: abs_fresh fresh_prod)
|
|
33 |
apply(rule_tac S="supp f3" in supports_fresh)
|
|
34 |
apply(supports_simp add: perm_fst perm_snd)
|
|
35 |
apply(simp add: supp_prod)
|
|
36 |
apply(simp add: fresh_def)
|
|
37 |
done
|
|
38 |
|
|
39 |
lemma fsupp':
|
|
40 |
fixes f1::"('a::pt_name) f1_ty'"
|
|
41 |
and f2::"('a::pt_name) f2_ty'"
|
|
42 |
and f3::"('a::pt_name) f3_ty'"
|
|
43 |
assumes f: "finite ((supp (f1,f2,f3))::name set)"
|
|
44 |
shows "finite((supp
|
|
45 |
(\<lambda>a. (Var a, f1 a),
|
|
46 |
\<lambda>r1 r2. (App (fst r1) (fst r2), f2 (fst r1) (fst r2) (snd r1) (snd r2)),
|
|
47 |
\<lambda>a r. (Lam [a].fst r, f3 (fst r) a (snd r))))::name set)"
|
|
48 |
using f by (finite_guess add: perm_fst perm_snd fs_name1 supp_prod)
|
|
49 |
|
|
50 |
lemma rfun'_fst:
|
|
51 |
fixes f1::"('a::pt_name) f1_ty'"
|
|
52 |
and f2::"('a::pt_name) f2_ty'"
|
|
53 |
and f3::"('a::pt_name) f3_ty'"
|
|
54 |
assumes f: "finite ((supp (f1,f2,f3))::name set)"
|
|
55 |
and c: "(\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y))"
|
|
56 |
shows "fst (rfun' f1 f2 f3 t) = t"
|
|
57 |
apply(rule lam.induct'[of "\<lambda>_. ((supp (f1,f2,f3))::name set)" "\<lambda>_ t. fst (rfun' f1 f2 f3 t) = t"])
|
|
58 |
apply(fold fresh_def)
|
|
59 |
apply(simp add: f)
|
|
60 |
apply(unfold rfun'_def)
|
|
61 |
apply(simp only: itfun_Var[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
|
|
62 |
apply(simp)
|
|
63 |
apply(simp only: itfun_App[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
|
|
64 |
apply(simp)
|
|
65 |
apply(auto)
|
|
66 |
apply(rule trans)
|
|
67 |
apply(rule_tac f="fst" in arg_cong)
|
|
68 |
apply(rule itfun_Lam[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
|
|
69 |
apply(auto simp add: fresh_prod)
|
|
70 |
apply(rule_tac S="supp f1" in supports_fresh)
|
|
71 |
apply(supports_simp)
|
|
72 |
apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
|
|
73 |
apply(simp add: supp_prod)
|
|
74 |
apply(rule f)
|
|
75 |
apply(simp add: fresh_def)
|
|
76 |
apply(rule_tac S="supp f2" in supports_fresh)
|
|
77 |
apply(supports_simp add: perm_fst perm_snd)
|
|
78 |
apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
|
|
79 |
apply(simp add: supp_prod)
|
|
80 |
apply(rule f)
|
|
81 |
apply(simp add: fresh_def)
|
|
82 |
apply(rule_tac S="supp f3" in supports_fresh)
|
|
83 |
apply(supports_simp add: perm_fst perm_snd)
|
|
84 |
apply(subgoal_tac "finite ((supp (f1,f2,f3))::name set)")
|
|
85 |
apply(simp add: supp_prod)
|
|
86 |
apply(rule f)
|
|
87 |
apply(simp add: fresh_def)
|
|
88 |
done
|
|
89 |
|
|
90 |
lemma rfun'_Var:
|
|
91 |
fixes f1::"('a::pt_name) f1_ty'"
|
|
92 |
and f2::"('a::pt_name) f2_ty'"
|
|
93 |
and f3::"('a::pt_name) f3_ty'"
|
|
94 |
assumes f: "finite ((supp (f1,f2,f3))::name set)"
|
|
95 |
and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
|
|
96 |
shows "rfun' f1 f2 f3 (Var c) = (Var c, f1 c)"
|
|
97 |
apply(simp add: rfun'_def)
|
|
98 |
apply(simp add: itfun_Var[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
|
|
99 |
done
|
|
100 |
|
|
101 |
lemma rfun'_App:
|
|
102 |
fixes f1::"('a::pt_name) f1_ty'"
|
|
103 |
and f2::"('a::pt_name) f2_ty'"
|
|
104 |
and f3::"('a::pt_name) f3_ty'"
|
|
105 |
assumes f: "finite ((supp (f1,f2,f3))::name set)"
|
|
106 |
and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
|
|
107 |
shows "rfun' f1 f2 f3 (App t1 t2) =
|
|
108 |
(App t1 t2, f2 t1 t2 (rfun f1 f2 f3 t1) (rfun f1 f2 f3 t2))"
|
|
109 |
apply(simp add: rfun'_def)
|
|
110 |
apply(rule trans)
|
|
111 |
apply(rule itfun_App[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
|
|
112 |
apply(fold rfun'_def)
|
|
113 |
apply(simp_all add: rfun'_fst[OF f, OF c])
|
|
114 |
apply(simp_all add: rfun_def)
|
|
115 |
done
|
|
116 |
|
|
117 |
lemma rfun'_Lam:
|
|
118 |
fixes f1::"('a::pt_name) f1_ty'"
|
|
119 |
and f2::"('a::pt_name) f2_ty'"
|
|
120 |
and f3::"('a::pt_name) f3_ty'"
|
|
121 |
assumes f: "finite ((supp (f1,f2,f3))::name set)"
|
|
122 |
and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
|
|
123 |
and a: "b\<sharp>(f1,f2,f3)"
|
|
124 |
shows "rfun' f1 f2 f3 (Lam [b].t) = (Lam [b].t, f3 t b (rfun f1 f2 f3 t))"
|
|
125 |
using a f
|
|
126 |
apply(simp add: rfun'_def)
|
|
127 |
apply(rule trans)
|
|
128 |
apply(rule itfun_Lam[OF fsupp'[OF f],OF fcb'[OF f, OF c]])
|
|
129 |
apply(auto simp add: fresh_prod)
|
|
130 |
apply(rule_tac S="supp f1" in supports_fresh)
|
|
131 |
apply(supports_simp)
|
|
132 |
apply(simp add: supp_prod)
|
|
133 |
apply(simp add: fresh_def)
|
|
134 |
apply(rule_tac S="supp f2" in supports_fresh)
|
|
135 |
apply(supports_simp add: perm_fst perm_snd)
|
|
136 |
apply(simp add: supp_prod)
|
|
137 |
apply(simp add: fresh_def)
|
|
138 |
apply(rule_tac S="supp f3" in supports_fresh)
|
|
139 |
apply(supports_simp add: perm_snd perm_fst)
|
|
140 |
apply(simp add: supp_prod)
|
|
141 |
apply(simp add: fresh_def)
|
|
142 |
apply(fold rfun'_def)
|
|
143 |
apply(simp_all add: rfun'_fst[OF f, OF c])
|
|
144 |
apply(simp_all add: rfun_def)
|
|
145 |
done
|
|
146 |
|
|
147 |
lemma rfun_Var:
|
|
148 |
fixes f1::"('a::pt_name) f1_ty'"
|
|
149 |
and f2::"('a::pt_name) f2_ty'"
|
|
150 |
and f3::"('a::pt_name) f3_ty'"
|
|
151 |
assumes f: "finite ((supp (f1,f2,f3))::name set)"
|
|
152 |
and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
|
|
153 |
shows "rfun f1 f2 f3 (Var c) = f1 c"
|
|
154 |
apply(unfold rfun_def)
|
|
155 |
apply(simp add: rfun'_Var[OF f, OF c])
|
|
156 |
done
|
|
157 |
|
|
158 |
lemma rfun_App:
|
|
159 |
fixes f1::"('a::pt_name) f1_ty'"
|
|
160 |
and f2::"('a::pt_name) f2_ty'"
|
|
161 |
and f3::"('a::pt_name) f3_ty'"
|
|
162 |
assumes f: "finite ((supp (f1,f2,f3))::name set)"
|
|
163 |
and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
|
|
164 |
shows "rfun f1 f2 f3 (App t1 t2) = f2 t1 t2 (rfun f1 f2 f3 t1) (rfun f1 f2 f3 t2)"
|
|
165 |
apply(unfold rfun_def)
|
|
166 |
apply(simp add: rfun'_App[OF f, OF c])
|
|
167 |
apply(simp add: rfun_def)
|
|
168 |
done
|
|
169 |
|
|
170 |
lemma rfun_Lam:
|
|
171 |
fixes f1::"('a::pt_name) f1_ty'"
|
|
172 |
and f2::"('a::pt_name) f2_ty'"
|
|
173 |
and f3::"('a::pt_name) f3_ty'"
|
|
174 |
assumes f: "finite ((supp (f1,f2,f3))::name set)"
|
|
175 |
and c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name) t. a\<sharp>f3 t a y)"
|
|
176 |
and a: "b\<sharp>(f1,f2,f3)"
|
|
177 |
shows "rfun f1 f2 f3 (Lam [b].t) = f3 t b (rfun f1 f2 f3 t)"
|
|
178 |
using a
|
|
179 |
apply(unfold rfun_def)
|
|
180 |
apply(simp add: rfun'_Lam[OF f, OF c])
|
|
181 |
apply(simp add: rfun_def)
|
|
182 |
done
|
|
183 |
|
19651
|
184 |
|
19171
|
185 |
end |