# HG changeset patch # User berghofe # Date 1275387400 -7200 # Node ID d94459cf7ea860258d9a961f3c6aa21036a227b7 # Parent 7c59ab0a419b20c5597e1daf930a3a1c94c91d24# Parent 957753a476700ff528f6f6b82c6a70d4850ff15a merged diff -r 7c59ab0a419b -r d94459cf7ea8 src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Tue Jun 01 11:37:41 2010 +0200 +++ b/src/HOL/Extraction.thy Tue Jun 01 12:16:40 2010 +0200 @@ -18,7 +18,8 @@ Proofterm.rewrite_proof_notypes ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o Proofterm.rewrite_proof thy - (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o + (RewriteHOLProof.rews, + ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o ProofRewriteRules.elim_vars (curry Const @{const_name default})) *} @@ -199,223 +200,212 @@ theorem exE_realizer': "P (snd p) (fst p) \ (\x y. P y x \ Q) \ Q" by (cases p) simp -setup {* - Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::type"}) -*} - realizers impI (P, Q): "\pq. pq" - "\ P Q pq (h: _). allI \ _ \ (\ x. impI \ _ \ _ \ (h \ x))" + "\ (c: _) (d: _) P Q pq (h: _). allI \ _ \ c \ (\ x. impI \ _ \ _ \ (h \ x))" impI (P): "Null" - "\ P Q (h: _). allI \ _ \ (\ x. impI \ _ \ _ \ (h \ x))" + "\ (c: _) P Q (h: _). allI \ _ \ c \ (\ x. impI \ _ \ _ \ (h \ x))" - impI (Q): "\q. q" "\ P Q q. impI \ _ \ _" + impI (Q): "\q. q" "\ (c: _) P Q q. impI \ _ \ _" impI: "Null" "impI" mp (P, Q): "\pq. pq" - "\ P Q pq (h: _) p. mp \ _ \ _ \ (spec \ _ \ p \ h)" + "\ (c: _) (d: _) P Q pq (h: _) p. mp \ _ \ _ \ (spec \ _ \ p \ c \ h)" mp (P): "Null" - "\ P Q (h: _) p. mp \ _ \ _ \ (spec \ _ \ p \ h)" + "\ (c: _) P Q (h: _) p. mp \ _ \ _ \ (spec \ _ \ p \ c \ h)" - mp (Q): "\q. q" "\ P Q q. mp \ _ \ _" + mp (Q): "\q. q" "\ (c: _) P Q q. mp \ _ \ _" mp: "Null" "mp" - allI (P): "\p. p" "\ P p. allI \ _" + allI (P): "\p. p" "\ (c: _) P (d: _) p. allI \ _ \ d" allI: "Null" "allI" - spec (P): "\x p. p x" "\ P x p. spec \ _ \ x" + spec (P): "\x p. p x" "\ (c: _) P x (d: _) p. spec \ _ \ x \ d" spec: "Null" "spec" - exI (P): "\x p. (x, p)" "\ P x p. exI_realizer \ P \ p \ x" + exI (P): "\x p. (x, p)" "\ (c: _) P x (d: _) p. exI_realizer \ P \ p \ x \ c \ d" - exI: "\x. x" "\ P x (h: _). h" + exI: "\x. x" "\ P x (c: _) (h: _). h" exE (P, Q): "\p pq. let (x, y) = p in pq x y" - "\ P Q p (h: _) pq. exE_realizer \ P \ p \ Q \ pq \ h" + "\ (c: _) (d: _) P Q (e: _) p (h: _) pq. exE_realizer \ P \ p \ Q \ pq \ c \ e \ d \ h" exE (P): "Null" - "\ P Q p. exE_realizer' \ _ \ _ \ _" + "\ (c: _) P Q (d: _) p. exE_realizer' \ _ \ _ \ _ \ c \ d" exE (Q): "\x pq. pq x" - "\ P Q x (h1: _) pq (h2: _). h2 \ x \ h1" + "\ (c: _) P Q (d: _) x (h1: _) pq (h2: _). h2 \ x \ h1" exE: "Null" - "\ P Q x (h1: _) (h2: _). h2 \ x \ h1" + "\ P Q (c: _) x (h1: _) (h2: _). h2 \ x \ h1" conjI (P, Q): "Pair" - "\ P Q p (h: _) q. conjI_realizer \ P \ p \ Q \ q \ h" + "\ (c: _) (d: _) P Q p (h: _) q. conjI_realizer \ P \ p \ Q \ q \ c \ d \ h" conjI (P): "\p. p" - "\ P Q p. conjI \ _ \ _" + "\ (c: _) P Q p. conjI \ _ \ _" conjI (Q): "\q. q" - "\ P Q (h: _) q. conjI \ _ \ _ \ h" + "\ (c: _) P Q (h: _) q. conjI \ _ \ _ \ h" conjI: "Null" "conjI" conjunct1 (P, Q): "fst" - "\ P Q pq. conjunct1 \ _ \ _" + "\ (c: _) (d: _) P Q pq. conjunct1 \ _ \ _" conjunct1 (P): "\p. p" - "\ P Q p. conjunct1 \ _ \ _" + "\ (c: _) P Q p. conjunct1 \ _ \ _" conjunct1 (Q): "Null" - "\ P Q q. conjunct1 \ _ \ _" + "\ (c: _) P Q q. conjunct1 \ _ \ _" conjunct1: "Null" "conjunct1" conjunct2 (P, Q): "snd" - "\ P Q pq. conjunct2 \ _ \ _" + "\ (c: _) (d: _) P Q pq. conjunct2 \ _ \ _" conjunct2 (P): "Null" - "\ P Q p. conjunct2 \ _ \ _" + "\ (c: _) P Q p. conjunct2 \ _ \ _" conjunct2 (Q): "\p. p" - "\ P Q p. conjunct2 \ _ \ _" + "\ (c: _) P Q p. conjunct2 \ _ \ _" conjunct2: "Null" "conjunct2" disjI1 (P, Q): "Inl" - "\ P Q p. iffD2 \ _ \ _ \ (sum.cases_1 \ P \ _ \ p)" + "\ (c: _) (d: _) P Q p. iffD2 \ _ \ _ \ (sum.cases_1 \ P \ _ \ p \ arity_type_bool \ c \ d)" disjI1 (P): "Some" - "\ P Q p. iffD2 \ _ \ _ \ (option.cases_2 \ _ \ P \ p)" + "\ (c: _) P Q p. iffD2 \ _ \ _ \ (option.cases_2 \ _ \ P \ p \ arity_type_bool \ c)" disjI1 (Q): "None" - "\ P Q. iffD2 \ _ \ _ \ (option.cases_1 \ _ \ _)" + "\ (c: _) P Q. iffD2 \ _ \ _ \ (option.cases_1 \ _ \ _ \ arity_type_bool \ c)" disjI1: "Left" - "\ P Q. iffD2 \ _ \ _ \ (sumbool.cases_1 \ _ \ _)" + "\ P Q. iffD2 \ _ \ _ \ (sumbool.cases_1 \ _ \ _ \ arity_type_bool)" disjI2 (P, Q): "Inr" - "\ Q P q. iffD2 \ _ \ _ \ (sum.cases_2 \ _ \ Q \ q)" + "\ (d: _) (c: _) Q P q. iffD2 \ _ \ _ \ (sum.cases_2 \ _ \ Q \ q \ arity_type_bool \ c \ d)" disjI2 (P): "None" - "\ Q P. iffD2 \ _ \ _ \ (option.cases_1 \ _ \ _)" + "\ (c: _) Q P. iffD2 \ _ \ _ \ (option.cases_1 \ _ \ _ \ arity_type_bool \ c)" disjI2 (Q): "Some" - "\ Q P q. iffD2 \ _ \ _ \ (option.cases_2 \ _ \ Q \ q)" + "\ (c: _) Q P q. iffD2 \ _ \ _ \ (option.cases_2 \ _ \ Q \ q \ arity_type_bool \ c)" disjI2: "Right" - "\ Q P. iffD2 \ _ \ _ \ (sumbool.cases_2 \ _ \ _)" + "\ Q P. iffD2 \ _ \ _ \ (sumbool.cases_2 \ _ \ _ \ arity_type_bool)" disjE (P, Q, R): "\pq pr qr. (case pq of Inl p \ pr p | Inr q \ qr q)" - "\ P Q R pq (h1: _) pr (h2: _) qr. - disjE_realizer \ _ \ _ \ pq \ R \ pr \ qr \ h1 \ h2" + "\ (c: _) (d: _) (e: _) P Q R pq (h1: _) pr (h2: _) qr. + disjE_realizer \ _ \ _ \ pq \ R \ pr \ qr \ c \ d \ e \ h1 \ h2" disjE (Q, R): "\pq pr qr. (case pq of None \ pr | Some q \ qr q)" - "\ P Q R pq (h1: _) pr (h2: _) qr. - disjE_realizer2 \ _ \ _ \ pq \ R \ pr \ qr \ h1 \ h2" + "\ (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr. + disjE_realizer2 \ _ \ _ \ pq \ R \ pr \ qr \ c \ d \ h1 \ h2" disjE (P, R): "\pq pr qr. (case pq of None \ qr | Some p \ pr p)" - "\ P Q R pq (h1: _) pr (h2: _) qr (h3: _). - disjE_realizer2 \ _ \ _ \ pq \ R \ qr \ pr \ h1 \ h3 \ h2" + "\ (c: _) (d: _) P Q R pq (h1: _) pr (h2: _) qr (h3: _). + disjE_realizer2 \ _ \ _ \ pq \ R \ qr \ pr \ c \ d \ h1 \ h3 \ h2" disjE (R): "\pq pr qr. (case pq of Left \ pr | Right \ qr)" - "\ P Q R pq (h1: _) pr (h2: _) qr. - disjE_realizer3 \ _ \ _ \ pq \ R \ pr \ qr \ h1 \ h2" + "\ (c: _) P Q R pq (h1: _) pr (h2: _) qr. + disjE_realizer3 \ _ \ _ \ pq \ R \ pr \ qr \ c \ h1 \ h2" disjE (P, Q): "Null" - "\ P Q R pq. disjE_realizer \ _ \ _ \ pq \ (\x. R) \ _ \ _" + "\ (c: _) (d: _) P Q R pq. disjE_realizer \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ c \ d \ arity_type_bool" disjE (Q): "Null" - "\ P Q R pq. disjE_realizer2 \ _ \ _ \ pq \ (\x. R) \ _ \ _" + "\ (c: _) P Q R pq. disjE_realizer2 \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ c \ arity_type_bool" disjE (P): "Null" - "\ P Q R pq (h1: _) (h2: _) (h3: _). - disjE_realizer2 \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ h1 \ h3 \ h2" + "\ (c: _) P Q R pq (h1: _) (h2: _) (h3: _). + disjE_realizer2 \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ c \ arity_type_bool \ h1 \ h3 \ h2" disjE: "Null" - "\ P Q R pq. disjE_realizer3 \ _ \ _ \ pq \ (\x. R) \ _ \ _" + "\ P Q R pq. disjE_realizer3 \ _ \ _ \ pq \ (\x. R) \ _ \ _ \ arity_type_bool" FalseE (P): "default" - "\ P. FalseE \ _" + "\ (c: _) P. FalseE \ _" FalseE: "Null" "FalseE" notI (P): "Null" - "\ P (h: _). allI \ _ \ (\ x. notI \ _ \ (h \ x))" + "\ (c: _) P (h: _). allI \ _ \ c \ (\ x. notI \ _ \ (h \ x))" notI: "Null" "notI" notE (P, R): "\p. default" - "\ P R (h: _) p. notE \ _ \ _ \ (spec \ _ \ p \ h)" + "\ (c: _) (d: _) P R (h: _) p. notE \ _ \ _ \ (spec \ _ \ p \ c \ h)" notE (P): "Null" - "\ P R (h: _) p. notE \ _ \ _ \ (spec \ _ \ p \ h)" + "\ (c: _) P R (h: _) p. notE \ _ \ _ \ (spec \ _ \ p \ c \ h)" notE (R): "default" - "\ P R. notE \ _ \ _" + "\ (c: _) P R. notE \ _ \ _" notE: "Null" "notE" subst (P): "\s t ps. ps" - "\ s t P (h: _) ps. subst \ s \ t \ P ps \ h" + "\ (c: _) s t P (d: _) (h: _) ps. subst \ s \ t \ P ps \ d \ h" subst: "Null" "subst" iffD1 (P, Q): "fst" - "\ Q P pq (h: _) p. - mp \ _ \ _ \ (spec \ _ \ p \ (conjunct1 \ _ \ _ \ h))" + "\ (d: _) (c: _) Q P pq (h: _) p. + mp \ _ \ _ \ (spec \ _ \ p \ d \ (conjunct1 \ _ \ _ \ h))" iffD1 (P): "\p. p" - "\ Q P p (h: _). mp \ _ \ _ \ (conjunct1 \ _ \ _ \ h)" + "\ (c: _) Q P p (h: _). mp \ _ \ _ \ (conjunct1 \ _ \ _ \ h)" iffD1 (Q): "Null" - "\ Q P q1 (h: _) q2. - mp \ _ \ _ \ (spec \ _ \ q2 \ (conjunct1 \ _ \ _ \ h))" + "\ (c: _) Q P q1 (h: _) q2. + mp \ _ \ _ \ (spec \ _ \ q2 \ c \ (conjunct1 \ _ \ _ \ h))" iffD1: "Null" "iffD1" iffD2 (P, Q): "snd" - "\ P Q pq (h: _) q. - mp \ _ \ _ \ (spec \ _ \ q \ (conjunct2 \ _ \ _ \ h))" + "\ (c: _) (d: _) P Q pq (h: _) q. + mp \ _ \ _ \ (spec \ _ \ q \ d \ (conjunct2 \ _ \ _ \ h))" iffD2 (P): "\p. p" - "\ P Q p (h: _). mp \ _ \ _ \ (conjunct2 \ _ \ _ \ h)" + "\ (c: _) P Q p (h: _). mp \ _ \ _ \ (conjunct2 \ _ \ _ \ h)" iffD2 (Q): "Null" - "\ P Q q1 (h: _) q2. - mp \ _ \ _ \ (spec \ _ \ q2 \ (conjunct2 \ _ \ _ \ h))" + "\ (c: _) P Q q1 (h: _) q2. + mp \ _ \ _ \ (spec \ _ \ q2 \ c \ (conjunct2 \ _ \ _ \ h))" iffD2: "Null" "iffD2" iffI (P, Q): "Pair" - "\ P Q pq (h1 : _) qp (h2 : _). conjI_realizer \ + "\ (c: _) (d: _) P Q pq (h1 : _) qp (h2 : _). conjI_realizer \ (\pq. \x. P x \ Q (pq x)) \ pq \ (\qp. \x. Q x \ P (qp x)) \ qp \ - (allI \ _ \ (\ x. impI \ _ \ _ \ (h1 \ x))) \ - (allI \ _ \ (\ x. impI \ _ \ _ \ (h2 \ x)))" + (arity_type_fun \ c \ d) \ + (arity_type_fun \ d \ c) \ + (allI \ _ \ c \ (\ x. impI \ _ \ _ \ (h1 \ x))) \ + (allI \ _ \ d \ (\ x. impI \ _ \ _ \ (h2 \ x)))" iffI (P): "\p. p" - "\ P Q (h1 : _) p (h2 : _). conjI \ _ \ _ \ - (allI \ _ \ (\ x. impI \ _ \ _ \ (h1 \ x))) \ + "\ (c: _) P Q (h1 : _) p (h2 : _). conjI \ _ \ _ \ + (allI \ _ \ c \ (\ x. impI \ _ \ _ \ (h1 \ x))) \ (impI \ _ \ _ \ h2)" iffI (Q): "\q. q" - "\ P Q q (h1 : _) (h2 : _). conjI \ _ \ _ \ + "\ (c: _) P Q q (h1 : _) (h2 : _). conjI \ _ \ _ \ (impI \ _ \ _ \ h1) \ - (allI \ _ \ (\ x. impI \ _ \ _ \ (h2 \ x)))" + (allI \ _ \ c \ (\ x. impI \ _ \ _ \ (h2 \ x)))" iffI: "Null" "iffI" -(* - classical: "Null" - "\ P. classical \ _" -*) - -setup {* - Sign.add_const_constraint (@{const_name "default"}, SOME @{typ "'a::default"}) -*} - end diff -r 7c59ab0a419b -r d94459cf7ea8 src/HOL/Lambda/WeakNorm.thy --- a/src/HOL/Lambda/WeakNorm.thy Tue Jun 01 11:37:41 2010 +0200 +++ b/src/HOL/Lambda/WeakNorm.thy Tue Jun 01 12:16:40 2010 +0200 @@ -264,6 +264,7 @@ lemmas [extraction_expand] = conj_assoc listall_cons_eq extract type_NF + lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b" apply (rule iffI) apply (erule rtranclpR.induct) diff -r 7c59ab0a419b -r d94459cf7ea8 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 01 12:16:40 2010 +0200 @@ -22,10 +22,6 @@ in map (fn ks => i::ks) is @ is end else [[]]; -fun forall_intr_prf (t, prf) = - let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) - in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end; - fun prf_of thm = Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm); @@ -130,12 +126,12 @@ val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []); val rvs = rev (Thm.fold_terms Term.add_vars thm' []); - val ivs1 = map Var (filter_out (fn (_, T) => (* FIXME set (!??) *) - member (op =) [@{type_abbrev set}, @{type_name bool}] (tname_of (body_type T))) ivs); + val ivs1 = map Var (filter_out (fn (_, T) => + @{type_name bool} = tname_of (body_type T)) ivs); val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs; val prf = - List.foldr forall_intr_prf + Extraction.abs_corr_shyps thy' induct vs ivs2 (fold_rev (fn (f, p) => fn prf => (case head_of (strip_abs_body f) of Free (s, T) => @@ -145,7 +141,7 @@ end | _ => AbsP ("H", SOME p, prf))) (rec_fns ~~ prems_of thm) - (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))) ivs2; + (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))); val r' = if null is then r @@ -198,18 +194,21 @@ ||> Sign.restore_naming thy; val P = Var (("P", 0), rT' --> HOLogic.boolT); - val prf = forall_intr_prf (y, forall_intr_prf (P, - fold_rev (fn (p, r) => fn prf => - forall_intr_prf (Logic.varify_global r, AbsP ("H", SOME (Logic.varify_global p), prf))) + val prf = Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P] + (fold_rev (fn (p, r) => fn prf => + 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 (prf_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); 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]))))); in Extraction.add_realizers_i [(exh_name, (["P"], r', prf)), - (exh_name, ([], Extraction.nullt, prf_of exhaust))] thy' + (exh_name, ([], Extraction.nullt, prf'))] thy' end; fun add_dt_realizers config names thy = diff -r 7c59ab0a419b -r d94459cf7ea8 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 01 12:16:40 2010 +0200 @@ -21,18 +21,12 @@ [name] => name | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm)); -val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps}; - 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 *) -fun forall_intr_prf t prf = - let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) - in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end; - fun subsets [] = [[]] | subsets (x::xs) = let val ys = subsets xs @@ -55,15 +49,19 @@ (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q)) | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q); -fun relevant_vars prop = List.foldr (fn - (Var ((a, i), T), vs) => (case strip_type T of +fun relevant_vars prop = fold (fn ((a, i), T) => fn vs => + (case strip_type T of (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs - | _ => vs) - | (_, vs) => vs) [] (OldTerm.term_vars prop); + | _ => vs)) (Term.add_vars prop []) []; + +val attach_typeS = map_types (map_atyps + (fn TFree (s, []) => TFree (s, HOLogic.typeS) + | TVar (ixn, []) => TVar (ixn, HOLogic.typeS) + | T => T)); fun dt_of_intrs thy vs nparms intrs = let - val iTs = OldTerm.term_tvars (prop_of (hd intrs)); + val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []); val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intrs)))); val params = map dest_Var (take nparms ts); @@ -84,7 +82,7 @@ fun gen_rvar vs (t as Var ((a, 0), T)) = if body_type T <> HOLogic.boolT then t else let - val U = TVar (("'" ^ a, 0), HOLogic.typeS) + val U = TVar (("'" ^ a, 0), []) val Ts = binder_types T; val i = length Ts; val xs = map (pair "x") Ts; @@ -98,8 +96,9 @@ fun mk_realizes_eqn n vs nparms intrs = let - val concl = HOLogic.dest_Trueprop (concl_of (hd intrs)); - val iTs = OldTerm.term_tvars concl; + val intr = map_types Type.strip_sorts (prop_of (hd intrs)); + val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr); + val iTs = rev (Term.add_tvars intr []); val Tvs = map TVar iTs; val (h as Const (s, T), us) = strip_comb concl; val params = List.take (us, nparms); @@ -110,7 +109,7 @@ (Name.variant_list used (replicate (length elTs) "x") ~~ elTs); val rT = if n then Extraction.nullT else Type (space_implode "_" (s ^ "T" :: vs), - map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs); + map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs); val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT); val S = list_comb (h, params @ xs); val rvs = relevant_vars S; @@ -121,7 +120,7 @@ let val T = (the o AList.lookup (op =) rvs) v in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T), Extraction.mk_typ (if n then Extraction.nullT - else TVar (("'" ^ v, 0), HOLogic.typeS))) + else TVar (("'" ^ v, 0), []))) end; val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs; @@ -261,12 +260,12 @@ val rlzvs = rev (Term.add_vars (prop_of rrule) []); val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs; val rs = map Var (subtract (op = o pairself fst) xs rlzvs); - val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule); - val rlz'' = fold_rev Logic.all vs2 rlz + val rlz' = fold_rev Logic.all rs (prop_of rrule) in (name, (vs, if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt, - ProofRewriteRules.un_hhf_proof rlz' rlz'' - (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule)))) + Extraction.abs_corr_shyps thy rule vs vs2 + (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz) + (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule))))) end; fun rename tab = map (fn x => the_default x (AList.lookup op = tab x)); @@ -275,7 +274,7 @@ let val qualifier = Long_Name.qualifier (name_of_thm induct); val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts"); - val iTs = OldTerm.term_tvars (prop_of (hd intrs)); + val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []); val ar = length vs + length iTs; val params = Inductive.params_of raw_induct; val arities = Inductive.arities_of raw_induct; @@ -297,8 +296,6 @@ val thy1' = thy1 |> Theory.copy |> Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |> - fold (fn s => AxClass.axiomatize_arity - (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |> Extraction.add_typeof_eqns_i ty_eqs; val dts = map_filter (fn (s, rs) => if member (op =) rsets s then SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss; @@ -328,10 +325,10 @@ end else (replicate (length rs) Extraction.nullt, (recs, dummies))) rss (rec_thms, dummies); - val rintrs = map (fn (intr, c) => Envir.eta_contract + val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract (Extraction.realizes_of thy2 vs (if c = Extraction.nullt then c else list_comb (c, map Var (rev - (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr))) + (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))) (maps snd rss ~~ flat constrss); val (rlzpreds, rlzpreds') = rintrs |> map (fn rintr => @@ -390,7 +387,9 @@ val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs')); val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms); - val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY + val thm = Goal.prove_global thy [] + (map attach_typeS prems) (attach_typeS concl) + (fn {prems, ...} => EVERY [rtac (#raw_induct ind_info) 1, rewrite_goals_tac rews, REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' @@ -408,10 +407,10 @@ in Extraction.add_realizers_i (map (fn (((ind, corr), rlz), r) => - mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r)) + mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r)) realizers @ (case realizers of [(((ind, corr), rlz), r)] => - [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct", + [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct", ind, corr, rlz, r)] | _ => [])) thy'' end; @@ -445,7 +444,7 @@ map reorder2 (intrs ~~ (length prems - 1 downto 0)) @ [Bound (length prems)])); val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim); - val rlz' = strip_all (Logic.unvarify_global rlz); + val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz)); val rews = map mk_meta_eq case_thms; val thm = Goal.prove_global thy [] (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY @@ -488,7 +487,7 @@ val vss = sort (int_ord o pairself length) (subsets (map fst (relevant_vars (concl_of (hd intrs))))) in - fold (add_ind_realizer rsets intrs induct raw_induct elims) vss thy + fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy end fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping diff -r 7c59ab0a419b -r d94459cf7ea8 src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 01 12:16:40 2010 +0200 @@ -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 * Proofterm.proof) option + val elim_cong: typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option end; structure RewriteHOLProof : REWRITE_HOL_PROOF = @@ -16,7 +16,7 @@ open Proofterm; val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o - Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} propT) + Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT) (** eliminate meta-equality rules **) @@ -24,237 +24,258 @@ \ (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %% \ \ (axm.reflexive % TYPE('T3) % x4) %% prf1)) == \ \ (iffD1 % A % B %% \ - \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))", + \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))", "(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %% \ \ (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %% \ \ (axm.reflexive % TYPE('T4) % x6) %% prf1))) == \ \ (iffD2 % A % B %% \ - \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))", + \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))", - "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% \ + "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% prfU %% \ \ (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) == \ \ (cong % TYPE('T) % TYPE('U) % f % g % x % y %% \ - \ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %% \ - \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))", - - "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% \ - \ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \ - \ (HOL.trans % TYPE('T) % x % y % z %% \ - \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf1) %% \ - \ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prf2))", + \ (OfClass type_class % TYPE('T)) %% prfU %% \ + \ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% (OfClass type_class % TYPE('T => 'U)) %% prf1) %% \ + \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% (OfClass type_class % TYPE('T)) %% prf2))", - "(meta_eq_to_obj_eq % TYPE('T) % x % x %% (axm.reflexive % TYPE('T) % x)) == \ - \ (HOL.refl % TYPE('T) % x)", + "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% \ + \ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \ + \ (HOL.trans % TYPE('T) % x % y % z %% prfT %% \ + \ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf1) %% \ + \ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prfT %% prf2))", - "(meta_eq_to_obj_eq % TYPE('T) % x % y %% \ + "(meta_eq_to_obj_eq % TYPE('T) % x % x %% prfT %% (axm.reflexive % TYPE('T) % x)) == \ + \ (HOL.refl % TYPE('T) % x %% prfT)", + + "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% \ \ (axm.symmetric % TYPE('T) % x % y %% prf)) == \ - \ (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))", + \ (sym % TYPE('T) % x % y %% prfT %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf))", - "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% \ + "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% prfTU %% \ \ (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) == \ \ (ext % TYPE('T) % TYPE('U) % f % g %% \ - \ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))", + \ (OfClass type_class % TYPE('T)) %% (OfClass type_class % TYPE('U)) %% \ + \ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% \ + \ (OfClass type_class % TYPE('U)) %% (prf % x)))", - "(meta_eq_to_obj_eq % TYPE('T) % x % y %% \ - \ (eq_reflection % TYPE('T) % x % y %% prf)) == prf", + "(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% \ + \ (eq_reflection % TYPE('T) % x % y %% prfT %% prf)) == prf", - "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \ + "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %% \ \ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \ \ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \ \ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) == \ \ (iffD1 % A = C % B = D %% \ - \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \ + \ (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %% \ + \ prfT %% arity_type_bool %% \ \ (cong % TYPE('T) % TYPE('T=>bool) % \ \ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \ - \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ - \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ - \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ - \ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prf3))", + \ prfT %% (OfClass type_class % TYPE('T=>bool)) %% \ + \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %% \ + \ (OfClass type_class % TYPE('T=>'T=>bool))) %% \ + \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %% \ + \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %% \ + \ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prfT %% prf3))", - "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \ + "(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %% \ \ (axm.symmetric % TYPE('T2) % x5 % x6 %% \ \ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \ \ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \ \ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) == \ \ (iffD2 % A = C % B = D %% \ - \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \ + \ (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %% \ + \ prfT %% arity_type_bool %% \ \ (cong % TYPE('T) % TYPE('T=>bool) % \ \ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \ - \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \ - \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \ - \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prf2)) %% \ - \ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prf3))", + \ prfT %% (OfClass type_class % TYPE('T=>bool)) %% \ + \ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %% \ + \ (OfClass type_class % TYPE('T=>'T=>bool))) %% \ + \ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %% \ + \ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %% \ + \ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prfT %% prf3))", (** rewriting on bool: insert proper congruence rules for logical connectives **) (* All *) - "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \ - \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \ - \ (allI % TYPE('a) % Q %% \ + "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %% \ + \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \ + \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \ + \ (allI % TYPE('a) % Q %% prfa %% \ \ (Lam x. \ \ iffD1 % P x % Q x %% (prf % x) %% \ - \ (spec % TYPE('a) % P % x %% prf')))", + \ (spec % TYPE('a) % P % x %% prfa %% prf')))", - "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \ - \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \ - \ (allI % TYPE('a) % P %% \ + "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %% \ + \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \ + \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \ + \ (allI % TYPE('a) % P %% prfa %% \ \ (Lam x. \ \ iffD2 % P x % Q x %% (prf % x) %% \ - \ (spec % TYPE('a) % Q % x %% prf')))", + \ (spec % TYPE('a) % Q % x %% prfa %% prf')))", (* Ex *) - "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \ - \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \ - \ (exE % TYPE('a) % P % EX x. Q x %% prf' %% \ + "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \ + \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \ + \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \ + \ (exE % TYPE('a) % P % EX x. Q x %% prfa %% prf' %% \ \ (Lam x H : P x. \ - \ exI % TYPE('a) % Q % x %% \ + \ exI % TYPE('a) % Q % x %% prfa %% \ \ (iffD1 % P x % Q x %% (prf % x) %% H)))", - "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \ - \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \ - \ (exE % TYPE('a) % Q % EX x. P x %% prf' %% \ + "(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \ + \ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \ + \ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \ + \ (exE % TYPE('a) % Q % EX x. P x %% prfa %% prf' %% \ \ (Lam x H : Q x. \ - \ exI % TYPE('a) % P % x %% \ + \ exI % TYPE('a) % P % x %% prfa %% \ \ (iffD2 % P x % Q x %% (prf % x) %% H)))", (* & *) - "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \ - \ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \ + "(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \ \ (conjI % B % D %% \ \ (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %% \ \ (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))", - "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% \ - \ (HOL.refl % TYPE('T5) % op &) %% prf1) %% prf2) %% prf3) == \ + "(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \ \ (conjI % A % C %% \ \ (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %% \ \ (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))", - "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \ - \ (HOL.refl % TYPE(bool=>bool) % op & A)) == \ - \ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \ + "(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \ + \ (HOL.refl % TYPE(bool=>bool) % op & A %% prfbb)) == \ + \ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \ \ (cong % TYPE(bool) % TYPE(bool=>bool) % \ \ (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %% \ - \ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %% \ - \ (HOL.refl % TYPE(bool) % A)))", + \ prfb %% prfbb %% \ + \ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool) %% \ + \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \ + \ (HOL.refl % TYPE(bool) % A %% prfb)))", (* | *) - "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \ - \ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \ + "(iffD1 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) == \ \ (disjE % A % C % B | D %% prf3 %% \ \ (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %% \ \ (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))", - "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% \ - \ (HOL.refl % TYPE('T5) % op | ) %% prf1) %% prf2) %% prf3) == \ + "(iffD2 % A | C % B | D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op | % op | % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op | %% prfT5) %% prf1) %% prf2) %% prf3) == \ \ (disjE % B % D % A | C %% prf3 %% \ \ (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %% \ \ (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))", - "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \ - \ (HOL.refl % TYPE(bool=>bool) % op | A)) == \ - \ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \ + "(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %% \ + \ (HOL.refl % TYPE(bool=>bool) % op | A %% prfbb)) == \ + \ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% prfb %% prfb %% \ \ (cong % TYPE(bool) % TYPE(bool=>bool) % \ \ (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %% \ - \ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %% \ - \ (HOL.refl % TYPE(bool) % A)))", + \ prfb %% prfbb %% \ + \ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool) %% \ + \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \ + \ (HOL.refl % TYPE(bool) % A %% prfb)))", (* --> *) - "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \ - \ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \ + "(iffD1 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) == \ \ (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %% \ \ (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))", - "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% \ - \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% \ - \ (HOL.refl % TYPE('T5) % op --> ) %% prf1) %% prf2) %% prf3) == \ + "(iffD2 % A --> C % B --> D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ + \ (cong % TYPE('T3) % TYPE('T4) % op --> % op --> % A % B %% prfT3 %% prfT4 %% \ + \ (HOL.refl % TYPE('T5) % op --> %% prfT5) %% prf1) %% prf2) %% prf3) == \ \ (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %% \ \ (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))", - "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \ - \ (HOL.refl % TYPE(bool=>bool) % op --> A)) == \ - \ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \ + "(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %% \ + \ (HOL.refl % TYPE(bool=>bool) % op --> A %% prfbb)) == \ + \ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% prfb %% prfb %% \ \ (cong % TYPE(bool) % TYPE(bool=>bool) % \ \ (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %% \ - \ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %% \ - \ (HOL.refl % TYPE(bool) % A)))", + \ prfb %% prfbb %% \ + \ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool) %% \ + \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \ + \ (HOL.refl % TYPE(bool) % A %% prfb)))", (* ~ *) - "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \ - \ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \ + "(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \ + \ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \ \ (notI % Q %% (Lam H: Q. \ \ notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))", - "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% \ - \ (HOL.refl % TYPE('T3) % Not) %% prf1) %% prf2) == \ + "(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \ + \ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \ \ (notI % P %% (Lam H: P. \ \ notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))", (* = *) "(iffD1 % B % D %% \ - \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \ - \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \ - \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \ + \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \ + \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \ + \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \ \ (iffD1 % C % D %% prf2 %% \ \ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))", "(iffD2 % B % D %% \ - \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \ - \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \ - \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \ + \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \ + \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \ + \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \ \ (iffD1 % A % B %% prf1 %% \ \ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))", "(iffD1 % A % C %% \ - \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \ - \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \ - \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)== \ + \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \ + \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \ + \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4)== \ \ (iffD2 % C % D %% prf2 %% \ \ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))", "(iffD2 % A % C %% \ - \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \ - \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \ - \ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \ + \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \ + \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \ + \ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \ \ (iffD2 % A % B %% prf1 %% \ \ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))", - "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \ - \ (HOL.refl % TYPE(bool=>bool) % op = A)) == \ - \ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \ + "(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %% \ + \ (HOL.refl % TYPE(bool=>bool) % op = A %% prfbb)) == \ + \ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %% \ \ (cong % TYPE(bool) % TYPE(bool=>bool) % \ \ (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %% \ - \ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %% \ - \ (HOL.refl % TYPE(bool) % A)))", + \ prfb %% prfbb %% \ + \ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool) %% \ + \ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \ + \ (HOL.refl % TYPE(bool) % A %% prfb)))", (** transitivity, reflexivity, and symmetry **) - "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \ + "(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) == \ \ (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))", - "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prf1 %% prf2) %% prf3) == \ + "(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) == \ \ (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))", - "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf", + "(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf", - "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A) %% prf) == prf", + "(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf", - "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD2 % B % A %% prf)", + "(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD2 % B % A %% prf)", - "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prf)) == (iffD1 % B % A %% prf)", + "(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD1 % B % A %% prf)", (** normalization of HOL proofs **) @@ -262,13 +283,13 @@ "(impI % A % B %% (mp % A % B %% prf)) == prf", - "(spec % TYPE('a) % P % x %% (allI % TYPE('a) % P %% prf)) == prf % x", + "(spec % TYPE('a) % P % x %% prfa %% (allI % TYPE('a) % P %% prfa %% prf)) == prf % x", - "(allI % TYPE('a) % P %% (Lam x::'a. spec % TYPE('a) % P % x %% prf)) == prf", + "(allI % TYPE('a) % P %% prfa %% (Lam x::'a. spec % TYPE('a) % P % x %% prfa %% prf)) == prf", - "(exE % TYPE('a) % P % Q %% (exI % TYPE('a) % P % x %% prf1) %% prf2) == (prf2 % x %% prf1)", + "(exE % TYPE('a) % P % Q %% prfa %% (exI % TYPE('a) % P % x %% prfa %% prf1) %% prf2) == (prf2 % x %% prf1)", - "(exE % TYPE('a) % P % Q %% prf %% (exI % TYPE('a) % P)) == prf", + "(exE % TYPE('a) % P % Q %% prfa %% prf %% (exI % TYPE('a) % P %% prfa)) == prf", "(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)", @@ -286,26 +307,26 @@ (** Replace congruence rules by substitution rules **) fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %% - prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1 - | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps) + prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1 + | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps) | strip_cong _ _ = NONE; -val subst_prf = fst (strip_combt (Thm.proof_of subst)); -val sym_prf = fst (strip_combt (Thm.proof_of sym)); +val subst_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of subst)))); +val sym_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of sym)))); fun make_subst Ts prf xs (_, []) = prf - | make_subst Ts prf xs (f, ((x, y), prf') :: ps) = + | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) = let val T = fastype_of1 (Ts, x) in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps) else change_type (SOME [T]) subst_prf %> x %> y %> Abs ("z", T, list_comb (incr_boundvars 1 f, map (incr_boundvars 1) xs @ Bound 0 :: - map (incr_boundvars 1 o snd o fst) ps)) %% prf' %% + map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %% make_subst Ts prf (xs @ [x]) (f, ps) end; -fun make_sym Ts ((x, y), prf) = - ((y, x), change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% prf); +fun make_sym Ts ((x, y), (prf, clprf)) = + ((y, x), (change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf)); fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t); @@ -322,6 +343,6 @@ apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf)) | elim_cong_aux _ _ = NONE; -fun elim_cong Ts prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf); +fun elim_cong Ts hs prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf); end; diff -r 7c59ab0a419b -r d94459cf7ea8 src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/Pure/Isar/class_target.ML Tue Jun 01 12:16:40 2010 +0200 @@ -243,7 +243,7 @@ | NONE => I in thy - |> AxClass.add_classrel classrel + |> AxClass.add_classrel true classrel |> ClassData.map (Graph.add_edge (sub, sup)) |> activate_defs sub (these_defs thy diff_sort) |> add_dependency @@ -366,7 +366,7 @@ fun gen_classrel mk_prop classrel thy = let fun after_qed results = - ProofContext.theory ((fold o fold) AxClass.add_classrel results); + ProofContext.theory ((fold o fold) (AxClass.add_classrel true) results); in thy |> ProofContext.init_global @@ -531,7 +531,7 @@ val (tycos, vs, sort) = (#arities o the_instantiation) lthy; val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; fun after_qed' results = - Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) + Local_Theory.theory (fold (AxClass.add_arity true o Thm.varifyT_global) results) #> after_qed; in lthy @@ -591,7 +591,7 @@ val sorts = map snd vs; val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; fun after_qed results = ProofContext.theory - ((fold o fold) AxClass.add_arity results); + ((fold o fold) (AxClass.add_arity true) results); in thy |> ProofContext.init_global diff -r 7c59ab0a419b -r d94459cf7ea8 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Jun 01 12:16:40 2010 +0200 @@ -24,6 +24,7 @@ val mk_typ : typ -> term val etype_of : theory -> string list -> typ list -> term -> typ val realizes_of: theory -> string list -> term -> term -> term + val abs_corr_shyps: theory -> thm -> string list -> term list -> Proofterm.proof -> Proofterm.proof end; structure Extraction : EXTRACTION = @@ -126,11 +127,9 @@ fun frees_of t = map Free (rev (Term.add_frees t [])); fun vfs_of t = vars_of t @ frees_of t; -fun forall_intr_prf (t, prf) = - let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) - in Abst (a, SOME T, prf_abstract_over t prf) end; +val mkabs = fold_rev (fn v => fn t => Abs ("x", fastype_of v, abstract_over (v, t))); -val mkabs = List.foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t))); +val mkabsp = fold_rev (fn t => fn prf => AbsP ("H", SOME t, prf)); fun strip_abs 0 t = t | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t @@ -161,6 +160,14 @@ | _ => error "get_var_type: not a variable" end; +fun read_term thy T s = + let + val ctxt = ProofContext.init_global thy + |> Proof_Syntax.strip_sorts_consttypes + |> ProofContext.set_defsort []; + val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term; + in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end; + (**** theory data ****) @@ -175,7 +182,7 @@ (term -> typ -> term -> typ -> term) option)) list, realizers : (string list * (term * proof)) list Symtab.table, defs : thm list, - expand : (string * term) list, + expand : string list, prep : (theory -> proof -> proof) option} val empty = @@ -198,14 +205,14 @@ types = AList.merge (op =) (K true) (types1, types2), realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2), defs = Library.merge Thm.eq_thm (defs1, defs2), - expand = Library.merge (op =) (expand1, expand2), (* FIXME proper aconv !?! *) + expand = Library.merge (op =) (expand1, expand2), prep = (case prep1 of NONE => prep2 | _ => prep1)}; ); fun read_condeq thy = let val thy' = add_syntax thy in fn s => - let val t = Logic.varify_global (Syntax.read_prop_global thy' s) + let val t = Logic.varify_global (read_term thy' propT s) in (map Logic.dest_equals (Logic.strip_imp_prems t), Logic.dest_equals (Logic.strip_imp_concl t)) @@ -274,7 +281,7 @@ fun err () = error ("Unable to determine type of extracted program for\n" ^ Syntax.string_of_term_global thy t) in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns) - [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts), + [typeof_proc [] vs]) (list_abs (map (pair "x") (rev Ts), Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of Const ("Type", _) $ u => (Logic.dest_type u handle TERM _ => err ()) | _ => err () @@ -300,25 +307,30 @@ val rtypes = map fst types; val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); val thy' = add_syntax thy; - val rd = Proof_Syntax.read_proof thy' false; + val rd = Proof_Syntax.read_proof thy' true false; in fn (thm, (vs, s1, s2)) => let val name = Thm.derivation_name thm; val _ = name <> "" orelse error "add_realizers: unnamed theorem"; - val prop = Pattern.rewrite_term thy' - (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm); + val prop = Thm.unconstrainT thm |> prop_of |> + Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) []; val vars = vars_of prop; val vars' = filter_out (fn v => member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars; + val shyps = maps (fn Var ((x, i), _) => + if member (op =) vs x then Logic.mk_of_sort + (TVar (("'" ^ x, i), []), Sign.defaultS thy') + else []) vars; val T = etype_of thy' vs [] prop; val (T', thw) = Type.legacy_freeze_thaw_type (if T = nullT then nullT else map fastype_of vars' ---> T); - val t = map_types thw (OldGoals.simple_read_term thy' T' s1); + val t = map_types thw (read_term thy' T' s1); val r' = freeze_thaw (condrew thy' eqns - (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc])) + (procs @ [typeof_proc [] vs, rlz_proc])) (Const ("realizes", T --> propT --> propT) $ (if T = nullT then t else list_comb (t, vars')) $ prop); - val r = fold_rev Logic.all (map (get_var_type r') vars) r'; + val r = Logic.list_implies (shyps, + fold_rev Logic.all (map (get_var_type r') vars) r'); val prf = Reconstruct.reconstruct_proof thy' r (rd s2); in (name, (vs, (t, prf))) end end; @@ -337,10 +349,34 @@ val prop' = Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) [] prop; in freeze_thaw (condrew thy' eqns - (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc])) + (procs @ [typeof_proc [] vs, rlz_proc])) (Const ("realizes", fastype_of t --> propT --> propT) $ t $ prop') end; +fun abs_corr_shyps thy thm vs xs prf = + let + val S = Sign.defaultS thy; + val ((atyp_map, constraints, _), prop') = + Logic.unconstrainT (#shyps (rep_thm thm)) (prop_of thm); + val atyps = fold_types (fold_atyps (insert (op =))) (prop_of thm) []; + val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then + SOME (TVar (("'" ^ v, i), [])) else NONE) + (rev (Term.add_vars prop' [])); + val cs = maps (fn T => map (pair T) S) Ts; + val constraints' = map Logic.mk_of_class cs; + val cs' = rev (cs @ map (Logic.dest_of_class o snd) constraints); + fun typ_map T = Type.strip_sorts + (map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T); + fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c)); + val xs' = map (map_types typ_map) xs + in + prf |> + Same.commit (map_proof_same (map_types typ_map) typ_map mk_hyp) |> + fold_rev implies_intr_proof' (map snd constraints) |> + fold_rev forall_intr_proof' xs' |> + fold_rev implies_intr_proof' constraints' + end; + (** expanding theorems / definitions **) fun add_expand_thm is_def thm thy = @@ -354,15 +390,15 @@ thy |> ExtractionData.put (if is_def then {realizes_eqns = realizes_eqns, - typeof_eqns = add_rule ([], - Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns, + typeof_eqns = add_rule ([], Logic.dest_equals (map_types + Type.strip_sorts (prop_of (Drule.abs_def thm)))) typeof_eqns, types = types, realizers = realizers, defs = insert Thm.eq_thm thm defs, expand = expand, prep = prep} else {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types, realizers = realizers, defs = defs, - expand = insert (op =) (name, prop_of thm) expand, prep = prep}) + expand = insert (op =) name expand, prep = prep}) end; fun extraction_expand is_def = @@ -443,9 +479,9 @@ ExtractionData.get thy; val procs = maps (rev o fst o snd) types; val rtypes = map fst types; - val typroc = typeof_proc (Sign.defaultS thy'); + val typroc = typeof_proc []; val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o - Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand); + Reconstruct.expand_proof thy' (map (rpair NONE) ("" :: expand)); val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); fun find_inst prop Ts ts vs = @@ -464,6 +500,13 @@ in fold_rev add_args (take n vars ~~ take n ts) ([], []) end; + fun mk_shyps tye = maps (fn (ixn, _) => + Logic.mk_of_sort (TVar (ixn, []), Sign.defaultS thy)) tye; + + fun mk_sprfs cs tye = maps (fn (_, T) => + ProofRewriteRules.mk_of_sort_proof thy (map SOME cs) + (T, Sign.defaultS thy)) tye; + fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst); fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE); @@ -474,22 +517,22 @@ fun realizes_null vs prop = app_rlz_rews [] vs (Const ("realizes", nullT --> propT --> propT) $ nullt $ prop); - fun corr d defs vs ts Ts hs (PBound i) _ _ = (defs, PBound i) + fun corr d defs vs ts Ts hs cs (PBound i) _ _ = (defs, PBound i) - | corr d defs vs ts Ts hs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t = + | corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t = let val (defs', corr_prf) = corr d defs vs [] (T :: Ts) - (dummyt :: hs) prf (incr_pboundvars 1 0 prf') + (dummyt :: hs) cs prf (incr_pboundvars 1 0 prf') (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE) in (defs', Abst (s, SOME T, corr_prf)) end - | corr d defs vs ts Ts hs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t = + | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t = let val T = etype_of thy' vs Ts prop; val u = if T = nullT then (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE) else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE); val (defs', corr_prf) = corr d defs vs [] (T :: Ts) (prop :: hs) - (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u; + (prop :: cs) (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u; val rlz = Const ("realizes", T --> propT --> propT) in (defs', if T = nullT then AbsP ("R", @@ -500,10 +543,10 @@ (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf))) end - | corr d defs vs ts Ts hs (prf % SOME t) (prf' % _) t' = + | corr d defs vs ts Ts hs cs (prf % SOME t) (prf' % _) t' = let val (Us, T) = strip_type (fastype_of1 (Ts, t)); - val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs prf prf' + val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs cs prf prf' (if member (op =) rtypes (tname_of T) then t' else (case t' of SOME (u $ _) => SOME u | _ => NONE)); val u = if not (member (op =) rtypes (tname_of T)) then t else @@ -519,7 +562,7 @@ in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end in (defs', corr_prf % SOME u) end - | corr d defs vs ts Ts hs (prf1 %% prf2) (prf1' %% prf2') t = + | corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t = let val prop = Reconstruct.prop_of' hs prf2'; val T = etype_of thy' vs Ts prop; @@ -529,17 +572,19 @@ | _ => let val (defs1, u) = extr d defs vs [] Ts hs prf2' in (defs1, NONE, SOME u) end) - val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs prf1 prf1' f; - val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs prf2 prf2' u; + val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs cs prf1 prf1' f; + val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs cs prf2 prf2' u; in if T = nullT then (defs3, corr_prf1 %% corr_prf2) else (defs3, corr_prf1 % u %% corr_prf2) end - | corr d defs vs ts Ts hs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ = + | corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ = let val prf = join_proof body; val (vs', tye) = find_inst prop Ts ts vs; + val shyps = mk_shyps tye; + val sprfs = mk_sprfs cs tye; val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye; val T = etype_of thy' vs' [] prop; val defs' = if T = nullT then defs @@ -555,28 +600,31 @@ (if null vs' then "" else " (relevant variables: " ^ commas_quote vs' ^ ")")); val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf); - val (defs'', corr_prf) = - corr (d + 1) defs' vs' [] [] [] prf' prf' NONE; + val (defs'', corr_prf0) = corr (d + 1) defs' vs' [] [] [] + (rev shyps) prf' prf' NONE; + val corr_prf = mkabsp shyps corr_prf0; val corr_prop = Reconstruct.prop_of corr_prf; - val corr_prf' = List.foldr forall_intr_prf - (proof_combt + val corr_prf' = + proof_combP (proof_combt (PThm (serial (), ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))), - Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop)) - (map (get_var_type corr_prop) (vfs_of prop)) + Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop), + map PBound (length shyps - 1 downto 0)) |> + fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |> + mkabsp shyps in ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'', - prf_subst_TVars tye' corr_prf') + proof_combP (prf_subst_TVars tye' corr_prf', sprfs)) end - | SOME (_, (_, prf')) => (defs', prf_subst_TVars tye' prf')) + | SOME (_, (_, prf')) => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs))) | SOME rs => (case find vs' rs of - SOME (_, prf') => (defs', prf_subst_TVars tye' prf') + SOME (_, prf') => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs)) | NONE => error ("corr: no realizer for instance of theorem " ^ quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm (Reconstruct.prop_of (proof_combt (prf0, ts)))))) end - | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ = + | corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ = let val (vs', tye) = find_inst prop Ts ts vs; val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye @@ -584,13 +632,14 @@ if etype_of thy' vs' [] prop = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0) else case find vs' (Symtab.lookup_list realizers s) of - SOME (_, prf) => (defs, prf_subst_TVars tye' prf) + SOME (_, prf) => (defs, + proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye)) | NONE => error ("corr: no realizer for instance of axiom " ^ quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm (Reconstruct.prop_of (proof_combt (prf0, ts))))) end - | corr d defs vs ts Ts hs _ _ _ = error "corr: bad proof" + | corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof" and extr d defs vs ts Ts hs (PBound i) = (defs, Bound i) @@ -630,6 +679,7 @@ let val prf = join_proof body; val (vs', tye) = find_inst prop Ts ts vs; + val shyps = mk_shyps tye; val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye in case Symtab.lookup realizers s of @@ -641,18 +691,18 @@ else " (relevant variables: " ^ commas_quote vs' ^ ")")); val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf); val (defs', t) = extr (d + 1) defs vs' [] [] [] prf'; - val (defs'', corr_prf) = - corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t); + val (defs'', corr_prf) = corr (d + 1) defs' vs' [] [] [] + (rev shyps) prf' prf' (SOME t); val nt = Envir.beta_norm t; val args = filter_out (fn v => member (op =) rtypes (tname_of (body_type (fastype_of v)))) (vfs_of prop); val args' = filter (fn v => Logic.occs (v, nt)) args; - val t' = mkabs nt args'; + val t' = mkabs args' nt; val T = fastype_of t'; val cname = extr_name s vs'; val c = Const (cname, T); - val u = mkabs (list_comb (c, args')) args; + val u = mkabs args (list_comb (c, args')); val eqn = Logic.mk_equals (c, t'); val rlz = Const ("realizes", fastype_of nt --> propT --> propT); @@ -661,20 +711,22 @@ val f = app_rlz_rews [] vs' (Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop)); - val corr_prf' = - chtype [] equal_elim_axm %> lhs %> rhs %% + val corr_prf' = mkabsp shyps + (chtype [] equal_elim_axm %> lhs %> rhs %% (chtype [propT] symmetric_axm %> rhs %> lhs %% (chtype [T, propT] combination_axm %> f %> f %> c %> t' %% (chtype [T --> propT] reflexive_axm %> f) %% PAxm (cname ^ "_def", eqn, - SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf; + SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf); val corr_prop = Reconstruct.prop_of corr_prf'; - val corr_prf'' = List.foldr forall_intr_prf - (proof_combt + val corr_prf'' = + proof_combP (proof_combt (PThm (serial (), ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))), - Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop)) - (map (get_var_type corr_prop) (vfs_of prop)); + Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop), + map PBound (length shyps - 1 downto 0)) |> + fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |> + mkabsp shyps in ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'', subst_TVars tye' u) @@ -731,7 +783,7 @@ in thy' |> PureThy.store_thm (Binding.qualified_name (corr_name s vs), - Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop)) + Thm.varifyT_global (funpow (length (vars_of corr_prop)) (Thm.forall_elim_var 0) (Thm.forall_intr_frees (ProofChecker.thm_of_proof thy' (fst (Proofterm.freeze_thaw_prf prf)))))) diff -r 7c59ab0a419b -r d94459cf7ea8 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Jun 01 12:16:40 2010 +0200 @@ -6,14 +6,17 @@ signature PROOF_REWRITE_RULES = sig - val rew : bool -> typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option + val rew : bool -> typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option val rprocs : bool -> - (typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list + (typ list -> term option 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 val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof + val mk_of_sort_proof : theory -> term option list -> typ * sort -> Proofterm.proof list + val expand_of_class : theory -> typ list -> term option list -> Proofterm.proof -> + (Proofterm.proof * Proofterm.proof) option end; structure ProofRewriteRules : PROOF_REWRITE_RULES = @@ -21,7 +24,7 @@ open Proofterm; -fun rew b _ = +fun rew b _ _ = let fun ?? x = if b then SOME x else NONE; fun ax (prf as PAxm (s, prop, _)) Ts = @@ -219,31 +222,36 @@ fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []); fun insert_refl defs Ts (prf1 %% prf2) = - insert_refl defs Ts prf1 %% insert_refl defs Ts prf2 + let val (prf1', b) = insert_refl defs Ts prf1 + in + if b then (prf1', true) + else (prf1' %% fst (insert_refl defs Ts prf2), false) + end | insert_refl defs Ts (Abst (s, SOME T, prf)) = - Abst (s, SOME T, insert_refl defs (T :: Ts) prf) + (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false) | insert_refl defs Ts (AbsP (s, t, prf)) = - AbsP (s, t, insert_refl defs Ts prf) + (AbsP (s, t, fst (insert_refl defs Ts prf)), false) | insert_refl defs Ts prf = (case strip_combt prf of (PThm (_, ((s, prop, SOME Ts), _)), ts) => if member (op =) defs s then let val vs = vars_of prop; val tvars = Term.add_tvars prop [] |> rev; - val (_, rhs) = Logic.dest_equals prop; + val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop); val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts) (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs), map the ts); in - change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs' + (change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs', true) end - else prf - | (_, []) => prf - | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts)); + else (prf, false) + | (_, []) => (prf, false) + | (prf', ts) => (proof_combt' (fst (insert_refl defs Ts prf'), ts), false)); fun elim_defs thy r defs prf = let - val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs + val defs' = map (Logic.dest_equals o + map_types Type.strip_sorts o prop_of o Drule.abs_def) defs; val defnames = map Thm.derivation_name defs; val f = if not r then I else let @@ -258,7 +266,7 @@ in Reconstruct.expand_proof thy thms end; in rewrite_terms (Pattern.rewrite_term thy defs' []) - (insert_refl defnames [] (f prf)) + (fst (insert_refl defnames [] (f prf))) end; @@ -327,4 +335,35 @@ mk_prf Q end; + +(**** expand OfClass proofs ****) + +fun mk_of_sort_proof thy hs (T, S) = + let + val hs' = map + (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE) + | NONE => NONE) hs; + val sorts = AList.coalesce (op =) (rev (map_filter I hs')); + fun get_sort T = the_default [] (AList.lookup (op =) sorts T); + val subst = map_atyps + (fn T as TVar (ixn, _) => TVar (ixn, get_sort T) + | T as TFree (s, _) => TFree (s, get_sort T)); + fun hyp T_c = case find_index (equal (SOME T_c)) hs' of + ~1 => error "expand_of_class: missing class hypothesis" + | i => PBound i; + fun reconstruct prf prop = prf |> + Reconstruct.reconstruct_proof thy prop |> + Reconstruct.expand_proof thy [("", NONE)] |> + Same.commit (map_proof_same Same.same Same.same hyp) + in + map2 reconstruct + (of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S)) + (Logic.mk_of_sort (T, S)) + end; + +fun expand_of_class thy Ts hs (OfClass (T, c)) = + mk_of_sort_proof thy hs (T, [c]) |> + hd |> rpair no_skel |> SOME + | expand_of_class thy Ts hs _ = NONE; + end; diff -r 7c59ab0a419b -r d94459cf7ea8 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Tue Jun 01 12:16:40 2010 +0200 @@ -11,8 +11,9 @@ val proof_of_term: theory -> bool -> term -> Proofterm.proof val term_of_proof: Proofterm.proof -> term val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof) - val read_term: theory -> typ -> string -> term - val read_proof: theory -> bool -> string -> Proofterm.proof + val strip_sorts_consttypes: Proof.context -> Proof.context + val read_term: theory -> bool -> typ -> string -> term + val read_proof: theory -> bool -> bool -> string -> Proofterm.proof val proof_syntax: Proofterm.proof -> theory -> theory val proof_of: bool -> thm -> Proofterm.proof val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T @@ -109,7 +110,7 @@ | "thm" :: xs => let val name = Long_Name.implode xs; in (case AList.lookup (op =) thms name of - SOME thm => fst (strip_combt (Thm.proof_of thm)) + SOME thm => fst (strip_combt (fst (strip_combP (Thm.proof_of thm)))) | NONE => error ("Unknown theorem " ^ quote name)) end | _ => error ("Illegal proof constant name: " ^ quote s)) @@ -198,7 +199,14 @@ (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) end; -fun read_term thy = +fun strip_sorts_consttypes ctxt = + let val {constants = (_, tab), ...} = Consts.dest (ProofContext.consts_of ctxt) + in Symtab.fold (fn (s, (T, _)) => + ProofContext.add_const_constraint (s, SOME (Type.strip_sorts T))) + tab ctxt + end; + +fun read_term thy topsort = let val thm_names = filter_out (fn s => s = "") (map fst (PureThy.all_thms_of thy)); val axm_names = map fst (Theory.all_axioms_of thy); @@ -208,15 +216,19 @@ (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names) |> ProofContext.init_global |> ProofContext.allow_dummies - |> ProofContext.set_mode ProofContext.mode_schematic; + |> ProofContext.set_mode ProofContext.mode_schematic + |> (if topsort then + strip_sorts_consttypes #> + ProofContext.set_defsort [] + else I); in fn ty => fn s => (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s |> Type_Infer.constrain ty |> Syntax.check_term ctxt end; -fun read_proof thy = - let val rd = read_term thy proofT +fun read_proof thy topsort = + let val rd = read_term thy topsort proofT in fn ty => fn s => proof_of_term thy ty (Logic.varify_global (rd s)) end; fun proof_syntax prf = diff -r 7c59ab0a419b -r d94459cf7ea8 src/Pure/Proof/proofchecker.ML --- a/src/Pure/Proof/proofchecker.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/Pure/Proof/proofchecker.ML Tue Jun 01 12:16:40 2010 +0200 @@ -28,6 +28,48 @@ 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 |> prf_subst_bounds (map Free vs) |> + 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; @@ -45,9 +87,9 @@ fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) = let - val thm = Drule.implies_intr_hyps (lookup name); + val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name)); val {prop, ...} = rep_thm thm; - val _ = if prop aconv prop' then () else + 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'); @@ -70,7 +112,10 @@ 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 end + 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 @@ -86,6 +131,7 @@ 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) diff -r 7c59ab0a419b -r d94459cf7ea8 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/Pure/Proof/reconstruct.ML Tue Jun 01 12:16:40 2010 +0200 @@ -28,11 +28,7 @@ fun forall_intr_vfs prop = fold_rev Logic.all (vars_of prop @ frees_of prop) prop; -fun forall_intr_prf t prf = - let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) - in Abst (a, SOME T, prf_abstract_over t prf) end; - -fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf +fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (vars_of prop @ frees_of prop) prf; diff -r 7c59ab0a419b -r d94459cf7ea8 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/Pure/axclass.ML Tue Jun 01 12:16:40 2010 +0200 @@ -24,8 +24,8 @@ val read_classrel: theory -> xstring * xstring -> class * class val declare_overloaded: string * typ -> theory -> term * theory val define_overloaded: binding -> string * term -> theory -> thm * theory - val add_classrel: thm -> theory -> theory - val add_arity: thm -> theory -> theory + val add_classrel: bool -> thm -> theory -> theory + val add_arity: bool -> thm -> theory -> theory val prove_classrel: class * class -> tactic -> theory -> theory val prove_arity: string * sort list * sort -> tactic -> theory -> theory val define_class: binding * class list -> string list -> @@ -412,46 +412,55 @@ (* primitive rules *) -fun add_classrel raw_th thy = +fun add_classrel store raw_th thy = let val th = Thm.strip_shyps (Thm.transfer thy raw_th); val prop = Thm.plain_prop_of th; fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); val rel = Logic.dest_classrel prop handle TERM _ => err (); val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); - val th' = th + val (th', thy') = + if store then PureThy.store_thm + (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy + else (th, thy); + val th'' = th' |> Thm.unconstrainT - |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [])))] []; + |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] []; in - thy + thy' |> Sign.primitive_classrel (c1, c2) - |> (#2 oo put_trancl_classrel) ((c1, c2), th') + |> (#2 oo put_trancl_classrel) ((c1, c2), th'') |> perhaps complete_arities end; -fun add_arity raw_th thy = +fun add_arity store raw_th thy = let val th = Thm.strip_shyps (Thm.transfer thy raw_th); val prop = Thm.plain_prop_of th; fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); - val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); + val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); + + val (th', thy') = + if store then PureThy.store_thm + (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy + else (th, thy); val args = Name.names Name.context Name.aT Ss; val T = Type (t, map TFree args); - val std_vars = map (fn (a, S) => SOME (ctyp_of thy (TVar ((a, 0), [])))) args; + val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args; - val missing_params = Sign.complete_sort thy [c] - |> maps (these o Option.map #params o try (get_info thy)) - |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t)) + val missing_params = Sign.complete_sort thy' [c] + |> maps (these o Option.map #params o try (get_info thy')) + |> filter_out (fn (const, _) => can (get_inst_param thy') (const, t)) |> (map o apsnd o map_atyps) (K T); - val th' = th + val th'' = th' |> Thm.unconstrainT |> Drule.instantiate' std_vars []; in - thy + thy' |> fold (#2 oo declare_overloaded) missing_params |> Sign.primitive_arity (t, Ss, [c]) - |> put_arity ((t, Ss, c), th') + |> put_arity ((t, Ss, c), th'') end; @@ -468,7 +477,7 @@ thy |> PureThy.add_thms [((Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])] - |-> (fn [th'] => add_classrel th') + |-> (fn [th'] => add_classrel false th') end; fun prove_arity raw_arity tac thy = @@ -484,7 +493,7 @@ in thy |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths)) - |-> fold add_arity + |-> fold (add_arity false) end; @@ -618,11 +627,11 @@ fun ax_classrel prep = axiomatize (map o prep) (map Logic.mk_classrel) - (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel; + (map (prefix classrel_prefix o Logic.name_classrel)) (add_classrel false); fun ax_arity prep = axiomatize (prep o ProofContext.init_global) Logic.mk_arities - (map (prefix arity_prefix) o Logic.name_arities) add_arity; + (map (prefix arity_prefix) o Logic.name_arities) (add_arity false); fun class_const c = (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT); diff -r 7c59ab0a419b -r d94459cf7ea8 src/Pure/logic.ML --- a/src/Pure/logic.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/Pure/logic.ML Tue Jun 01 12:16:40 2010 +0200 @@ -46,7 +46,8 @@ val name_arity: string * sort list * class -> string val mk_arities: arity -> term list val dest_arity: term -> string * sort list * class - val unconstrainT: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term + val unconstrainT: sort list -> term -> + ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term val protectC: term val protect: term -> term val unprotect: term -> term @@ -299,11 +300,15 @@ map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S) constraints_map; + val outer_constraints = + maps (fn (T, S) => map (pair T) S) + (present @ map (fn S => (TFree ("'dummy", S), S)) extra); + val prop' = prop |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map) |> curry list_implies (map snd constraints); - in ((atyp_map, constraints), prop') end; + in ((atyp_map, constraints, outer_constraints), prop') end; diff -r 7c59ab0a419b -r d94459cf7ea8 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/Pure/proofterm.ML Tue Jun 01 12:16:40 2010 +0200 @@ -58,6 +58,8 @@ val strip_combt: proof -> proof * term option list val strip_combP: proof -> proof * proof list val strip_thm: proof_body -> proof_body + val map_proof_same: term Same.operation -> typ Same.operation + -> (typ * class -> proof) -> proof Same.operation val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation val map_proof_types_same: typ Same.operation -> proof Same.operation val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof @@ -80,7 +82,9 @@ (** proof terms for specific inference rules **) val implies_intr_proof: term -> proof -> proof + val implies_intr_proof': term -> proof -> proof val forall_intr_proof: term -> string -> proof -> proof + val forall_intr_proof': term -> proof -> proof val varify_proof: term -> (string * sort) list -> proof -> proof val legacy_freezeT: term -> proof -> proof val rotate_proof: term list -> term -> int -> proof -> proof @@ -121,13 +125,13 @@ (** rewriting on proof terms **) val add_prf_rrule: proof * proof -> theory -> theory - val add_prf_rproc: (typ list -> proof -> (proof * proof) option) -> theory -> theory + val add_prf_rproc: (typ list -> term option 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 * proof) option) list -> proof -> proof + (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof val rewrite_proof_notypes: (proof * proof) list * - (typ list -> proof -> (proof * proof) option) list -> proof -> proof + (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof val rew_proof: theory -> proof -> proof val promise_proof: theory -> serial -> term -> proof @@ -618,7 +622,7 @@ (***** implication introduction *****) -fun implies_intr_proof h prf = +fun gen_implies_intr_proof f h prf = let fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME | abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf) @@ -630,14 +634,21 @@ | abshyp _ _ = raise Same.SAME and abshyph i prf = (abshyp i prf handle Same.SAME => prf); in - AbsP ("H", NONE (*h*), abshyph 0 prf) + AbsP ("H", f h, abshyph 0 prf) end; +val implies_intr_proof = gen_implies_intr_proof (K NONE); +val implies_intr_proof' = gen_implies_intr_proof SOME; + (***** forall introduction *****) fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf); +fun forall_intr_proof' t prf = + let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) + in Abst (a, SOME T, prf_abstract_over t prf) end; + (***** varify *****) @@ -1105,7 +1116,7 @@ fun flt (i: int) = filter (fn n => n < i); -fun fomatch Ts tymatch j = +fun fomatch Ts tymatch j instsp p = let fun mtch (instsp as (tyinsts, insts)) = fn (Var (ixn, T), t) => @@ -1120,7 +1131,7 @@ | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u) | (Bound i, Bound j) => if i=j then instsp else raise PMatch | _ => raise PMatch - in mtch end; + in mtch instsp (pairself Envir.beta_eta_contract p) end; fun match_proof Ts tymatch = let @@ -1253,72 +1264,72 @@ fun rewrite_prf tymatch (rules, procs) prf = let - 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 + 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 hs prf = + (case get_first (fn r => r Ts hs 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 + fun rew0 Ts hs (prf as AbsP (_, _, prf' %% PBound 0)) = + if prf_loose_Pbvar1 prf' 0 then rew Ts hs prf else let val prf'' = incr_pboundvars (~1) 0 prf' - 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 + in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end + | rew0 Ts hs (prf as Abst (_, _, prf' % SOME (Bound 0))) = + if prf_loose_bvar1 prf' 0 then rew Ts hs prf else let val prf'' = incr_pboundvars 0 (~1) prf' - in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end - | rew0 Ts prf = rew Ts prf; + in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end + | rew0 Ts hs prf = rew Ts hs prf; - fun rew1 _ (Hyp (Var _)) _ = NONE - | rew1 Ts skel prf = (case rew2 Ts skel prf of - SOME prf1 => (case rew0 Ts prf1 of - SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts skel' prf2)) + fun rew1 _ _ (Hyp (Var _)) _ = NONE + | rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of + SOME prf1 => (case rew0 Ts hs prf1 of + SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2)) | NONE => SOME prf1) - | NONE => (case rew0 Ts prf of - SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts skel' prf1)) + | NONE => (case rew0 Ts hs prf of + SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1)) | NONE => NONE)) - and rew2 Ts skel (prf % SOME t) = (case prf of + and rew2 Ts hs skel (prf % SOME t) = (case prf of Abst (_, _, body) => let val prf' = prf_subst_bounds [t] body - in SOME (the_default prf' (rew2 Ts no_skel prf')) end - | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf of + in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end + | _ => (case rew1 Ts hs (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' | _ => no_skel) prf) - | rew2 Ts skel (prf1 %% prf2) = (case prf1 of + | rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE) + (rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf) + | rew2 Ts hs skel (prf1 %% prf2) = (case prf1 of AbsP (_, _, body) => let val prf' = prf_subst_pbounds [prf2] body - in SOME (the_default prf' (rew2 Ts no_skel prf')) end + in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end | _ => let val (skel1, skel2) = (case skel of skel1 %% skel2 => (skel1, skel2) | _ => (no_skel, no_skel)) - in case rew1 Ts skel1 prf1 of - SOME prf1' => (case rew1 Ts skel2 prf2 of + in case rew1 Ts hs skel1 prf1 of + SOME prf1' => (case rew1 Ts hs skel2 prf2 of SOME prf2' => SOME (prf1' %% prf2') | NONE => SOME (prf1' %% prf2)) - | NONE => (case rew1 Ts skel2 prf2 of + | NONE => (case rew1 Ts hs skel2 prf2 of SOME prf2' => SOME (prf1 %% prf2') | NONE => NONE) end) - | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) + | rew2 Ts hs skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) hs (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 + | rew2 Ts hs skel (AbsP (s, t, prf)) = (case rew1 Ts (t :: hs) (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of SOME prf' => SOME (AbsP (s, t, prf')) | NONE => NONE) - | rew2 _ _ _ = NONE; + | rew2 _ _ _ _ = NONE; - in the_default prf (rew1 [] no_skel 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); @@ -1332,7 +1343,7 @@ ( type T = (stamp * (proof * proof)) list * - (stamp * (typ list -> proof -> (proof * proof) option)) list; + (stamp * (typ list -> term option list -> proof -> (proof * proof) option)) list; val empty = ([], []); val extend = I; @@ -1373,7 +1384,7 @@ | 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; + val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0; in PBody {oracles = oracles, thms = thms, proof = proof} end; fun fulfill_proof_future _ [] postproc body = Future.value (postproc body) @@ -1421,12 +1432,13 @@ val (postproc, ofclasses, prop1, args1) = if do_unconstrain then let - val ((atyp_map, constraints), prop1) = Logic.unconstrainT shyps prop; + val ((atyp_map, constraints, outer_constraints), prop1) = + Logic.unconstrainT shyps prop; val postproc = unconstrainT_body thy (atyp_map, constraints); val args1 = (map o Option.map o Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map) args; - in (postproc, map (OfClass o fst) constraints, prop1, args1) end + in (postproc, map OfClass outer_constraints, prop1, args1) end else (I, [], prop, args); val argsP = ofclasses @ map Hyp hyps; @@ -1447,7 +1459,7 @@ val head = PThm (i, ((name, prop1, NONE), body')); in ((i, (name, prop1, body')), head, args, argsP, args1) end; -val unconstrain_thm_proofs = Unsynchronized.ref false; +val unconstrain_thm_proofs = Unsynchronized.ref true; fun thm_proof thy name shyps hyps concl promises body = let val (pthm, head, args, argsP, _) = diff -r 7c59ab0a419b -r d94459cf7ea8 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Tue Jun 01 11:37:41 2010 +0200 +++ b/src/Pure/type_infer.ML Tue Jun 01 12:16:40 2010 +0200 @@ -295,11 +295,11 @@ | occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts | occurs_check _ _ _ = (); - fun assign i (T as Param (i', _)) S (tye_idx as (tye, idx)) = + fun assign i (T as Param (i', _)) S tye_idx = if i = i' then tye_idx - else meet (T, S) (Inttab.update_new (i, T) tye, idx) - | assign i T S (tye, idx) = - (occurs_check tye i T; meet (T, S) (Inttab.update_new (i, T) tye, idx)); + else tye_idx |> meet (T, S) |>> Inttab.update_new (i, T) + | assign i T S (tye_idx as (tye, _)) = + (occurs_check tye i T; tye_idx |> meet (T, S) |>> Inttab.update_new (i, T)); (* unification *)