42 fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1 |
42 fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1 |
43 | mk_union_env tys (@{term "{}::atom set"}, t2) = t2 |
43 | mk_union_env tys (@{term "{}::atom set"}, t2) = t2 |
44 | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1 |
44 | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1 |
45 | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2 |
45 | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2 |
46 | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2) |
46 | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2) |
47 *} |
47 |
48 |
|
49 ML {* |
|
50 fun fold_left f [] z = z |
48 fun fold_left f [] z = z |
51 | fold_left f [x] z = x |
49 | fold_left f [x] z = x |
52 | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z |
50 | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z |
53 *} |
51 |
54 |
|
55 ML {* |
|
56 fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} |
52 fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} |
57 *} |
53 *} |
58 |
54 |
59 ML {* |
|
60 fold_union_env [] [@{term "t1::atom set"}, @{term "t2::atom set"}, @{term "t3::atom set"}] |
|
61 |> Syntax.string_of_term @{context} |
|
62 |> writeln |
|
63 *} |
|
64 |
55 |
65 |
56 |
66 ML {* |
57 ML {* |
67 (* adds a freshness condition to the assumptions *) |
58 (* adds a freshness condition to the assumptions *) |
68 fun mk_ecase_prems lthy c (params, prems, concl) bclauses = |
59 fun mk_ecase_prems lthy c (params, prems, concl) bclauses = |
137 (bclause as (BC (bmode, binders, bodies))) = |
128 (bclause as (BC (bmode, binders, bodies))) = |
138 case binders of |
129 case binders of |
139 [] => [] |
130 [] => [] |
140 | _ => |
131 | _ => |
141 let |
132 let |
|
133 val flag = is_recursive_binder bclause |
142 val binder_trm = comb_binders ctxt bmode parms binders |
134 val binder_trm = comb_binders ctxt bmode parms binders |
143 val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) |
135 val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) |
144 val body_ty = fastype_of body_trm |
136 val body_ty = fastype_of body_trm |
145 |
137 |
146 fun mk_abs cnst_name ty1 ty2 = |
138 fun mk_abs cnst_name ty1 ty2 = |
151 Lst => mk_abs @{const_name "Abs_lst"} @{typ "atom list"} @{type_name abs_lst} |
143 Lst => mk_abs @{const_name "Abs_lst"} @{typ "atom list"} @{type_name abs_lst} |
152 | Set => mk_abs @{const_name "Abs_set"} @{typ "atom set"} @{type_name abs_set} |
144 | Set => mk_abs @{const_name "Abs_set"} @{typ "atom set"} @{type_name abs_set} |
153 | Res => mk_abs @{const_name "Abs_res"} @{typ "atom set"} @{type_name abs_res} |
145 | Res => mk_abs @{const_name "Abs_res"} @{typ "atom set"} @{type_name abs_res} |
154 |
146 |
155 val abs_lhs = abs_const $ binder_trm $ body_trm |
147 val abs_lhs = abs_const $ binder_trm $ body_trm |
156 val abs_rhs = abs_const $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm |
148 val abs_rhs = |
157 val abs_rhs' = abs_const $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm |
149 if flag |
|
150 then abs_const $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm |
|
151 else abs_const $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm |
|
152 |
158 val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) |
153 val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) |
159 val abs_eq' = HOLogic.mk_eq (abs_lhs, abs_rhs') |
154 val peq = 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) |
155 |
161 |
156 val goal = HOLogic.mk_conj (abs_eq, peq) |
162 val goal = HOLogic.mk_conj (abs_eq, eq) |
|
163 |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |
157 |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |
164 |> HOLogic.mk_Trueprop |
158 |> HOLogic.mk_Trueprop |
165 |
|
166 val goal' = HOLogic.mk_conj (abs_eq', eq) |
|
167 |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |
|
168 |> HOLogic.mk_Trueprop |
|
169 |
159 |
170 val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt} |
160 val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt} |
171 @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset |
161 @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset |
172 fresh_star_set} @ @{thms finite.intros finite_fset} |
162 fresh_star_set} @ @{thms finite.intros finite_fset} |
|
163 |
|
164 val tac1 = |
|
165 if flag |
|
166 then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} |
|
167 else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} |
|
168 |
|
169 val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] |
173 in |
170 in |
174 if is_recursive_binder bclause |
171 [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) |
175 then |
172 |> (if flag |
176 (tracing "recursive"; |
173 then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt [] |
177 [ Goal.prove ctxt [] [] goal' |
174 else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) |
178 (K (HEADGOAL (resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} |
175 ] |
179 THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss)))) |
|
180 |> Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt [] |
|
181 ]) |
|
182 else |
|
183 (tracing "non-recursive"; |
|
184 [ Goal.prove ctxt [] [] goal |
|
185 (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} |
|
186 THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss)))) |
|
187 |> Nominal_Permeq.eqvt_strict_rule ctxt permute_bns [] |
|
188 ]) |
|
189 end |
176 end |
190 *} |
177 *} |
191 |
178 |
192 ML {* |
179 ML {* |
193 fun conj_tac tac i = |
180 fun conj_tac tac i = |