61 |> Syntax.string_of_term @{context} |
61 |> Syntax.string_of_term @{context} |
62 |> writeln |
62 |> writeln |
63 *} |
63 *} |
64 |
64 |
65 |
65 |
66 |
66 ML {* |
67 |
67 (* adds a freshness condition to the assumptions *) |
68 ML {* |
68 fun mk_ecase_prems lthy c (params, prems, concl) bclauses = |
69 fun process_ecase lthy c (params, prems, concl) bclauses = |
|
70 let |
69 let |
71 val tys = map snd params |
70 val tys = map snd params |
72 val binders = get_all_binders bclauses |
71 val binders = get_all_binders bclauses |
73 |
72 |
74 fun prep_binder (opt, i) = |
73 fun prep_binder (opt, i) = |
78 case opt of |
77 case opt of |
79 NONE => setify_ty lthy (nth tys i) t |
78 NONE => setify_ty lthy (nth tys i) t |
80 | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) |
79 | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) |
81 end |
80 end |
82 |
81 |
83 val fresh_prem = |
82 val prems' = |
84 case binders of |
83 case binders of |
85 [] => [] (* case: no binders *) |
84 [] => prems (* case: no binders *) |
86 | _ => binders (* case: binders *) |
85 | _ => binders (* case: binders *) |
87 |> map prep_binder |
86 |> map prep_binder |
88 |> fold_union_env tys |
87 |> fold_union_env tys |
89 |> (fn t => mk_fresh_star t c) |
88 |> (fn t => mk_fresh_star t c) |
90 |> HOLogic.mk_Trueprop |
89 |> (fn t => HOLogic.mk_Trueprop t :: prems) |
91 |> single |
|
92 in |
90 in |
93 list_params_prems_concl params (fresh_prem @ prems) concl |
91 list_params_prems_concl params prems' concl |
94 end |
92 end |
95 *} |
93 *} |
96 |
94 |
97 |
95 |
98 ML {* |
96 ML {* |
128 THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) |
126 THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) |
129 end |
127 end |
130 *} |
128 *} |
131 |
129 |
132 ML {* |
130 ML {* |
133 (* derives abs_eq theorems of the form Exists s. [as].t = [p o as].s *) |
131 (* derives an abs_eq theorem of the form |
|
132 |
|
133 Exists q. [as].x = [p o as].(q o x) for non-recursive binders |
|
134 Exists q. [as].x = [q o as].(q o x) for recursive binders |
|
135 *) |
134 fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns |
136 fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns |
135 (bclause as (BC (bmode, binders, bodies))) = |
137 (bclause as (BC (bmode, binders, bodies))) = |
136 case binders of |
138 case binders of |
137 [] => [] |
139 [] => [] |
138 | _ => |
140 | _ => |
139 let |
141 let |
140 val binder_trm = comb_binders ctxt bmode parms binders |
142 val binder_trm = comb_binders ctxt bmode parms binders |
141 val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) |
143 val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) |
142 val body_ty = fastype_of body_trm |
144 val body_ty = fastype_of body_trm |
143 |
145 |
144 val (abs_name, binder_ty, abs_ty) = |
146 fun mk_abs cnst_name ty1 ty2 = |
|
147 Const (cnst_name, [ty1, body_ty] ---> Type (ty2, [body_ty])) |
|
148 |
|
149 val abs_const = |
145 case bmode of |
150 case bmode of |
146 Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst}) |
151 Lst => mk_abs @{const_name "Abs_lst"} @{typ "atom list"} @{type_name abs_lst} |
147 | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set}) |
152 | Set => mk_abs @{const_name "Abs_set"} @{typ "atom set"} @{type_name abs_set} |
148 | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res}) |
153 | Res => mk_abs @{const_name "Abs_res"} @{typ "atom set"} @{type_name abs_res} |
149 |
154 |
150 val abs = Const (abs_name, [binder_ty, body_ty] ---> Type (abs_ty, [body_ty])) |
155 val abs_lhs = abs_const $ binder_trm $ body_trm |
151 val abs_lhs = abs $ binder_trm $ body_trm |
156 val abs_rhs = abs_const $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm |
152 val abs_rhs = abs $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm |
157 val abs_rhs' = abs_const $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm |
153 val abs_rhs' = abs $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm |
|
154 val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) |
158 val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) |
155 val abs_eq' = HOLogic.mk_eq (abs_lhs, abs_rhs') |
159 val abs_eq' = HOLogic.mk_eq (abs_lhs, abs_rhs') |
156 val eq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) |
160 val eq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) |
157 |
161 |
158 val goal = HOLogic.mk_conj (abs_eq, eq) |
162 val goal = HOLogic.mk_conj (abs_eq, eq) |
308 |> map prop_of |
312 |> map prop_of |
309 |> map Logic.strip_horn |
313 |> map Logic.strip_horn |
310 |> split_list |
314 |> split_list |
311 |>> (map o map) strip_params_prems_concl |
315 |>> (map o map) strip_params_prems_concl |
312 |
316 |
313 val premss = (map2 o map2) (process_ecase lthy'' c) ecases bclausesss |
317 val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases bclausesss |
314 |
318 |
315 fun tac bclausess exhaust {prems, context} = |
319 fun tac bclausess exhaust {prems, context} = |
316 case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas |
320 case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas |
317 prems bclausess exhaust |
321 prems bclausess exhaust |
318 |
322 |