76 apply(simp add: permute_bn trm_assn.bn_defs) |
77 apply(simp add: permute_bn trm_assn.bn_defs) |
77 apply(simp add: permute_bn trm_assn.bn_defs) |
78 apply(simp add: permute_bn trm_assn.bn_defs) |
78 apply(simp add: atom_eqvt) |
79 apply(simp add: atom_eqvt) |
79 done |
80 done |
80 |
81 |
81 thm trm_assn.supp |
82 lemma strong_exhaust1: |
82 |
83 fixes c::"'a::fs" |
83 lemma "as \<sharp>* x \<longleftrightarrow> (\<forall>a\<in>as. a \<sharp> x)" |
84 assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P" |
84 apply(simp add: fresh_def) |
85 and "\<And>trm1 trm2 ca. \<lbrakk>c = ca; y = App trm1 trm2\<rbrakk> \<Longrightarrow> P" |
85 apply(simp add: fresh_star_def) |
86 and "\<And>name trm ca. \<lbrakk>{atom name} \<sharp>* ca; c = ca; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
86 oops |
87 and "\<And>assn trm ca. \<lbrakk>set (bn assn) \<sharp>* ca; c = ca; y = Let assn trm\<rbrakk> \<Longrightarrow> P" |
87 |
88 shows "P" |
88 inductive |
89 apply(rule_tac y="y" in trm_assn.exhaust(1)) |
89 test_trm :: "trm \<Rightarrow> bool" |
90 apply(rule assms(1)) |
90 and test_assn :: "assn \<Rightarrow> bool" |
91 apply(auto)[2] |
91 where |
92 apply(rule assms(2)) |
92 "test_trm (Var x)" |
93 apply(auto)[2] |
93 | "\<lbrakk>test_trm t1; test_trm t2\<rbrakk> \<Longrightarrow> test_trm (App t1 t2)" |
94 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
94 | "\<lbrakk>test_trm t; {atom x} \<sharp>* Lam x t\<rbrakk> \<Longrightarrow> test_trm (Lam x t)" |
|
95 | "\<lbrakk>test_assn as; test_trm t; set (bn as) \<sharp>* Let as t\<rbrakk> \<Longrightarrow> test_trm (Let as t)" |
|
96 | "test_assn ANil" |
|
97 | "\<lbrakk>test_trm t; test_assn as\<rbrakk> \<Longrightarrow> test_assn (ACons x t as)" |
|
98 |
|
99 declare trm_assn.fv_bn_eqvt[eqvt] |
|
100 equivariance test_trm |
|
101 |
|
102 lemma |
|
103 fixes p::"perm" |
|
104 shows "test_trm (p \<bullet> t)" and "test_assn (p \<bullet> as)" |
|
105 apply(induct t and as arbitrary: p and p rule: trm_assn.inducts) |
|
106 apply(simp) |
|
107 apply(rule test_trm_test_assn.intros) |
|
108 apply(simp) |
|
109 apply(rule test_trm_test_assn.intros) |
|
110 apply(assumption) |
|
111 apply(assumption) |
|
112 apply(simp) |
|
113 apply(rule test_trm_test_assn.intros) |
|
114 apply(assumption) |
|
115 apply(simp add: trm_assn.fresh fresh_star_def) |
|
116 apply(simp) |
|
117 defer |
|
118 apply(simp) |
|
119 apply(rule test_trm_test_assn.intros) |
|
120 apply(simp) |
|
121 apply(rule test_trm_test_assn.intros) |
|
122 apply(assumption) |
|
123 apply(assumption) |
|
124 apply(subgoal_tac "finite (set (bn (p \<bullet> assn)))") |
|
125 apply(subgoal_tac "set (bn (p \<bullet> assn)) \<sharp>* (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm))") |
|
126 apply(drule_tac c="()" in at_set_avoiding2) |
|
127 apply(simp add: supp_Unit) |
|
128 prefer 2 |
|
129 apply(assumption) |
|
130 apply(simp add: finite_supp) |
|
131 apply(erule exE) |
95 apply(erule exE) |
132 apply(erule conjE) |
96 apply(erule conjE) |
133 apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" and |
97 apply(rule assms(3)) |
134 s = "Let (permute_bn pa (p \<bullet> assn)) (pa \<bullet> (p \<bullet> trm))" in subst) |
98 apply(perm_simp) |
135 apply(rule trm_assn.eq_iff(4)[THEN iffD2]) |
99 apply(assumption) |
136 apply(simp add: uu) |
100 apply(rule refl) |
137 apply(drule supp_perm_eq) |
101 apply(drule supp_perm_eq[symmetric]) |
|
102 apply(simp) |
|
103 apply(rule at_set_avoiding2) |
|
104 apply(simp add: finite_supp) |
|
105 apply(simp add: finite_supp) |
|
106 apply(simp add: finite_supp) |
|
107 apply(simp add: trm_assn.fresh fresh_star_def) |
|
108 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* c \<and> supp ([bn assn]lst.trm) \<sharp>* q") |
|
109 apply(erule exE) |
|
110 apply(erule conjE) |
|
111 apply(rule assms(4)) |
|
112 apply(simp add: set_eqvt) |
138 apply(simp add: tt) |
113 apply(simp add: tt) |
139 apply(rule test_trm_test_assn.intros(4)) |
114 apply(rule refl) |
140 defer |
115 apply(simp) |
141 apply(subst permute_plus[symmetric]) |
116 apply(simp add: trm_assn.eq_iff) |
142 apply(blast) |
117 apply(drule supp_perm_eq[symmetric]) |
143 oops |
118 apply(simp) |
144 |
119 apply(simp add: tt uu) |
145 |
120 apply(rule at_set_avoiding2) |
146 (* |
121 apply(simp add: finite_supp) |
|
122 apply(simp add: finite_supp) |
|
123 apply(simp add: finite_supp) |
|
124 apply(simp add: Abs_fresh_star) |
|
125 done |
|
126 |
|
127 |
|
128 lemma strong_exhaust2: |
|
129 assumes "\<And>ca. \<lbrakk>c = ca; as = ANil\<rbrakk> \<Longrightarrow> P" |
|
130 and "\<And>x t assn ca. \<lbrakk>c = ca; as = ACons x t assn\<rbrakk> \<Longrightarrow> P" |
|
131 shows "P" |
|
132 apply(rule_tac y="as" in trm_assn.exhaust(2)) |
|
133 apply(rule assms(1)) |
|
134 apply(auto)[2] |
|
135 apply(rule assms(2)) |
|
136 apply(auto)[2] |
|
137 done |
|
138 |
|
139 |
147 lemma |
140 lemma |
148 fixes t::trm |
141 fixes t::trm |
149 and as::assn |
142 and as::assn |
150 and c::"'a::fs" |
143 and c::"'a::fs" |
151 assumes a1: "\<And>x c. P1 c (Var x)" |
144 assumes a1: "\<And>x c. P1 c (Var x)" |
152 and a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)" |
145 and a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)" |
153 and a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)" |
146 and a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)" |
154 and a4: "\<And>as t c. \<lbrakk>set (bn as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let as t)" |
147 and a4: "\<And>as t c. \<lbrakk>set (bn as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let as t)" |
155 and a5: "\<And>c. P2 c ANil" |
148 and a5: "\<And>c. P2 c ANil" |
156 and a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)" |
149 and a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)" |
157 shows "P1 c t" and "P2 c as" |
150 shows "P1 c t" "P2 c as" |
|
151 using assms |
|
152 apply(induction_schema) |
|
153 apply(rule_tac y="t" in strong_exhaust1) |
|
154 apply(blast) |
|
155 apply(blast) |
|
156 apply(blast) |
|
157 apply(blast) |
|
158 apply(rule_tac as="as" in strong_exhaust2) |
|
159 apply(blast) |
|
160 apply(blast) |
|
161 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))") |
|
162 apply(auto)[1] |
|
163 apply(simp_all add: trm_assn.size)[7] |
|
164 done |
|
165 |
|
166 text {* *} |
|
167 |
|
168 |
|
169 (* |
158 proof - |
170 proof - |
159 have x: "\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t)" |
171 have x: "\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t)" |
160 and y: "\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> as)" |
172 and y: "\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> as)" |
161 apply(induct rule: trm_assn.inducts) |
173 apply(induct rule: trm_assn.inducts) |
162 apply(simp) |
174 apply(simp) |