1.1 --- a/src/Pure/Proof/proofchecker.ML Tue Jun 01 10:48:38 2010 +0200
1.2 +++ b/src/Pure/Proof/proofchecker.ML Tue Jun 01 10:53:55 2010 +0200
1.3 @@ -28,6 +28,48 @@
1.4 val beta_eta_convert =
1.5 Conv.fconv_rule Drule.beta_eta_conversion;
1.6
1.7 +(* equality modulo renaming of type variables *)
1.8 +fun is_equal t t' =
1.9 + let
1.10 + val atoms = fold_types (fold_atyps (insert (op =))) t [];
1.11 + val atoms' = fold_types (fold_atyps (insert (op =))) t' []
1.12 + in
1.13 + length atoms = length atoms' andalso
1.14 + map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
1.15 + end;
1.16 +
1.17 +fun pretty_prf thy vs Hs prf =
1.18 + let val prf' = prf |> prf_subst_bounds (map Free vs) |>
1.19 + prf_subst_pbounds (map (Hyp o prop_of) Hs)
1.20 + in
1.21 + (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
1.22 + Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
1.23 + end;
1.24 +
1.25 +fun pretty_term thy vs _ t =
1.26 + let val t' = subst_bounds (map Free vs, t)
1.27 + in
1.28 + (Syntax.pretty_term_global thy t',
1.29 + Syntax.pretty_typ_global thy (fastype_of t'))
1.30 + end;
1.31 +
1.32 +fun appl_error thy prt vs Hs s f a =
1.33 + let
1.34 + val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
1.35 + val (pp_a, pp_aT) = prt thy vs Hs a
1.36 + in
1.37 + error (cat_lines
1.38 + [s,
1.39 + "",
1.40 + Pretty.string_of (Pretty.block
1.41 + [Pretty.str "Operator:", Pretty.brk 2, pp_f,
1.42 + Pretty.str " ::", Pretty.brk 1, pp_fT]),
1.43 + Pretty.string_of (Pretty.block
1.44 + [Pretty.str "Operand:", Pretty.brk 3, pp_a,
1.45 + Pretty.str " ::", Pretty.brk 1, pp_aT]),
1.46 + ""])
1.47 + end;
1.48 +
1.49 fun thm_of_proof thy prf =
1.50 let
1.51 val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
1.52 @@ -45,9 +87,9 @@
1.53
1.54 fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
1.55 let
1.56 - val thm = Drule.implies_intr_hyps (lookup name);
1.57 + val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
1.58 val {prop, ...} = rep_thm thm;
1.59 - val _ = if prop aconv prop' then () else
1.60 + val _ = if is_equal prop prop' then () else
1.61 error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
1.62 Syntax.string_of_term_global thy prop ^ "\n\n" ^
1.63 Syntax.string_of_term_global thy prop');
1.64 @@ -70,7 +112,10 @@
1.65 let
1.66 val thm = thm_of (vs, names) Hs prf;
1.67 val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
1.68 - in Thm.forall_elim ct thm end
1.69 + in
1.70 + Thm.forall_elim ct thm
1.71 + handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
1.72 + end
1.73
1.74 | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
1.75 let
1.76 @@ -86,6 +131,7 @@
1.77 val thm' = beta_eta_convert (thm_of vars Hs prf');
1.78 in
1.79 Thm.implies_elim thm thm'
1.80 + handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
1.81 end
1.82
1.83 | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)