|
1 (* Title: HOL/Tools/BNF/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: (string -> bool) -> (binding option * (typ * sort)) list -> binding -> |
|
11 mixfix -> binding -> binding -> binding -> typ list -> local_theory -> |
|
12 BNF_Def.bnf * local_theory |
|
13 end |
|
14 |
|
15 structure BNF_Axiomatization : BNF_AXIOMATIZATION = |
|
16 struct |
|
17 |
|
18 open BNF_Util |
|
19 open BNF_Def |
|
20 |
|
21 fun prepare_decl prepare_plugins prepare_constraint prepare_typ |
|
22 raw_plugins raw_vars b mx user_mapb user_relb user_predb user_witTs lthy = |
|
23 let |
|
24 val plugins = prepare_plugins lthy raw_plugins; |
|
25 |
|
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); |
|
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); |
|
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); |
|
53 val mapb = mk_b mapN user_mapb; |
|
54 val bdb = mk_b "bd" Binding.empty; |
|
55 val setbs = map2 (fn b => fn i => mk_b (mk_setN i) b) user_setbs |
|
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; |
|
60 val witbs = map (fn i => mk_b (mk_witN i) Binding.empty) |
|
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)) |
|
76 user_mapb user_relb user_predb user_setbs |
|
77 (((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE), NONE) |
|
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 |
|
84 val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result |
|
85 (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy; |
|
86 |
|
87 fun mk_wit_thms set_maps = |
|
88 Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) |
|
89 (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps) |
|
90 |> Thm.close_derivation |
|
91 |> Conjunction.elim_balanced (length wit_goals) |
|
92 |> map2 (Conjunction.elim_balanced o length) wit_goalss |
|
93 |> (map o map) (Thm.forall_elim_vars 0); |
|
94 val phi = Local_Theory.target_morphism lthy; |
|
95 val thms = unflat all_goalss (Morphism.fact phi raw_thms); |
|
96 |
|
97 val (bnf, lthy') = after_qed mk_wit_thms thms lthy |
|
98 in |
|
99 (bnf, register_bnf plugins key bnf lthy') |
|
100 end; |
|
101 |
|
102 val bnf_axiomatization = prepare_decl (K I) (K I) (K I); |
|
103 |
|
104 fun read_constraint _ NONE = @{sort type} |
|
105 | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; |
|
106 |
|
107 val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ; |
|
108 |
|
109 val parse_witTs = |
|
110 @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.typ |
|
111 >> (fn ("wits", Ts) => Ts |
|
112 | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| |
|
113 @{keyword "]"} || Scan.succeed []; |
|
114 |
|
115 val parse_bnf_axiomatization_options = |
|
116 Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"}) (K (K true)); |
|
117 |
|
118 val parse_bnf_axiomatization = |
|
119 parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding -- |
|
120 parse_witTs -- Parse.opt_mixfix -- parse_map_rel_pred_bindings; |
|
121 |
|
122 val _ = |
|
123 Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration" |
|
124 (parse_bnf_axiomatization >> |
|
125 (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) => |
|
126 bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd)); |
|
127 |
|
128 end; |