author | wenzelm |
Mon, 13 Oct 2014 18:45:48 +0200 | |
changeset 58659 | 6c9821c32dd5 |
parent 58634 | 9f10d82e8188 |
child 58963 | 26bf09b95dda |
permissions | -rw-r--r-- |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Transfer/transfer_bnf.ML |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
2 |
Author: Ondrej Kuncar, TU Muenchen |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
3 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
4 |
Setup for Lifting for types that are BNF. |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
5 |
*) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
6 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
7 |
signature LIFTING_BNF = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
8 |
sig |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
9 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
10 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
11 |
structure Lifting_BNF : LIFTING_BNF = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
12 |
struct |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
13 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
14 |
open BNF_Util |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
15 |
open BNF_Def |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
16 |
open Transfer_BNF |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
17 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
18 |
(* Quotient map theorem *) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
19 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
20 |
fun Quotient_tac bnf ctxt i = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
21 |
let |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
22 |
val rel_Grp = rel_Grp_of_bnf bnf |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
23 |
fun get_lhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
24 |
val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd)) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
25 |
val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
26 |
val inst = map2 (curry(pairself (certify ctxt))) vars UNIVs |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
27 |
val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
28 |
|> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)} |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
29 |
|> (fn thm => thm RS sym) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
30 |
val rel_mono = rel_mono_of_bnf bnf |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
31 |
val rel_conversep_sym = rel_conversep_of_bnf bnf RS sym |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
32 |
in |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
33 |
EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Quotient_alt_def5}]), |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
34 |
REPEAT_DETERM o (etac conjE), rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_Grp_UNIV_sym]), |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
35 |
rtac rel_mono THEN_ALL_NEW atac, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
36 |
[rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW atac, |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
37 |
SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_conversep_sym, rel_OO_of_bnf bnf RS sym]), |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
38 |
hyp_subst_tac ctxt, rtac refl] i |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
39 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
40 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
41 |
fun mk_Quotient args = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
42 |
let |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
43 |
val argTs = map fastype_of args |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
44 |
in |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
45 |
list_comb (Const (@{const_name Quotient}, argTs ---> HOLogic.boolT), args) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
46 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
47 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
48 |
fun prove_Quotient_map bnf ctxt = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
49 |
let |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
50 |
val live = live_of_bnf bnf |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
51 |
val old_ctxt = ctxt |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
52 |
val (((As, Bs), Ds), ctxt) = ctxt |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
53 |
|> mk_TFrees live |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
54 |
||>> mk_TFrees live |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
55 |
||>> mk_TFrees (dead_of_bnf bnf) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
56 |
val argTss = map2 (fn a => fn b => [mk_pred2T a a, a --> b, b --> a,mk_pred2T a b]) As Bs |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58243
diff
changeset
|
57 |
val ((argss, argss'), ctxt) = |
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58243
diff
changeset
|
58 |
@{fold_map 2} mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
59 |
|>> `transpose |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
60 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
61 |
val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
62 |
val R_rel = list_comb (mk_rel_of_bnf Ds As As bnf, nth argss' 0) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
63 |
val Abs_map = list_comb (mk_map_of_bnf Ds As Bs bnf, nth argss' 1) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
64 |
val Rep_map = list_comb (mk_map_of_bnf Ds Bs As bnf, nth argss' 2) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
65 |
val T_rel = list_comb (mk_rel_of_bnf Ds As Bs bnf, nth argss' 3) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
66 |
val concl = mk_Quotient [R_rel, Abs_map, Rep_map, T_rel] |> HOLogic.mk_Trueprop |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
67 |
val goal = Logic.list_implies (assms, concl) |
57890
1e13f63fb452
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
traytel
parents:
56677
diff
changeset
|
68 |
val thm = Goal.prove_sorry ctxt [] [] goal |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
69 |
(fn {context = ctxt, prems = _} => Quotient_tac bnf ctxt 1) |
57890
1e13f63fb452
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
traytel
parents:
56677
diff
changeset
|
70 |
|> Thm.close_derivation |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
71 |
in |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
72 |
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
73 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
74 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
75 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
76 |
fun Quotient_map bnf ctxt = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
77 |
let |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
78 |
val Quotient = prove_Quotient_map bnf ctxt |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
79 |
fun qualify defname suffix = Binding.qualified true suffix defname |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
80 |
val Quotient_thm_name = qualify (base_name_of_bnf bnf) "Quotient" |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
81 |
val notes = [((Quotient_thm_name, []), [([Quotient], @{attributes [quot_map]})])] |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
82 |
in |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
83 |
notes |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
84 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
85 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
86 |
(* relator_eq_onp *) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
87 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
88 |
fun relator_eq_onp bnf ctxt = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
89 |
let |
56677
660ffb526069
predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents:
56524
diff
changeset
|
90 |
val relator_eq_onp_thm = lookup_defined_pred_data ctxt (type_name_of_bnf bnf) |
660ffb526069
predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents:
56524
diff
changeset
|
91 |
|> Transfer.rel_eq_onp |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv |
660ffb526069
predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents:
56524
diff
changeset
|
92 |
(Raw_Simplifier.rewrite ctxt false @{thms eq_onp_top_eq_eq[THEN eq_reflection]}))) |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
93 |
in |
56677
660ffb526069
predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents:
56524
diff
changeset
|
94 |
[((Binding.empty, []), [([relator_eq_onp_thm], @{attributes [relator_eq_onp]})])] |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
95 |
end |
58243 | 96 |
handle ERROR _ => [] (* the "lifting" plugin should work even if "quotient" is disabled *) |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
97 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
98 |
(* relator_mono *) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
99 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
100 |
fun relator_mono bnf = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
101 |
[((Binding.empty, []), [([rel_mono_of_bnf bnf], @{attributes [relator_mono]})])] |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
102 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
103 |
(* relator_distr *) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
104 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
105 |
fun relator_distr bnf = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
106 |
[((Binding.empty, []), [([rel_OO_of_bnf bnf RS sym], @{attributes [relator_distr]})])] |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
107 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
108 |
(* interpretation *) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
109 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
110 |
fun lifting_bnf_interpretation bnf lthy = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
111 |
if dead_of_bnf bnf > 0 then lthy |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
112 |
else |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
113 |
let |
58243 | 114 |
val notess = [relator_eq_onp bnf lthy, Quotient_map bnf lthy, relator_mono bnf, |
115 |
relator_distr bnf] |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
116 |
in |
58243 | 117 |
lthy |> fold (perhaps o try o (snd oo Local_Theory.notes)) notess |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
118 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
119 |
|
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58634
diff
changeset
|
120 |
val lifting_plugin = Plugin_Name.declare_setup @{binding lifting} |
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58634
diff
changeset
|
121 |
|
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58634
diff
changeset
|
122 |
val _ = |
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58634
diff
changeset
|
123 |
Theory.setup |
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58634
diff
changeset
|
124 |
(bnf_interpretation lifting_plugin (bnf_only_type_ctr lifting_bnf_interpretation)) |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
125 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
126 |
end |