# HG changeset patch # User berghofe # Date 1275383589 -7200 # Node ID b78f31ca46754fb71a4886c8c39848ab5663a817 # Parent c10fb22a5e0c907234a12365a3102b0912d88586 Adapted to new format of proof terms containing explicit proofs of class membership. diff -r c10fb22a5e0c -r b78f31ca4675 src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Tue Jun 01 11:04:49 2010 +0200 +++ b/src/HOL/Extraction.thy Tue Jun 01 11:13:09 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 c10fb22a5e0c -r b78f31ca4675 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 01 11:04:49 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Jun 01 11:13:09 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 c10fb22a5e0c -r b78f31ca4675 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 01 11:04:49 2010 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 01 11:13:09 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 (fst_conv :: 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 c10fb22a5e0c -r b78f31ca4675 src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 01 11:04:49 2010 +0200 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Tue Jun 01 11:13:09 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 c10fb22a5e0c -r b78f31ca4675 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Jun 01 11:04:49 2010 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Jun 01 11:13:09 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 |> TypeInfer.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 c10fb22a5e0c -r b78f31ca4675 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Jun 01 11:04:49 2010 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Jun 01 11:13:09 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;