75 in |
77 in |
76 list_params_prems_concl params (fresh_prem @ prems) concl |
78 list_params_prems_concl params (fresh_prem @ prems) concl |
77 end |
79 end |
78 *} |
80 *} |
79 |
81 |
80 ML {* |
82 |
81 fun fresh_thm ctxt c params binders bn_finite_thms = |
83 ML {* |
|
84 fun fresh_thm ctxt c parms binders bn_finite_thms = |
82 let |
85 let |
83 fun prep_binder (opt, i) = |
86 fun prep_binder (opt, i) = |
84 case opt of |
87 case opt of |
85 NONE => setify ctxt (nth params i) |
88 NONE => setify ctxt (nth parms i) |
86 | SOME bn => to_set (bn $ (nth params i)) |
89 | SOME bn => to_set (bn $ (nth parms i)) |
87 |
90 |
88 val rhs = HOLogic.mk_tuple (c :: params) |
91 fun prep_binder2 (opt, i) = |
|
92 case opt of |
|
93 NONE => atomify ctxt (nth parms i) |
|
94 | SOME bn => bn $ (nth parms i) |
|
95 |
|
96 val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders)) |
89 val lhs = binders |
97 val lhs = binders |
90 |> map prep_binder |
98 |> map prep_binder |
91 |> fold_union |
99 |> fold_union |
92 |> mk_perm (Bound 0) |
100 |> mk_perm (Bound 0) |
93 |
101 |
94 val goal = mk_fresh_star lhs rhs |
102 val goal = mk_fresh_star lhs rhs |
95 |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t)) |
103 |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t)) |
96 |> HOLogic.mk_Trueprop |
104 |> HOLogic.mk_Trueprop |
97 val ss = @{thms finite.emptyI finite.insertI finite_supp supp_Pair finite_Un finite_fset finite_set} |
105 |
98 @ bn_finite_thms |
106 val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} |
|
107 @ @{thms finite.intros finite_Un finite_set finite_fset} |
99 in |
108 in |
100 Goal.prove ctxt [] [] goal |
109 Goal.prove ctxt [] [] goal |
101 (K (HEADGOAL (rtac @{thm at_set_avoiding1} |
110 (K (HEADGOAL (rtac @{thm at_set_avoiding1} |
102 THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) |
111 THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) |
103 end |
112 end |
104 *} |
113 |
105 |
114 fun abs_eq_thm ctxt fprops p parms bn_finite_thms (BC (bmode, binders, bodies)) = |
106 |
115 case binders of |
107 ML {* |
116 [] => [] |
108 fun case_tac ctxt c bn_finite_thms binderss thm = |
117 | binders => |
|
118 let |
|
119 val binder_trm = Nominal_Dt_Alpha.comb_binders ctxt bmode parms binders |
|
120 val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) |
|
121 val body_ty = fastype_of body_trm |
|
122 |
|
123 val (abs_name, binder_ty, abs_ty) = |
|
124 case bmode of |
|
125 Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst}) |
|
126 | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set}) |
|
127 | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res}) |
|
128 |
|
129 val abs = Const (abs_name, [binder_ty, body_ty] ---> Type (abs_ty, [body_ty])) |
|
130 val abs_lhs = abs $ binder_trm $ body_trm |
|
131 val abs_rhs = abs $ mk_perm p binder_trm $ Bound 0 |
|
132 val goal = HOLogic.mk_eq (abs_lhs, abs_rhs) |
|
133 |> (fn t => HOLogic.mk_exists ("y", body_ty, t)) |
|
134 |> HOLogic.mk_Trueprop |
|
135 |
|
136 val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt} |
|
137 @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset |
|
138 fresh_star_set} @ @{thms finite.intros finite_fset} |
|
139 in |
|
140 [Goal.prove ctxt [] [] goal |
|
141 (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} |
|
142 THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))] |
|
143 end |
|
144 *} |
|
145 |
|
146 ML {* |
|
147 fun partitions [] [] = [] |
|
148 | partitions xs (i :: js) = |
|
149 let |
|
150 val (head, tail) = chop i xs |
|
151 in |
|
152 head :: partitions tail js |
|
153 end |
|
154 *} |
|
155 |
|
156 |
|
157 ML {* |
|
158 fun mk_cperm ctxt p ctrm = |
|
159 mk_perm (term_of p) (term_of ctrm) |
|
160 |> cterm_of (ProofContext.theory_of ctxt) |
|
161 *} |
|
162 |
|
163 |
|
164 ML {* |
|
165 fun case_tac ctxt c bn_finite_thms (prems, bclausess) thm = |
109 let |
166 let |
110 fun aux_tac (binders : (term option * int) list)= |
167 fun aux_tac prem bclauses = |
111 Subgoal.FOCUS (fn {params, context, ...} => |
168 case (get_all_binders bclauses) of |
112 let |
169 [] => EVERY' [rtac prem, atac] |
113 val prms = map (term_of o snd) params |
170 | binders => Subgoal.FOCUS (fn {params, prems, context = ctxt, ...} => |
114 val fthm = fresh_thm ctxt c prms binders bn_finite_thms |
171 let |
115 val _ = tracing ("params" ^ @{make_string} params) |
172 val parms = map (term_of o snd) params |
116 val _ = tracing ("binders" ^ @{make_string} binders) |
173 val fthm = fresh_thm ctxt c parms binders bn_finite_thms |
117 in |
174 |
118 Skip_Proof.cheat_tac (ProofContext.theory_of ctxt) |
175 val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un} |
119 end) ctxt |
176 val (([(_, fperm)], fprops), ctxt') = Obtain.result |
|
177 (K (EVERY1 [etac exE, |
|
178 full_simp_tac (HOL_basic_ss addsimps ss), |
|
179 REPEAT o (etac conjE)])) [fthm] ctxt |
|
180 (* |
|
181 val _ = tracing ("fprop:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) fprops)) |
|
182 *) |
|
183 val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses) |
|
184 (* |
|
185 val _ = tracing ("abs_eqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) abs_eqs)) |
|
186 *) |
|
187 in |
|
188 (*HEADGOAL (rtac prem THEN' RANGE [K all_tac, simp_tac (HOL_basic_ss addsimps prems)])*) |
|
189 Skip_Proof.cheat_tac (ProofContext.theory_of ctxt') |
|
190 end) ctxt |
120 in |
191 in |
121 rtac thm THEN' RANGE (map aux_tac binderss) |
192 rtac thm THEN' RANGE (map2 aux_tac prems bclausess) |
122 end |
193 end |
123 |
194 *} |
|
195 |
|
196 |
|
197 ML {* |
124 fun prove_strong_exhausts lthy qexhausts qtrms bclausesss bn_finite_thms = |
198 fun prove_strong_exhausts lthy qexhausts qtrms bclausesss bn_finite_thms = |
125 let |
199 let |
126 val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy |
200 val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy |
127 |
201 |
128 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
202 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
129 val c = Free (c, TFree (a, @{sort fs})) |
203 val c = Free (c, TFree (a, @{sort fs})) |
130 |
|
131 val binderss = map (map get_all_binders) bclausesss |
|
132 |
204 |
133 val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *) |
205 val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *) |
134 |> map prop_of |
206 |> map prop_of |
135 |> map Logic.strip_horn |
207 |> map Logic.strip_horn |
136 |> split_list |
208 |> split_list |
137 |>> map (map strip_params_prems_concl) |
209 |>> map (map strip_params_prems_concl) |
138 |
210 |
139 val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat binderss) |
211 val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat bclausesss) |
140 |
|
141 val _ = tracing ("binderss: " ^ @{make_string} binderss) |
|
142 in |
212 in |
143 Goal.prove_multi lthy'' [] prems main_concls |
213 Goal.prove_multi lthy'' [] prems main_concls |
144 (fn {prems, context} => |
214 (fn {prems:thm list, context} => |
145 EVERY1 [Goal.conjunction_tac, |
215 let |
146 RANGE (map2 (case_tac context c bn_finite_thms) binderss qexhausts')]) |
216 val prems' = partitions prems (map length bclausesss) |
|
217 in |
|
218 EVERY1 [Goal.conjunction_tac, |
|
219 RANGE (map2 (case_tac context c bn_finite_thms) (prems' ~~ bclausesss) qexhausts')] |
|
220 end) |
147 end |
221 end |
148 *} |
222 *} |
149 |
223 |
150 |
224 |
151 |
225 |