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