src/HOL/Tools/BNF/Tools/bnf_decl.ML
changeset 55058 4e700eb471d4
parent 55025 1ac0a0194428
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/BNF/Tools/bnf_decl.ML	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -0,0 +1,117 @@
     1.4 +(*  Title:      HOL/BNF/Tools/bnf_decl.ML
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Copyright   2013
     1.7 +
     1.8 +Axiomatic declaration of bounded natural functors.
     1.9 +*)
    1.10 +
    1.11 +signature BNF_DECL =
    1.12 +sig
    1.13 +  val bnf_decl: (binding option * (typ * sort)) list -> binding -> mixfix -> binding -> binding ->
    1.14 +    typ list -> local_theory -> BNF_Def.bnf * local_theory
    1.15 +end
    1.16 +
    1.17 +structure BNF_Decl : BNF_DECL =
    1.18 +struct
    1.19 +
    1.20 +open BNF_Util
    1.21 +open BNF_Def
    1.22 +
    1.23 +fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy =
    1.24 +  let
    1.25 +   fun prepare_type_arg (set_opt, (ty, c)) =
    1.26 +      let val s = fst (dest_TFree (prepare_typ lthy ty)) in
    1.27 +        (set_opt, (s, prepare_constraint lthy c))
    1.28 +      end;
    1.29 +    val ((user_setbs, vars), raw_vars') =
    1.30 +      map prepare_type_arg raw_vars
    1.31 +      |> `split_list
    1.32 +      |>> apfst (map_filter I);
    1.33 +    val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars';
    1.34 +
    1.35 +    fun mk_b name user_b =
    1.36 +      (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
    1.37 +      |> Binding.qualify false (Binding.name_of b);
    1.38 +    val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy;
    1.39 +    val (bd_type_Tname, lthy) =
    1.40 +      Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy;
    1.41 +    val T = Type (Tname, map TFree vars);
    1.42 +    val bd_type_T = Type (bd_type_Tname, map TFree deads);
    1.43 +    val lives = map TFree (filter_out (member (op =) deads) vars);
    1.44 +    val live = length lives;
    1.45 +    val _ = "Trying to declare a BNF with no live variables" |> null lives ? error;
    1.46 +    val (lives', _) = BNF_Util.mk_TFrees (length lives)
    1.47 +      (fold Variable.declare_typ (map TFree vars) lthy);
    1.48 +    val T' = Term.typ_subst_atomic (lives ~~ lives') T;
    1.49 +    val mapT = map2 (curry op -->) lives lives' ---> T --> T';
    1.50 +    val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
    1.51 +    val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
    1.52 +    val mapb = mk_b BNF_Def.mapN user_mapb;
    1.53 +    val bdb = mk_b "bd" Binding.empty;
    1.54 +    val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs
    1.55 +      (if live = 1 then [0] else 1 upto live);
    1.56 +
    1.57 +    val witTs = map (prepare_typ lthy) user_witTs;
    1.58 +    val nwits = length witTs;
    1.59 +    val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty)
    1.60 +      (if nwits = 1 then [0] else 1 upto nwits);
    1.61 +
    1.62 +    val lthy = Local_Theory.background_theory
    1.63 +      (Sign.add_consts_i ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
    1.64 +        map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
    1.65 +        map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
    1.66 +      lthy;
    1.67 +    val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
    1.68 +    val Fsets = map2 (fn setb => fn setT =>
    1.69 +      Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
    1.70 +    val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
    1.71 +    val Fwits = map2 (fn witb => fn witT =>
    1.72 +      Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
    1.73 +    val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
    1.74 +      prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads))
    1.75 +      user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
    1.76 +      lthy;
    1.77 +
    1.78 +    fun mk_wits_tac set_maps = K (TRYALL Goal.conjunction_tac) THEN' the triv_tac_opt set_maps;
    1.79 +    val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
    1.80 +    val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
    1.81 +
    1.82 +    val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result
    1.83 +      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy
    1.84 +      ||> `Local_Theory.restore;
    1.85 +
    1.86 +    fun mk_wit_thms set_maps =
    1.87 +      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
    1.88 +      |> Conjunction.elim_balanced (length wit_goals)
    1.89 +      |> map2 (Conjunction.elim_balanced o length) wit_goalss
    1.90 +      |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
    1.91 +    val phi = Proof_Context.export_morphism lthy_old lthy;
    1.92 +    val thms = unflat all_goalss (Morphism.fact phi raw_thms);
    1.93 +  in
    1.94 +    BNF_Def.register_bnf key (after_qed mk_wit_thms thms lthy)
    1.95 +  end;
    1.96 +
    1.97 +val bnf_decl = prepare_decl (K I) (K I);
    1.98 +
    1.99 +fun read_constraint _ NONE = HOLogic.typeS
   1.100 +  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
   1.101 +
   1.102 +val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ;
   1.103 +
   1.104 +val parse_witTs =
   1.105 +  @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ
   1.106 +    >> (fn ("wits", Ts) => Ts
   1.107 +         | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
   1.108 +  @{keyword "]"} || Scan.succeed [];
   1.109 +
   1.110 +val parse_bnf_decl =
   1.111 +  parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
   1.112 +    parse_witTs -- Parse.opt_mixfix;
   1.113 +
   1.114 +val _ =
   1.115 +  Outer_Syntax.local_theory @{command_spec "bnf_decl"} "bnf declaration"
   1.116 +    (parse_bnf_decl >> 
   1.117 +      (fn ((((bsTs, b), (mapb, relb)), witTs), mx) =>
   1.118 +         bnf_decl_cmd bsTs b mx mapb relb witTs #> snd));
   1.119 +
   1.120 +end;