# HG changeset patch
# User nipkow
# Date 971369075 -7200
# Node ID 01c2744a378621dad14341a7a8ef83c1e6812ec3
# Parent  33fe2d701ddda1b8f09cdddfd0397e9480a5730b
*** empty log message ***

diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,187 +0,0 @@
-(*  Title:      HOL/Arith.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Further proofs about elementary arithmetic, using the arithmetic proof
-procedures.
-*)
-
-(*legacy ...*)
-structure Arith = struct val thy = the_context () end;
-
-
-Goal "m <= m*(m::nat)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "le_square";
-
-Goal "(m::nat) <= m*(m*m)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "le_cube";
-
-
-(*** Subtraction laws -- mostly from Clemens Ballarin ***)
-
-Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
-by (arith_tac 1);
-qed "diff_less_mono";
-
-Goal "(i < j-k) = (i+k < (j::nat))";
-by (arith_tac 1);
-qed "less_diff_conv";
-
-Goal "(j-k <= (i::nat)) = (j <= i+k)";
-by (arith_tac 1);
-qed "le_diff_conv";
-
-Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
-by (arith_tac 1);
-qed "le_diff_conv2";
-
-Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
-by (arith_tac 1);
-qed "Suc_diff_Suc";
-
-Goal "i <= (n::nat) ==> n - (n - i) = i";
-by (arith_tac 1);
-qed "diff_diff_cancel";
-Addsimps [diff_diff_cancel];
-
-Goal "k <= (n::nat) ==> m <= n + m - k";
-by (arith_tac 1);
-qed "le_add_diff";
-
-Goal "m-1 < n ==> m <= n";
-by (arith_tac 1);
-qed "pred_less_imp_le";
-
-Goal "j<=i ==> i - j < Suc i - j";
-by (arith_tac 1);
-qed "diff_less_Suc_diff";
-
-Goal "i - j <= Suc i - j";
-by (arith_tac 1);
-qed "diff_le_Suc_diff";
-AddIffs [diff_le_Suc_diff];
-
-Goal "n - Suc i <= n - i";
-by (arith_tac 1);
-qed "diff_Suc_le_diff";
-AddIffs [diff_Suc_le_diff];
-
-Goal "!!m::nat. 0 < n ==> (m <= n-1) = (m<n)";
-by (arith_tac 1);
-qed "le_pred_eq";
-
-Goal "!!m::nat. 0 < n ==> (m-1 < n) = (m<=n)";
-by (arith_tac 1);
-qed "less_pred_eq";
-
-(*Replaces the previous diff_less and le_diff_less, which had the stronger
-  second premise n<=m*)
-Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
-by (arith_tac 1);
-qed "diff_less";
-
-Goal "j <= (k::nat) ==> (j+i)-k = i-(k-j)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_add_assoc_diff";
-
-
-(*** Reducing subtraction to addition ***)
-
-Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
-by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed_spec_mp "Suc_diff_add_le";
-
-Goal "i<n ==> n - Suc i < n - i";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_Suc_less_diff";
-
-Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
-by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "if_Suc_diff_le";
-
-Goal "Suc(m)-n <= Suc(m-n)";
-by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_Suc_le_Suc_diff";
-
-(** Simplification of relational expressions involving subtraction **)
-
-Goal "[| k <= m;  k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_diff_eq";
-
-Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-qed "eq_diff_iff";
-
-Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k < n-k) = (m<n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-qed "less_diff_iff";
-
-Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-qed "le_diff_iff";
-
-
-(** (Anti)Monotonicity of subtraction -- by Stephan Merz **)
-
-(* Monotonicity of subtraction in first argument *)
-Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_le_mono";
-
-Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_le_mono2";
-
-Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_less_mono2";
-
-Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n";
-by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diffs0_imp_equal";
-
-(** Lemmas for ex/Factorization **)
-
-Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
-by (case_tac "m" 1);
-by Auto_tac;
-qed "one_less_mult"; 
-
-Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n";
-by (case_tac "m" 1);
-by Auto_tac;
-qed "n_less_m_mult_n"; 
-
-Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
-by (case_tac "m" 1);
-by Auto_tac;
-qed "n_less_n_mult_m"; 
-
-
-(** Rewriting to pull differences out **)
-
-Goal "k<=j --> i - (j - k) = i + (k::nat) - j";
-by (arith_tac 1);
-qed "diff_diff_right";
-
-Goal "k <= j ==> m - Suc (j - k) = m + k - Suc j";
-by (arith_tac 1);
-qed "diff_Suc_diff_eq1"; 
-
-Goal "k <= j ==> Suc (j - k) - m = Suc j - (k + m)";
-by (arith_tac 1);
-qed "diff_Suc_diff_eq2"; 
-
-(*The others are
-      i - j - k = i - (j + k),
-      k <= j ==> j - k + i = j + i - k,
-      k <= j ==> i + (j - k) = i + j - k *)
-Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym, 
-	  diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2];
-
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(*  Title:      HOL/Arith.thy
-    ID:         $Id$
-
-Setup arithmetic proof procedures.
-*)
-
-theory Arith = Nat
-files "arith_data.ML":
-
-setup arith_setup
-
-(*elimination of `-' on nat*)
-lemma nat_diff_split:
-    "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
-  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
-
-ML {* val nat_diff_split = thm "nat_diff_split" *}
-
-lemmas [arith_split] = nat_diff_split split_min split_max
-
-end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Arithmetic.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Arithmetic.ML	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,187 @@
+(*  Title:      HOL/Arithmetic.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Further proofs about elementary arithmetic, using the arithmetic proof
+procedures.
+*)
+
+(*legacy ...*)
+structure Arithmetic = struct val thy = the_context () end;
+
+
+Goal "m <= m*(m::nat)";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "le_square";
+
+Goal "(m::nat) <= m*(m*m)";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "le_cube";
+
+
+(*** Subtraction laws -- mostly from Clemens Ballarin ***)
+
+Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
+by (arith_tac 1);
+qed "diff_less_mono";
+
+Goal "(i < j-k) = (i+k < (j::nat))";
+by (arith_tac 1);
+qed "less_diff_conv";
+
+Goal "(j-k <= (i::nat)) = (j <= i+k)";
+by (arith_tac 1);
+qed "le_diff_conv";
+
+Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
+by (arith_tac 1);
+qed "le_diff_conv2";
+
+Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
+by (arith_tac 1);
+qed "Suc_diff_Suc";
+
+Goal "i <= (n::nat) ==> n - (n - i) = i";
+by (arith_tac 1);
+qed "diff_diff_cancel";
+Addsimps [diff_diff_cancel];
+
+Goal "k <= (n::nat) ==> m <= n + m - k";
+by (arith_tac 1);
+qed "le_add_diff";
+
+Goal "m-1 < n ==> m <= n";
+by (arith_tac 1);
+qed "pred_less_imp_le";
+
+Goal "j<=i ==> i - j < Suc i - j";
+by (arith_tac 1);
+qed "diff_less_Suc_diff";
+
+Goal "i - j <= Suc i - j";
+by (arith_tac 1);
+qed "diff_le_Suc_diff";
+AddIffs [diff_le_Suc_diff];
+
+Goal "n - Suc i <= n - i";
+by (arith_tac 1);
+qed "diff_Suc_le_diff";
+AddIffs [diff_Suc_le_diff];
+
+Goal "!!m::nat. 0 < n ==> (m <= n-1) = (m<n)";
+by (arith_tac 1);
+qed "le_pred_eq";
+
+Goal "!!m::nat. 0 < n ==> (m-1 < n) = (m<=n)";
+by (arith_tac 1);
+qed "less_pred_eq";
+
+(*Replaces the previous diff_less and le_diff_less, which had the stronger
+  second premise n<=m*)
+Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
+by (arith_tac 1);
+qed "diff_less";
+
+Goal "j <= (k::nat) ==> (j+i)-k = i-(k-j)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_add_assoc_diff";
+
+
+(*** Reducing subtraction to addition ***)
+
+Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
+by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed_spec_mp "Suc_diff_add_le";
+
+Goal "i<n ==> n - Suc i < n - i";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_Suc_less_diff";
+
+Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
+by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "if_Suc_diff_le";
+
+Goal "Suc(m)-n <= Suc(m-n)";
+by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_Suc_le_Suc_diff";
+
+(** Simplification of relational expressions involving subtraction **)
+
+Goal "[| k <= m;  k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_diff_eq";
+
+Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
+qed "eq_diff_iff";
+
+Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k < n-k) = (m<n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
+qed "less_diff_iff";
+
+Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
+qed "le_diff_iff";
+
+
+(** (Anti)Monotonicity of subtraction -- by Stephan Merz **)
+
+(* Monotonicity of subtraction in first argument *)
+Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_le_mono";
+
+Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_le_mono2";
+
+Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_less_mono2";
+
+Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n";
+by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diffs0_imp_equal";
+
+(** Lemmas for ex/Factorization **)
+
+Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
+by (case_tac "m" 1);
+by Auto_tac;
+qed "one_less_mult"; 
+
+Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n";
+by (case_tac "m" 1);
+by Auto_tac;
+qed "n_less_m_mult_n"; 
+
+Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
+by (case_tac "m" 1);
+by Auto_tac;
+qed "n_less_n_mult_m"; 
+
+
+(** Rewriting to pull differences out **)
+
+Goal "k<=j --> i - (j - k) = i + (k::nat) - j";
+by (arith_tac 1);
+qed "diff_diff_right";
+
+Goal "k <= j ==> m - Suc (j - k) = m + k - Suc j";
+by (arith_tac 1);
+qed "diff_Suc_diff_eq1"; 
+
+Goal "k <= j ==> Suc (j - k) - m = Suc j - (k + m)";
+by (arith_tac 1);
+qed "diff_Suc_diff_eq2"; 
+
+(*The others are
+      i - j - k = i - (j + k),
+      k <= j ==> j - k + i = j + i - k,
+      k <= j ==> i + (j - k) = i + j - k *)
+Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym, 
+	  diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2];
+
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Arithmetic.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Arithmetic.thy	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,21 @@
+(*  Title:      HOL/Arithmetic.thy
+    ID:         $Id$
+
+Setup arithmetic proof procedures.
+*)
+
+theory Arithmetic = Nat
+files "arith_data.ML":
+
+setup arith_setup
+
+(*elimination of `-' on nat*)
+lemma nat_diff_split:
+    "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
+  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
+
+ML {* val nat_diff_split = thm "nat_diff_split" *}
+
+lemmas [arith_split] = nat_diff_split split_min split_max
+
+end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Datatype_Universe.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Universe.ML	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,595 @@
+(*  Title:      HOL/Datatype_Universe.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+*)
+
+(** apfst -- can be used in similar type definitions **)
+
+Goalw [apfst_def] "apfst f (a,b) = (f(a),b)";
+by (rtac split 1);
+qed "apfst_conv";
+
+val [major,minor] = Goal
+    "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R \
+\    |] ==> R";
+by (rtac PairE 1);
+by (rtac minor 1);
+by (assume_tac 1);
+by (rtac (major RS trans) 1);
+by (etac ssubst 1);
+by (rtac apfst_conv 1);
+qed "apfst_convE";
+
+(** Push -- an injection, analogous to Cons on lists **)
+
+Goalw [Push_def] "Push i f = Push j g  ==> i=j";
+by (etac (fun_cong RS box_equals) 1);
+by (rtac nat_case_0 1);
+by (rtac nat_case_0 1);
+qed "Push_inject1";
+
+Goalw [Push_def] "Push i f = Push j g  ==> f=g";
+by (rtac (ext RS box_equals) 1);
+by (etac fun_cong 1);
+by (rtac (nat_case_Suc RS ext) 1);
+by (rtac (nat_case_Suc RS ext) 1);
+qed "Push_inject2";
+
+val [major,minor] = Goal
+    "[| Push i f =Push j g;  [| i=j;  f=g |] ==> P \
+\    |] ==> P";
+by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1);
+qed "Push_inject";
+
+Goalw [Push_def] "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P";
+by (rtac Suc_neq_Zero 1);
+by (etac (fun_cong RS box_equals RS Inr_inject) 1);
+by (rtac nat_case_0 1);
+by (rtac refl 1);
+qed "Push_neq_K0";
+
+(*** Isomorphisms ***)
+
+Goal "inj(Rep_Node)";
+by (rtac inj_inverseI 1);       (*cannot combine by RS: multiple unifiers*)
+by (rtac Rep_Node_inverse 1);
+qed "inj_Rep_Node";
+
+Goal "inj_on Abs_Node Node";
+by (rtac inj_on_inverseI 1);
+by (etac Abs_Node_inverse 1);
+qed "inj_on_Abs_Node";
+
+bind_thm ("Abs_Node_inject", inj_on_Abs_Node RS inj_onD);
+
+
+(*** Introduction rules for Node ***)
+
+Goalw [Node_def] "(%k. Inr 0, a) : Node";
+by (Blast_tac 1);
+qed "Node_K0_I";
+
+Goalw [Node_def,Push_def]
+    "p: Node ==> apfst (Push i) p : Node";
+by (fast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
+qed "Node_Push_I";
+
+
+(*** Distinctness of constructors ***)
+
+(** Scons vs Atom **)
+
+Goalw [Atom_def,Scons_def,Push_Node_def] "Scons M N ~= Atom(a)";
+by (rtac notI 1);
+by (etac (equalityD2 RS subsetD RS UnE) 1);
+by (rtac singletonI 1);
+by (REPEAT (eresolve_tac [imageE, Abs_Node_inject RS apfst_convE, 
+                          Pair_inject, sym RS Push_neq_K0] 1
+     ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1));
+qed "Scons_not_Atom";
+bind_thm ("Atom_not_Scons", Scons_not_Atom RS not_sym);
+
+
+(*** Injectiveness ***)
+
+(** Atomic nodes **)
+
+Goalw [Atom_def] "inj(Atom)";
+by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inject]) 1);
+qed "inj_Atom";
+bind_thm ("Atom_inject", inj_Atom RS injD);
+
+Goal "(Atom(a)=Atom(b)) = (a=b)";
+by (blast_tac (claset() addSDs [Atom_inject]) 1);
+qed "Atom_Atom_eq";
+AddIffs [Atom_Atom_eq];
+
+Goalw [Leaf_def,o_def] "inj(Leaf)";
+by (rtac injI 1);
+by (etac (Atom_inject RS Inl_inject) 1);
+qed "inj_Leaf";
+
+bind_thm ("Leaf_inject", inj_Leaf RS injD);
+AddSDs [Leaf_inject];
+
+Goalw [Numb_def,o_def] "inj(Numb)";
+by (rtac injI 1);
+by (etac (Atom_inject RS Inr_inject) 1);
+qed "inj_Numb";
+
+bind_thm ("Numb_inject", inj_Numb RS injD);
+AddSDs [Numb_inject];
+
+(** Injectiveness of Push_Node **)
+
+val [major,minor] = Goalw [Push_Node_def]
+    "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P \
+\    |] ==> P";
+by (rtac (major RS Abs_Node_inject RS apfst_convE) 1);
+by (REPEAT (resolve_tac [Rep_Node RS Node_Push_I] 1));
+by (etac (sym RS apfst_convE) 1);
+by (rtac minor 1);
+by (etac Pair_inject 1);
+by (etac (Push_inject1 RS sym) 1);
+by (rtac (inj_Rep_Node RS injD) 1);
+by (etac trans 1);
+by (safe_tac (claset() addSEs [Push_inject,sym]));
+qed "Push_Node_inject";
+
+
+(** Injectiveness of Scons **)
+
+Goalw [Scons_def] "Scons M N <= Scons M' N' ==> M<=M'";
+by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
+qed "Scons_inject_lemma1";
+
+Goalw [Scons_def] "Scons M N <= Scons M' N' ==> N<=N'";
+by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
+qed "Scons_inject_lemma2";
+
+Goal "Scons M N = Scons M' N' ==> M=M'";
+by (etac equalityE 1);
+by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
+qed "Scons_inject1";
+
+Goal "Scons M N = Scons M' N' ==> N=N'";
+by (etac equalityE 1);
+by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
+qed "Scons_inject2";
+
+val [major,minor] = Goal
+    "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P \
+\    |] ==> P";
+by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
+qed "Scons_inject";
+
+Goal "(Scons M N = Scons M' N') = (M=M' & N=N')";
+by (blast_tac (claset() addSEs [Scons_inject]) 1);
+qed "Scons_Scons_eq";
+
+(*** Distinctness involving Leaf and Numb ***)
+
+(** Scons vs Leaf **)
+
+Goalw [Leaf_def,o_def] "Scons M N ~= Leaf(a)";
+by (rtac Scons_not_Atom 1);
+qed "Scons_not_Leaf";
+bind_thm ("Leaf_not_Scons", Scons_not_Leaf RS not_sym);
+
+AddIffs [Scons_not_Leaf, Leaf_not_Scons];
+
+
+(** Scons vs Numb **)
+
+Goalw [Numb_def,o_def] "Scons M N ~= Numb(k)";
+by (rtac Scons_not_Atom 1);
+qed "Scons_not_Numb";
+bind_thm ("Numb_not_Scons", Scons_not_Numb RS not_sym);
+
+AddIffs [Scons_not_Numb, Numb_not_Scons];
+
+
+(** Leaf vs Numb **)
+
+Goalw [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)";
+by (simp_tac (simpset() addsimps [Inl_not_Inr]) 1);
+qed "Leaf_not_Numb";
+bind_thm ("Numb_not_Leaf", Leaf_not_Numb RS not_sym);
+
+AddIffs [Leaf_not_Numb, Numb_not_Leaf];
+
+
+(*** ndepth -- the depth of a node ***)
+
+Addsimps [apfst_conv];
+AddIffs  [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
+
+
+Goalw [ndepth_def] "ndepth (Abs_Node(%k. Inr 0, x)) = 0";
+by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
+by (rtac Least_equality 1);
+by (rtac refl 1);
+by (etac less_zeroE 1);
+qed "ndepth_K0";
+
+Goal "k < Suc(LEAST x. f x = Inr 0) --> nat_case (Inr (Suc i)) f k ~= Inr 0";
+by (induct_tac "k" 1);
+by (ALLGOALS Simp_tac);
+by (rtac impI 1);
+by (etac not_less_Least 1);
+val lemma = result();
+
+Goalw [ndepth_def,Push_Node_def]
+    "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))";
+by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1);
+by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
+by Safe_tac;
+by (etac ssubst 1);  (*instantiates type variables!*)
+by (Simp_tac 1);
+by (rtac Least_equality 1);
+by (rewtac Push_def);
+by (rtac (nat_case_Suc RS trans) 1);
+by (etac LeastI 1);
+by (asm_simp_tac (simpset() addsimps [lemma]) 1);
+qed "ndepth_Push_Node";
+
+
+(*** ntrunc applied to the various node sets ***)
+
+Goalw [ntrunc_def] "ntrunc 0 M = {}";
+by (Blast_tac 1);
+qed "ntrunc_0";
+
+Goalw [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)";
+by (fast_tac (claset() addss (simpset() addsimps [ndepth_K0])) 1);
+qed "ntrunc_Atom";
+
+Goalw [Leaf_def,o_def] "ntrunc (Suc k) (Leaf a) = Leaf(a)";
+by (rtac ntrunc_Atom 1);
+qed "ntrunc_Leaf";
+
+Goalw [Numb_def,o_def] "ntrunc (Suc k) (Numb i) = Numb(i)";
+by (rtac ntrunc_Atom 1);
+qed "ntrunc_Numb";
+
+Goalw [Scons_def,ntrunc_def]
+    "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)";
+by (safe_tac (claset() addSIs [imageI]));
+by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
+by (REPEAT (rtac Suc_less_SucD 1 THEN 
+            rtac (ndepth_Push_Node RS subst) 1 THEN 
+            assume_tac 1));
+qed "ntrunc_Scons";
+
+Addsimps [ntrunc_0, ntrunc_Atom, ntrunc_Leaf, ntrunc_Numb, ntrunc_Scons];
+
+
+(** Injection nodes **)
+
+Goalw [In0_def] "ntrunc 1 (In0 M) = {}";
+by (Simp_tac 1);
+by (rewtac Scons_def);
+by (Blast_tac 1);
+qed "ntrunc_one_In0";
+
+Goalw [In0_def]
+    "ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)";
+by (Simp_tac 1);
+qed "ntrunc_In0";
+
+Goalw [In1_def] "ntrunc 1 (In1 M) = {}";
+by (Simp_tac 1);
+by (rewtac Scons_def);
+by (Blast_tac 1);
+qed "ntrunc_one_In1";
+
+Goalw [In1_def]
+    "ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)";
+by (Simp_tac 1);
+qed "ntrunc_In1";
+
+Addsimps [ntrunc_one_In0, ntrunc_In0, ntrunc_one_In1, ntrunc_In1];
+
+
+(*** Cartesian Product ***)
+
+Goalw [uprod_def] "[| M:A;  N:B |] ==> Scons M N : uprod A B";
+by (REPEAT (ares_tac [singletonI,UN_I] 1));
+qed "uprodI";
+
+(*The general elimination rule*)
+val major::prems = Goalw [uprod_def]
+    "[| c : uprod A B;  \
+\       !!x y. [| x:A;  y:B;  c = Scons x y |] ==> P \
+\    |] ==> P";
+by (cut_facts_tac [major] 1);
+by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1
+     ORELSE resolve_tac prems 1));
+qed "uprodE";
+
+(*Elimination of a pair -- introduces no eigenvariables*)
+val prems = Goal
+    "[| Scons M N : uprod A B;      [| M:A;  N:B |] ==> P   \
+\    |] ==> P";
+by (rtac uprodE 1);
+by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Scons_inject,ssubst] 1));
+qed "uprodE2";
+
+
+(*** Disjoint Sum ***)
+
+Goalw [usum_def] "M:A ==> In0(M) : usum A B";
+by (Blast_tac 1);
+qed "usum_In0I";
+
+Goalw [usum_def] "N:B ==> In1(N) : usum A B";
+by (Blast_tac 1);
+qed "usum_In1I";
+
+val major::prems = Goalw [usum_def]
+    "[| u : usum A B;  \
+\       !!x. [| x:A;  u=In0(x) |] ==> P; \
+\       !!y. [| y:B;  u=In1(y) |] ==> P \
+\    |] ==> P";
+by (rtac (major RS UnE) 1);
+by (REPEAT (rtac refl 1 
+     ORELSE eresolve_tac (prems@[imageE,ssubst]) 1));
+qed "usumE";
+
+
+(** Injection **)
+
+Goalw [In0_def,In1_def] "In0(M) ~= In1(N)";
+by (rtac notI 1);
+by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
+qed "In0_not_In1";
+
+bind_thm ("In1_not_In0", In0_not_In1 RS not_sym);
+
+AddIffs [In0_not_In1, In1_not_In0];
+
+Goalw [In0_def] "In0(M) = In0(N) ==>  M=N";
+by (etac (Scons_inject2) 1);
+qed "In0_inject";
+
+Goalw [In1_def] "In1(M) = In1(N) ==>  M=N";
+by (etac (Scons_inject2) 1);
+qed "In1_inject";
+
+Goal "(In0 M = In0 N) = (M=N)";
+by (blast_tac (claset() addSDs [In0_inject]) 1);
+qed "In0_eq";
+
+Goal "(In1 M = In1 N) = (M=N)";
+by (blast_tac (claset() addSDs [In1_inject]) 1);
+qed "In1_eq";
+
+AddIffs [In0_eq, In1_eq];
+
+Goal "inj In0";
+by (blast_tac (claset() addSIs [injI]) 1);
+qed "inj_In0";
+
+Goal "inj In1";
+by (blast_tac (claset() addSIs [injI]) 1);
+qed "inj_In1";
+
+
+(*** Function spaces ***)
+
+Goalw [Lim_def] "Lim f = Lim g ==> f = g";
+by (rtac ext 1);
+by (blast_tac (claset() addSEs [Push_Node_inject]) 1);
+qed "Lim_inject";
+
+Goalw [Funs_def] "S <= T ==> Funs S <= Funs T";
+by (Blast_tac 1);
+qed "Funs_mono";
+
+val [prem] = Goalw [Funs_def] "(!!x. f x : S) ==> f : Funs S";
+by (blast_tac (claset() addIs [prem]) 1);
+qed "FunsI";
+
+Goalw [Funs_def] "f : Funs S ==> f x : S";
+by (etac CollectE 1);
+by (etac subsetD 1);
+by (rtac rangeI 1);
+qed "FunsD";
+
+val [p1, p2] = Goalw [o_def]
+   "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
+by (rtac (p2 RS ext) 1);
+by (rtac (p1 RS FunsD) 1);
+qed "Funs_inv";
+
+val [p1, p2] = Goalw [o_def]
+     "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
+by (res_inst_tac [("h", "%x. @y. (f::'a=>'b) x = g y")] p2 1);
+by (rtac ext 1);
+by (rtac (p1 RS FunsD RS rangeE) 1);
+by (etac (exI RS (some_eq_ex RS iffD2)) 1);
+qed "Funs_rangeE";
+
+Goal "a : S ==> (%x. a) : Funs S";
+by (rtac FunsI 1);
+by (assume_tac 1);
+qed "Funs_nonempty";
+
+
+(*** proving equality of sets and functions using ntrunc ***)
+
+Goalw [ntrunc_def] "ntrunc k M <= M";
+by (Blast_tac 1);
+qed "ntrunc_subsetI";
+
+val [major] = Goalw [ntrunc_def] "(!!k. ntrunc k M <= N) ==> M<=N";
+by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2, 
+			       major RS subsetD]) 1);
+qed "ntrunc_subsetD";
+
+(*A generalized form of the take-lemma*)
+val [major] = Goal "(!!k. ntrunc k M = ntrunc k N) ==> M=N";
+by (rtac equalityI 1);
+by (ALLGOALS (rtac ntrunc_subsetD));
+by (ALLGOALS (rtac (ntrunc_subsetI RSN (2, subset_trans))));
+by (rtac (major RS equalityD1) 1);
+by (rtac (major RS equalityD2) 1);
+qed "ntrunc_equality";
+
+val [major] = Goalw [o_def]
+    "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
+by (rtac (ntrunc_equality RS ext) 1);
+by (rtac (major RS fun_cong) 1);
+qed "ntrunc_o_equality";
+
+(*** Monotonicity ***)
+
+Goalw [uprod_def] "[| A<=A';  B<=B' |] ==> uprod A B <= uprod A' B'";
+by (Blast_tac 1);
+qed "uprod_mono";
+
+Goalw [usum_def] "[| A<=A';  B<=B' |] ==> usum A B <= usum A' B'";
+by (Blast_tac 1);
+qed "usum_mono";
+
+Goalw [Scons_def] "[| M<=M';  N<=N' |] ==> Scons M N <= Scons M' N'";
+by (Blast_tac 1);
+qed "Scons_mono";
+
+Goalw [In0_def] "M<=N ==> In0(M) <= In0(N)";
+by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
+qed "In0_mono";
+
+Goalw [In1_def] "M<=N ==> In1(M) <= In1(N)";
+by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
+qed "In1_mono";
+
+
+(*** Split and Case ***)
+
+Goalw [Split_def] "Split c (Scons M N) = c M N";
+by (Blast_tac  1);
+qed "Split";
+
+Goalw [Case_def] "Case c d (In0 M) = c(M)";
+by (Blast_tac 1);
+qed "Case_In0";
+
+Goalw [Case_def] "Case c d (In1 N) = d(N)";
+by (Blast_tac 1);
+qed "Case_In1";
+
+Addsimps [Split, Case_In0, Case_In1];
+
+
+(**** UN x. B(x) rules ****)
+
+Goalw [ntrunc_def] "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))";
+by (Blast_tac 1);
+qed "ntrunc_UN1";
+
+Goalw [Scons_def] "Scons (UN x. f x) M = (UN x. Scons (f x) M)";
+by (Blast_tac 1);
+qed "Scons_UN1_x";
+
+Goalw [Scons_def] "Scons M (UN x. f x) = (UN x. Scons M (f x))";
+by (Blast_tac 1);
+qed "Scons_UN1_y";
+
+Goalw [In0_def] "In0(UN x. f(x)) = (UN x. In0(f(x)))";
+by (rtac Scons_UN1_y 1);
+qed "In0_UN1";
+
+Goalw [In1_def] "In1(UN x. f(x)) = (UN x. In1(f(x)))";
+by (rtac Scons_UN1_y 1);
+qed "In1_UN1";
+
+
+(*** Equality for Cartesian Product ***)
+
+Goalw [dprod_def]
+    "[| (M,M'):r;  (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s";
+by (Blast_tac 1);
+qed "dprodI";
+
+(*The general elimination rule*)
+val major::prems = Goalw [dprod_def]
+    "[| c : dprod r s;  \
+\       !!x y x' y'. [| (x,x') : r;  (y,y') : s;  c = (Scons x y, Scons x' y') |] ==> P \
+\    |] ==> P";
+by (cut_facts_tac [major] 1);
+by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, mem_splitE, singletonE]));
+by (REPEAT (ares_tac prems 1 ORELSE hyp_subst_tac 1));
+qed "dprodE";
+
+
+(*** Equality for Disjoint Sum ***)
+
+Goalw [dsum_def]  "(M,M'):r ==> (In0(M), In0(M')) : dsum r s";
+by (Blast_tac 1);
+qed "dsum_In0I";
+
+Goalw [dsum_def]  "(N,N'):s ==> (In1(N), In1(N')) : dsum r s";
+by (Blast_tac 1);
+qed "dsum_In1I";
+
+val major::prems = Goalw [dsum_def]
+    "[| w : dsum r s;  \
+\       !!x x'. [| (x,x') : r;  w = (In0(x), In0(x')) |] ==> P; \
+\       !!y y'. [| (y,y') : s;  w = (In1(y), In1(y')) |] ==> P \
+\    |] ==> P";
+by (cut_facts_tac [major] 1);
+by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, UnE, mem_splitE, singletonE]));
+by (DEPTH_SOLVE (ares_tac prems 1 ORELSE hyp_subst_tac 1));
+qed "dsumE";
+
+AddSIs [uprodI, dprodI];
+AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
+AddSEs [uprodE, dprodE, usumE, dsumE];
+
+
+(*** Monotonicity ***)
+
+Goal "[| r<=r';  s<=s' |] ==> dprod r s <= dprod r' s'";
+by (Blast_tac 1);
+qed "dprod_mono";
+
+Goal "[| r<=r';  s<=s' |] ==> dsum r s <= dsum r' s'";
+by (Blast_tac 1);
+qed "dsum_mono";
+
+
+(*** Bounding theorems ***)
+
+Goal "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)";
+by (Blast_tac 1);
+qed "dprod_Sigma";
+
+bind_thm ("dprod_subset_Sigma", [dprod_mono, dprod_Sigma] MRS subset_trans |> standard);
+
+(*Dependent version*)
+Goal "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))";
+by Safe_tac;
+by (stac Split 1);
+by (Blast_tac 1);
+qed "dprod_subset_Sigma2";
+
+Goal "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)";
+by (Blast_tac 1);
+qed "dsum_Sigma";
+
+bind_thm ("dsum_subset_Sigma", [dsum_mono, dsum_Sigma] MRS subset_trans |> standard);
+
+
+(*** Domain ***)
+
+Goal "Domain (dprod r s) = uprod (Domain r) (Domain s)";
+by Auto_tac;
+qed "Domain_dprod";
+
+Goal "Domain (dsum r s) = usum (Domain r) (Domain s)";
+by Auto_tac;
+qed "Domain_dsum";
+
+Addsimps [Domain_dprod, Domain_dsum];
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Datatype_Universe.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Universe.thy	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,102 @@
+(*  Title:      HOL/Datatype_Universe.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Declares the type ('a, 'b) node, a subtype of (nat=>'b+nat) * ('a+nat)
+
+Defines "Cartesian Product" and "Disjoint Sum" as set operations.
+Could <*> be generalized to a general summation (Sigma)?
+*)
+
+Datatype_Universe = Arithmetic + Sum_Type +
+
+
+(** lists, trees will be sets of nodes **)
+
+typedef (Node)
+  ('a, 'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
+
+types
+  'a item = ('a, unit) node set
+  ('a, 'b) dtree = ('a, 'b) node set
+
+consts
+  apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
+  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
+
+  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
+  ndepth    :: ('a, 'b) node => nat
+
+  Atom      :: "('a + nat) => ('a, 'b) dtree"
+  Leaf      :: 'a => ('a, 'b) dtree
+  Numb      :: nat => ('a, 'b) dtree
+  Scons     :: [('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree
+  In0,In1   :: ('a, 'b) dtree => ('a, 'b) dtree
+
+  Lim       :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree
+  Funs      :: "'u set => ('t => 'u) set"
+
+  ntrunc    :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree
+
+  uprod     :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set
+  usum      :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set
+
+  Split     :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
+  Case      :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
+
+  dprod     :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 
+                => (('a, 'b) dtree * ('a, 'b) dtree)set"
+  dsum      :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 
+                => (('a, 'b) dtree * ('a, 'b) dtree)set"
+
+
+defs
+
+  Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
+
+  (*crude "lists" of nats -- needed for the constructions*)
+  apfst_def  "apfst == (%f (x,y). (f(x),y))"
+  Push_def   "Push == (%b h. nat_case b h)"
+
+  (** operations on S-expressions -- sets of nodes **)
+
+  (*S-expression constructors*)
+  Atom_def   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
+  Scons_def  "Scons M N == (Push_Node (Inr 1) `` M) Un (Push_Node (Inr 2) `` N)"
+
+  (*Leaf nodes, with arbitrary or nat labels*)
+  Leaf_def   "Leaf == Atom o Inl"
+  Numb_def   "Numb == Atom o Inr"
+
+  (*Injections of the "disjoint sum"*)
+  In0_def    "In0(M) == Scons (Numb 0) M"
+  In1_def    "In1(M) == Scons (Numb 1) M"
+
+  (*Function spaces*)
+  Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) `` (f x)}"
+  Funs_def "Funs S == {f. range f <= S}"
+
+  (*the set of nodes with depth less than k*)
+  ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
+  ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}"
+
+  (*products and sums for the "universe"*)
+  uprod_def  "uprod A B == UN x:A. UN y:B. { Scons x y }"
+  usum_def   "usum A B == In0``A Un In1``B"
+
+  (*the corresponding eliminators*)
+  Split_def  "Split c M == @u. ? x y. M = Scons x y & u = c x y"
+
+  Case_def   "Case c d M == @u.  (? x . M = In0(x) & u = c(x)) 
+                               | (? y . M = In1(y) & u = d(y))"
+
+
+  (** equality for the "universe" **)
+
+  dprod_def  "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
+
+  dsum_def   "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 
+                          (UN (y,y'):s. {(In1(y),In1(y'))})"
+
+end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Inverse_Image.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Inverse_Image.ML	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,108 @@
+(*  Title:      HOL/Inverse_Image.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Inverse image of a function
+*)
+
+(** Basic rules **)
+
+Goalw [vimage_def] "(a : f-``B) = (f a : B)";
+by (Blast_tac 1) ;
+qed "vimage_eq";
+
+Addsimps [vimage_eq];
+
+Goal "(a : f-``{b}) = (f a = b)";
+by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
+qed "vimage_singleton_eq";
+
+Goalw [vimage_def]
+    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B";
+by (Blast_tac 1) ;
+qed "vimageI";
+
+Goalw [vimage_def] "f a : A ==> a : f -`` A";
+by (Fast_tac 1);
+qed "vimageI2";
+
+val major::prems = Goalw [vimage_def]
+    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
+by (rtac (major RS CollectE) 1);
+by (blast_tac (claset() addIs prems) 1) ;
+qed "vimageE";
+
+Goalw [vimage_def] "a : f -`` A ==> f a : A";
+by (Fast_tac 1);
+qed "vimageD";
+
+AddIs  [vimageI];
+AddSEs [vimageE];
+
+
+(*** Equations ***)
+
+Goal "f-``{} = {}";
+by (Blast_tac 1);
+qed "vimage_empty";
+
+Goal "f-``(-A) = -(f-``A)";
+by (Blast_tac 1);
+qed "vimage_Compl";
+
+Goal "f-``(A Un B) = (f-``A) Un (f-``B)";
+by (Blast_tac 1);
+qed "vimage_Un";
+
+Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)";
+by (Fast_tac 1);
+qed "vimage_Int";
+
+Goal "f -`` (Union A) = (UN X:A. f -`` X)";
+by (Blast_tac 1);
+qed "vimage_Union";
+
+Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
+by (Blast_tac 1);
+qed "vimage_UN";
+
+Goal "f-``(INT x:A. B x) = (INT x:A. f -`` B x)";
+by (Blast_tac 1);
+qed "vimage_INT";
+
+Goal "f -`` Collect P = {y. P (f y)}";
+by (Blast_tac 1);
+qed "vimage_Collect_eq";
+Addsimps [vimage_Collect_eq];
+
+(*A strange result used in Tools/inductive_package*)
+val prems = Goal "(!!x. P (f x) = Q x) ==> f -`` (Collect P) = Collect Q";
+by (force_tac (claset(), simpset() addsimps prems) 1);
+qed "vimage_Collect";
+
+Addsimps [vimage_empty, vimage_Un, vimage_Int];
+
+(*NOT suitable for rewriting because of the recurrence of {a}*)
+Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)";
+by (Blast_tac 1);
+qed "vimage_insert";
+
+Goal "f-``(A-B) = (f-``A) - (f-``B)";
+by (Blast_tac 1);
+qed "vimage_Diff";
+
+Goal "f-``UNIV = UNIV";
+by (Blast_tac 1);
+qed "vimage_UNIV";
+Addsimps [vimage_UNIV];
+
+(*NOT suitable for rewriting*)
+Goal "f-``B = (UN y: B. f-``{y})";
+by (Blast_tac 1);
+qed "vimage_eq_UN";
+
+(*monotonicity*)
+Goal "A<=B ==> f-``A <= f-``B";
+by (Blast_tac 1);
+qed "vimage_mono";
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Inverse_Image.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Inverse_Image.thy	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,15 @@
+(*  Title:      HOL/Inverse_Image.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Inverse image of a function
+*)
+
+Inverse_Image = Set +
+
+constdefs
+  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-``" 90)
+    "f-``B  == {x. f(x) : B}"
+
+end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,602 +0,0 @@
-(*  Title:      HOL/prod
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-Ordered Pairs, the Cartesian product type, the unit type
-*)
-
-(** unit **)
-
-Goalw [Unity_def]
-    "u = ()";
-by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
-by (rtac (Rep_unit_inverse RS sym) 1);
-qed "unit_eq";
-
-(*simplification procedure for unit_eq.
-  Cannot use this rule directly -- it loops!*)
-local
-  val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT));
-  val unit_meta_eq = standard (mk_meta_eq unit_eq);
-  fun proc _ _ t =
-    if HOLogic.is_unit t then None
-    else Some unit_meta_eq;
-in
-  val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc;
-end;
-
-Addsimprocs [unit_eq_proc];
-
-Goal "(!!x::unit. PROP P x) == PROP P ()";
-by (Simp_tac 1);
-qed "unit_all_eq1";
-
-Goal "(!!x::unit. PROP P) == PROP P";
-by (rtac triv_forall_equality 1);
-qed "unit_all_eq2";
-
-Goal "P () ==> P x";
-by (Simp_tac 1);
-qed "unit_induct";
-
-(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u),
-  replacing it by f rather than by %u.f(). *)
-Goal "(%u::unit. f()) = f";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "unit_abs_eta_conv";
-Addsimps [unit_abs_eta_conv];
-
-
-(** prod **)
-
-Goalw [Prod_def] "Pair_Rep a b : Prod";
-by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
-qed "ProdI";
-
-Goalw [Pair_Rep_def] "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
-by (dtac (fun_cong RS fun_cong) 1);
-by (Blast_tac 1);
-qed "Pair_Rep_inject";
-
-Goal "inj_on Abs_Prod Prod";
-by (rtac inj_on_inverseI 1);
-by (etac Abs_Prod_inverse 1);
-qed "inj_on_Abs_Prod";
-
-val prems = Goalw [Pair_def]
-    "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
-by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
-by (REPEAT (ares_tac (prems@[ProdI]) 1));
-qed "Pair_inject";
-
-Goal "((a,b) = (a',b')) = (a=a' & b=b')";
-by (blast_tac (claset() addSEs [Pair_inject]) 1);
-qed "Pair_eq";
-AddIffs [Pair_eq];
-
-Goalw [fst_def] "fst (a,b) = a";
-by (Blast_tac 1);
-qed "fst_conv";
-Goalw [snd_def] "snd (a,b) = b";
-by (Blast_tac 1);
-qed "snd_conv";
-Addsimps [fst_conv, snd_conv];
-
-Goal "fst (x, y) = a ==> x = a";
-by (Asm_full_simp_tac 1);
-qed "fst_eqD";
-Goal "snd (x, y) = a ==> y = a";
-by (Asm_full_simp_tac 1);
-qed "snd_eqD";
-
-Goalw [Pair_def] "? x y. p = (x,y)";
-by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
-by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
-           rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
-qed "PairE_lemma";
-
-val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
-by (rtac (PairE_lemma RS exE) 1);
-by (REPEAT (eresolve_tac [prem,exE] 1));
-qed "PairE";
-
-fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac,
-                         K prune_params_tac];
-
-(* Do not add as rewrite rule: invalidates some proofs in IMP *)
-Goal "p = (fst(p),snd(p))";
-by (pair_tac "p" 1);
-by (Asm_simp_tac 1);
-qed "surjective_pairing";
-Addsimps [surjective_pairing RS sym];
-
-Goal "? x y. z = (x, y)";
-by (rtac exI 1);
-by (rtac exI 1);
-by (rtac surjective_pairing 1);
-qed "surj_pair";
-Addsimps [surj_pair];
-
-
-bind_thm ("split_paired_all",
-  SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
-bind_thms ("split_tupled_all", [split_paired_all, unit_all_eq2]);
-
-(*
-Addsimps [split_paired_all] does not work with simplifier
-because it also affects premises in congrence rules,
-where is can lead to premises of the form !!a b. ... = ?P(a,b)
-which cannot be solved by reflexivity.
-*)
-
-(* replace parameters of product type by individual component parameters *)
-local
-  fun exists_paired_all prem =   (* FIXME check deeper nesting of params!?! *)
-    Library.exists (can HOLogic.dest_prodT o #2) (Logic.strip_params prem);
-  val ss = HOL_basic_ss
-    addsimps [split_paired_all, unit_all_eq2, unit_abs_eta_conv]
-    addsimprocs [unit_eq_proc];
-  val split_tac = full_simp_tac ss;
-in
-  val split_all_tac = SUBGOAL (fn (prem,i) =>
-    if exists_paired_all prem then split_tac i else no_tac);
-end;
-
-claset_ref() := claset()
-  addSWrapper ("split_all_tac", fn tac2 => split_all_tac ORELSE' tac2);
-
-Goal "(!x. P x) = (!a b. P(a,b))";
-by (Fast_tac 1);
-qed "split_paired_All";
-Addsimps [split_paired_All];
-(* AddIffs is not a good idea because it makes Blast_tac loop *)
-
-bind_thm ("prod_induct",
-  allI RS (allI RS (split_paired_All RS iffD2)) RS spec);
-
-Goal "(? x. P x) = (? a b. P(a,b))";
-by (Fast_tac 1);
-qed "split_paired_Ex";
-Addsimps [split_paired_Ex];
-
-Goalw [split_def] "split c (a,b) = c a b";
-by (Simp_tac 1);
-qed "split";
-Addsimps [split];
-
-(*Subsumes the old split_Pair when f is the identity function*)
-Goal "split (%x y. f(x,y)) = f";
-by (rtac ext 1);
-by (pair_tac "x" 1);
-by (Simp_tac 1);
-qed "split_Pair_apply";
-
-(*Can't be added to simpset: loops!*)
-Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
-by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
-qed "split_paired_Eps";
-
-Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
-by (split_all_tac 1);
-by (Asm_simp_tac 1);
-qed "Pair_fst_snd_eq";
-
-Goal "fst p = fst q ==> snd p = snd q ==> p = q";
-by (asm_simp_tac (simpset() addsimps [Pair_fst_snd_eq]) 1);
-qed "prod_eqI";
-AddXIs [prod_eqI];
-
-(*Prevents simplification of c: much faster*)
-Goal "p=q ==> split c p = split c q";
-by (etac arg_cong 1);
-qed "split_weak_cong";
-
-Goal "(%(x,y). f(x,y)) = f";
-by (rtac ext 1);
-by (split_all_tac 1);
-by (rtac split 1);
-qed "split_eta";
-
-val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
-by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1);
-qed "cond_split_eta";
-
-(*simplification procedure for cond_split_eta.
-  using split_eta a rewrite rule is not general enough, and using
-  cond_split_eta directly would render some existing proofs very inefficient.
-  similarly for split_beta. *)
-local
-  fun  Pair_pat k 0 (Bound m) = (m = k)
-  |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
-                        m = k+i andalso Pair_pat k (i-1) t
-  |    Pair_pat _ _ _ = false;
-  fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
-  |   no_args k i (t $ u) = no_args k i t andalso no_args k i u
-  |   no_args k i (Bound m) = m < k orelse m > k+i
-  |   no_args _ _ _ = true;
-  fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then Some (i,t) else None
-  |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
-  |   split_pat tp i _ = None;
-  fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
-        (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
-        (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
-  val sign = sign_of (the_context ());
-  fun simproc name patstr = Simplifier.mk_simproc name
-                [Thm.read_cterm sign (patstr, HOLogic.termT)];
-
-  val beta_patstr = "split f z";
-  val  eta_patstr = "split f";
-  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
-  |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
-                        (beta_term_pat k i t andalso beta_term_pat k i u)
-  |   beta_term_pat k i t = no_args k i t;
-  fun  eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
-  |    eta_term_pat _ _ _ = false;
-  fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
-  |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
-                              else (subst arg k i t $ subst arg k i u)
-  |   subst arg k i t = t;
-  fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
-        (case split_pat beta_term_pat 1 t of
-        Some (i,f) => Some (metaeq sg s (subst arg 0 i f))
-        | None => None)
-  |   beta_proc _ _ _ = None;
-  fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) =
-        (case split_pat eta_term_pat 1 t of
-          Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end))
-        | None => None)
-  |   eta_proc _ _ _ = None;
-in
-  val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
-  val split_eta_proc  = simproc "split_eta"   eta_patstr  eta_proc;
-end;
-
-Addsimprocs [split_beta_proc,split_eta_proc];
-
-Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
-by (stac surjective_pairing 1 THEN rtac split 1);
-qed "split_beta";
-
-(*For use with split_tac and the simplifier*)
-Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
-by (stac surjective_pairing 1);
-by (stac split 1);
-by (Blast_tac 1);
-qed "split_split";
-
-(* could be done after split_tac has been speeded up significantly:
-simpset_ref() := simpset() addsplits [split_split];
-   precompute the constants involved and don't do anything unless
-   the current goal contains one of those constants
-*)
-
-Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
-by (stac split_split 1);
-by (Simp_tac 1);
-qed "expand_split_asm";
-
-(** split used as a logical connective or set former **)
-
-(*These rules are for use with blast_tac.
-  Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
-
-Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
-by (split_all_tac 1);
-by (Asm_simp_tac 1);
-qed "splitI2";
-
-Goal "!!p. [| !!a b. (a,b)=p ==> c a b x |] ==> split c p x";
-by (split_all_tac 1);
-by (Asm_simp_tac 1);
-qed "splitI2'";
-
-Goal "c a b ==> split c (a,b)";
-by (Asm_simp_tac 1);
-qed "splitI";
-
-val prems = Goalw [split_def]
-    "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
-by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
-qed "splitE";
-
-val prems = Goalw [split_def]
-    "[| split c p z;  !!x y. [| p = (x,y);  c x y z |] ==> Q |] ==> Q";
-by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
-qed "splitE'";
-
-val major::prems = Goal
-    "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R  \
-\    |] ==> R";
-by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
-by (rtac (split_beta RS subst) 1 THEN rtac major 1);
-qed "splitE2";
-
-Goal "split R (a,b) ==> R a b";
-by (etac (split RS iffD1) 1);
-qed "splitD";
-
-Goal "z: c a b ==> z: split c (a,b)";
-by (Asm_simp_tac 1);
-qed "mem_splitI";
-
-Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
-by (split_all_tac 1);
-by (Asm_simp_tac 1);
-qed "mem_splitI2";
-
-val prems = Goalw [split_def]
-    "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
-by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
-qed "mem_splitE";
-
-AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2];
-AddSEs [splitE, splitE', mem_splitE];
-
-Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P";
-by (rtac ext 1);
-by (Fast_tac 1);
-qed "split_eta_SetCompr";
-Addsimps [split_eta_SetCompr];
-
-Goal "(%u. ? x y. u = (x, y) & P x y) = split P";
-br ext 1;
-by (Fast_tac 1);
-qed "split_eta_SetCompr2";
-Addsimps [split_eta_SetCompr2];
-
-(* allows simplifications of nested splits in case of independent predicates *)
-Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";
-by (rtac ext 1);
-by (Blast_tac 1);
-qed "split_part";
-Addsimps [split_part];
-
-Goal "(@(x',y'). x = x' & y = y') = (x,y)";
-by (Blast_tac 1);
-qed "Eps_split_eq";
-Addsimps [Eps_split_eq];
-(*
-the following  would be slightly more general,
-but cannot be used as rewrite rule:
-### Cannot add premise as rewrite rule because it contains (type) unknowns:
-### ?y = .x
-Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
-by (rtac some_equality 1);
-by ( Simp_tac 1);
-by (split_all_tac 1);
-by (Asm_full_simp_tac 1);
-qed "Eps_split_eq";
-*)
-
-(*** prod_fun -- action of the product functor upon functions ***)
-
-Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
-by (rtac split 1);
-qed "prod_fun";
-Addsimps [prod_fun];
-
-Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
-by (rtac ext 1);
-by (pair_tac "x" 1);
-by (Asm_simp_tac 1);
-qed "prod_fun_compose";
-
-Goal "prod_fun (%x. x) (%y. y) = (%z. z)";
-by (rtac ext 1);
-by (pair_tac "z" 1);
-by (Asm_simp_tac 1);
-qed "prod_fun_ident";
-Addsimps [prod_fun_ident];
-
-Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
-by (rtac image_eqI 1);
-by (rtac (prod_fun RS sym) 1);
-by (assume_tac 1);
-qed "prod_fun_imageI";
-
-val major::prems = Goal
-    "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
-\    |] ==> P";
-by (rtac (major RS imageE) 1);
-by (res_inst_tac [("p","x")] PairE 1);
-by (resolve_tac prems 1);
-by (Blast_tac 2);
-by (blast_tac (claset() addIs [prod_fun]) 1);
-qed "prod_fun_imageE";
-
-AddIs  [prod_fun_imageI];
-AddSEs [prod_fun_imageE];
-
-
-(*** Disjoint union of a family of sets - Sigma ***)
-
-Goalw [Sigma_def] "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B";
-by (REPEAT (ares_tac [singletonI,UN_I] 1));
-qed "SigmaI";
-
-AddSIs [SigmaI];
-
-(*The general elimination rule*)
-val major::prems = Goalw [Sigma_def]
-    "[| c: Sigma A B;  \
-\       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
-\    |] ==> P";
-by (cut_facts_tac [major] 1);
-by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
-qed "SigmaE";
-
-(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
-
-Goal "(a,b) : Sigma A B ==> a : A";
-by (etac SigmaE 1);
-by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
-qed "SigmaD1";
-
-Goal "(a,b) : Sigma A B ==> b : B(a)";
-by (etac SigmaE 1);
-by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
-qed "SigmaD2";
-
-val [major,minor]= Goal
-    "[| (a,b) : Sigma A B;    \
-\       [| a:A;  b:B(a) |] ==> P   \
-\    |] ==> P";
-by (rtac minor 1);
-by (rtac (major RS SigmaD1) 1);
-by (rtac (major RS SigmaD2) 1) ;
-qed "SigmaE2";
-
-AddSEs [SigmaE2, SigmaE];
-
-val prems = Goal
-    "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
-by (cut_facts_tac prems 1);
-by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
-qed "Sigma_mono";
-
-Goal "Sigma {} B = {}";
-by (Blast_tac 1) ;
-qed "Sigma_empty1";
-
-Goal "A <*> {} = {}";
-by (Blast_tac 1) ;
-qed "Sigma_empty2";
-
-Addsimps [Sigma_empty1,Sigma_empty2];
-
-Goal "UNIV <*> UNIV = UNIV";
-by Auto_tac;
-qed "UNIV_Times_UNIV";
-Addsimps [UNIV_Times_UNIV];
-
-Goal "- (UNIV <*> A) = UNIV <*> (-A)";
-by Auto_tac;
-qed "Compl_Times_UNIV1";
-
-Goal "- (A <*> UNIV) = (-A) <*> UNIV";
-by Auto_tac;
-qed "Compl_Times_UNIV2";
-
-Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2];
-
-Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
-by (Blast_tac 1);
-qed "mem_Sigma_iff";
-AddIffs [mem_Sigma_iff];
-
-Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)";
-by (Blast_tac 1);
-qed "Times_subset_cancel2";
-
-Goal "x:C ==> (A <*> C = B <*> C) = (A = B)";
-by (blast_tac (claset() addEs [equalityE]) 1);
-qed "Times_eq_cancel2";
-
-Goal "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))";
-by (Fast_tac 1);
-qed "SetCompr_Sigma_eq";
-
-(*** Complex rules for Sigma ***)
-
-Goal "{(a,b). P a & Q b} = Collect P <*> Collect Q";
-by (Blast_tac 1);
-qed "Collect_split";
-
-Addsimps [Collect_split];
-
-(*Suggested by Pierre Chartier*)
-Goal "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)";
-by (Blast_tac 1);
-qed "UN_Times_distrib";
-
-Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))";
-by (Fast_tac 1);
-qed "split_paired_Ball_Sigma";
-Addsimps [split_paired_Ball_Sigma];
-
-Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))";
-by (Fast_tac 1);
-qed "split_paired_Bex_Sigma";
-Addsimps [split_paired_Bex_Sigma];
-
-Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))";
-by (Blast_tac 1);
-qed "Sigma_Un_distrib1";
-
-Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))";
-by (Blast_tac 1);
-qed "Sigma_Un_distrib2";
-
-Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))";
-by (Blast_tac 1);
-qed "Sigma_Int_distrib1";
-
-Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))";
-by (Blast_tac 1);
-qed "Sigma_Int_distrib2";
-
-Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))";
-by (Blast_tac 1);
-qed "Sigma_Diff_distrib1";
-
-Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))";
-by (Blast_tac 1);
-qed "Sigma_Diff_distrib2";
-
-Goal "Sigma (Union X) B = (UN A:X. Sigma A B)";
-by (Blast_tac 1);
-qed "Sigma_Union";
-
-(*Non-dependent versions are needed to avoid the need for higher-order
-  matching, especially when the rules are re-oriented*)
-Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)";
-by (Blast_tac 1);
-qed "Times_Un_distrib1";
-
-Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)";
-by (Blast_tac 1);
-qed "Times_Int_distrib1";
-
-Goal "(A - B) <*> C = (A <*> C) - (B <*> C)";
-by (Blast_tac 1);
-qed "Times_Diff_distrib1";
-
-
-(*Attempts to remove occurrences of split, and pair-valued parameters*)
-val remove_split = rewrite_rule [split RS eq_reflection] o
-                   rule_by_tactic (TRYALL split_all_tac);
-
-local
-
-(*In ap_split S T u, term u expects separate arguments for the factors of S,
-  with result type T.  The call creates a new term expecting one argument
-  of type S.*)
-fun ap_split (Type ("*", [T1, T2])) T3 u =
-      HOLogic.split_const (T1, T2, T3) $
-      Abs("v", T1,
-          ap_split T2 T3
-             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
-              Bound 0))
-  | ap_split T T3 u = u;
-
-(*Curries any Var of function type in the rule*)
-fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
-      let val T' = HOLogic.prodT_factors T1 ---> T2
-          val newt = ap_split T1 T2 (Var (v, T'))
-          val cterm = Thm.cterm_of (#sign (rep_thm rl))
-      in
-          instantiate ([], [(cterm t, cterm newt)]) rl
-      end
-  | split_rule_var' (t, rl) = rl;
-
-in
-
-val split_rule_var = standard o remove_split o split_rule_var';
-
-(*Curries ALL function variables occurring in a rule's conclusion*)
-fun split_rule rl = remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl))
-                    |> standard;
-
-end;
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(*  Title:      HOL/Prod.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Ordered Pairs and the Cartesian product type.
-The unit type.
-*)
-
-Prod = Fun + equalities +
-
-
-(** products **)
-
-(* type definition *)
-
-constdefs
-  Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
-  "Pair_Rep == (%a b. %x y. x=a & y=b)"
-
-global
-
-typedef (Prod)
-  ('a, 'b) "*"          (infixr 20)
-    = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
-
-syntax (symbols)
-  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
-
-syntax (HTML output)
-  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
-
-
-(* abstract constants and syntax *)
-
-consts
-  fst           :: "'a * 'b => 'a"
-  snd           :: "'a * 'b => 'b"
-  split         :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
-  prod_fun      :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
-  Pair          :: "['a, 'b] => 'a * 'b"
-  Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
-
-
-(* patterns -- extends pre-defined type "pttrn" used in abstractions *)
-
-nonterminals
-  tuple_args patterns
-
-syntax
-  "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")
-  "_tuple_arg"  :: "'a => tuple_args"                   ("_")
-  "_tuple_args" :: "'a => tuple_args => tuple_args"     ("_,/ _")
-  "_pattern"    :: [pttrn, patterns] => pttrn           ("'(_,/ _')")
-  ""            :: pttrn => patterns                    ("_")
-  "_patterns"   :: [pttrn, patterns] => patterns        ("_,/ _")
-  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
-  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    (infixr "<*>" 80)
-
-translations
-  "(x, y)"       == "Pair x y"
-  "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
-  "%(x,y,zs).b"  == "split(%x (y,zs).b)"
-  "%(x,y).b"     == "split(%x y. b)"
-  "_abs (Pair x y) t" => "%(x,y).t"
-  (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
-     The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
-
-  "SIGMA x:A. B" => "Sigma A (%x. B)"
-  "A <*> B"      => "Sigma A (_K B)"
-
-syntax (symbols)
-  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
-  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ \\<times> _" [81, 80] 80)
-
-
-(* definitions *)
-
-local
-
-defs
-  Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
-  fst_def       "fst p == @a. ? b. p = (a, b)"
-  snd_def       "snd p == @b. ? a. p = (a, b)"
-  split_def     "split == (%c p. c (fst p) (snd p))"
-  prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
-  Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
-
-
-
-(** unit **)
-
-global
-
-typedef  unit = "{True}"
-
-consts
-  "()"          :: unit                           ("'(')")
-
-local
-
-defs
-  Unity_def     "() == Abs_unit True"
-
-end
-
-ML
-
-val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))];
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Product_Type.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Product_Type.ML	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,602 @@
+(*  Title:      HOL/Product_Type.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+
+Ordered Pairs, the Cartesian product type, the unit type
+*)
+
+(** unit **)
+
+Goalw [Unity_def]
+    "u = ()";
+by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
+by (rtac (Rep_unit_inverse RS sym) 1);
+qed "unit_eq";
+
+(*simplification procedure for unit_eq.
+  Cannot use this rule directly -- it loops!*)
+local
+  val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT));
+  val unit_meta_eq = standard (mk_meta_eq unit_eq);
+  fun proc _ _ t =
+    if HOLogic.is_unit t then None
+    else Some unit_meta_eq;
+in
+  val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc;
+end;
+
+Addsimprocs [unit_eq_proc];
+
+Goal "(!!x::unit. PROP P x) == PROP P ()";
+by (Simp_tac 1);
+qed "unit_all_eq1";
+
+Goal "(!!x::unit. PROP P) == PROP P";
+by (rtac triv_forall_equality 1);
+qed "unit_all_eq2";
+
+Goal "P () ==> P x";
+by (Simp_tac 1);
+qed "unit_induct";
+
+(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u),
+  replacing it by f rather than by %u.f(). *)
+Goal "(%u::unit. f()) = f";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "unit_abs_eta_conv";
+Addsimps [unit_abs_eta_conv];
+
+
+(** prod **)
+
+Goalw [Prod_def] "Pair_Rep a b : Prod";
+by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
+qed "ProdI";
+
+Goalw [Pair_Rep_def] "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
+by (dtac (fun_cong RS fun_cong) 1);
+by (Blast_tac 1);
+qed "Pair_Rep_inject";
+
+Goal "inj_on Abs_Prod Prod";
+by (rtac inj_on_inverseI 1);
+by (etac Abs_Prod_inverse 1);
+qed "inj_on_Abs_Prod";
+
+val prems = Goalw [Pair_def]
+    "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
+by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
+by (REPEAT (ares_tac (prems@[ProdI]) 1));
+qed "Pair_inject";
+
+Goal "((a,b) = (a',b')) = (a=a' & b=b')";
+by (blast_tac (claset() addSEs [Pair_inject]) 1);
+qed "Pair_eq";
+AddIffs [Pair_eq];
+
+Goalw [fst_def] "fst (a,b) = a";
+by (Blast_tac 1);
+qed "fst_conv";
+Goalw [snd_def] "snd (a,b) = b";
+by (Blast_tac 1);
+qed "snd_conv";
+Addsimps [fst_conv, snd_conv];
+
+Goal "fst (x, y) = a ==> x = a";
+by (Asm_full_simp_tac 1);
+qed "fst_eqD";
+Goal "snd (x, y) = a ==> y = a";
+by (Asm_full_simp_tac 1);
+qed "snd_eqD";
+
+Goalw [Pair_def] "? x y. p = (x,y)";
+by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
+by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
+           rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
+qed "PairE_lemma";
+
+val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
+by (rtac (PairE_lemma RS exE) 1);
+by (REPEAT (eresolve_tac [prem,exE] 1));
+qed "PairE";
+
+fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac,
+                         K prune_params_tac];
+
+(* Do not add as rewrite rule: invalidates some proofs in IMP *)
+Goal "p = (fst(p),snd(p))";
+by (pair_tac "p" 1);
+by (Asm_simp_tac 1);
+qed "surjective_pairing";
+Addsimps [surjective_pairing RS sym];
+
+Goal "? x y. z = (x, y)";
+by (rtac exI 1);
+by (rtac exI 1);
+by (rtac surjective_pairing 1);
+qed "surj_pair";
+Addsimps [surj_pair];
+
+
+bind_thm ("split_paired_all",
+  SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
+bind_thms ("split_tupled_all", [split_paired_all, unit_all_eq2]);
+
+(*
+Addsimps [split_paired_all] does not work with simplifier
+because it also affects premises in congrence rules,
+where is can lead to premises of the form !!a b. ... = ?P(a,b)
+which cannot be solved by reflexivity.
+*)
+
+(* replace parameters of product type by individual component parameters *)
+local
+  fun exists_paired_all prem =   (* FIXME check deeper nesting of params!?! *)
+    Library.exists (can HOLogic.dest_prodT o #2) (Logic.strip_params prem);
+  val ss = HOL_basic_ss
+    addsimps [split_paired_all, unit_all_eq2, unit_abs_eta_conv]
+    addsimprocs [unit_eq_proc];
+  val split_tac = full_simp_tac ss;
+in
+  val split_all_tac = SUBGOAL (fn (prem,i) =>
+    if exists_paired_all prem then split_tac i else no_tac);
+end;
+
+claset_ref() := claset()
+  addSWrapper ("split_all_tac", fn tac2 => split_all_tac ORELSE' tac2);
+
+Goal "(!x. P x) = (!a b. P(a,b))";
+by (Fast_tac 1);
+qed "split_paired_All";
+Addsimps [split_paired_All];
+(* AddIffs is not a good idea because it makes Blast_tac loop *)
+
+bind_thm ("prod_induct",
+  allI RS (allI RS (split_paired_All RS iffD2)) RS spec);
+
+Goal "(? x. P x) = (? a b. P(a,b))";
+by (Fast_tac 1);
+qed "split_paired_Ex";
+Addsimps [split_paired_Ex];
+
+Goalw [split_def] "split c (a,b) = c a b";
+by (Simp_tac 1);
+qed "split";
+Addsimps [split];
+
+(*Subsumes the old split_Pair when f is the identity function*)
+Goal "split (%x y. f(x,y)) = f";
+by (rtac ext 1);
+by (pair_tac "x" 1);
+by (Simp_tac 1);
+qed "split_Pair_apply";
+
+(*Can't be added to simpset: loops!*)
+Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
+by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
+qed "split_paired_Eps";
+
+Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
+by (split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "Pair_fst_snd_eq";
+
+Goal "fst p = fst q ==> snd p = snd q ==> p = q";
+by (asm_simp_tac (simpset() addsimps [Pair_fst_snd_eq]) 1);
+qed "prod_eqI";
+AddXIs [prod_eqI];
+
+(*Prevents simplification of c: much faster*)
+Goal "p=q ==> split c p = split c q";
+by (etac arg_cong 1);
+qed "split_weak_cong";
+
+Goal "(%(x,y). f(x,y)) = f";
+by (rtac ext 1);
+by (split_all_tac 1);
+by (rtac split 1);
+qed "split_eta";
+
+val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
+by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1);
+qed "cond_split_eta";
+
+(*simplification procedure for cond_split_eta.
+  using split_eta a rewrite rule is not general enough, and using
+  cond_split_eta directly would render some existing proofs very inefficient.
+  similarly for split_beta. *)
+local
+  fun  Pair_pat k 0 (Bound m) = (m = k)
+  |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
+                        m = k+i andalso Pair_pat k (i-1) t
+  |    Pair_pat _ _ _ = false;
+  fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
+  |   no_args k i (t $ u) = no_args k i t andalso no_args k i u
+  |   no_args k i (Bound m) = m < k orelse m > k+i
+  |   no_args _ _ _ = true;
+  fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then Some (i,t) else None
+  |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
+  |   split_pat tp i _ = None;
+  fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
+        (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
+        (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
+  val sign = sign_of (the_context ());
+  fun simproc name patstr = Simplifier.mk_simproc name
+                [Thm.read_cterm sign (patstr, HOLogic.termT)];
+
+  val beta_patstr = "split f z";
+  val  eta_patstr = "split f";
+  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
+  |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
+                        (beta_term_pat k i t andalso beta_term_pat k i u)
+  |   beta_term_pat k i t = no_args k i t;
+  fun  eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
+  |    eta_term_pat _ _ _ = false;
+  fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
+  |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
+                              else (subst arg k i t $ subst arg k i u)
+  |   subst arg k i t = t;
+  fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
+        (case split_pat beta_term_pat 1 t of
+        Some (i,f) => Some (metaeq sg s (subst arg 0 i f))
+        | None => None)
+  |   beta_proc _ _ _ = None;
+  fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) =
+        (case split_pat eta_term_pat 1 t of
+          Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end))
+        | None => None)
+  |   eta_proc _ _ _ = None;
+in
+  val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
+  val split_eta_proc  = simproc "split_eta"   eta_patstr  eta_proc;
+end;
+
+Addsimprocs [split_beta_proc,split_eta_proc];
+
+Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
+by (stac surjective_pairing 1 THEN rtac split 1);
+qed "split_beta";
+
+(*For use with split_tac and the simplifier*)
+Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
+by (stac surjective_pairing 1);
+by (stac split 1);
+by (Blast_tac 1);
+qed "split_split";
+
+(* could be done after split_tac has been speeded up significantly:
+simpset_ref() := simpset() addsplits [split_split];
+   precompute the constants involved and don't do anything unless
+   the current goal contains one of those constants
+*)
+
+Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
+by (stac split_split 1);
+by (Simp_tac 1);
+qed "expand_split_asm";
+
+(** split used as a logical connective or set former **)
+
+(*These rules are for use with blast_tac.
+  Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
+
+Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
+by (split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "splitI2";
+
+Goal "!!p. [| !!a b. (a,b)=p ==> c a b x |] ==> split c p x";
+by (split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "splitI2'";
+
+Goal "c a b ==> split c (a,b)";
+by (Asm_simp_tac 1);
+qed "splitI";
+
+val prems = Goalw [split_def]
+    "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+qed "splitE";
+
+val prems = Goalw [split_def]
+    "[| split c p z;  !!x y. [| p = (x,y);  c x y z |] ==> Q |] ==> Q";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+qed "splitE'";
+
+val major::prems = Goal
+    "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R  \
+\    |] ==> R";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+by (rtac (split_beta RS subst) 1 THEN rtac major 1);
+qed "splitE2";
+
+Goal "split R (a,b) ==> R a b";
+by (etac (split RS iffD1) 1);
+qed "splitD";
+
+Goal "z: c a b ==> z: split c (a,b)";
+by (Asm_simp_tac 1);
+qed "mem_splitI";
+
+Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
+by (split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "mem_splitI2";
+
+val prems = Goalw [split_def]
+    "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+qed "mem_splitE";
+
+AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2];
+AddSEs [splitE, splitE', mem_splitE];
+
+Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P";
+by (rtac ext 1);
+by (Fast_tac 1);
+qed "split_eta_SetCompr";
+Addsimps [split_eta_SetCompr];
+
+Goal "(%u. ? x y. u = (x, y) & P x y) = split P";
+br ext 1;
+by (Fast_tac 1);
+qed "split_eta_SetCompr2";
+Addsimps [split_eta_SetCompr2];
+
+(* allows simplifications of nested splits in case of independent predicates *)
+Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";
+by (rtac ext 1);
+by (Blast_tac 1);
+qed "split_part";
+Addsimps [split_part];
+
+Goal "(@(x',y'). x = x' & y = y') = (x,y)";
+by (Blast_tac 1);
+qed "Eps_split_eq";
+Addsimps [Eps_split_eq];
+(*
+the following  would be slightly more general,
+but cannot be used as rewrite rule:
+### Cannot add premise as rewrite rule because it contains (type) unknowns:
+### ?y = .x
+Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
+by (rtac some_equality 1);
+by ( Simp_tac 1);
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
+qed "Eps_split_eq";
+*)
+
+(*** prod_fun -- action of the product functor upon functions ***)
+
+Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
+by (rtac split 1);
+qed "prod_fun";
+Addsimps [prod_fun];
+
+Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
+by (rtac ext 1);
+by (pair_tac "x" 1);
+by (Asm_simp_tac 1);
+qed "prod_fun_compose";
+
+Goal "prod_fun (%x. x) (%y. y) = (%z. z)";
+by (rtac ext 1);
+by (pair_tac "z" 1);
+by (Asm_simp_tac 1);
+qed "prod_fun_ident";
+Addsimps [prod_fun_ident];
+
+Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
+by (rtac image_eqI 1);
+by (rtac (prod_fun RS sym) 1);
+by (assume_tac 1);
+qed "prod_fun_imageI";
+
+val major::prems = Goal
+    "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
+\    |] ==> P";
+by (rtac (major RS imageE) 1);
+by (res_inst_tac [("p","x")] PairE 1);
+by (resolve_tac prems 1);
+by (Blast_tac 2);
+by (blast_tac (claset() addIs [prod_fun]) 1);
+qed "prod_fun_imageE";
+
+AddIs  [prod_fun_imageI];
+AddSEs [prod_fun_imageE];
+
+
+(*** Disjoint union of a family of sets - Sigma ***)
+
+Goalw [Sigma_def] "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B";
+by (REPEAT (ares_tac [singletonI,UN_I] 1));
+qed "SigmaI";
+
+AddSIs [SigmaI];
+
+(*The general elimination rule*)
+val major::prems = Goalw [Sigma_def]
+    "[| c: Sigma A B;  \
+\       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
+\    |] ==> P";
+by (cut_facts_tac [major] 1);
+by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
+qed "SigmaE";
+
+(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
+
+Goal "(a,b) : Sigma A B ==> a : A";
+by (etac SigmaE 1);
+by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
+qed "SigmaD1";
+
+Goal "(a,b) : Sigma A B ==> b : B(a)";
+by (etac SigmaE 1);
+by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
+qed "SigmaD2";
+
+val [major,minor]= Goal
+    "[| (a,b) : Sigma A B;    \
+\       [| a:A;  b:B(a) |] ==> P   \
+\    |] ==> P";
+by (rtac minor 1);
+by (rtac (major RS SigmaD1) 1);
+by (rtac (major RS SigmaD2) 1) ;
+qed "SigmaE2";
+
+AddSEs [SigmaE2, SigmaE];
+
+val prems = Goal
+    "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
+by (cut_facts_tac prems 1);
+by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
+qed "Sigma_mono";
+
+Goal "Sigma {} B = {}";
+by (Blast_tac 1) ;
+qed "Sigma_empty1";
+
+Goal "A <*> {} = {}";
+by (Blast_tac 1) ;
+qed "Sigma_empty2";
+
+Addsimps [Sigma_empty1,Sigma_empty2];
+
+Goal "UNIV <*> UNIV = UNIV";
+by Auto_tac;
+qed "UNIV_Times_UNIV";
+Addsimps [UNIV_Times_UNIV];
+
+Goal "- (UNIV <*> A) = UNIV <*> (-A)";
+by Auto_tac;
+qed "Compl_Times_UNIV1";
+
+Goal "- (A <*> UNIV) = (-A) <*> UNIV";
+by Auto_tac;
+qed "Compl_Times_UNIV2";
+
+Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2];
+
+Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
+by (Blast_tac 1);
+qed "mem_Sigma_iff";
+AddIffs [mem_Sigma_iff];
+
+Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)";
+by (Blast_tac 1);
+qed "Times_subset_cancel2";
+
+Goal "x:C ==> (A <*> C = B <*> C) = (A = B)";
+by (blast_tac (claset() addEs [equalityE]) 1);
+qed "Times_eq_cancel2";
+
+Goal "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))";
+by (Fast_tac 1);
+qed "SetCompr_Sigma_eq";
+
+(*** Complex rules for Sigma ***)
+
+Goal "{(a,b). P a & Q b} = Collect P <*> Collect Q";
+by (Blast_tac 1);
+qed "Collect_split";
+
+Addsimps [Collect_split];
+
+(*Suggested by Pierre Chartier*)
+Goal "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)";
+by (Blast_tac 1);
+qed "UN_Times_distrib";
+
+Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))";
+by (Fast_tac 1);
+qed "split_paired_Ball_Sigma";
+Addsimps [split_paired_Ball_Sigma];
+
+Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))";
+by (Fast_tac 1);
+qed "split_paired_Bex_Sigma";
+Addsimps [split_paired_Bex_Sigma];
+
+Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))";
+by (Blast_tac 1);
+qed "Sigma_Un_distrib1";
+
+Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))";
+by (Blast_tac 1);
+qed "Sigma_Un_distrib2";
+
+Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))";
+by (Blast_tac 1);
+qed "Sigma_Int_distrib1";
+
+Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))";
+by (Blast_tac 1);
+qed "Sigma_Int_distrib2";
+
+Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))";
+by (Blast_tac 1);
+qed "Sigma_Diff_distrib1";
+
+Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))";
+by (Blast_tac 1);
+qed "Sigma_Diff_distrib2";
+
+Goal "Sigma (Union X) B = (UN A:X. Sigma A B)";
+by (Blast_tac 1);
+qed "Sigma_Union";
+
+(*Non-dependent versions are needed to avoid the need for higher-order
+  matching, especially when the rules are re-oriented*)
+Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)";
+by (Blast_tac 1);
+qed "Times_Un_distrib1";
+
+Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)";
+by (Blast_tac 1);
+qed "Times_Int_distrib1";
+
+Goal "(A - B) <*> C = (A <*> C) - (B <*> C)";
+by (Blast_tac 1);
+qed "Times_Diff_distrib1";
+
+
+(*Attempts to remove occurrences of split, and pair-valued parameters*)
+val remove_split = rewrite_rule [split RS eq_reflection] o
+                   rule_by_tactic (TRYALL split_all_tac);
+
+local
+
+(*In ap_split S T u, term u expects separate arguments for the factors of S,
+  with result type T.  The call creates a new term expecting one argument
+  of type S.*)
+fun ap_split (Type ("*", [T1, T2])) T3 u =
+      HOLogic.split_const (T1, T2, T3) $
+      Abs("v", T1,
+          ap_split T2 T3
+             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
+              Bound 0))
+  | ap_split T T3 u = u;
+
+(*Curries any Var of function type in the rule*)
+fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
+      let val T' = HOLogic.prodT_factors T1 ---> T2
+          val newt = ap_split T1 T2 (Var (v, T'))
+          val cterm = Thm.cterm_of (#sign (rep_thm rl))
+      in
+          instantiate ([], [(cterm t, cterm newt)]) rl
+      end
+  | split_rule_var' (t, rl) = rl;
+
+in
+
+val split_rule_var = standard o remove_split o split_rule_var';
+
+(*Curries ALL function variables occurring in a rule's conclusion*)
+fun split_rule rl = remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl))
+                    |> standard;
+
+end;
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Product_Type.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Product_Type.thy	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,109 @@
+(*  Title:      HOL/Product_Type.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Ordered Pairs and the Cartesian product type.
+The unit type.
+*)
+
+Product_Type = Fun + equalities +
+
+
+(** products **)
+
+(* type definition *)
+
+constdefs
+  Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
+  "Pair_Rep == (%a b. %x y. x=a & y=b)"
+
+global
+
+typedef (Prod)
+  ('a, 'b) "*"          (infixr 20)
+    = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
+
+syntax (symbols)
+  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
+
+syntax (HTML output)
+  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
+
+
+(* abstract constants and syntax *)
+
+consts
+  fst           :: "'a * 'b => 'a"
+  snd           :: "'a * 'b => 'b"
+  split         :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
+  prod_fun      :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
+  Pair          :: "['a, 'b] => 'a * 'b"
+  Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
+
+
+(* patterns -- extends pre-defined type "pttrn" used in abstractions *)
+
+nonterminals
+  tuple_args patterns
+
+syntax
+  "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")
+  "_tuple_arg"  :: "'a => tuple_args"                   ("_")
+  "_tuple_args" :: "'a => tuple_args => tuple_args"     ("_,/ _")
+  "_pattern"    :: [pttrn, patterns] => pttrn           ("'(_,/ _')")
+  ""            :: pttrn => patterns                    ("_")
+  "_patterns"   :: [pttrn, patterns] => patterns        ("_,/ _")
+  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
+  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    (infixr "<*>" 80)
+
+translations
+  "(x, y)"       == "Pair x y"
+  "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
+  "%(x,y,zs).b"  == "split(%x (y,zs).b)"
+  "%(x,y).b"     == "split(%x y. b)"
+  "_abs (Pair x y) t" => "%(x,y).t"
+  (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
+     The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
+
+  "SIGMA x:A. B" => "Sigma A (%x. B)"
+  "A <*> B"      => "Sigma A (_K B)"
+
+syntax (symbols)
+  "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
+  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ \\<times> _" [81, 80] 80)
+
+
+(* definitions *)
+
+local
+
+defs
+  Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
+  fst_def       "fst p == @a. ? b. p = (a, b)"
+  snd_def       "snd p == @b. ? a. p = (a, b)"
+  split_def     "split == (%c p. c (fst p) (snd p))"
+  prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
+  Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
+
+
+
+(** unit **)
+
+global
+
+typedef  unit = "{True}"
+
+consts
+  "()"          :: unit                           ("'(')")
+
+local
+
+defs
+  Unity_def     "() == Abs_unit True"
+
+end
+
+ML
+
+val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))];
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-(*  Title:      HOL/RelPow.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1996  TU Muenchen
-*)
-
-open RelPow;
-
-Goal "!!R:: ('a*'a)set. R^1 = R";
-by (Simp_tac 1);
-qed "rel_pow_1";
-Addsimps [rel_pow_1];
-
-Goal "(x,x) : R^0";
-by (Simp_tac 1);
-qed "rel_pow_0_I";
-
-Goal "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
-by (Simp_tac  1);
-by (Blast_tac 1);
-qed "rel_pow_Suc_I";
-
-Goal "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
-by (induct_tac "n" 1);
-by (Simp_tac  1);
-by (Asm_full_simp_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "rel_pow_Suc_I2";
-
-Goal "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
-by (Asm_full_simp_tac 1);
-qed "rel_pow_0_E";
-
-val [major,minor] = Goal
-  "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
-by (cut_facts_tac [major] 1);
-by (Asm_full_simp_tac  1);
-by (blast_tac (claset() addIs [minor]) 1);
-qed "rel_pow_Suc_E";
-
-val [p1,p2,p3] = Goal
-    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
-\       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
-\    |] ==> P";
-by (cut_facts_tac [p1] 1);
-by (case_tac "n" 1);
-by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
-by (Asm_full_simp_tac 1);
-by (etac compEpair 1);
-by (REPEAT(ares_tac [p3] 1));
-qed "rel_pow_E";
-
-Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
-by (induct_tac "n" 1);
-by (blast_tac (claset() addIs [rel_pow_0_I] 
-	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
-by (blast_tac (claset() addIs [rel_pow_Suc_I]  
-	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
-qed_spec_mp "rel_pow_Suc_D2";
-
-
-Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
-by (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-qed_spec_mp "rel_pow_Suc_D2'";
-
-val [p1,p2,p3] = Goal
-    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
-\       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
-\    |] ==> P";
-by (cut_facts_tac [p1] 1);
-by (case_tac "n" 1);
-by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
-by (Asm_full_simp_tac 1);
-by (etac compEpair 1);
-by (dtac (conjI RS rel_pow_Suc_D2') 1);
-by (assume_tac 1);
-by (etac exE 1);
-by (etac p3 1);
-by (etac conjunct1 1);
-by (etac conjunct2 1);
-qed "rel_pow_E2";
-
-Goal "!!p. p:R^* ==> p : (UN n. R^n)";
-by (split_all_tac 1);
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [rel_pow_0_I,rel_pow_Suc_I])));
-qed "rtrancl_imp_UN_rel_pow";
-
-Goal "!y. (x,y):R^n --> (x,y):R^*";
-by (induct_tac "n" 1);
-by (blast_tac (claset() addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
-by (blast_tac (claset() addEs [rel_pow_Suc_E]
-                       addIs [rtrancl_into_rtrancl]) 1);
-val lemma = result() RS spec RS mp;
-
-Goal "!!p. p:R^n ==> p:R^*";
-by (split_all_tac 1);
-by (etac lemma 1);
-qed "rel_pow_imp_rtrancl";
-
-Goal "R^* = (UN n. R^n)";
-by (blast_tac (claset() addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
-qed "rtrancl_is_UN_rel_pow";
-
-
-Goal "!!r::('a * 'a)set. univalent r ==> univalent (r^n)";
-by (rtac univalentI 1);
-by (induct_tac "n" 1);
- by (Simp_tac 1);
-by (fast_tac (claset() addDs [univalentD] addEs [rel_pow_Suc_E]) 1);
-qed_spec_mp "univalent_rel_pow";
-
-
-
-
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/RelPow.thy
--- a/src/HOL/RelPow.thy	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      HOL/RelPow.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1996  TU Muenchen
-
-R^n = R O ... O R, the n-fold composition of R
-*)
-
-RelPow = Nat +
-
-instance
-  set :: (term) {power}   (* only ('a * 'a) set should be in power! *)
-
-primrec (relpow)
-  "R^0 = Id"
-  "R^(Suc n) = R O (R^n)"
-
-end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Relation_Power.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Relation_Power.ML	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,115 @@
+(*  Title:      HOL/Relation_Power.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996  TU Muenchen
+*)
+
+Goal "!!R:: ('a*'a)set. R^1 = R";
+by (Simp_tac 1);
+qed "rel_pow_1";
+Addsimps [rel_pow_1];
+
+Goal "(x,x) : R^0";
+by (Simp_tac 1);
+qed "rel_pow_0_I";
+
+Goal "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
+by (Simp_tac  1);
+by (Blast_tac 1);
+qed "rel_pow_Suc_I";
+
+Goal "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
+by (induct_tac "n" 1);
+by (Simp_tac  1);
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
+qed_spec_mp "rel_pow_Suc_I2";
+
+Goal "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
+by (Asm_full_simp_tac 1);
+qed "rel_pow_0_E";
+
+val [major,minor] = Goal
+  "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
+by (cut_facts_tac [major] 1);
+by (Asm_full_simp_tac  1);
+by (blast_tac (claset() addIs [minor]) 1);
+qed "rel_pow_Suc_E";
+
+val [p1,p2,p3] = Goal
+    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
+\       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
+\    |] ==> P";
+by (cut_facts_tac [p1] 1);
+by (case_tac "n" 1);
+by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
+by (Asm_full_simp_tac 1);
+by (etac compEpair 1);
+by (REPEAT(ares_tac [p3] 1));
+qed "rel_pow_E";
+
+Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
+by (induct_tac "n" 1);
+by (blast_tac (claset() addIs [rel_pow_0_I] 
+	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (blast_tac (claset() addIs [rel_pow_Suc_I]  
+	                addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
+qed_spec_mp "rel_pow_Suc_D2";
+
+
+Goal "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
+by (induct_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+qed_spec_mp "rel_pow_Suc_D2'";
+
+val [p1,p2,p3] = Goal
+    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
+\       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
+\    |] ==> P";
+by (cut_facts_tac [p1] 1);
+by (case_tac "n" 1);
+by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
+by (Asm_full_simp_tac 1);
+by (etac compEpair 1);
+by (dtac (conjI RS rel_pow_Suc_D2') 1);
+by (assume_tac 1);
+by (etac exE 1);
+by (etac p3 1);
+by (etac conjunct1 1);
+by (etac conjunct2 1);
+qed "rel_pow_E2";
+
+Goal "!!p. p:R^* ==> p : (UN n. R^n)";
+by (split_all_tac 1);
+by (etac rtrancl_induct 1);
+by (ALLGOALS (blast_tac (claset() addIs [rel_pow_0_I,rel_pow_Suc_I])));
+qed "rtrancl_imp_UN_rel_pow";
+
+Goal "!y. (x,y):R^n --> (x,y):R^*";
+by (induct_tac "n" 1);
+by (blast_tac (claset() addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
+by (blast_tac (claset() addEs [rel_pow_Suc_E]
+                       addIs [rtrancl_into_rtrancl]) 1);
+val lemma = result() RS spec RS mp;
+
+Goal "!!p. p:R^n ==> p:R^*";
+by (split_all_tac 1);
+by (etac lemma 1);
+qed "rel_pow_imp_rtrancl";
+
+Goal "R^* = (UN n. R^n)";
+by (blast_tac (claset() addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
+qed "rtrancl_is_UN_rel_pow";
+
+
+Goal "!!r::('a * 'a)set. univalent r ==> univalent (r^n)";
+by (rtac univalentI 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (fast_tac (claset() addDs [univalentD] addEs [rel_pow_Suc_E]) 1);
+qed_spec_mp "univalent_rel_pow";
+
+
+
+
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Relation_Power.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Relation_Power.thy	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,18 @@
+(*  Title:      HOL/Relation_Power.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1996  TU Muenchen
+
+R^n = R O ... O R, the n-fold composition of R
+*)
+
+Relation_Power = Nat +
+
+instance
+  set :: (term) {power}   (* only ('a * 'a) set should be in power! *)
+
+primrec (relpow)
+  "R^0 = Id"
+  "R^(Suc n) = R O (R^n)"
+
+end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Sum.thy
--- a/src/HOL/Sum.thy	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(*  Title:      HOL/Sum.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-The disjoint sum of two types.
-*)
-
-Sum = mono + Prod +
-
-(* type definition *)
-
-constdefs
-  Inl_Rep       :: ['a, 'a, 'b, bool] => bool
-  "Inl_Rep == (%a. %x y p. x=a & p)"
-
-  Inr_Rep       :: ['b, 'a, 'b, bool] => bool
-  "Inr_Rep == (%b. %x y p. y=b & ~p)"
-
-global
-
-typedef (Sum)
-  ('a, 'b) "+"          (infixr 10)
-    = "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}"
-
-
-(* abstract constants and syntax *)
-
-consts
-  Inl            :: "'a => 'a + 'b"
-  Inr            :: "'b => 'a + 'b"
-
-  (*disjoint sum for sets; the operator + is overloaded with wrong type!*)
-  Plus          :: "['a set, 'b set] => ('a + 'b) set"        (infixr "<+>" 65)
-  Part          :: ['a set, 'b => 'a] => 'a set
-
-local
-
-defs
-  Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
-  Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
-
-  sum_def       "A <+> B == (Inl``A) Un (Inr``B)"
-
-  (*for selecting out the components of a mutually recursive definition*)
-  Part_def      "Part A h == A Int {x. ? z. x = h(z)}"
-
-end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Sum_Type.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Sum_Type.ML	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,178 @@
+(*  Title:      HOL/Sum_Type.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+
+The disjoint sum of two types
+*)
+
+(** Inl_Rep and Inr_Rep: Representations of the constructors **)
+
+(*This counts as a non-emptiness result for admitting 'a+'b as a type*)
+Goalw [Sum_def] "Inl_Rep(a) : Sum";
+by (EVERY1 [rtac CollectI, rtac disjI1, rtac exI, rtac refl]);
+qed "Inl_RepI";
+
+Goalw [Sum_def] "Inr_Rep(b) : Sum";
+by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]);
+qed "Inr_RepI";
+
+Goal "inj_on Abs_Sum Sum";
+by (rtac inj_on_inverseI 1);
+by (etac Abs_Sum_inverse 1);
+qed "inj_on_Abs_Sum";
+
+(** Distinctness of Inl and Inr **)
+
+Goalw [Inl_Rep_def, Inr_Rep_def] "Inl_Rep(a) ~= Inr_Rep(b)";
+by (EVERY1 [rtac notI,
+            etac (fun_cong RS fun_cong RS fun_cong RS iffE), 
+            rtac (notE RS ccontr),  etac (mp RS conjunct2), 
+            REPEAT o (ares_tac [refl,conjI]) ]);
+qed "Inl_Rep_not_Inr_Rep";
+
+Goalw [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
+by (rtac (inj_on_Abs_Sum RS inj_on_contraD) 1);
+by (rtac Inl_Rep_not_Inr_Rep 1);
+by (rtac Inl_RepI 1);
+by (rtac Inr_RepI 1);
+qed "Inl_not_Inr";
+
+bind_thm ("Inr_not_Inl", Inl_not_Inr RS not_sym);
+
+AddIffs [Inl_not_Inr, Inr_not_Inl];
+
+bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE);
+bind_thm ("Inr_neq_Inl", sym RS Inl_neq_Inr);
+
+
+(** Injectiveness of Inl and Inr **)
+
+Goalw [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
+by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
+by (Blast_tac 1);
+qed "Inl_Rep_inject";
+
+Goalw [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
+by (etac (fun_cong RS fun_cong RS fun_cong RS iffE) 1);
+by (Blast_tac 1);
+qed "Inr_Rep_inject";
+
+Goalw [Inl_def] "inj(Inl)";
+by (rtac injI 1);
+by (etac (inj_on_Abs_Sum RS inj_onD RS Inl_Rep_inject) 1);
+by (rtac Inl_RepI 1);
+by (rtac Inl_RepI 1);
+qed "inj_Inl";
+bind_thm ("Inl_inject", inj_Inl RS injD);
+
+Goalw [Inr_def] "inj(Inr)";
+by (rtac injI 1);
+by (etac (inj_on_Abs_Sum RS inj_onD RS Inr_Rep_inject) 1);
+by (rtac Inr_RepI 1);
+by (rtac Inr_RepI 1);
+qed "inj_Inr";
+bind_thm ("Inr_inject", inj_Inr RS injD);
+
+Goal "(Inl(x)=Inl(y)) = (x=y)";
+by (blast_tac (claset() addSDs [Inl_inject]) 1);
+qed "Inl_eq";
+
+Goal "(Inr(x)=Inr(y)) = (x=y)";
+by (blast_tac (claset() addSDs [Inr_inject]) 1);
+qed "Inr_eq";
+
+AddIffs [Inl_eq, Inr_eq];
+
+(*** Rules for the disjoint sum of two SETS ***)
+
+(** Introduction rules for the injections **)
+
+Goalw [sum_def] "a : A ==> Inl(a) : A <+> B";
+by (Blast_tac 1);
+qed "InlI";
+
+Goalw [sum_def] "b : B ==> Inr(b) : A <+> B";
+by (Blast_tac 1);
+qed "InrI";
+
+(** Elimination rules **)
+
+val major::prems = Goalw [sum_def]
+    "[| u: A <+> B;  \
+\       !!x. [| x:A;  u=Inl(x) |] ==> P; \
+\       !!y. [| y:B;  u=Inr(y) |] ==> P \
+\    |] ==> P";
+by (rtac (major RS UnE) 1);
+by (REPEAT (rtac refl 1
+     ORELSE eresolve_tac (prems@[imageE,ssubst]) 1));
+qed "PlusE";
+
+
+AddSIs [InlI, InrI]; 
+AddSEs [PlusE];
+
+
+(** Exhaustion rule for sums -- a degenerate form of induction **)
+
+val prems = Goalw [Inl_def,Inr_def]
+    "[| !!x::'a. s = Inl(x) ==> P;  !!y::'b. s = Inr(y) ==> P \
+\    |] ==> P";
+by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
+by (REPEAT (eresolve_tac [disjE,exE] 1
+     ORELSE EVERY1 [resolve_tac prems, 
+                    etac subst,
+                    rtac (Rep_Sum_inverse RS sym)]));
+qed "sumE";
+
+val prems = Goal "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x";
+by (res_inst_tac [("s","x")] sumE 1);
+by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
+qed "sum_induct";
+
+
+(** Rules for the Part primitive **)
+
+Goalw [Part_def] "[| a : A;  a=h(b) |] ==> a : Part A h";
+by (Blast_tac 1);
+qed "Part_eqI";
+
+bind_thm ("PartI", refl RSN (2,Part_eqI));
+
+val major::prems = Goalw [Part_def]
+    "[| a : Part A h;  !!z. [| a : A;  a=h(z) |] ==> P  \
+\    |] ==> P";
+by (rtac (major RS IntE) 1);
+by (etac CollectE 1);
+by (etac exE 1);
+by (REPEAT (ares_tac prems 1));
+qed "PartE";
+
+AddIs  [Part_eqI];
+AddSEs [PartE];
+
+Goalw [Part_def] "Part A h <= A";
+by (rtac Int_lower1 1);
+qed "Part_subset";
+
+Goal "A<=B ==> Part A h <= Part B h";
+by (Blast_tac 1);
+qed "Part_mono";
+
+val basic_monos = basic_monos @ [Part_mono];
+
+Goalw [Part_def] "a : Part A h ==> a : A";
+by (etac IntD1 1);
+qed "PartD1";
+
+Goal "Part A (%x. x) = A";
+by (Blast_tac 1);
+qed "Part_id";
+
+Goal "Part (A Int B) h = (Part A h) Int (Part B h)";
+by (Blast_tac 1);
+qed "Part_Int";
+
+Goal "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}";
+by (Blast_tac 1);
+qed "Part_Collect";
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Sum_Type.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Sum_Type.thy	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,48 @@
+(*  Title:      HOL/Sum_Type.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+The disjoint sum of two types.
+*)
+
+Sum_Type = mono + Product_Type +
+
+(* type definition *)
+
+constdefs
+  Inl_Rep       :: ['a, 'a, 'b, bool] => bool
+  "Inl_Rep == (%a. %x y p. x=a & p)"
+
+  Inr_Rep       :: ['b, 'a, 'b, bool] => bool
+  "Inr_Rep == (%b. %x y p. y=b & ~p)"
+
+global
+
+typedef (Sum)
+  ('a, 'b) "+"          (infixr 10)
+    = "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}"
+
+
+(* abstract constants and syntax *)
+
+consts
+  Inl            :: "'a => 'a + 'b"
+  Inr            :: "'b => 'a + 'b"
+
+  (*disjoint sum for sets; the operator + is overloaded with wrong type!*)
+  Plus          :: "['a set, 'b set] => ('a + 'b) set"        (infixr "<+>" 65)
+  Part          :: ['a set, 'b => 'a] => 'a set
+
+local
+
+defs
+  Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
+  Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
+
+  sum_def       "A <+> B == (Inl``A) Un (Inr``B)"
+
+  (*for selecting out the components of a mutually recursive definition*)
+  Part_def      "Part A h == A Int {x. ? z. x = h(z)}"
+
+end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,403 +0,0 @@
-(*  Title:      HOL/Trancl
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Theorems about the transitive closure of a relation
-*)
-
-(** The relation rtrancl **)
-
-section "^*";
-
-Goal "mono(%s. Id Un (r O s))";
-by (rtac monoI 1);
-by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
-qed "rtrancl_fun_mono";
-
-bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_unfold));
-
-(*Reflexivity of rtrancl*)
-Goal "(a,a) : r^*";
-by (stac rtrancl_unfold 1);
-by (Blast_tac 1);
-qed "rtrancl_refl";
-
-Addsimps [rtrancl_refl];
-AddSIs   [rtrancl_refl];
-
-
-(*Closure under composition with r*)
-Goal "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
-by (stac rtrancl_unfold 1);
-by (Blast_tac 1);
-qed "rtrancl_into_rtrancl";
-
-(*rtrancl of r contains r*)
-Goal "!!p. p : r ==> p : r^*";
-by (split_all_tac 1);
-by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
-qed "r_into_rtrancl";
-
-AddIs [r_into_rtrancl];
-
-(*monotonicity of rtrancl*)
-Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
-by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
-qed "rtrancl_mono";
-
-(** standard induction rule **)
-
-val major::prems = Goal 
-  "[| (a,b) : r^*; \
-\     !!x. P(x,x); \
-\     !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |]  ==>  P(x,z) |] \
-\  ==>  P(a,b)";
-by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_lfp_induct) 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "rtrancl_full_induct";
-
-(*nice induction rule*)
-val major::prems = Goal
-    "[| (a::'a,b) : r^*;    \
-\       P(a); \
-\       !!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
-\     ==> P(b)";
-(*by induction on this formula*)
-by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
-(*now solve first subgoal: this formula is sufficient*)
-by (Blast_tac 1);
-(*now do the induction*)
-by (resolve_tac [major RS rtrancl_full_induct] 1);
-by (blast_tac (claset() addIs prems) 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "rtrancl_induct";
-
-bind_thm ("rtrancl_induct2", split_rule
-  (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct));
-
-(*transitivity of transitive closure!! -- by induction.*)
-Goalw [trans_def] "trans(r^*)";
-by Safe_tac;
-by (eres_inst_tac [("b","z")] rtrancl_induct 1);
-by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl])));
-qed "trans_rtrancl";
-
-bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
-
-
-(*elimination of rtrancl -- by induction on a special formula*)
-val major::prems = Goal
-    "[| (a::'a,b) : r^*;  (a = b) ==> P;        \
-\       !!y.[| (a,y) : r^*; (y,b) : r |] ==> P  \
-\    |] ==> P";
-by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
-by (rtac (major RS rtrancl_induct) 2);
-by (blast_tac (claset() addIs prems) 2);
-by (blast_tac (claset() addIs prems) 2);
-by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
-qed "rtranclE";
-
-bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
-bind_thms("rtranclIs", [r_into_rtrancl, rtrancl_trans]);
-
-(*** More r^* equations and inclusions ***)
-
-Goal "(r^*)^* = r^*";
-by Auto_tac;
-by (etac rtrancl_induct 1);
-by (rtac rtrancl_refl 1);
-by (blast_tac (claset() addIs rtranclIs) 1);
-qed "rtrancl_idemp";
-Addsimps [rtrancl_idemp];
-
-Goal "R^* O R^* = R^*";
-by (rtac set_ext 1);
-by (split_all_tac 1);
-by (blast_tac (claset() addIs rtranclIs) 1);
-qed "rtrancl_idemp_self_comp";
-Addsimps [rtrancl_idemp_self_comp];
-
-Goal "r <= s^* ==> r^* <= s^*";
-by (dtac rtrancl_mono 1);
-by (Asm_full_simp_tac 1);
-qed "rtrancl_subset_rtrancl";
-
-Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
-by (dtac rtrancl_mono 1);
-by (dtac rtrancl_mono 1);
-by (Asm_full_simp_tac 1);
-by (Blast_tac 1);
-qed "rtrancl_subset";
-
-Goal "(R^* Un S^*)^* = (R Un S)^*";
-by (blast_tac (claset() addSIs [rtrancl_subset]
-                        addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
-qed "rtrancl_Un_rtrancl";
-
-Goal "(R^=)^* = R^*";
-by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1);
-qed "rtrancl_reflcl";
-Addsimps [rtrancl_reflcl];
-
-Goal "(r - Id)^* = r^*";
-by (rtac sym 1);
-by (rtac rtrancl_subset 1);
- by (Blast_tac 1);
-by (Clarify_tac 1);
-by (rename_tac "a b" 1);
-by (case_tac "a=b" 1);
- by (Blast_tac 1);
-by (blast_tac (claset() addSIs [r_into_rtrancl]) 1);
-qed "rtrancl_r_diff_Id";
-
-Goal "(x,y) : (r^-1)^* ==> (y,x) : r^*";
-by (etac rtrancl_induct 1);
-by (rtac rtrancl_refl 1);
-by (blast_tac (claset() addIs rtranclIs) 1);
-qed "rtrancl_converseD";
-
-Goal "(y,x) : r^* ==> (x,y) : (r^-1)^*";
-by (etac rtrancl_induct 1);
-by (rtac rtrancl_refl 1);
-by (blast_tac (claset() addIs rtranclIs) 1);
-qed "rtrancl_converseI";
-
-Goal "(r^-1)^* = (r^*)^-1";
-(*blast_tac fails: the split_all_tac wrapper must be called to convert
-  the set element to a pair*)
-by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
-qed "rtrancl_converse";
-
-val major::prems = Goal
-    "[| (a,b) : r^*; P(b); \
-\       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
-\     ==> P(a)";
-by (rtac (major RS rtrancl_converseI RS rtrancl_induct) 1);
-by (resolve_tac prems 1);
-by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
-qed "converse_rtrancl_induct";
-
-bind_thm ("converse_rtrancl_induct2", split_rule
-  (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")]converse_rtrancl_induct));
-
-val major::prems = Goal
- "[| (x,z):r^*; \
-\    x=z ==> P; \
-\    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
-\ |] ==> P";
-by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
-by (rtac (major RS converse_rtrancl_induct) 2);
-by (blast_tac (claset() addIs prems) 2);
-by (blast_tac (claset() addIs prems) 2);
-by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
-qed "converse_rtranclE";
-
-bind_thm ("converse_rtranclE2", split_rule
-  (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] converse_rtranclE));
-
-Goal "r O r^* = r^* O r";
-by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] 
-	               addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
-qed "r_comp_rtrancl_eq";
-
-
-(**** The relation trancl ****)
-
-section "^+";
-
-Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
-by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
-qed "trancl_mono";
-
-(** Conversions between trancl and rtrancl **)
-
-Goalw [trancl_def]
-    "!!p. p : r^+ ==> p : r^*";
-by (split_all_tac 1);
-by (etac compEpair 1);
-by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
-qed "trancl_into_rtrancl";
-
-(*r^+ contains r*)
-Goalw [trancl_def]
-   "!!p. p : r ==> p : r^+";
-by (split_all_tac 1);
-by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
-qed "r_into_trancl";
-AddIs [r_into_trancl];
-
-(*intro rule by definition: from rtrancl and r*)
-Goalw [trancl_def] "[| (a,b) : r^*;  (b,c) : r |]   ==>  (a,c) : r^+";
-by Auto_tac;
-qed "rtrancl_into_trancl1";
-
-(*intro rule from r and rtrancl*)
-Goal "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+";
-by (etac rtranclE 1);
-by (blast_tac (claset() addIs [r_into_trancl]) 1);
-by (rtac (rtrancl_trans RS rtrancl_into_trancl1) 1);
-by (REPEAT (ares_tac [r_into_rtrancl] 1));
-qed "rtrancl_into_trancl2";
-
-(*Nice induction rule for trancl*)
-val major::prems = Goal
-  "[| (a,b) : r^+;                                      \
-\     !!y.  [| (a,y) : r |] ==> P(y);                   \
-\     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
-\  |] ==> P(b)";
-by (rtac (rewrite_rule [trancl_def] major  RS  compEpair) 1);
-(*by induction on this formula*)
-by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
-(*now solve first subgoal: this formula is sufficient*)
-by (Blast_tac 1);
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs (rtrancl_into_trancl1::prems))));
-qed "trancl_induct";
-
-(*Another induction rule for trancl, incorporating transitivity.*)
-val major::prems = Goal
- "[| (x,y) : r^+; \
-\    !!x y. (x,y) : r ==> P x y; \
-\    !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
-\ |] ==> P x y";
-by (blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
-qed "trancl_trans_induct";
-
-(*elimination of r^+ -- NOT an induction rule*)
-val major::prems = Goal
-    "[| (a::'a,b) : r^+;  \
-\       (a,b) : r ==> P; \
-\       !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P  \
-\    |] ==> P";
-by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+  &  (y,b) : r)" 1);
-by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
-by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
-by (etac rtranclE 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addSIs [rtrancl_into_trancl1]) 1);
-qed "tranclE";
-
-(*Transitivity of r^+.
-  Proved by unfolding since it uses transitivity of rtrancl. *)
-Goalw [trancl_def] "trans(r^+)";
-by (rtac transI 1);
-by (REPEAT (etac compEpair 1));
-by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS compI)) 1);
-by (REPEAT (assume_tac 1));
-qed "trans_trancl";
-
-bind_thm ("trancl_trans", trans_trancl RS transD);
-
-Goalw [trancl_def] "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
-by (blast_tac (claset() addIs rtranclIs) 1);
-qed "rtrancl_trancl_trancl";
-
-(* "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+" *)
-bind_thm ("trancl_into_trancl2", [trans_trancl, r_into_trancl] MRS transD);
-
-(* primitive recursion for trancl over finite relations: *)
-Goal "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
-by (rtac equalityI 1);
- by (rtac subsetI 1);
- by (split_all_tac 1);
- by (etac trancl_induct 1);
-  by (blast_tac (claset() addIs [r_into_trancl]) 1);
- by (blast_tac (claset() addIs
-     [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
-by (rtac subsetI 1);
-by (blast_tac (claset() addIs
-     [rtrancl_into_trancl2, rtrancl_trancl_trancl,
-      impOfSubs rtrancl_mono, trancl_mono]) 1);
-qed "trancl_insert";
-
-Goalw [trancl_def] "(r^-1)^+ = (r^+)^-1";
-by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
-by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,
-				  r_comp_rtrancl_eq]) 1);
-qed "trancl_converse";
-
-Goal "(x,y) : (r^+)^-1 ==> (x,y) : (r^-1)^+";
-by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
-qed "trancl_converseI";
-
-Goal "(x,y) : (r^-1)^+ ==> (x,y) : (r^+)^-1";
-by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
-qed "trancl_converseD";
-
-val major::prems = Goal
-    "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); \
-\       !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]  \
-\     ==> P(a)";
-by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
- by (resolve_tac prems 1);
- by (etac converseD 1);
-by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
-qed "converse_trancl_induct";
-
-Goal "(x,y):R^+ ==> ? z. (x,z):R & (z,y):R^*";
-be converse_trancl_induct 1;
-by Auto_tac;
-by (blast_tac (claset() addIs [rtrancl_trans]) 1);
-qed "tranclD";
-
-(*Unused*)
-Goal "r^-1 Int r^+ = {} ==> (x, x) ~: r^+";
-by (subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1);
-by (Fast_tac 1);
-by (strip_tac 1);
-by (etac trancl_induct 1);
-by (auto_tac (claset() addIs [r_into_trancl], simpset()));
-qed "irrefl_tranclI";
-
-Goal "!!X. [| !x. (x, x) ~: r^+; (x,y) : r |] ==> x ~= y";
-by (blast_tac (claset() addDs [r_into_trancl]) 1);
-qed "irrefl_trancl_rD";
-
-Goal "[| (a,b) : r^*;  r <= A <*> A |] ==> a=b | a:A";
-by (etac rtrancl_induct 1);
-by Auto_tac;
-val lemma = result();
-
-Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
-by (blast_tac (claset() addSDs [lemma]) 1);
-qed "trancl_subset_Sigma";
-
-
-Goal "(r^+)^= = r^*";
-by Safe_tac;
-by  (etac trancl_into_rtrancl 1);
-by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
-qed "reflcl_trancl";
-Addsimps[reflcl_trancl];
-
-Goal "(r^=)^+ = r^*";
-by Safe_tac;
-by  (dtac trancl_into_rtrancl 1);
-by  (Asm_full_simp_tac 1);
-by (etac rtranclE 1);
-by  Safe_tac;
-by  (rtac r_into_trancl 1);
-by  (Simp_tac 1);
-by (rtac rtrancl_into_trancl1 1);
-by (etac (rtrancl_reflcl RS equalityD2 RS subsetD) 1);
-by (Fast_tac 1);
-qed "trancl_reflcl";
-Addsimps[trancl_reflcl];
-
-Goal "{}^+ = {}";
-by (auto_tac (claset() addEs [trancl_induct], simpset()));
-qed "trancl_empty";
-Addsimps[trancl_empty];
-
-Goal "{}^* = Id";
-by (rtac (reflcl_trancl RS subst) 1);
-by (Simp_tac 1);
-qed "rtrancl_empty";
-Addsimps[rtrancl_empty];
-
-Goal "(a,b):R^* ==> a=b | a~=b & (a,b):R^+";
-by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
-				  delsimps [reflcl_trancl]) 1);
-qed "rtranclD";
-
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Trancl.thy
--- a/src/HOL/Trancl.thy	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      HOL/Trancl.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Relfexive and Transitive closure of a relation
-
-rtrancl is reflexive/transitive closure;
-trancl  is transitive closure
-reflcl  is reflexive closure
-
-These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
-      atomic.
-*)
-
-Trancl = Lfp + Relation + 
-
-constdefs
-  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 999)
-  "r^*  ==  lfp(%s. Id Un (r O s))"
-
-  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
-  "r^+  ==  r O rtrancl(r)"
-
-syntax
-  "_reflcl"  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
-
-translations
-  "r^=" == "r Un Id"
-
-end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Transitive_Closure.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Transitive_Closure.ML	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,402 @@
+(*  Title:      HOL/Transitive_Closure
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Theorems about the transitive closure of a relation
+*)
+
+(** The relation rtrancl **)
+
+section "^*";
+
+Goal "mono(%s. Id Un (r O s))";
+by (rtac monoI 1);
+by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
+qed "rtrancl_fun_mono";
+
+bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_unfold));
+
+(*Reflexivity of rtrancl*)
+Goal "(a,a) : r^*";
+by (stac rtrancl_unfold 1);
+by (Blast_tac 1);
+qed "rtrancl_refl";
+
+Addsimps [rtrancl_refl];
+AddSIs   [rtrancl_refl];
+
+
+(*Closure under composition with r*)
+Goal "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
+by (stac rtrancl_unfold 1);
+by (Blast_tac 1);
+qed "rtrancl_into_rtrancl";
+
+(*rtrancl of r contains r*)
+Goal "!!p. p : r ==> p : r^*";
+by (split_all_tac 1);
+by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
+qed "r_into_rtrancl";
+
+AddIs [r_into_rtrancl];
+
+(*monotonicity of rtrancl*)
+Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
+by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
+qed "rtrancl_mono";
+
+(** standard induction rule **)
+
+val major::prems = Goal 
+  "[| (a,b) : r^*; \
+\     !!x. P(x,x); \
+\     !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |]  ==>  P(x,z) |] \
+\  ==>  P(a,b)";
+by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_lfp_induct) 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "rtrancl_full_induct";
+
+(*nice induction rule*)
+val major::prems = Goal
+    "[| (a::'a,b) : r^*;    \
+\       P(a); \
+\       !!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
+\     ==> P(b)";
+(*by induction on this formula*)
+by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
+(*now solve first subgoal: this formula is sufficient*)
+by (Blast_tac 1);
+(*now do the induction*)
+by (resolve_tac [major RS rtrancl_full_induct] 1);
+by (blast_tac (claset() addIs prems) 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "rtrancl_induct";
+
+bind_thm ("rtrancl_induct2", split_rule
+  (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct));
+
+(*transitivity of transitive closure!! -- by induction.*)
+Goalw [trans_def] "trans(r^*)";
+by Safe_tac;
+by (eres_inst_tac [("b","z")] rtrancl_induct 1);
+by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl])));
+qed "trans_rtrancl";
+
+bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
+
+
+(*elimination of rtrancl -- by induction on a special formula*)
+val major::prems = Goal
+    "[| (a::'a,b) : r^*;  (a = b) ==> P;        \
+\       !!y.[| (a,y) : r^*; (y,b) : r |] ==> P  \
+\    |] ==> P";
+by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
+by (rtac (major RS rtrancl_induct) 2);
+by (blast_tac (claset() addIs prems) 2);
+by (blast_tac (claset() addIs prems) 2);
+by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
+qed "rtranclE";
+
+bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
+
+(*** More r^* equations and inclusions ***)
+
+Goal "(r^*)^* = r^*";
+by Auto_tac;
+by (etac rtrancl_induct 1);
+by (rtac rtrancl_refl 1);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
+qed "rtrancl_idemp";
+Addsimps [rtrancl_idemp];
+
+Goal "R^* O R^* = R^*";
+by (rtac set_ext 1);
+by (split_all_tac 1);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
+qed "rtrancl_idemp_self_comp";
+Addsimps [rtrancl_idemp_self_comp];
+
+Goal "r <= s^* ==> r^* <= s^*";
+by (dtac rtrancl_mono 1);
+by (Asm_full_simp_tac 1);
+qed "rtrancl_subset_rtrancl";
+
+Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
+by (dtac rtrancl_mono 1);
+by (dtac rtrancl_mono 1);
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
+qed "rtrancl_subset";
+
+Goal "(R^* Un S^*)^* = (R Un S)^*";
+by (blast_tac (claset() addSIs [rtrancl_subset]
+                        addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
+qed "rtrancl_Un_rtrancl";
+
+Goal "(R^=)^* = R^*";
+by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1);
+qed "rtrancl_reflcl";
+Addsimps [rtrancl_reflcl];
+
+Goal "(r - Id)^* = r^*";
+by (rtac sym 1);
+by (rtac rtrancl_subset 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (rename_tac "a b" 1);
+by (case_tac "a=b" 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addSIs [r_into_rtrancl]) 1);
+qed "rtrancl_r_diff_Id";
+
+Goal "(x,y) : (r^-1)^* ==> (y,x) : r^*";
+by (etac rtrancl_induct 1);
+by (rtac rtrancl_refl 1);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
+qed "rtrancl_converseD";
+
+Goal "(y,x) : r^* ==> (x,y) : (r^-1)^*";
+by (etac rtrancl_induct 1);
+by (rtac rtrancl_refl 1);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
+qed "rtrancl_converseI";
+
+Goal "(r^-1)^* = (r^*)^-1";
+(*blast_tac fails: the split_all_tac wrapper must be called to convert
+  the set element to a pair*)
+by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
+qed "rtrancl_converse";
+
+val major::prems = Goal
+    "[| (a,b) : r^*; P(b); \
+\       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
+\     ==> P(a)";
+by (rtac (major RS rtrancl_converseI RS rtrancl_induct) 1);
+by (resolve_tac prems 1);
+by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
+qed "converse_rtrancl_induct";
+
+bind_thm ("converse_rtrancl_induct2", split_rule
+  (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")]converse_rtrancl_induct));
+
+val major::prems = Goal
+ "[| (x,z):r^*; \
+\    x=z ==> P; \
+\    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
+\ |] ==> P";
+by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
+by (rtac (major RS converse_rtrancl_induct) 2);
+by (blast_tac (claset() addIs prems) 2);
+by (blast_tac (claset() addIs prems) 2);
+by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
+qed "converse_rtranclE";
+
+bind_thm ("converse_rtranclE2", split_rule
+  (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] converse_rtranclE));
+
+Goal "r O r^* = r^* O r";
+by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] 
+	               addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
+qed "r_comp_rtrancl_eq";
+
+
+(**** The relation trancl ****)
+
+section "^+";
+
+Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
+by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
+qed "trancl_mono";
+
+(** Conversions between trancl and rtrancl **)
+
+Goalw [trancl_def]
+    "!!p. p : r^+ ==> p : r^*";
+by (split_all_tac 1);
+by (etac compEpair 1);
+by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
+qed "trancl_into_rtrancl";
+
+(*r^+ contains r*)
+Goalw [trancl_def]
+   "!!p. p : r ==> p : r^+";
+by (split_all_tac 1);
+by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
+qed "r_into_trancl";
+AddIs [r_into_trancl];
+
+(*intro rule by definition: from rtrancl and r*)
+Goalw [trancl_def] "[| (a,b) : r^*;  (b,c) : r |]   ==>  (a,c) : r^+";
+by Auto_tac;
+qed "rtrancl_into_trancl1";
+
+(*intro rule from r and rtrancl*)
+Goal "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+";
+by (etac rtranclE 1);
+by (blast_tac (claset() addIs [r_into_trancl]) 1);
+by (rtac (rtrancl_trans RS rtrancl_into_trancl1) 1);
+by (REPEAT (ares_tac [r_into_rtrancl] 1));
+qed "rtrancl_into_trancl2";
+
+(*Nice induction rule for trancl*)
+val major::prems = Goal
+  "[| (a,b) : r^+;                                      \
+\     !!y.  [| (a,y) : r |] ==> P(y);                   \
+\     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
+\  |] ==> P(b)";
+by (rtac (rewrite_rule [trancl_def] major  RS  compEpair) 1);
+(*by induction on this formula*)
+by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
+(*now solve first subgoal: this formula is sufficient*)
+by (Blast_tac 1);
+by (etac rtrancl_induct 1);
+by (ALLGOALS (blast_tac (claset() addIs (rtrancl_into_trancl1::prems))));
+qed "trancl_induct";
+
+(*Another induction rule for trancl, incorporating transitivity.*)
+val major::prems = Goal
+ "[| (x,y) : r^+; \
+\    !!x y. (x,y) : r ==> P x y; \
+\    !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
+\ |] ==> P x y";
+by (blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
+qed "trancl_trans_induct";
+
+(*elimination of r^+ -- NOT an induction rule*)
+val major::prems = Goal
+    "[| (a::'a,b) : r^+;  \
+\       (a,b) : r ==> P; \
+\       !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P  \
+\    |] ==> P";
+by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+  &  (y,b) : r)" 1);
+by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
+by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
+by (etac rtranclE 1);
+by (Blast_tac 1);
+by (blast_tac (claset() addSIs [rtrancl_into_trancl1]) 1);
+qed "tranclE";
+
+(*Transitivity of r^+.
+  Proved by unfolding since it uses transitivity of rtrancl. *)
+Goalw [trancl_def] "trans(r^+)";
+by (rtac transI 1);
+by (REPEAT (etac compEpair 1));
+by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS compI)) 1);
+by (REPEAT (assume_tac 1));
+qed "trans_trancl";
+
+bind_thm ("trancl_trans", trans_trancl RS transD);
+
+Goalw [trancl_def] "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
+qed "rtrancl_trancl_trancl";
+
+(* "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+" *)
+bind_thm ("trancl_into_trancl2", [trans_trancl, r_into_trancl] MRS transD);
+
+(* primitive recursion for trancl over finite relations: *)
+Goal "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
+by (rtac equalityI 1);
+ by (rtac subsetI 1);
+ by (split_all_tac 1);
+ by (etac trancl_induct 1);
+  by (blast_tac (claset() addIs [r_into_trancl]) 1);
+ by (blast_tac (claset() addIs
+     [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
+by (rtac subsetI 1);
+by (blast_tac (claset() addIs
+     [rtrancl_into_trancl2, rtrancl_trancl_trancl,
+      impOfSubs rtrancl_mono, trancl_mono]) 1);
+qed "trancl_insert";
+
+Goalw [trancl_def] "(r^-1)^+ = (r^+)^-1";
+by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
+by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,
+				  r_comp_rtrancl_eq]) 1);
+qed "trancl_converse";
+
+Goal "(x,y) : (r^+)^-1 ==> (x,y) : (r^-1)^+";
+by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
+qed "trancl_converseI";
+
+Goal "(x,y) : (r^-1)^+ ==> (x,y) : (r^+)^-1";
+by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
+qed "trancl_converseD";
+
+val major::prems = Goal
+    "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); \
+\       !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]  \
+\     ==> P(a)";
+by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
+ by (resolve_tac prems 1);
+ by (etac converseD 1);
+by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
+qed "converse_trancl_induct";
+
+Goal "(x,y):R^+ ==> ? z. (x,z):R & (z,y):R^*";
+be converse_trancl_induct 1;
+by Auto_tac;
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
+qed "tranclD";
+
+(*Unused*)
+Goal "r^-1 Int r^+ = {} ==> (x, x) ~: r^+";
+by (subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1);
+by (Fast_tac 1);
+by (strip_tac 1);
+by (etac trancl_induct 1);
+by (auto_tac (claset() addIs [r_into_trancl], simpset()));
+qed "irrefl_tranclI";
+
+Goal "!!X. [| !x. (x, x) ~: r^+; (x,y) : r |] ==> x ~= y";
+by (blast_tac (claset() addDs [r_into_trancl]) 1);
+qed "irrefl_trancl_rD";
+
+Goal "[| (a,b) : r^*;  r <= A <*> A |] ==> a=b | a:A";
+by (etac rtrancl_induct 1);
+by Auto_tac;
+val lemma = result();
+
+Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
+by (blast_tac (claset() addSDs [lemma]) 1);
+qed "trancl_subset_Sigma";
+
+
+Goal "(r^+)^= = r^*";
+by Safe_tac;
+by  (etac trancl_into_rtrancl 1);
+by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
+qed "reflcl_trancl";
+Addsimps[reflcl_trancl];
+
+Goal "(r^=)^+ = r^*";
+by Safe_tac;
+by  (dtac trancl_into_rtrancl 1);
+by  (Asm_full_simp_tac 1);
+by (etac rtranclE 1);
+by  Safe_tac;
+by  (rtac r_into_trancl 1);
+by  (Simp_tac 1);
+by (rtac rtrancl_into_trancl1 1);
+by (etac (rtrancl_reflcl RS equalityD2 RS subsetD) 1);
+by (Fast_tac 1);
+qed "trancl_reflcl";
+Addsimps[trancl_reflcl];
+
+Goal "{}^+ = {}";
+by (auto_tac (claset() addEs [trancl_induct], simpset()));
+qed "trancl_empty";
+Addsimps[trancl_empty];
+
+Goal "{}^* = Id";
+by (rtac (reflcl_trancl RS subst) 1);
+by (Simp_tac 1);
+qed "rtrancl_empty";
+Addsimps[rtrancl_empty];
+
+Goal "(a,b):R^* ==> a=b | a~=b & (a,b):R^+";
+by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
+				  delsimps [reflcl_trancl]) 1);
+qed "rtranclD";
+
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Transitive_Closure.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Transitive_Closure.thy	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,31 @@
+(*  Title:      HOL/Transitive_Closure.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Relfexive and Transitive closure of a relation
+
+rtrancl is reflexive/transitive closure;
+trancl  is transitive closure
+reflcl  is reflexive closure
+
+These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
+      atomic.
+*)
+
+Transitive_Closure = Lfp + Relation + 
+
+constdefs
+  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 999)
+  "r^*  ==  lfp(%s. Id Un (r O s))"
+
+  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
+  "r^+  ==  r O rtrancl(r)"
+
+syntax
+  "_reflcl"  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
+
+translations
+  "r^=" == "r Un Id"
+
+end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,595 +0,0 @@
-(*  Title:      HOL/Univ
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-*)
-
-(** apfst -- can be used in similar type definitions **)
-
-Goalw [apfst_def] "apfst f (a,b) = (f(a),b)";
-by (rtac split 1);
-qed "apfst_conv";
-
-val [major,minor] = Goal
-    "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R \
-\    |] ==> R";
-by (rtac PairE 1);
-by (rtac minor 1);
-by (assume_tac 1);
-by (rtac (major RS trans) 1);
-by (etac ssubst 1);
-by (rtac apfst_conv 1);
-qed "apfst_convE";
-
-(** Push -- an injection, analogous to Cons on lists **)
-
-Goalw [Push_def] "Push i f = Push j g  ==> i=j";
-by (etac (fun_cong RS box_equals) 1);
-by (rtac nat_case_0 1);
-by (rtac nat_case_0 1);
-qed "Push_inject1";
-
-Goalw [Push_def] "Push i f = Push j g  ==> f=g";
-by (rtac (ext RS box_equals) 1);
-by (etac fun_cong 1);
-by (rtac (nat_case_Suc RS ext) 1);
-by (rtac (nat_case_Suc RS ext) 1);
-qed "Push_inject2";
-
-val [major,minor] = Goal
-    "[| Push i f =Push j g;  [| i=j;  f=g |] ==> P \
-\    |] ==> P";
-by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1);
-qed "Push_inject";
-
-Goalw [Push_def] "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P";
-by (rtac Suc_neq_Zero 1);
-by (etac (fun_cong RS box_equals RS Inr_inject) 1);
-by (rtac nat_case_0 1);
-by (rtac refl 1);
-qed "Push_neq_K0";
-
-(*** Isomorphisms ***)
-
-Goal "inj(Rep_Node)";
-by (rtac inj_inverseI 1);       (*cannot combine by RS: multiple unifiers*)
-by (rtac Rep_Node_inverse 1);
-qed "inj_Rep_Node";
-
-Goal "inj_on Abs_Node Node";
-by (rtac inj_on_inverseI 1);
-by (etac Abs_Node_inverse 1);
-qed "inj_on_Abs_Node";
-
-bind_thm ("Abs_Node_inject", inj_on_Abs_Node RS inj_onD);
-
-
-(*** Introduction rules for Node ***)
-
-Goalw [Node_def] "(%k. Inr 0, a) : Node";
-by (Blast_tac 1);
-qed "Node_K0_I";
-
-Goalw [Node_def,Push_def]
-    "p: Node ==> apfst (Push i) p : Node";
-by (fast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
-qed "Node_Push_I";
-
-
-(*** Distinctness of constructors ***)
-
-(** Scons vs Atom **)
-
-Goalw [Atom_def,Scons_def,Push_Node_def] "Scons M N ~= Atom(a)";
-by (rtac notI 1);
-by (etac (equalityD2 RS subsetD RS UnE) 1);
-by (rtac singletonI 1);
-by (REPEAT (eresolve_tac [imageE, Abs_Node_inject RS apfst_convE, 
-                          Pair_inject, sym RS Push_neq_K0] 1
-     ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1));
-qed "Scons_not_Atom";
-bind_thm ("Atom_not_Scons", Scons_not_Atom RS not_sym);
-
-
-(*** Injectiveness ***)
-
-(** Atomic nodes **)
-
-Goalw [Atom_def] "inj(Atom)";
-by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inject]) 1);
-qed "inj_Atom";
-bind_thm ("Atom_inject", inj_Atom RS injD);
-
-Goal "(Atom(a)=Atom(b)) = (a=b)";
-by (blast_tac (claset() addSDs [Atom_inject]) 1);
-qed "Atom_Atom_eq";
-AddIffs [Atom_Atom_eq];
-
-Goalw [Leaf_def,o_def] "inj(Leaf)";
-by (rtac injI 1);
-by (etac (Atom_inject RS Inl_inject) 1);
-qed "inj_Leaf";
-
-bind_thm ("Leaf_inject", inj_Leaf RS injD);
-AddSDs [Leaf_inject];
-
-Goalw [Numb_def,o_def] "inj(Numb)";
-by (rtac injI 1);
-by (etac (Atom_inject RS Inr_inject) 1);
-qed "inj_Numb";
-
-bind_thm ("Numb_inject", inj_Numb RS injD);
-AddSDs [Numb_inject];
-
-(** Injectiveness of Push_Node **)
-
-val [major,minor] = Goalw [Push_Node_def]
-    "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P \
-\    |] ==> P";
-by (rtac (major RS Abs_Node_inject RS apfst_convE) 1);
-by (REPEAT (resolve_tac [Rep_Node RS Node_Push_I] 1));
-by (etac (sym RS apfst_convE) 1);
-by (rtac minor 1);
-by (etac Pair_inject 1);
-by (etac (Push_inject1 RS sym) 1);
-by (rtac (inj_Rep_Node RS injD) 1);
-by (etac trans 1);
-by (safe_tac (claset() addSEs [Push_inject,sym]));
-qed "Push_Node_inject";
-
-
-(** Injectiveness of Scons **)
-
-Goalw [Scons_def] "Scons M N <= Scons M' N' ==> M<=M'";
-by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
-qed "Scons_inject_lemma1";
-
-Goalw [Scons_def] "Scons M N <= Scons M' N' ==> N<=N'";
-by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
-qed "Scons_inject_lemma2";
-
-Goal "Scons M N = Scons M' N' ==> M=M'";
-by (etac equalityE 1);
-by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));
-qed "Scons_inject1";
-
-Goal "Scons M N = Scons M' N' ==> N=N'";
-by (etac equalityE 1);
-by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1));
-qed "Scons_inject2";
-
-val [major,minor] = Goal
-    "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P \
-\    |] ==> P";
-by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
-qed "Scons_inject";
-
-Goal "(Scons M N = Scons M' N') = (M=M' & N=N')";
-by (blast_tac (claset() addSEs [Scons_inject]) 1);
-qed "Scons_Scons_eq";
-
-(*** Distinctness involving Leaf and Numb ***)
-
-(** Scons vs Leaf **)
-
-Goalw [Leaf_def,o_def] "Scons M N ~= Leaf(a)";
-by (rtac Scons_not_Atom 1);
-qed "Scons_not_Leaf";
-bind_thm ("Leaf_not_Scons", Scons_not_Leaf RS not_sym);
-
-AddIffs [Scons_not_Leaf, Leaf_not_Scons];
-
-
-(** Scons vs Numb **)
-
-Goalw [Numb_def,o_def] "Scons M N ~= Numb(k)";
-by (rtac Scons_not_Atom 1);
-qed "Scons_not_Numb";
-bind_thm ("Numb_not_Scons", Scons_not_Numb RS not_sym);
-
-AddIffs [Scons_not_Numb, Numb_not_Scons];
-
-
-(** Leaf vs Numb **)
-
-Goalw [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)";
-by (simp_tac (simpset() addsimps [Inl_not_Inr]) 1);
-qed "Leaf_not_Numb";
-bind_thm ("Numb_not_Leaf", Leaf_not_Numb RS not_sym);
-
-AddIffs [Leaf_not_Numb, Numb_not_Leaf];
-
-
-(*** ndepth -- the depth of a node ***)
-
-Addsimps [apfst_conv];
-AddIffs  [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
-
-
-Goalw [ndepth_def] "ndepth (Abs_Node(%k. Inr 0, x)) = 0";
-by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
-by (rtac Least_equality 1);
-by (rtac refl 1);
-by (etac less_zeroE 1);
-qed "ndepth_K0";
-
-Goal "k < Suc(LEAST x. f x = Inr 0) --> nat_case (Inr (Suc i)) f k ~= Inr 0";
-by (induct_tac "k" 1);
-by (ALLGOALS Simp_tac);
-by (rtac impI 1);
-by (etac not_less_Least 1);
-val lemma = result();
-
-Goalw [ndepth_def,Push_Node_def]
-    "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))";
-by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1);
-by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
-by Safe_tac;
-by (etac ssubst 1);  (*instantiates type variables!*)
-by (Simp_tac 1);
-by (rtac Least_equality 1);
-by (rewtac Push_def);
-by (rtac (nat_case_Suc RS trans) 1);
-by (etac LeastI 1);
-by (asm_simp_tac (simpset() addsimps [lemma]) 1);
-qed "ndepth_Push_Node";
-
-
-(*** ntrunc applied to the various node sets ***)
-
-Goalw [ntrunc_def] "ntrunc 0 M = {}";
-by (Blast_tac 1);
-qed "ntrunc_0";
-
-Goalw [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)";
-by (fast_tac (claset() addss (simpset() addsimps [ndepth_K0])) 1);
-qed "ntrunc_Atom";
-
-Goalw [Leaf_def,o_def] "ntrunc (Suc k) (Leaf a) = Leaf(a)";
-by (rtac ntrunc_Atom 1);
-qed "ntrunc_Leaf";
-
-Goalw [Numb_def,o_def] "ntrunc (Suc k) (Numb i) = Numb(i)";
-by (rtac ntrunc_Atom 1);
-qed "ntrunc_Numb";
-
-Goalw [Scons_def,ntrunc_def]
-    "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)";
-by (safe_tac (claset() addSIs [imageI]));
-by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
-by (REPEAT (rtac Suc_less_SucD 1 THEN 
-            rtac (ndepth_Push_Node RS subst) 1 THEN 
-            assume_tac 1));
-qed "ntrunc_Scons";
-
-Addsimps [ntrunc_0, ntrunc_Atom, ntrunc_Leaf, ntrunc_Numb, ntrunc_Scons];
-
-
-(** Injection nodes **)
-
-Goalw [In0_def] "ntrunc 1 (In0 M) = {}";
-by (Simp_tac 1);
-by (rewtac Scons_def);
-by (Blast_tac 1);
-qed "ntrunc_one_In0";
-
-Goalw [In0_def]
-    "ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)";
-by (Simp_tac 1);
-qed "ntrunc_In0";
-
-Goalw [In1_def] "ntrunc 1 (In1 M) = {}";
-by (Simp_tac 1);
-by (rewtac Scons_def);
-by (Blast_tac 1);
-qed "ntrunc_one_In1";
-
-Goalw [In1_def]
-    "ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)";
-by (Simp_tac 1);
-qed "ntrunc_In1";
-
-Addsimps [ntrunc_one_In0, ntrunc_In0, ntrunc_one_In1, ntrunc_In1];
-
-
-(*** Cartesian Product ***)
-
-Goalw [uprod_def] "[| M:A;  N:B |] ==> Scons M N : uprod A B";
-by (REPEAT (ares_tac [singletonI,UN_I] 1));
-qed "uprodI";
-
-(*The general elimination rule*)
-val major::prems = Goalw [uprod_def]
-    "[| c : uprod A B;  \
-\       !!x y. [| x:A;  y:B;  c = Scons x y |] ==> P \
-\    |] ==> P";
-by (cut_facts_tac [major] 1);
-by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1
-     ORELSE resolve_tac prems 1));
-qed "uprodE";
-
-(*Elimination of a pair -- introduces no eigenvariables*)
-val prems = Goal
-    "[| Scons M N : uprod A B;      [| M:A;  N:B |] ==> P   \
-\    |] ==> P";
-by (rtac uprodE 1);
-by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Scons_inject,ssubst] 1));
-qed "uprodE2";
-
-
-(*** Disjoint Sum ***)
-
-Goalw [usum_def] "M:A ==> In0(M) : usum A B";
-by (Blast_tac 1);
-qed "usum_In0I";
-
-Goalw [usum_def] "N:B ==> In1(N) : usum A B";
-by (Blast_tac 1);
-qed "usum_In1I";
-
-val major::prems = Goalw [usum_def]
-    "[| u : usum A B;  \
-\       !!x. [| x:A;  u=In0(x) |] ==> P; \
-\       !!y. [| y:B;  u=In1(y) |] ==> P \
-\    |] ==> P";
-by (rtac (major RS UnE) 1);
-by (REPEAT (rtac refl 1 
-     ORELSE eresolve_tac (prems@[imageE,ssubst]) 1));
-qed "usumE";
-
-
-(** Injection **)
-
-Goalw [In0_def,In1_def] "In0(M) ~= In1(N)";
-by (rtac notI 1);
-by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
-qed "In0_not_In1";
-
-bind_thm ("In1_not_In0", In0_not_In1 RS not_sym);
-
-AddIffs [In0_not_In1, In1_not_In0];
-
-Goalw [In0_def] "In0(M) = In0(N) ==>  M=N";
-by (etac (Scons_inject2) 1);
-qed "In0_inject";
-
-Goalw [In1_def] "In1(M) = In1(N) ==>  M=N";
-by (etac (Scons_inject2) 1);
-qed "In1_inject";
-
-Goal "(In0 M = In0 N) = (M=N)";
-by (blast_tac (claset() addSDs [In0_inject]) 1);
-qed "In0_eq";
-
-Goal "(In1 M = In1 N) = (M=N)";
-by (blast_tac (claset() addSDs [In1_inject]) 1);
-qed "In1_eq";
-
-AddIffs [In0_eq, In1_eq];
-
-Goal "inj In0";
-by (blast_tac (claset() addSIs [injI]) 1);
-qed "inj_In0";
-
-Goal "inj In1";
-by (blast_tac (claset() addSIs [injI]) 1);
-qed "inj_In1";
-
-
-(*** Function spaces ***)
-
-Goalw [Lim_def] "Lim f = Lim g ==> f = g";
-by (rtac ext 1);
-by (blast_tac (claset() addSEs [Push_Node_inject]) 1);
-qed "Lim_inject";
-
-Goalw [Funs_def] "S <= T ==> Funs S <= Funs T";
-by (Blast_tac 1);
-qed "Funs_mono";
-
-val [prem] = Goalw [Funs_def] "(!!x. f x : S) ==> f : Funs S";
-by (blast_tac (claset() addIs [prem]) 1);
-qed "FunsI";
-
-Goalw [Funs_def] "f : Funs S ==> f x : S";
-by (etac CollectE 1);
-by (etac subsetD 1);
-by (rtac rangeI 1);
-qed "FunsD";
-
-val [p1, p2] = Goalw [o_def]
-   "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
-by (rtac (p2 RS ext) 1);
-by (rtac (p1 RS FunsD) 1);
-qed "Funs_inv";
-
-val [p1, p2] = Goalw [o_def]
-     "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
-by (res_inst_tac [("h", "%x. @y. (f::'a=>'b) x = g y")] p2 1);
-by (rtac ext 1);
-by (rtac (p1 RS FunsD RS rangeE) 1);
-by (etac (exI RS (some_eq_ex RS iffD2)) 1);
-qed "Funs_rangeE";
-
-Goal "a : S ==> (%x. a) : Funs S";
-by (rtac FunsI 1);
-by (assume_tac 1);
-qed "Funs_nonempty";
-
-
-(*** proving equality of sets and functions using ntrunc ***)
-
-Goalw [ntrunc_def] "ntrunc k M <= M";
-by (Blast_tac 1);
-qed "ntrunc_subsetI";
-
-val [major] = Goalw [ntrunc_def] "(!!k. ntrunc k M <= N) ==> M<=N";
-by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2, 
-			       major RS subsetD]) 1);
-qed "ntrunc_subsetD";
-
-(*A generalized form of the take-lemma*)
-val [major] = Goal "(!!k. ntrunc k M = ntrunc k N) ==> M=N";
-by (rtac equalityI 1);
-by (ALLGOALS (rtac ntrunc_subsetD));
-by (ALLGOALS (rtac (ntrunc_subsetI RSN (2, subset_trans))));
-by (rtac (major RS equalityD1) 1);
-by (rtac (major RS equalityD2) 1);
-qed "ntrunc_equality";
-
-val [major] = Goalw [o_def]
-    "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
-by (rtac (ntrunc_equality RS ext) 1);
-by (rtac (major RS fun_cong) 1);
-qed "ntrunc_o_equality";
-
-(*** Monotonicity ***)
-
-Goalw [uprod_def] "[| A<=A';  B<=B' |] ==> uprod A B <= uprod A' B'";
-by (Blast_tac 1);
-qed "uprod_mono";
-
-Goalw [usum_def] "[| A<=A';  B<=B' |] ==> usum A B <= usum A' B'";
-by (Blast_tac 1);
-qed "usum_mono";
-
-Goalw [Scons_def] "[| M<=M';  N<=N' |] ==> Scons M N <= Scons M' N'";
-by (Blast_tac 1);
-qed "Scons_mono";
-
-Goalw [In0_def] "M<=N ==> In0(M) <= In0(N)";
-by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
-qed "In0_mono";
-
-Goalw [In1_def] "M<=N ==> In1(M) <= In1(N)";
-by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
-qed "In1_mono";
-
-
-(*** Split and Case ***)
-
-Goalw [Split_def] "Split c (Scons M N) = c M N";
-by (Blast_tac  1);
-qed "Split";
-
-Goalw [Case_def] "Case c d (In0 M) = c(M)";
-by (Blast_tac 1);
-qed "Case_In0";
-
-Goalw [Case_def] "Case c d (In1 N) = d(N)";
-by (Blast_tac 1);
-qed "Case_In1";
-
-Addsimps [Split, Case_In0, Case_In1];
-
-
-(**** UN x. B(x) rules ****)
-
-Goalw [ntrunc_def] "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))";
-by (Blast_tac 1);
-qed "ntrunc_UN1";
-
-Goalw [Scons_def] "Scons (UN x. f x) M = (UN x. Scons (f x) M)";
-by (Blast_tac 1);
-qed "Scons_UN1_x";
-
-Goalw [Scons_def] "Scons M (UN x. f x) = (UN x. Scons M (f x))";
-by (Blast_tac 1);
-qed "Scons_UN1_y";
-
-Goalw [In0_def] "In0(UN x. f(x)) = (UN x. In0(f(x)))";
-by (rtac Scons_UN1_y 1);
-qed "In0_UN1";
-
-Goalw [In1_def] "In1(UN x. f(x)) = (UN x. In1(f(x)))";
-by (rtac Scons_UN1_y 1);
-qed "In1_UN1";
-
-
-(*** Equality for Cartesian Product ***)
-
-Goalw [dprod_def]
-    "[| (M,M'):r;  (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s";
-by (Blast_tac 1);
-qed "dprodI";
-
-(*The general elimination rule*)
-val major::prems = Goalw [dprod_def]
-    "[| c : dprod r s;  \
-\       !!x y x' y'. [| (x,x') : r;  (y,y') : s;  c = (Scons x y, Scons x' y') |] ==> P \
-\    |] ==> P";
-by (cut_facts_tac [major] 1);
-by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, mem_splitE, singletonE]));
-by (REPEAT (ares_tac prems 1 ORELSE hyp_subst_tac 1));
-qed "dprodE";
-
-
-(*** Equality for Disjoint Sum ***)
-
-Goalw [dsum_def]  "(M,M'):r ==> (In0(M), In0(M')) : dsum r s";
-by (Blast_tac 1);
-qed "dsum_In0I";
-
-Goalw [dsum_def]  "(N,N'):s ==> (In1(N), In1(N')) : dsum r s";
-by (Blast_tac 1);
-qed "dsum_In1I";
-
-val major::prems = Goalw [dsum_def]
-    "[| w : dsum r s;  \
-\       !!x x'. [| (x,x') : r;  w = (In0(x), In0(x')) |] ==> P; \
-\       !!y y'. [| (y,y') : s;  w = (In1(y), In1(y')) |] ==> P \
-\    |] ==> P";
-by (cut_facts_tac [major] 1);
-by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, UnE, mem_splitE, singletonE]));
-by (DEPTH_SOLVE (ares_tac prems 1 ORELSE hyp_subst_tac 1));
-qed "dsumE";
-
-AddSIs [uprodI, dprodI];
-AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
-AddSEs [uprodE, dprodE, usumE, dsumE];
-
-
-(*** Monotonicity ***)
-
-Goal "[| r<=r';  s<=s' |] ==> dprod r s <= dprod r' s'";
-by (Blast_tac 1);
-qed "dprod_mono";
-
-Goal "[| r<=r';  s<=s' |] ==> dsum r s <= dsum r' s'";
-by (Blast_tac 1);
-qed "dsum_mono";
-
-
-(*** Bounding theorems ***)
-
-Goal "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)";
-by (Blast_tac 1);
-qed "dprod_Sigma";
-
-bind_thm ("dprod_subset_Sigma", [dprod_mono, dprod_Sigma] MRS subset_trans |> standard);
-
-(*Dependent version*)
-Goal "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))";
-by Safe_tac;
-by (stac Split 1);
-by (Blast_tac 1);
-qed "dprod_subset_Sigma2";
-
-Goal "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)";
-by (Blast_tac 1);
-qed "dsum_Sigma";
-
-bind_thm ("dsum_subset_Sigma", [dsum_mono, dsum_Sigma] MRS subset_trans |> standard);
-
-
-(*** Domain ***)
-
-Goal "Domain (dprod r s) = uprod (Domain r) (Domain s)";
-by Auto_tac;
-qed "Domain_dprod";
-
-Goal "Domain (dsum r s) = usum (Domain r) (Domain s)";
-by Auto_tac;
-qed "Domain_dsum";
-
-Addsimps [Domain_dprod, Domain_dsum];
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Univ.thy
--- a/src/HOL/Univ.thy	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-(*  Title:      HOL/Univ.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Declares the type ('a, 'b) node, a subtype of (nat=>'b+nat) * ('a+nat)
-
-Defines "Cartesian Product" and "Disjoint Sum" as set operations.
-Could <*> be generalized to a general summation (Sigma)?
-*)
-
-Univ = Arith + Sum +
-
-
-(** lists, trees will be sets of nodes **)
-
-typedef (Node)
-  ('a, 'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
-
-types
-  'a item = ('a, unit) node set
-  ('a, 'b) dtree = ('a, 'b) node set
-
-consts
-  apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
-  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
-
-  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
-  ndepth    :: ('a, 'b) node => nat
-
-  Atom      :: "('a + nat) => ('a, 'b) dtree"
-  Leaf      :: 'a => ('a, 'b) dtree
-  Numb      :: nat => ('a, 'b) dtree
-  Scons     :: [('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree
-  In0,In1   :: ('a, 'b) dtree => ('a, 'b) dtree
-
-  Lim       :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree
-  Funs      :: "'u set => ('t => 'u) set"
-
-  ntrunc    :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree
-
-  uprod     :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set
-  usum      :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set
-
-  Split     :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
-  Case      :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
-
-  dprod     :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 
-                => (('a, 'b) dtree * ('a, 'b) dtree)set"
-  dsum      :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 
-                => (('a, 'b) dtree * ('a, 'b) dtree)set"
-
-
-defs
-
-  Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
-
-  (*crude "lists" of nats -- needed for the constructions*)
-  apfst_def  "apfst == (%f (x,y). (f(x),y))"
-  Push_def   "Push == (%b h. nat_case b h)"
-
-  (** operations on S-expressions -- sets of nodes **)
-
-  (*S-expression constructors*)
-  Atom_def   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
-  Scons_def  "Scons M N == (Push_Node (Inr 1) `` M) Un (Push_Node (Inr 2) `` N)"
-
-  (*Leaf nodes, with arbitrary or nat labels*)
-  Leaf_def   "Leaf == Atom o Inl"
-  Numb_def   "Numb == Atom o Inr"
-
-  (*Injections of the "disjoint sum"*)
-  In0_def    "In0(M) == Scons (Numb 0) M"
-  In1_def    "In1(M) == Scons (Numb 1) M"
-
-  (*Function spaces*)
-  Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) `` (f x)}"
-  Funs_def "Funs S == {f. range f <= S}"
-
-  (*the set of nodes with depth less than k*)
-  ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
-  ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}"
-
-  (*products and sums for the "universe"*)
-  uprod_def  "uprod A B == UN x:A. UN y:B. { Scons x y }"
-  usum_def   "usum A B == In0``A Un In1``B"
-
-  (*the corresponding eliminators*)
-  Split_def  "Split c M == @u. ? x y. M = Scons x y & u = c x y"
-
-  Case_def   "Case c d M == @u.  (? x . M = In0(x) & u = c(x)) 
-                               | (? y . M = In1(y) & u = d(y))"
-
-
-  (** equality for the "universe" **)
-
-  dprod_def  "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
-
-  dsum_def   "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 
-                          (UN (y,y'):s. {(In1(y),In1(y'))})"
-
-end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,108 +0,0 @@
-(*  Title:      HOL/Vimage
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Inverse image of a function
-*)
-
-(** Basic rules **)
-
-Goalw [vimage_def] "(a : f-``B) = (f a : B)";
-by (Blast_tac 1) ;
-qed "vimage_eq";
-
-Addsimps [vimage_eq];
-
-Goal "(a : f-``{b}) = (f a = b)";
-by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
-qed "vimage_singleton_eq";
-
-Goalw [vimage_def]
-    "!!A B f. [| f a = b;  b:B |] ==> a : f-``B";
-by (Blast_tac 1) ;
-qed "vimageI";
-
-Goalw [vimage_def] "f a : A ==> a : f -`` A";
-by (Fast_tac 1);
-qed "vimageI2";
-
-val major::prems = Goalw [vimage_def]
-    "[| a: f-``B;  !!x.[| f a = x;  x:B |] ==> P |] ==> P";
-by (rtac (major RS CollectE) 1);
-by (blast_tac (claset() addIs prems) 1) ;
-qed "vimageE";
-
-Goalw [vimage_def] "a : f -`` A ==> f a : A";
-by (Fast_tac 1);
-qed "vimageD";
-
-AddIs  [vimageI];
-AddSEs [vimageE];
-
-
-(*** Equations ***)
-
-Goal "f-``{} = {}";
-by (Blast_tac 1);
-qed "vimage_empty";
-
-Goal "f-``(-A) = -(f-``A)";
-by (Blast_tac 1);
-qed "vimage_Compl";
-
-Goal "f-``(A Un B) = (f-``A) Un (f-``B)";
-by (Blast_tac 1);
-qed "vimage_Un";
-
-Goal "f -`` (A Int B) = (f -`` A) Int (f -`` B)";
-by (Fast_tac 1);
-qed "vimage_Int";
-
-Goal "f -`` (Union A) = (UN X:A. f -`` X)";
-by (Blast_tac 1);
-qed "vimage_Union";
-
-Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
-by (Blast_tac 1);
-qed "vimage_UN";
-
-Goal "f-``(INT x:A. B x) = (INT x:A. f -`` B x)";
-by (Blast_tac 1);
-qed "vimage_INT";
-
-Goal "f -`` Collect P = {y. P (f y)}";
-by (Blast_tac 1);
-qed "vimage_Collect_eq";
-Addsimps [vimage_Collect_eq];
-
-(*A strange result used in Tools/inductive_package*)
-val prems = Goal "(!!x. P (f x) = Q x) ==> f -`` (Collect P) = Collect Q";
-by (force_tac (claset(), simpset() addsimps prems) 1);
-qed "vimage_Collect";
-
-Addsimps [vimage_empty, vimage_Un, vimage_Int];
-
-(*NOT suitable for rewriting because of the recurrence of {a}*)
-Goal "f-``(insert a B) = (f-``{a}) Un (f-``B)";
-by (Blast_tac 1);
-qed "vimage_insert";
-
-Goal "f-``(A-B) = (f-``A) - (f-``B)";
-by (Blast_tac 1);
-qed "vimage_Diff";
-
-Goal "f-``UNIV = UNIV";
-by (Blast_tac 1);
-qed "vimage_UNIV";
-Addsimps [vimage_UNIV];
-
-(*NOT suitable for rewriting*)
-Goal "f-``B = (UN y: B. f-``{y})";
-by (Blast_tac 1);
-qed "vimage_eq_UN";
-
-(*monotonicity*)
-Goal "A<=B ==> f-``A <= f-``B";
-by (Blast_tac 1);
-qed "vimage_mono";
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Vimage.thy
--- a/src/HOL/Vimage.thy	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      HOL/Vimage
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Inverse image of a function
-*)
-
-Vimage = Set +
-
-constdefs
-  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-``" 90)
-    "f-``B  == {x. f(x) : B}"
-
-end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,370 +0,0 @@
-(*  Title:      HOL/WF.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow, with minor changes by Konrad Slind
-    Copyright   1992  University of Cambridge/1995 TU Munich
-
-Wellfoundedness, induction, and  recursion
-*)
-
-Goal "x = y ==> H x z = H y z";
-by (Asm_simp_tac 1);
-val H_cong2 = (*freeze H!*)
-	      read_instantiate [("H","H")] (result());
-
-val [prem] = Goalw [wf_def]
- "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)";
-by (Clarify_tac 1);
-by (rtac prem 1);
-by (assume_tac 1);
-qed "wfUNIVI";
-
-(*Restriction to domain A.  If r is well-founded over A then wf(r)*)
-val [prem1,prem2] = Goalw [wf_def]
- "[| r <= A <*> A;  \
-\    !!x P. [| ALL x. (ALL y. (y,x) : r --> P y) --> P x;  x:A |] ==> P x |]  \
-\ ==>  wf r";
-by (cut_facts_tac [prem1] 1);
-by (blast_tac (claset() addIs [prem2]) 1);
-qed "wfI";
-
-val major::prems = Goalw [wf_def]
-    "[| wf(r);          \
-\       !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x) \
-\    |]  ==>  P(a)";
-by (rtac (major RS spec RS mp RS spec) 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "wf_induct";
-
-(*Perform induction on i, then prove the wf(r) subgoal using prems. *)
-fun wf_ind_tac a prems i = 
-    EVERY [res_inst_tac [("a",a)] wf_induct i,
-           rename_last_tac a ["1"] (i+1),
-           ares_tac prems i];
-
-Goal "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r";
-by (wf_ind_tac "a" [] 1);
-by (Blast_tac 1);
-qed_spec_mp "wf_not_sym";
-
-(* [| wf r;  ~Z ==> (a,x) : r;  (x,a) ~: r ==> Z |] ==> Z *)
-bind_thm ("wf_asym", cla_make_elim wf_not_sym);
-
-Goal "wf(r) ==> (a,a) ~: r";
-by (blast_tac (claset() addEs [wf_asym]) 1);
-qed "wf_not_refl";
-
-(* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
-bind_thm ("wf_irrefl", make_elim wf_not_refl);
-
-(*transitive closure of a wf relation is wf! *)
-Goal "wf(r) ==> wf(r^+)";
-by (stac wf_def 1);
-by (Clarify_tac 1);
-(*must retain the universal formula for later use!*)
-by (rtac allE 1 THEN assume_tac 1);
-by (etac mp 1);
-by (eres_inst_tac [("a","x")] wf_induct 1);
-by (blast_tac (claset() addEs [tranclE]) 1);
-qed "wf_trancl";
-
-Goal "wf (r^-1) ==> wf ((r^+)^-1)";
-by (stac (trancl_converse RS sym) 1);
-by (etac wf_trancl 1);
-qed "wf_converse_trancl";
-
-
-(*----------------------------------------------------------------------------
- * Minimal-element characterization of well-foundedness
- *---------------------------------------------------------------------------*)
-
-Goalw [wf_def] "wf r ==> x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q)";
-by (dtac spec 1);
-by (etac (mp RS spec) 1);
-by (Blast_tac 1);
-val lemma1 = result();
-
-Goalw [wf_def] "(ALL Q x. x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q)) ==> wf r";
-by (Clarify_tac 1);
-by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1);
-by (Blast_tac 1);
-val lemma2 = result();
-
-Goal "wf r = (ALL Q x. x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q))";
-by (blast_tac (claset() addSIs [lemma1, lemma2]) 1);
-qed "wf_eq_minimal";
-
-(*---------------------------------------------------------------------------
- * Wellfoundedness of subsets
- *---------------------------------------------------------------------------*)
-
-Goal "[| wf(r);  p<=r |] ==> wf(p)";
-by (full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
-by (Fast_tac 1);
-qed "wf_subset";
-
-(*---------------------------------------------------------------------------
- * Wellfoundedness of the empty relation.
- *---------------------------------------------------------------------------*)
-
-Goal "wf({})";
-by (simp_tac (simpset() addsimps [wf_def]) 1);
-qed "wf_empty";
-AddIffs [wf_empty];
-
-(*---------------------------------------------------------------------------
- * Wellfoundedness of `insert'
- *---------------------------------------------------------------------------*)
-
-Goal "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
-by (rtac iffI 1);
- by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] 
-	addIs [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
-by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
-by Safe_tac;
-by (EVERY1[rtac allE, assume_tac, etac impE, Blast_tac]);
-by (etac bexE 1);
-by (rename_tac "a" 1);
-by (case_tac "a = x" 1);
- by (res_inst_tac [("x","a")]bexI 2);
-  by (assume_tac 3);
- by (Blast_tac 2);
-by (case_tac "y:Q" 1);
- by (Blast_tac 2);
-by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1);
- by (assume_tac 1);
-by (thin_tac "ALL Q. (EX x. x : Q) --> ?P Q" 1);	(*essential for speed*)
-(*Blast_tac with new substOccur fails*)
-by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
-qed "wf_insert";
-AddIffs [wf_insert];
-
-(*---------------------------------------------------------------------------
- * Wellfoundedness of `disjoint union'
- *---------------------------------------------------------------------------*)
-
-(*Intuition behind this proof for the case of binary union:
-
-  Goal: find an (R u S)-min element of a nonempty subset A.
-  by case distinction:
-  1. There is a step a -R-> b with a,b : A.
-     Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.
-     By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the
-     subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot
-     have an S-successor and is thus S-min in A as well.
-  2. There is no such step.
-     Pick an S-min element of A. In this case it must be an R-min
-     element of A as well.
-
-*)
-
-Goal "[| ALL i:I. wf(r i); \
-\        ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
-\                                         Domain(r j) Int Range(r i) = {} \
-\     |] ==> wf(UN i:I. r i)";
-by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
-by (Clarify_tac 1);
-by (rename_tac "A a" 1);
-by (case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i" 1);
- by (Asm_full_simp_tac 2);
- by (Best_tac 2);  (*much faster than Blast_tac*)
-by (Clarify_tac 1);
-by (EVERY1[dtac bspec, assume_tac,
-	   eres_inst_tac [("x","{a. a:A & (EX b:A. (b,a) : r i)}")] allE]);
-by (EVERY1[etac allE, etac impE]);
- by (ALLGOALS Blast_tac);
-qed "wf_UN";
-
-Goalw [Union_def]
- "[| ALL r:R. wf r; \
-\    ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {} & \
-\                                 Domain s Int Range r = {} \
-\ |] ==> wf(Union R)";
-by (blast_tac (claset() addIs [wf_UN]) 1);
-qed "wf_Union";
-
-Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
-\     |] ==> wf(r Un s)";
-by (rtac (simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-qed "wf_Un";
-
-(*---------------------------------------------------------------------------
- * Wellfoundedness of `image'
- *---------------------------------------------------------------------------*)
-
-Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)";
-by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
-by (Clarify_tac 1);
-by (case_tac "EX p. f p : Q" 1);
-by (eres_inst_tac [("x","{p. f p : Q}")]allE 1);
-by (fast_tac (claset() addDs [injD]) 1);
-by (Blast_tac 1);
-qed "wf_prod_fun_image";
-
-(*** acyclic ***)
-
-Goalw [acyclic_def] "ALL x. (x, x) ~: r^+ ==> acyclic r";
-by (assume_tac 1);
-qed "acyclicI";
-
-Goalw [acyclic_def] "wf r ==> acyclic r";
-by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1);
-qed "wf_acyclic";
-
-Goalw [acyclic_def] "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
-by (simp_tac (simpset() addsimps [trancl_insert]) 1);
-by (blast_tac (claset() addIs [rtrancl_trans]) 1);
-qed "acyclic_insert";
-AddIffs [acyclic_insert];
-
-Goalw [acyclic_def] "acyclic(r^-1) = acyclic r";
-by (simp_tac (simpset() addsimps [trancl_converse]) 1);
-qed "acyclic_converse";
-AddIffs [acyclic_converse];
-
-Goalw [acyclic_def,antisym_def] "acyclic r ==> antisym(r^*)";
-by(blast_tac (claset() addEs [rtranclE]
-     addIs [rtrancl_into_trancl1,rtrancl_trancl_trancl]) 1);
-qed "acyclic_impl_antisym_rtrancl";
-
-(* Other direction:
-acyclic = no loops
-antisym = only self loops
-Goalw [acyclic_def,antisym_def] "antisym(r^* ) ==> acyclic(r - Id)";
-==> "antisym(r^* ) = acyclic(r - Id)";
-*)
-
-Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r";
-by (blast_tac (claset() addIs [trancl_mono]) 1);
-qed "acyclic_subset";
-
-(** cut **)
-
-(*This rewrite rule works upon formulae; thus it requires explicit use of
-  H_cong to expose the equality*)
-Goalw [cut_def] "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))";
-by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1);
-qed "cuts_eq";
-
-Goalw [cut_def] "(x,a):r ==> (cut f r a)(x) = f(x)";
-by (asm_simp_tac HOL_ss 1);
-qed "cut_apply";
-
-(*** is_recfun ***)
-
-Goalw [is_recfun_def,cut_def]
-    "[| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = arbitrary";
-by (etac ssubst 1);
-by (asm_simp_tac HOL_ss 1);
-qed "is_recfun_undef";
-
-(*** NOTE! some simplifications need a different Solver!! ***)
-fun indhyp_tac hyps =
-    (cut_facts_tac hyps THEN'
-       DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
-                        eresolve_tac [transD, mp, allE]));
-val wf_super_ss = HOL_ss addSolver (mk_solver "WF" indhyp_tac);
-
-Goalw [is_recfun_def,cut_def]
-    "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \
-    \ (x,a):r --> (x,b):r --> f(x)=g(x)";
-by (etac wf_induct 1);
-by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
-by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
-qed_spec_mp "is_recfun_equal";
-
-
-val prems as [wfr,transr,recfa,recgb,_] = goalw (the_context ()) [cut_def]
-    "[| wf(r);  trans(r); \
-\       is_recfun r H a f;  is_recfun r H b g;  (b,a):r |] ==> \
-\    cut f r b = g";
-val gundef = recgb RS is_recfun_undef
-and fisg   = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
-by (cut_facts_tac prems 1);
-by (rtac ext 1);
-by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]) 1);
-qed "is_recfun_cut";
-
-(*** Main Existence Lemma -- Basic Properties of the_recfun ***)
-
-Goalw [the_recfun_def]
-    "is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)";
-by (eres_inst_tac [("P", "is_recfun r H a")] someI 1);
-qed "is_the_recfun";
-
-Goal "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
-by (wf_ind_tac "a" [] 1);
-by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
-                 is_the_recfun 1);
-by (rewtac is_recfun_def);
-by (stac cuts_eq 1);
-by (Clarify_tac 1);
-by (rtac H_cong2 1);
-by (subgoal_tac
-         "the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1);
- by (Blast_tac 2);
-by (etac ssubst 1);
-by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
-by (Clarify_tac 1);
-by (stac cut_apply 1);
- by (fast_tac (claset() addDs [transD]) 1);
-by (fold_tac [is_recfun_def]);
-by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1);
-qed "unfold_the_recfun";
-
-Goal "[| wf r; trans r; (x,a) : r; (x,b) : r |] \
-\     ==> the_recfun r H a x = the_recfun r H b x";
-by (best_tac (claset() addIs [is_recfun_equal, unfold_the_recfun]) 1);
-qed "the_recfun_equal";
-
-(** Removal of the premise trans(r) **)
-val th = rewrite_rule[is_recfun_def]
-                     (trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun)));
-
-Goalw [wfrec_def]
-    "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
-by (rtac H_cong2 1);
-by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
-by (rtac allI 1);
-by (rtac impI 1);
-by (res_inst_tac [("a1","a")] (th RS ssubst) 1);
-by (assume_tac 1);
-by (ftac wf_trancl 1);
-by (ftac r_into_trancl 1);
-by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1);
-by (rtac H_cong2 1);    (*expose the equality of cuts*)
-by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1);
-by (blast_tac (claset() addIs [the_recfun_equal, transD, trans_trancl, 
-			       r_into_trancl]) 1);
-qed "wfrec";
-
-(*---------------------------------------------------------------------------
- * This form avoids giant explosions in proofs.  NOTE USE OF == 
- *---------------------------------------------------------------------------*)
-Goal "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a";
-by Auto_tac;
-by (blast_tac (claset() addIs [wfrec]) 1);   
-qed "def_wfrec";
-
-
-(**** TFL variants ****)
-
-Goal "ALL R. wf R --> \
-\      (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))";
-by (Clarify_tac 1);
-by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-qed"tfl_wf_induct";
-
-Goal "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)";
-by (Clarify_tac 1);
-by (rtac cut_apply 1);
-by (assume_tac 1);
-qed"tfl_cut_apply";
-
-Goal "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)";
-by (Clarify_tac 1);
-by (etac wfrec 1);
-qed "tfl_wfrec";
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/WF.thy
--- a/src/HOL/WF.thy	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      HOL/wf.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1992  University of Cambridge
-
-Well-founded Recursion
-*)
-
-WF = Trancl +
-
-constdefs
-  wf         :: "('a * 'a)set => bool"
-  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
-
-  acyclic :: "('a*'a)set => bool"
-  "acyclic r == !x. (x,x) ~: r^+"
-
-  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
-  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
-
-  is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
-  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
-
-  the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
-  "the_recfun r H a  == (@f. is_recfun r H a f)"
-
-  wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
-  "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
-                            r x)  x)"
-
-end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,226 +0,0 @@
-(*  Title: 	HOL/WF_Rel
-    ID:         $Id$
-    Author: 	Konrad Slind
-    Copyright   1996  TU Munich
-
-Derived WF relations: inverse image, lexicographic product, measure, ...
-*)
-
-
-(*----------------------------------------------------------------------------
- * "Less than" on the natural numbers
- *---------------------------------------------------------------------------*)
-
-Goalw [less_than_def] "wf less_than"; 
-by (rtac (wf_pred_nat RS wf_trancl) 1);
-qed "wf_less_than";
-AddIffs [wf_less_than];
-
-Goalw [less_than_def] "trans less_than"; 
-by (rtac trans_trancl 1);
-qed "trans_less_than";
-AddIffs [trans_less_than];
-
-Goalw [less_than_def, less_def] "((x,y): less_than) = (x<y)"; 
-by (Simp_tac 1);
-qed "less_than_iff";
-AddIffs [less_than_iff];
-
-Goal "(!!n. (ALL m. Suc m <= n --> P m) ==> P n) ==> P n";
-by (rtac (wf_less_than RS wf_induct) 1);
-by (resolve_tac (premises()) 1);
-by Auto_tac;
-qed_spec_mp "full_nat_induct";
-
-(*----------------------------------------------------------------------------
- * The inverse image into a wellfounded relation is wellfounded.
- *---------------------------------------------------------------------------*)
-
-Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
-by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1);
-by (Clarify_tac 1);
-by (subgoal_tac "EX (w::'b). w : {w. EX (x::'a). x: Q & (f x = w)}" 1);
-by (blast_tac (claset() delrules [allE]) 2);
-by (etac allE 1);
-by (mp_tac 1);
-by (Blast_tac 1);
-qed "wf_inv_image";
-AddSIs [wf_inv_image];
-
-Goalw [trans_def,inv_image_def]
-    "!!r. trans r ==> trans (inv_image r f)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "trans_inv_image";
-
-
-(*----------------------------------------------------------------------------
- * All measures are wellfounded.
- *---------------------------------------------------------------------------*)
-
-Goalw [measure_def] "wf (measure f)";
-by (rtac (wf_less_than RS wf_inv_image) 1);
-qed "wf_measure";
-AddIffs [wf_measure];
-
-val measure_induct = standard
-    (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
-      (wf_measure RS wf_induct));
-bind_thm ("measure_induct", measure_induct);
-
-(*----------------------------------------------------------------------------
- * Wellfoundedness of lexicographic combinations
- *---------------------------------------------------------------------------*)
-
-val [wfa,wfb] = goalw (the_context ()) [wf_def,lex_prod_def]
- "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)";
-by (EVERY1 [rtac allI,rtac impI]);
-by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
-by (rtac (wfa RS spec RS mp) 1);
-by (EVERY1 [rtac allI,rtac impI]);
-by (rtac (wfb RS spec RS mp) 1);
-by (Blast_tac 1);
-qed "wf_lex_prod";
-AddSIs [wf_lex_prod];
-
-(*---------------------------------------------------------------------------
- * Transitivity of WF combinators.
- *---------------------------------------------------------------------------*)
-Goalw [trans_def, lex_prod_def]
-    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "trans_lex_prod";
-AddSIs [trans_lex_prod];
-
-
-(*---------------------------------------------------------------------------
- * Wellfoundedness of proper subset on finite sets.
- *---------------------------------------------------------------------------*)
-Goalw [finite_psubset_def] "wf(finite_psubset)";
-by (rtac (wf_measure RS wf_subset) 1);
-by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def,
-				 symmetric less_def])1);
-by (fast_tac (claset() addSEs [psubset_card_mono]) 1);
-qed "wf_finite_psubset";
-
-Goalw [finite_psubset_def, trans_def] "trans finite_psubset";
-by (simp_tac (simpset() addsimps [psubset_def]) 1);
-by (Blast_tac 1);
-qed "trans_finite_psubset";
-
-(*---------------------------------------------------------------------------
- * Wellfoundedness of finite acyclic relations
- * Cannot go into WF because it needs Finite.
- *---------------------------------------------------------------------------*)
-
-Goal "finite r ==> acyclic r --> wf r";
-by (etac finite_induct 1);
- by (Blast_tac 1);
-by (split_all_tac 1);
-by (Asm_full_simp_tac 1);
-qed_spec_mp "finite_acyclic_wf";
-
-Goal "[|finite r; acyclic r|] ==> wf (r^-1)";
-by (etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1);
-by (etac (acyclic_converse RS iffD2) 1);
-qed "finite_acyclic_wf_converse";
-
-Goal "finite r ==> wf r = acyclic r";
-by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
-qed "wf_iff_acyclic_if_finite";
-
-
-(*---------------------------------------------------------------------------
- * A relation is wellfounded iff it has no infinite descending chain
- * Cannot go into WF because it needs type nat.
- *---------------------------------------------------------------------------*)
-
-Goalw [wf_eq_minimal RS eq_reflection]
-  "wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))";
-by (rtac iffI 1);
- by (rtac notI 1);
- by (etac exE 1);
- by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
- by (Blast_tac 1);
-by (etac swap 1);
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
- by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
- by (rtac allI 1);
- by (Simp_tac 1);
- by (rtac someI2_ex 1);
-  by (Blast_tac 1);
- by (Blast_tac 1);
-by (rtac allI 1);
-by (induct_tac "n" 1);
- by (Asm_simp_tac 1);
-by (Simp_tac 1);
-by (rtac someI2_ex 1);
- by (Blast_tac 1);
-by (Blast_tac 1);
-qed "wf_iff_no_infinite_down_chain";
-
-(*----------------------------------------------------------------------------
- * Weakly decreasing sequences (w.r.t. some well-founded order) stabilize.
- *---------------------------------------------------------------------------*)
-
-Goal "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*";
-by (induct_tac "k" 1);
- by (ALLGOALS Simp_tac);
-by (blast_tac (claset() addIs [rtrancl_trans]) 1);
-val lemma = result();
-
-Goal "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] \
-\     ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))";
-by (etac wf_induct 1);
-by (Clarify_tac 1);
-by (case_tac "EX j. (f (m+j), f m) : r^+" 1);
- by (Clarify_tac 1);
- by (subgoal_tac "EX i. ALL k. f ((m+j)+i+k) = f ((m+j)+i)" 1);
-  by (Clarify_tac 1);
-  by (res_inst_tac [("x","j+i")] exI 1);
-  by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
- by (Blast_tac 1);
-by (res_inst_tac [("x","0")] exI 1);
-by (Clarsimp_tac 1);
-by (dres_inst_tac [("i","m"), ("k","k")] lemma 1);
-by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
-val lemma = result();
-
-Goal "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] \
-\     ==> EX i. ALL k. f (i+k) = f i";
-by (dres_inst_tac [("x","0")] (lemma RS spec) 1);
-by Auto_tac;
-qed "wf_weak_decr_stable";
-
-(* special case: <= *)
-
-Goal "(m, n) : pred_nat^* = (m <= n)";
-by (simp_tac (simpset() addsimps [less_eq, reflcl_trancl RS sym] 
-                        delsimps [reflcl_trancl]) 1);
-by (arith_tac 1);
-qed "le_eq";
-
-Goal "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i";
-by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1);
-by (asm_simp_tac (simpset() addsimps [le_eq]) 1);
-by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1));
-qed "weak_decr_stable";
-
-(*----------------------------------------------------------------------------
- * Wellfoundedness of same_fst
- *---------------------------------------------------------------------------*)
-
-val prems = goalw thy [same_fst_def]
-  "(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)";
-by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);
-by(strip_tac 1);
-by(rename_tac "a b" 1);
-by(case_tac "wf(R a)" 1);
- by (eres_inst_tac [("a","b")] wf_induct 1);
- by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs prems) 1);
-qed "wf_same_fstI";
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/WF_Rel.thy
--- a/src/HOL/WF_Rel.thy	Thu Oct 12 18:38:23 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(*  Title:      HOL/WF_Rel
-    ID:         $Id$
-    Author:     Konrad Slind
-    Copyright   1995 TU Munich
-
-Derived WF relations: inverse image, lexicographic product, measure, ...
-
-The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a
-subset of the lexicographic product, and therefore does not need to be defined
-separately.
-*)
-
-WF_Rel = Finite +
-
-(* actually belongs to theory Finite *)
-instance unit :: finite                  (finite_unit)
-instance "*" :: (finite,finite) finite   (finite_Prod)
-
-
-constdefs
- less_than :: "(nat*nat)set"
-"less_than == trancl pred_nat"
-
- inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
-"inv_image r f == {(x,y). (f(x), f(y)) : r}"
-
- measure   :: "('a => nat) => ('a * 'a)set"
-"measure == inv_image less_than"
-
- lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
-               (infixr "<*lex*>" 80)
-"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
-
- (* finite proper subset*)
- finite_psubset  :: "('a set * 'a set) set"
-"finite_psubset == {(A,B). A < B & finite B}"
-
-(* For rec_defs where the first n parameters stay unchanged in the recursive
-   call. See While for an application.
-*)
- same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
-"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
-
-end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Wellfounded_Recursion.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Wellfounded_Recursion.ML	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,370 @@
+(*  Title:      HOL/Wellfounded_Recursion.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow, with minor changes by Konrad Slind
+    Copyright   1992  University of Cambridge/1995 TU Munich
+
+Wellfoundedness, induction, and  recursion
+*)
+
+Goal "x = y ==> H x z = H y z";
+by (Asm_simp_tac 1);
+val H_cong2 = (*freeze H!*)
+	      read_instantiate [("H","H")] (result());
+
+val [prem] = Goalw [wf_def]
+ "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)";
+by (Clarify_tac 1);
+by (rtac prem 1);
+by (assume_tac 1);
+qed "wfUNIVI";
+
+(*Restriction to domain A.  If r is well-founded over A then wf(r)*)
+val [prem1,prem2] = Goalw [wf_def]
+ "[| r <= A <*> A;  \
+\    !!x P. [| ALL x. (ALL y. (y,x) : r --> P y) --> P x;  x:A |] ==> P x |]  \
+\ ==>  wf r";
+by (cut_facts_tac [prem1] 1);
+by (blast_tac (claset() addIs [prem2]) 1);
+qed "wfI";
+
+val major::prems = Goalw [wf_def]
+    "[| wf(r);          \
+\       !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x) \
+\    |]  ==>  P(a)";
+by (rtac (major RS spec RS mp RS spec) 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "wf_induct";
+
+(*Perform induction on i, then prove the wf(r) subgoal using prems. *)
+fun wf_ind_tac a prems i = 
+    EVERY [res_inst_tac [("a",a)] wf_induct i,
+           rename_last_tac a ["1"] (i+1),
+           ares_tac prems i];
+
+Goal "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r";
+by (wf_ind_tac "a" [] 1);
+by (Blast_tac 1);
+qed_spec_mp "wf_not_sym";
+
+(* [| wf r;  ~Z ==> (a,x) : r;  (x,a) ~: r ==> Z |] ==> Z *)
+bind_thm ("wf_asym", cla_make_elim wf_not_sym);
+
+Goal "wf(r) ==> (a,a) ~: r";
+by (blast_tac (claset() addEs [wf_asym]) 1);
+qed "wf_not_refl";
+
+(* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
+bind_thm ("wf_irrefl", make_elim wf_not_refl);
+
+(*transitive closure of a wf relation is wf! *)
+Goal "wf(r) ==> wf(r^+)";
+by (stac wf_def 1);
+by (Clarify_tac 1);
+(*must retain the universal formula for later use!*)
+by (rtac allE 1 THEN assume_tac 1);
+by (etac mp 1);
+by (eres_inst_tac [("a","x")] wf_induct 1);
+by (blast_tac (claset() addEs [tranclE]) 1);
+qed "wf_trancl";
+
+Goal "wf (r^-1) ==> wf ((r^+)^-1)";
+by (stac (trancl_converse RS sym) 1);
+by (etac wf_trancl 1);
+qed "wf_converse_trancl";
+
+
+(*----------------------------------------------------------------------------
+ * Minimal-element characterization of well-foundedness
+ *---------------------------------------------------------------------------*)
+
+Goalw [wf_def] "wf r ==> x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q)";
+by (dtac spec 1);
+by (etac (mp RS spec) 1);
+by (Blast_tac 1);
+val lemma1 = result();
+
+Goalw [wf_def] "(ALL Q x. x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q)) ==> wf r";
+by (Clarify_tac 1);
+by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1);
+by (Blast_tac 1);
+val lemma2 = result();
+
+Goal "wf r = (ALL Q x. x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q))";
+by (blast_tac (claset() addSIs [lemma1, lemma2]) 1);
+qed "wf_eq_minimal";
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of subsets
+ *---------------------------------------------------------------------------*)
+
+Goal "[| wf(r);  p<=r |] ==> wf(p)";
+by (full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
+by (Fast_tac 1);
+qed "wf_subset";
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of the empty relation.
+ *---------------------------------------------------------------------------*)
+
+Goal "wf({})";
+by (simp_tac (simpset() addsimps [wf_def]) 1);
+qed "wf_empty";
+AddIffs [wf_empty];
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of `insert'
+ *---------------------------------------------------------------------------*)
+
+Goal "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
+by (rtac iffI 1);
+ by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] 
+	addIs [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
+by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
+by Safe_tac;
+by (EVERY1[rtac allE, assume_tac, etac impE, Blast_tac]);
+by (etac bexE 1);
+by (rename_tac "a" 1);
+by (case_tac "a = x" 1);
+ by (res_inst_tac [("x","a")]bexI 2);
+  by (assume_tac 3);
+ by (Blast_tac 2);
+by (case_tac "y:Q" 1);
+ by (Blast_tac 2);
+by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1);
+ by (assume_tac 1);
+by (thin_tac "ALL Q. (EX x. x : Q) --> ?P Q" 1);	(*essential for speed*)
+(*Blast_tac with new substOccur fails*)
+by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
+qed "wf_insert";
+AddIffs [wf_insert];
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of `disjoint union'
+ *---------------------------------------------------------------------------*)
+
+(*Intuition behind this proof for the case of binary union:
+
+  Goal: find an (R u S)-min element of a nonempty subset A.
+  by case distinction:
+  1. There is a step a -R-> b with a,b : A.
+     Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.
+     By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the
+     subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot
+     have an S-successor and is thus S-min in A as well.
+  2. There is no such step.
+     Pick an S-min element of A. In this case it must be an R-min
+     element of A as well.
+
+*)
+
+Goal "[| ALL i:I. wf(r i); \
+\        ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
+\                                         Domain(r j) Int Range(r i) = {} \
+\     |] ==> wf(UN i:I. r i)";
+by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
+by (Clarify_tac 1);
+by (rename_tac "A a" 1);
+by (case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i" 1);
+ by (Asm_full_simp_tac 2);
+ by (Best_tac 2);  (*much faster than Blast_tac*)
+by (Clarify_tac 1);
+by (EVERY1[dtac bspec, assume_tac,
+	   eres_inst_tac [("x","{a. a:A & (EX b:A. (b,a) : r i)}")] allE]);
+by (EVERY1[etac allE, etac impE]);
+ by (ALLGOALS Blast_tac);
+qed "wf_UN";
+
+Goalw [Union_def]
+ "[| ALL r:R. wf r; \
+\    ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {} & \
+\                                 Domain s Int Range r = {} \
+\ |] ==> wf(Union R)";
+by (blast_tac (claset() addIs [wf_UN]) 1);
+qed "wf_Union";
+
+Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
+\     |] ==> wf(r Un s)";
+by (rtac (simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
+qed "wf_Un";
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of `image'
+ *---------------------------------------------------------------------------*)
+
+Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)";
+by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
+by (Clarify_tac 1);
+by (case_tac "EX p. f p : Q" 1);
+by (eres_inst_tac [("x","{p. f p : Q}")]allE 1);
+by (fast_tac (claset() addDs [injD]) 1);
+by (Blast_tac 1);
+qed "wf_prod_fun_image";
+
+(*** acyclic ***)
+
+Goalw [acyclic_def] "ALL x. (x, x) ~: r^+ ==> acyclic r";
+by (assume_tac 1);
+qed "acyclicI";
+
+Goalw [acyclic_def] "wf r ==> acyclic r";
+by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1);
+qed "wf_acyclic";
+
+Goalw [acyclic_def] "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
+by (simp_tac (simpset() addsimps [trancl_insert]) 1);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
+qed "acyclic_insert";
+AddIffs [acyclic_insert];
+
+Goalw [acyclic_def] "acyclic(r^-1) = acyclic r";
+by (simp_tac (simpset() addsimps [trancl_converse]) 1);
+qed "acyclic_converse";
+AddIffs [acyclic_converse];
+
+Goalw [acyclic_def,antisym_def] "acyclic r ==> antisym(r^*)";
+by(blast_tac (claset() addEs [rtranclE]
+     addIs [rtrancl_into_trancl1,rtrancl_trancl_trancl]) 1);
+qed "acyclic_impl_antisym_rtrancl";
+
+(* Other direction:
+acyclic = no loops
+antisym = only self loops
+Goalw [acyclic_def,antisym_def] "antisym(r^* ) ==> acyclic(r - Id)";
+==> "antisym(r^* ) = acyclic(r - Id)";
+*)
+
+Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r";
+by (blast_tac (claset() addIs [trancl_mono]) 1);
+qed "acyclic_subset";
+
+(** cut **)
+
+(*This rewrite rule works upon formulae; thus it requires explicit use of
+  H_cong to expose the equality*)
+Goalw [cut_def] "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))";
+by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1);
+qed "cuts_eq";
+
+Goalw [cut_def] "(x,a):r ==> (cut f r a)(x) = f(x)";
+by (asm_simp_tac HOL_ss 1);
+qed "cut_apply";
+
+(*** is_recfun ***)
+
+Goalw [is_recfun_def,cut_def]
+    "[| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = arbitrary";
+by (etac ssubst 1);
+by (asm_simp_tac HOL_ss 1);
+qed "is_recfun_undef";
+
+(*** NOTE! some simplifications need a different Solver!! ***)
+fun indhyp_tac hyps =
+    (cut_facts_tac hyps THEN'
+       DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
+                        eresolve_tac [transD, mp, allE]));
+val wf_super_ss = HOL_ss addSolver (mk_solver "WF" indhyp_tac);
+
+Goalw [is_recfun_def,cut_def]
+    "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \
+    \ (x,a):r --> (x,b):r --> f(x)=g(x)";
+by (etac wf_induct 1);
+by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
+by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
+qed_spec_mp "is_recfun_equal";
+
+
+val prems as [wfr,transr,recfa,recgb,_] = goalw (the_context ()) [cut_def]
+    "[| wf(r);  trans(r); \
+\       is_recfun r H a f;  is_recfun r H b g;  (b,a):r |] ==> \
+\    cut f r b = g";
+val gundef = recgb RS is_recfun_undef
+and fisg   = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
+by (cut_facts_tac prems 1);
+by (rtac ext 1);
+by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]) 1);
+qed "is_recfun_cut";
+
+(*** Main Existence Lemma -- Basic Properties of the_recfun ***)
+
+Goalw [the_recfun_def]
+    "is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)";
+by (eres_inst_tac [("P", "is_recfun r H a")] someI 1);
+qed "is_the_recfun";
+
+Goal "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
+by (wf_ind_tac "a" [] 1);
+by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
+                 is_the_recfun 1);
+by (rewtac is_recfun_def);
+by (stac cuts_eq 1);
+by (Clarify_tac 1);
+by (rtac H_cong2 1);
+by (subgoal_tac
+         "the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1);
+ by (Blast_tac 2);
+by (etac ssubst 1);
+by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
+by (Clarify_tac 1);
+by (stac cut_apply 1);
+ by (fast_tac (claset() addDs [transD]) 1);
+by (fold_tac [is_recfun_def]);
+by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1);
+qed "unfold_the_recfun";
+
+Goal "[| wf r; trans r; (x,a) : r; (x,b) : r |] \
+\     ==> the_recfun r H a x = the_recfun r H b x";
+by (best_tac (claset() addIs [is_recfun_equal, unfold_the_recfun]) 1);
+qed "the_recfun_equal";
+
+(** Removal of the premise trans(r) **)
+val th = rewrite_rule[is_recfun_def]
+                     (trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun)));
+
+Goalw [wfrec_def]
+    "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
+by (rtac H_cong2 1);
+by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
+by (rtac allI 1);
+by (rtac impI 1);
+by (res_inst_tac [("a1","a")] (th RS ssubst) 1);
+by (assume_tac 1);
+by (ftac wf_trancl 1);
+by (ftac r_into_trancl 1);
+by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1);
+by (rtac H_cong2 1);    (*expose the equality of cuts*)
+by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1);
+by (blast_tac (claset() addIs [the_recfun_equal, transD, trans_trancl, 
+			       r_into_trancl]) 1);
+qed "wfrec";
+
+(*---------------------------------------------------------------------------
+ * This form avoids giant explosions in proofs.  NOTE USE OF == 
+ *---------------------------------------------------------------------------*)
+Goal "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a";
+by Auto_tac;
+by (blast_tac (claset() addIs [wfrec]) 1);   
+qed "def_wfrec";
+
+
+(**** TFL variants ****)
+
+Goal "ALL R. wf R --> \
+\      (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))";
+by (Clarify_tac 1);
+by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1);
+by (assume_tac 1);
+by (Blast_tac 1);
+qed"tfl_wf_induct";
+
+Goal "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)";
+by (Clarify_tac 1);
+by (rtac cut_apply 1);
+by (assume_tac 1);
+qed"tfl_cut_apply";
+
+Goal "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)";
+by (Clarify_tac 1);
+by (etac wfrec 1);
+qed "tfl_wfrec";
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Wellfounded_Recursion.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Wellfounded_Recursion.thy	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,31 @@
+(*  Title:      HOL/Wellfounded_Recursion.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1992  University of Cambridge
+
+Well-founded Recursion
+*)
+
+Wellfounded_Recursion = Transitive_Closure +
+
+constdefs
+  wf         :: "('a * 'a)set => bool"
+  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
+
+  acyclic :: "('a*'a)set => bool"
+  "acyclic r == !x. (x,x) ~: r^+"
+
+  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
+  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
+
+  is_recfun  :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) =>'a=>('a=>'b) => bool"
+  "is_recfun r H a f == (f = cut (%x. H (cut f r x) x) r a)"
+
+  the_recfun :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'a => 'b"
+  "the_recfun r H a  == (@f. is_recfun r H a f)"
+
+  wfrec      :: "('a * 'a)set => (('a=>'b) => ('a=>'b)) => 'a => 'b"
+  "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
+                            r x)  x)"
+
+end
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Wellfounded_Relations.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Wellfounded_Relations.ML	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,226 @@
+(*  Title: 	HOL/Wellfounded_Relations
+    ID:         $Id$
+    Author: 	Konrad Slind
+    Copyright   1996  TU Munich
+
+Derived WF relations: inverse image, lexicographic product, measure, ...
+*)
+
+
+(*----------------------------------------------------------------------------
+ * "Less than" on the natural numbers
+ *---------------------------------------------------------------------------*)
+
+Goalw [less_than_def] "wf less_than"; 
+by (rtac (wf_pred_nat RS wf_trancl) 1);
+qed "wf_less_than";
+AddIffs [wf_less_than];
+
+Goalw [less_than_def] "trans less_than"; 
+by (rtac trans_trancl 1);
+qed "trans_less_than";
+AddIffs [trans_less_than];
+
+Goalw [less_than_def, less_def] "((x,y): less_than) = (x<y)"; 
+by (Simp_tac 1);
+qed "less_than_iff";
+AddIffs [less_than_iff];
+
+Goal "(!!n. (ALL m. Suc m <= n --> P m) ==> P n) ==> P n";
+by (rtac (wf_less_than RS wf_induct) 1);
+by (resolve_tac (premises()) 1);
+by Auto_tac;
+qed_spec_mp "full_nat_induct";
+
+(*----------------------------------------------------------------------------
+ * The inverse image into a wellfounded relation is wellfounded.
+ *---------------------------------------------------------------------------*)
+
+Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
+by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1);
+by (Clarify_tac 1);
+by (subgoal_tac "EX (w::'b). w : {w. EX (x::'a). x: Q & (f x = w)}" 1);
+by (blast_tac (claset() delrules [allE]) 2);
+by (etac allE 1);
+by (mp_tac 1);
+by (Blast_tac 1);
+qed "wf_inv_image";
+AddSIs [wf_inv_image];
+
+Goalw [trans_def,inv_image_def]
+    "!!r. trans r ==> trans (inv_image r f)";
+by (Simp_tac 1);
+by (Blast_tac 1);
+qed "trans_inv_image";
+
+
+(*----------------------------------------------------------------------------
+ * All measures are wellfounded.
+ *---------------------------------------------------------------------------*)
+
+Goalw [measure_def] "wf (measure f)";
+by (rtac (wf_less_than RS wf_inv_image) 1);
+qed "wf_measure";
+AddIffs [wf_measure];
+
+val measure_induct = standard
+    (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
+      (wf_measure RS wf_induct));
+bind_thm ("measure_induct", measure_induct);
+
+(*----------------------------------------------------------------------------
+ * Wellfoundedness of lexicographic combinations
+ *---------------------------------------------------------------------------*)
+
+val [wfa,wfb] = goalw (the_context ()) [wf_def,lex_prod_def]
+ "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)";
+by (EVERY1 [rtac allI,rtac impI]);
+by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
+by (rtac (wfa RS spec RS mp) 1);
+by (EVERY1 [rtac allI,rtac impI]);
+by (rtac (wfb RS spec RS mp) 1);
+by (Blast_tac 1);
+qed "wf_lex_prod";
+AddSIs [wf_lex_prod];
+
+(*---------------------------------------------------------------------------
+ * Transitivity of WF combinators.
+ *---------------------------------------------------------------------------*)
+Goalw [trans_def, lex_prod_def]
+    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)";
+by (Simp_tac 1);
+by (Blast_tac 1);
+qed "trans_lex_prod";
+AddSIs [trans_lex_prod];
+
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of proper subset on finite sets.
+ *---------------------------------------------------------------------------*)
+Goalw [finite_psubset_def] "wf(finite_psubset)";
+by (rtac (wf_measure RS wf_subset) 1);
+by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def,
+				 symmetric less_def])1);
+by (fast_tac (claset() addSEs [psubset_card_mono]) 1);
+qed "wf_finite_psubset";
+
+Goalw [finite_psubset_def, trans_def] "trans finite_psubset";
+by (simp_tac (simpset() addsimps [psubset_def]) 1);
+by (Blast_tac 1);
+qed "trans_finite_psubset";
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of finite acyclic relations
+ * Cannot go into WF because it needs Finite.
+ *---------------------------------------------------------------------------*)
+
+Goal "finite r ==> acyclic r --> wf r";
+by (etac finite_induct 1);
+ by (Blast_tac 1);
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
+qed_spec_mp "finite_acyclic_wf";
+
+Goal "[|finite r; acyclic r|] ==> wf (r^-1)";
+by (etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1);
+by (etac (acyclic_converse RS iffD2) 1);
+qed "finite_acyclic_wf_converse";
+
+Goal "finite r ==> wf r = acyclic r";
+by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
+qed "wf_iff_acyclic_if_finite";
+
+
+(*---------------------------------------------------------------------------
+ * A relation is wellfounded iff it has no infinite descending chain
+ * Cannot go into WF because it needs type nat.
+ *---------------------------------------------------------------------------*)
+
+Goalw [wf_eq_minimal RS eq_reflection]
+  "wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))";
+by (rtac iffI 1);
+ by (rtac notI 1);
+ by (etac exE 1);
+ by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
+ by (Blast_tac 1);
+by (etac swap 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
+ by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
+ by (rtac allI 1);
+ by (Simp_tac 1);
+ by (rtac someI2_ex 1);
+  by (Blast_tac 1);
+ by (Blast_tac 1);
+by (rtac allI 1);
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+by (Simp_tac 1);
+by (rtac someI2_ex 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
+qed "wf_iff_no_infinite_down_chain";
+
+(*----------------------------------------------------------------------------
+ * Weakly decreasing sequences (w.r.t. some well-founded order) stabilize.
+ *---------------------------------------------------------------------------*)
+
+Goal "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*";
+by (induct_tac "k" 1);
+ by (ALLGOALS Simp_tac);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
+val lemma = result();
+
+Goal "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] \
+\     ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))";
+by (etac wf_induct 1);
+by (Clarify_tac 1);
+by (case_tac "EX j. (f (m+j), f m) : r^+" 1);
+ by (Clarify_tac 1);
+ by (subgoal_tac "EX i. ALL k. f ((m+j)+i+k) = f ((m+j)+i)" 1);
+  by (Clarify_tac 1);
+  by (res_inst_tac [("x","j+i")] exI 1);
+  by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
+ by (Blast_tac 1);
+by (res_inst_tac [("x","0")] exI 1);
+by (Clarsimp_tac 1);
+by (dres_inst_tac [("i","m"), ("k","k")] lemma 1);
+by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
+val lemma = result();
+
+Goal "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] \
+\     ==> EX i. ALL k. f (i+k) = f i";
+by (dres_inst_tac [("x","0")] (lemma RS spec) 1);
+by Auto_tac;
+qed "wf_weak_decr_stable";
+
+(* special case: <= *)
+
+Goal "(m, n) : pred_nat^* = (m <= n)";
+by (simp_tac (simpset() addsimps [less_eq, reflcl_trancl RS sym] 
+                        delsimps [reflcl_trancl]) 1);
+by (arith_tac 1);
+qed "le_eq";
+
+Goal "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i";
+by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1);
+by (asm_simp_tac (simpset() addsimps [le_eq]) 1);
+by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1));
+qed "weak_decr_stable";
+
+(*----------------------------------------------------------------------------
+ * Wellfoundedness of same_fst
+ *---------------------------------------------------------------------------*)
+
+val prems = goalw thy [same_fst_def]
+  "(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)";
+by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);
+by(strip_tac 1);
+by(rename_tac "a b" 1);
+by(case_tac "wf(R a)" 1);
+ by (eres_inst_tac [("a","b")] wf_induct 1);
+ by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs prems) 1);
+qed "wf_same_fstI";
diff -r 33fe2d701ddd -r 01c2744a3786 src/HOL/Wellfounded_Relations.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Wellfounded_Relations.thy	Thu Oct 12 18:44:35 2000 +0200
@@ -0,0 +1,44 @@
+(*  Title:      HOL/Wellfounded_Relations
+    ID:         $Id$
+    Author:     Konrad Slind
+    Copyright   1995 TU Munich
+
+Derived WF relations: inverse image, lexicographic product, measure, ...
+
+The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a
+subset of the lexicographic product, and therefore does not need to be defined
+separately.
+*)
+
+Wellfounded_Relations = Finite +
+
+(* actually belongs to theory Finite *)
+instance unit :: finite                  (finite_unit)
+instance "*" :: (finite,finite) finite   (finite_Prod)
+
+
+constdefs
+ less_than :: "(nat*nat)set"
+"less_than == trancl pred_nat"
+
+ inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
+"inv_image r f == {(x,y). (f(x), f(y)) : r}"
+
+ measure   :: "('a => nat) => ('a * 'a)set"
+"measure == inv_image less_than"
+
+ lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
+               (infixr "<*lex*>" 80)
+"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
+
+ (* finite proper subset*)
+ finite_psubset  :: "('a set * 'a set) set"
+"finite_psubset == {(A,B). A < B & finite B}"
+
+(* For rec_defs where the first n parameters stay unchanged in the recursive
+   call. See While for an application.
+*)
+ same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
+"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
+
+end