adaptions in class_package
authorhaftmann
Wed Jul 12 17:00:30 2006 +0200 (2006-07-12)
changeset 20106a3d4b4eb35b9
parent 20105 454f4be984b7
child 20107 239a0efd38b2
adaptions in class_package
src/HOL/ex/Classpackage.thy
src/Pure/Tools/class_package.ML
     1.1 --- a/src/HOL/ex/Classpackage.thy	Wed Jul 12 17:00:22 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Wed Jul 12 17:00:30 2006 +0200
     1.3 @@ -223,8 +223,6 @@
     1.4    from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
     1.5  qed
     1.6  
     1.7 -print_theorems
     1.8 -
     1.9  instance group < monoid
    1.10  proof
    1.11    fix x :: "'a::group"
     2.1 --- a/src/Pure/Tools/class_package.ML	Wed Jul 12 17:00:22 2006 +0200
     2.2 +++ b/src/Pure/Tools/class_package.ML	Wed Jul 12 17:00:30 2006 +0200
     2.3 @@ -46,9 +46,6 @@
     2.4    val sortcontext_of_typ: theory -> typ -> sortcontext
     2.5    val sortlookup: theory -> sort * typ -> classlookup list
     2.6    val sortlookups_const: theory -> string * typ -> classlookup list list
     2.7 -
     2.8 -  val use_instance2: bool ref;
     2.9 -  val the_propnames: theory -> class -> string list
    2.10  end;
    2.11  
    2.12  structure ClassPackage: CLASS_PACKAGE =
    2.13 @@ -206,6 +203,7 @@
    2.14        ClassData (classd, Symtab.insert_list eq_thm (tyco, thm) instd))
    2.15    );
    2.16  
    2.17 +
    2.18  (* name handling *)
    2.19  
    2.20  fun certify_class thy class =
    2.21 @@ -517,30 +515,21 @@
    2.22      val const_names = (map (NameSpace.base o fst o snd)
    2.23        o maps (#consts o fst o the_class_data theory)
    2.24        o the_ancestry theory) [class];
    2.25 -    val prop_tab = AList.make (the_propnames theory)
    2.26 -      (the_ancestry theory sort);
    2.27 -    fun mk_thm_names (superclass, prop_names) =
    2.28 -      let
    2.29 -        val thm_name_base = NameSpace.append "local" (space_implode "_" const_names);
    2.30 -        val export_name = class ^ "_" ^ superclass;
    2.31 -      in (export_name, map (Name o NameSpace.append thm_name_base) prop_names) end;
    2.32 -    val notes_tab_proto = map mk_thm_names prop_tab;
    2.33 -    fun test_note thy thmref =
    2.34 -      can (Locale.note_thmss PureThy.corollaryK loc_name
    2.35 -        [(("", []), [(thmref, [])])]) (Theory.copy thy);
    2.36 -    val notes_tab = map_filter (fn (export_name, thm_names) =>
    2.37 -     case filter (test_note theory) thm_names
    2.38 -     of [] => NONE
    2.39 -      | thm_names' => SOME (export_name, thm_names')) notes_tab_proto;
    2.40 -    val _ = writeln ("fishing for ");
    2.41 -    val _ = print notes_tab;
    2.42 -    fun after_qed thy = thy;
    2.43 -    fun after_qed''' thy =
    2.44 -      fold (fn supclass =>
    2.45 -        AxClass.prove_classrel (class, supclass)
    2.46 -          (ALLGOALS (K (intro_classes_tac [])) THEN
    2.47 -            (ALLGOALS o resolve_tac o flat) [])
    2.48 -      ) sort thy;
    2.49 +    fun get_thms thy =
    2.50 +      the_ancestry thy sort
    2.51 +      |> AList.make (the_propnames thy)
    2.52 +      |> map (apsnd (map (NameSpace.append (loc_name))))
    2.53 +      |> map_filter (fn (superclass, thm_names) =>
    2.54 +          case map_filter (try (PureThy.get_thm thy o Name)) thm_names
    2.55 +           of [] => NONE
    2.56 +            | thms => SOME (superclass, thms));
    2.57 +    fun after_qed thy =
    2.58 +      thy
    2.59 +      |> `get_thms
    2.60 +      |-> fold (fn (supclass, thms) => I
    2.61 +            AxClass.prove_classrel (class, supclass)
    2.62 +              (ALLGOALS (K (intro_classes_tac [])) THEN
    2.63 +                (ALLGOALS o ProofContext.fact_tac) thms))
    2.64    in
    2.65      theory
    2.66      |> do_proof after_qed (loc_name, loc_expr)
    2.67 @@ -605,7 +594,7 @@
    2.68  
    2.69  fun sortlookups_const thy (c, typ_ctxt) =
    2.70    let
    2.71 -    val typ_decl = case AxClass.class_of thy c
    2.72 +    val typ_decl = case AxClass.class_of_param thy c
    2.73       of NONE => Sign.the_const_type thy c
    2.74        | SOME class => case the_consts_sign thy class of (v, cs) =>
    2.75            (Logic.legacy_varifyT o subst_clsvar v (TFree (v, [class])))
    2.76 @@ -629,15 +618,13 @@
    2.77  
    2.78  val (classK, instanceK) = ("class", "instance")
    2.79  
    2.80 -val use_instance2 = ref false;
    2.81 -
    2.82 -fun wrap_add_instance_sort (class, sort) thy =
    2.83 -  if ! use_instance2
    2.84 +fun wrap_add_instance_sort ((class, sort), use_interp) thy =
    2.85 +  if use_interp
    2.86      andalso forall (is_some o lookup_class_data thy) (Sign.read_sort thy sort)
    2.87    then
    2.88      instance_sort (class, sort) thy
    2.89    else
    2.90 -    axclass_instance_sort (class, sort) thy
    2.91 +    axclass_instance_sort (class, sort) thy;
    2.92  
    2.93  val parse_inst =
    2.94    (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 P.sort --| P.$$$ ")")) [] -- P.xname --| P.$$$ "::" -- P.sort)
    2.95 @@ -665,7 +652,7 @@
    2.96  
    2.97  val instanceP =
    2.98    OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
    2.99 -      P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> wrap_add_instance_sort
   2.100 +      P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) -- P.opt_keyword "open" >> wrap_add_instance_sort
   2.101        || P.opt_thm_name ":" -- (parse_inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop))
   2.102             >> (fn (("", []), (((tyco, asorts), sort), [])) => axclass_instance_arity I (tyco, asorts, sort)
   2.103                  | (natts, (inst, defs)) => instance_arity inst natts defs)