src/Pure/proofterm.ML

    | AbsP of string * term option * proof
    | % of proof * term option
    | %% of proof * proof
    | Hyp of term
    | PAxm of string * term * typ list option
-   | OfClass of typ * class
+   | PClass of typ * class
    | Oracle of string * term * typ list option
    | PThm of thm_header * thm_body
   and proof_body = PBody of
     {oracles: ((string * Position.T) * term option) Ord_List.T,
      thms: (serial * thm_node) Ord_List.T,

  | AbsP of string * term option * proof
  | op % of proof * term option
  | op %% of proof * proof
  | Hyp of term
  | PAxm of string * term * typ list option
- | OfClass of typ * class
+ | PClass of typ * class
  | Oracle of string * term * typ list option
  | PThm of thm_header * thm_body
 and proof_body = PBody of
   {oracles: ((string * Position.T) * term option) Ord_List.T,
    thms: (serial * thm_node) Ord_List.T,

   fn AbsP (a, b, c) => ([a], pair (option (term consts)) (proof consts) (b, c)),
   fn a % b => ([], pair (proof consts) (option (term consts)) (a, b)),
   fn a %% b => ([], pair (proof consts) (proof consts) (a, b)),
   fn Hyp a => ([], term consts a),
   fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
-  fn OfClass (a, b) => ([b], typ a),
+  fn PClass (a, b) => ([b], typ a),
   fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
   fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
     ([int_atom serial, theory_name, name],
       pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
         (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]

   fn AbsP (a, SOME b, c) => ([a], pair (standard_term consts) (standard_proof consts) (b, c)),
   fn a % SOME b => ([], pair (standard_proof consts) (standard_term consts) (a, b)),
   fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)),
   fn Hyp a => ([], standard_term consts a),
   fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
-  fn OfClass (T, c) => ([c], typ T),
+  fn PClass (T, c) => ([c], typ T),
   fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)),
   fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
     ([int_atom serial, theory_name, name], list typ Ts)];
 
 in

   fn ([a], b) => let val (c, d) = pair (option (term consts)) (proof consts) b in AbsP (a, c, d) end,
   fn ([], a) => op % (pair (proof consts) (option (term consts)) a),
   fn ([], a) => op %% (pair (proof consts) (proof consts) a),
   fn ([], a) => Hyp (term consts a),
   fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end,
-  fn ([b], a) => OfClass (typ a, b),
+  fn ([b], a) => PClass (typ a, b),
   fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end,
   fn ([a, b, c], d) =>
     let
       val ((e, (f, (g, h)))) =
         pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) d;

             handle Same.SAME => prf % Same.map_option term t)
       | proof (prf1 %% prf2) =
           (proof prf1 %% Same.commit proof prf2
             handle Same.SAME => prf1 %% proof prf2)
       | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
-      | proof (OfClass T_c) = ofclass T_c
+      | proof (PClass T_c) = ofclass T_c
       | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
       | proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) =
           PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body)
       | proof _ = raise Same.SAME;
   in proof end;
 
-fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => OfClass (typ T, c));
+fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => PClass (typ T, c));
 fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;
 
 fun same eq f x =
   let val x' = f x
   in if eq (x, x') then raise Same.SAME else x' end;

   | fold_proof_terms_types f g (prf % SOME t) = fold_proof_terms_types f g prf #> f t
   | fold_proof_terms_types f g (prf % NONE) = fold_proof_terms_types f g prf
   | fold_proof_terms_types f g (prf1 %% prf2) =
       fold_proof_terms_types f g prf1 #> fold_proof_terms_types f g prf2
   | fold_proof_terms_types _ g (PAxm (_, _, SOME Ts)) = fold g Ts
-  | fold_proof_terms_types _ g (OfClass (T, _)) = g T
+  | fold_proof_terms_types _ g (PClass (T, _)) = g T
   | fold_proof_terms_types _ g (Oracle (_, _, SOME Ts)) = fold g Ts
   | fold_proof_terms_types _ g (PThm ({types = SOME Ts, ...}, _)) = fold g Ts
   | fold_proof_terms_types _ _ _ = I;
 
 fun maxidx_proof prf = fold_proof_terms_types Term.maxidx_term Term.maxidx_typ prf;

   | size_of_proof (prf % _) = 1 + size_of_proof prf
   | size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2
   | size_of_proof _ = 1;
 
 fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
-  | change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
+  | change_types (SOME [T]) (PClass (_, c)) = PClass (T, c)
   | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
   | change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) =
       PThm (thm_header serial pos theory_name name prop types, thm_body)
   | change_types _ prf = prf;
 

       | norm (prf1 %% prf2) =
           (norm prf1 %% Same.commit norm prf2
             handle Same.SAME => prf1 %% norm prf2)
       | norm (PAxm (s, prop, Ts)) =
           PAxm (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
-      | norm (OfClass (T, c)) =
-          OfClass (htypeT Envir.norm_type_same T, c)
+      | norm (PClass (T, c)) =
+          PClass (htypeT Envir.norm_type_same T, c)
       | norm (Oracle (s, prop, Ts)) =
           Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
       | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) =
           PThm (thm_header i p theory_name a t
             (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)

           handle Same.SAME => prf % Same.map_option (same (op =) (lift'' Us Ts)) t)
       | lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2
           handle Same.SAME => prf1 %% lift' Us Ts prf2)
       | lift' _ _ (PAxm (s, prop, Ts)) =
           PAxm (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
-      | lift' _ _ (OfClass (T, c)) =
-          OfClass (Logic.incr_tvar_same inc T, c)
+      | lift' _ _ (PClass (T, c)) =
+          PClass (Logic.incr_tvar_same inc T, c)
       | lift' _ _ (Oracle (s, prop, Ts)) =
           Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
       | lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) =
           PThm (thm_header i p theory_name s prop
             ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), thm_body)

 fun const_proof mk name prop =
   let
     val args = prop_args prop;
     val ({outer_constraints, ...}, prop1) = Logic.unconstrainT [] prop;
     val head = mk (name, prop1, NONE);
