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