author | wenzelm |
Fri, 09 Aug 2019 17:14:49 +0200 | |
changeset 70494 | 41108e3e9ca5 |
parent 69593 | 3dda49e08b9d |
permissions | -rw-r--r-- |
62691
9bfcbab7cd99
put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
blanchet
parents:
62531
diff
changeset
|
1 |
(* Title: HOL/Tools/BNF/bnf_axiomatization.ML |
56942 | 2 |
Author: Dmitriy Traytel, TU Muenchen |
3 |
Copyright 2013 |
|
4 |
||
5 |
Axiomatic declaration of bounded natural functors. |
|
6 |
*) |
|
7 |
||
8 |
signature BNF_AXIOMATIZATION = |
|
9 |
sig |
|
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset
|
10 |
val bnf_axiomatization: (string -> bool) -> (binding option * (typ * sort)) list -> binding -> |
62324 | 11 |
mixfix -> binding -> binding -> binding -> typ list -> local_theory -> |
12 |
BNF_Def.bnf * local_theory |
|
56942 | 13 |
end |
14 |
||
15 |
structure BNF_Axiomatization : BNF_AXIOMATIZATION = |
|
16 |
struct |
|
17 |
||
18 |
open BNF_Util |
|
19 |
open BNF_Def |
|
20 |
||
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58189
diff
changeset
|
21 |
fun prepare_decl prepare_plugins prepare_constraint prepare_typ |
62324 | 22 |
raw_plugins raw_vars b mx user_mapb user_relb user_predb user_witTs lthy = |
56942 | 23 |
let |
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58189
diff
changeset
|
24 |
val plugins = prepare_plugins lthy raw_plugins; |
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58189
diff
changeset
|
25 |
|
56942 | 26 |
fun prepare_type_arg (set_opt, (ty, c)) = |
27 |
let val s = fst (dest_TFree (prepare_typ lthy ty)) in |
|
28 |
(set_opt, (s, prepare_constraint lthy c)) |
|
29 |
end; |
|
30 |
val ((user_setbs, vars), raw_vars') = |
|
31 |
map prepare_type_arg raw_vars |
|
32 |
|> `split_list |
|
33 |
|>> apfst (map_filter I); |
|
34 |
val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars'; |
|
35 |
||
36 |
fun mk_b name user_b = |
|
37 |
(if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b) |
|
38 |
|> Binding.qualify false (Binding.name_of b); |
|
61259 | 39 |
val (Tname, lthy) = Typedecl.basic_typedecl {final = true} (b, length vars, mx) lthy; |
40 |
val (bd_type_Tname, lthy) = lthy |
|
41 |
|> Typedecl.basic_typedecl {final = true} (mk_b "bd_type" Binding.empty, length deads, NoSyn); |
|
56942 | 42 |
val T = Type (Tname, map TFree vars); |
43 |
val bd_type_T = Type (bd_type_Tname, map TFree deads); |
|
44 |
val lives = map TFree (filter_out (member (op =) deads) vars); |
|
45 |
val live = length lives; |
|
46 |
val _ = "Trying to declare a BNF with no live variables" |> null lives ? error; |
|
47 |
val (lives', _) = BNF_Util.mk_TFrees (length lives) |
|
48 |
(fold Variable.declare_typ (map TFree vars) lthy); |
|
49 |
val T' = Term.typ_subst_atomic (lives ~~ lives') T; |
|
50 |
val mapT = map2 (curry op -->) lives lives' ---> T --> T'; |
|
51 |
val setTs = map (fn U => T --> HOLogic.mk_setT U) lives; |
|
52 |
val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T); |
|
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset
|
53 |
val mapb = mk_b mapN user_mapb; |
56942 | 54 |
val bdb = mk_b "bd" Binding.empty; |
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset
|
55 |
val setbs = map2 (fn b => fn i => mk_b (mk_setN i) b) user_setbs |
56942 | 56 |
(if live = 1 then [0] else 1 upto live); |
57 |
||
58 |
val witTs = map (prepare_typ lthy) user_witTs; |
|
59 |
val nwits = length witTs; |
|
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset
|
60 |
val witbs = map (fn i => mk_b (mk_witN i) Binding.empty) |
56942 | 61 |
(if nwits = 1 then [0] else 1 upto nwits); |
62 |
||
63 |
val lthy = Local_Theory.background_theory |
|
64 |
(Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: |
|
65 |
map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @ |
|
66 |
map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs)) |
|
67 |
lthy; |
|
68 |
val Fmap = Const (Local_Theory.full_name lthy mapb, mapT); |
|
69 |
val Fsets = map2 (fn setb => fn setT => |
|
70 |
Const (Local_Theory.full_name lthy setb, setT)) setbs setTs; |
|
71 |
val Fbd = Const (Local_Theory.full_name lthy bdb, bdT); |
|
72 |
val Fwits = map2 (fn witb => fn witT => |
|
73 |
Const (Local_Theory.full_name lthy witb, witT)) witbs witTs; |
|
74 |
val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) = |
|
75 |
prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads)) |
|
62324 | 76 |
user_mapb user_relb user_predb user_setbs |
77 |
(((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE), NONE) |
|
56942 | 78 |
lthy; |
79 |
||
80 |
fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps; |
|
81 |
val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; |
|
82 |
val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []); |
|
83 |
||
63178 | 84 |
val (((_, raw_thms)), lthy) = Local_Theory.background_theory_result |
85 |
(Specification.axiomatization [] [] [] |
|
86 |
(map_index (fn (i, ax) => |
|
87 |
((mk_b ("axiom" ^ string_of_int (i + 1)) Binding.empty, []), ax)) (flat all_goalss))) lthy; |
|
56942 | 88 |
|
89 |
fun mk_wit_thms set_maps = |
|
90 |
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) |
|
91 |
(fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps) |
|
70494 | 92 |
|> Thm.close_derivation \<^here> |
56942 | 93 |
|> Conjunction.elim_balanced (length wit_goals) |
94 |
|> map2 (Conjunction.elim_balanced o length) wit_goalss |
|
61116
6189d179c2b5
close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
wenzelm
parents:
59936
diff
changeset
|
95 |
|> (map o map) (Thm.forall_elim_vars 0); |
62531 | 96 |
val phi = Local_Theory.target_morphism lthy; |
56942 | 97 |
val thms = unflat all_goalss (Morphism.fact phi raw_thms); |
98 |
||
99 |
val (bnf, lthy') = after_qed mk_wit_thms thms lthy |
|
100 |
in |
|
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset
|
101 |
(bnf, register_bnf plugins key bnf lthy') |
56942 | 102 |
end; |
103 |
||
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58189
diff
changeset
|
104 |
val bnf_axiomatization = prepare_decl (K I) (K I) (K I); |
56942 | 105 |
|
69593 | 106 |
fun read_constraint _ NONE = \<^sort>\<open>type\<close> |
56942 | 107 |
| read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; |
108 |
||
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58189
diff
changeset
|
109 |
val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ; |
56942 | 110 |
|
111 |
val parse_witTs = |
|
69593 | 112 |
\<^keyword>\<open>[\<close> |-- (Parse.name --| \<^keyword>\<open>:\<close> -- Scan.repeat Parse.typ |
56942 | 113 |
>> (fn ("wits", Ts) => Ts |
114 |
| (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| |
|
69593 | 115 |
\<^keyword>\<open>]\<close> || Scan.succeed []; |
56942 | 116 |
|
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset
|
117 |
val parse_bnf_axiomatization_options = |
69593 | 118 |
Scan.optional (\<^keyword>\<open>(\<close> |-- Plugin_Name.parse_filter --| \<^keyword>\<open>)\<close>) (K (K true)); |
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset
|
119 |
|
56942 | 120 |
val parse_bnf_axiomatization = |
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
58188
diff
changeset
|
121 |
parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding -- |
62324 | 122 |
parse_witTs -- Parse.opt_mixfix -- parse_map_rel_pred_bindings; |
56942 | 123 |
|
124 |
val _ = |
|
69593 | 125 |
Outer_Syntax.local_theory \<^command_keyword>\<open>bnf_axiomatization\<close> "bnf declaration" |
62698 | 126 |
(parse_bnf_axiomatization >> |
62324 | 127 |
(fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) => |
128 |
bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd)); |
|
56942 | 129 |
|
130 |
end; |