misc tuning and modernisation;
authorwenzelm
Thu Dec 11 00:42:52 2008 +0100 (2008-12-11)
changeset 29056dc08e3990c77
parent 29055 edaef19665e6
child 29057 d219318fd89a
misc tuning and modernisation;
src/HOL/Tools/typedef_package.ML
src/HOL/Typedef.thy
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Dec 10 22:05:58 2008 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Dec 11 00:42:52 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Tools/typedef_package.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     1.7  
     1.8  Gordon/HOL-style type definitions: create a new syntactic type
     1.9 @@ -27,22 +26,6 @@
    1.10  structure TypedefPackage: TYPEDEF_PACKAGE =
    1.11  struct
    1.12  
    1.13 -(** theory context references **)
    1.14 -
    1.15 -val type_definitionN = "Typedef.type_definition";
    1.16 -
    1.17 -val Rep = @{thm "type_definition.Rep"};
    1.18 -val Rep_inverse = @{thm "type_definition.Rep_inverse"};
    1.19 -val Abs_inverse = @{thm "type_definition.Abs_inverse"};
    1.20 -val Rep_inject = @{thm "type_definition.Rep_inject"};
    1.21 -val Abs_inject = @{thm "type_definition.Abs_inject"};
    1.22 -val Rep_cases = @{thm "type_definition.Rep_cases"};
    1.23 -val Abs_cases = @{thm "type_definition.Abs_cases"};
    1.24 -val Rep_induct = @{thm "type_definition.Rep_induct"};
    1.25 -val Abs_induct = @{thm "type_definition.Abs_induct"};
    1.26 -
    1.27 -
    1.28 -
    1.29  (** type definitions **)
    1.30  
    1.31  (* theory data *)
    1.32 @@ -108,58 +91,56 @@
    1.33      val RepC = Const (full Rep_name, newT --> oldT);
    1.34      val AbsC = Const (full Abs_name, oldT --> newT);
    1.35  
    1.36 -    val set' = if def then setC else set;
    1.37 -    fun mk_inhabited A =
    1.38 +    val A = if def then setC else set;
    1.39 +    val goal =
    1.40        HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
    1.41 -    val goal = mk_inhabited set';
    1.42 -    val term_binding = (the_default (name, 0) (Syntax.read_variable name), SOME set)
    1.43 +    val term_binding = (the_default (name, 0) (Syntax.read_variable name), SOME set);
    1.44  
    1.45      val typedef_name = "type_definition_" ^ name;
    1.46      val typedefC =
    1.47 -      Const (type_definitionN, (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
    1.48 -    val typedef_prop =
    1.49 -      Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
    1.50 -    val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' [];
    1.51 +      Const (@{const_name type_definition},
    1.52 +        (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
    1.53 +    val typedef_prop = Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A));
    1.54 +    val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) A [];
    1.55  
    1.56 -    val (set_def, thy') = if def then
    1.57 +    val (set_def, thy') =
    1.58 +      if def then
    1.59          thy
    1.60          |> Sign.add_consts_i [(name, setT', NoSyn)]
    1.61          |> PureThy.add_defs false [Thm.no_attributes (PrimitiveDefs.mk_defpair (setC, set))]
    1.62          |-> (fn [th] => pair (SOME th))
    1.63        else (NONE, thy);
    1.64  
    1.65 -    fun typedef_result inhabited = 
    1.66 +    fun typedef_result inhabited =
    1.67        ObjectLogic.typedecl (t, vs, mx)
    1.68        #> snd
    1.69        #> Sign.add_consts_i
    1.70          [(Rep_name, newT --> oldT, NoSyn),
    1.71           (Abs_name, oldT --> newT, NoSyn)]
    1.72        #> PureThy.add_axioms [((typedef_name, typedef_prop),
    1.73 -          [apsnd (fn cond_axm => inhabited RS cond_axm)])]
    1.74 +          [Thm.rule_attribute (fn _ => fn cond_axm => inhabited RS cond_axm)])]
    1.75        ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
    1.76        ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
    1.77        #-> (fn [type_definition] => fn thy1 =>
    1.78          let
    1.79            fun make th = Drule.standard (th OF [type_definition]);
    1.80 -          val abs_inject = make Abs_inject;
    1.81 -          val abs_inverse = make Abs_inverse;
    1.82            val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
    1.83                Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
    1.84              thy1
    1.85              |> Sign.add_path name
    1.86              |> PureThy.add_thms
    1.87 -              ([((Rep_name, make Rep), []),
    1.88 -                ((Rep_name ^ "_inverse", make Rep_inverse), []),
    1.89 -                ((Abs_name ^ "_inverse", abs_inverse), []),
    1.90 -                ((Rep_name ^ "_inject", make Rep_inject), []),
    1.91 -                ((Abs_name ^ "_inject", abs_inject), []),
    1.92 -                ((Rep_name ^ "_cases", make Rep_cases),
    1.93 +              ([((Rep_name, make @{thm type_definition.Rep}), []),
    1.94 +                ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []),
    1.95 +                ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []),
    1.96 +                ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []),
    1.97 +                ((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []),
    1.98 +                ((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}),
    1.99                    [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]),
   1.100 -                ((Abs_name ^ "_cases", make Abs_cases),
   1.101 +                ((Abs_name ^ "_cases", make @{thm type_definition.Abs_cases}),
   1.102                    [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
   1.103 -                ((Rep_name ^ "_induct", make Rep_induct),
   1.104 +                ((Rep_name ^ "_induct", make @{thm type_definition.Rep_induct}),
   1.105                    [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]),
   1.106 -                ((Abs_name ^ "_induct", make Abs_induct),
   1.107 +                ((Abs_name ^ "_induct", make @{thm type_definition.Abs_induct}),
   1.108                    [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
   1.109              ||> Sign.parent_path;
   1.110            val info = {rep_type = oldT, abs_type = newT,
   1.111 @@ -175,6 +156,7 @@
   1.112            |> pair (full_tname, info)
   1.113          end);
   1.114  
   1.115 +
   1.116      (* errors *)
   1.117  
   1.118      fun show_names pairs = commas_quote (map fst pairs);
   1.119 @@ -207,7 +189,7 @@
   1.120    handle ERROR msg => err_in_typedef msg name;
   1.121  
   1.122  
   1.123 -(* add_typedef interface *)
   1.124 +(* add_typedef: tactic interface *)
   1.125  
   1.126  fun add_typedef def opt_name typ set opt_morphs tac thy =
   1.127    let
   1.128 @@ -220,7 +202,7 @@
   1.129    in typedef_result non_empty thy' end;
   1.130  
   1.131  
   1.132 -(* Isar typedef interface *)
   1.133 +(* typedef: proof interface *)
   1.134  
   1.135  local
   1.136  
   1.137 @@ -229,12 +211,11 @@
   1.138      val ((_, goal, term_binding, set_def, typedef_result), thy') =
   1.139        prepare_typedef prep_term def name typ set opt_morphs thy;
   1.140      fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th);
   1.141 -  in 
   1.142 -    Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy')
   1.143 -    |> Proof.add_binds_i [term_binding] 
   1.144 -    |> (if def 
   1.145 -        then Seq.hd o Proof.refine (Method.Basic (Method.unfold [the set_def], Position.none))
   1.146 -        else I)
   1.147 +  in
   1.148 +    ProofContext.init thy'
   1.149 +    |> Proof.theorem_i NONE after_qed [[(goal, [])]]
   1.150 +    |> Proof.add_binds_i [term_binding]
   1.151 +    |> Proof.unfolding_i [[(the_list set_def, [])]]
   1.152    end;
   1.153  
   1.154  in
   1.155 @@ -248,7 +229,7 @@
   1.156  
   1.157  (** outer syntax **)
   1.158  
   1.159 -local structure P = OuterParse and K = OuterKeyword in
   1.160 +local structure P = OuterParse in
   1.161  
   1.162  val _ = OuterKeyword.keyword "morphisms";
   1.163  
   1.164 @@ -263,11 +244,13 @@
   1.165    typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
   1.166  
   1.167  val _ =
   1.168 -  OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
   1.169 +  OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
   1.170 +    OuterKeyword.thy_goal
   1.171      (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
   1.172  
   1.173 +end;
   1.174 +
   1.175 +
   1.176  val setup = TypedefInterpretation.init;
   1.177  
   1.178  end;
   1.179 -
   1.180 -end;
     2.1 --- a/src/HOL/Typedef.thy	Wed Dec 10 22:05:58 2008 +0100
     2.2 +++ b/src/HOL/Typedef.thy	Thu Dec 11 00:42:52 2008 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/Typedef.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Markus Wenzel, TU Munich
     2.7  *)
     2.8  
     2.9 @@ -116,15 +115,10 @@
    2.10  
    2.11  end
    2.12  
    2.13 -use "Tools/typedef_package.ML"
    2.14 -use "Tools/typecopy_package.ML"
    2.15 -use "Tools/typedef_codegen.ML"
    2.16 +use "Tools/typedef_package.ML" setup TypedefPackage.setup
    2.17 +use "Tools/typecopy_package.ML" setup TypecopyPackage.setup
    2.18 +use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
    2.19  
    2.20 -setup {*
    2.21 -  TypedefPackage.setup
    2.22 -  #> TypecopyPackage.setup
    2.23 -  #> TypedefCodegen.setup
    2.24 -*}
    2.25  
    2.26  text {* This class is just a workaround for classes without parameters;
    2.27    it shall disappear as soon as possible. *}