--- a/src/ZF/Bool.ML Fri Jun 21 18:40:06 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-(* Title: ZF/bool
- ID: $Id$
- Author: Martin D Coen, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
-
-Booleans in Zermelo-Fraenkel Set Theory
-*)
-
-bind_thms ("bool_defs", [bool_def,cond_def]);
-
-Goalw [succ_def] "{0} = 1";
-by (rtac refl 1);
-qed "singleton_0";
-
-(* Introduction rules *)
-
-Goalw bool_defs "1 : bool";
-by (rtac (consI1 RS consI2) 1);
-qed "bool_1I";
-
-Goalw bool_defs "0 : bool";
-by (rtac consI1 1);
-qed "bool_0I";
-
-Addsimps [bool_1I, bool_0I];
-AddTCs [bool_1I, bool_0I];
-
-Goalw bool_defs "1~=0";
-by (rtac succ_not_0 1);
-qed "one_not_0";
-
-(** 1=0 ==> R **)
-bind_thm ("one_neq_0", one_not_0 RS notE);
-
-val major::prems = Goalw bool_defs
- "[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P";
-by (rtac (major RS consE) 1);
-by (REPEAT (eresolve_tac (singletonE::prems) 1));
-qed "boolE";
-
-(** cond **)
-
-(*1 means true*)
-Goalw bool_defs "cond(1,c,d) = c";
-by (rtac (refl RS if_P) 1);
-qed "cond_1";
-
-(*0 means false*)
-Goalw bool_defs "cond(0,c,d) = d";
-by (rtac (succ_not_0 RS not_sym RS if_not_P) 1);
-qed "cond_0";
-
-Addsimps [cond_1, cond_0];
-
-fun bool_tac i = fast_tac (claset() addSEs [boolE] addss (simpset())) i;
-
-
-Goal "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)";
-by (bool_tac 1);
-qed "cond_type";
-AddTCs [cond_type];
-
-(*For Simp_tac and Blast_tac*)
-Goal "[| b: bool; c: A; d: A |] ==> cond(b,c,d): A";
-by (bool_tac 1);
-qed "cond_simple_type";
-
-val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
-by (rewtac rew);
-by (rtac cond_1 1);
-qed "def_cond_1";
-
-val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
-by (rewtac rew);
-by (rtac cond_0 1);
-qed "def_cond_0";
-
-fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)];
-
-val [not_1, not_0] = conds not_def;
-val [and_1, and_0] = conds and_def;
-val [or_1, or_0] = conds or_def;
-val [xor_1, xor_0] = conds xor_def;
-
-bind_thm ("not_1", not_1);
-bind_thm ("not_0", not_0);
-bind_thm ("and_1", and_1);
-bind_thm ("and_0", and_0);
-bind_thm ("or_1", or_1);
-bind_thm ("or_0", or_0);
-bind_thm ("xor_1", xor_1);
-bind_thm ("xor_0", xor_0);
-
-Addsimps [not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
-
-Goalw [not_def] "a:bool ==> not(a) : bool";
-by (Asm_simp_tac 1);
-qed "not_type";
-
-Goalw [and_def] "[| a:bool; b:bool |] ==> a and b : bool";
-by (Asm_simp_tac 1);
-qed "and_type";
-
-Goalw [or_def] "[| a:bool; b:bool |] ==> a or b : bool";
-by (Asm_simp_tac 1);
-qed "or_type";
-
-AddTCs [not_type, and_type, or_type];
-
-Goalw [xor_def] "[| a:bool; b:bool |] ==> a xor b : bool";
-by (Asm_simp_tac 1);
-qed "xor_type";
-
-AddTCs [xor_type];
-
-bind_thms ("bool_typechecks",
- [bool_1I, bool_0I, cond_type, not_type, and_type, or_type, xor_type]);
-
-(*** Laws for 'not' ***)
-
-Goal "a:bool ==> not(not(a)) = a";
-by (bool_tac 1);
-qed "not_not";
-
-Goal "a:bool ==> not(a and b) = not(a) or not(b)";
-by (bool_tac 1);
-qed "not_and";
-
-Goal "a:bool ==> not(a or b) = not(a) and not(b)";
-by (bool_tac 1);
-qed "not_or";
-
-Addsimps [not_not, not_and, not_or];
-
-(*** Laws about 'and' ***)
-
-Goal "a: bool ==> a and a = a";
-by (bool_tac 1);
-qed "and_absorb";
-
-Addsimps [and_absorb];
-
-Goal "[| a: bool; b:bool |] ==> a and b = b and a";
-by (bool_tac 1);
-qed "and_commute";
-
-Goal "a: bool ==> (a and b) and c = a and (b and c)";
-by (bool_tac 1);
-qed "and_assoc";
-
-Goal "[| a: bool; b:bool; c:bool |] ==> \
-\ (a or b) and c = (a and c) or (b and c)";
-by (bool_tac 1);
-qed "and_or_distrib";
-
-(** binary orion **)
-
-Goal "a: bool ==> a or a = a";
-by (bool_tac 1);
-qed "or_absorb";
-
-Addsimps [or_absorb];
-
-Goal "[| a: bool; b:bool |] ==> a or b = b or a";
-by (bool_tac 1);
-qed "or_commute";
-
-Goal "a: bool ==> (a or b) or c = a or (b or c)";
-by (bool_tac 1);
-qed "or_assoc";
-
-Goal "[| a: bool; b: bool; c: bool |] ==> \
-\ (a and b) or c = (a or c) and (b or c)";
-by (bool_tac 1);
-qed "or_and_distrib";
-
--- a/src/ZF/Bool.thy Fri Jun 21 18:40:06 2002 +0200
+++ b/src/ZF/Bool.thy Sat Jun 22 18:28:46 2002 +0200
@@ -8,14 +8,7 @@
2 is equal to bool, but serves a different purpose
*)
-Bool = pair +
-consts
- bool :: i
- cond :: "[i,i,i]=>i"
- not :: "i=>i"
- "and" :: "[i,i]=>i" (infixl 70)
- or :: "[i,i]=>i" (infixl 65)
- xor :: "[i,i]=>i" (infixl 65)
+theory Bool = pair:
syntax
"1" :: i ("1")
@@ -25,11 +18,181 @@
"1" == "succ(0)"
"2" == "succ(1)"
-defs
- bool_def "bool == {0,1}"
- cond_def "cond(b,c,d) == if(b=1,c,d)"
- not_def "not(b) == cond(b,0,1)"
- and_def "a and b == cond(a,b,0)"
- or_def "a or b == cond(a,1,b)"
- xor_def "a xor b == cond(a,not(b),b)"
+constdefs
+ bool :: i
+ "bool == {0,1}"
+
+ cond :: "[i,i,i]=>i"
+ "cond(b,c,d) == if(b=1,c,d)"
+
+ not :: "i=>i"
+ "not(b) == cond(b,0,1)"
+
+ "and" :: "[i,i]=>i" (infixl "and" 70)
+ "a and b == cond(a,b,0)"
+
+ or :: "[i,i]=>i" (infixl "or" 65)
+ "a or b == cond(a,1,b)"
+
+ xor :: "[i,i]=>i" (infixl "xor" 65)
+ "a xor b == cond(a,not(b),b)"
+
+
+lemmas bool_defs = bool_def cond_def
+
+lemma singleton_0: "{0} = 1"
+by (simp add: succ_def)
+
+(* Introduction rules *)
+
+lemma bool_1I [simp,TC]: "1 : bool"
+by (simp add: bool_defs )
+
+lemma bool_0I [simp,TC]: "0 : bool"
+by (simp add: bool_defs)
+
+lemma one_not_0: "1~=0"
+by (simp add: bool_defs )
+
+(** 1=0 ==> R **)
+lemmas one_neq_0 = one_not_0 [THEN notE, standard]
+
+lemma boolE:
+ "[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P"
+by (simp add: bool_defs, blast)
+
+(** cond **)
+
+(*1 means true*)
+lemma cond_1 [simp]: "cond(1,c,d) = c"
+by (simp add: bool_defs )
+
+(*0 means false*)
+lemma cond_0 [simp]: "cond(0,c,d) = d"
+by (simp add: bool_defs )
+
+lemma cond_type [TC]: "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)"
+by (simp add: bool_defs , blast)
+
+(*For Simp_tac and Blast_tac*)
+lemma cond_simple_type: "[| b: bool; c: A; d: A |] ==> cond(b,c,d): A"
+by (simp add: bool_defs )
+
+lemma def_cond_1: "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c"
+by simp
+
+lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d"
+by simp
+
+lemmas not_1 = not_def [THEN def_cond_1, standard, simp]
+lemmas not_0 = not_def [THEN def_cond_0, standard, simp]
+
+lemmas and_1 = and_def [THEN def_cond_1, standard, simp]
+lemmas and_0 = and_def [THEN def_cond_0, standard, simp]
+
+lemmas or_1 = or_def [THEN def_cond_1, standard, simp]
+lemmas or_0 = or_def [THEN def_cond_0, standard, simp]
+
+lemmas xor_1 = xor_def [THEN def_cond_1, standard, simp]
+lemmas xor_0 = xor_def [THEN def_cond_0, standard, simp]
+
+lemma not_type [TC]: "a:bool ==> not(a) : bool"
+by (simp add: not_def)
+
+lemma and_type [TC]: "[| a:bool; b:bool |] ==> a and b : bool"
+by (simp add: and_def)
+
+lemma or_type [TC]: "[| a:bool; b:bool |] ==> a or b : bool"
+by (simp add: or_def)
+
+lemma xor_type [TC]: "[| a:bool; b:bool |] ==> a xor b : bool"
+by (simp add: xor_def)
+
+lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type
+ or_type xor_type
+
+(*** Laws for 'not' ***)
+
+lemma not_not [simp]: "a:bool ==> not(not(a)) = a"
+by (elim boolE, auto)
+
+lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)"
+by (elim boolE, auto)
+
+lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)"
+by (elim boolE, auto)
+
+(*** Laws about 'and' ***)
+
+lemma and_absorb [simp]: "a: bool ==> a and a = a"
+by (elim boolE, auto)
+
+lemma and_commute: "[| a: bool; b:bool |] ==> a and b = b and a"
+by (elim boolE, auto)
+
+lemma and_assoc: "a: bool ==> (a and b) and c = a and (b and c)"
+by (elim boolE, auto)
+
+lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==>
+ (a or b) and c = (a and c) or (b and c)"
+by (elim boolE, auto)
+
+(** binary orion **)
+
+lemma or_absorb [simp]: "a: bool ==> a or a = a"
+by (elim boolE, auto)
+
+lemma or_commute: "[| a: bool; b:bool |] ==> a or b = b or a"
+by (elim boolE, auto)
+
+lemma or_assoc: "a: bool ==> (a or b) or c = a or (b or c)"
+by (elim boolE, auto)
+
+lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==>
+ (a and b) or c = (a or c) and (b or c)"
+by (elim boolE, auto)
+
+ML
+{*
+val bool_def = thm "bool_def";
+
+val bool_defs = thms "bool_defs";
+val singleton_0 = thm "singleton_0";
+val bool_1I = thm "bool_1I";
+val bool_0I = thm "bool_0I";
+val one_not_0 = thm "one_not_0";
+val one_neq_0 = thm "one_neq_0";
+val boolE = thm "boolE";
+val cond_1 = thm "cond_1";
+val cond_0 = thm "cond_0";
+val cond_type = thm "cond_type";
+val cond_simple_type = thm "cond_simple_type";
+val def_cond_1 = thm "def_cond_1";
+val def_cond_0 = thm "def_cond_0";
+val not_1 = thm "not_1";
+val not_0 = thm "not_0";
+val and_1 = thm "and_1";
+val and_0 = thm "and_0";
+val or_1 = thm "or_1";
+val or_0 = thm "or_0";
+val xor_1 = thm "xor_1";
+val xor_0 = thm "xor_0";
+val not_type = thm "not_type";
+val and_type = thm "and_type";
+val or_type = thm "or_type";
+val xor_type = thm "xor_type";
+val bool_typechecks = thms "bool_typechecks";
+val not_not = thm "not_not";
+val not_and = thm "not_and";
+val not_or = thm "not_or";
+val and_absorb = thm "and_absorb";
+val and_commute = thm "and_commute";
+val and_assoc = thm "and_assoc";
+val and_or_distrib = thm "and_or_distrib";
+val or_absorb = thm "or_absorb";
+val or_commute = thm "or_commute";
+val or_assoc = thm "or_assoc";
+val or_and_distrib = thm "or_and_distrib";
+*}
+
end
--- a/src/ZF/Integ/EquivClass.thy Fri Jun 21 18:40:06 2002 +0200
+++ b/src/ZF/Integ/EquivClass.thy Sat Jun 22 18:28:46 2002 +0200
@@ -6,7 +6,7 @@
Equivalence relations in Zermelo-Fraenkel Set Theory
*)
-EquivClass = Rel + Perm +
+EquivClass = Trancl + Perm +
constdefs
--- a/src/ZF/IsaMakefile Fri Jun 21 18:40:06 2002 +0200
+++ b/src/ZF/IsaMakefile Sat Jun 22 18:28:46 2002 +0200
@@ -29,7 +29,7 @@
@cd $(SRC)/FOL; $(ISATOOL) make FOL
$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.ML \
- ArithSimp.thy Bool.ML Bool.thy Cardinal.thy \
+ ArithSimp.thy Bool.thy Cardinal.thy \
CardinalArith.thy Cardinal_AC.thy \
Datatype.ML Datatype.thy Epsilon.thy Finite.thy \
Fixedpt.thy Inductive.ML Inductive.thy \
@@ -39,11 +39,11 @@
Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy \
Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy \
OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy \
- QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML \
+ QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Sum.ML \
Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \
Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \
Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \
- Trancl.ML Trancl.thy Univ.thy Update.thy \
+ Trancl.thy Univ.thy Update.thy \
WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy \
ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML \
subset.ML subset.thy thy_syntax.ML upair.ML upair.thy
--- a/src/ZF/Rel.ML Fri Jun 21 18:40:06 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-(* Title: ZF/Rel.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Relations in Zermelo-Fraenkel Set Theory
-*)
-
-(*** Some properties of relations -- useful? ***)
-
-(* irreflexivity *)
-
-val prems = Goalw [irrefl_def]
- "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)";
-by (REPEAT (ares_tac (prems @ [ballI]) 1));
-qed "irreflI";
-
-Goalw [irrefl_def] "[| irrefl(A,r); x:A |] ==> <x,x> ~: r";
-by (Blast_tac 1);
-qed "irreflE";
-
-(* symmetry *)
-
-val prems = Goalw [sym_def]
- "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)";
-by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
-qed "symI";
-
-Goalw [sym_def] "[| sym(r); <x,y>: r |] ==> <y,x>: r";
-by (Blast_tac 1);
-qed "symE";
-
-(* antisymmetry *)
-
-val prems = Goalw [antisym_def]
- "[| !!x y.[| <x,y>: r; <y,x>: r |] ==> x=y |] ==> \
-\ antisym(r)";
-by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
-qed "antisymI";
-
-Goalw [antisym_def] "[| antisym(r); <x,y>: r; <y,x>: r |] ==> x=y";
-by (Blast_tac 1);
-qed "antisymE";
-
-(* transitivity *)
-
-Goalw [trans_def] "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
-by (Blast_tac 1);
-qed "transD";
-
-Goalw [trans_on_def]
- "[| trans[A](r); <a,b>:r; <b,c>:r; a:A; b:A; c:A |] ==> <a,c>:r";
-by (Blast_tac 1);
-qed "trans_onD";
-
--- a/src/ZF/Rel.thy Fri Jun 21 18:40:06 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(* Title: ZF/Rel.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Relations in Zermelo-Fraenkel Set Theory
-*)
-
-Rel = equalities +
-consts
- refl :: "[i,i]=>o"
- irrefl :: "[i,i]=>o"
- equiv :: "[i,i]=>o"
- sym :: "i=>o"
- asym :: "i=>o"
- antisym :: "i=>o"
- trans :: "i=>o"
- trans_on :: "[i,i]=>o" ("trans[_]'(_')")
-
-defs
- refl_def "refl(A,r) == (ALL x: A. <x,x> : r)"
-
- irrefl_def "irrefl(A,r) == ALL x: A. <x,x> ~: r"
-
- sym_def "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
-
- asym_def "asym(r) == ALL x y. <x,y>:r --> ~ <y,x>:r"
-
- antisym_def "antisym(r) == ALL x y.<x,y>:r --> <y,x>:r --> x=y"
-
- trans_def "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
-
- trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.
- <x,y>: r --> <y,z>: r --> <x,z>: r"
-
- equiv_def "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
-
-end
--- a/src/ZF/Trancl.ML Fri Jun 21 18:40:06 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,267 +0,0 @@
-(* Title: ZF/trancl.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
-
-Transitive closure of a relation
-*)
-
-Goal "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))";
-by (rtac bnd_monoI 1);
-by (REPEAT (ares_tac [subset_refl, Un_mono, comp_mono] 2));
-by (Blast_tac 1);
-qed "rtrancl_bnd_mono";
-
-Goalw [rtrancl_def] "r<=s ==> r^* <= s^*";
-by (rtac lfp_mono 1);
-by (REPEAT (ares_tac [rtrancl_bnd_mono, subset_refl, id_mono,
- comp_mono, Un_mono, field_mono, Sigma_mono] 1));
-qed "rtrancl_mono";
-
-(* r^* = id(field(r)) Un ( r O r^* ) *)
-bind_thm ("rtrancl_unfold", rtrancl_bnd_mono RS (rtrancl_def RS def_lfp_unfold));
-
-(** The relation rtrancl **)
-
-(* r^* <= field(r) * field(r) *)
-bind_thm ("rtrancl_type", rtrancl_def RS def_lfp_subset);
-
-(*Reflexivity of rtrancl*)
-Goal "[| a: field(r) |] ==> <a,a> : r^*";
-by (resolve_tac [rtrancl_unfold RS ssubst] 1);
-by (etac (idI RS UnI1) 1);
-qed "rtrancl_refl";
-
-(*Closure under composition with r *)
-Goal "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*";
-by (resolve_tac [rtrancl_unfold RS ssubst] 1);
-by (rtac (compI RS UnI2) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "rtrancl_into_rtrancl";
-
-(*rtrancl of r contains all pairs in r *)
-Goal "<a,b> : r ==> <a,b> : r^*";
-by (resolve_tac [rtrancl_refl RS rtrancl_into_rtrancl] 1);
-by (REPEAT (ares_tac [fieldI1] 1));
-qed "r_into_rtrancl";
-
-(*The premise ensures that r consists entirely of pairs*)
-Goal "r <= Sigma(A,B) ==> r <= r^*";
-by (blast_tac (claset() addIs [r_into_rtrancl]) 1);
-qed "r_subset_rtrancl";
-
-Goal "field(r^*) = field(r)";
-by (blast_tac (claset() addIs [r_into_rtrancl]
- addSDs [rtrancl_type RS subsetD]) 1);
-qed "rtrancl_field";
-
-
-(** standard induction rule **)
-
-val major::prems = Goal
- "[| <a,b> : r^*; \
-\ !!x. x: field(r) ==> 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_bnd_mono, major] MRS def_induct) 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "rtrancl_full_induct";
-
-(*nice induction rule.
- Tried adding the typing hypotheses y,z:field(r), but these
- caused expensive case splits!*)
-val major::prems = Goal
- "[| <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 "ALL y. <a,b> = <a,y> --> P(y)" 1);
-(*now solve first subgoal: this formula is sufficient*)
-by (EVERY1 [etac (spec RS mp), rtac refl]);
-(*now do the induction*)
-by (resolve_tac [major RS rtrancl_full_induct] 1);
-by (ALLGOALS (blast_tac (claset() addIs prems)));
-qed "rtrancl_induct";
-
-(*transitivity of transitive closure!! -- by induction.*)
-Goalw [trans_def] "trans(r^*)";
-by (REPEAT (resolve_tac [allI,impI] 1));
-by (eres_inst_tac [("b","z")] rtrancl_induct 1);
-by (DEPTH_SOLVE (eresolve_tac [asm_rl, rtrancl_into_rtrancl] 1));
-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,b> : r^*; (a=b) ==> P; \
-\ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |] \
-\ ==> P";
-by (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r)" 1);
-(*see HOL/trancl*)
-by (rtac (major RS rtrancl_induct) 2);
-by (ALLGOALS (fast_tac (claset() addSEs prems)));
-qed "rtranclE";
-
-
-(**** The relation trancl ****)
-
-(*Transitivity of r^+ is proved by transitivity of r^* *)
-Goalw [trans_def,trancl_def] "trans(r^+)";
-by (blast_tac (claset() addIs [rtrancl_into_rtrancl RS
- (trans_rtrancl RS transD RS compI)]) 1);
-qed "trans_trancl";
-
-bind_thm ("trancl_trans", trans_trancl RS transD);
-
-(** Conversions between trancl and rtrancl **)
-
-Goalw [trancl_def] "<a,b> : r^+ ==> <a,b> : r^*";
-by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
-qed "trancl_into_rtrancl";
-
-(*r^+ contains all pairs in r *)
-Goalw [trancl_def] "<a,b> : r ==> <a,b> : r^+";
-by (blast_tac (claset() addSIs [rtrancl_refl]) 1);
-qed "r_into_trancl";
-
-(*The premise ensures that r consists entirely of pairs*)
-Goal "r <= Sigma(A,B) ==> r <= r^+";
-by (blast_tac (claset() addIs [r_into_trancl]) 1);
-qed "r_subset_trancl";
-
-(*intro rule by definition: from r^* and r *)
-Goalw [trancl_def] "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+";
-by (Blast_tac 1);
-qed "rtrancl_into_trancl1";
-
-(*intro rule from r and r^* *)
-val prems = goal (the_context ())
- "[| <a,b> : r; <b,c> : r^* |] ==> <a,c> : r^+";
-by (resolve_tac (prems RL [rtrancl_induct]) 1);
-by (resolve_tac (prems RL [r_into_trancl]) 1);
-by (etac trancl_trans 1);
-by (etac r_into_trancl 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 (fast_tac (claset() addIs (rtrancl_into_trancl1::prems))));
-qed "trancl_induct";
-
-(*elimination of r^+ -- NOT an induction rule*)
-val major::prems = Goal
- "[| <a,b> : r^+; \
-\ <a,b> : r ==> P; \
-\ !!y.[| <a,y> : r^+; <y,b> : r |] ==> P \
-\ |] ==> P";
-by (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r)" 1);
-by (fast_tac (claset() addIs prems) 1);
-by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
-by (etac rtranclE 1);
-by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_trancl1])));
-qed "tranclE";
-
-Goalw [trancl_def] "r^+ <= field(r)*field(r)";
-by (blast_tac (claset() addEs [rtrancl_type RS subsetD RS SigmaE2]) 1);
-qed "trancl_type";
-
-Goalw [trancl_def] "r<=s ==> r^+ <= s^+";
-by (REPEAT (ares_tac [comp_mono, rtrancl_mono] 1));
-qed "trancl_mono";
-
-(** Suggested by Sidi Ould Ehmety **)
-
-Goal "(r^*)^* = r^*";
-by (rtac equalityI 1);
-by Auto_tac;
-by (ALLGOALS (forward_tac [impOfSubs rtrancl_type]));
-by (ALLGOALS Clarify_tac);
-by (etac r_into_rtrancl 2);
-by (etac rtrancl_induct 1);
-by (asm_full_simp_tac (simpset() addsimps [rtrancl_refl, rtrancl_field]) 1);
-by (blast_tac (claset() addIs [rtrancl_trans]) 1);
-qed "rtrancl_idemp";
-Addsimps [rtrancl_idemp];
-
-Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
-by (dtac rtrancl_mono 1);
-by (dtac rtrancl_mono 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (Blast_tac 1);
-qed "rtrancl_subset";
-
-Goal "[| r<= Sigma(A,B); s<=Sigma(C,D) |] ==> (r^* Un s^*)^* = (r Un s)^*";
-by (rtac rtrancl_subset 1);
-by (blast_tac (claset() addDs [r_subset_rtrancl]) 1);
-by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
-qed "rtrancl_Un_rtrancl";
-
-(*** "converse" laws by Sidi Ould Ehmety ***)
-
-(** rtrancl **)
-
-Goal "<x,y>:converse(r)^* ==> <x,y>:converse(r^*)";
-by (rtac converseI 1);
-by (forward_tac [rtrancl_type RS subsetD] 1);
-by (etac rtrancl_induct 1);
-by (blast_tac (claset() addIs [rtrancl_refl]) 1);
-by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
-qed "rtrancl_converseD";
-
-Goal "<x,y>:converse(r^*) ==> <x,y>:converse(r)^*";
-by (dtac converseD 1);
-by (forward_tac [rtrancl_type RS subsetD] 1);
-by (etac rtrancl_induct 1);
-by (blast_tac (claset() addIs [rtrancl_refl]) 1);
-by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
-qed "rtrancl_converseI";
-
-Goal "converse(r)^* = converse(r^*)";
-by (safe_tac (claset() addSIs [equalityI]));
-by (forward_tac [rtrancl_type RS subsetD] 1);
-by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
-qed "rtrancl_converse";
-
-(** trancl **)
-
-Goal "<a, b>:converse(r)^+ ==> <a, b>:converse(r^+)";
-by (etac trancl_induct 1);
-by (auto_tac (claset() addIs [r_into_trancl, trancl_trans], simpset()));
-qed "trancl_converseD";
-
-Goal "<x,y>:converse(r^+) ==> <x,y>:converse(r)^+";
-by (dtac converseD 1);
-by (etac trancl_induct 1);
-by (auto_tac (claset() addIs [r_into_trancl, trancl_trans], simpset()));
-qed "trancl_converseI";
-
-Goal "converse(r)^+ = converse(r^+)";
-by (safe_tac (claset() addSIs [equalityI]));
-by (forward_tac [trancl_type RS subsetD] 1);
-by (safe_tac (claset() addSDs [trancl_converseD] addSIs [trancl_converseI]));
-qed "trancl_converse";
-
-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 (cut_facts_tac [major] 1);
-by (dtac converseI 1);
-by (full_simp_tac (simpset() addsimps [trancl_converse RS sym]) 1);
-by (etac trancl_induct 1);
-by (auto_tac (claset() addIs prems,
- simpset() addsimps [trancl_converse]));
-qed "converse_trancl_induct";
--- a/src/ZF/Trancl.thy Fri Jun 21 18:40:06 2002 +0200
+++ b/src/ZF/Trancl.thy Sat Jun 22 18:28:46 2002 +0200
@@ -3,15 +3,422 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Transitive closure of a relation
+1. General Properties of relations
+2. Transitive closure of a relation
*)
-Trancl = Fixedpt + Perm + mono + Rel +
-consts
- rtrancl :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*)
- trancl :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*)
+theory Trancl = Fixedpt + Perm + mono:
+
+constdefs
+ refl :: "[i,i]=>o"
+ "refl(A,r) == (ALL x: A. <x,x> : r)"
+
+ irrefl :: "[i,i]=>o"
+ "irrefl(A,r) == ALL x: A. <x,x> ~: r"
+
+ equiv :: "[i,i]=>o"
+ "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
+
+ sym :: "i=>o"
+ "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
+
+ asym :: "i=>o"
+ "asym(r) == ALL x y. <x,y>:r --> ~ <y,x>:r"
+
+ antisym :: "i=>o"
+ "antisym(r) == ALL x y.<x,y>:r --> <y,x>:r --> x=y"
+
+ trans :: "i=>o"
+ "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
+
+ trans_on :: "[i,i]=>o" ("trans[_]'(_')")
+ "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.
+ <x,y>: r --> <y,z>: r --> <x,z>: r"
+
+ rtrancl :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*)
+ "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
+
+ trancl :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*)
+ "r^+ == r O r^*"
+
+subsection{*General properties of relations*}
+
+subsubsection{*irreflexivity*}
+
+lemma irreflI:
+ "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)"
+by (simp add: irrefl_def);
+
+lemma symI: "[| irrefl(A,r); x:A |] ==> <x,x> ~: r"
+apply (simp add: irrefl_def)
+done
+
+subsubsection{*symmetry*}
+
+lemma symI:
+ "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"
+apply (unfold sym_def);
+apply (blast intro: elim:);
+done
+
+lemma antisymI: "[| sym(r); <x,y>: r |] ==> <y,x>: r"
+apply (unfold sym_def)
+apply blast
+done
+
+subsubsection{*antisymmetry*}
+
+lemma antisymI:
+ "[| !!x y.[| <x,y>: r; <y,x>: r |] ==> x=y |] ==> antisym(r)"
+apply (simp add: antisym_def)
+apply (blast intro: elim:);
+done
+
+lemma antisymE: "[| antisym(r); <x,y>: r; <y,x>: r |] ==> x=y"
+apply (simp add: antisym_def)
+apply blast
+done
+
+subsubsection{*transitivity*}
+
+lemma transD: "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r"
+apply (unfold trans_def)
+apply blast
+done
+
+lemma trans_onD:
+ "[| trans[A](r); <a,b>:r; <b,c>:r; a:A; b:A; c:A |] ==> <a,c>:r"
+apply (unfold trans_on_def)
+apply blast
+done
+
+subsection{*Transitive closure of a relation*}
+
+lemma rtrancl_bnd_mono:
+ "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))"
+apply (rule bnd_monoI)
+apply (blast intro: elim:)+
+done
+
+lemma rtrancl_mono: "r<=s ==> r^* <= s^*"
+apply (unfold rtrancl_def)
+apply (rule lfp_mono)
+apply (rule rtrancl_bnd_mono)+
+apply (blast intro: elim:);
+done
+
+(* r^* = id(field(r)) Un ( r O r^* ) *)
+lemmas rtrancl_unfold =
+ rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold], standard]
+
+(** The relation rtrancl **)
+
+(* r^* <= field(r) * field(r) *)
+lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset, standard]
+
+(*Reflexivity of rtrancl*)
+lemma rtrancl_refl: "[| a: field(r) |] ==> <a,a> : r^*"
+apply (rule rtrancl_unfold [THEN ssubst])
+apply (erule idI [THEN UnI1])
+done
+
+(*Closure under composition with r *)
+lemma rtrancl_into_rtrancl: "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*"
+apply (rule rtrancl_unfold [THEN ssubst])
+apply (rule compI [THEN UnI2])
+apply assumption
+apply assumption
+done
+
+(*rtrancl of r contains all pairs in r *)
+lemma r_into_rtrancl: "<a,b> : r ==> <a,b> : r^*"
+apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
+apply (blast intro: elim:)+
+done
+
+(*The premise ensures that r consists entirely of pairs*)
+lemma r_subset_rtrancl: "r <= Sigma(A,B) ==> r <= r^*"
+apply (blast intro: r_into_rtrancl)
+done
+
+lemma rtrancl_field: "field(r^*) = field(r)"
+apply (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD])
+done
+
+
+(** standard induction rule **)
+
+lemma rtrancl_full_induct:
+ "[| <a,b> : r^*;
+ !!x. x: field(r) ==> P(<x,x>);
+ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |]
+ ==> P(<a,b>)"
+apply (erule def_induct [OF rtrancl_def rtrancl_bnd_mono])
+apply (blast intro: elim:);
+done
+
+(*nice induction rule.
+ Tried adding the typing hypotheses y,z:field(r), but these
+ caused expensive case splits!*)
+lemma rtrancl_induct:
+ "[| <a,b> : r^*;
+ P(a);
+ !!y z.[| <a,y> : r^*; <y,z> : r; P(y) |] ==> P(z)
+ |] ==> P(b)"
+(*by induction on this formula*)
+apply (subgoal_tac "ALL y. <a,b> = <a,y> --> P (y) ")
+(*now solve first subgoal: this formula is sufficient*)
+apply (erule spec [THEN mp], rule refl)
+(*now do the induction*)
+apply (erule rtrancl_full_induct)
+apply (blast)+
+done
+
+(*transitivity of transitive closure!! -- by induction.*)
+lemma trans_rtrancl: "trans(r^*)"
+apply (unfold trans_def)
+apply (intro allI impI)
+apply (erule_tac b = "z" in rtrancl_induct)
+apply assumption;
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
+
+(*elimination of rtrancl -- by induction on a special formula*)
+lemma rtranclE:
+ "[| <a,b> : r^*; (a=b) ==> P;
+ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |]
+ ==> P"
+apply (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r) ")
+(*see HOL/trancl*)
+apply (blast intro: elim:);
+apply (erule rtrancl_induct)
+apply (blast intro: elim:)+
+done
+
+
+(**** The relation trancl ****)
+
+(*Transitivity of r^+ is proved by transitivity of r^* *)
+lemma trans_trancl: "trans(r^+)"
+apply (unfold trans_def trancl_def)
+apply (blast intro: rtrancl_into_rtrancl
+ trans_rtrancl [THEN transD, THEN compI])
+done
+
+lemmas trancl_trans = trans_trancl [THEN transD, standard]
+
+(** Conversions between trancl and rtrancl **)
-defs
- rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
- trancl_def "r^+ == r O r^*"
+lemma trancl_into_rtrancl: "<a,b> : r^+ ==> <a,b> : r^*"
+apply (unfold trancl_def)
+apply (blast intro: rtrancl_into_rtrancl)
+done
+
+(*r^+ contains all pairs in r *)
+lemma r_into_trancl: "<a,b> : r ==> <a,b> : r^+"
+apply (unfold trancl_def)
+apply (blast intro!: rtrancl_refl)
+done
+
+(*The premise ensures that r consists entirely of pairs*)
+lemma r_subset_trancl: "r <= Sigma(A,B) ==> r <= r^+"
+apply (blast intro: r_into_trancl)
+done
+
+(*intro rule by definition: from r^* and r *)
+lemma rtrancl_into_trancl1: "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+"
+apply (unfold trancl_def)
+apply blast
+done
+
+(*intro rule from r and r^* *)
+lemma rtrancl_into_trancl2:
+ "[| <a,b> : r; <b,c> : r^* |] ==> <a,c> : r^+"
+apply (erule rtrancl_induct)
+ apply (erule r_into_trancl)
+apply (blast intro: r_into_trancl trancl_trans)
+done
+
+(*Nice induction rule for trancl*)
+lemma trancl_induct:
+ "[| <a,b> : r^+;
+ !!y. [| <a,y> : r |] ==> P(y);
+ !!y z.[| <a,y> : r^+; <y,z> : r; P(y) |] ==> P(z)
+ |] ==> P(b)"
+apply (rule compEpair)
+apply (unfold trancl_def, assumption)
+(*by induction on this formula*)
+apply (subgoal_tac "ALL z. <y,z> : r --> P (z) ")
+(*now solve first subgoal: this formula is sufficient*)
+ apply blast
+apply (erule rtrancl_induct)
+apply (blast intro: rtrancl_into_trancl1)+
+done
+
+(*elimination of r^+ -- NOT an induction rule*)
+lemma tranclE:
+ "[| <a,b> : r^+;
+ <a,b> : r ==> P;
+ !!y.[| <a,y> : r^+; <y,b> : r |] ==> P
+ |] ==> P"
+apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r) ")
+apply (blast intro: elim:);
+apply (rule compEpair)
+apply (unfold trancl_def, assumption)
+apply (erule rtranclE)
+apply (blast intro: rtrancl_into_trancl1)+
+done
+
+lemma trancl_type: "r^+ <= field(r)*field(r)"
+apply (unfold trancl_def)
+apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2])
+done
+
+lemma trancl_mono: "r<=s ==> r^+ <= s^+"
+by (unfold trancl_def, intro comp_mono rtrancl_mono)
+
+
+(** Suggested by Sidi Ould Ehmety **)
+
+lemma rtrancl_idemp [simp]: "(r^*)^* = r^*"
+apply (rule equalityI)
+apply auto
+ prefer 2
+ apply (frule rtrancl_type [THEN subsetD])
+ apply (blast intro: r_into_rtrancl elim:);
+txt{*converse direction*}
+apply (frule rtrancl_type [THEN subsetD])
+apply (clarify );
+apply (erule rtrancl_induct)
+apply (simp add: rtrancl_refl rtrancl_field)
+apply (blast intro: rtrancl_trans)
+done
+
+lemma rtrancl_subset: "[| R <= S; S <= R^* |] ==> S^* = R^*"
+apply (drule rtrancl_mono)
+apply (drule rtrancl_mono)
+apply simp_all
+apply blast
+done
+
+lemma rtrancl_Un_rtrancl:
+ "[| r<= Sigma(A,B); s<=Sigma(C,D) |] ==> (r^* Un s^*)^* = (r Un s)^*"
+apply (rule rtrancl_subset)
+apply (blast dest: r_subset_rtrancl)
+apply (blast intro: rtrancl_mono [THEN subsetD])
+done
+
+(*** "converse" laws by Sidi Ould Ehmety ***)
+
+(** rtrancl **)
+
+lemma rtrancl_converseD: "<x,y>:converse(r)^* ==> <x,y>:converse(r^*)"
+apply (rule converseI)
+apply (frule rtrancl_type [THEN subsetD])
+apply (erule rtrancl_induct)
+apply (blast intro: rtrancl_refl)
+apply (blast intro: r_into_rtrancl rtrancl_trans)
+done
+
+lemma rtrancl_converseI: "<x,y>:converse(r^*) ==> <x,y>:converse(r)^*"
+apply (drule converseD)
+apply (frule rtrancl_type [THEN subsetD])
+apply (erule rtrancl_induct)
+apply (blast intro: rtrancl_refl)
+apply (blast intro: r_into_rtrancl rtrancl_trans)
+done
+
+lemma rtrancl_converse: "converse(r)^* = converse(r^*)"
+apply (safe intro!: equalityI)
+apply (frule rtrancl_type [THEN subsetD])
+apply (safe dest!: rtrancl_converseD intro!: rtrancl_converseI)
+done
+
+(** trancl **)
+
+lemma trancl_converseD: "<a, b>:converse(r)^+ ==> <a, b>:converse(r^+)"
+apply (erule trancl_induct)
+apply (auto intro: r_into_trancl trancl_trans)
+done
+
+lemma trancl_converseI: "<x,y>:converse(r^+) ==> <x,y>:converse(r)^+"
+apply (drule converseD)
+apply (erule trancl_induct)
+apply (auto intro: r_into_trancl trancl_trans)
+done
+
+lemma trancl_converse: "converse(r)^+ = converse(r^+)"
+apply (safe intro!: equalityI)
+apply (frule trancl_type [THEN subsetD])
+apply (safe dest!: trancl_converseD intro!: trancl_converseI)
+done
+
+lemma converse_trancl_induct:
+"[| <a, b>:r^+; !!y. <y, b> :r ==> P(y);
+ !!y z. [| <y, z> : r; <z, b> : r^+; P(z) |] ==> P(y) |]
+ ==> P(a)"
+apply (drule converseI)
+apply (simp (no_asm_use) add: trancl_converse [symmetric])
+apply (erule trancl_induct)
+apply (auto simp add: trancl_converse)
+done
+
+ML
+{*
+val refl_def = thm "refl_def";
+val irrefl_def = thm "irrefl_def";
+val equiv_def = thm "equiv_def";
+val sym_def = thm "sym_def";
+val asym_def = thm "asym_def";
+val antisym_def = thm "antisym_def";
+val trans_def = thm "trans_def";
+val trans_on_def = thm "trans_on_def";
+
+val irreflI = thm "irreflI";
+val symI = thm "symI";
+val symI = thm "symI";
+val antisymI = thm "antisymI";
+val antisymE = thm "antisymE";
+val transD = thm "transD";
+val trans_onD = thm "trans_onD";
+
+val rtrancl_bnd_mono = thm "rtrancl_bnd_mono";
+val rtrancl_mono = thm "rtrancl_mono";
+val rtrancl_unfold = thm "rtrancl_unfold";
+val rtrancl_type = thm "rtrancl_type";
+val rtrancl_refl = thm "rtrancl_refl";
+val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
+val r_into_rtrancl = thm "r_into_rtrancl";
+val r_subset_rtrancl = thm "r_subset_rtrancl";
+val rtrancl_field = thm "rtrancl_field";
+val rtrancl_full_induct = thm "rtrancl_full_induct";
+val rtrancl_induct = thm "rtrancl_induct";
+val trans_rtrancl = thm "trans_rtrancl";
+val rtrancl_trans = thm "rtrancl_trans";
+val rtranclE = thm "rtranclE";
+val trans_trancl = thm "trans_trancl";
+val trancl_trans = thm "trancl_trans";
+val trancl_into_rtrancl = thm "trancl_into_rtrancl";
+val r_into_trancl = thm "r_into_trancl";
+val r_subset_trancl = thm "r_subset_trancl";
+val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1";
+val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2";
+val trancl_induct = thm "trancl_induct";
+val tranclE = thm "tranclE";
+val trancl_type = thm "trancl_type";
+val trancl_mono = thm "trancl_mono";
+val rtrancl_idemp = thm "rtrancl_idemp";
+val rtrancl_subset = thm "rtrancl_subset";
+val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl";
+val rtrancl_converseD = thm "rtrancl_converseD";
+val rtrancl_converseI = thm "rtrancl_converseI";
+val rtrancl_converse = thm "rtrancl_converse";
+val trancl_converseD = thm "trancl_converseD";
+val trancl_converseI = thm "trancl_converseI";
+val trancl_converse = thm "trancl_converse";
+val converse_trancl_induct = thm "converse_trancl_induct";
+*}
+
end