56942
|
1 |
(* Title: HOL/Library/bnf_axiomatization.ML
|
|
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
|
|
10 |
val bnf_axiomatization: (binding option * (typ * sort)) list -> binding -> mixfix -> binding ->
|
|
11 |
binding -> typ list -> local_theory -> BNF_Def.bnf * local_theory
|
|
12 |
end
|
|
13 |
|
|
14 |
structure BNF_Axiomatization : BNF_AXIOMATIZATION =
|
|
15 |
struct
|
|
16 |
|
|
17 |
open BNF_Util
|
|
18 |
open BNF_Def
|
|
19 |
|
|
20 |
fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy =
|
|
21 |
let
|
|
22 |
fun prepare_type_arg (set_opt, (ty, c)) =
|
|
23 |
let val s = fst (dest_TFree (prepare_typ lthy ty)) in
|
|
24 |
(set_opt, (s, prepare_constraint lthy c))
|
|
25 |
end;
|
|
26 |
val ((user_setbs, vars), raw_vars') =
|
|
27 |
map prepare_type_arg raw_vars
|
|
28 |
|> `split_list
|
|
29 |
|>> apfst (map_filter I);
|
|
30 |
val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars';
|
|
31 |
|
|
32 |
fun mk_b name user_b =
|
|
33 |
(if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
|
|
34 |
|> Binding.qualify false (Binding.name_of b);
|
|
35 |
val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy;
|
|
36 |
val (bd_type_Tname, lthy) =
|
|
37 |
Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy;
|
|
38 |
val T = Type (Tname, map TFree vars);
|
|
39 |
val bd_type_T = Type (bd_type_Tname, map TFree deads);
|
|
40 |
val lives = map TFree (filter_out (member (op =) deads) vars);
|
|
41 |
val live = length lives;
|
|
42 |
val _ = "Trying to declare a BNF with no live variables" |> null lives ? error;
|
|
43 |
val (lives', _) = BNF_Util.mk_TFrees (length lives)
|
|
44 |
(fold Variable.declare_typ (map TFree vars) lthy);
|
|
45 |
val T' = Term.typ_subst_atomic (lives ~~ lives') T;
|
|
46 |
val mapT = map2 (curry op -->) lives lives' ---> T --> T';
|
|
47 |
val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
|
|
48 |
val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
|
|
49 |
val mapb = mk_b BNF_Def.mapN user_mapb;
|
|
50 |
val bdb = mk_b "bd" Binding.empty;
|
|
51 |
val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs
|
|
52 |
(if live = 1 then [0] else 1 upto live);
|
|
53 |
|
|
54 |
val witTs = map (prepare_typ lthy) user_witTs;
|
|
55 |
val nwits = length witTs;
|
|
56 |
val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty)
|
|
57 |
(if nwits = 1 then [0] else 1 upto nwits);
|
|
58 |
|
|
59 |
val lthy = Local_Theory.background_theory
|
|
60 |
(Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
|
|
61 |
map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
|
|
62 |
map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
|
|
63 |
lthy;
|
|
64 |
val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
|
|
65 |
val Fsets = map2 (fn setb => fn setT =>
|
|
66 |
Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
|
|
67 |
val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
|
|
68 |
val Fwits = map2 (fn witb => fn witT =>
|
|
69 |
Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
|
|
70 |
val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
|
|
71 |
prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
|
|
72 |
user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
|
|
73 |
lthy;
|
|
74 |
|
|
75 |
fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
|
|
76 |
val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
|
|
77 |
val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
|
|
78 |
|
|
79 |
val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result
|
|
80 |
(Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy
|
|
81 |
||> `Local_Theory.restore;
|
|
82 |
|
|
83 |
fun mk_wit_thms set_maps =
|
|
84 |
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
|
|
85 |
(fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
|
|
86 |
|> Conjunction.elim_balanced (length wit_goals)
|
|
87 |
|> map2 (Conjunction.elim_balanced o length) wit_goalss
|
|
88 |
|> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
|
|
89 |
val phi = Proof_Context.export_morphism lthy_old lthy;
|
|
90 |
val thms = unflat all_goalss (Morphism.fact phi raw_thms);
|
|
91 |
|
|
92 |
val (bnf, lthy') = after_qed mk_wit_thms thms lthy
|
|
93 |
in
|
|
94 |
(bnf, BNF_Def.register_bnf key bnf lthy')
|
|
95 |
end;
|
|
96 |
|
|
97 |
val bnf_axiomatization = prepare_decl (K I) (K I);
|
|
98 |
|
|
99 |
fun read_constraint _ NONE = @{sort type}
|
|
100 |
| read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
|
|
101 |
|
|
102 |
val bnf_axiomatization_cmd = prepare_decl read_constraint Syntax.read_typ;
|
|
103 |
|
|
104 |
val parse_witTs =
|
|
105 |
@{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ
|
|
106 |
>> (fn ("wits", Ts) => Ts
|
|
107 |
| (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
|
|
108 |
@{keyword "]"} || Scan.succeed [];
|
|
109 |
|
|
110 |
val parse_bnf_axiomatization =
|
57091
|
111 |
parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
|
56942
|
112 |
parse_witTs -- Parse.opt_mixfix;
|
|
113 |
|
|
114 |
val _ =
|
|
115 |
Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration"
|
|
116 |
(parse_bnf_axiomatization >>
|
|
117 |
(fn ((((bsTs, b), (mapb, relb)), witTs), mx) =>
|
|
118 |
bnf_axiomatization_cmd bsTs b mx mapb relb witTs #> snd));
|
|
119 |
|
|
120 |
end;
|