# HG changeset patch # User wenzelm # Date 1312833301 -7200 # Node ID 9ee98b584494d08438084571ca5f166d65c2e3ba # Parent cebb7abb54b18bcac5705320cbd11e5d70b80a74# Parent 55a4df7f2568936d2290b0817be1ae6950997292 merged diff -r cebb7abb54b1 -r 9ee98b584494 src/HOL/Library/positivstellensatz.ML --- 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 diff -r cebb7abb54b1 -r 9ee98b584494 src/HOL/Orderings.thy --- 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; diff -r cebb7abb54b1 -r 9ee98b584494 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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)) = diff -r cebb7abb54b1 -r 9ee98b584494 src/HOL/Tools/Datatype/datatype_realizer.ML --- 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]))))); diff -r cebb7abb54b1 -r 9ee98b584494 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- 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 diff -r cebb7abb54b1 -r 9ee98b584494 src/HOL/Tools/TFL/rules.ML --- 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 diff -r cebb7abb54b1 -r 9ee98b584494 src/HOL/Tools/inductive_codegen.ML --- 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) = diff -r cebb7abb54b1 -r 9ee98b584494 src/HOL/Tools/inductive_realizer.ML --- 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) = diff -r cebb7abb54b1 -r 9ee98b584494 src/HOL/Tools/sat_funcs.ML --- 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 diff -r cebb7abb54b1 -r 9ee98b584494 src/Provers/hypsubst.ML --- 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 => []; diff -r cebb7abb54b1 -r 9ee98b584494 src/Pure/IsaMakefile --- 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 \ diff -r cebb7abb54b1 -r 9ee98b584494 src/Pure/Isar/element.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)); diff -r cebb7abb54b1 -r 9ee98b584494 src/Pure/Isar/rule_insts.ML --- 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)) = diff -r cebb7abb54b1 -r 9ee98b584494 src/Pure/Proof/extraction.ML --- 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 diff -r cebb7abb54b1 -r 9ee98b584494 src/Pure/Proof/proof_checker.ML --- /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; diff -r cebb7abb54b1 -r 9ee98b584494 src/Pure/Proof/proofchecker.ML --- 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; diff -r cebb7abb54b1 -r 9ee98b584494 src/Pure/Proof/reconstruct.ML --- 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 diff -r cebb7abb54b1 -r 9ee98b584494 src/Pure/ROOT.ML --- 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"; diff -r cebb7abb54b1 -r 9ee98b584494 src/Pure/raw_simplifier.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) diff -r cebb7abb54b1 -r 9ee98b584494 src/Pure/simplifier.ML --- 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 diff -r cebb7abb54b1 -r 9ee98b584494 src/Tools/jEdit/src/text_area_painter.scala --- 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 diff -r cebb7abb54b1 -r 9ee98b584494 src/ZF/Tools/datatype_package.ML --- 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); diff -r cebb7abb54b1 -r 9ee98b584494 src/ZF/Tools/induct_tacs.ML --- 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)); diff -r cebb7abb54b1 -r 9ee98b584494 src/ZF/arith_data.ML --- 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 =>