class package now using Locale.interpretation_i
authorhaftmann
Wed Feb 14 10:06:17 2007 +0100 (2007-02-14 ago)
changeset 22321e5cddafe2629
parent 22320 d5260836d662
child 22322 b9924abb8c66
class package now using Locale.interpretation_i
src/HOL/ex/Classpackage.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Tools/class_package.ML
     1.1 --- a/src/HOL/ex/Classpackage.thy	Wed Feb 14 10:06:16 2007 +0100
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Wed Feb 14 10:06:17 2007 +0100
     1.3 @@ -219,7 +219,7 @@
     1.4    with cancel show ?thesis ..
     1.5  qed
     1.6  
     1.7 -instance group < monoid
     1.8 +instance advanced group < monoid
     1.9  proof unfold_locales
    1.10    fix x
    1.11    from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Feb 14 10:06:16 2007 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 14 10:06:17 2007 +0100
     2.3 @@ -427,14 +427,16 @@
     2.4      -- P.opt_begin
     2.5      >> (fn ((bname, (supclasses, elems)), begin) =>
     2.6          Toplevel.begin_local_theory begin
     2.7 -          (ClassPackage.class_e bname supclasses elems #-> TheoryTarget.begin true)));
     2.8 +          (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin true)));
     2.9  
    2.10  val instanceP =
    2.11    OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
    2.12        P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    2.13 -           >> ClassPackage.instance_sort_e
    2.14 +           >> ClassPackage.instance_class_cmd
    2.15 +      || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    2.16 +           >> ClassPackage.instance_sort_cmd (*experimental: by interpretation of locales*)
    2.17        || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    2.18 -           >> (fn (arities, defs) => ClassPackage.instance_arity_e arities defs)
    2.19 +           >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
    2.20      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    2.21  
    2.22  val print_classesP =
     3.1 --- a/src/Pure/Tools/class_package.ML	Wed Feb 14 10:06:16 2007 +0100
     3.2 +++ b/src/Pure/Tools/class_package.ML	Wed Feb 14 10:06:17 2007 +0100
     3.3 @@ -11,19 +11,21 @@
     3.4  
     3.5    val class: bstring -> class list -> Element.context_i Locale.element list -> theory ->
     3.6      string * Proof.context
     3.7 -  val class_e: bstring -> string list -> Element.context Locale.element list -> theory ->
     3.8 +  val class_cmd: bstring -> string list -> Element.context Locale.element list -> theory ->
     3.9      string * Proof.context
    3.10    val instance_arity: ((bstring * sort list) * sort) list
    3.11      -> ((bstring * Attrib.src list) * term) list
    3.12      -> theory -> Proof.state
    3.13 -  val instance_arity_e: ((bstring * string list) * string) list
    3.14 +  val instance_arity_cmd: ((bstring * string list) * string) list
    3.15      -> ((bstring * Attrib.src list) * string) list
    3.16      -> theory -> Proof.state
    3.17    val prove_instance_arity: tactic -> ((string * sort list) * sort) list
    3.18      -> ((bstring * Attrib.src list) * term) list
    3.19      -> theory -> theory
    3.20 +  val instance_class: class * class -> theory -> Proof.state
    3.21 +  val instance_class_cmd: string * string -> theory -> Proof.state
    3.22    val instance_sort: class * sort -> theory -> Proof.state
    3.23 -  val instance_sort_e: string * string -> theory -> Proof.state
    3.24 +  val instance_sort_cmd: string * string -> theory -> Proof.state
    3.25    val prove_instance_sort: tactic -> class * sort -> theory -> theory
    3.26  
    3.27    val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool
    3.28 @@ -101,7 +103,7 @@
    3.29      #-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs) axioms_prop
    3.30      #-> (fn class => `(fn thy => AxClass.get_definition thy class)
    3.31      #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
    3.32 -    #> pair (class, ((intro, (map snd axioms_prop, axioms)), cs))))))
    3.33 +    #> pair (class, ((intro, (maps snd axioms_prop, axioms)), cs))))))
    3.34    end;
    3.35  
    3.36  
    3.37 @@ -137,7 +139,7 @@
    3.38        | _ => SOME raw_name;
    3.39    in (c, (insts, ((name, t), atts))) end;
    3.40  
    3.41 -fun read_def_e thy = gen_read_def thy Attrib.intern_src read_axm;
    3.42 +fun read_def_cmd thy = gen_read_def thy Attrib.intern_src read_axm;
    3.43  fun read_def thy = gen_read_def thy (K I) (K I);
    3.44  
    3.45  fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory =
    3.46 @@ -208,7 +210,7 @@
    3.47      |-> (fn (cs, _) => do_proof (after_qed cs) arities)
    3.48    end;
    3.49  
    3.50 -fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity read_def_e do_proof;
    3.51 +fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;
    3.52  fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof;
    3.53  fun tactic_proof tac after_qed arities =
    3.54    fold (fn arity => AxClass.prove_arity arity tac) arities
    3.55 @@ -216,7 +218,7 @@
    3.56  
    3.57  in
    3.58  
    3.59 -val instance_arity_e = instance_arity_e' axclass_instance_arity;
    3.60 +val instance_arity_cmd = instance_arity_e' axclass_instance_arity;
    3.61  val instance_arity = instance_arity' axclass_instance_arity;
    3.62  val prove_instance_arity = instance_arity' o tactic_proof;
    3.63  
    3.64 @@ -359,6 +361,7 @@
    3.65  
    3.66  (* tactics and methods *)
    3.67  
    3.68 +(*FIXME adjust these when minimal intro rules are at hand*)
    3.69  fun intro_classes_tac facts st =
    3.70    let
    3.71      val thy = Thm.theory_of_thm st;
    3.72 @@ -366,9 +369,10 @@
    3.73      val intro_classes_tac = ALLGOALS
    3.74        (Method.insert_tac facts THEN' REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros thy)))
    3.75          THEN Tactic.distinct_subgoals_tac;
    3.76 -    val intro_locales_tac = Locale.intro_locales_tac true ctxt facts;
    3.77 +    val intro_locales_tac = SOMEGOAL (SELECT_GOAL (Locale.intro_locales_tac true ctxt facts))
    3.78 +      THEN Tactic.distinct_subgoals_tac;
    3.79    in
    3.80 -    (intro_classes_tac THEN TRY intro_locales_tac) st
    3.81 +    (intro_classes_tac THEN REPEAT (intro_locales_tac ORELSE intro_locales_tac)) st
    3.82    end;
    3.83  
    3.84  fun default_intro_classes_tac [] = intro_classes_tac []
    3.85 @@ -384,27 +388,13 @@
    3.86    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
    3.87      "apply some intro/elim rule")]);
    3.88  
    3.89 -
    3.90 -(* FIXME workarounds for locale package *)
    3.91 +(* tactical interfaces to locale commands *)
    3.92  
    3.93 -fun prove_interpretation (prfx, atts) expr insts tac thy =
    3.94 -  let
    3.95 -    fun ad_hoc_term (Const (c, ty)) =
    3.96 -          let
    3.97 -            val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_typ thy))) ty;
    3.98 -            val s = c ^ "::" ^ Pretty.output p;
    3.99 -          in s end
   3.100 -      | ad_hoc_term t =
   3.101 -          let
   3.102 -            val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_term thy))) t;
   3.103 -            val s = Pretty.output p;
   3.104 -          in s end;
   3.105 -  in
   3.106 -    thy
   3.107 -    |> Locale.interpretation I (prfx, atts) expr (map (Option.map ad_hoc_term) insts)
   3.108 -    |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
   3.109 -    |> ProofContext.theory_of
   3.110 -  end;
   3.111 +fun prove_interpretation tac prfx_atts expr insts thy =
   3.112 +  thy
   3.113 +  |> Locale.interpretation_i I prfx_atts expr insts
   3.114 +  |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
   3.115 +  |> ProofContext.theory_of;
   3.116  
   3.117  fun prove_interpretation_in tac after_qed (name, expr) thy =
   3.118    thy
   3.119 @@ -462,46 +452,46 @@
   3.120  
   3.121  fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
   3.122    let
   3.123 -    val elems = fold_rev (fn Locale.Elem e => cons e | _ => I) raw_elems [];
   3.124 -      (*FIXME add constrains here to elements as hint for locale*)
   3.125 +    (*FIXME need proper concept for reading locale statements*)
   3.126 +    fun subst_classtyvar (_, _) =
   3.127 +          TFree (AxClass.param_tyvarname, [])
   3.128 +      | subst_classtyvar (v, sort) =
   3.129 +          error ("Sort constraint illegal in type class, for type variable " ^ v ^ "::" ^ Sign.string_of_sort thy sort);
   3.130 +    (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
   3.131 +      typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
   3.132 +    val elems = fold_rev (fn Locale.Elem e => cons e | _ => I)
   3.133 +      raw_elems []; (*FIXME make include possible here?*)
   3.134      val supclasses = map (prep_class thy) raw_supclasses;
   3.135      val supsort =
   3.136        supclasses
   3.137        |> Sign.certify_sort thy
   3.138        |> (fn [] => Sign.defaultS thy | S => S);    (*FIXME Why syntax defaultS?*)
   3.139 -    val supexpr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses);
   3.140 +    val supexpr = Locale.Merge
   3.141 +      (map (Locale.Locale o #locale o the_class_data thy) supclasses);
   3.142 +    val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
   3.143      val supconsts = AList.make
   3.144 -      (the o AList.lookup (op =) (param_map thy supclasses))
   3.145 -      ((map (fst o fst) o Locale.parameters_of_expr thy) supexpr);
   3.146 -    fun check_locale thy name_locale =
   3.147 +      (the o AList.lookup (op =) (param_map thy supclasses)) (map fst supparams);
   3.148 +      (*FIXME include proper*)
   3.149 +    (*val elems_constrains = map
   3.150 +      (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*)
   3.151 +    fun extract_params thy name_locale =
   3.152        let
   3.153 -        val tfrees =
   3.154 -          []
   3.155 -          |> fold (fold Term.add_tfrees o snd) (Locale.global_asms_of thy name_locale)
   3.156 -          |> fold (Term.add_tfreesT o snd o fst) (Locale.parameters_of thy name_locale);
   3.157 -      in case tfrees
   3.158 -       of [(_, _)] => ()
   3.159 -        (*| [(_, sort)] => error ("Additional sort constraint on class variable: "
   3.160 -            ^ Sign.string_of_sort thy sort) FIXME what to do about this?*)
   3.161 -        | [] => error ("No type variable in class specification")
   3.162 -        | tfrees => error ("More than one type variable in class specification: " ^
   3.163 -            (commas o map fst) tfrees)
   3.164 +        val params = Locale.parameters_of thy name_locale;
   3.165 +      in
   3.166 +        (map (fst o fst) params, params
   3.167 +        |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, Sign.defaultS thy)))
   3.168 +        |> (map o apsnd) (fork_mixfix false true #> fst)
   3.169 +        |> chop (length supconsts)
   3.170 +        |> snd)
   3.171        end;
   3.172 -    fun extract_params thy name_locale =
   3.173 -      Locale.parameters_of thy name_locale
   3.174 -      |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, [])))
   3.175 -      |> (map o apsnd) (fork_mixfix false true #> fst)
   3.176 -      |> chop (length supconsts)
   3.177 -      |> snd;
   3.178      fun extract_assumes name_locale params thy cs =
   3.179        let
   3.180          val consts = supconsts @ (map (fst o fst) params ~~ cs);
   3.181 -        (*FIXME is this type handling correct?*)
   3.182          fun subst (Free (c, ty)) =
   3.183                Const ((fst o the o AList.lookup (op =) consts) c, ty)
   3.184            | subst t = t;
   3.185          fun prep_asm ((name, atts), ts) =
   3.186 -          (*FIXME*)
   3.187 +          (*FIXME: name handling?*)
   3.188            ((NameSpace.base name, map (Attrib.attribute thy) atts), (map o map_aterms) subst ts);
   3.189        in
   3.190          Locale.global_asms_of thy name_locale
   3.191 @@ -510,33 +500,37 @@
   3.192      fun extract_axiom_names thy name_locale =
   3.193        name_locale
   3.194        |> Locale.global_asms_of thy
   3.195 -      |> map (NameSpace.base o fst o fst) (*FIXME*)
   3.196 -    fun mk_const thy class (c, ty) =
   3.197 -      Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty);
   3.198 +      |> map (NameSpace.base o fst o fst) (*FIXME - is finally dropped*)
   3.199 +    fun mk_instT class = Symtab.empty
   3.200 +      |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
   3.201 +    fun mk_inst class param_names cs =
   3.202 +      Symtab.empty
   3.203 +      |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
   3.204 +           (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
   3.205 +    fun make_witness t thm = Element.make_witness t (Goal.protect thm);
   3.206    in
   3.207      thy
   3.208 -    |> add_locale bname supexpr elems
   3.209 +    |> add_locale bname supexpr ((*elems_constrains @*) elems)
   3.210      |-> (fn name_locale => ProofContext.theory_result (
   3.211 -      tap (fn thy => check_locale thy name_locale)
   3.212 -      #> `(fn thy => extract_params thy name_locale)
   3.213 -      #-> (fn params =>
   3.214 +      `(fn thy => extract_params thy name_locale)
   3.215 +      #-> (fn (param_names, params) =>
   3.216          axclass_params (bname, supsort) params (extract_assumes name_locale params)
   3.217        #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
   3.218          `(fn thy => extract_axiom_names thy name_locale)
   3.219        #-> (fn axiom_names =>
   3.220          add_class_data ((name_axclass, supclasses),
   3.221            (name_locale, map (fst o fst) params ~~ map fst consts,
   3.222 -            map2 Element.make_witness (map Logic.mk_conjunction_list ax_terms) ax_axioms, axiom_names))
   3.223 -      #> prove_interpretation (Logic.const_of_class bname, [])
   3.224 -          (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts))
   3.225 -            ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   3.226 +            map2 make_witness ax_terms ax_axioms, axiom_names))
   3.227 +      #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   3.228 +          (Logic.const_of_class bname, []) (Locale.Locale name_locale)
   3.229 +          (mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts))
   3.230        #> pair name_axclass
   3.231        )))))
   3.232    end;
   3.233  
   3.234  in
   3.235  
   3.236 -val class_e = gen_class (Locale.add_locale true) read_class;
   3.237 +val class_cmd = gen_class (Locale.add_locale true) read_class;
   3.238  val class = gen_class (Locale.add_locale_i true) certify_class;
   3.239  
   3.240  end; (*local*)
   3.241 @@ -547,21 +541,26 @@
   3.242    let
   3.243      val class = prep_class theory raw_class;
   3.244      val sort = prep_sort theory raw_sort;
   3.245 -    val is_class = is_some o lookup_class_data theory;
   3.246 -  in if is_class class andalso forall is_class sort then
   3.247 +  in
   3.248      theory
   3.249      |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort)
   3.250 -  else case sort
   3.251 -   of [class'] =>
   3.252 -        theory
   3.253 -        |> axclass_instance_sort (class, class')
   3.254 -    | _ => error ("Exactly one class expected: " ^ Sign.string_of_sort theory sort)
   3.255 +  end;
   3.256 +
   3.257 +fun gen_instance_class prep_class (raw_class, raw_superclass) theory =
   3.258 +  let
   3.259 +    val class = prep_class theory raw_class;
   3.260 +    val superclass = prep_class theory raw_superclass;
   3.261 +  in
   3.262 +    theory
   3.263 +    |> axclass_instance_sort (class, superclass)
   3.264    end;
   3.265  
   3.266  in
   3.267  
   3.268 -val instance_sort_e = gen_instance_sort Sign.read_class Sign.read_sort;
   3.269 +val instance_sort_cmd = gen_instance_sort Sign.read_class Sign.read_sort;
   3.270  val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort;
   3.271 +val instance_class_cmd = gen_instance_class Sign.read_class;
   3.272 +val instance_class = gen_instance_class Sign.certify_class;
   3.273  
   3.274  end; (* local *)
   3.275