src/HOL/BNF/Tools/bnf_decl.ML
changeset 55025 1ac0a0194428
parent 54960 d72279b9bc44
     1.1 --- a/src/HOL/BNF/Tools/bnf_decl.ML	Thu Jan 16 21:22:01 2014 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_decl.ML	Fri Jan 17 09:52:19 2014 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  signature BNF_DECL =
     1.5  sig
     1.6    val bnf_decl: (binding option * (typ * sort)) list -> binding -> mixfix -> binding -> binding ->
     1.7 -    local_theory -> BNF_Def.bnf * local_theory
     1.8 +    typ list -> local_theory -> BNF_Def.bnf * local_theory
     1.9  end
    1.10  
    1.11  structure BNF_Decl : BNF_DECL =
    1.12 @@ -17,7 +17,7 @@
    1.13  open BNF_Util
    1.14  open BNF_Def
    1.15  
    1.16 -fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb lthy =
    1.17 +fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy =
    1.18    let
    1.19     fun prepare_type_arg (set_opt, (ty, c)) =
    1.20        let val s = fst (dest_TFree (prepare_typ lthy ty)) in
    1.21 @@ -50,23 +50,34 @@
    1.22      val bdb = mk_b "bd" Binding.empty;
    1.23      val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs
    1.24        (if live = 1 then [0] else 1 upto live);
    1.25 +
    1.26 +    val witTs = map (prepare_typ lthy) user_witTs;
    1.27 +    val nwits = length witTs;
    1.28 +    val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty)
    1.29 +      (if nwits = 1 then [0] else 1 upto nwits);
    1.30 +
    1.31      val lthy = Local_Theory.background_theory
    1.32        (Sign.add_consts_i ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
    1.33 -        map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs))
    1.34 +        map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
    1.35 +        map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
    1.36        lthy;
    1.37      val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
    1.38      val Fsets = map2 (fn setb => fn setT =>
    1.39        Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
    1.40      val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
    1.41 +    val Fwits = map2 (fn witb => fn witT =>
    1.42 +      Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
    1.43      val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
    1.44        prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads))
    1.45 -      user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), []), NONE) lthy;
    1.46 +      user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE)
    1.47 +      lthy;
    1.48  
    1.49      fun mk_wits_tac set_maps = K (TRYALL Goal.conjunction_tac) THEN' the triv_tac_opt set_maps;
    1.50      val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
    1.51 +    val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
    1.52  
    1.53 -    val ((_, [thms]), (lthy_old, lthy)) = Local_Theory.background_theory_result
    1.54 -      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), goals)]) lthy
    1.55 +    val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result
    1.56 +      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy
    1.57        ||> `Local_Theory.restore;
    1.58  
    1.59      fun mk_wit_thms set_maps =
    1.60 @@ -75,8 +86,9 @@
    1.61        |> map2 (Conjunction.elim_balanced o length) wit_goalss
    1.62        |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
    1.63      val phi = Proof_Context.export_morphism lthy_old lthy;
    1.64 +    val thms = unflat all_goalss (Morphism.fact phi raw_thms);
    1.65    in
    1.66 -    BNF_Def.register_bnf key (after_qed mk_wit_thms (map single (Morphism.fact phi thms)) lthy)
    1.67 +    BNF_Def.register_bnf key (after_qed mk_wit_thms thms lthy)
    1.68    end;
    1.69  
    1.70  val bnf_decl = prepare_decl (K I) (K I);
    1.71 @@ -84,14 +96,22 @@
    1.72  fun read_constraint _ NONE = HOLogic.typeS
    1.73    | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
    1.74  
    1.75 -val bnf_decl_cmd = prepare_decl read_constraint Syntax.parse_typ;
    1.76 +val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ;
    1.77 +
    1.78 +val parse_witTs =
    1.79 +  @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ
    1.80 +    >> (fn ("wits", Ts) => Ts
    1.81 +         | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
    1.82 +  @{keyword "]"} || Scan.succeed [];
    1.83  
    1.84  val parse_bnf_decl =
    1.85 -  parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- Parse.opt_mixfix;
    1.86 +  parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
    1.87 +    parse_witTs -- Parse.opt_mixfix;
    1.88  
    1.89  val _ =
    1.90    Outer_Syntax.local_theory @{command_spec "bnf_decl"} "bnf declaration"
    1.91      (parse_bnf_decl >> 
    1.92 -      (fn (((bsTs, b), (mapb, relb)), mx) => bnf_decl_cmd bsTs b mx mapb relb #> snd));
    1.93 +      (fn ((((bsTs, b), (mapb, relb)), witTs), mx) =>
    1.94 +         bnf_decl_cmd bsTs b mx mapb relb witTs #> snd));
    1.95  
    1.96  end;