-  in proof_combP (proof_combt' (head, args), map OfClass outer_constraints) end;
+  in proof_combP (proof_combt' (head, args), map PClass outer_constraints) end;
 
 val axm_proof = const_proof PAxm;
 val oracle_proof = const_proof Oracle;
 
 val shrink_proof =

              orelse has_duplicates (op =)
                (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
              orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
       | shrink' _ _ ts _ (Hyp t) = ([], false, map (pair false) ts, Hyp t)
       | shrink' _ _ ts _ (prf as MinProof) = ([], false, map (pair false) ts, prf)
-      | shrink' _ _ ts _ (prf as OfClass _) = ([], false, map (pair false) ts, prf)
+      | shrink' _ _ ts _ (prf as PClass _) = ([], false, map (pair false) ts, prf)
       | shrink' _ _ ts prfs prf =
           let
             val prop =
               (case prf of
                 PAxm (_, prop, _) => prop

       | mtch Ts i j inst (prf1, AbsP (_, _, prf2)) =
           mtch Ts (i+1) j inst (incr_pboundvars 1 0 prf1 %% PBound 0, prf2)
       | mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) =
           if s1 = s2 then optmatch matchTs inst (opTs, opUs)
           else raise PMatch
-      | mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) =
+      | mtch Ts i j inst (PClass (T1, c1), PClass (T2, c2)) =
           if c1 = c2 then matchT inst (T1, T2)
           else raise PMatch
       | mtch Ts i j inst
             (PThm ({name = name1, prop = prop1, types = types1, ...}, _),
               PThm ({name = name2, prop = prop2, types = types2, ...}, _)) =

       | subst plev tlev (Hyp (Var (xi, _))) =
           (case AList.lookup (op =) pinst xi of
             NONE => raise Same.SAME
           | SOME prf' => incr_pboundvars plev tlev prf')
       | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
-      | subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
+      | subst _ _ (PClass (T, c)) = PClass (substT T, c)
       | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
       | subst _ _ (PThm ({serial = i, pos = p, theory_name, name = id, prop, types}, thm_body)) =
           PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body)
       | subst _ _ _ = raise Same.SAME;
   in fn t => subst 0 0 t handle Same.SAME => t end;

 
   in case (head_of prf1, head_of prf2) of
         (_, Hyp (Var _)) => true
       | (Hyp (Var _), _) => true
       | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
-      | (OfClass (_, c), OfClass (_, d)) => c = d andalso matchrands prf1 prf2
+      | (PClass (_, c), PClass (_, d)) => c = d andalso matchrands prf1 prf2
       | (PThm ({name = a, prop = propa, ...}, _), PThm ({name = b, prop = propb, ...}, _)) =>
           a = b andalso propa = propb andalso matchrands prf1 prf2
       | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
       | (AbsP _, _) =>  true   (*because of possible eta equality*)
       | (Abst _, _) =>  true

         (fn TVar ((a, i), S) => subst_same (TVar ((a, i - shift), S)) | A => subst_same A);
   in Same.commit (map_proof_types_same subst_type_same) prf end;
 
 fun guess_name (PThm ({name, ...}, _)) = name
   | guess_name (prf %% Hyp _) = guess_name prf
-  | guess_name (prf %% OfClass _) = guess_name prf
+  | guess_name (prf %% PClass _) = guess_name prf
   | guess_name (prf % NONE) = guess_name prf
   | guess_name (prf % SOME (Var _)) = guess_name prf
   | guess_name _ = "";
 
 

                end)
       | mk_cnstrts env _ _ vTs (prf as PThm ({prop, types = opTs, ...}, _)) =
           mk_cnstrts_atom env vTs prop opTs prf
       | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) =
           mk_cnstrts_atom env vTs prop opTs prf
-      | mk_cnstrts env _ _ vTs (prf as OfClass (T, c)) =
+      | mk_cnstrts env _ _ vTs (prf as PClass (T, c)) =
           mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf
       | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) =
           mk_cnstrts_atom env vTs prop opTs prf
       | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs)
       | mk_cnstrts _ _ _ _ MinProof = raise MIN_PROOF ()

       Const ("Pure.imp", _) $ _ $ Q => Q
     | _ => error "prop_of: ==> expected")
   | prop_of0 _ (Hyp t) = t
   | prop_of0 _ (PThm ({prop, types = SOME Ts, ...}, _)) = prop_of_atom prop Ts
   | prop_of0 _ (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
-  | prop_of0 _ (OfClass (T, c)) = Logic.mk_of_class (T, c)
+  | prop_of0 _ (PClass (T, c)) = Logic.mk_of_class (T, c)
   | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
   | prop_of0 _ _ = error "prop_of: partial proof object";
 
 val prop_of' = Envir.beta_eta_contract oo prop_of0;
 val prop_of = prop_of' [];

     val proof =
       if unconstrain then
         proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args)
       else
         proof_combP (proof_combt' (head, args),
-          map OfClass (#outer_constraints ucontext) @ map Hyp hyps);
+          map PClass (#outer_constraints ucontext) @ map Hyp hyps);
   in (thm, proof) end;
 
 in
 
 fun thm_proof thy = prepare_thm_proof false thy;