src/Pure/drule.ML
changeset 561 95225e63ef02
parent 400 3c2c40c87112
child 575 74f0e5fce609
     1.1 --- a/src/Pure/drule.ML	Fri Aug 19 15:39:52 1994 +0200
     1.2 +++ b/src/Pure/drule.ML	Fri Aug 19 15:40:10 1994 +0200
     1.3 @@ -12,6 +12,8 @@
     1.4    sig
     1.5    structure Thm : THM
     1.6    local open Thm  in
     1.7 +  val add_defs: (string * string) list -> theory -> theory
     1.8 +  val add_defs_i: (string * term) list -> theory -> theory
     1.9    val asm_rl: thm
    1.10    val assume_ax: theory -> string -> thm
    1.11    val COMP: thm * thm -> thm
    1.12 @@ -90,6 +92,118 @@
    1.13  local open Thm
    1.14  in
    1.15  
    1.16 +(**** Extend Theories ****)
    1.17 +
    1.18 +(** add constant definitions **)
    1.19 +
    1.20 +(* all_axioms_of *)
    1.21 +
    1.22 +(*results may contain duplicates!*)
    1.23 +
    1.24 +fun ancestry_of thy =
    1.25 +  thy :: flat (map ancestry_of (parents_of thy));
    1.26 +
    1.27 +val all_axioms_of = flat o map axioms_of o ancestry_of;
    1.28 +
    1.29 +
    1.30 +(* clash_types, clash_consts *)
    1.31 +
    1.32 +(*check if types have common instance (ignoring sorts)*)
    1.33 +
    1.34 +fun clash_types ty1 ty2 =
    1.35 +  let
    1.36 +    val ty1' = Type.varifyT ty1;
    1.37 +    val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2);
    1.38 +  in
    1.39 +    Type.raw_unify (ty1', ty2')
    1.40 +  end;
    1.41 +
    1.42 +fun clash_consts (c1, ty1) (c2, ty2) =
    1.43 +  c1 = c2 andalso clash_types ty1 ty2;
    1.44 +
    1.45 +
    1.46 +(* clash_defns *)
    1.47 +
    1.48 +fun clash_defn c_ty (name, tm) =
    1.49 +  let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in
    1.50 +    if clash_consts c_ty (c, ty') then Some (name, ty') else None
    1.51 +  end handle TERM _ => None;
    1.52 +
    1.53 +fun clash_defns c_ty axms =
    1.54 +  distinct (mapfilter (clash_defn c_ty) axms);
    1.55 +
    1.56 +
    1.57 +(* dest_defn *)
    1.58 +
    1.59 +fun dest_defn tm =
    1.60 +  let
    1.61 +    fun err msg = raise_term msg [tm];
    1.62 +
    1.63 +    val (lhs, rhs) = Logic.dest_equals tm
    1.64 +      handle TERM _ => err "Not a meta-equality (==)";
    1.65 +    val (head, args) = strip_comb lhs;
    1.66 +    val (c, ty) = dest_Const head
    1.67 +      handle TERM _ => err "Head of lhs not a constant";
    1.68 +
    1.69 +    fun occs_const (Const c_ty') = clash_consts (c, ty) c_ty'
    1.70 +      | occs_const (Abs (_, _, t)) = occs_const t
    1.71 +      | occs_const (t $ u) = occs_const t orelse occs_const u
    1.72 +      | occs_const _ = false;
    1.73 +  in
    1.74 +    if not (forall is_Free args) then
    1.75 +      err "Arguments of lhs have to be variables"
    1.76 +    else if not (null (duplicates args)) then
    1.77 +      err "Duplicate variables on lhs"
    1.78 +    else if not (term_frees rhs subset args) then
    1.79 +      err "Extra variables on rhs"
    1.80 +    else if not (term_tfrees rhs subset typ_tfrees ty) then
    1.81 +      err "Extra type variables on rhs"
    1.82 +    else if occs_const rhs then
    1.83 +      err "Constant to be defined clashes with occurrence(s) on rhs"
    1.84 +    else (c, ty)
    1.85 +  end;
    1.86 +
    1.87 +
    1.88 +(* check_defn *)
    1.89 +
    1.90 +fun err_in_axm name msg =
    1.91 +  (writeln msg; error ("The error(s) above occurred in axiom " ^ quote name));
    1.92 +
    1.93 +fun check_defn sign (axms, (name, tm)) =
    1.94 +  let
    1.95 +    fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block
    1.96 +      [Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty]));
    1.97 +
    1.98 +    fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn;
    1.99 +    fun show_defns c = commas o map (show_defn c);
   1.100 +
   1.101 +    val (c, ty) = dest_defn tm
   1.102 +      handle TERM (msg, _) => err_in_axm name msg;
   1.103 +    val defns = clash_defns (c, ty) axms;
   1.104 +  in
   1.105 +    if not (null defns) then
   1.106 +      err_in_axm name ("Definition of " ^ show_const (c, ty) ^
   1.107 +        " clashes with " ^ show_defns c defns)
   1.108 +    else (name, tm) :: axms
   1.109 +  end;
   1.110 +
   1.111 +
   1.112 +(* add_defs *)
   1.113 +
   1.114 +fun ext_defns prep_axm raw_axms thy =
   1.115 +  let
   1.116 +    val axms = map (prep_axm (sign_of thy)) raw_axms;
   1.117 +    val all_axms = all_axioms_of thy;
   1.118 +  in
   1.119 +    foldl (check_defn (sign_of thy)) (all_axms, axms);
   1.120 +    add_axioms_i axms thy
   1.121 +  end;
   1.122 +
   1.123 +val add_defs_i = ext_defns cert_axm;
   1.124 +val add_defs = ext_defns read_axm;
   1.125 +
   1.126 +
   1.127 +
   1.128  (**** More derived rules and operations on theorems ****)
   1.129  
   1.130  (** reading of instantiations **)