--- 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];
-
--- 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
--- /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];
+
--- /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
--- /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];
--- /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
--- /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";
--- /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
--- 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;
--- 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"))];
--- /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;
--- /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"))];
--- 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";
-
-
-
-
--- 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
--- /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";
+
+
+
+
--- /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
--- 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
--- /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";
--- /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
--- 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";
-
--- 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
--- /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";
+
--- /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
--- 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];
--- 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
--- 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";
--- 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
--- 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";
--- 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
--- 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";
--- 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
--- /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";
--- /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
--- /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";
--- /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