1.1 --- a/src/Pure/Isar/class.ML	Thu Oct 25 19:27:52 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Oct 25 19:27:53 2007 +0200
     1.3 @@ -26,6 +26,8 @@
     1.4    val refresh_syntax: class -> Proof.context -> Proof.context
     1.5    val intro_classes_tac: thm list -> tactic
     1.6    val default_intro_classes_tac: thm list -> tactic
     1.7 +  val prove_subclass: class * class -> thm list -> Proof.context
     1.8 +    -> theory -> theory
     1.9    val print_classes: theory -> unit
    1.10    val uncheck: bool ref
    1.11  
    1.12 @@ -61,6 +63,13 @@
    1.13        (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    1.14    #> ProofContext.theory_of;
    1.15  
    1.16 +fun prove_interpretation_in tac after_qed (name, expr) =
    1.17 +  Locale.interpretation_in_locale
    1.18 +      (ProofContext.theory after_qed) (name, expr)
    1.19 +  #> Proof.global_terminal_proof
    1.20 +      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    1.21 +  #> ProofContext.theory_of;
    1.22 +
    1.23  fun OF_LAST thm1 thm2 = thm1 RSN (Thm.nprems_of thm2, thm2);
    1.24  
    1.25  fun strip_all_ofclass thy sort =
    1.26 @@ -315,29 +324,31 @@
    1.27      (*partial morphism of canonical interpretation*)
    1.28    intro: thm,
    1.29    defs: thm list,
    1.30 -  operations: (string * ((term * (typ * int)) * (term * typ))) list
    1.31 -    (*constant name ~> ((locale term,
    1.32 -        (constant constraint, instantiaton index of class typ)), locale term & typ for uncheck)*)
    1.33 +  operations: (string * (term * (typ * int))) list,
    1.34 +    (*constant name ~> (locale term,
    1.35 +        (constant constraint, instantiaton index of class typ))*)
    1.36 +  unchecks: (term * term) list
    1.37  };
    1.38  
    1.39  fun rep_class_data (ClassData d) = d;
    1.40  fun mk_class_data ((consts, base_sort, inst, morphism, intro),
    1.41 -    (defs, operations)) =
    1.42 +    (defs, (operations, unchecks))) =
    1.43    ClassData { consts = consts, base_sort = base_sort, inst = inst,
    1.44      morphism = morphism, intro = intro, defs = defs,
    1.45 -    operations = operations };
    1.46 +    operations = operations, unchecks = unchecks };
    1.47  fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro,
    1.48 -    defs, operations }) =
    1.49 +    defs, operations, unchecks }) =
    1.50    mk_class_data (f ((consts, base_sort, inst, morphism, intro),
    1.51 -    (defs, operations)));
    1.52 +    (defs, (operations, unchecks))));
    1.53  fun merge_class_data _ (ClassData { consts = consts,
    1.54      base_sort = base_sort, inst = inst, morphism = morphism, intro = intro,
    1.55 -    defs = defs1, operations = operations1 },
    1.56 +    defs = defs1, operations = operations1, unchecks = unchecks1 },
    1.57    ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _,
    1.58 -    defs = defs2, operations = operations2 }) =
    1.59 +    defs = defs2, operations = operations2, unchecks = unchecks2 }) =
    1.60    mk_class_data ((consts, base_sort, inst, morphism, intro),
    1.61      (Thm.merge_thms (defs1, defs2),
    1.62 -      AList.merge (op =) (K true) (operations1, operations2)));
    1.63 +      (AList.merge (op =) (K true) (operations1, operations2),
    1.64 +        Library.merge (op aconv o pairself snd) (unchecks1, unchecks2))));
    1.65  
    1.66  structure ClassData = TheoryDataFun
    1.67  (
    1.68 @@ -383,7 +394,8 @@
    1.69  fun these_operations thy =
    1.70    maps (#operations o the_class_data thy) o ancestry thy;
    1.71  
    1.72 -fun local_operation thy = AList.lookup (op =) o these_operations thy;
    1.73 +fun these_unchecks thy =
    1.74 +  maps (#unchecks o the_class_data thy) o ancestry thy;
    1.75  
    1.76  fun sups_base_sort thy sort =
    1.77    let
    1.78 @@ -435,30 +447,35 @@
    1.79  
    1.80  fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
    1.81    let
    1.82 -    val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
    1.83 -      (c, ((Free v_ty, (Logic.varifyT ty, 0)), (Free v_ty, ty')))) cs;
    1.84 +    val operations = map (fn (v_ty, (c, ty)) =>
    1.85 +      (c, ((Free v_ty, (Logic.varifyT ty, 0))))) cs;
    1.86 +    val unchecks = map (fn ((v, ty'), (c, _)) =>
    1.87 +      (Free (v, Type.strip_sorts ty'), Const (c, Type.strip_sorts ty'))) cs;
    1.88      val cs = (map o pairself) fst cs;
    1.89      val add_class = Graph.new_node (class,
    1.90 -        mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], operations)))
    1.91 +        mk_class_data ((cs, base_sort, map (SOME o Const) inst, phi, intro), ([], (operations, unchecks))))
    1.92        #> fold (curry Graph.add_edge class) superclasses;
    1.93    in
    1.94      ClassData.map add_class thy
    1.95    end;
    1.96  
    1.97 -fun register_operation class ((c, (t, t_rev)), some_def) thy =
    1.98 +fun register_operation class (c, ((t, some_t_rev), some_def)) thy =
    1.99    let
   1.100      val ty = Sign.the_const_constraint thy c;
   1.101      val typargs = Sign.const_typargs thy (c, ty);
   1.102      val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v | _ => false) typargs;
   1.103 -    val t_rev' = (map_types o map_atyps)
   1.104 -      (fn ty as TFree (v, _) => if Name.aT = v then TFree (v, []) else ty | ty => ty) t_rev;
   1.105 -    val ty' = Term.fastype_of t_rev';
   1.106 +    fun mk_uncheck t_rev =
   1.107 +      let
   1.108 +        val t_rev' = map_types Type.strip_sorts t_rev;
   1.109 +        val ty' = Term.fastype_of t_rev';
   1.110 +      in (t_rev', Const (c, ty')) end;
   1.111 +    val some_t_rev' = Option.map mk_uncheck some_t_rev;
   1.112    in
   1.113      thy
   1.114      |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
   1.115 -      (fn (defs, operations) =>
   1.116 +      (fn (defs, (operations, unchecks)) =>
   1.117          (fold cons (the_list some_def) defs,
   1.118 -          (c, ((t, (ty, typidx)), (t_rev', ty'))) :: operations))
   1.119 +          ((c, (t, (ty, typidx))) :: operations, fold cons (the_list some_t_rev') unchecks)))
   1.120    end;
   1.121  
   1.122  
   1.123 @@ -550,6 +567,56 @@
   1.124    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   1.125      "apply some intro/elim rule")]);
   1.126  
   1.127 +fun subclass_rule thy (sub, sup) =
   1.128 +  let
   1.129 +    val ctxt = Locale.init sub thy;
   1.130 +    val ctxt_thy = ProofContext.init thy;
   1.131 +    val props =
   1.132 +      Locale.global_asms_of thy sup
   1.133 +      |> maps snd
   1.134 +      |> map (ObjectLogic.ensure_propT thy);
   1.135 +    fun tac { prems, context } =
   1.136 +      Locale.intro_locales_tac true context prems
   1.137 +        ORELSE ALLGOALS assume_tac;
   1.138 +  in
   1.139 +    Goal.prove_multi ctxt [] [] props tac
   1.140 +    |> map (Assumption.export false ctxt ctxt_thy)
   1.141 +    |> Variable.export ctxt ctxt_thy
   1.142 +  end;
   1.143 +
   1.144 +fun prove_single_subclass (sub, sup) thms ctxt thy =
   1.145 +  let
   1.146 +    val ctxt_thy = ProofContext.init thy;
   1.147 +    val subclass_rule = Conjunction.intr_balanced thms
   1.148 +      |> Assumption.export false ctxt ctxt_thy
   1.149 +      |> singleton (Variable.export ctxt ctxt_thy);
   1.150 +    val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub]));
   1.151 +    val sub_ax = #axioms (AxClass.get_info thy sub);
   1.152 +    val classrel =
   1.153 +      #intro (AxClass.get_info thy sup)
   1.154 +      |> Drule.instantiate' [SOME sub_inst] []
   1.155 +      |> OF_LAST (subclass_rule OF sub_ax)
   1.156 +      |> strip_all_ofclass thy (Sign.super_classes thy sup)
   1.157 +      |> Thm.strip_shyps
   1.158 +  in
   1.159 +    thy
   1.160 +    |> AxClass.add_classrel classrel
   1.161 +    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac thms))
   1.162 +         I (sub, Locale.Locale sup)
   1.163 +    |> ClassData.map (Graph.add_edge (sub, sup))
   1.164 +  end;
   1.165 +
   1.166 +fun prove_subclass (sub, sup) thms ctxt thy =
   1.167 +  let
   1.168 +    val supclasses = Sign.complete_sort thy [sup]
   1.169 +      |> filter_out (fn class => Sign.subsort thy ([sub], [class]));
   1.170 +    fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms);
   1.171 +  in
   1.172 +    thy
   1.173 +    |> fold_rev (fn sup' => prove_single_subclass (sub, sup')
   1.174 +         (transform sup') ctxt) supclasses
   1.175 + end;
   1.176 +
   1.177  
   1.178  (** classes and class target **)
   1.179  
   1.180 @@ -560,7 +627,7 @@
   1.181      constraints: (string * typ) list,
   1.182      base_sort: sort,
   1.183      local_operation: string * typ -> (typ * term) option,
   1.184 -    rews: (term * term) list,
   1.185 +    unchecks: (term * term) list,
   1.186      passed: bool
   1.187    } option;
   1.188    fun init _ = NONE;
   1.189 @@ -568,27 +635,30 @@
   1.190  
   1.191  fun synchronize_syntax thy sups base_sort ctxt =
   1.192    let
   1.193 +    (* constraints *)
   1.194      val operations = these_operations thy sups;
   1.195 -
   1.196 -    (* constraints *)
   1.197 -    fun local_constraint (c, ((_, (ty, _)),_ )) =
   1.198 +    fun local_constraint (c, (_, (ty, _))) =
   1.199        let
   1.200          val ty' = ty
   1.201            |> map_atyps (fn ty as TVar ((v, 0), _) =>
   1.202                 if v = Name.aT then TVar ((v, 0), base_sort) else ty)
   1.203            |> SOME;
   1.204        in (c, ty') end
   1.205 -    val constraints = (map o apsnd) (fst o snd o fst) operations;
   1.206 +    val constraints = (map o apsnd) (fst o snd) operations;
   1.207  
   1.208      (* check phase *)
   1.209      val typargs = Consts.typargs (ProofContext.consts_of ctxt);
   1.210 -    fun check_const (c, ty) ((t, (_, idx)), _) =
   1.211 +    fun check_const (c, ty) (t, (_, idx)) =
   1.212        ((nth (typargs (c, ty)) idx), t);
   1.213      fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c
   1.214        |> Option.map (check_const c_ty);
   1.215  
   1.216      (* uncheck phase *)
   1.217 -    val rews = map (fn (c, (_, (t, ty))) => (t, Const (c, ty))) operations;
   1.218 +    val basify =
   1.219 +      map_atyps (fn ty as TFree (v, _) => if Name.aT = v then TFree (v, base_sort)
   1.220 +        else ty | ty => ty);
   1.221 +    val unchecks = these_unchecks thy sups
   1.222 +      |> (map o pairself o map_types) basify;
   1.223    in
   1.224      ctxt
   1.225      |> fold (ProofContext.add_const_constraint o local_constraint) operations
   1.226 @@ -596,7 +666,7 @@
   1.227          constraints = constraints,
   1.228          base_sort = base_sort,
   1.229          local_operation = local_operation,
   1.230 -        rews = rews,
   1.231 +        unchecks = unchecks,
   1.232          passed = false
   1.233        }))
   1.234    end;
   1.235 @@ -608,9 +678,9 @@
   1.236    in synchronize_syntax thy [class] base_sort ctxt end;
   1.237  
   1.238  val mark_passed = (ClassSyntax.map o Option.map)
   1.239 -  (fn { constraints, base_sort, local_operation, rews, passed } =>
   1.240 +  (fn { constraints, base_sort, local_operation, unchecks, passed } =>
   1.241      { constraints = constraints, base_sort = base_sort,
   1.242 -      local_operation = local_operation, rews = rews, passed = true });
   1.243 +      local_operation = local_operation, unchecks = unchecks, passed = true });
   1.244  
   1.245  fun sort_term_check ts ctxt =
   1.246    let
   1.247 @@ -647,9 +717,9 @@
   1.248    let
   1.249      (*FIXME abbreviations*)
   1.250      val thy = ProofContext.theory_of ctxt;
   1.251 -    val rews = (#rews o the o ClassSyntax.get) ctxt;
   1.252 +    val unchecks = (#unchecks o the o ClassSyntax.get) ctxt;
   1.253      val ts' = if ! uncheck
   1.254 -      then map (Pattern.rewrite_term thy rews []) ts else ts;
   1.255 +      then map (Pattern.rewrite_term thy unchecks []) ts else ts;
   1.256    in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
   1.257  
   1.258  fun init_ctxt thy sups base_sort ctxt =
   1.259 @@ -802,6 +872,7 @@
   1.260      val prfx = class_prefix class;
   1.261      val thy' = thy |> Sign.add_path prfx;
   1.262      val phi = morphism thy' class;
   1.263 +    val base_sort = (#base_sort o the_class_data thy) class;
   1.264  
   1.265      val c' = Sign.full_name thy' c;
   1.266      val dict' = (map_types Logic.unvarifyT o Morphism.term phi) dict;
   1.267 @@ -817,7 +888,7 @@
   1.268      |> Thm.add_def false (c, def_eq)
   1.269      |>> Thm.symmetric
   1.270      |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
   1.271 -          #> register_operation class ((c', (dict, dict')), SOME (Thm.varifyT def)))
   1.272 +          #> register_operation class (c', ((dict, SOME dict'), SOME (Thm.varifyT def))))
   1.273      |> Sign.restore_naming thy
   1.274      |> Sign.add_const_constraint (c', SOME ty')
   1.275    end;
   1.276 @@ -834,8 +905,7 @@
   1.277      val c' = Sign.full_name thy' c;
   1.278      val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class])
   1.279      val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs;
   1.280 -    val rhs'' = map_types Logic.unvarifyT rhs';
   1.281 -    val ty' = Term.fastype_of rhs'';
   1.282 +    val ty' = (Logic.unvarifyT o Term.fastype_of) rhs';
   1.283  
   1.284      val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
   1.285      val ty'' = (Type.strip_sorts o Logic.unvarifyT) (Sign.the_const_constraint thy' c'');
   1.286 @@ -846,7 +916,7 @@
   1.287      |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
   1.288      |> Sign.add_const_constraint (c', SOME ty')
   1.289      |> Sign.notation true prmode [(Const (c', ty'), mx)]
   1.290 -    |> register_operation class ((c', (rhs, rhs'')), NONE)
   1.291 +    |> register_operation class (c', ((rhs, NONE), NONE))
   1.292      |> Sign.restore_naming thy
   1.293    end;
   1.294