|
1 theory Lambda imports "../Nominal2" begin |
|
2 |
|
3 atom_decl name |
|
4 |
|
5 nominal_datatype lam = |
|
6 Var "name" |
|
7 | App "lam" "lam" |
|
8 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
|
9 |
|
10 nominal_primrec lam2_rec where |
|
11 "lam2_rec faa fll xs (Var n) (Var m) = ((n, m) \<in> set xs)" |
|
12 | "lam2_rec faa fll xs (Var n) (App l r) = False" |
|
13 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False" |
|
14 | "lam2_rec faa fll xs (App l r) (Var n) = False" |
|
15 | "lam2_rec faa fll xs (App l1 r1) (App l2 r2) = faa l1 r1 l2 r2" |
|
16 | "lam2_rec faa fll xs (App l r) (Lam [x]. t) = False" |
|
17 | "lam2_rec faa fll xs (Lam [x]. t) (Var n) = False" |
|
18 | "lam2_rec faa fll xs (Lam [x]. t) (App l1 r1) = False" |
|
19 | "(atom x \<sharp> (xs, Lam [y]. s) \<and> atom y \<sharp> (x, xs, Lam [x]. t) \<and> |
|
20 (\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s' |
|
21 \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow> |
|
22 lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = fll x t y s" |
|
23 | "(atom x \<sharp> (xs, Lam [y]. s) \<and> atom y \<sharp> (x, xs, Lam [x]. t) \<and> |
|
24 \<not>(\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s' |
|
25 \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow> |
|
26 lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = False" |
|
27 apply (simp add: eqvt_def lam2_rec_graph_def) |
|
28 apply (rule, perm_simp, rule, rule) |
|
29 defer |
|
30 apply (simp_all)[53] |
|
31 apply clarify |
|
32 apply metis |
|
33 apply simp |
|
34 apply (case_tac x) |
|
35 apply (rule_tac y="d" and c="(c, e)" in lam.strong_exhaust) |
|
36 apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust) |
|
37 apply simp_all[3] |
|
38 apply (metis, metis, metis) |
|
39 apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust) |
|
40 apply simp_all[3] |
|
41 apply (metis, metis, metis) |
|
42 apply (rule_tac y="e" and c="(name, c, d)" in lam.strong_exhaust) |
|
43 apply simp_all[2] |
|
44 apply (metis, metis) |
|
45 apply (thin_tac "\<And>faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \<Longrightarrow> P") |
|
46 apply (thin_tac "\<And>faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \<Longrightarrow> P") |
|
47 apply (thin_tac "\<And>faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \<Longrightarrow> P") |
|
48 apply (thin_tac "\<And>faa fll xs l1 r1 l2 r2. x = (faa, fll, xs, App l1 r1, App l2 r2) \<Longrightarrow> P") |
|
49 apply (thin_tac "\<And>faa fll xs l r n. x = (faa, fll, xs, App l r, Var n) \<Longrightarrow> P") |
|
50 apply (thin_tac "\<And>faa fll xs l r xa t. x = (faa, fll, xs, App l r, Lam [xa]. t) \<Longrightarrow> P") |
|
51 apply (thin_tac "\<And>faa fll xs xa t n. x = (faa, fll, xs, Lam [xa]. t, Var n) \<Longrightarrow> P") |
|
52 apply (thin_tac "\<And>faa fll xs xa t l1 r1. x = (faa, fll, xs, Lam [xa]. t, App l1 r1) \<Longrightarrow> P") |
|
53 apply (drule_tac x="name" in meta_spec)+ |
|
54 apply (drule_tac x="c" in meta_spec)+ |
|
55 apply (drule_tac x="namea" in meta_spec)+ |
|
56 apply (drule_tac x="lama" in meta_spec) |
|
57 apply (drule_tac x="lama" in meta_spec) |
|
58 apply (drule_tac x="lam" in meta_spec)+ |
|
59 apply (drule_tac x="b" in meta_spec)+ |
|
60 apply (drule_tac x="a" in meta_spec)+ |
|
61 apply (case_tac " |
|
62 (\<forall>x' y' t' s'. |
|
63 atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow> |
|
64 atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> |
|
65 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
|
66 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s') |
|
67 ") |
|
68 apply clarify |
|
69 apply (simp add: fresh_star_def) |
|
70 apply (thin_tac "\<lbrakk>atom name \<sharp> (c, Lam [namea]. lama) \<and> |
|
71 atom namea \<sharp> (name, c, Lam [name]. lam) \<and> |
|
72 (\<forall>x' y' t' s'. |
|
73 atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow> |
|
74 atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow> |
|
75 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
|
76 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s'); |
|
77 x = (a, b, c, Lam [name]. lam, Lam [namea]. lama)\<rbrakk> |
|
78 \<Longrightarrow> P") |
|
79 apply (simp add: fresh_star_def) |
|
80 done |
|
81 |
|
82 termination (eqvt) by lexicographic_order |
|
83 |
|
84 lemma lam_rec2_cong[fundef_cong]: |
|
85 "(\<And>s1 s2 s3 s4. l = App s1 s2 \<Longrightarrow> l2 = App s3 s4 \<Longrightarrow> faa s1 s2 s3 s4 = faa' s1 s2 s3 s4) \<Longrightarrow> |
|
86 (\<And>n t n' t'. l = Lam [n]. t \<Longrightarrow> l2 = Lam [n']. t' \<Longrightarrow> fll n t n' t' = fll' n t n' t') \<Longrightarrow> |
|
87 lam2_rec faa fll xs l l2 = lam2_rec faa' fll' xs l l2" |
|
88 apply (rule_tac y="l" and c="(xs, l2)" in lam.strong_exhaust) |
|
89 apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3] |
|
90 apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3] |
|
91 apply (rule_tac y="l2" and c="(name, xs, l)" in lam.strong_exhaust) |
|
92 apply auto[2] |
|
93 apply clarify |
|
94 apply (case_tac "(\<forall>x' y' t' s'. |
|
95 atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> |
|
96 atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> |
|
97 Lam [name]. lam = Lam [x']. t' \<longrightarrow> |
|
98 Lam [namea]. lama = Lam [y']. s' \<longrightarrow> |
|
99 fll name lam namea lama = fll x' t' y' s')") |
|
100 apply (subst lam2_rec.simps) apply (simp add: fresh_star_def) |
|
101 apply (subst lam2_rec.simps) apply (simp add: fresh_star_def) |
|
102 using Abs1_eq_iff lam.eq_iff apply metis |
|
103 apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def) |
|
104 apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def) |
|
105 apply rule |
|
106 done |
|
107 |
|
108 nominal_primrec aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool" |
|
109 where |
|
110 [simp del]: "aux l r xs = lam2_rec |
|
111 (%t1 t2 t3 t4. (aux t1 t3 xs) \<and> (aux t2 t4 xs)) |
|
112 (%x t y s. aux t s ((x, y) # xs)) xs l r" |
|
113 unfolding eqvt_def aux_graph_def |
|
114 apply (rule, perm_simp, rule, rule) |
|
115 by pat_completeness auto |
|
116 |
|
117 termination (eqvt) |
|
118 by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all |
|
119 |
|
120 lemma aux_simps: |
|
121 "aux (Var x) (Var y) xs = ((x, y) \<in> set xs)" |
|
122 "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)" |
|
123 "aux (Var x) (App t1 t2) xs = False" |
|
124 "aux (Var x) (Lam [y].t) xs = False" |
|
125 "aux (App t1 t2) (Var x) xs = False" |
|
126 "aux (App t1 t2) (Lam [x].t) xs = False" |
|
127 "aux (Lam [x].t) (Var y) xs = False" |
|
128 "aux (Lam [x].t) (App t1 t2) xs = False" |
|
129 "\<lbrakk>atom x \<sharp> (s, xs); atom y \<sharp> (x, t, xs)\<rbrakk> \<Longrightarrow> aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)" |
|
130 apply (subst aux.simps, simp) |
|
131 apply (subst aux.simps, simp) |
|
132 apply (subst aux.simps, simp) |
|
133 apply (subst aux.simps, simp) |
|
134 apply (subst aux.simps, simp) |
|
135 apply (subst aux.simps, simp) |
|
136 apply (subst aux.simps, simp) |
|
137 apply (subst aux.simps, simp) |
|
138 apply (subst aux.simps) |
|
139 apply (subst lam2_rec.simps) |
|
140 prefer 2 apply rule |
|
141 apply (rule, simp add: lam.fresh) |
|
142 apply (rule, simp add: lam.fresh) |
|
143 apply (intro allI impI) |
|
144 apply (rule_tac x="(x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh) |
|
145 apply (rule_tac x="(a, x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh) |
|
146 apply (rule_tac s="aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) s ((a, y) # xs)" in trans) |
|
147 apply (rule_tac s="(atom x \<rightleftharpoons> atom a) \<bullet> aux t s ((x, y) # xs)" in trans) |
|
148 apply (rule permute_pure[symmetric]) |
|
149 apply (simp add: eqvts swap_fresh_fresh) |
|
150 apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim) |
|
151 apply (rename_tac b) |
|
152 apply (rule_tac s="aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) ((atom y \<rightleftharpoons> atom b) \<bullet> s) ((a, b) # xs)" in trans) |
|
153 apply (rule_tac s="(atom y \<rightleftharpoons> atom b) \<bullet> aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) s ((a, y) # xs)" in trans) |
|
154 apply (rule permute_pure[symmetric]) |
|
155 apply (simp add: eqvts swap_fresh_fresh) |
|
156 apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim) |
|
157 apply (subst permute_eqvt) |
|
158 apply (simp add: eqvts swap_fresh_fresh) |
|
159 apply (rule sym) |
|
160 apply (rule_tac s="aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') s' ((a, y') # xs)" in trans) |
|
161 apply (rule_tac s="(atom x' \<rightleftharpoons> atom a) \<bullet> aux t' s' ((x', y') # xs)" in trans) |
|
162 apply (rule permute_pure[symmetric]) |
|
163 apply (simp add: eqvts swap_fresh_fresh) |
|
164 apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim swap_fresh_fresh) |
|
165 apply (rule_tac s="aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') ((atom y' \<rightleftharpoons> atom b) \<bullet> s') ((a, b) # xs)" in trans) |
|
166 apply (rule_tac s="(atom y' \<rightleftharpoons> atom b) \<bullet> aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') s' ((a, y') # xs)" in trans) |
|
167 apply (rule permute_pure[symmetric]) |
|
168 apply (simp add: eqvts swap_fresh_fresh) |
|
169 apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim swap_fresh_fresh) |
|
170 apply (subst permute_eqvt) |
|
171 apply (simp add: eqvts swap_fresh_fresh) |
|
172 apply (subgoal_tac "(atom x' \<rightleftharpoons> atom a) \<bullet> t' = (atom x \<rightleftharpoons> atom a) \<bullet> t") |
|
173 apply (subgoal_tac "(atom y' \<rightleftharpoons> atom b) \<bullet> s' = (atom y \<rightleftharpoons> atom b) \<bullet> s") |
|
174 apply simp |
|
175 apply (subgoal_tac "Lam [y]. s = Lam [b]. ((atom y \<rightleftharpoons> atom b) \<bullet> s)") |
|
176 apply (subgoal_tac "Lam [y']. s' = Lam [b]. ((atom y' \<rightleftharpoons> atom b) \<bullet> s')") |
|
177 apply (auto simp add: fresh_Pair_elim Abs1_eq_iff)[1] |
|
178 apply (rule sym) |
|
179 apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute) |
|
180 apply (rule sym) |
|
181 apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute) |
|
182 apply (subgoal_tac "Lam [x]. t = Lam [a]. ((atom x \<rightleftharpoons> atom a) \<bullet> t)") |
|
183 apply (subgoal_tac "Lam [x']. t' = Lam [a]. ((atom x' \<rightleftharpoons> atom a) \<bullet> t')") |
|
184 apply (auto simp add: fresh_Pair_elim Abs1_eq_iff)[1] |
|
185 apply (rule sym) |
|
186 apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute) |
|
187 apply (rule sym) |
|
188 apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute) |
|
189 done |
|
190 |
|
191 end |
|
192 |
|
193 |
|
194 |