|
1 (* Title: HOL/Tools/BNF/bnf_lfp_countable.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2014 |
|
4 |
|
5 Countability tactic for BNF datatypes. |
|
6 *) |
|
7 |
|
8 signature BNF_LFP_COUNTABLE = |
|
9 sig |
|
10 val derive_encode_injectives_thms: Proof.context -> string list -> thm list |
|
11 val countable_datatype_tac: Proof.context -> tactic |
|
12 end; |
|
13 |
|
14 structure BNF_LFP_Countable : BNF_LFP_COUNTABLE = |
|
15 struct |
|
16 |
|
17 open BNF_FP_Rec_Sugar_Util |
|
18 open BNF_Def |
|
19 open BNF_Util |
|
20 open BNF_Tactics |
|
21 open BNF_FP_Util |
|
22 open BNF_FP_Def_Sugar |
|
23 |
|
24 val countableS = @{sort countable}; |
|
25 |
|
26 fun nchotomy_tac ctxt nchotomy = |
|
27 HEADGOAL (resolve_tac ctxt [nchotomy RS @{thm all_reg[rotated]}] THEN' |
|
28 REPEAT_ALL_NEW (resolve_tac ctxt [allI, impI] ORELSE' eresolve_tac ctxt [exE, disjE])); |
|
29 |
|
30 fun meta_spec_mp_tac ctxt 0 = K all_tac |
|
31 | meta_spec_mp_tac ctxt depth = |
|
32 dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN' |
|
33 dtac ctxt meta_mp THEN' assume_tac ctxt; |
|
34 |
|
35 fun use_induction_hypothesis_tac ctxt = |
|
36 DEEPEN (1, 64 (* large number *)) |
|
37 (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN' |
|
38 assume_tac ctxt THEN' assume_tac ctxt) 0; |
|
39 |
|
40 val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split |
|
41 id_apply snd_conv simp_thms}; |
|
42 val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms}; |
|
43 |
|
44 fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' = |
|
45 HEADGOAL (asm_full_simp_tac |
|
46 (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE' |
|
47 TRY o REPEAT_ALL_NEW (rtac ctxt conjI) THEN_ALL_NEW |
|
48 REPEAT_ALL_NEW (eresolve_tac ctxt (conjE :: inj_map_strongs')) THEN_ALL_NEW |
|
49 (assume_tac ctxt ORELSE' use_induction_hypothesis_tac ctxt)); |
|
50 |
|
51 fun distinct_ctrs_tac ctxt recs = |
|
52 HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt)); |
|
53 |
|
54 fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' = |
|
55 let val ks = 1 upto n in |
|
56 EVERY (maps (fn k => nchotomy_tac ctxt nchotomy :: map (fn k' => |
|
57 if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs' |
|
58 else distinct_ctrs_tac ctxt recs) ks) ks) |
|
59 end; |
|
60 |
|
61 fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' = |
|
62 HEADGOAL (rtac ctxt induct) THEN |
|
63 EVERY (@{map 4} (fn n => fn nchotomy => fn injects => fn recs => |
|
64 mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs') |
|
65 ns nchotomys injectss recss); |
|
66 |
|
67 fun endgame_tac ctxt encode_injectives = |
|
68 unfold_thms_tac ctxt @{thms inj_on_def ball_UNIV} THEN |
|
69 ALLGOALS (rtac ctxt exI THEN' rtac ctxt allI THEN' resolve_tac ctxt encode_injectives); |
|
70 |
|
71 fun encode_sumN n k t = |
|
72 Balanced_Tree.access {init = t, |
|
73 left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t), |
|
74 right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)} |
|
75 n k; |
|
76 |
|
77 fun encode_tuple [] = @{term "0 :: nat"} |
|
78 | encode_tuple ts = |
|
79 Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts; |
|
80 |
|
81 fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 = |
|
82 let |
|
83 val thy = Proof_Context.theory_of ctxt; |
|
84 |
|
85 fun check_countable T = |
|
86 Sign.of_sort thy (T, countableS) orelse |
|
87 raise TYPE ("Type is not of sort " ^ Syntax.string_of_sort ctxt countableS, [T], []); |
|
88 |
|
89 fun mk_to_nat_checked T = |
|
90 Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT); |
|
91 |
|
92 val nn = length ns; |
|
93 val recs as rec1 :: _ = map2 (mk_co_rec thy Least_FP (replicate nn HOLogic.natT)) fpTs recs0; |
|
94 val arg_Ts = binder_fun_types (fastype_of rec1); |
|
95 val arg_Tss = Library.unflat ctrss0 arg_Ts; |
|
96 |
|
97 fun mk_U (Type (@{type_name prod}, [T1, T2])) = |
|
98 if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2) |
|
99 | mk_U (Type (s, Ts)) = Type (s, map mk_U Ts) |
|
100 | mk_U T = T; |
|
101 |
|
102 fun mk_nat (j, T) = |
|
103 if T = HOLogic.natT then |
|
104 SOME (Bound j) |
|
105 else if member (op =) fpTs T then |
|
106 NONE |
|
107 else if exists_subtype_in fpTs T then |
|
108 let val U = mk_U T in |
|
109 SOME (mk_to_nat_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j)) |
|
110 end |
|
111 else |
|
112 SOME (mk_to_nat_checked T $ Bound j); |
|
113 |
|
114 fun mk_arg n (k, arg_T) = |
|
115 let |
|
116 val bound_Ts = rev (binder_types arg_T); |
|
117 val nats = map_filter mk_nat (tag_list 0 bound_Ts); |
|
118 in |
|
119 fold (fn T => fn t => Abs (Name.uu, T, t)) bound_Ts (encode_sumN n k (encode_tuple nats)) |
|
120 end; |
|
121 |
|
122 val argss = map2 (map o mk_arg) ns (map (tag_list 1) arg_Tss); |
|
123 in |
|
124 map (fn recx => Term.list_comb (recx, flat argss)) recs |
|
125 end; |
|
126 |
|
127 fun derive_encode_injectives_thms _ [] = [] |
|
128 | derive_encode_injectives_thms ctxt fpT_names0 = |
|
129 let |
|
130 fun not_datatype s = error (quote s ^ " is not a datatype"); |
|
131 fun not_mutually_recursive ss = error (commas ss ^ " are not mutually recursive datatypes"); |
|
132 |
|
133 fun lfp_sugar_of s = |
|
134 (case fp_sugar_of ctxt s of |
|
135 SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar |
|
136 | _ => not_datatype s); |
|
137 |
|
138 val fpTs0 as Type (_, var_As) :: _ = |
|
139 map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0)))); |
|
140 val fpT_names = map (fst o dest_Type) fpTs0; |
|
141 |
|
142 val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt; |
|
143 val As = |
|
144 map2 (fn s => fn TVar (_, S) => TFree (s, union (op =) countableS S)) |
|
145 As_names var_As; |
|
146 val fpTs = map (fn s => Type (s, As)) fpT_names; |
|
147 |
|
148 val _ = subset (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0; |
|
149 |
|
150 fun mk_conjunct fpT x encode_fun = |
|
151 HOLogic.all_const fpT $ Abs (Name.uu, fpT, |
|
152 HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0), |
|
153 HOLogic.eq_const fpT $ x $ Bound 0)); |
|
154 |
|
155 val fp_sugars as |
|
156 {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ = |
|
157 map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0; |
|
158 val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars; |
|
159 |
|
160 val ctrss0 = map #ctrs ctr_sugars; |
|
161 val ns = map length ctrss0; |
|
162 val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars; |
|
163 val nchotomys = map #nchotomy ctr_sugars; |
|
164 val injectss = map #injects ctr_sugars; |
|
165 val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars; |
|
166 val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs; |
|
167 val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs; |
|
168 |
|
169 val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs; |
|
170 |
|
171 val conjuncts = @{map 3} mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0); |
|
172 val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts); |
|
173 in |
|
174 Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} => |
|
175 mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps' |
|
176 inj_map_strongs') |
|
177 |> HOLogic.conj_elims ctxt |
|
178 |> Proof_Context.export names_ctxt ctxt |
|
179 |> map Thm.close_derivation |
|
180 end; |
|
181 |
|
182 fun get_countable_goal_type_name (@{const Trueprop} $ (Const (@{const_name Ex}, _) |
|
183 $ Abs (_, Type (_, [Type (s, _), _]), Const (@{const_name inj_on}, _) $ Bound 0 |
|
184 $ Const (@{const_name top}, _)))) = s |
|
185 | get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic"; |
|
186 |
|
187 fun core_countable_datatype_tac ctxt st = |
|
188 let val T_names = map get_countable_goal_type_name (Thm.prems_of st) in |
|
189 endgame_tac ctxt (derive_encode_injectives_thms ctxt T_names) st |
|
190 end; |
|
191 |
|
192 fun countable_datatype_tac ctxt = |
|
193 TRY (Class.intro_classes_tac ctxt []) THEN core_countable_datatype_tac ctxt; |
|
194 |
|
195 end; |