--- a/src/HOL/Library/positivstellensatz.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Mon Aug 08 21:55:01 2011 +0200
@@ -170,8 +170,8 @@
Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha)
(Thm.implies_intr (cprop_of tha) thb);
-fun prove_hyp tha thb =
- if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb))
+fun prove_hyp tha thb =
+ if exists (curry op aconv (concl_of tha)) (Thm.hyps_of thb) (* FIXME !? *)
then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb;
val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and
--- a/src/HOL/Orderings.thy Mon Aug 08 16:47:55 2011 +0200
+++ b/src/HOL/Orderings.thy Mon Aug 08 21:55:01 2011 +0200
@@ -531,7 +531,7 @@
setup {*
let
-fun prp t thm = (#prop (rep_thm thm) = t);
+fun prp t thm = Thm.prop_of thm = t; (* FIXME aconv!? *)
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
let val prems = Simplifier.prems_of ss;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Aug 08 21:55:01 2011 +0200
@@ -46,7 +46,7 @@
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val newTs = take (length (hd descr)) recTs;
- val {maxidx, ...} = rep_thm induct;
+ val maxidx = Thm.maxidx_of induct;
val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
fun prove_casedist_thm (i, (T, t)) =
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Aug 08 21:55:01 2011 +0200
@@ -20,9 +20,6 @@
in map (fn ks => i::ks) is @ is end
else [[]];
-fun prf_of thm =
- Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-
fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
fun tname_of (Type (s, _)) = s
@@ -141,7 +138,8 @@
end
| _ => AbsP ("H", SOME p, prf)))
(rec_fns ~~ prems_of thm)
- (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
+ (Proofterm.proof_combP
+ (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
val r' =
if null is then r
@@ -201,9 +199,10 @@
Proofterm.forall_intr_proof' (Logic.varify_global r)
(AbsP ("H", SOME (Logic.varify_global p), prf)))
(prems ~~ rs)
- (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
+ (Proofterm.proof_combP
+ (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
val prf' = Extraction.abs_corr_shyps thy' exhaust []
- (map Var (Term.add_vars (prop_of exhaust) [])) (prf_of exhaust);
+ (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
val r' = Logic.varify_global (Abs ("y", T,
list_abs (map dest_Free rs, list_comb (r,
map Bound ((length rs - 1 downto 0) @ [length rs])))));
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Aug 08 21:55:01 2011 +0200
@@ -270,7 +270,7 @@
fun lemma thm ct =
let
val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
- val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
+ val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm)
val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
in Thm (Z3_Proof_Tools.compose ccontr th) end
end
--- a/src/HOL/Tools/TFL/rules.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Mon Aug 08 21:55:01 2011 +0200
@@ -245,9 +245,7 @@
fun DISJ_CASESL disjth thl =
let val c = cconcl disjth
- fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
- aconv term_of atm)
- (#hyps(rep_thm th))
+ fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t aconv term_of atm) (Thm.hyps_of th)
val tml = Dcterm.strip_disj c
fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
| DL th [th1] = PROVE_HYP th th1
--- a/src/HOL/Tools/inductive_codegen.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Mon Aug 08 21:55:01 2011 +0200
@@ -581,7 +581,7 @@
(ks @ [SOME k]))) arities));
fun prep_intrs intrs =
- map (Codegen.rename_term o #prop o rep_thm o Drule.export_without_context) intrs;
+ map (Codegen.rename_term o Thm.prop_of o Drule.export_without_context) intrs;
fun constrain cs [] = []
| constrain cs ((s, xs) :: ys) =
--- a/src/HOL/Tools/inductive_realizer.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Mon Aug 08 21:55:01 2011 +0200
@@ -22,10 +22,8 @@
| _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
fun prf_of thm =
- let
- val thy = Thm.theory_of_thm thm;
- val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
- in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
+ Reconstruct.proof_of thm
+ |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)]; (* FIXME *)
fun subsets [] = [[]]
| subsets (x::xs) =
--- a/src/HOL/Tools/sat_funcs.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Mon Aug 08 21:55:01 2011 +0200
@@ -153,11 +153,13 @@
fun resolution (c1, hyps1) (c2, hyps2) =
let
val _ =
- if ! trace_sat then
+ if ! trace_sat then (* FIXME !? *)
tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
- " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
+ " (hyps: " ^ ML_Syntax.print_list
+ (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
- " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
+ " (hyps: " ^ ML_Syntax.print_list
+ (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
else ()
(* the two literals used for resolution *)
@@ -189,7 +191,7 @@
if !trace_sat then
tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
" (hyps: " ^ ML_Syntax.print_list
- (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
+ (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
else ()
val _ = Unsynchronized.inc counter
in
--- a/src/Provers/hypsubst.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/Provers/hypsubst.ML Mon Aug 08 21:55:01 2011 +0200
@@ -116,8 +116,7 @@
(*For the simpset. Adds ALL suitable equalities, even if not first!
No vars are allowed here, as simpsets are built from meta-assumptions*)
fun mk_eqs bnd th =
- [ if inspect_pair bnd false (Data.dest_eq
- (Data.dest_Trueprop (#prop (rep_thm th))))
+ [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th)))
then th RS Data.eq_reflection
else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
handle TERM _ => [] | Match => [];
--- a/src/Pure/IsaMakefile Mon Aug 08 16:47:55 2011 +0200
+++ b/src/Pure/IsaMakefile Mon Aug 08 21:55:01 2011 +0200
@@ -158,9 +158,9 @@
PIDE/document.ML \
PIDE/isar_document.ML \
Proof/extraction.ML \
+ Proof/proof_checker.ML \
Proof/proof_rewrite_rules.ML \
Proof/proof_syntax.ML \
- Proof/proofchecker.ML \
Proof/reconstruct.ML \
ProofGeneral/pgip.ML \
ProofGeneral/pgip_input.ML \
--- a/src/Pure/Isar/element.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/Pure/Isar/element.ML Mon Aug 08 21:55:01 2011 +0200
@@ -266,7 +266,7 @@
val mark_witness = Logic.protect;
fun witness_prop (Witness (t, _)) = t;
-fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
+fun witness_hyps (Witness (_, th)) = Thm.hyps_of th;
fun map_witness f (Witness witn) = Witness (f witn);
fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
--- a/src/Pure/Isar/rule_insts.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/Pure/Isar/rule_insts.ML Mon Aug 08 21:55:01 2011 +0200
@@ -312,7 +312,7 @@
(fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
(xis ~~ ts));
(* Lift and instantiate rule *)
- val {maxidx, ...} = rep_thm st;
+ val maxidx = Thm.maxidx_of st;
val paramTs = map #2 params
and inc = maxidx+1
fun liftvar (Var ((a,j), T)) =
--- a/src/Pure/Proof/extraction.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/Pure/Proof/extraction.ML Mon Aug 08 21:55:01 2011 +0200
@@ -795,7 +795,7 @@
|> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
Thm.varifyT_global (funpow (length (vars_of corr_prop))
(Thm.forall_elim_var 0) (Thm.forall_intr_frees
- (ProofChecker.thm_of_proof thy'
+ (Proof_Checker.thm_of_proof thy'
(fst (Proofterm.freeze_thaw_prf prf))))))
|> snd
|> fold Code.add_default_eqn def_thms
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Proof/proof_checker.ML Mon Aug 08 21:55:01 2011 +0200
@@ -0,0 +1,145 @@
+(* Title: Pure/Proof/proofchecker.ML
+ Author: Stefan Berghofer, TU Muenchen
+
+Simple proof checker based only on the core inference rules
+of Isabelle/Pure.
+*)
+
+signature PROOF_CHECKER =
+sig
+ val thm_of_proof : theory -> Proofterm.proof -> thm
+end;
+
+structure Proof_Checker : PROOF_CHECKER =
+struct
+
+(***** construct a theorem out of a proof term *****)
+
+fun lookup_thm thy =
+ let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in
+ fn s =>
+ (case Symtab.lookup tab s of
+ NONE => error ("Unknown theorem " ^ quote s)
+ | SOME thm => thm)
+ end;
+
+val beta_eta_convert =
+ Conv.fconv_rule Drule.beta_eta_conversion;
+
+(* equality modulo renaming of type variables *)
+fun is_equal t t' =
+ let
+ val atoms = fold_types (fold_atyps (insert (op =))) t [];
+ val atoms' = fold_types (fold_atyps (insert (op =))) t' []
+ in
+ length atoms = length atoms' andalso
+ map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
+ end;
+
+fun pretty_prf thy vs Hs prf =
+ let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
+ Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs)
+ in
+ (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
+ Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
+ end;
+
+fun pretty_term thy vs _ t =
+ let val t' = subst_bounds (map Free vs, t)
+ in
+ (Syntax.pretty_term_global thy t',
+ Syntax.pretty_typ_global thy (fastype_of t'))
+ end;
+
+fun appl_error thy prt vs Hs s f a =
+ let
+ val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
+ val (pp_a, pp_aT) = prt thy vs Hs a
+ in
+ error (cat_lines
+ [s,
+ "",
+ Pretty.string_of (Pretty.block
+ [Pretty.str "Operator:", Pretty.brk 2, pp_f,
+ Pretty.str " ::", Pretty.brk 1, pp_fT]),
+ Pretty.string_of (Pretty.block
+ [Pretty.str "Operand:", Pretty.brk 3, pp_a,
+ Pretty.str " ::", Pretty.brk 1, pp_aT]),
+ ""])
+ end;
+
+fun thm_of_proof thy =
+ let val lookup = lookup_thm thy in
+ fn prf =>
+ let
+ val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
+
+ fun thm_of_atom thm Ts =
+ let
+ val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
+ val (fmap, thm') = Thm.varifyT_global' [] thm;
+ val ctye = map (pairself (Thm.ctyp_of thy))
+ (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
+ in
+ Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
+ end;
+
+ fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
+ let
+ val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
+ val prop = Thm.prop_of thm;
+ val _ =
+ if is_equal prop prop' then ()
+ else
+ error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
+ Syntax.string_of_term_global thy prop ^ "\n\n" ^
+ Syntax.string_of_term_global thy prop');
+ in thm_of_atom thm Ts end
+
+ | thm_of _ _ (PAxm (name, _, SOME Ts)) =
+ thm_of_atom (Thm.axiom thy name) Ts
+
+ | thm_of _ Hs (PBound i) = nth Hs i
+
+ | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
+ let
+ val (x, names') = Name.variant s names;
+ val thm = thm_of ((x, T) :: vs, names') Hs prf
+ in
+ Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
+ end
+
+ | thm_of (vs, names) Hs (prf % SOME t) =
+ let
+ val thm = thm_of (vs, names) Hs prf;
+ val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
+ in
+ Thm.forall_elim ct thm
+ handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
+ end
+
+ | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
+ let
+ val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
+ val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
+ in
+ Thm.implies_intr ct thm
+ end
+
+ | thm_of vars Hs (prf %% prf') =
+ let
+ val thm = beta_eta_convert (thm_of vars Hs prf);
+ val thm' = beta_eta_convert (thm_of vars Hs prf');
+ in
+ Thm.implies_elim thm thm'
+ handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
+ end
+
+ | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
+
+ | thm_of _ _ _ = error "thm_of_proof: partial proof term";
+
+ in beta_eta_convert (thm_of ([], prf_names) [] prf) end
+ end;
+
+end;
--- a/src/Pure/Proof/proofchecker.ML Mon Aug 08 16:47:55 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(* Title: Pure/Proof/proofchecker.ML
- Author: Stefan Berghofer, TU Muenchen
-
-Simple proof checker based only on the core inference rules
-of Isabelle/Pure.
-*)
-
-signature PROOF_CHECKER =
-sig
- val thm_of_proof : theory -> Proofterm.proof -> thm
-end;
-
-structure ProofChecker : PROOF_CHECKER =
-struct
-
-(***** construct a theorem out of a proof term *****)
-
-fun lookup_thm thy =
- let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty
- in
- (fn s => case Symtab.lookup tab s of
- NONE => error ("Unknown theorem " ^ quote s)
- | SOME thm => thm)
- end;
-
-val beta_eta_convert =
- Conv.fconv_rule Drule.beta_eta_conversion;
-
-(* equality modulo renaming of type variables *)
-fun is_equal t t' =
- let
- val atoms = fold_types (fold_atyps (insert (op =))) t [];
- val atoms' = fold_types (fold_atyps (insert (op =))) t' []
- in
- length atoms = length atoms' andalso
- map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
- end;
-
-fun pretty_prf thy vs Hs prf =
- let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
- Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs)
- in
- (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
- Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
- end;
-
-fun pretty_term thy vs _ t =
- let val t' = subst_bounds (map Free vs, t)
- in
- (Syntax.pretty_term_global thy t',
- Syntax.pretty_typ_global thy (fastype_of t'))
- end;
-
-fun appl_error thy prt vs Hs s f a =
- let
- val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
- val (pp_a, pp_aT) = prt thy vs Hs a
- in
- error (cat_lines
- [s,
- "",
- Pretty.string_of (Pretty.block
- [Pretty.str "Operator:", Pretty.brk 2, pp_f,
- Pretty.str " ::", Pretty.brk 1, pp_fT]),
- Pretty.string_of (Pretty.block
- [Pretty.str "Operand:", Pretty.brk 3, pp_a,
- Pretty.str " ::", Pretty.brk 1, pp_aT]),
- ""])
- end;
-
-fun thm_of_proof thy prf =
- let
- val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
- val lookup = lookup_thm thy;
-
- fun thm_of_atom thm Ts =
- let
- val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
- val (fmap, thm') = Thm.varifyT_global' [] thm;
- val ctye = map (pairself (Thm.ctyp_of thy))
- (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
- in
- Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
- end;
-
- fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
- let
- val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
- val {prop, ...} = rep_thm thm;
- val _ = if is_equal prop prop' then () else
- error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
- Syntax.string_of_term_global thy prop ^ "\n\n" ^
- Syntax.string_of_term_global thy prop');
- in thm_of_atom thm Ts end
-
- | thm_of _ _ (PAxm (name, _, SOME Ts)) =
- thm_of_atom (Thm.axiom thy name) Ts
-
- | thm_of _ Hs (PBound i) = nth Hs i
-
- | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
- let
- val (x, names') = Name.variant s names;
- val thm = thm_of ((x, T) :: vs, names') Hs prf
- in
- Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
- end
-
- | thm_of (vs, names) Hs (prf % SOME t) =
- let
- val thm = thm_of (vs, names) Hs prf;
- val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
- in
- Thm.forall_elim ct thm
- handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
- end
-
- | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
- let
- val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
- val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
- in
- Thm.implies_intr ct thm
- end
-
- | thm_of vars Hs (prf %% prf') =
- let
- val thm = beta_eta_convert (thm_of vars Hs prf);
- val thm' = beta_eta_convert (thm_of vars Hs prf');
- in
- Thm.implies_elim thm thm'
- handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
- end
-
- | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
-
- | thm_of _ _ _ = error "thm_of_proof: partial proof term";
-
- in beta_eta_convert (thm_of ([], prf_names) [] prf) end;
-
-end;
--- a/src/Pure/Proof/reconstruct.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/Pure/Proof/reconstruct.ML Mon Aug 08 21:55:01 2011 +0200
@@ -10,6 +10,7 @@
val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
val prop_of' : term list -> Proofterm.proof -> term
val prop_of : Proofterm.proof -> term
+ val proof_of : thm -> Proofterm.proof
val expand_proof : theory -> (string * term option) list ->
Proofterm.proof -> Proofterm.proof
end;
@@ -323,6 +324,10 @@
val prop_of' = Envir.beta_eta_contract oo prop_of0;
val prop_of = prop_of' [];
+fun proof_of thm =
+ reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
+
+
(**** expand and reconstruct subproofs ****)
@@ -352,8 +357,9 @@
(case AList.lookup (op =) prfs (a, prop) of
NONE =>
let
- val _ = message ("Reconstructing proof of " ^ a);
- val _ = message (Syntax.string_of_term_global thy prop);
+ val _ =
+ message ("Reconstructing proof of " ^ a ^ "\n" ^
+ Syntax.string_of_term_global thy prop);
val prf' = forall_intr_vfs_prf prop
(reconstruct_proof thy prop (Proofterm.join_proof body));
val (maxidx', prfs', prf) = expand
--- a/src/Pure/ROOT.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/Pure/ROOT.ML Mon Aug 08 21:55:01 2011 +0200
@@ -175,7 +175,7 @@
use "Proof/reconstruct.ML";
use "Proof/proof_syntax.ML";
use "Proof/proof_rewrite_rules.ML";
-use "Proof/proofchecker.ML";
+use "Proof/proof_checker.ML";
(*outer syntax*)
use "Isar/token.ML";
--- a/src/Pure/raw_simplifier.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/Pure/raw_simplifier.ML Mon Aug 08 21:55:01 2011 +0200
@@ -1197,7 +1197,7 @@
val prem' = Thm.rhs_of eqn;
val tprems = map term_of prems;
val i = 1 + fold Integer.max (map (fn p =>
- find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
+ find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
val (rrs', asm') = rules_of_prem ss prem'
in mut_impc prems concl rrss asms (prem' :: prems')
(rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
--- a/src/Pure/simplifier.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/Pure/simplifier.ML Mon Aug 08 21:55:01 2011 +0200
@@ -410,7 +410,7 @@
if can Logic.dest_equals (Thm.concl_of thm) then [thm]
else [thm RS reflect] handle THM _ => [];
- fun mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
+ fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm);
in
empty_ss setsubgoaler asm_simp_tac
setSSolver safe_solver
--- a/src/Tools/jEdit/src/text_area_painter.scala Mon Aug 08 16:47:55 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala Mon Aug 08 21:55:01 2011 +0200
@@ -204,6 +204,10 @@
val chunk_font = chunk.style.getFont
val chunk_color = chunk.style.getForegroundColor
+ def string_width(s: String): Float =
+ if (s.isEmpty) 0.0f
+ else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
+
val caret_range =
if (text_area.hasFocus) doc_view.caret_range()
else Text.Range(-1)
@@ -230,17 +234,27 @@
range.try_restrict(caret_range) match {
case Some(r) if !r.is_singularity =>
- val astr = new AttributedString(str)
val i = r.start - range.start
val j = r.stop - range.start
+ val s1 = str.substring(0, i)
+ val s2 = str.substring(i, j)
+ val s3 = str.substring(j)
+
+ if (!s1.isEmpty) gfx.drawString(s1, x1, y)
+
+ val astr = new AttributedString(s2)
astr.addAttribute(TextAttribute.FONT, chunk_font)
- astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
- astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
- gfx.drawString(astr.getIterator, x1, y)
+ astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
+ astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
+ gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
+
+ if (!s3.isEmpty)
+ gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
+
case _ =>
gfx.drawString(str, x1, y)
}
- x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
+ x1 += string_width(str)
}
}
w += chunk.width
--- a/src/ZF/Tools/datatype_package.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/ZF/Tools/datatype_package.ML Mon Aug 08 21:55:01 2011 +0200
@@ -339,7 +339,7 @@
end
val constructors =
- map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
+ map (head_of o #1 o Logic.dest_equals o Thm.prop_of) (tl con_defs);
val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs);
--- a/src/ZF/Tools/induct_tacs.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Mon Aug 08 21:55:01 2011 +0200
@@ -123,8 +123,7 @@
Syntax.string_of_term_global thy eqn);
val constructors =
- map (head_of o const_of o FOLogic.dest_Trueprop o
- #prop o rep_thm) case_eqns;
+ map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
val Const (@{const_name mem}, _) $ _ $ data =
FOLogic.dest_Trueprop (hd (prems_of elim));
--- a/src/ZF/arith_data.ML Mon Aug 08 16:47:55 2011 +0200
+++ b/src/ZF/arith_data.ML Mon Aug 08 21:55:01 2011 +0200
@@ -61,7 +61,7 @@
(*We remove equality assumptions because they confuse the simplifier and
because only type-checking assumptions are necessary.*)
fun is_eq_thm th =
- can FOLogic.dest_eq (FOLogic.dest_Trueprop (#prop (rep_thm th)));
+ can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th));
fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
@@ -69,7 +69,7 @@
if t aconv u then NONE
else
let val prems' = filter_out is_eq_thm prems
- val goal = Logic.list_implies (map (#prop o Thm.rep_thm) prems',
+ val goal = Logic.list_implies (map Thm.prop_of prems',
FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
handle ERROR msg =>