equal
deleted
inserted
replaced
13 (n, m) = (hn, hm) \<or> (n \<noteq> hn \<and> m \<noteq> hm \<and> lookup n m t)" |
13 (n, m) = (hn, hm) \<or> (n \<noteq> hn \<and> m \<noteq> hm \<and> lookup n m t)" |
14 apply (simp add: eqvt_def lookup_graph_def) |
14 apply (simp add: eqvt_def lookup_graph_def) |
15 apply (rule, perm_simp, rule, rule) |
15 apply (rule, perm_simp, rule, rule) |
16 by pat_completeness auto |
16 by pat_completeness auto |
17 |
17 |
18 termination (eqvt) by lexicographic_order |
18 nominal_termination (eqvt) by lexicographic_order |
19 |
19 |
20 nominal_function lam2_rec where |
20 nominal_function lam2_rec where |
21 "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs" |
21 "lam2_rec faa fll xs (Var n) (Var m) = lookup n m xs" |
22 | "lam2_rec faa fll xs (Var n) (App l r) = False" |
22 | "lam2_rec faa fll xs (Var n) (App l r) = False" |
23 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False" |
23 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False" |
72 apply clarify |
72 apply clarify |
73 apply metis |
73 apply metis |
74 apply simp |
74 apply simp |
75 done |
75 done |
76 |
76 |
77 termination (eqvt) by lexicographic_order |
77 nominal_termination (eqvt) by lexicographic_order |
78 |
78 |
79 lemma lam_rec2_cong[fundef_cong]: |
79 lemma lam_rec2_cong[fundef_cong]: |
80 "(\<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> |
80 "(\<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> |
81 (\<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> |
81 (\<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> |
82 lam2_rec faa fll xs l l2 = lam2_rec faa' fll' xs l l2" |
82 lam2_rec faa fll xs l l2 = lam2_rec faa' fll' xs l l2" |
104 (%x t y s. aux t s ((x, y) # xs)) xs l r" |
104 (%x t y s. aux t s ((x, y) # xs)) xs l r" |
105 unfolding eqvt_def aux_graph_def |
105 unfolding eqvt_def aux_graph_def |
106 apply (rule, perm_simp, rule, rule) |
106 apply (rule, perm_simp, rule, rule) |
107 by pat_completeness auto |
107 by pat_completeness auto |
108 |
108 |
109 termination (eqvt) |
109 nominal_termination (eqvt) |
110 by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all |
110 by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all |
111 |
111 |
112 lemma aux_simps[simp]: |
112 lemma aux_simps[simp]: |
113 "aux (Var x) (Var y) xs = lookup x y xs" |
113 "aux (Var x) (Var y) xs = lookup x y xs" |
114 "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)" |
114 "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)" |
231 apply (simp add: flip_fresh_fresh flip_eqvt) |
231 apply (simp add: flip_fresh_fresh flip_eqvt) |
232 apply (subst permute_eqvt) |
232 apply (subst permute_eqvt) |
233 apply (simp add: flip_fresh_fresh flip_eqvt) |
233 apply (simp add: flip_fresh_fresh flip_eqvt) |
234 done |
234 done |
235 |
235 |
236 termination (eqvt) by lexicographic_order |
236 nominal_termination (eqvt) by lexicographic_order |
237 |
237 |
238 lemma var_eq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> swapequal (Var ab) (Var ab) xs" |
238 lemma var_eq_swapequal: "atom ab \<sharp> xs \<Longrightarrow> swapequal (Var ab) (Var ab) xs" |
239 apply (induct xs) |
239 apply (induct xs) |
240 apply simp |
240 apply simp |
241 apply (case_tac a) |
241 apply (case_tac a) |