10 val prove_supports: Proof.context -> thm list -> term list -> thm list |
10 val prove_supports: Proof.context -> thm list -> term list -> thm list |
11 val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list |
11 val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list |
12 |
12 |
13 val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> |
13 val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> |
14 local_theory -> local_theory |
14 local_theory -> local_theory |
|
15 |
|
16 val prove_fv_supp: typ list -> term list -> term list -> term list -> thm list -> thm list -> |
|
17 thm list -> thm list -> thm list -> thm list -> bclause list list -> Proof.context -> thm list |
15 end |
18 end |
16 |
19 |
17 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
20 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
18 struct |
21 struct |
19 |
22 |
|
23 fun lookup xs x = the (AList.lookup (op=) xs x) |
20 |
24 |
21 (* supports lemmas for constructors *) |
25 (* supports lemmas for constructors *) |
22 |
26 |
23 fun mk_supports_goal ctxt qtrm = |
27 fun mk_supports_goal ctxt qtrm = |
24 let |
28 let |
25 val vs = fresh_args ctxt qtrm |
29 val vs = fresh_args ctxt qtrm |
26 val rhs = list_comb (qtrm, vs) |
30 val rhs = list_comb (qtrm, vs) |
27 val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"} |
31 val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"} |
28 |> mk_supp |
32 |> mk_supp |
29 in |
33 in |
30 mk_supports lhs rhs |
34 mk_supports lhs rhs |
31 |> HOLogic.mk_Trueprop |
35 |> HOLogic.mk_Trueprop |
32 end |
36 end |
33 |
37 |
34 fun supports_tac ctxt perm_simps = |
38 fun supports_tac ctxt perm_simps = |
35 let |
39 let |
36 val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} |
40 val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} |
37 val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} |
41 val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} |
38 in |
42 in |
39 EVERY' [ simp_tac ss1, |
43 EVERY' [ simp_tac ss1, |
40 Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], |
44 Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], |
41 simp_tac ss2 ] |
45 simp_tac ss2 ] |
42 end |
46 end |
43 |
47 |
44 fun prove_supports_single ctxt perm_simps qtrm = |
48 fun prove_supports_single ctxt perm_simps qtrm = |
45 let |
49 let |
46 val goal = mk_supports_goal ctxt qtrm |
50 val goal = mk_supports_goal ctxt qtrm |
47 val ctxt' = Variable.auto_fixes goal ctxt |
51 val ctxt' = Variable.auto_fixes goal ctxt |
48 in |
52 in |
49 Goal.prove ctxt' [] [] goal |
53 Goal.prove ctxt' [] [] goal |
50 (K (HEADGOAL (supports_tac ctxt perm_simps))) |
54 (K (HEADGOAL (supports_tac ctxt perm_simps))) |
51 |> singleton (ProofContext.export ctxt' ctxt) |
55 |> singleton (ProofContext.export ctxt' ctxt) |
52 end |
56 end |
53 |
57 |
54 fun prove_supports ctxt perm_simps qtrms = |
58 fun prove_supports ctxt perm_simps qtrms = |
55 map (prove_supports_single ctxt perm_simps) qtrms |
59 map (prove_supports_single ctxt perm_simps) qtrms |
56 |
60 |
57 |
61 |
58 (* finite supp lemmas for qtypes *) |
62 (* finite supp lemmas for qtypes *) |
59 |
63 |
60 fun prove_fsupp ctxt qtys qinduct qsupports_thms = |
64 fun prove_fsupp ctxt qtys qinduct qsupports_thms = |
61 let |
65 let |
62 val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt |
66 val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt |
63 val goals = vs ~~ qtys |
67 val goals = vs ~~ qtys |
64 |> map Free |
68 |> map Free |
65 |> map (mk_finite o mk_supp) |
69 |> map (mk_finite o mk_supp) |
66 |> foldr1 (HOLogic.mk_conj) |
70 |> foldr1 (HOLogic.mk_conj) |
67 |> HOLogic.mk_Trueprop |
71 |> HOLogic.mk_Trueprop |
68 |
72 |
69 val tac = |
73 val tac = |
70 EVERY' [ rtac @{thm supports_finite}, |
74 EVERY' [ rtac @{thm supports_finite}, |
71 resolve_tac qsupports_thms, |
75 resolve_tac qsupports_thms, |
72 asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] |
76 asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] |
73 in |
77 in |
74 Goal.prove ctxt' [] [] goals |
78 Goal.prove ctxt' [] [] goals |
75 (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) |
79 (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) |
76 |> singleton (ProofContext.export ctxt' ctxt) |
80 |> singleton (ProofContext.export ctxt' ctxt) |
77 |> Datatype_Aux.split_conj_thm |
81 |> Datatype_Aux.split_conj_thm |
78 |> map zero_var_indexes |
82 |> map zero_var_indexes |
79 end |
83 end |
80 |
84 |
81 |
85 |
82 (* finite supp instances *) |
86 (* finite supp instances *) |
83 |
87 |
84 fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy = |
88 fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy = |
85 let |
89 let |
86 val lthy1 = |
90 val lthy1 = |
87 lthy |
91 lthy |
88 |> Local_Theory.exit_global |
92 |> Local_Theory.exit_global |
89 |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) |
93 |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) |
90 |
94 |
91 fun tac _ = |
95 fun tac _ = |
92 Class.intro_classes_tac [] THEN |
96 Class.intro_classes_tac [] THEN |
93 (ALLGOALS (resolve_tac qfsupp_thms)) |
97 (ALLGOALS (resolve_tac qfsupp_thms)) |
94 in |
98 in |
95 lthy1 |
99 lthy1 |
96 |> Class.prove_instantiation_exit tac |
100 |> Class.prove_instantiation_exit tac |
97 |> Named_Target.theory_init |
101 |> Named_Target.theory_init |
98 end |
102 end |
|
103 |
|
104 |
|
105 (* proves that fv and fv_bn equals supp *) |
|
106 |
|
107 fun mk_fvs_goals ty_arg_map fv = |
|
108 let |
|
109 val arg = fastype_of fv |
|
110 |> domain_type |
|
111 |> lookup ty_arg_map |
|
112 in |
|
113 (fv $ arg, mk_supp arg) |
|
114 |> HOLogic.mk_eq |
|
115 |> HOLogic.mk_Trueprop |
|
116 end |
|
117 |
|
118 fun mk_fv_bns_goals ty_arg_map fv_bn alpha_bn = |
|
119 let |
|
120 val arg = fastype_of fv_bn |
|
121 |> domain_type |
|
122 |> lookup ty_arg_map |
|
123 in |
|
124 (fv_bn $ arg, mk_supp_rel alpha_bn arg) |
|
125 |> HOLogic.mk_eq |
|
126 |> HOLogic.mk_Trueprop |
|
127 end |
|
128 |
|
129 fun add_ss thms = |
|
130 HOL_basic_ss addsimps thms |
|
131 |
|
132 fun symmetric thms = |
|
133 map (fn thm => thm RS @{thm sym}) thms |
|
134 |
|
135 val supp_abs_set = @{thms supp_abs(1)[symmetric]} |
|
136 val supp_abs_res = @{thms supp_abs(2)[symmetric]} |
|
137 val supp_abs_lst = @{thms supp_abs(3)[symmetric]} |
|
138 |
|
139 fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_set |
|
140 | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_res |
|
141 | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_lst |
|
142 |
|
143 fun mk_supp_abs_tac ctxt [] = [] |
|
144 | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs |
|
145 | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs |
|
146 |
|
147 fun mk_bn_supp_abs_tac thm = |
|
148 (prop_of thm) |
|
149 |> HOLogic.dest_Trueprop |
|
150 |> snd o HOLogic.dest_eq |
|
151 |> fastype_of |
|
152 |> (fn ty => case ty of |
|
153 @{typ "atom set"} => simp_tac (add_ss supp_abs_set) |
|
154 | @{typ "atom list"} => simp_tac (add_ss supp_abs_lst) |
|
155 | _ => raise TERM ("mk_bn_supp_abs_tac", [prop_of thm])) |
|
156 |
|
157 |
|
158 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
|
159 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
|
160 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def |
|
161 prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI} |
|
162 |
|
163 fun ind_tac ctxt qinducts = |
|
164 let |
|
165 fun CASES_TAC_TO_TAC cases_tac st = Seq.map snd (cases_tac st) |
|
166 in |
|
167 DETERM o (CASES_TAC_TO_TAC o (Induct.induct_tac ctxt false [] [] [] (SOME qinducts) [])) |
|
168 end |
|
169 |
|
170 fun p_tac msg i = |
|
171 if false then print_tac ("ptest: " ^ msg) else all_tac |
|
172 |
|
173 fun q_tac msg i = |
|
174 if true then print_tac ("qtest: " ^ msg) else all_tac |
|
175 |
|
176 fun prove_fv_supp qtys fvs fv_bns alpha_bns bn_simps fv_simps eq_iffs perm_simps |
|
177 fv_bn_eqvts qinducts bclausess ctxt = |
|
178 let |
|
179 val (arg_names, ctxt') = |
|
180 Variable.variant_fixes (replicate (length qtys) "x") ctxt |
|
181 val args = map2 (curry Free) arg_names qtys |
|
182 val ty_arg_map = qtys ~~ args |
|
183 val ind_args = map SOME arg_names |
|
184 |
|
185 val goals1 = map (mk_fvs_goals ty_arg_map) fvs |
|
186 val goals2 = map2 (mk_fv_bns_goals ty_arg_map) fv_bns alpha_bns |
|
187 |
|
188 fun fv_tac ctxt bclauses = |
|
189 SOLVED' (EVERY' [ |
|
190 (fn i => print_tac ("FV Goal: " ^ string_of_int i ^ " with " ^ (@{make_string} bclauses))), |
|
191 TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
|
192 p_tac "A", |
|
193 TRY o EVERY' (mk_supp_abs_tac ctxt bclauses), |
|
194 p_tac "B", |
|
195 TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), |
|
196 p_tac "C", |
|
197 TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], |
|
198 p_tac "D", |
|
199 TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), |
|
200 p_tac "E", |
|
201 TRY o asm_full_simp_tac (add_ss thms3), |
|
202 p_tac "F", |
|
203 TRY o simp_tac (add_ss thms2), |
|
204 p_tac "G", |
|
205 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), |
|
206 p_tac "H", |
|
207 (fn i => print_tac ("finished with FV Goal: " ^ string_of_int i)) |
|
208 ]) |
|
209 |
|
210 fun bn_tac ctxt bn_simp = |
|
211 SOLVED' (EVERY' [ |
|
212 (fn i => print_tac ("BN Goal: " ^ string_of_int i)), |
|
213 TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
|
214 q_tac "A", |
|
215 TRY o mk_bn_supp_abs_tac bn_simp, |
|
216 q_tac "B", |
|
217 TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), |
|
218 q_tac "C", |
|
219 TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], |
|
220 q_tac "D", |
|
221 TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), |
|
222 q_tac "E", |
|
223 TRY o asm_full_simp_tac (add_ss thms3), |
|
224 q_tac "F", |
|
225 TRY o simp_tac (add_ss thms2), |
|
226 q_tac "G", |
|
227 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts))), |
|
228 (fn i => print_tac ("finished with BN Goal: " ^ string_of_int i)) |
|
229 ]) |
|
230 |
|
231 fun fv_tacs ctxt = map (fv_tac ctxt) bclausess |
|
232 fun bn_tacs ctxt = map (bn_tac ctxt) bn_simps |
|
233 |
|
234 in |
|
235 Goal.prove_multi ctxt' [] [] (goals1 @ goals2) |
|
236 (fn {context as ctxt, ...} => HEADGOAL |
|
237 (ind_tac ctxt qinducts THEN' RANGE (fv_tacs ctxt @ bn_tacs ctxt))) |
|
238 |> ProofContext.export ctxt' ctxt |
|
239 end |
|
240 |
99 |
241 |
100 |
242 |
101 end (* structure *) |
243 end (* structure *) |
102 |
244 |