|
1 (* Title: HOL/Tools/Transfer/transfer_bnf.ML |
|
2 Author: Ondrej Kuncar, TU Muenchen |
|
3 |
|
4 Setup for Lifting for types that are BNF. |
|
5 *) |
|
6 |
|
7 signature LIFTING_BNF = |
|
8 sig |
|
9 end |
|
10 |
|
11 structure Lifting_BNF : LIFTING_BNF = |
|
12 struct |
|
13 |
|
14 open BNF_Util |
|
15 open BNF_Def |
|
16 open Transfer_BNF |
|
17 |
|
18 (* Quotient map theorem *) |
|
19 |
|
20 fun Quotient_tac bnf ctxt i = |
|
21 let |
|
22 val rel_Grp = rel_Grp_of_bnf bnf |
|
23 fun get_lhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |
|
24 val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd)) |
|
25 val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars |
|
26 val inst = map2 (curry(pairself (certify ctxt))) vars UNIVs |
|
27 val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst) |
|
28 |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)} |
|
29 |> (fn thm => thm RS sym) |
|
30 val rel_mono = rel_mono_of_bnf bnf |
|
31 val rel_conversep_sym = rel_conversep_of_bnf bnf RS sym |
|
32 in |
|
33 EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Quotient_alt_def5}]), |
|
34 REPEAT_DETERM o (etac conjE), rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_Grp_UNIV_sym]), |
|
35 rtac rel_mono THEN_ALL_NEW atac, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt |
|
36 [rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW atac, |
|
37 SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_conversep_sym, rel_OO_of_bnf bnf RS sym]), |
|
38 hyp_subst_tac ctxt, rtac refl] i |
|
39 end |
|
40 |
|
41 fun mk_Quotient args = |
|
42 let |
|
43 val argTs = map fastype_of args |
|
44 in |
|
45 list_comb (Const (@{const_name Quotient}, argTs ---> HOLogic.boolT), args) |
|
46 end |
|
47 |
|
48 fun prove_Quotient_map bnf ctxt = |
|
49 let |
|
50 val live = live_of_bnf bnf |
|
51 val old_ctxt = ctxt |
|
52 val (((As, Bs), Ds), ctxt) = ctxt |
|
53 |> mk_TFrees live |
|
54 ||>> mk_TFrees live |
|
55 ||>> mk_TFrees (dead_of_bnf bnf) |
|
56 val argTss = map2 (fn a => fn b => [mk_pred2T a a, a --> b, b --> a,mk_pred2T a b]) As Bs |
|
57 val ((argss, argss'), ctxt) = fold_map2 mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt |
|
58 |>> `transpose |
|
59 |
|
60 val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss |
|
61 val R_rel = list_comb (mk_rel_of_bnf Ds As As bnf, nth argss' 0) |
|
62 val Abs_map = list_comb (mk_map_of_bnf Ds As Bs bnf, nth argss' 1) |
|
63 val Rep_map = list_comb (mk_map_of_bnf Ds Bs As bnf, nth argss' 2) |
|
64 val T_rel = list_comb (mk_rel_of_bnf Ds As Bs bnf, nth argss' 3) |
|
65 val concl = mk_Quotient [R_rel, Abs_map, Rep_map, T_rel] |> HOLogic.mk_Trueprop |
|
66 val goal = Logic.list_implies (assms, concl) |
|
67 val thm = Goal.prove ctxt [] [] goal |
|
68 (fn {context = ctxt, prems = _} => Quotient_tac bnf ctxt 1) |
|
69 in |
|
70 Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) |
|
71 end |
|
72 |
|
73 |
|
74 fun Quotient_map bnf ctxt = |
|
75 let |
|
76 val Quotient = prove_Quotient_map bnf ctxt |
|
77 fun qualify defname suffix = Binding.qualified true suffix defname |
|
78 val Quotient_thm_name = qualify (base_name_of_bnf bnf) "Quotient" |
|
79 val notes = [((Quotient_thm_name, []), [([Quotient], @{attributes [quot_map]})])] |
|
80 in |
|
81 notes |
|
82 end |
|
83 |
|
84 (* relator_eq_onp *) |
|
85 |
|
86 fun relator_eq_onp bnf ctxt = |
|
87 let |
|
88 val pred_data = lookup_defined_pred_data ctxt (type_name_of_bnf bnf) |
|
89 in |
|
90 [((Binding.empty, []), [([Transfer.rel_eq_onp pred_data], @{attributes [relator_eq_onp]})])] |
|
91 end |
|
92 |
|
93 (* relator_mono *) |
|
94 |
|
95 fun relator_mono bnf = |
|
96 [((Binding.empty, []), [([rel_mono_of_bnf bnf], @{attributes [relator_mono]})])] |
|
97 |
|
98 (* relator_distr *) |
|
99 |
|
100 fun relator_distr bnf = |
|
101 [((Binding.empty, []), [([rel_OO_of_bnf bnf RS sym], @{attributes [relator_distr]})])] |
|
102 |
|
103 (* interpretation *) |
|
104 |
|
105 fun lifting_bnf_interpretation bnf lthy = |
|
106 if dead_of_bnf bnf > 0 then lthy |
|
107 else |
|
108 let |
|
109 val notes = relator_eq_onp bnf lthy @ Quotient_map bnf lthy @ relator_mono bnf |
|
110 @ relator_distr bnf |
|
111 in |
|
112 snd (Local_Theory.notes notes lthy) |
|
113 end |
|
114 |
|
115 val _ = Context.>> (Context.map_theory (bnf_interpretation |
|
116 (bnf_only_type_ctr (fn bnf => map_local_theory (lifting_bnf_interpretation bnf))))) |
|
117 |
|
118 end |