# HG changeset patch # User krauss # Date 1269955530 -7200 # Node ID 85efdadee8aed0de5122baae687bafb2afe9a2d8 # Parent 8b25e3b217bce5f235def59a1e96e301b765ba97 switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged) diff -r 8b25e3b217bc -r 85efdadee8ae src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Tue Mar 30 12:47:39 2010 +0200 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Tue Mar 30 15:25:30 2010 +0200 @@ -33,8 +33,8 @@ \ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))", "(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% \ - \ (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) == \ - \ (cong % TYPE('U) % TYPE('T) % f % g % x % y %% \ + \ (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))", @@ -52,20 +52,20 @@ \ (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))", "(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% \ - \ (abstract_rule % TYPE('U) % TYPE('T) % f % g %% prf)) == \ - \ (ext % TYPE('U) % TYPE('T) % f % g %% \ + \ (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)))", "(meta_eq_to_obj_eq % TYPE('T) % x % y %% \ \ (eq_reflection % TYPE('T) % x % y %% prf)) == prf", "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \ - \ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \ - \ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \ + \ (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(bool) % TYPE('T::type) % op = A % op = B % C % D %% \ - \ (cong % TYPE('T=>bool) % TYPE('T) % \ + \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \ + \ (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)) %% \ @@ -74,12 +74,12 @@ "(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \ \ (axm.symmetric % TYPE('T2) % x5 % x6 %% \ - \ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \ - \ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \ + \ (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(bool) % TYPE('T::type) % op = A % op = B % C % D %% \ - \ (cong % TYPE('T=>bool) % TYPE('T) % \ + \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \ + \ (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)) %% \ @@ -91,14 +91,14 @@ (* All *) "(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \ - \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ + \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \ \ (allI % TYPE('a) % Q %% \ \ (Lam x. \ \ iffD1 % P x % Q x %% (prf % x) %% \ \ (spec % TYPE('a) % P % x %% prf')))", "(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \ - \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ + \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \ \ (allI % TYPE('a) % P %% \ \ (Lam x. \ \ iffD2 % P x % Q x %% (prf % x) %% \ @@ -107,14 +107,14 @@ (* Ex *) "(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \ - \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ + \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \ \ (exE % TYPE('a) % P % EX x. Q x %% prf' %% \ \ (Lam x H : P x. \ \ exI % TYPE('a) % Q % x %% \ \ (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(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \ + \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \ \ (exE % TYPE('a) % Q % EX x. P x %% prf' %% \ \ (Lam x H : Q x. \ \ exI % TYPE('a) % P % x %% \ @@ -139,7 +139,7 @@ "(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=>bool) % TYPE(bool) % \ + \ (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)))", @@ -163,7 +163,7 @@ "(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=>bool) % TYPE(bool) % \ + \ (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)))", @@ -185,7 +185,7 @@ "(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=>bool) % TYPE(bool) % \ + \ (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)))", @@ -205,29 +205,29 @@ (* = *) "(iffD1 % B % D %% \ - \ (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \ - \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \ + \ (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 % C % D %% prf2 %% \ \ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))", "(iffD2 % B % D %% \ - \ (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \ - \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \ + \ (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 % B %% prf1 %% \ \ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))", "(iffD1 % A % C %% \ - \ (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \ - \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \ + \ (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 % C % D %% prf2 %% \ \ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))", "(iffD2 % A % C %% \ - \ (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \ - \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \ + \ (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 % B %% prf1 %% \ \ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))", @@ -235,7 +235,7 @@ "(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=>bool) % TYPE(bool) % \ + \ (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)))", diff -r 8b25e3b217bc -r 85efdadee8ae src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Mar 30 12:47:39 2010 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Mar 30 15:25:30 2010 +0200 @@ -541,7 +541,7 @@ let val prf = join_proof body; val (vs', tye) = find_inst prop Ts ts vs; - val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ 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 else fst (extr d defs vs ts Ts hs prf0) @@ -562,7 +562,7 @@ val corr_prf' = List.foldr forall_intr_prf (proof_combt (PThm (serial (), - ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))), + ((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)) in @@ -580,7 +580,7 @@ | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ = let val (vs', tye) = find_inst prop Ts ts vs; - val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye + val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye in if etype_of thy' vs' [] prop = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0) @@ -631,7 +631,7 @@ let val prf = join_proof body; val (vs', tye) = find_inst prop Ts ts vs; - val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye + val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye in case Symtab.lookup realizers s of NONE => (case find vs' (find' s defs) of @@ -665,15 +665,15 @@ val corr_prf' = chtype [] equal_elim_axm %> lhs %> rhs %% (chtype [propT] symmetric_axm %> rhs %> lhs %% - (chtype [propT, T] combination_axm %> f %> f %> c %> t' %% + (chtype [T, propT] combination_axm %> f %> f %> c %> t' %% (chtype [T --> propT] reflexive_axm %> f) %% PAxm (cname ^ "_def", eqn, - SOME (map TVar (OldTerm.term_tvars eqn))))) %% 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 (PThm (serial (), - ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))), + ((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)); in @@ -691,7 +691,7 @@ | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) = let val (vs', tye) = find_inst prop Ts ts vs; - val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye + val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye in case find vs' (Symtab.lookup_list realizers s) of SOME (t, _) => (defs, subst_TVars tye' t) diff -r 8b25e3b217bc -r 85efdadee8ae src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Mar 30 12:47:39 2010 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Mar 30 15:25:30 2010 +0200 @@ -179,7 +179,7 @@ (PAxm ("Pure.reflexive", _, _) % _)) = let val (U, V) = (case T of Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT)) - in SOME (prf %% (ax combination_axm [V, U] %> eq % ?? eq % ?? t % ?? t %% + in SOME (prf %% (ax combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %% (ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t))) end @@ -229,7 +229,7 @@ if member (op =) defs s then let val vs = vars_of prop; - val tvars = OldTerm.term_tvars prop; + val tvars = Term.add_tvars prop [] |> rev; val (_, rhs) = Logic.dest_equals 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), diff -r 8b25e3b217bc -r 85efdadee8ae src/Pure/Proof/proofchecker.ML --- a/src/Pure/Proof/proofchecker.ML Tue Mar 30 12:47:39 2010 +0200 +++ b/src/Pure/Proof/proofchecker.ML Tue Mar 30 15:25:30 2010 +0200 @@ -35,7 +35,7 @@ fun thm_of_atom thm Ts = let - val tvars = OldTerm.term_tvars (Thm.full_prop_of thm); + val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev; val (fmap, thm') = Thm.varifyT_global' [] thm; val ctye = map (pairself (Thm.ctyp_of thy)) (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) diff -r 8b25e3b217bc -r 85efdadee8ae src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Tue Mar 30 12:47:39 2010 +0200 +++ b/src/Pure/Proof/reconstruct.ML Tue Mar 30 15:25:30 2010 +0200 @@ -136,8 +136,8 @@ fun mk_cnstrts_atom env vTs prop opTs prf = let - val tvars = OldTerm.term_tvars prop; - val tfrees = OldTerm.term_tfrees prop; + val tvars = Term.add_tvars prop [] |> rev; + val tfrees = Term.add_tfrees prop [] |> rev; val (Ts, env') = (case opTs of NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env @@ -304,7 +304,7 @@ end; fun prop_of_atom prop Ts = subst_atomic_types - (map TVar (OldTerm.term_tvars prop) @ map TFree (OldTerm.term_tfrees prop) ~~ Ts) + (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts) (forall_intr_vfs prop); val head_norm = Envir.head_norm (Envir.empty 0); @@ -370,9 +370,9 @@ end | SOME (maxidx', prf) => (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs)); - val tfrees = OldTerm.term_tfrees prop; + val tfrees = Term.add_tfrees prop [] |> rev; val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j)) - (OldTerm.term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts; + (Term.add_tvars prop [] |> rev) @ map (rpair ~1 o fst) tfrees ~~ Ts; val varify = map_type_tfree (fn p as (a, S) => if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p) in