Exported function unify_consts (workaround to avoid inconsistently
authorberghofe
Fri Jul 16 14:06:13 1999 +0200 (1999-07-16)
changeset 702075ff179df7b7
parent 7019 71f2155cdd85
child 7021 0073aa571502
Exported function unify_consts (workaround to avoid inconsistently
typed recursive constants in inductive and primrec definitions).
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jul 16 14:03:33 1999 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jul 16 14:06:13 1999 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4  signature INDUCTIVE_PACKAGE =
     1.5  sig
     1.6    val quiet_mode: bool ref
     1.7 +  val unify_consts: Sign.sg -> term list -> term list -> term list * term list
     1.8    val get_inductive: theory -> string ->
     1.9      {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    1.10        induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.11 @@ -62,6 +63,37 @@
    1.12    | coind_prefix false = "";
    1.13  
    1.14  
    1.15 +(* the following code ensures that each recursive set *)
    1.16 +(* always has the same type in all introduction rules *)
    1.17 +
    1.18 +fun unify_consts sign cs intr_ts =
    1.19 +  (let
    1.20 +    val {tsig, ...} = Sign.rep_sg sign;
    1.21 +    val add_term_consts_2 =
    1.22 +      foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
    1.23 +    fun varify (t, (i, ts)) =
    1.24 +      let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
    1.25 +      in (maxidx_of_term t', t'::ts) end;
    1.26 +    val (i, cs') = foldr varify (cs, (~1, []));
    1.27 +    val (i', intr_ts') = foldr varify (intr_ts, (i, []));
    1.28 +    val rec_consts = foldl add_term_consts_2 ([], cs');
    1.29 +    val intr_consts = foldl add_term_consts_2 ([], intr_ts');
    1.30 +    fun unify (env, (cname, cT)) =
    1.31 +      let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
    1.32 +      in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
    1.33 +          (env, (replicate (length consts) cT) ~~ consts)
    1.34 +      end;
    1.35 +    val (env, _) = foldl unify (([], i'), rec_consts);
    1.36 +    fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
    1.37 +      in if T = T' then T else typ_subst_TVars_2 env T' end;
    1.38 +    val subst = fst o Type.freeze_thaw o
    1.39 +      (map_term_types (typ_subst_TVars_2 env))
    1.40 +
    1.41 +  in (map subst cs', map subst intr_ts')
    1.42 +  end) handle Type.TUNIFY =>
    1.43 +    (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
    1.44 +
    1.45 +
    1.46  (* misc *)
    1.47  
    1.48  (*For proving monotonicity of recursion operator*)
    1.49 @@ -143,7 +175,9 @@
    1.50        | _ => err_in_rule sign r msg1)
    1.51    end;
    1.52  
    1.53 -fun try' f msg sign t = (f t) handle _ => error (msg ^ Sign.string_of_term sign t);
    1.54 +fun try' f msg sign t = (case (try f t) of
    1.55 +      Some x => x
    1.56 +    | None => error (msg ^ Sign.string_of_term sign t));
    1.57  
    1.58  
    1.59  
    1.60 @@ -656,41 +690,14 @@
    1.61      val intr_names = map (fst o fst) intro_srcs;
    1.62      val intr_ts = map (readtm (Theory.sign_of thy) propT o snd o fst) intro_srcs;
    1.63      val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
    1.64 -
    1.65 -    (* the following code ensures that each recursive set *)
    1.66 -    (* always has the same type in all introduction rules *)
    1.67 -
    1.68 -    val {tsig, ...} = Sign.rep_sg sign;
    1.69 -    val add_term_consts_2 =
    1.70 -      foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
    1.71 -    fun varify (t, (i, ts)) =
    1.72 -      let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
    1.73 -      in (maxidx_of_term t', t'::ts) end;
    1.74 -    val (i, cs') = foldr varify (cs, (~1, []));
    1.75 -    val (i', intr_ts') = foldr varify (intr_ts, (i, []));
    1.76 -    val rec_consts = foldl add_term_consts_2 ([], cs');
    1.77 -    val intr_consts = foldl add_term_consts_2 ([], intr_ts');
    1.78 -    fun unify (env, (cname, cT)) =
    1.79 -      let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
    1.80 -      in (foldl (fn ((env', j'), Tp) => Type.unify tsig j' env' Tp)
    1.81 -        (env, (replicate (length consts) cT) ~~ consts)) handle _ =>
    1.82 -          error ("Occurrences of constant '" ^ cname ^
    1.83 -            "' have incompatible types")
    1.84 -      end;
    1.85 -    val (env, _) = foldl unify (([], i'), rec_consts);
    1.86 -    fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
    1.87 -      in if T = T' then T else typ_subst_TVars_2 env T' end;
    1.88 -    val subst = fst o Type.freeze_thaw o
    1.89 -      (map_term_types (typ_subst_TVars_2 env));
    1.90 -    val cs'' = map subst cs';
    1.91 -    val intr_ts'' = map subst intr_ts';
    1.92 +    val (cs', intr_ts') = unify_consts sign cs intr_ts;
    1.93  
    1.94      val ((thy', con_defs), monos) = thy
    1.95        |> IsarThy.apply_theorems raw_monos
    1.96        |> apfst (IsarThy.apply_theorems raw_con_defs);
    1.97    in
    1.98 -    add_inductive_i verbose false "" coind false false cs''
    1.99 -      atts ((intr_names ~~ intr_ts'') ~~ intr_atts) monos con_defs thy'
   1.100 +    add_inductive_i verbose false "" coind false false cs'
   1.101 +      atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   1.102    end;
   1.103  
   1.104