45 Plugins_Option of Proof.context -> Plugin_Name.filter |
45 Plugins_Option of Proof.context -> Plugin_Name.filter |
46 | No_Warn_Wits; |
46 | No_Warn_Wits; |
47 |
47 |
48 fun typedef_bnf thm wits specs map_b rel_b opts lthy = |
48 fun typedef_bnf thm wits specs map_b rel_b opts lthy = |
49 let |
49 let |
50 val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) |
50 val plugins = |
|
51 get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) |
51 |> the_default Plugin_Name.default_filter; |
52 |> the_default Plugin_Name.default_filter; |
52 val no_warn_wits = exists (fn No_Warn_Wits => true | _ => false) opts; |
53 val no_warn_wits = exists (fn No_Warn_Wits => true | _ => false) opts; |
53 |
54 |
54 (* extract Rep Abs F RepT AbsT *) |
55 (* extract Rep Abs F RepT AbsT *) |
55 val (_, [Rep_G, Abs_G, F]) = Thm.prop_of thm |
56 val (_, [Rep_G, Abs_G, F]) = Term.strip_comb (HOLogic.dest_Trueprop (Thm.prop_of thm)); |
56 |> HOLogic.dest_Trueprop |
57 val typ_Abs_G = dest_funT (fastype_of Abs_G); |
57 |> Term.strip_comb; |
|
58 val typ_Abs_G = fastype_of Abs_G |> dest_funT; |
|
59 val RepT = fst typ_Abs_G; (* F *) |
58 val RepT = fst typ_Abs_G; (* F *) |
60 val AbsT = snd typ_Abs_G; (* G *) |
59 val AbsT = snd typ_Abs_G; (* G *) |
61 val AbsT_name = fst (dest_Type AbsT); |
60 val AbsT_name = fst (dest_Type AbsT); |
62 val tvs = AbsT |> dest_Type |> snd |> map (fst o dest_TVar); |
61 val tvs = AbsT |> dest_Type |> snd |> map (fst o dest_TVar); |
63 val alpha0s = map (TFree o snd) specs; |
62 val alpha0s = map (TFree o snd) specs; |
70 val Abs_G = subst Abs_G; |
69 val Abs_G = subst Abs_G; |
71 val F = subst F; |
70 val F = subst F; |
72 val RepT = typ_subst RepT; |
71 val RepT = typ_subst RepT; |
73 val AbsT = typ_subst AbsT; |
72 val AbsT = typ_subst AbsT; |
74 |
73 |
75 fun flatten_tyargs Ass = map dest_TFree alpha0s |> |
74 fun flatten_tyargs Ass = |
76 filter (fn T => exists (fn Ts => member (op =) Ts T) Ass); |
75 map dest_TFree alpha0s |
|
76 |> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass); |
77 |
77 |
78 val Ds0 = filter (is_none o fst) specs |> map snd; |
78 val Ds0 = filter (is_none o fst) specs |> map snd; |
79 |
79 |
80 (* get the bnf for RepT *) |
80 (* get the bnf for RepT *) |
81 val ((bnf, (deads, alphas)),((_, unfolds), lthy)) = |
81 val ((bnf, (deads, alphas)),((_, unfolds), lthy)) = |
82 bnf_of_typ Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs [] |
82 bnf_of_typ Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs [] |
83 Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy); |
83 Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy); |
84 |
84 |
85 val set_bs = map (fn T => find_index (fn U => T = U) alpha0s) alphas |
85 val set_bs = |
|
86 map (fn T => find_index (fn U => T = U) alpha0s) alphas |
86 |> map (the_default Binding.empty o fst o nth specs); |
87 |> map (the_default Binding.empty o fst o nth specs); |
87 |
88 |
88 val _ = (case alphas of [] => error "No live variables" | _ => ()); |
89 val _ = (case alphas of [] => error "No live variables" | _ => ()); |
89 |
90 |
90 val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds; |
91 val defs = #map_unfolds unfolds @ flat (#set_unfoldss unfolds) @ #rel_unfolds unfolds; |
119 (replicate (nwits_of_bnf bnf) alphas) bnf; |
120 (replicate (nwits_of_bnf bnf) alphas) bnf; |
120 |
121 |
121 (* val map_closed_F = @{term "\<And>f x. x \<in> F \<Longrightarrow> map_F f x \<in> F"}; *) |
122 (* val map_closed_F = @{term "\<And>f x. x \<in> F \<Longrightarrow> map_F f x \<in> F"}; *) |
122 val (var_fs, names_lthy) = mk_Frees "f" typ_fs names_lthy; |
123 val (var_fs, names_lthy) = mk_Frees "f" typ_fs names_lthy; |
123 val (var_x, names_lthy) = mk_Frees "x" [typ_aF] names_lthy |>> the_single; |
124 val (var_x, names_lthy) = mk_Frees "x" [typ_aF] names_lthy |>> the_single; |
124 val mem_x = HOLogic.mk_mem (var_x, aF_set) |> HOLogic.mk_Trueprop; |
125 val mem_x = HOLogic.mk_Trueprop (HOLogic.mk_mem (var_x, aF_set)); |
125 val map_f = list_comb (map_F, var_fs); |
126 val map_f = list_comb (map_F, var_fs); |
126 val mem_map = HOLogic.mk_mem (map_f $ var_x, bF_set) |> HOLogic.mk_Trueprop; |
127 val mem_map = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_f $ var_x, bF_set)); |
127 val imp_map = Logic.mk_implies (mem_x, mem_map); |
128 val imp_map = Logic.mk_implies (mem_x, mem_map); |
128 val map_closed_F = Library.foldr (Library.uncurry Logic.all) (var_fs, Logic.all var_x imp_map); |
129 val map_closed_F = fold_rev Logic.all var_fs (Logic.all var_x imp_map); |
129 |
130 |
130 (* val zip_closed_F = @{term "\<And>z. map_F fst z \<in> F \<Longrightarrow> map_F snd z \<in> F \<Longrightarrow> z \<in> F"}; *) |
131 (* val zip_closed_F = @{term "\<And>z. map_F fst z \<in> F \<Longrightarrow> map_F snd z \<in> F \<Longrightarrow> z \<in> F"}; *) |
131 val (var_zs, names_lthy) = mk_Frees "z" [typ_pair] names_lthy; |
132 val (var_zs, names_lthy) = mk_Frees "z" [typ_pair] names_lthy; |
132 val (pairs, names_lthy) = mk_Frees "tmp" typ_pairs names_lthy; |
133 val (pairs, names_lthy) = mk_Frees "tmp" typ_pairs names_lthy; |
133 val var_z = hd var_zs; |
134 val var_z = hd var_zs; |
134 val fsts = map (fst o Term.strip_comb o HOLogic.mk_fst) pairs; |
135 val fsts = map (fst o Term.strip_comb o HOLogic.mk_fst) pairs; |
135 val snds = map (fst o Term.strip_comb o HOLogic.mk_snd) pairs; |
136 val snds = map (fst o Term.strip_comb o HOLogic.mk_snd) pairs; |
136 val map_fst = list_comb (list_comb (map_F_fst, fsts), var_zs); |
137 val map_fst = list_comb (list_comb (map_F_fst, fsts), var_zs); |
137 val mem_map_fst = HOLogic.mk_mem (map_fst, aF_set) |> HOLogic.mk_Trueprop; |
138 val mem_map_fst = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_fst, aF_set)); |
138 val map_snd = list_comb (list_comb (map_F_snd, snds), var_zs); |
139 val map_snd = list_comb (list_comb (map_F_snd, snds), var_zs); |
139 val mem_map_snd = HOLogic.mk_mem (map_snd, aF_set') |> HOLogic.mk_Trueprop; |
140 val mem_map_snd = HOLogic.mk_Trueprop (HOLogic.mk_mem (map_snd, aF_set')); |
140 val mem_z = HOLogic.mk_mem (var_z, pairF_set) |> HOLogic.mk_Trueprop; |
141 val mem_z = HOLogic.mk_Trueprop (HOLogic.mk_mem (var_z, pairF_set)); |
141 val imp_zip = Logic.mk_implies (mem_map_fst, Logic.mk_implies (mem_map_snd, mem_z)); |
142 val imp_zip = Logic.mk_implies (mem_map_fst, Logic.mk_implies (mem_map_snd, mem_z)); |
142 val zip_closed_F = Logic.all var_z imp_zip; |
143 val zip_closed_F = Logic.all var_z imp_zip; |
143 |
144 |
144 (* val wit_closed_F = @{term "wit_F a \<in> F"}; *) |
145 (* val wit_closed_F = @{term "wit_F a \<in> F"}; *) |
145 val (var_as, names_lthy) = mk_Frees "a" alphas names_lthy; |
146 val (var_as, names_lthy) = mk_Frees "a" alphas names_lthy; |
149 val wit_closed_Fs = |
150 val wit_closed_Fs = |
150 Iwits |> map (fn (I, wit_F) => |
151 Iwits |> map (fn (I, wit_F) => |
151 let |
152 let |
152 val vars = map (nth var_as) I; |
153 val vars = map (nth var_as) I; |
153 val wit_a = list_comb (wit_F, vars); |
154 val wit_a = list_comb (wit_F, vars); |
154 in |
155 in fold_rev Logic.all vars (HOLogic.mk_Trueprop (HOLogic.mk_mem (wit_a, aF_set))) end); |
155 Library.foldr (Library.uncurry Logic.all) (vars, |
|
156 HOLogic.mk_mem (wit_a, aF_set) |> HOLogic.mk_Trueprop) |
|
157 end); |
|
158 |
156 |
159 val mk_wit_goals = mk_wit_goals var_as var_bs |
157 val mk_wit_goals = mk_wit_goals var_as var_bs |
160 (mk_sets_of_bnf (replicate lives deads) (replicate lives alphas) bnf); |
158 (mk_sets_of_bnf (replicate lives deads) (replicate lives alphas) bnf); |
161 |
159 |
162 val goals = [map_closed_F, zip_closed_F] @ wit_closed_Fs @ |
160 val goals = [map_closed_F, zip_closed_F] @ wit_closed_Fs @ |
185 | _ => chop (length wit_closed_Fs) (map the_single wit_thmss)) |
183 | _ => chop (length wit_closed_Fs) (map the_single wit_thmss)) |
186 |
184 |
187 (* construct map set bd rel wit *) |
185 (* construct map set bd rel wit *) |
188 (* val map_G = @{term "\<lambda>f. Abs_G o map_F f o Rep_G"}; *) |
186 (* val map_G = @{term "\<lambda>f. Abs_G o map_F f o Rep_G"}; *) |
189 val Abs_Gb = subst_b Abs_G; |
187 val Abs_Gb = subst_b Abs_G; |
190 val map_G = Library.foldr (uncurry HOLogic.tupled_lambda) |
188 val map_G = |
191 (var_fs, HOLogic.mk_comp (HOLogic.mk_comp (Abs_Gb, map_f), |
189 fold_rev HOLogic.tupled_lambda var_fs |
192 Rep_G)); |
190 (HOLogic.mk_comp (HOLogic.mk_comp (Abs_Gb, map_f), Rep_G)); |
193 |
191 |
194 (* val sets_G = [@{term "set_F o Rep_G"}]; *) |
192 (* val sets_G = [@{term "set_F o Rep_G"}]; *) |
195 val sets_F = mk_sets_of_bnf (replicate lives deads) (replicate lives alphas) bnf; |
193 val sets_F = mk_sets_of_bnf (replicate lives deads) (replicate lives alphas) bnf; |
196 val sets_G = map (fn set_F => HOLogic.mk_comp (set_F, Rep_G)) sets_F; |
194 val sets_G = map (fn set_F => HOLogic.mk_comp (set_F, Rep_G)) sets_F; |
197 |
195 |
199 val bd_F = mk_bd_of_bnf deads alphas bnf; |
197 val bd_F = mk_bd_of_bnf deads alphas bnf; |
200 val bd_G = bd_F; |
198 val bd_G = bd_F; |
201 |
199 |
202 (* val rel_G = @{term "\<lambda>R. BNF_Def.vimage2p Rep_G Rep_G (rel_F R)"}; *) |
200 (* val rel_G = @{term "\<lambda>R. BNF_Def.vimage2p Rep_G Rep_G (rel_F R)"}; *) |
203 val rel_F = mk_rel_of_bnf deads alphas betas bnf; |
201 val rel_F = mk_rel_of_bnf deads alphas betas bnf; |
204 val (typ_Rs, _) = fastype_of rel_F |> strip_typeN lives; |
202 val (typ_Rs, _) = strip_typeN lives (fastype_of rel_F); |
205 |
203 |
206 val (var_Rs, names_lthy) = mk_Frees "R" typ_Rs lthy; |
204 val (var_Rs, names_lthy) = mk_Frees "R" typ_Rs lthy; |
207 val Rep_Gb = subst_b Rep_G; |
205 val Rep_Gb = subst_b Rep_G; |
208 val rel_G = fold_rev absfree (map dest_Free var_Rs) |
206 val rel_G = fold_rev absfree (map dest_Free var_Rs) |
209 (mk_vimage2p Rep_G Rep_Gb $ list_comb (rel_F, var_Rs)); |
207 (mk_vimage2p Rep_G Rep_Gb $ list_comb (rel_F, var_Rs)); |