71 apply (subgoal_tac "Lam [x]. Var x = Lam [fv]. Var fv") |
71 apply (subgoal_tac "Lam [x]. Var x = Lam [fv]. Var fv") |
72 apply simp |
72 apply simp |
73 apply (simp add: lam.eq_iff Abs1_eq_iff lam.supp fresh_def supp_at_base) |
73 apply (simp add: lam.eq_iff Abs1_eq_iff lam.supp fresh_def supp_at_base) |
74 done |
74 done |
75 |
75 |
|
76 nominal_primrec |
|
77 Pair_pre |
|
78 where |
|
79 "atom z \<sharp> (M, N) \<Longrightarrow> (Pair_pre M N) (Lam [z]. _) = (Lam [z]. App (App (Var z) M) N)" |
|
80 | "(Pair_pre M N) (App l r) = (App l r)" |
|
81 | "(Pair_pre M N) (Var v) = (Var v)" |
|
82 apply (subgoal_tac "\<And>p a x. Pair_pre_graph a x \<Longrightarrow> Pair_pre_graph (p \<bullet> a) (p \<bullet> x)") |
|
83 apply (simp add: eqvt_def) |
|
84 apply (intro allI) |
|
85 apply(simp add: permute_fun_def) |
|
86 apply(rule ext) |
|
87 apply(rule ext) |
|
88 apply(simp add: permute_bool_def) |
|
89 apply rule |
|
90 apply(drule_tac x="p" in meta_spec) |
|
91 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
92 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
93 apply simp |
|
94 apply(drule_tac x="-p" in meta_spec) |
|
95 apply(drule_tac x="x" in meta_spec) |
|
96 apply(drule_tac x="xa" in meta_spec) |
|
97 apply simp |
|
98 apply (erule Pair_pre_graph.induct) |
|
99 apply (simp_all add: Pair_pre_graph.intros)[3] |
|
100 apply (case_tac x) |
|
101 apply clarify |
|
102 apply (simp add: symmetric[OF atomize_conjL]) |
|
103 apply (rule_tac y="c" and c="(ab, ba)" in lam.strong_exhaust) |
|
104 apply (simp_all add: lam.distinct symmetric[OF atomize_conjL] lam.eq_iff Abs1_eq_iff fresh_star_def) |
|
105 apply auto[1] |
|
106 apply (simp_all add: fresh_Pair lam.fresh fresh_at_base) |
|
107 apply (rule swap_fresh_fresh[symmetric]) |
|
108 prefer 3 |
|
109 apply (rule swap_fresh_fresh[symmetric]) |
|
110 apply simp_all |
|
111 done |
|
112 |
|
113 termination |
|
114 by (relation "measure (\<lambda>(t,_). size t)") |
|
115 (simp_all add: lam.size) |
|
116 |
|
117 consts cx :: name |
|
118 |
|
119 fun |
|
120 Pair where |
|
121 "(Pair M N) = (Pair_pre M N (Lam [cx]. Var cx))" |
|
122 |
|
123 lemma Pair : "atom z \<sharp> (M, N) \<Longrightarrow> Pair M N = (Lam [z]. App (App (Var z) M) N)" |
|
124 apply simp |
|
125 apply (subgoal_tac "Lam [cx]. Var cx = Lam[z]. Var z") |
|
126 apply simp |
|
127 apply (auto simp add: lam.eq_iff Abs1_eq_iff) |
|
128 by (metis Rep_name_inject atom_name_def fresh_at_base lam.fresh(1)) |
|
129 |
|
130 |
|
131 |
76 end |
132 end |
77 |
133 |
78 |
134 |
79 |
135 |