improved internal interface of typedef;
authorwenzelm
Wed Oct 17 20:25:19 2001 +0200 (2001-10-17)
changeset 11822122834177ec1
parent 11821 ad32c92435db
child 11823 5a3fcd84e55e
improved internal interface of typedef;
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/typedef_package.ML
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Oct 17 20:24:37 2001 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Oct 17 20:25:19 2001 +0200
     1.3 @@ -181,9 +181,9 @@
     1.4  
     1.5      val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
     1.6        setmp TypedefPackage.quiet_mode true
     1.7 -        (TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
     1.8 -          (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1)
     1.9 -            (resolve_tac (Funs_nonempty::rep_intrs) 1)))) thy |> #1)
    1.10 +        (TypedefPackage.add_typedef_i false name' (name, tvs, mx) c None
    1.11 +          (QUIET_BREADTH_FIRST (has_fewer_prems 1)
    1.12 +            (resolve_tac (Funs_nonempty::rep_intrs) 1))) thy |> #1)
    1.13                (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
    1.14                  (take (length newTs, consts)) ~~ new_type_names));
    1.15  
     2.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Oct 17 20:24:37 2001 +0200
     2.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Oct 17 20:25:19 2001 +0200
     2.3 @@ -10,14 +10,18 @@
     2.4  sig
     2.5    val quiet_mode: bool ref
     2.6    val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
     2.7 -  val add_typedef: string -> bstring * string list * mixfix ->
     2.8 -    string -> string list -> thm list -> tactic option -> theory -> theory * thm
     2.9 -  val add_typedef_no_result: string -> bstring * string list * mixfix ->
    2.10 +  val add_typedef_x: string -> bstring * string list * mixfix ->
    2.11      string -> string list -> thm list -> tactic option -> theory -> theory
    2.12 -  val add_typedef_i: string -> bstring * string list * mixfix ->
    2.13 -    term -> string list -> thm list -> tactic option -> theory -> theory * thm
    2.14 -  val add_typedef_i_no_def: string -> bstring * string list * mixfix ->
    2.15 -    term -> string list -> thm list -> tactic option -> theory -> theory * thm
    2.16 +  val add_typedef: bool -> string -> bstring * string list * mixfix ->
    2.17 +    string -> (bstring * bstring) option -> tactic -> theory -> theory *
    2.18 +    {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    2.19 +      Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
    2.20 +      Rep_induct: thm, Abs_induct: thm}
    2.21 +  val add_typedef_i: bool -> string -> bstring * string list * mixfix ->
    2.22 +    term -> (bstring * bstring) option -> tactic -> theory -> theory *
    2.23 +    {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    2.24 +      Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
    2.25 +      Rep_induct: thm, Abs_induct: thm}
    2.26    val typedef_proof:
    2.27      (string * (bstring * string list * mixfix) * string * (string * string) option) * Comment.text
    2.28      -> bool -> theory -> ProofHistory.T
    2.29 @@ -100,7 +104,7 @@
    2.30  fun err_in_typedef name =
    2.31    error ("The error(s) above occurred in typedef " ^ quote name);
    2.32  
    2.33 -fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set opt_morphs thy =
    2.34 +fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
    2.35    let
    2.36      val _ = Theory.requires thy "Typedef" "typedefs";
    2.37      val sign = Theory.sign_of thy;
    2.38 @@ -133,7 +137,7 @@
    2.39      val x_new = Free ("x", newT);
    2.40      val y_old = Free ("y", oldT);
    2.41  
    2.42 -    val set' = if no_def then set else setC;
    2.43 +    val set' = if def then setC else set;
    2.44  
    2.45      val typedef_name = "type_definition_" ^ name;
    2.46      val typedefC =
    2.47 @@ -141,35 +145,42 @@
    2.48      val typedef_prop =
    2.49        Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
    2.50  
    2.51 -    fun typedef_att (theory, nonempty) =
    2.52 +    fun typedef_result (theory, nonempty) =
    2.53        theory
    2.54        |> add_typedecls [(t, vs, mx)]
    2.55        |> Theory.add_consts_i
    2.56 -       ((if no_def then [] else [(name, setT, NoSyn)]) @
    2.57 +       ((if def then [(name, setT, NoSyn)] else []) @
    2.58          [(Rep_name, newT --> oldT, NoSyn),
    2.59           (Abs_name, oldT --> newT, NoSyn)])
    2.60 -      |> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes))
    2.61 -       [Logic.mk_defpair (setC, set)])
    2.62 -      |> PureThy.add_axioms_i [((typedef_name, typedef_prop),
    2.63 +      |> (if def then (apsnd (Some o hd) oo (PureThy.add_defs_i false o map Thm.no_attributes))
    2.64 +           [Logic.mk_defpair (setC, set)]
    2.65 +          else rpair None)
    2.66 +      |>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
    2.67            [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])]
    2.68 -      |> (fn (theory', axm) =>
    2.69 -        let fun make th = Drule.standard (th OF axm) in
    2.70 -          rpair (hd axm) (theory'
    2.71 -          |> (#1 oo PureThy.add_thms)
    2.72 -            ([((Rep_name, make Rep), []),
    2.73 -              ((Rep_name ^ "_inverse", make Rep_inverse), []),
    2.74 -              ((Abs_name ^ "_inverse", make Abs_inverse), []),
    2.75 -              ((Rep_name ^ "_inject", make Rep_inject), []),
    2.76 -              ((Abs_name ^ "_inject", make Abs_inject), []),
    2.77 -              ((Rep_name ^ "_cases", make Rep_cases),
    2.78 -                [RuleCases.case_names [Rep_name], InductAttrib.cases_set_global full_name]),
    2.79 -              ((Abs_name ^ "_cases", make Abs_cases),
    2.80 -                [RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]),
    2.81 -              ((Rep_name ^ "_induct", make Rep_induct),
    2.82 -                [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
    2.83 -              ((Abs_name ^ "_induct", make Abs_induct),
    2.84 -                [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]))
    2.85 -        end);
    2.86 +      |> (fn ((theory', [type_definition]), set_def) =>
    2.87 +        let
    2.88 +          fun make th = Drule.standard (th OF [type_definition]);
    2.89 +          val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
    2.90 +              Rep_cases, Abs_cases, Rep_induct, Abs_induct]) =
    2.91 +            theory' |> PureThy.add_thms
    2.92 +              ([((Rep_name, make Rep), []),
    2.93 +                ((Rep_name ^ "_inverse", make Rep_inverse), []),
    2.94 +                ((Abs_name ^ "_inverse", make Abs_inverse), []),
    2.95 +                ((Rep_name ^ "_inject", make Rep_inject), []),
    2.96 +                ((Abs_name ^ "_inject", make Abs_inject), []),
    2.97 +                ((Rep_name ^ "_cases", make Rep_cases),
    2.98 +                  [RuleCases.case_names [Rep_name], InductAttrib.cases_set_global full_name]),
    2.99 +                ((Abs_name ^ "_cases", make Abs_cases),
   2.100 +                  [RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]),
   2.101 +                ((Rep_name ^ "_induct", make Rep_induct),
   2.102 +                  [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
   2.103 +                ((Abs_name ^ "_induct", make Abs_induct),
   2.104 +                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]);
   2.105 +          val result = {type_definition = type_definition, set_def = set_def,
   2.106 +            Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
   2.107 +            Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
   2.108 +            Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
   2.109 +        in ((theory'', type_definition), result) end);
   2.110  
   2.111  
   2.112      (* errors *)
   2.113 @@ -198,32 +209,41 @@
   2.114      (*test theory errors now!*)
   2.115      val test_thy = Theory.copy thy;
   2.116      val _ = (test_thy,
   2.117 -      setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_att;
   2.118 +      setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_result;
   2.119  
   2.120 -  in (cset, goal, goal_pat, typedef_att) end
   2.121 +  in (cset, goal, goal_pat, typedef_result) end
   2.122    handle ERROR => err_in_typedef name;
   2.123  
   2.124  
   2.125  (* add_typedef interfaces *)
   2.126  
   2.127 -fun gen_add_typedef prep_term no_def name typ set names thms tac thy =
   2.128 +fun gen_typedef prep_term def name typ set opt_morphs names thms tac thy =
   2.129    let
   2.130 -    val (cset, goal, _, typedef_att) = prepare_typedef prep_term no_def name typ set None thy;
   2.131 -    val result = prove_nonempty thy cset goal (names, thms, tac);
   2.132 -  in (thy, result) |> typedef_att end;
   2.133 +    val (cset, goal, _, typedef_result) =
   2.134 +      prepare_typedef prep_term def name typ set opt_morphs thy;
   2.135 +    val non_empty = prove_nonempty thy cset goal (names, thms, tac);
   2.136 +    val ((thy', _), result) = (thy, non_empty) |> typedef_result;
   2.137 +  in (thy', result) end;
   2.138  
   2.139 -val add_typedef = gen_add_typedef read_term false;
   2.140 -val add_typedef_i = gen_add_typedef cert_term false;
   2.141 -val add_typedef_i_no_def = gen_add_typedef cert_term true;
   2.142 -fun add_typedef_no_result x y z = #1 oooo add_typedef x y z;
   2.143 +fun sane_typedef prep_term def name typ set opt_morphs tac =
   2.144 +  gen_typedef prep_term def name typ set opt_morphs [] [] (Some tac);
   2.145 +
   2.146 +fun add_typedef_x name typ set names thms tac =
   2.147 +  #1 o gen_typedef read_term true name typ set None names thms tac;
   2.148 +
   2.149 +val add_typedef = sane_typedef read_term;
   2.150 +val add_typedef_i = sane_typedef cert_term;
   2.151  
   2.152  
   2.153  (* typedef_proof interface *)
   2.154  
   2.155  fun gen_typedef_proof prep_term ((name, typ, set, opt_morphs), comment) int thy =
   2.156 -  let val (_, goal, goal_pat, att) = prepare_typedef prep_term false name typ set opt_morphs thy in
   2.157 -    thy |>
   2.158 -    IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
   2.159 +  let
   2.160 +    val (_, goal, goal_pat, att_result) =
   2.161 +      prepare_typedef prep_term true name typ set opt_morphs thy;
   2.162 +    val att = #1 o att_result;
   2.163 +  in
   2.164 +    thy |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
   2.165    end;
   2.166  
   2.167  val typedef_proof = gen_typedef_proof read_term;
     3.1 --- a/src/HOL/thy_syntax.ML	Wed Oct 17 20:24:37 2001 +0200
     3.2 +++ b/src/HOL/thy_syntax.ML	Wed Oct 17 20:25:19 2001 +0200
     3.3 @@ -280,7 +280,7 @@
     3.4  val _ = ThySyn.add_syntax
     3.5   ["intrs", "monos", "con_defs", "congs", "simpset", "|",
     3.6    "and", "distinct", "inject", "induct"]
     3.7 - [axm_section "typedef" "|> TypedefPackage.add_typedef_no_result" typedef_decl,
     3.8 + [axm_section "typedef" "|> TypedefPackage.add_typedef_x" typedef_decl,
     3.9    section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
    3.10    section "inductive" 	"" (inductive_decl false),
    3.11    section "coinductive"	"" (inductive_decl true),