66 and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l" |
66 and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l" |
67 and fcb2: "\<And>l t1 t2 r1 r2. atom ` set l \<sharp>* (r1, r2) \<Longrightarrow> atom ` set l \<sharp>* f2 t1 t2 r1 r2 l" |
67 and fcb2: "\<And>l t1 t2 r1 r2. atom ` set l \<sharp>* (r1, r2) \<Longrightarrow> atom ` set l \<sharp>* f2 t1 t2 r1 r2 l" |
68 and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l" |
68 and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l" |
69 begin |
69 begin |
70 |
70 |
71 nominal_primrec |
71 nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y") |
72 f |
72 f |
73 where |
73 where |
74 "f (Var x) l = f1 x l" |
74 "f (Var x) l = f1 x l" |
75 | "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l" |
75 | "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l" |
76 | "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l" |
76 | "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l" |
77 apply (simp add: eqvt_def f_graph_def) |
77 apply (simp add: eqvt_def f_graph_def) |
78 apply (rule, perm_simp) |
78 apply (rule, perm_simp) |
79 apply (simp only: eq[unfolded eqvt_def]) |
79 apply (simp only: eq[unfolded eqvt_def]) |
|
80 apply (erule f_graph.induct) |
|
81 apply (simp add: fcb1) |
|
82 apply (simp add: fcb2 fresh_star_Pair) |
|
83 apply simp |
|
84 apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l") |
|
85 apply (simp add: fresh_star_def) |
|
86 apply (rule fcb3) |
|
87 apply (simp add: fresh_star_def fresh_def) |
|
88 apply simp_all |
80 apply(case_tac x) |
89 apply(case_tac x) |
81 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
90 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
82 apply(auto simp add: fresh_star_def) |
91 apply(auto simp add: fresh_star_def) |
83 apply(erule Abs1_eq_fdest) |
92 apply(erule Abs1_eq_fdest) |
84 defer |
93 defer |
97 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
106 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
98 apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la") |
107 apply (subgoal_tac "atom ` set (x # la) \<sharp>* f3 x t (f_sumC (t, x # la)) la") |
99 apply (simp add: fresh_star_def) |
108 apply (simp add: fresh_star_def) |
100 apply (rule fcb3) |
109 apply (rule fcb3) |
101 apply (rule_tac x="x # la" in meta_spec) |
110 apply (rule_tac x="x # la" in meta_spec) |
102 apply (thin_tac "eqvt_at f_sumC (t, x # la)") |
111 unfolding fresh_star_def |
103 apply (thin_tac "atom x \<sharp> la") |
112 --"Exactly the assumption just for the other argument" |
104 apply (thin_tac "atom xa \<sharp> la") |
|
105 apply (thin_tac "x \<noteq> xa") |
|
106 apply (thin_tac "atom xa \<sharp> t") |
|
107 apply (subgoal_tac "atom ` set (snd (t, xb)) \<sharp>* f_sumC (t, xb)") |
|
108 apply simp |
|
109 apply (rule_tac x="(t, xb)" in meta_spec) |
|
110 apply (simp only: triv_forall_equality) |
|
111 --"We start induction on the graph. We need the 2nd subgoal in the first one" |
|
112 apply (subgoal_tac "\<And>x y. f_graph x y \<Longrightarrow> atom ` set (snd x) \<sharp>* y") |
|
113 apply (rule the_default_pty[OF f_sumC_def]) |
|
114 prefer 2 |
|
115 apply blast |
|
116 prefer 2 |
|
117 apply (erule f_graph.induct) |
|
118 apply (simp add: fcb1) |
|
119 apply (simp add: fcb2 fresh_star_Pair) |
|
120 apply (simp only: snd_conv) |
|
121 apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l") |
|
122 apply (simp add: fresh_star_def) |
|
123 apply (rule fcb3) |
|
124 apply assumption |
|
125 --"We'd like to do the proof with this property" |
|
126 apply (case_tac xc) |
|
127 apply simp |
|
128 apply (rule_tac lam="a" and c="b" in lam.strong_induct) |
|
129 apply (rule_tac a="f1 name c" in ex1I) |
|
130 apply (rule f_graph.intros) |
|
131 apply (erule f_graph.cases) |
|
132 apply simp_all[3] |
|
133 apply (drule_tac x="c" in meta_spec)+ |
|
134 apply (erule ex1E)+ |
|
135 apply (subgoal_tac "f_graph (lam1, c) (f_sumC (lam1, c))") |
|
136 apply (subgoal_tac "f_graph (lam2, c) (f_sumC (lam2, c))") |
|
137 apply (rule_tac a="f2 lam1 lam2 (f_sumC (lam1, c)) (f_sumC (lam2, c)) c" in ex1I) |
|
138 apply (rule_tac f_graph.intros(2)) |
|
139 apply assumption+ |
|
140 apply (rotate_tac 8) |
|
141 apply (erule f_graph.cases) |
|
142 apply simp |
|
143 apply auto[1] |
|
144 apply metis |
|
145 apply simp |
|
146 apply (simp add: f_sumC_def) |
|
147 apply (rule THE_defaultI') |
|
148 apply metis |
|
149 apply (simp add: f_sumC_def) |
|
150 apply (rule THE_defaultI') |
|
151 apply metis |
|
152 --"Only the Lambda case left" |
|
153 apply (subgoal_tac "f_graph (lam, (name # c)) (f_sumC (lam, (name # c)))") |
|
154 prefer 2 |
|
155 apply (simp add: f_sumC_def) |
|
156 apply (rule THE_defaultI') |
|
157 apply assumption |
|
158 apply (rule_tac a="f3 name lam (f_sumC (lam, name # c)) c" in ex1I) |
|
159 apply (rule f_graph.intros(3)) |
|
160 apply (simp add: fresh_star_def) |
|
161 apply assumption |
|
162 apply (rotate_tac -1) |
|
163 apply (erule f_graph.cases) |
|
164 apply simp_all[2] |
|
165 apply simp |
|
166 apply auto[1] |
|
167 apply (subgoal_tac "f_sumC (lam, name # l) = f_sum (lam, name # l)") |
|
168 apply simp |
|
169 apply (rule sym) |
|
170 apply (erule Abs1_eq_fdest) |
|
171 apply (subgoal_tac "atom ` set (name # l) \<sharp>* f3 name lam (f_sum (lam, name # l)) l") |
|
172 apply (simp add: fresh_star_def) |
|
173 apply (rule fcb3) |
|
174 apply metis |
|
175 apply (rule fresh_fun_eqvt_app4[OF eq(3)]) |
|
176 apply (simp add: fresh_at_base) |
|
177 apply assumption |
|
178 defer --"eqvt_at f_sumC" |
|
179 apply assumption |
|
180 apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 name y r l) = f3 (p \<bullet> name) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)") |
|
181 apply (subgoal_tac "(atom name \<rightleftharpoons> atom xa) \<bullet> l = l") |
|
182 apply (simp add: eq[unfolded eqvt_def]) |
|
183 defer --"eqvt_at f_sumC" |
|
184 apply (metis fresh_star_insert swap_fresh_fresh) |
|
185 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
|
186 apply simp |
|
187 sorry |
113 sorry |
188 |
114 |
189 termination |
115 termination |
190 by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size) |
116 by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size) |
191 |
117 |