author | wenzelm |
Tue, 04 Jun 2019 13:14:17 +0200 | |
changeset 70316 | c61b7af108a6 |
parent 69593 | 3dda49e08b9d |
child 70494 | 41108e3e9ca5 |
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 Transfer 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 TRANSFER_BNF = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
8 |
sig |
59823
a03696dc3283
more graceful failure if some of the involved BNFs have no data
blanchet
parents:
59621
diff
changeset
|
9 |
exception NO_PRED_DATA of unit |
a03696dc3283
more graceful failure if some of the involved BNFs have no data
blanchet
parents:
59621
diff
changeset
|
10 |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
11 |
val base_name_of_bnf: BNF_Def.bnf -> binding |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
12 |
val type_name_of_bnf: BNF_Def.bnf -> string |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
13 |
val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
14 |
val bnf_only_type_ctr: (BNF_Def.bnf -> 'a -> 'a) -> BNF_Def.bnf -> 'a -> 'a |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
15 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
16 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
17 |
structure Transfer_BNF : TRANSFER_BNF = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
18 |
struct |
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 |
open BNF_Util |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
21 |
open BNF_Def |
56651 | 22 |
open BNF_FP_Util |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
23 |
open BNF_FP_Def_Sugar |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
24 |
|
59823
a03696dc3283
more graceful failure if some of the involved BNFs have no data
blanchet
parents:
59621
diff
changeset
|
25 |
exception NO_PRED_DATA of unit |
a03696dc3283
more graceful failure if some of the involved BNFs have no data
blanchet
parents:
59621
diff
changeset
|
26 |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
27 |
(* util functions *) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
28 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
29 |
fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf)) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
30 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
31 |
fun mk_Domainp P = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
32 |
let |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
33 |
val PT = fastype_of P |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
34 |
val argT = hd (binder_types PT) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
35 |
in |
69593 | 36 |
Const (\<^const_name>\<open>Domainp\<close>, PT --> argT --> HOLogic.boolT) $ P |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
37 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
38 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
39 |
fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst |
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 bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
42 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
43 |
fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
44 |
|
61768
99f1eaf70c3d
reverted inadvertently qfinished/pushed change r164eeb2ab675
blanchet
parents:
61761
diff
changeset
|
45 |
fun fp_sugar_only_type_ctr f fp_sugars = |
99f1eaf70c3d
reverted inadvertently qfinished/pushed change r164eeb2ab675
blanchet
parents:
61761
diff
changeset
|
46 |
(case filter (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugars of |
99f1eaf70c3d
reverted inadvertently qfinished/pushed change r164eeb2ab675
blanchet
parents:
61761
diff
changeset
|
47 |
[] => I |
99f1eaf70c3d
reverted inadvertently qfinished/pushed change r164eeb2ab675
blanchet
parents:
61761
diff
changeset
|
48 |
| fp_sugars' => f fp_sugars') |
99f1eaf70c3d
reverted inadvertently qfinished/pushed change r164eeb2ab675
blanchet
parents:
61761
diff
changeset
|
49 |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
50 |
(* relation constraints - bi_total & co. *) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
51 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
52 |
fun mk_relation_constraint name arg = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
53 |
(Const (name, fastype_of arg --> HOLogic.boolT)) $ arg |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
54 |
|
62334 | 55 |
fun side_constraint_tac bnf constr_defs ctxt = |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
56 |
let |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
57 |
val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf, |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
58 |
rel_OO_of_bnf bnf] |
57399 | 59 |
in |
63170 | 60 |
SELECT_GOAL (Local_Defs.unfold0_tac ctxt thms) THEN' rtac ctxt (rel_mono_of_bnf bnf) |
62334 | 61 |
THEN_ALL_NEW assume_tac ctxt |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
62 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
63 |
|
62334 | 64 |
fun bi_constraint_tac constr_iff sided_constr_intros ctxt = |
63170 | 65 |
SELECT_GOAL (Local_Defs.unfold0_tac ctxt [constr_iff]) THEN' |
60728 | 66 |
CONJ_WRAP' (fn thm => rtac ctxt thm THEN_ALL_NEW |
62334 | 67 |
(REPEAT_DETERM o etac ctxt conjE THEN' assume_tac ctxt)) sided_constr_intros |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
68 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
69 |
fun generate_relation_constraint_goal ctxt bnf constraint_def = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
70 |
let |
59582 | 71 |
val constr_name = |
72 |
constraint_def |> Thm.prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
73 |
|> head_of |> fst o dest_Const |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
74 |
val live = live_of_bnf bnf |
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
75 |
val (((As, Bs), Ds), ctxt') = ctxt |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
76 |
|> mk_TFrees live |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
77 |
||>> mk_TFrees live |
60207 | 78 |
||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf)) |
57399 | 79 |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
80 |
val relator = mk_rel_of_bnf Ds As Bs bnf |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
81 |
val relsT = map2 mk_pred2T As Bs |
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
82 |
val (args, ctxt'') = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt' |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
83 |
val concl = HOLogic.mk_Trueprop (mk_relation_constraint constr_name (list_comb (relator, args))) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
84 |
val assms = map (HOLogic.mk_Trueprop o (mk_relation_constraint constr_name)) args |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
85 |
val goal = Logic.list_implies (assms, concl) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
86 |
in |
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
87 |
(goal, ctxt'') |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
88 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
89 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
90 |
fun prove_relation_side_constraint ctxt bnf constraint_def = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
91 |
let |
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
92 |
val (goal, ctxt') = generate_relation_constraint_goal ctxt bnf constraint_def |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
93 |
in |
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
94 |
Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} => |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
95 |
side_constraint_tac bnf [constraint_def] goal_ctxt 1) |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
96 |
|> Thm.close_derivation |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
97 |
|> singleton (Variable.export ctxt' ctxt) |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
98 |
|> Drule.zero_var_indexes |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
99 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
100 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
101 |
fun prove_relation_bi_constraint ctxt bnf constraint_def side_constraints = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
102 |
let |
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
103 |
val (goal, ctxt') = generate_relation_constraint_goal ctxt bnf constraint_def |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
104 |
in |
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
105 |
Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} => |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
106 |
bi_constraint_tac constraint_def side_constraints goal_ctxt 1) |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
107 |
|> Thm.close_derivation |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
108 |
|> singleton (Variable.export ctxt' ctxt) |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
109 |
|> Drule.zero_var_indexes |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
110 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
111 |
|
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
112 |
val defs = |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
113 |
[("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}), |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
114 |
("left_unique_rel", @{thm left_unique_alt_def}), ("right_unique_rel", @{thm right_unique_alt_def})] |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
115 |
|
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
116 |
fun prove_relation_constraints bnf ctxt = |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
117 |
let |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
118 |
val transfer_attr = @{attributes [transfer_rule]} |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
119 |
val Tname = base_name_of_bnf bnf |
57399 | 120 |
|
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
121 |
val defs = map (apsnd (prove_relation_side_constraint ctxt bnf)) defs |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
122 |
val bi_total = prove_relation_bi_constraint ctxt bnf @{thm bi_total_alt_def} |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
123 |
[snd (nth defs 0), snd (nth defs 1)] |
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
124 |
val bi_unique = prove_relation_bi_constraint ctxt bnf @{thm bi_unique_alt_def} |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
125 |
[snd (nth defs 2), snd (nth defs 3)] |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
126 |
val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
127 |
in |
63003 | 128 |
maps (fn (a, thm) => [((Binding.qualify_name true Tname a, []), [([thm], transfer_attr)])]) defs |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
129 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
130 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
131 |
(* relator_eq *) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
132 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
133 |
fun relator_eq bnf = |
63352 | 134 |
[(Binding.empty_atts, [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])] |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
135 |
|
58722 | 136 |
(* transfer rules *) |
137 |
||
138 |
fun bnf_transfer_rules bnf = |
|
139 |
let |
|
62329 | 140 |
val transfer_rules = map_transfer_of_bnf bnf :: pred_transfer_of_bnf bnf |
141 |
:: rel_transfer_of_bnf bnf :: set_transfer_of_bnf bnf |
|
58722 | 142 |
val transfer_attr = @{attributes [transfer_rule]} |
143 |
in |
|
63352 | 144 |
map (fn thm => (Binding.empty_atts, [([thm],transfer_attr)])) transfer_rules |
58722 | 145 |
end |
146 |
||
62324 | 147 |
(* Domainp theorem for predicator *) |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
148 |
|
62334 | 149 |
fun Domainp_tac bnf pred_def ctxt = |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
150 |
let |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
151 |
val n = live_of_bnf bnf |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
152 |
val set_map's = set_map_of_bnf bnf |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
153 |
in |
63170 | 154 |
EVERY' [rtac ctxt ext, SELECT_GOAL (Local_Defs.unfold0_tac ctxt [@{thm Domainp.simps}, |
60728 | 155 |
in_rel_of_bnf bnf, pred_def]), rtac ctxt iffI, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59276
diff
changeset
|
156 |
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], hyp_subst_tac ctxt, |
60728 | 157 |
CONJ_WRAP' (fn set_map => EVERY' [rtac ctxt ballI, dtac ctxt (set_map RS equalityD1 RS set_mp), |
158 |
etac ctxt imageE, dtac ctxt set_rev_mp, assume_tac ctxt, |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59276
diff
changeset
|
159 |
REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm case_prodE}], |
60728 | 160 |
hyp_subst_tac ctxt, rtac ctxt @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]}, |
161 |
etac ctxt @{thm DomainPI}]) set_map's, |
|
162 |
REPEAT_DETERM o etac ctxt conjE, |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59276
diff
changeset
|
163 |
REPEAT_DETERM o resolve_tac ctxt [exI, (refl RS conjI), rotate_prems 1 conjI], |
60728 | 164 |
rtac ctxt refl, rtac ctxt (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym, |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
165 |
map_id_of_bnf bnf]), |
60728 | 166 |
REPEAT_DETERM_N n o (EVERY' [rtac ctxt @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]}, |
167 |
rtac ctxt @{thm fst_conv}]), rtac ctxt CollectI, |
|
168 |
CONJ_WRAP' (fn set_map => EVERY' [rtac ctxt (set_map RS @{thm ord_eq_le_trans}), |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59276
diff
changeset
|
169 |
REPEAT_DETERM o resolve_tac ctxt [@{thm image_subsetI}, CollectI, @{thm case_prodI}], |
60728 | 170 |
dtac ctxt (rotate_prems 1 bspec), assume_tac ctxt, |
171 |
etac ctxt @{thm DomainpE}, etac ctxt @{thm someI}]) set_map's |
|
62334 | 172 |
] |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
173 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
174 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
175 |
fun prove_Domainp_rel ctxt bnf pred_def = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
176 |
let |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
177 |
val live = live_of_bnf bnf |
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
178 |
val (((As, Bs), Ds), ctxt') = ctxt |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
179 |
|> mk_TFrees live |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
180 |
||>> mk_TFrees live |
60207 | 181 |
||>> mk_TFrees' (map Type.sort_of_atyp (deads_of_bnf bnf)) |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
182 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
183 |
val relator = mk_rel_of_bnf Ds As Bs bnf |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
184 |
val relsT = map2 mk_pred2T As Bs |
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
185 |
val (args, ctxt'') = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt' |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
186 |
val lhs = mk_Domainp (list_comb (relator, args)) |
62324 | 187 |
val rhs = Term.list_comb (mk_pred_of_bnf Ds As bnf, map mk_Domainp args) |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
188 |
val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
189 |
in |
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
190 |
Goal.prove_sorry ctxt'' [] [] goal (fn {context = goal_ctxt, ...} => |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
191 |
Domainp_tac bnf pred_def goal_ctxt 1) |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
192 |
|> Thm.close_derivation |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
193 |
|> singleton (Variable.export ctxt'' ctxt) |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
194 |
|> Drule.zero_var_indexes |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
195 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
196 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
197 |
fun predicator bnf lthy = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
198 |
let |
62324 | 199 |
val pred_def = pred_set_of_bnf bnf |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
200 |
val Domainp_rel = prove_Domainp_rel lthy bnf pred_def |
62324 | 201 |
val rel_eq_onp = rel_eq_onp_of_bnf bnf |
63003 | 202 |
val Domainp_rel_thm_name = Binding.qualify_name true (base_name_of_bnf bnf) "Domainp_rel" |
60220 | 203 |
val pred_data = Transfer.mk_pred_data pred_def rel_eq_onp [] |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
204 |
val type_name = type_name_of_bnf bnf |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
205 |
val relator_domain_attr = @{attributes [relator_domain]} |
62324 | 206 |
val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)])] |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
207 |
in |
58356 | 208 |
lthy |
209 |
|> Local_Theory.notes notes |
|
210 |
|> snd |
|
211 |
|> Local_Theory.declaration {syntax = false, pervasive = true} |
|
212 |
(fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
213 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
214 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
215 |
(* BNF interpretation *) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
216 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
217 |
fun transfer_bnf_interpretation bnf lthy = |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
218 |
let |
58356 | 219 |
val dead = dead_of_bnf bnf |
220 |
val constr_notes = if dead > 0 then [] else prove_relation_constraints bnf lthy |
|
221 |
val relator_eq_notes = if dead > 0 then [] else relator_eq bnf |
|
58722 | 222 |
val transfer_rule_notes = if dead > 0 then [] else bnf_transfer_rules bnf |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
223 |
in |
58356 | 224 |
lthy |
58722 | 225 |
|> Local_Theory.notes (constr_notes @ relator_eq_notes @ transfer_rule_notes) |
58356 | 226 |
|> snd |
227 |
|> predicator bnf |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
228 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
229 |
|
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58458
diff
changeset
|
230 |
val _ = |
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58458
diff
changeset
|
231 |
Theory.setup |
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58458
diff
changeset
|
232 |
(bnf_interpretation transfer_plugin (bnf_only_type_ctr transfer_bnf_interpretation)) |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
233 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
234 |
(* simplification rules for the predicator *) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
235 |
|
70316
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
236 |
fun lookup_defined_pred_data ctxt name = |
c61b7af108a6
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
237 |
case Transfer.lookup_pred_data ctxt name of |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
238 |
SOME data => data |
59823
a03696dc3283
more graceful failure if some of the involved BNFs have no data
blanchet
parents:
59621
diff
changeset
|
239 |
| NONE => raise NO_PRED_DATA () |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
240 |
|
56677
660ffb526069
predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents:
56651
diff
changeset
|
241 |
|
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
242 |
(* fp_sugar interpretation *) |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
243 |
|
58722 | 244 |
fun fp_sugar_transfer_rules (fp_sugar:fp_sugar) = |
245 |
let |
|
246 |
val fp_ctr_sugar = #fp_ctr_sugar fp_sugar |
|
62531 | 247 |
val transfer_rules = #ctr_transfers fp_ctr_sugar @ #case_transfers fp_ctr_sugar |
248 |
@ #disc_transfers fp_ctr_sugar @ #sel_transfers fp_ctr_sugar |
|
63859
dca6fabd8060
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
blanchet
parents:
63352
diff
changeset
|
249 |
@ these (Option.map #co_rec_transfers (#fp_co_induct_sugar fp_sugar)) |
58722 | 250 |
val transfer_attr = @{attributes [transfer_rule]} |
251 |
in |
|
63352 | 252 |
map (fn thm => (Binding.empty_atts, [([thm], transfer_attr)])) transfer_rules |
58722 | 253 |
end |
254 |
||
62335 | 255 |
fun register_pred_injects fp_sugar lthy = |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
256 |
let |
62335 | 257 |
val pred_injects = #pred_injects (#fp_bnf_sugar fp_sugar) |
60220 | 258 |
val type_name = type_name_of_bnf (#fp_bnf fp_sugar) |
62531 | 259 |
val pred_data = lookup_defined_pred_data lthy type_name |
60220 | 260 |
|> Transfer.update_pred_simps pred_injects |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
261 |
in |
62531 | 262 |
lthy |
60220 | 263 |
|> Local_Theory.declaration {syntax = false, pervasive = true} |
62334 | 264 |
(fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) |
58722 | 265 |
end |
266 |
||
267 |
fun transfer_fp_sugars_interpretation fp_sugar lthy = |
|
268 |
let |
|
62335 | 269 |
val lthy = register_pred_injects fp_sugar lthy |
58722 | 270 |
val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar |
271 |
in |
|
272 |
lthy |
|
60220 | 273 |
|> Local_Theory.notes transfer_rules_notes |
58722 | 274 |
|> snd |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
275 |
end |
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
276 |
|
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58458
diff
changeset
|
277 |
val _ = |
61768
99f1eaf70c3d
reverted inadvertently qfinished/pushed change r164eeb2ab675
blanchet
parents:
61761
diff
changeset
|
278 |
Theory.setup (fp_sugars_interpretation transfer_plugin |
99f1eaf70c3d
reverted inadvertently qfinished/pushed change r164eeb2ab675
blanchet
parents:
61761
diff
changeset
|
279 |
(fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation))) |
56524
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
280 |
|
f4ba736040fa
setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff
changeset
|
281 |
end |