some steps towards explicit class target for canonical interpretation
authorhaftmann
Tue Jul 29 08:15:39 2008 +0200 (2008-07-29)
changeset 2769024738db98d34
parent 27689 268a7d02cf7a
child 27691 ce171cbd4b93
some steps towards explicit class target for canonical interpretation
src/Pure/Isar/class.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/class.ML	Tue Jul 29 08:15:38 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Jul 29 08:15:39 2008 +0200
     1.3 @@ -14,10 +14,14 @@
     1.4      -> theory -> string * Proof.context
     1.5  
     1.6    val init: class -> theory -> Proof.context
     1.7 -  val declare: string -> Markup.property list
     1.8 +  val declare: class -> Markup.property list
     1.9 +    -> (string * mixfix) * term -> theory -> theory
    1.10 +  val abbrev: class -> Syntax.mode -> Markup.property list
    1.11      -> (string * mixfix) * term -> theory -> theory
    1.12 -  val abbrev: string -> Syntax.mode -> Markup.property list
    1.13 -    -> (string * mixfix) * term -> theory -> theory
    1.14 +  val note: class -> string
    1.15 +    -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.16 +    -> theory -> (bstring * thm list) list * theory
    1.17 +  val declaration: class -> declaration -> theory -> theory
    1.18    val refresh_syntax: class -> Proof.context -> Proof.context
    1.19  
    1.20    val intro_classes_tac: thm list -> tactic
    1.21 @@ -58,9 +62,6 @@
    1.22  
    1.23  (** auxiliary **)
    1.24  
    1.25 -val classN = "class";
    1.26 -val introN = "intro";
    1.27 -
    1.28  fun prove_interpretation tac prfx_atts expr inst =
    1.29    Locale.interpretation_i I prfx_atts expr inst
    1.30    #> Proof.global_terminal_proof
    1.31 @@ -283,17 +284,20 @@
    1.32        (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
    1.33          (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
    1.34            Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
    1.35 -    val instantiate_base_sort = instantiate thy base_sort;
    1.36 -    val instantiate_class = instantiate thy [class];
    1.37 +    (*fun inst thy sort thm = (tracing (makestring thm); instantiate thy sort thm);
    1.38 +    val instantiate = inst;*)
    1.39      val (proto_assm_intro, locale_intro) = Locale.intros thy class
    1.40        |> pairself (try the_single);
    1.41      val axiom_premises = map_filter (#axiom o the_class_data thy) sups
    1.42        @ the_list assm_axiom;
    1.43      val axiom = locale_intro
    1.44 -      |> Option.map (Drule.standard o (fn thm => thm OF axiom_premises) o instantiate_class)
    1.45 +      |> Option.map (Thm.close_derivation o Drule.standard' o (fn thm => thm OF axiom_premises) o instantiate thy [class])
    1.46        |> (fn x as SOME _ => x | NONE => assm_axiom);
    1.47      val lift_axiom = case axiom
    1.48 -     of SOME axiom => (fn thm => Thm.implies_elim thm axiom)
    1.49 +     of SOME axiom => (fn thm => ((*tracing "-(morphism)-";
    1.50 +          tracing (makestring thm);
    1.51 +          tracing (makestring axiom);*)
    1.52 +          Thm.implies_elim thm axiom))
    1.53        | NONE => I;
    1.54  
    1.55      (*dynamic parts of morphism*)
    1.56 @@ -301,17 +305,17 @@
    1.57        (map (Logic.dest_equals o Thm.prop_of) defs) [];
    1.58      fun subst_term thy defs = map_aterms subst_aterm #> rew_term thy defs
    1.59        #> map_types subst_typ;
    1.60 -    fun subst_thm defs = Drule.standard' #> instantiate_class #> lift_axiom
    1.61 +    fun subst_thm thy defs = Drule.standard' #> instantiate thy [class] #> lift_axiom
    1.62        #> MetaSimplifier.rewrite_rule defs;
    1.63      fun morphism thy defs =
    1.64        Morphism.typ_morphism subst_typ
    1.65        $> Morphism.term_morphism (subst_term thy defs)
    1.66 -      $> Morphism.thm_morphism (subst_thm defs);
    1.67 +      $> Morphism.thm_morphism (subst_thm thy defs);
    1.68  
    1.69      (*class rules*)
    1.70      val defs = these_defs thy sups;
    1.71      val assm_intro = proto_assm_intro
    1.72 -      |> Option.map instantiate_base_sort
    1.73 +      |> Option.map (instantiate thy base_sort)
    1.74        |> Option.map (MetaSimplifier.rewrite_rule defs)
    1.75        |> Option.map Thm.close_derivation;
    1.76      val class_intro = (#intro o AxClass.get_info thy) class;
    1.77 @@ -344,6 +348,8 @@
    1.78      |> pair (morphism, axiom, assm_intro, of_class)
    1.79    end;
    1.80  
    1.81 +fun class_interpretation class facts defs thy = thy;
    1.82 +
    1.83  fun class_interpretation class facts defs thy =
    1.84    let
    1.85      val consts = map (apsnd fst o snd) (these_params thy [class]);
    1.86 @@ -406,7 +412,6 @@
    1.87        "apply some intro/elim rule")]));
    1.88  
    1.89  
    1.90 -
    1.91  (** classes and class target **)
    1.92  
    1.93  (* class context syntax *)
    1.94 @@ -464,6 +469,72 @@
    1.95    |> init_ctxt [class] ((#base_sort o the_class_data thy) class);
    1.96  
    1.97  
    1.98 +(* class target *)
    1.99 +
   1.100 +fun declare class pos ((c, mx), dict) thy =
   1.101 +  let
   1.102 +    val prfx = class_prefix class;
   1.103 +    val thy' = thy |> Sign.add_path prfx;
   1.104 +    val phi = morphism thy' class;
   1.105 +
   1.106 +    val c' = Sign.full_name thy' c;
   1.107 +    val dict' = Morphism.term phi dict;
   1.108 +    val dict_def = map_types Logic.unvarifyT dict';
   1.109 +    val ty' = Term.fastype_of dict_def;
   1.110 +    val ty'' = Type.strip_sorts ty';
   1.111 +    val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
   1.112 +    fun get_axiom thy = ((Thm.varifyT o Thm.get_axiom_i thy) c', thy);
   1.113 +  in
   1.114 +    thy'
   1.115 +    |> Sign.declare_const pos (c, ty'', mx) |> snd
   1.116 +    |> Thm.add_def false false (c, def_eq)
   1.117 +    |>> Thm.symmetric
   1.118 +    ||>> get_axiom
   1.119 +    |-> (fn (def, def') => class_interpretation class [def] [Thm.prop_of def]
   1.120 +      #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
   1.121 +      #> PureThy.store_thm (c ^ "_raw", def')
   1.122 +      #> snd)
   1.123 +    |> Sign.restore_naming thy
   1.124 +    |> Sign.add_const_constraint (c', SOME ty')
   1.125 +  end;
   1.126 +
   1.127 +fun abbrev class prmode pos ((c, mx), rhs) thy =
   1.128 +  let
   1.129 +    val prfx = class_prefix class;
   1.130 +    val thy' = thy |> Sign.add_path prfx;
   1.131 +
   1.132 +    val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
   1.133 +      (these_operations thy [class]);
   1.134 +    val c' = Sign.full_name thy' c;
   1.135 +    val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
   1.136 +    val rhs'' = map_types Logic.varifyT rhs';
   1.137 +    val ty' = Term.fastype_of rhs';
   1.138 +  in
   1.139 +    thy'
   1.140 +    |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs'') |> snd
   1.141 +    |> Sign.add_const_constraint (c', SOME ty')
   1.142 +    |> Sign.notation true prmode [(Const (c', ty'), mx)]
   1.143 +    |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
   1.144 +    |> Sign.restore_naming thy
   1.145 +  end;
   1.146 +
   1.147 +fun note class kind facts thy =
   1.148 +  let
   1.149 +    val phi = morphism thy class;
   1.150 +    val facts' = facts
   1.151 +      |> PureThy.map_facts (Morphism.thm phi) 
   1.152 +      |> Attrib.map_facts (Attrib.attribute_i thy);
   1.153 +  in
   1.154 +    thy
   1.155 +    |> Sign.add_path (class_prefix class)
   1.156 +    |> PureThy.note_thmss kind facts'
   1.157 +    ||> Sign.restore_naming thy
   1.158 +  end;
   1.159 +
   1.160 +fun declaration class decl thy =
   1.161 +  Context.theory_map (decl (morphism thy class)) thy;
   1.162 +
   1.163 +
   1.164  (* class definition *)
   1.165  
   1.166  local
   1.167 @@ -559,6 +630,9 @@
   1.168      val class = Sign.full_name thy bname;
   1.169      val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
   1.170        prep_spec thy raw_supclasses raw_elems;
   1.171 +    fun assms_of thy class =
   1.172 +      Locale.elems thy class
   1.173 +      |> map_filter (fn Element.Notes (_, facts) => SOME facts | _ => NONE);
   1.174    in
   1.175      thy
   1.176      |> Locale.add_locale_i "" bname mergeexpr elems
   1.177 @@ -570,7 +644,10 @@
   1.178      #-> (fn (morphism, axiom, assm_intro, of_class) =>
   1.179          add_class_data ((class, sups), (params, base_sort,
   1.180            map snd param_map, morphism, axiom, assm_intro, of_class))
   1.181 -    #> class_interpretation class (the_list axiom) []))
   1.182 +    (*#> `(fn thy => assms_of thy class)
   1.183 +    #-> (fn assms => fold_map (note class Thm.assumptionK) assms
   1.184 +    #> snd*)
   1.185 +    #> class_interpretation class (the_list axiom) []))(*)*)
   1.186      |> init class
   1.187      |> pair class
   1.188    end;
   1.189 @@ -583,55 +660,6 @@
   1.190  end; (*local*)
   1.191  
   1.192  
   1.193 -(* class target *)
   1.194 -
   1.195 -fun declare class pos ((c, mx), dict) thy =
   1.196 -  let
   1.197 -    val prfx = class_prefix class;
   1.198 -    val thy' = thy |> Sign.add_path prfx;
   1.199 -    val phi = morphism thy' class;
   1.200 -
   1.201 -    val c' = Sign.full_name thy' c;
   1.202 -    val dict' = Morphism.term phi dict;
   1.203 -    val dict_def = map_types Logic.unvarifyT dict';
   1.204 -    val ty' = Term.fastype_of dict_def;
   1.205 -    val ty'' = Type.strip_sorts ty';
   1.206 -    val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
   1.207 -    fun get_axiom thy = ((Thm.varifyT o Thm.get_axiom_i thy) c', thy);
   1.208 -  in
   1.209 -    thy'
   1.210 -    |> Sign.declare_const pos (c, ty'', mx) |> snd
   1.211 -    |> Thm.add_def false false (c, def_eq)
   1.212 -    |>> Thm.symmetric
   1.213 -    ||>> get_axiom
   1.214 -    |-> (fn (def, def') => class_interpretation class [def] [Thm.prop_of def]
   1.215 -      #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
   1.216 -      #> PureThy.store_thm (c ^ "_raw", def')
   1.217 -      #> snd)
   1.218 -    |> Sign.restore_naming thy
   1.219 -    |> Sign.add_const_constraint (c', SOME ty')
   1.220 -  end;
   1.221 -
   1.222 -fun abbrev class prmode pos ((c, mx), rhs) thy =
   1.223 -  let
   1.224 -    val prfx = class_prefix class;
   1.225 -    val thy' = thy |> Sign.add_path prfx;
   1.226 -
   1.227 -    val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
   1.228 -      (these_operations thy [class]);
   1.229 -    val c' = Sign.full_name thy' c;
   1.230 -    val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
   1.231 -    val rhs'' = map_types Logic.varifyT rhs';
   1.232 -    val ty' = Term.fastype_of rhs';
   1.233 -  in
   1.234 -    thy'
   1.235 -    |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs'') |> snd
   1.236 -    |> Sign.add_const_constraint (c', SOME ty')
   1.237 -    |> Sign.notation true prmode [(Const (c', ty'), mx)]
   1.238 -    |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
   1.239 -    |> Sign.restore_naming thy
   1.240 -  end;
   1.241 -
   1.242  
   1.243  (** instantiation target **)
   1.244  
     2.1 --- a/src/Pure/Isar/theory_target.ML	Tue Jul 29 08:15:38 2008 +0200
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Jul 29 08:15:39 2008 +0200
     2.3 @@ -70,7 +70,7 @@
     2.4  
     2.5  (* target declarations *)
     2.6  
     2.7 -fun target_decl add (Target {target, ...}) d lthy =
     2.8 +fun target_decl add (Target {target, is_class, ...}) d lthy =
     2.9    let
    2.10      val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
    2.11      val d0 = Morphism.form d';
    2.12 @@ -82,6 +82,7 @@
    2.13      else
    2.14        lthy
    2.15        |> LocalTheory.target (add target d')
    2.16 +      (*|> is_class ? LocalTheory.raw_theory (Class.declaration target d')*)
    2.17    end;
    2.18  
    2.19  val type_syntax = target_decl Locale.add_type_syntax;
    2.20 @@ -147,7 +148,7 @@
    2.21    |> ProofContext.note_thmss_i kind facts
    2.22    ||> ProofContext.restore_naming ctxt;
    2.23  
    2.24 -fun notes (Target {target, is_locale, ...}) kind facts lthy =
    2.25 +fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy =
    2.26    let
    2.27      val thy = ProofContext.theory_of lthy;
    2.28      val full = LocalTheory.full_name lthy;
    2.29 @@ -166,10 +167,9 @@
    2.30        (Sign.qualified_names
    2.31          #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
    2.32          #> Sign.restore_naming thy)
    2.33 -
    2.34      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
    2.35      |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
    2.36 -
    2.37 +    (*|> is_class ? LocalTheory.raw_theory (Class.note target kind target_facts #> snd)*)
    2.38      |> note_local kind local_facts
    2.39    end;
    2.40