1(*  Title:      HOL/Tools/BNF/bnf_axiomatization.ML
2    Author:     Dmitriy Traytel, TU Muenchen
3    Copyright   2013
4
5Axiomatic declaration of bounded natural functors.
6*)
7
8signature BNF_AXIOMATIZATION =
9sig
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
13end
14
15structure BNF_Axiomatization : BNF_AXIOMATIZATION =
16struct
17
18open BNF_Util
19open BNF_Def
20
21fun 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 [] [] []
86        (map_index (fn (i, ax) =>
87          ((mk_b ("axiom" ^ string_of_int (i + 1)) Binding.empty, []), ax)) (flat all_goalss))) lthy;
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)
92      |> Thm.close_derivation \<^here>
93      |> Conjunction.elim_balanced (length wit_goals)
94      |> map2 (Conjunction.elim_balanced o length) wit_goalss
95      |> (map o map) (Thm.forall_elim_vars 0);
96    val phi = Local_Theory.target_morphism lthy;
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
101    (bnf, register_bnf plugins key bnf lthy')
102  end;
103
104val bnf_axiomatization = prepare_decl (K I) (K I) (K I);
105
106fun read_constraint _ NONE = \<^sort>\<open>type\<close>
107  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
108
109val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ;
110
111val parse_witTs =
112  \<^keyword>\<open>[\<close> |-- (Parse.name --| \<^keyword>\<open>:\<close> -- Scan.repeat Parse.typ
113    >> (fn ("wits", Ts) => Ts
114         | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
115  \<^keyword>\<open>]\<close> || Scan.succeed [];
116
117val parse_bnf_axiomatization_options =
118  Scan.optional (\<^keyword>\<open>(\<close> |-- Plugin_Name.parse_filter --| \<^keyword>\<open>)\<close>) (K (K true));
119
120val parse_bnf_axiomatization =
121  parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding --
122  parse_witTs -- Parse.opt_mixfix -- parse_map_rel_pred_bindings;
123
124val _ =
125  Outer_Syntax.local_theory \<^command_keyword>\<open>bnf_axiomatization\<close> "bnf declaration"
126    (parse_bnf_axiomatization >>
127      (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) =>
128         bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd));
129
130end;
131