1 (* Title: nominal_dt_alpha.ML |
|
2 Author: Christian Urban |
|
3 Author: Cezary Kaliszyk |
|
4 |
|
5 Deriving support propoerties for the quotient types. |
|
6 *) |
|
7 |
|
8 signature NOMINAL_DT_SUPP = |
|
9 sig |
|
10 |
|
11 end |
|
12 |
|
13 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP = |
|
14 struct |
|
15 |
|
16 (* supports lemmas for constructors *) |
|
17 |
|
18 fun mk_supports_goal ctxt qtrm = |
|
19 let |
|
20 val vs = fresh_args ctxt qtrm |
|
21 val rhs = list_comb (qtrm, vs) |
|
22 val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"} |
|
23 |> mk_supp |
|
24 in |
|
25 mk_supports lhs rhs |
|
26 |> HOLogic.mk_Trueprop |
|
27 end |
|
28 |
|
29 fun supports_tac ctxt perm_simps = |
|
30 let |
|
31 val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} |
|
32 val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} |
|
33 in |
|
34 EVERY' [ simp_tac ss1, |
|
35 Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], |
|
36 simp_tac ss2 ] |
|
37 end |
|
38 |
|
39 fun prove_supports_single ctxt perm_simps qtrm = |
|
40 let |
|
41 val goal = mk_supports_goal ctxt qtrm |
|
42 val ctxt' = Variable.auto_fixes goal ctxt |
|
43 in |
|
44 Goal.prove ctxt' [] [] goal |
|
45 (K (HEADGOAL (supports_tac ctxt perm_simps))) |
|
46 |> singleton (ProofContext.export ctxt' ctxt) |
|
47 end |
|
48 |
|
49 fun prove_supports ctxt perm_simps qtrms = |
|
50 map (prove_supports_single ctxt perm_simps) qtrms |
|
51 |
|
52 |
|
53 (* finite supp lemmas for qtypes *) |
|
54 |
|
55 fun prove_fsupp ctxt qtys qinduct qsupports_thms = |
|
56 let |
|
57 val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt |
|
58 val goals = vs ~~ qtys |
|
59 |> map Free |
|
60 |> map (mk_finite o mk_supp) |
|
61 |> foldr1 (HOLogic.mk_conj) |
|
62 |> HOLogic.mk_Trueprop |
|
63 |
|
64 val tac = |
|
65 EVERY' [ rtac @{thm supports_finite}, |
|
66 resolve_tac qsupports_thms, |
|
67 asm_simp_tac (HOL_ss addsimps @{thms finite_supp supp_Pair finite_Un}) ] |
|
68 in |
|
69 Goal.prove ctxt' [] [] goals |
|
70 (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac))) |
|
71 |> singleton (ProofContext.export ctxt' ctxt) |
|
72 |> Datatype_Aux.split_conj_thm |
|
73 |> map zero_var_indexes |
|
74 end |
|
75 |
|
76 |
|
77 (* finite supp instances *) |
|
78 |
|
79 fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy = |
|
80 let |
|
81 val lthy1 = |
|
82 lthy |
|
83 |> Local_Theory.exit_global |
|
84 |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) |
|
85 |
|
86 fun tac _ = |
|
87 Class.intro_classes_tac [] THEN |
|
88 (ALLGOALS (resolve_tac qfsupp_thms)) |
|
89 in |
|
90 lthy1 |
|
91 |> Class.prove_instantiation_exit tac |
|
92 |> Named_Target.theory_init |
|
93 end |
|
94 |
|
95 |
|
96 (* proves that fv and fv_bn equals supp *) |
|
97 |
|
98 fun gen_mk_goals fv supp = |
|
99 let |
|
100 val arg_ty = |
|
101 fastype_of fv |
|
102 |> domain_type |
|
103 in |
|
104 (arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x)) |
|
105 end |
|
106 |
|
107 fun mk_fvs_goals fv = gen_mk_goals fv mk_supp |
|
108 fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn) |
|
109 |
|
110 fun add_ss thms = |
|
111 HOL_basic_ss addsimps thms |
|
112 |
|
113 fun symmetric thms = |
|
114 map (fn thm => thm RS @{thm sym}) thms |
|
115 |
|
116 val supp_Abs_set = @{thms supp_Abs(1)[symmetric]} |
|
117 val supp_Abs_res = @{thms supp_Abs(2)[symmetric]} |
|
118 val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]} |
|
119 |
|
120 fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set |
|
121 | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res |
|
122 | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst |
|
123 |
|
124 fun mk_supp_abs_tac ctxt [] = [] |
|
125 | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs |
|
126 | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs |
|
127 |
|
128 fun mk_bn_supp_abs_tac trm = |
|
129 trm |
|
130 |> fastype_of |
|
131 |> body_type |
|
132 |> (fn ty => case ty of |
|
133 @{typ "atom set"} => simp_tac (add_ss supp_Abs_set) |
|
134 | @{typ "atom list"} => simp_tac (add_ss supp_Abs_lst) |
|
135 | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) |
|
136 |
|
137 |
|
138 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
|
139 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
|
140 val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def |
|
141 prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} |
|
142 |
|
143 fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps |
|
144 fv_bn_eqvts qinduct bclausess ctxt = |
|
145 let |
|
146 val goals1 = map mk_fvs_goals fvs |
|
147 val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns |
|
148 |
|
149 fun tac ctxt = |
|
150 SUBGOAL (fn (goal, i) => |
|
151 let |
|
152 val (fv_fun, arg) = |
|
153 goal |> Envir.eta_contract |
|
154 |> Logic.strip_assums_concl |
|
155 |> HOLogic.dest_Trueprop |
|
156 |> fst o HOLogic.dest_eq |
|
157 |> dest_comb |
|
158 val supp_abs_tac = |
|
159 case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of |
|
160 SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses) |
|
161 | NONE => mk_bn_supp_abs_tac fv_fun |
|
162 in |
|
163 EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
|
164 TRY o supp_abs_tac, |
|
165 TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), |
|
166 TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], |
|
167 TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), |
|
168 TRY o asm_full_simp_tac (add_ss thms3), |
|
169 TRY o simp_tac (add_ss thms2), |
|
170 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i |
|
171 end) |
|
172 in |
|
173 induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |
|
174 |> map atomize |
|
175 |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]})) |
|
176 end |
|
177 |
|
178 |
|
179 fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt = |
|
180 let |
|
181 fun mk_goal qbn = |
|
182 let |
|
183 val arg_ty = domain_type (fastype_of qbn) |
|
184 val finite = @{term "finite :: atom set => bool"} |
|
185 in |
|
186 (arg_ty, fn x => finite $ (to_set (qbn $ x))) |
|
187 end |
|
188 |
|
189 val props = map mk_goal qbns |
|
190 val ss_tac = asm_full_simp_tac (HOL_basic_ss addsimps (qbn_simps @ |
|
191 @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) |
|
192 in |
|
193 induct_prove qtys props qinduct (K ss_tac) ctxt |
|
194 end |
|
195 |
|
196 fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt = |
|
197 let |
|
198 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
|
199 val p = Free (p, @{typ perm}) |
|
200 |
|
201 fun mk_goal qperm_bn alpha_bn = |
|
202 let |
|
203 val arg_ty = domain_type (fastype_of alpha_bn) |
|
204 in |
|
205 (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x) |
|
206 end |
|
207 |
|
208 val props = map2 mk_goal qperm_bns alpha_bns |
|
209 val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls |
|
210 val ss_tac = asm_full_simp_tac (HOL_ss addsimps ss) |
|
211 in |
|
212 induct_prove qtys props qinduct (K ss_tac) ctxt' |
|
213 |> ProofContext.export ctxt' ctxt |
|
214 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
|
215 end |
|
216 |
|
217 |
|
218 end (* structure *) |
|