72 apply(simp add: atom_eqvt) |
72 apply(simp add: atom_eqvt) |
73 done |
73 done |
74 |
74 |
75 lemma strong_exhaust1: |
75 lemma strong_exhaust1: |
76 fixes c::"'a::fs" |
76 fixes c::"'a::fs" |
77 assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P" |
77 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
78 and "\<And>trm1 trm2 ca. \<lbrakk>c = ca; y = App trm1 trm2\<rbrakk> \<Longrightarrow> P" |
78 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
79 and "\<And>name trm ca. \<lbrakk>{atom name} \<sharp>* ca; c = ca; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
79 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
80 and "\<And>assn trm ca. \<lbrakk>set (bn assn) \<sharp>* ca; c = ca; y = Let assn trm\<rbrakk> \<Longrightarrow> P" |
80 and "\<And>assn trm. \<lbrakk>set (bn assn) \<sharp>* c; y = Let assn trm\<rbrakk> \<Longrightarrow> P" |
81 shows "P" |
81 shows "P" |
82 apply(rule_tac y="y" in trm_assn.exhaust(1)) |
82 apply(rule_tac y="y" in trm_assn.exhaust(1)) |
83 apply(rule assms(1)) |
83 apply(rule assms(1)) |
84 apply(auto)[2] |
84 apply(assumption) |
85 apply(rule assms(2)) |
85 apply(rule assms(2)) |
86 apply(auto)[2] |
86 apply(assumption) |
87 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
87 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
88 apply(erule exE) |
88 apply(erule exE) |
89 apply(erule conjE) |
89 apply(erule conjE) |
90 apply(rule assms(3)) |
90 apply(rule assms(3)) |
91 apply(perm_simp) |
91 apply(perm_simp) |
92 apply(assumption) |
92 apply(assumption) |
93 apply(rule refl) |
|
94 apply(drule supp_perm_eq[symmetric]) |
93 apply(drule supp_perm_eq[symmetric]) |
95 apply(simp) |
94 apply(simp) |
96 apply(rule at_set_avoiding2) |
95 apply(rule at_set_avoiding2) |
97 apply(simp add: finite_supp) |
96 apply(simp add: finite_supp) |
98 apply(simp add: finite_supp) |
97 apply(simp add: finite_supp) |
99 apply(simp add: finite_supp) |
98 apply(simp add: finite_supp) |
100 apply(simp add: trm_assn.fresh fresh_star_def) |
99 apply(simp add: trm_assn.fresh fresh_star_def) |
101 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* c \<and> supp ([bn assn]lst.trm) \<sharp>* q") |
100 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q") |
102 apply(erule exE) |
101 apply(erule exE) |
103 apply(erule conjE) |
102 apply(erule conjE) |
104 apply(rule assms(4)) |
103 apply(rule_tac assms(4)) |
105 apply(simp add: set_eqvt) |
104 apply(simp add: set_eqvt) |
106 apply(simp add: tt) |
105 apply(simp add: tt) |
107 apply(rule refl) |
|
108 apply(simp) |
106 apply(simp) |
109 apply(simp add: trm_assn.eq_iff) |
107 apply(simp add: trm_assn.eq_iff) |
110 apply(drule supp_perm_eq[symmetric]) |
108 apply(drule supp_perm_eq[symmetric]) |
111 apply(simp) |
109 apply(simp) |
112 apply(simp add: tt uu) |
110 apply(simp add: tt uu) |
117 apply(simp add: Abs_fresh_star) |
115 apply(simp add: Abs_fresh_star) |
118 done |
116 done |
119 |
117 |
120 |
118 |
121 lemma strong_exhaust2: |
119 lemma strong_exhaust2: |
122 assumes "\<And>ca. \<lbrakk>c = ca; as = ANil\<rbrakk> \<Longrightarrow> P" |
120 assumes "as = ANil \<Longrightarrow> P" |
123 and "\<And>x t assn ca. \<lbrakk>c = ca; as = ACons x t assn\<rbrakk> \<Longrightarrow> P" |
121 and "\<And>x t assn. \<lbrakk>as = ACons x t assn\<rbrakk> \<Longrightarrow> P" |
124 shows "P" |
122 shows "P" |
125 apply(rule_tac y="as" in trm_assn.exhaust(2)) |
123 apply(rule_tac y="as" in trm_assn.exhaust(2)) |
126 apply(rule assms(1)) |
124 apply(rule assms(1)) |
127 apply(auto)[2] |
125 apply(assumption) |
128 apply(rule assms(2)) |
126 apply(rule assms(2)) |
129 apply(auto)[2] |
127 apply(assumption)+ |
130 done |
128 done |
131 |
129 |
132 |
130 |
133 lemma |
131 lemma |
134 fixes t::trm |
132 fixes t::trm |