equal
deleted
inserted
replaced
54 |
54 |
55 (* |
55 (* |
56 lemma strong_induct: |
56 lemma strong_induct: |
57 assumes a1: "\<And>name b. P b (Var name)" |
57 assumes a1: "\<And>name b. P b (Var name)" |
58 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
58 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
59 and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)" |
59 and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)" |
60 shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts " |
60 shows "P (a :: 'a :: pt) t \<and> P' (d :: 'b :: {fs}) ts " |
61 proof - |
61 proof - |
62 have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))" |
62 have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))" |
63 apply (rule ty_tys.induct) |
63 apply (rule ty_tys.induct) |
64 apply (simp add: a1) |
64 apply (simp add: a1) |
67 apply (rule a2) |
67 apply (rule a2) |
68 apply simp |
68 apply simp |
69 apply simp |
69 apply simp |
70 apply (rule allI) |
70 apply (rule allI) |
71 apply (rule allI) |
71 apply (rule allI) |
72 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset ty) \<sharp>* pa)") |
72 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset ty) \<sharp>* pa)") |
73 apply clarify |
73 apply clarify |
74 apply(rule_tac t="p \<bullet> All fset ty" and |
74 apply(rule_tac t="p \<bullet> All fset ty" and |
75 s="pa \<bullet> (p \<bullet> All fset ty)" in subst) |
75 s="pa \<bullet> (p \<bullet> All fset ty)" in subst) |
76 apply (rule supp_perm_eq) |
76 apply (rule supp_perm_eq) |
77 apply assumption |
77 apply assumption |
79 apply (rule a3) |
79 apply (rule a3) |
80 apply(erule_tac x="(pa + p)" in allE) |
80 apply(erule_tac x="(pa + p)" in allE) |
81 apply simp |
81 apply simp |
82 apply (simp add: eqvts eqvts_raw) |
82 apply (simp add: eqvts eqvts_raw) |
83 apply (rule at_set_avoiding2) |
83 apply (rule at_set_avoiding2) |
84 apply (simp add: fin_fset_to_set) |
84 apply (simp add: fin_fset) |
85 apply (simp add: finite_supp) |
85 apply (simp add: finite_supp) |
86 apply (simp add: eqvts finite_supp) |
86 apply (simp add: eqvts finite_supp) |
87 apply (rule_tac p=" -p" in permute_boolE) |
87 apply (rule_tac p=" -p" in permute_boolE) |
88 apply(simp add: eqvts) |
88 apply(simp add: eqvts) |
89 apply(simp add: permute_fun_def atom_eqvt) |
89 apply(simp add: permute_fun_def atom_eqvt) |
140 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
140 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
141 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
141 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
142 assumes |
142 assumes |
143 s1: "subst \<theta> (Var n) = lookup \<theta> n" |
143 s1: "subst \<theta> (Var n) = lookup \<theta> n" |
144 and s2: "subst \<theta> (Fun l r) = Fun (subst \<theta> l) (subst \<theta> r)" |
144 and s2: "subst \<theta> (Fun l r) = Fun (subst \<theta> l) (subst \<theta> r)" |
145 and s3: "fset_to_set (fmap atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)" |
145 and s3: "fset (fmap atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)" |
146 begin |
146 begin |
147 |
147 |
148 lemma subst_ty: |
148 lemma subst_ty: |
149 assumes x: "atom x \<sharp> t" |
149 assumes x: "atom x \<sharp> t" |
150 shows "subst [(x, S)] t = t" |
150 shows "subst [(x, S)] t = t" |
161 apply (simp add: fresh_star_def fresh_Cons fresh_Nil) |
161 apply (simp add: fresh_star_def fresh_Cons fresh_Nil) |
162 apply (subst subst_ty) |
162 apply (subst subst_ty) |
163 apply (simp_all add: fresh_star_prod_elim) |
163 apply (simp_all add: fresh_star_prod_elim) |
164 apply (drule fresh_star_atom) |
164 apply (drule fresh_star_atom) |
165 apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp]) |
165 apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp]) |
166 apply (subgoal_tac "atom a \<notin> fset_to_set (fmap atom fset)") |
166 apply (subgoal_tac "atom a \<notin> fset (fmap atom fset)") |
167 apply blast |
167 apply blast |
168 apply (metis supp_finite_atom_set finite_fset) |
168 apply (metis supp_finite_atom_set finite_fset) |
169 done |
169 done |
170 |
170 |
171 lemma subst_lemma_pre: |
171 lemma subst_lemma_pre: |
195 apply blast |
195 apply blast |
196 apply (subgoal_tac "atom a \<notin> supp t") |
196 apply (subgoal_tac "atom a \<notin> supp t") |
197 apply (fold fresh_def)[1] |
197 apply (fold fresh_def)[1] |
198 apply (rule mp[OF subst_lemma_pre]) |
198 apply (rule mp[OF subst_lemma_pre]) |
199 apply (simp add: fresh_Pair) |
199 apply (simp add: fresh_Pair) |
200 apply (subgoal_tac "atom a \<notin> (fset_to_set (fmap atom fset))") |
200 apply (subgoal_tac "atom a \<notin> (fset (fmap atom fset))") |
201 apply blast |
201 apply blast |
202 apply (metis supp_finite_atom_set finite_fset) |
202 apply (metis supp_finite_atom_set finite_fset) |
203 done |
203 done |
204 |
204 |
205 lemma subst_lemma: |
205 lemma subst_lemma: |