60 |
60 |
61 lemma |
61 lemma |
62 fixes c::"'a::fs" |
62 fixes c::"'a::fs" |
63 assumes a1: "\<And>name c. P c (Vr name)" |
63 assumes a1: "\<And>name c. P c (Vr name)" |
64 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
64 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
65 and a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
65 and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
66 shows "P c lm" |
66 shows "P c lm" |
67 proof - |
67 proof - |
68 have "\<And>p. P c (p \<bullet> lm)" |
68 have "\<And>p. P c (p \<bullet> lm)" |
69 apply(induct lm arbitrary: c rule: lm.induct) |
69 apply(induct lm arbitrary: c rule: lm.induct) |
70 apply(simp only: lm.perm) |
70 apply(simp only: lm.perm) |
85 apply(simp only: supp_fn') |
85 apply(simp only: supp_fn') |
86 apply(simp) |
86 apply(simp) |
87 apply(simp add: fresh_Pair) |
87 apply(simp add: fresh_Pair) |
88 apply(simp) |
88 apply(simp) |
89 apply(rule a3) |
89 apply(rule a3) |
|
90 apply(simp add: fresh_Pair) |
90 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
91 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
91 apply(simp) |
92 apply(simp) |
92 apply(simp add: fresh_def) |
93 apply(simp add: fresh_def) |
93 apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base) |
94 apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base) |
94 apply(simp add: supp_Pair finite_supp) |
95 apply(simp add: supp_Pair finite_supp) |
95 apply(blast) |
96 apply(blast) |
96 done |
97 done |
|
98 then have "P c (0 \<bullet> lm)" by blast |
|
99 then show "P c lm" by simp |
|
100 qed |
|
101 |
|
102 |
|
103 lemma |
|
104 fixes c::"'a::fs" |
|
105 assumes a1: "\<And>name c. P c (Vr name)" |
|
106 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
|
107 and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
|
108 shows "P c lm" |
|
109 proof - |
|
110 have "\<And>p. P c (p \<bullet> lm)" |
|
111 apply(induct lm arbitrary: c rule: lm_induct) |
|
112 apply(simp only: lm_perm) |
|
113 apply(rule a1) |
|
114 apply(simp only: lm_perm) |
|
115 apply(rule a2) |
|
116 apply(blast)[1] |
|
117 apply(assumption) |
|
118 thm at_set_avoiding |
|
119 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q") |
|
120 apply(erule exE) |
|
121 apply(rule_tac t="p \<bullet> Lm name lm" and |
|
122 s="q \<bullet> p \<bullet> Lm name lm" in subst) |
|
123 defer |
|
124 apply(simp add: lm_perm) |
|
125 apply(rule a3) |
|
126 apply(simp add: eqvts fresh_star_def) |
|
127 apply(drule_tac x="q + p" in meta_spec) |
|
128 apply(simp) |
|
129 sorry |
97 then have "P c (0 \<bullet> lm)" by blast |
130 then have "P c (0 \<bullet> lm)" by blast |
98 then show "P c lm" by simp |
131 then show "P c lm" by simp |
99 qed |
132 qed |
100 |
133 |
101 |
134 |
416 thm t_tyS.distinct |
449 thm t_tyS.distinct |
417 |
450 |
418 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
451 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} |
419 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *} |
452 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *} |
420 |
453 |
421 lemma supports_subset: |
|
422 fixes S1 S2 :: "atom set" |
|
423 assumes a: "S1 supports x" |
|
424 and b: "S1 \<subseteq> S2" |
|
425 shows "S2 supports x" |
|
426 using a b |
|
427 by (auto simp add: supports_def) |
|
428 |
|
429 lemma finite_fv_t_tyS: |
454 lemma finite_fv_t_tyS: |
430 fixes T::"t" |
455 fixes T::"t" |
431 and S::"tyS" |
456 and S::"tyS" |
432 shows "finite (fv_t T)" |
457 shows "finite (fv_t T)" |
433 and "finite (fv_tyS S)" |
458 and "finite (fv_tyS S)" |