# HG changeset patch # User wenzelm # Date 1258405036 -3600 # Node ID e588744f14dabc1bb5944513cc344df7949e7840 # Parent f15c9ded96761491a9b4b2e34aa7ea1735a5de61 generalized procs for rewrite_proof: allow skeleton; fulfill_norm_proof: always normalize result here, no re-normalization after filling; diff -r f15c9ded9676 -r e588744f14da src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Mon Nov 16 21:56:32 2009 +0100 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Mon Nov 16 21:57:16 2009 +0100 @@ -7,7 +7,7 @@ signature REWRITE_HOL_PROOF = sig val rews: (Proofterm.proof * Proofterm.proof) list - val elim_cong: typ list -> Proofterm.proof -> Proofterm.proof option + val elim_cong: typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option end; structure RewriteHOLProof : REWRITE_HOL_PROOF = @@ -309,17 +309,19 @@ fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t); -fun elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) = +fun elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) = Option.map (make_subst Ts prf2 []) (strip_cong [] prf1) - | elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) = + | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) = Option.map (mk_AbsP P o make_subst Ts (PBound 0) []) (strip_cong [] (incr_pboundvars 1 0 prf)) - | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) = + | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) = Option.map (make_subst Ts prf2 [] o apsnd (map (make_sym Ts))) (strip_cong [] prf1) - | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) = + | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) = Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf)) - | elim_cong _ _ = NONE; + | elim_cong_aux _ _ = NONE; + +fun elim_cong Ts prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf); end; diff -r f15c9ded9676 -r e588744f14da src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Mon Nov 16 21:56:32 2009 +0100 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Mon Nov 16 21:57:16 2009 +0100 @@ -6,8 +6,9 @@ signature PROOF_REWRITE_RULES = sig - val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option - val rprocs : bool -> (typ list -> Proofterm.proof -> Proofterm.proof option) list + val rew : bool -> typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option + val rprocs : bool -> + (typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof @@ -183,7 +184,7 @@ end | rew' _ = NONE; - in rew' end; + in rew' #> Option.map (rpair no_skel) end; fun rprocs b = [rew b]; val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false))); diff -r f15c9ded9676 -r e588744f14da src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Nov 16 21:56:32 2009 +0100 +++ b/src/Pure/proofterm.ML Mon Nov 16 21:57:16 2009 +0100 @@ -109,18 +109,20 @@ val axm_proof: string -> term -> proof val oracle_proof: string -> term -> oracle * proof val promise_proof: theory -> serial -> term -> proof - val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body + val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body val thm_proof: theory -> string -> term list -> term -> (serial * proof_body future) list -> proof_body -> pthm * proof val get_name: term list -> term -> proof -> string (** rewriting on proof terms **) val add_prf_rrule: proof * proof -> theory -> theory - val add_prf_rproc: (typ list -> proof -> proof option) -> theory -> theory + val add_prf_rproc: (typ list -> proof -> (proof * proof) option) -> theory -> theory + val no_skel: proof + val normal_skel: proof val rewrite_proof: theory -> (proof * proof) list * - (typ list -> proof -> proof option) list -> proof -> proof + (typ list -> proof -> (proof * proof) option) list -> proof -> proof val rewrite_proof_notypes: (proof * proof) list * - (typ list -> proof -> proof option) list -> proof -> proof + (typ list -> proof -> (proof * proof) option) list -> proof -> proof val rew_proof: theory -> proof -> proof end @@ -1169,28 +1171,30 @@ (**** rewriting on proof terms ****) -val skel0 = PBound 0; +val no_skel = PBound 0; +val normal_skel = Hyp (Var ((Name.uu, 0), propT)); fun rewrite_prf tymatch (rules, procs) prf = let - fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, skel0) - | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, skel0) - | rew Ts prf = (case get_first (fn r => r Ts prf) procs of - SOME prf' => SOME (prf', skel0) - | NONE => get_first (fn (prf1, prf2) => SOME (prf_subst - (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2) - handle PMatch => NONE) (filter (could_unify prf o fst) rules)); + fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel) + | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel) + | rew Ts prf = + (case get_first (fn r => r Ts prf) procs of + NONE => get_first (fn (prf1, prf2) => SOME (prf_subst + (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2) + handle PMatch => NONE) (filter (could_unify prf o fst) rules) + | some => some); fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) = if prf_loose_Pbvar1 prf' 0 then rew Ts prf else let val prf'' = incr_pboundvars (~1) 0 prf' - in SOME (the_default (prf'', skel0) (rew Ts prf'')) end + in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end | rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) = if prf_loose_bvar1 prf' 0 then rew Ts prf else let val prf'' = incr_pboundvars 0 (~1) prf' - in SOME (the_default (prf'', skel0) (rew Ts prf'')) end + in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end | rew0 Ts prf = rew Ts prf; fun rew1 _ (Hyp (Var _)) _ = NONE @@ -1205,20 +1209,20 @@ and rew2 Ts skel (prf % SOME t) = (case prf of Abst (_, _, body) => let val prf' = prf_subst_bounds [t] body - in SOME (the_default prf' (rew2 Ts skel0 prf')) end - | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf of + in SOME (the_default prf' (rew2 Ts no_skel prf')) end + | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf of SOME prf' => SOME (prf' % SOME t) | NONE => NONE)) | rew2 Ts skel (prf % NONE) = Option.map (fn prf' => prf' % NONE) - (rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf) + (rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf) | rew2 Ts skel (prf1 %% prf2) = (case prf1 of AbsP (_, _, body) => let val prf' = prf_subst_pbounds [prf2] body - in SOME (the_default prf' (rew2 Ts skel0 prf')) end + in SOME (the_default prf' (rew2 Ts no_skel prf')) end | _ => let val (skel1, skel2) = (case skel of skel1 %% skel2 => (skel1, skel2) - | _ => (skel0, skel0)) + | _ => (no_skel, no_skel)) in case rew1 Ts skel1 prf1 of SOME prf1' => (case rew1 Ts skel2 prf2 of SOME prf2' => SOME (prf1' %% prf2') @@ -1228,16 +1232,16 @@ | NONE => NONE) end) | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) - (case skel of Abst (_, _, skel') => skel' | _ => skel0) prf of + (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of SOME prf' => SOME (Abst (s, T, prf')) | NONE => NONE) | rew2 Ts skel (AbsP (s, t, prf)) = (case rew1 Ts - (case skel of AbsP (_, _, skel') => skel' | _ => skel0) prf of + (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of SOME prf' => SOME (AbsP (s, t, prf')) | NONE => NONE) | rew2 _ _ _ = NONE; - in the_default prf (rew1 [] skel0 prf) end; + in the_default prf (rew1 [] no_skel prf) end; fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) => Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch); @@ -1249,7 +1253,9 @@ structure ProofData = Theory_Data ( - type T = (stamp * (proof * proof)) list * (stamp * (typ list -> proof -> proof option)) list; + type T = + (stamp * (proof * proof)) list * + (stamp * (typ list -> proof -> (proof * proof) option)) list; val empty = ([], []); val extend = I; @@ -1277,27 +1283,26 @@ | _ => false)); in Promise (i, prop, map TVar (Term.add_tvars prop [])) end; -fun fulfill_proof _ [] body0 = body0 - | fulfill_proof thy ps body0 = - let - val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0; - val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0; - val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0; - val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty; +fun fulfill_norm_proof thy ps body0 = + let + val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0; + val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0; + val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0; + val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty; - fun fill (Promise (i, prop, Ts)) = - (case Inttab.lookup proofs i of - NONE => NONE - | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf)) - | fill _ = NONE; - val (rules, procs) = get_data thy; - val proof = rewrite_prf fst (rules, K fill :: procs) proof0; - in PBody {oracles = oracles, thms = thms, proof = proof} end; + fun fill (Promise (i, prop, Ts)) = + (case Inttab.lookup proofs i of + NONE => NONE + | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf, normal_skel)) + | fill _ = NONE; + val (rules, procs) = get_data thy; + val proof = rewrite_prf fst (rules, K fill :: procs) proof0; + in PBody {oracles = oracles, thms = thms, proof = proof} end; fun fulfill_proof_future _ [] body = Future.value body | fulfill_proof_future thy promises body = Future.fork_deps (map snd promises) (fn () => - fulfill_proof thy (map (apsnd Future.join) promises) body); + fulfill_norm_proof thy (map (apsnd Future.join) promises) body); (***** theorems *****) diff -r f15c9ded9676 -r e588744f14da src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Nov 16 21:56:32 2009 +0100 +++ b/src/Pure/thm.ML Mon Nov 16 21:57:16 2009 +0100 @@ -540,7 +540,7 @@ fun raw_body (Thm (Deriv {body, ...}, _)) = body; fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) = - Pt.fulfill_proof (Theory.deref thy_ref) + Pt.fulfill_norm_proof (Theory.deref thy_ref) (map #1 promises ~~ fulfill_bodies (map #2 promises)) body and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));