switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
--- 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)))",
--- 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)
--- 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),
--- 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)
--- 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