70 and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
72 and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
71 shows "P c lam" |
73 shows "P c lam" |
72 proof - |
74 proof - |
73 have "\<And>p. P c (p \<bullet> lam)" |
75 have "\<And>p. P c (p \<bullet> lam)" |
74 apply(induct lam arbitrary: c rule: lam.induct) |
76 apply(induct lam arbitrary: c rule: lam.induct) |
75 apply(simp only: lam.perm) |
77 apply(perm_simp) |
76 apply(rule a1) |
78 apply(rule a1) |
77 apply(simp only: lam.perm) |
79 apply(perm_simp) |
78 apply(rule a2) |
80 apply(rule a2) |
79 apply(assumption) |
81 apply(assumption) |
80 apply(assumption) |
82 apply(assumption) |
81 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q") |
83 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q") |
82 apply(erule exE) |
84 apply(erule exE) |
83 apply(rule_tac t="p \<bullet> Lam name lam" and |
85 apply(rule_tac t="p \<bullet> Lam name lam" and |
84 s="q \<bullet> p \<bullet> Lam name lam" in subst) |
86 s="q \<bullet> p \<bullet> Lam name lam" in subst) |
85 defer |
87 defer |
86 apply(simp add: lam.perm) |
88 apply(simp) |
87 apply(rule a3) |
89 apply(rule a3) |
88 apply(simp add: eqvts fresh_star_def) |
90 apply(simp add: eqvts fresh_star_def) |
89 apply(drule_tac x="q + p" in meta_spec) |
91 apply(drule_tac x="q + p" in meta_spec) |
90 apply(simp) |
92 apply(simp) |
91 apply(rule at_set_avoiding2) |
93 apply(rule at_set_avoiding2) |
92 apply(simp add: finite_supp) |
94 apply(simp add: finite_supp) |
93 apply(simp add: finite_supp) |
95 apply(simp add: finite_supp) |
94 apply(simp add: finite_supp) |
96 apply(simp add: finite_supp) |
95 apply(simp only: lam.perm atom_eqvt) |
97 apply(perm_simp) |
96 apply(simp add: fresh_star_def fresh_def supp_fn') |
98 apply(simp add: fresh_star_def fresh_def supp_fn') |
97 apply(rule supp_perm_eq) |
99 apply(rule supp_perm_eq) |
98 apply(simp) |
100 apply(simp) |
99 done |
101 done |
100 then have "P c (0 \<bullet> lam)" by blast |
102 then have "P c (0 \<bullet> lam)" by blast |
101 then show "P c lam" by simp |
103 then show "P c lam" by simp |
102 qed |
104 qed |
|
105 |
|
106 section {* Typing *} |
|
107 |
|
108 nominal_datatype ty = |
|
109 TVar string |
|
110 | TFun ty ty ("_ \<rightarrow> _") |
|
111 |
|
112 inductive |
|
113 valid :: "(name \<times> ty) list \<Rightarrow> bool" |
|
114 where |
|
115 "valid []" |
|
116 | "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)" |
|
117 |
|
118 ML {* |
|
119 fun my_tac ctxt intros = |
|
120 Nominal_Permeq.eqvt_strict_tac ctxt [] [] |
|
121 THEN' resolve_tac intros |
|
122 THEN_ALL_NEW |
|
123 (atac ORELSE' |
|
124 EVERY' |
|
125 [ rtac (Drule.instantiate' [] [SOME @{cterm "- p::perm"}] @{thm permute_boolE}), |
|
126 Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [], |
|
127 atac ]) |
|
128 *} |
|
129 |
|
130 |
|
131 lemma |
|
132 assumes a: "valid Gamma" |
|
133 shows "valid (p \<bullet> Gamma)" |
|
134 using a |
|
135 apply(induct) |
|
136 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
|
137 apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *}) |
|
138 done |
|
139 |
|
140 declare permute_lam_raw.simps[eqvt] |
|
141 |
|
142 thm alpha_gen_real_eqvt[no_vars] |
|
143 |
|
144 lemma temporary: |
|
145 shows "(p \<bullet> (bs, x) \<approx>gen R f q (cs, y)) = (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)" |
|
146 apply(simp only: permute_bool_def) |
|
147 apply(rule iffI) |
|
148 apply(rule alpha_gen_real_eqvt) |
|
149 apply(assumption) |
|
150 apply(drule_tac p="-p" in alpha_gen_real_eqvt(1)) |
|
151 apply(simp) |
|
152 done |
|
153 |
|
154 lemma temporary_raw: |
|
155 shows "(p \<bullet> alpha_gen) \<equiv> alpha_gen" |
|
156 sorry |
|
157 |
|
158 declare temporary_raw[eqvt_raw] |
|
159 |
|
160 lemma |
|
161 assumes a: "alpha_lam_raw t1 t2" |
|
162 shows "alpha_lam_raw (p \<bullet> t1) (p \<bullet> t2)" |
|
163 using a |
|
164 apply(induct) |
|
165 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *}) |
|
166 apply(perm_strict_simp) |
|
167 apply(rule alpha_lam_raw.intros) |
|
168 apply(simp) |
|
169 apply(perm_strict_simp) |
|
170 apply(rule alpha_lam_raw.intros) |
|
171 apply(simp add: alphas) |
|
172 apply(rule_tac p="- p" in permute_boolE) |
|
173 apply(perm_simp permute_minus_cancel(2)) |
|
174 oops |
|
175 |
|
176 |
103 |
177 |
104 section {* size function *} |
178 section {* size function *} |
105 |
179 |
106 lemma size_eqvt_raw: |
180 lemma size_eqvt_raw: |
107 fixes t::"lam_raw" |
181 fixes t::"lam_raw" |