67 |> Pretty.writeln |
69 |> Pretty.writeln |
68 *} |
70 *} |
69 *) |
71 *) |
70 |
72 |
71 |
73 |
72 text {* *} |
74 |
73 |
75 |
74 |
|
75 |
|
76 (* |
|
77 thm at_set_avoiding1[THEN exE] |
|
78 |
|
79 |
|
80 lemma Let1_rename: |
|
81 fixes c::"'a::fs" |
|
82 shows "\<exists>name' trm'. {atom name'} \<sharp>* c \<and> Lam name trm = Lam name' trm'" |
|
83 apply(simp only: foo.eq_iff) |
|
84 apply(rule at_set_avoiding1[where c="(c, atom name, trm)" and xs="set [atom name]", THEN exE]) |
|
85 apply(simp) |
|
86 apply(simp add: finite_supp) |
|
87 apply(perm_simp) |
|
88 apply(rule Abs_rename_list[THEN exE]) |
|
89 apply(simp only: set_eqvt) |
|
90 apply |
|
91 sorry |
|
92 *) |
|
93 |
|
94 thm foo.exhaust |
|
95 |
|
96 ML {* |
|
97 fun strip_prems_concl trm = |
|
98 (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm) |
|
99 *} |
|
100 |
|
101 ML {* |
|
102 @{thms foo.exhaust} |
|
103 |> map prop_of |
|
104 |> map strip_prems_concl |
|
105 |> map fst |
|
106 |> map (map (Syntax.string_of_term @{context})) |
|
107 |> map cat_lines |
|
108 |> cat_lines |
|
109 |> writeln |
|
110 *} |
|
111 |
76 |
112 lemma test6: |
77 lemma test6: |
113 fixes c::"'a::fs" |
78 fixes c::"'a::fs" |
114 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
79 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
115 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
80 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
116 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
81 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
117 and "\<exists>a1 trm1 a2 trm2. ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P" |
82 and "\<And>a1 trm1 a2 trm2. \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P" |
118 and "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P" |
83 and "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P" |
119 shows "P" |
84 shows "P" |
120 apply(rule_tac foo.exhaust(1)) |
85 apply(rule_tac y="y" in foo.exhaust(1)) |
121 apply(rule assms(1)) |
86 apply(rule assms(1)) |
122 apply(rule exI)+ |
|
123 apply(assumption) |
87 apply(assumption) |
124 apply(rule assms(2)) |
88 apply(rule assms(2)) |
125 apply(rule exI)+ |
|
126 apply(assumption) |
89 apply(assumption) |
127 (* lam case *) |
90 (* lam case *) |
128 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)") |
91 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)") |
129 apply(erule exE) |
92 apply(erule exE) |
130 apply(insert Abs_rename_list)[1] |
93 apply(insert Abs_rename_lst)[1] |
131 apply(drule_tac x="p" in meta_spec) |
94 apply(drule_tac x="p" in meta_spec) |
132 apply(drule_tac x="[atom name]" in meta_spec) |
95 apply(drule_tac x="[atom name]" in meta_spec) |
133 apply(drule_tac x="trm" in meta_spec) |
96 apply(drule_tac x="trm" in meta_spec) |
134 apply(simp only: fresh_star_Pair set.simps) |
97 apply(simp only: fresh_star_Pair set.simps) |
135 apply(drule meta_mp) |
98 apply(drule meta_mp) |
148 apply(simp add: finite_supp) |
111 apply(simp add: finite_supp) |
149 (* let1 case *) |
112 (* let1 case *) |
150 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
113 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
151 apply(erule exE) |
114 apply(erule exE) |
152 apply(rule assms(4)) |
115 apply(rule assms(4)) |
|
116 apply(perm_simp add: foo.permute_bn) |
|
117 apply(simp add: fresh_star_Pair) |
|
118 apply(erule conjE)+ |
|
119 apply(assumption) |
|
120 apply(simp only:) |
153 apply(simp only: foo.eq_iff) |
121 apply(simp only: foo.eq_iff) |
154 apply(insert Abs_rename_list)[1] |
122 (* *) |
|
123 apply(insert Abs_rename_lst)[1] |
155 apply(drule_tac x="p" in meta_spec) |
124 apply(drule_tac x="p" in meta_spec) |
156 apply(drule_tac x="bn assg1" in meta_spec) |
125 apply(drule_tac x="bn assg1" in meta_spec) |
157 apply(drule_tac x="trm1" in meta_spec) |
126 apply(drule_tac x="trm1" in meta_spec) |
158 apply(insert Abs_rename_list)[1] |
127 apply(insert Abs_rename_lst)[1] |
159 apply(drule_tac x="p" in meta_spec) |
128 apply(drule_tac x="p" in meta_spec) |
160 apply(drule_tac x="bn assg2" in meta_spec) |
129 apply(drule_tac x="bn assg2" in meta_spec) |
161 apply(drule_tac x="trm2" in meta_spec) |
130 apply(drule_tac x="trm2" in meta_spec) |
162 apply(drule meta_mp) |
131 apply(drule meta_mp) |
163 apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) |
132 apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) |
164 apply(drule meta_mp) |
133 apply(drule meta_mp) |
165 apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) |
134 apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) |
166 apply(erule exE)+ |
135 apply(erule exE)+ |
167 apply(rule exI)+ |
|
168 apply(perm_simp add: foo.permute_bn) |
136 apply(perm_simp add: foo.permute_bn) |
169 apply(rule conjI) |
137 apply(simp add: fresh_star_Pair) |
170 apply(simp add: fresh_star_Pair fresh_star_Un) |
|
171 apply(erule conjE)+ |
138 apply(erule conjE)+ |
172 apply(rule conjI) |
139 apply(rule assms(4)) |
173 apply(assumption) |
140 apply(assumption) |
174 apply(rotate_tac 4) |
141 apply(simp add: foo.eq_iff refl) |
175 apply(assumption) |
142 apply(rule conjI) |
176 apply(rule conjI) |
143 apply(rule refl) |
177 apply(assumption) |
|
178 apply(rule conjI) |
144 apply(rule conjI) |
179 apply(rule foo.perm_bn_alpha) |
145 apply(rule foo.perm_bn_alpha) |
180 apply(rule conjI) |
146 apply(rule conjI) |
181 apply(assumption) |
147 apply(rule refl) |
182 apply(rule foo.perm_bn_alpha) |
148 apply(rule foo.perm_bn_alpha) |
183 apply(rule at_set_avoiding1) |
149 apply(rule at_set_avoiding1) |
184 apply(simp) |
150 apply(simp) |
185 apply(simp add: finite_supp) |
151 apply(simp add: finite_supp) |
186 (* let2 case *) |
152 (* let2 case *) |