converted Bool, Trancl, Rel to Isar format
authorpaulson
Sat Jun 22 18:28:46 2002 +0200 (2002-06-22)
changeset 13239f599984ec4c2
parent 13238 a6cb18a25cbb
child 13240 bb5f4faea1f3
converted Bool, Trancl, Rel to Isar format
src/ZF/Bool.ML
src/ZF/Bool.thy
src/ZF/Integ/EquivClass.thy
src/ZF/IsaMakefile
src/ZF/Rel.ML
src/ZF/Rel.thy
src/ZF/Trancl.ML
src/ZF/Trancl.thy
     1.1 --- a/src/ZF/Bool.ML	Fri Jun 21 18:40:06 2002 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,176 +0,0 @@
     1.4 -(*  Title:      ZF/bool
     1.5 -    ID:         $Id$
     1.6 -    Author:     Martin D Coen, Cambridge University Computer Laboratory
     1.7 -    Copyright   1992  University of Cambridge
     1.8 -
     1.9 -Booleans in Zermelo-Fraenkel Set Theory 
    1.10 -*)
    1.11 -
    1.12 -bind_thms ("bool_defs", [bool_def,cond_def]);
    1.13 -
    1.14 -Goalw [succ_def] "{0} = 1";
    1.15 -by (rtac refl 1);
    1.16 -qed "singleton_0";
    1.17 -
    1.18 -(* Introduction rules *)
    1.19 -
    1.20 -Goalw bool_defs "1 : bool";
    1.21 -by (rtac (consI1 RS consI2) 1);
    1.22 -qed "bool_1I";
    1.23 -
    1.24 -Goalw bool_defs "0 : bool";
    1.25 -by (rtac consI1 1);
    1.26 -qed "bool_0I";
    1.27 -
    1.28 -Addsimps [bool_1I, bool_0I];
    1.29 -AddTCs   [bool_1I, bool_0I];
    1.30 -
    1.31 -Goalw bool_defs "1~=0";
    1.32 -by (rtac succ_not_0 1);
    1.33 -qed "one_not_0";
    1.34 -
    1.35 -(** 1=0 ==> R **)
    1.36 -bind_thm ("one_neq_0", one_not_0 RS notE);
    1.37 -
    1.38 -val major::prems = Goalw bool_defs
    1.39 -    "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P";
    1.40 -by (rtac (major RS consE) 1);
    1.41 -by (REPEAT (eresolve_tac (singletonE::prems) 1));
    1.42 -qed "boolE";
    1.43 -
    1.44 -(** cond **)
    1.45 -
    1.46 -(*1 means true*)
    1.47 -Goalw bool_defs "cond(1,c,d) = c";
    1.48 -by (rtac (refl RS if_P) 1);
    1.49 -qed "cond_1";
    1.50 -
    1.51 -(*0 means false*)
    1.52 -Goalw bool_defs "cond(0,c,d) = d";
    1.53 -by (rtac (succ_not_0 RS not_sym RS if_not_P) 1);
    1.54 -qed "cond_0";
    1.55 -
    1.56 -Addsimps [cond_1, cond_0];
    1.57 -
    1.58 -fun bool_tac i = fast_tac (claset() addSEs [boolE] addss (simpset())) i;
    1.59 -
    1.60 -
    1.61 -Goal "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
    1.62 -by (bool_tac 1);
    1.63 -qed "cond_type";
    1.64 -AddTCs [cond_type];
    1.65 -
    1.66 -(*For Simp_tac and Blast_tac*)
    1.67 -Goal "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A";
    1.68 -by (bool_tac 1);
    1.69 -qed "cond_simple_type";
    1.70 -
    1.71 -val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
    1.72 -by (rewtac rew);
    1.73 -by (rtac cond_1 1);
    1.74 -qed "def_cond_1";
    1.75 -
    1.76 -val [rew] = Goal "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
    1.77 -by (rewtac rew);
    1.78 -by (rtac cond_0 1);
    1.79 -qed "def_cond_0";
    1.80 -
    1.81 -fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)];
    1.82 -
    1.83 -val [not_1, not_0] = conds not_def;
    1.84 -val [and_1, and_0] = conds and_def;
    1.85 -val [or_1, or_0]   = conds or_def;
    1.86 -val [xor_1, xor_0] = conds xor_def;
    1.87 -
    1.88 -bind_thm ("not_1", not_1);
    1.89 -bind_thm ("not_0", not_0);
    1.90 -bind_thm ("and_1", and_1);
    1.91 -bind_thm ("and_0", and_0);
    1.92 -bind_thm ("or_1", or_1);
    1.93 -bind_thm ("or_0", or_0);
    1.94 -bind_thm ("xor_1", xor_1);
    1.95 -bind_thm ("xor_0", xor_0);
    1.96 -
    1.97 -Addsimps [not_1,not_0,and_1,and_0,or_1,or_0,xor_1,xor_0];
    1.98 -
    1.99 -Goalw [not_def] "a:bool ==> not(a) : bool";
   1.100 -by (Asm_simp_tac 1);
   1.101 -qed "not_type";
   1.102 -
   1.103 -Goalw [and_def] "[| a:bool;  b:bool |] ==> a and b : bool";
   1.104 -by (Asm_simp_tac 1);
   1.105 -qed "and_type";
   1.106 -
   1.107 -Goalw [or_def] "[| a:bool;  b:bool |] ==> a or b : bool";
   1.108 -by (Asm_simp_tac 1);
   1.109 -qed "or_type";
   1.110 -
   1.111 -AddTCs [not_type, and_type, or_type];
   1.112 -
   1.113 -Goalw [xor_def] "[| a:bool;  b:bool |] ==> a xor b : bool";
   1.114 -by (Asm_simp_tac 1);
   1.115 -qed "xor_type";
   1.116 -
   1.117 -AddTCs [xor_type];
   1.118 -
   1.119 -bind_thms ("bool_typechecks",
   1.120 -  [bool_1I, bool_0I, cond_type, not_type, and_type, or_type, xor_type]);
   1.121 -
   1.122 -(*** Laws for 'not' ***)
   1.123 -
   1.124 -Goal "a:bool ==> not(not(a)) = a";
   1.125 -by (bool_tac 1);
   1.126 -qed "not_not";
   1.127 -
   1.128 -Goal "a:bool ==> not(a and b) = not(a) or not(b)";
   1.129 -by (bool_tac 1);
   1.130 -qed "not_and";
   1.131 -
   1.132 -Goal "a:bool ==> not(a or b) = not(a) and not(b)";
   1.133 -by (bool_tac 1);
   1.134 -qed "not_or";
   1.135 -
   1.136 -Addsimps [not_not, not_and, not_or];
   1.137 -
   1.138 -(*** Laws about 'and' ***)
   1.139 -
   1.140 -Goal "a: bool ==> a and a = a";
   1.141 -by (bool_tac 1);
   1.142 -qed "and_absorb";
   1.143 -
   1.144 -Addsimps [and_absorb];
   1.145 -
   1.146 -Goal "[| a: bool; b:bool |] ==> a and b = b and a";
   1.147 -by (bool_tac 1);
   1.148 -qed "and_commute";
   1.149 -
   1.150 -Goal "a: bool ==> (a and b) and c  =  a and (b and c)";
   1.151 -by (bool_tac 1);
   1.152 -qed "and_assoc";
   1.153 -
   1.154 -Goal "[| a: bool; b:bool; c:bool |] ==> \
   1.155 -\      (a or b) and c  =  (a and c) or (b and c)";
   1.156 -by (bool_tac 1);
   1.157 -qed "and_or_distrib";
   1.158 -
   1.159 -(** binary orion **)
   1.160 -
   1.161 -Goal "a: bool ==> a or a = a";
   1.162 -by (bool_tac 1);
   1.163 -qed "or_absorb";
   1.164 -
   1.165 -Addsimps [or_absorb];
   1.166 -
   1.167 -Goal "[| a: bool; b:bool |] ==> a or b = b or a";
   1.168 -by (bool_tac 1);
   1.169 -qed "or_commute";
   1.170 -
   1.171 -Goal "a: bool ==> (a or b) or c  =  a or (b or c)";
   1.172 -by (bool_tac 1);
   1.173 -qed "or_assoc";
   1.174 -
   1.175 -Goal "[| a: bool; b: bool; c: bool |] ==> \
   1.176 -\          (a and b) or c  =  (a or c) and (b or c)";
   1.177 -by (bool_tac 1);
   1.178 -qed "or_and_distrib";
   1.179 -
     2.1 --- a/src/ZF/Bool.thy	Fri Jun 21 18:40:06 2002 +0200
     2.2 +++ b/src/ZF/Bool.thy	Sat Jun 22 18:28:46 2002 +0200
     2.3 @@ -8,14 +8,7 @@
     2.4  2 is equal to bool, but serves a different purpose
     2.5  *)
     2.6  
     2.7 -Bool = pair + 
     2.8 -consts
     2.9 -    bool        :: i
    2.10 -    cond        :: "[i,i,i]=>i"
    2.11 -    not         :: "i=>i"
    2.12 -    "and"       :: "[i,i]=>i"      (infixl 70)
    2.13 -    or          :: "[i,i]=>i"      (infixl 65)
    2.14 -    xor         :: "[i,i]=>i"      (infixl 65)
    2.15 +theory Bool = pair:
    2.16  
    2.17  syntax
    2.18      "1"         :: i             ("1")
    2.19 @@ -25,11 +18,181 @@
    2.20     "1"  == "succ(0)"
    2.21     "2"  == "succ(1)"
    2.22  
    2.23 -defs
    2.24 -    bool_def    "bool == {0,1}"
    2.25 -    cond_def    "cond(b,c,d) == if(b=1,c,d)"
    2.26 -    not_def     "not(b) == cond(b,0,1)"
    2.27 -    and_def     "a and b == cond(a,b,0)"
    2.28 -    or_def      "a or b == cond(a,1,b)"
    2.29 -    xor_def     "a xor b == cond(a,not(b),b)"
    2.30 +constdefs
    2.31 +  bool        :: i
    2.32 +    "bool == {0,1}"
    2.33 +
    2.34 +  cond        :: "[i,i,i]=>i"
    2.35 +    "cond(b,c,d) == if(b=1,c,d)"
    2.36 +
    2.37 +  not         :: "i=>i"
    2.38 +    "not(b) == cond(b,0,1)"
    2.39 +
    2.40 +  "and"       :: "[i,i]=>i"      (infixl "and" 70)
    2.41 +    "a and b == cond(a,b,0)"
    2.42 +
    2.43 +  or          :: "[i,i]=>i"      (infixl "or" 65)
    2.44 +    "a or b == cond(a,1,b)"
    2.45 +
    2.46 +  xor         :: "[i,i]=>i"      (infixl "xor" 65)
    2.47 +    "a xor b == cond(a,not(b),b)"
    2.48 +
    2.49 +
    2.50 +lemmas bool_defs = bool_def cond_def
    2.51 +
    2.52 +lemma singleton_0: "{0} = 1"
    2.53 +by (simp add: succ_def)
    2.54 +
    2.55 +(* Introduction rules *)
    2.56 +
    2.57 +lemma bool_1I [simp,TC]: "1 : bool"
    2.58 +by (simp add: bool_defs )
    2.59 +
    2.60 +lemma bool_0I [simp,TC]: "0 : bool"
    2.61 +by (simp add: bool_defs)
    2.62 +
    2.63 +lemma one_not_0: "1~=0"
    2.64 +by (simp add: bool_defs )
    2.65 +
    2.66 +(** 1=0 ==> R **)
    2.67 +lemmas one_neq_0 = one_not_0 [THEN notE, standard]
    2.68 +
    2.69 +lemma boolE:
    2.70 +    "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P"
    2.71 +by (simp add: bool_defs, blast)  
    2.72 +
    2.73 +(** cond **)
    2.74 +
    2.75 +(*1 means true*)
    2.76 +lemma cond_1 [simp]: "cond(1,c,d) = c"
    2.77 +by (simp add: bool_defs )
    2.78 +
    2.79 +(*0 means false*)
    2.80 +lemma cond_0 [simp]: "cond(0,c,d) = d"
    2.81 +by (simp add: bool_defs )
    2.82 +
    2.83 +lemma cond_type [TC]: "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)"
    2.84 +by (simp add: bool_defs , blast)
    2.85 +
    2.86 +(*For Simp_tac and Blast_tac*)
    2.87 +lemma cond_simple_type: "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A"
    2.88 +by (simp add: bool_defs )
    2.89 +
    2.90 +lemma def_cond_1: "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c"
    2.91 +by simp
    2.92 +
    2.93 +lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d"
    2.94 +by simp
    2.95 +
    2.96 +lemmas not_1 = not_def [THEN def_cond_1, standard, simp]
    2.97 +lemmas not_0 = not_def [THEN def_cond_0, standard, simp]
    2.98 +
    2.99 +lemmas and_1 = and_def [THEN def_cond_1, standard, simp]
   2.100 +lemmas and_0 = and_def [THEN def_cond_0, standard, simp]
   2.101 +
   2.102 +lemmas or_1 = or_def [THEN def_cond_1, standard, simp]
   2.103 +lemmas or_0 = or_def [THEN def_cond_0, standard, simp]
   2.104 +
   2.105 +lemmas xor_1 = xor_def [THEN def_cond_1, standard, simp]
   2.106 +lemmas xor_0 = xor_def [THEN def_cond_0, standard, simp]
   2.107 +
   2.108 +lemma not_type [TC]: "a:bool ==> not(a) : bool"
   2.109 +by (simp add: not_def)
   2.110 +
   2.111 +lemma and_type [TC]: "[| a:bool;  b:bool |] ==> a and b : bool"
   2.112 +by (simp add: and_def)
   2.113 +
   2.114 +lemma or_type [TC]: "[| a:bool;  b:bool |] ==> a or b : bool"
   2.115 +by (simp add: or_def)
   2.116 +
   2.117 +lemma xor_type [TC]: "[| a:bool;  b:bool |] ==> a xor b : bool"
   2.118 +by (simp add: xor_def)
   2.119 +
   2.120 +lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type
   2.121 +                         or_type xor_type
   2.122 +
   2.123 +(*** Laws for 'not' ***)
   2.124 +
   2.125 +lemma not_not [simp]: "a:bool ==> not(not(a)) = a"
   2.126 +by (elim boolE, auto)
   2.127 +
   2.128 +lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)"
   2.129 +by (elim boolE, auto)
   2.130 +
   2.131 +lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)"
   2.132 +by (elim boolE, auto)
   2.133 +
   2.134 +(*** Laws about 'and' ***)
   2.135 +
   2.136 +lemma and_absorb [simp]: "a: bool ==> a and a = a"
   2.137 +by (elim boolE, auto)
   2.138 +
   2.139 +lemma and_commute: "[| a: bool; b:bool |] ==> a and b = b and a"
   2.140 +by (elim boolE, auto)
   2.141 +
   2.142 +lemma and_assoc: "a: bool ==> (a and b) and c  =  a and (b and c)"
   2.143 +by (elim boolE, auto)
   2.144 +
   2.145 +lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==>  
   2.146 +       (a or b) and c  =  (a and c) or (b and c)"
   2.147 +by (elim boolE, auto)
   2.148 +
   2.149 +(** binary orion **)
   2.150 +
   2.151 +lemma or_absorb [simp]: "a: bool ==> a or a = a"
   2.152 +by (elim boolE, auto)
   2.153 +
   2.154 +lemma or_commute: "[| a: bool; b:bool |] ==> a or b = b or a"
   2.155 +by (elim boolE, auto)
   2.156 +
   2.157 +lemma or_assoc: "a: bool ==> (a or b) or c  =  a or (b or c)"
   2.158 +by (elim boolE, auto)
   2.159 +
   2.160 +lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==>  
   2.161 +           (a and b) or c  =  (a or c) and (b or c)"
   2.162 +by (elim boolE, auto)
   2.163 +
   2.164 +ML
   2.165 +{*
   2.166 +val bool_def = thm "bool_def";
   2.167 +
   2.168 +val bool_defs = thms "bool_defs";
   2.169 +val singleton_0 = thm "singleton_0";
   2.170 +val bool_1I = thm "bool_1I";
   2.171 +val bool_0I = thm "bool_0I";
   2.172 +val one_not_0 = thm "one_not_0";
   2.173 +val one_neq_0 = thm "one_neq_0";
   2.174 +val boolE = thm "boolE";
   2.175 +val cond_1 = thm "cond_1";
   2.176 +val cond_0 = thm "cond_0";
   2.177 +val cond_type = thm "cond_type";
   2.178 +val cond_simple_type = thm "cond_simple_type";
   2.179 +val def_cond_1 = thm "def_cond_1";
   2.180 +val def_cond_0 = thm "def_cond_0";
   2.181 +val not_1 = thm "not_1";
   2.182 +val not_0 = thm "not_0";
   2.183 +val and_1 = thm "and_1";
   2.184 +val and_0 = thm "and_0";
   2.185 +val or_1 = thm "or_1";
   2.186 +val or_0 = thm "or_0";
   2.187 +val xor_1 = thm "xor_1";
   2.188 +val xor_0 = thm "xor_0";
   2.189 +val not_type = thm "not_type";
   2.190 +val and_type = thm "and_type";
   2.191 +val or_type = thm "or_type";
   2.192 +val xor_type = thm "xor_type";
   2.193 +val bool_typechecks = thms "bool_typechecks";
   2.194 +val not_not = thm "not_not";
   2.195 +val not_and = thm "not_and";
   2.196 +val not_or = thm "not_or";
   2.197 +val and_absorb = thm "and_absorb";
   2.198 +val and_commute = thm "and_commute";
   2.199 +val and_assoc = thm "and_assoc";
   2.200 +val and_or_distrib = thm "and_or_distrib";
   2.201 +val or_absorb = thm "or_absorb";
   2.202 +val or_commute = thm "or_commute";
   2.203 +val or_assoc = thm "or_assoc";
   2.204 +val or_and_distrib = thm "or_and_distrib";
   2.205 +*}
   2.206 +
   2.207  end
     3.1 --- a/src/ZF/Integ/EquivClass.thy	Fri Jun 21 18:40:06 2002 +0200
     3.2 +++ b/src/ZF/Integ/EquivClass.thy	Sat Jun 22 18:28:46 2002 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  Equivalence relations in Zermelo-Fraenkel Set Theory 
     3.5  *)
     3.6  
     3.7 -EquivClass = Rel + Perm + 
     3.8 +EquivClass = Trancl + Perm + 
     3.9  
    3.10  constdefs
    3.11  
     4.1 --- a/src/ZF/IsaMakefile	Fri Jun 21 18:40:06 2002 +0200
     4.2 +++ b/src/ZF/IsaMakefile	Sat Jun 22 18:28:46 2002 +0200
     4.3 @@ -29,7 +29,7 @@
     4.4  	@cd $(SRC)/FOL; $(ISATOOL) make FOL
     4.5  
     4.6  $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.ML	\
     4.7 -  ArithSimp.thy Bool.ML Bool.thy Cardinal.thy		\
     4.8 +  ArithSimp.thy Bool.thy Cardinal.thy		\
     4.9    CardinalArith.thy Cardinal_AC.thy \
    4.10    Datatype.ML Datatype.thy Epsilon.thy Finite.thy	\
    4.11    Fixedpt.thy Inductive.ML Inductive.thy 	\
    4.12 @@ -39,11 +39,11 @@
    4.13    Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
    4.14    Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy	\
    4.15    OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy	\
    4.16 -  QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML	\
    4.17 +  QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Sum.ML	\
    4.18    Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
    4.19    Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
    4.20    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
    4.21 -  Trancl.ML Trancl.thy Univ.thy Update.thy \
    4.22 +  Trancl.thy Univ.thy Update.thy \
    4.23    WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy	\
    4.24    ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML		\
    4.25    subset.ML subset.thy thy_syntax.ML upair.ML upair.thy
     5.1 --- a/src/ZF/Rel.ML	Fri Jun 21 18:40:06 2002 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,55 +0,0 @@
     5.4 -(*  Title:      ZF/Rel.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1994  University of Cambridge
     5.8 -
     5.9 -Relations in Zermelo-Fraenkel Set Theory 
    5.10 -*)
    5.11 -
    5.12 -(*** Some properties of relations -- useful? ***)
    5.13 -
    5.14 -(* irreflexivity *)
    5.15 -
    5.16 -val prems = Goalw [irrefl_def]
    5.17 -    "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)";
    5.18 -by (REPEAT (ares_tac (prems @ [ballI]) 1));
    5.19 -qed "irreflI";
    5.20 -
    5.21 -Goalw [irrefl_def] "[| irrefl(A,r);  x:A |] ==>  <x,x> ~: r";
    5.22 -by (Blast_tac 1);
    5.23 -qed "irreflE";
    5.24 -
    5.25 -(* symmetry *)
    5.26 -
    5.27 -val prems = Goalw [sym_def]
    5.28 -     "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)";
    5.29 -by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
    5.30 -qed "symI";
    5.31 -
    5.32 -Goalw [sym_def] "[| sym(r); <x,y>: r |]  ==>  <y,x>: r";
    5.33 -by (Blast_tac 1);
    5.34 -qed "symE";
    5.35 -
    5.36 -(* antisymmetry *)
    5.37 -
    5.38 -val prems = Goalw [antisym_def]
    5.39 -     "[| !!x y.[| <x,y>: r;  <y,x>: r |] ==> x=y |] ==> \
    5.40 -\     antisym(r)";
    5.41 -by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
    5.42 -qed "antisymI";
    5.43 -
    5.44 -Goalw [antisym_def] "[| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y";
    5.45 -by (Blast_tac 1);
    5.46 -qed "antisymE";
    5.47 -
    5.48 -(* transitivity *)
    5.49 -
    5.50 -Goalw [trans_def] "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
    5.51 -by (Blast_tac 1);
    5.52 -qed "transD";
    5.53 -
    5.54 -Goalw [trans_on_def]
    5.55 -    "[| trans[A](r);  <a,b>:r;  <b,c>:r;  a:A;  b:A;  c:A |] ==> <a,c>:r";
    5.56 -by (Blast_tac 1);
    5.57 -qed "trans_onD";
    5.58 -
     6.1 --- a/src/ZF/Rel.thy	Fri Jun 21 18:40:06 2002 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,38 +0,0 @@
     6.4 -(*  Title:      ZF/Rel.thy
     6.5 -    ID:         $Id$
     6.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 -    Copyright   1994  University of Cambridge
     6.8 -
     6.9 -Relations in Zermelo-Fraenkel Set Theory 
    6.10 -*)
    6.11 -
    6.12 -Rel = equalities +
    6.13 -consts
    6.14 -    refl     :: "[i,i]=>o"
    6.15 -    irrefl   :: "[i,i]=>o"
    6.16 -    equiv    :: "[i,i]=>o"
    6.17 -    sym      :: "i=>o"
    6.18 -    asym     :: "i=>o"
    6.19 -    antisym  :: "i=>o"
    6.20 -    trans    :: "i=>o"
    6.21 -    trans_on :: "[i,i]=>o"  ("trans[_]'(_')")
    6.22 -
    6.23 -defs
    6.24 -  refl_def     "refl(A,r) == (ALL x: A. <x,x> : r)"
    6.25 -
    6.26 -  irrefl_def   "irrefl(A,r) == ALL x: A. <x,x> ~: r"
    6.27 -
    6.28 -  sym_def      "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
    6.29 -
    6.30 -  asym_def     "asym(r) == ALL x y. <x,y>:r --> ~ <y,x>:r"
    6.31 -
    6.32 -  antisym_def  "antisym(r) == ALL x y.<x,y>:r --> <y,x>:r --> x=y"
    6.33 -
    6.34 -  trans_def    "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
    6.35 -
    6.36 -  trans_on_def "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.       
    6.37 -                          <x,y>: r --> <y,z>: r --> <x,z>: r"
    6.38 -
    6.39 -  equiv_def    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
    6.40 -
    6.41 -end
     7.1 --- a/src/ZF/Trancl.ML	Fri Jun 21 18:40:06 2002 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,267 +0,0 @@
     7.4 -(*  Title:      ZF/trancl.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 -    Copyright   1992  University of Cambridge
     7.8 -
     7.9 -Transitive closure of a relation
    7.10 -*)
    7.11 -
    7.12 -Goal "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))";
    7.13 -by (rtac bnd_monoI 1);
    7.14 -by (REPEAT (ares_tac [subset_refl, Un_mono, comp_mono] 2));
    7.15 -by (Blast_tac 1);
    7.16 -qed "rtrancl_bnd_mono";
    7.17 -
    7.18 -Goalw [rtrancl_def] "r<=s ==> r^* <= s^*";
    7.19 -by (rtac lfp_mono 1);
    7.20 -by (REPEAT (ares_tac [rtrancl_bnd_mono, subset_refl, id_mono,
    7.21 -		      comp_mono, Un_mono, field_mono, Sigma_mono] 1));
    7.22 -qed "rtrancl_mono";
    7.23 -
    7.24 -(* r^* = id(field(r)) Un ( r O r^* )    *)
    7.25 -bind_thm ("rtrancl_unfold", rtrancl_bnd_mono RS (rtrancl_def RS def_lfp_unfold));
    7.26 -
    7.27 -(** The relation rtrancl **)
    7.28 -
    7.29 -(*  r^* <= field(r) * field(r)  *)
    7.30 -bind_thm ("rtrancl_type", rtrancl_def RS def_lfp_subset);
    7.31 -
    7.32 -(*Reflexivity of rtrancl*)
    7.33 -Goal "[| a: field(r) |] ==> <a,a> : r^*";
    7.34 -by (resolve_tac [rtrancl_unfold RS ssubst] 1);
    7.35 -by (etac (idI RS UnI1) 1);
    7.36 -qed "rtrancl_refl";
    7.37 -
    7.38 -(*Closure under composition with r  *)
    7.39 -Goal "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*";
    7.40 -by (resolve_tac [rtrancl_unfold RS ssubst] 1);
    7.41 -by (rtac (compI RS UnI2) 1);
    7.42 -by (assume_tac 1);
    7.43 -by (assume_tac 1);
    7.44 -qed "rtrancl_into_rtrancl";
    7.45 -
    7.46 -(*rtrancl of r contains all pairs in r  *)
    7.47 -Goal "<a,b> : r ==> <a,b> : r^*";
    7.48 -by (resolve_tac [rtrancl_refl RS rtrancl_into_rtrancl] 1);
    7.49 -by (REPEAT (ares_tac [fieldI1] 1));
    7.50 -qed "r_into_rtrancl";
    7.51 -
    7.52 -(*The premise ensures that r consists entirely of pairs*)
    7.53 -Goal "r <= Sigma(A,B) ==> r <= r^*";
    7.54 -by (blast_tac (claset() addIs [r_into_rtrancl]) 1);
    7.55 -qed "r_subset_rtrancl";
    7.56 -
    7.57 -Goal "field(r^*) = field(r)";
    7.58 -by (blast_tac (claset() addIs [r_into_rtrancl] 
    7.59 -                    addSDs [rtrancl_type RS subsetD]) 1);
    7.60 -qed "rtrancl_field";
    7.61 -
    7.62 -
    7.63 -(** standard induction rule **)
    7.64 -
    7.65 -val major::prems = Goal
    7.66 -  "[| <a,b> : r^*; \
    7.67 -\     !!x. x: field(r) ==> P(<x,x>); \
    7.68 -\     !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |] \
    7.69 -\  ==>  P(<a,b>)";
    7.70 -by (rtac ([rtrancl_def, rtrancl_bnd_mono, major] MRS def_induct) 1);
    7.71 -by (blast_tac (claset() addIs prems) 1);
    7.72 -qed "rtrancl_full_induct";
    7.73 -
    7.74 -(*nice induction rule.
    7.75 -  Tried adding the typing hypotheses y,z:field(r), but these
    7.76 -  caused expensive case splits!*)
    7.77 -val major::prems = Goal
    7.78 -  "[| <a,b> : r^*;                                              \
    7.79 -\     P(a);                                                     \
    7.80 -\     !!y z.[| <a,y> : r^*;  <y,z> : r;  P(y) |] ==> P(z)       \
    7.81 -\  |] ==> P(b)";
    7.82 -(*by induction on this formula*)
    7.83 -by (subgoal_tac "ALL y. <a,b> = <a,y> --> P(y)" 1);
    7.84 -(*now solve first subgoal: this formula is sufficient*)
    7.85 -by (EVERY1 [etac (spec RS mp), rtac refl]);
    7.86 -(*now do the induction*)
    7.87 -by (resolve_tac [major RS rtrancl_full_induct] 1);
    7.88 -by (ALLGOALS (blast_tac (claset() addIs prems)));
    7.89 -qed "rtrancl_induct";
    7.90 -
    7.91 -(*transitivity of transitive closure!! -- by induction.*)
    7.92 -Goalw [trans_def] "trans(r^*)";
    7.93 -by (REPEAT (resolve_tac [allI,impI] 1));
    7.94 -by (eres_inst_tac [("b","z")] rtrancl_induct 1);
    7.95 -by (DEPTH_SOLVE (eresolve_tac [asm_rl, rtrancl_into_rtrancl] 1));
    7.96 -qed "trans_rtrancl";
    7.97 -
    7.98 -bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
    7.99 -
   7.100 -(*elimination of rtrancl -- by induction on a special formula*)
   7.101 -val major::prems = Goal
   7.102 -    "[| <a,b> : r^*;  (a=b) ==> P;                       \
   7.103 -\       !!y.[| <a,y> : r^*;   <y,b> : r |] ==> P |]      \
   7.104 -\    ==> P";
   7.105 -by (subgoal_tac "a = b  | (EX y. <a,y> : r^* & <y,b> : r)" 1);
   7.106 -(*see HOL/trancl*)
   7.107 -by (rtac (major RS rtrancl_induct) 2);
   7.108 -by (ALLGOALS (fast_tac (claset() addSEs prems)));
   7.109 -qed "rtranclE";
   7.110 -
   7.111 -
   7.112 -(**** The relation trancl ****)
   7.113 -
   7.114 -(*Transitivity of r^+ is proved by transitivity of r^*  *)
   7.115 -Goalw [trans_def,trancl_def] "trans(r^+)";
   7.116 -by (blast_tac (claset() addIs [rtrancl_into_rtrancl RS 
   7.117 -			      (trans_rtrancl RS transD RS compI)]) 1);
   7.118 -qed "trans_trancl";
   7.119 -
   7.120 -bind_thm ("trancl_trans", trans_trancl RS transD);
   7.121 -
   7.122 -(** Conversions between trancl and rtrancl **)
   7.123 -
   7.124 -Goalw [trancl_def] "<a,b> : r^+ ==> <a,b> : r^*";
   7.125 -by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   7.126 -qed "trancl_into_rtrancl";
   7.127 -
   7.128 -(*r^+ contains all pairs in r  *)
   7.129 -Goalw [trancl_def] "<a,b> : r ==> <a,b> : r^+";
   7.130 -by (blast_tac (claset() addSIs [rtrancl_refl]) 1);
   7.131 -qed "r_into_trancl";
   7.132 -
   7.133 -(*The premise ensures that r consists entirely of pairs*)
   7.134 -Goal "r <= Sigma(A,B) ==> r <= r^+";
   7.135 -by (blast_tac (claset() addIs [r_into_trancl]) 1);
   7.136 -qed "r_subset_trancl";
   7.137 -
   7.138 -(*intro rule by definition: from r^* and r  *)
   7.139 -Goalw [trancl_def] "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+";
   7.140 -by (Blast_tac 1);
   7.141 -qed "rtrancl_into_trancl1";
   7.142 -
   7.143 -(*intro rule from r and r^*  *)
   7.144 -val prems = goal (the_context ())
   7.145 -    "[| <a,b> : r;  <b,c> : r^* |]   ==>  <a,c> : r^+";
   7.146 -by (resolve_tac (prems RL [rtrancl_induct]) 1);
   7.147 -by (resolve_tac (prems RL [r_into_trancl]) 1);
   7.148 -by (etac trancl_trans 1);
   7.149 -by (etac r_into_trancl 1);
   7.150 -qed "rtrancl_into_trancl2";
   7.151 -
   7.152 -(*Nice induction rule for trancl*)
   7.153 -val major::prems = Goal
   7.154 -  "[| <a,b> : r^+;                                      \
   7.155 -\     !!y.  [| <a,y> : r |] ==> P(y);                   \
   7.156 -\     !!y z.[| <a,y> : r^+;  <y,z> : r;  P(y) |] ==> P(z)       \
   7.157 -\  |] ==> P(b)";
   7.158 -by (rtac (rewrite_rule [trancl_def] major  RS  compEpair) 1);
   7.159 -(*by induction on this formula*)
   7.160 -by (subgoal_tac "ALL z. <y,z> : r --> P(z)" 1);
   7.161 -(*now solve first subgoal: this formula is sufficient*)
   7.162 -by (Blast_tac 1);
   7.163 -by (etac rtrancl_induct 1);
   7.164 -by (ALLGOALS (fast_tac (claset() addIs (rtrancl_into_trancl1::prems))));
   7.165 -qed "trancl_induct";
   7.166 -
   7.167 -(*elimination of r^+ -- NOT an induction rule*)
   7.168 -val major::prems = Goal
   7.169 -    "[| <a,b> : r^+;  \
   7.170 -\       <a,b> : r ==> P; \
   7.171 -\       !!y.[| <a,y> : r^+; <y,b> : r |] ==> P  \
   7.172 -\    |] ==> P";
   7.173 -by (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+  &  <y,b> : r)" 1);
   7.174 -by (fast_tac (claset() addIs prems) 1);
   7.175 -by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
   7.176 -by (etac rtranclE 1);
   7.177 -by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_trancl1])));
   7.178 -qed "tranclE";
   7.179 -
   7.180 -Goalw [trancl_def] "r^+ <= field(r)*field(r)";
   7.181 -by (blast_tac (claset() addEs [rtrancl_type RS subsetD RS SigmaE2]) 1);
   7.182 -qed "trancl_type";
   7.183 -
   7.184 -Goalw [trancl_def] "r<=s ==> r^+ <= s^+";
   7.185 -by (REPEAT (ares_tac [comp_mono, rtrancl_mono] 1));
   7.186 -qed "trancl_mono";
   7.187 -
   7.188 -(** Suggested by Sidi Ould Ehmety **)
   7.189 -
   7.190 -Goal "(r^*)^* = r^*";
   7.191 -by (rtac equalityI 1);
   7.192 -by Auto_tac;
   7.193 -by (ALLGOALS (forward_tac [impOfSubs rtrancl_type]));
   7.194 -by (ALLGOALS Clarify_tac);
   7.195 -by (etac r_into_rtrancl 2);
   7.196 -by (etac rtrancl_induct 1);
   7.197 -by (asm_full_simp_tac (simpset() addsimps [rtrancl_refl, rtrancl_field]) 1);
   7.198 -by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   7.199 -qed "rtrancl_idemp";
   7.200 -Addsimps [rtrancl_idemp];
   7.201 -
   7.202 -Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
   7.203 -by (dtac rtrancl_mono 1);
   7.204 -by (dtac rtrancl_mono 1);
   7.205 -by (ALLGOALS Asm_full_simp_tac);
   7.206 -by (Blast_tac 1);
   7.207 -qed "rtrancl_subset";
   7.208 -
   7.209 -Goal "[| r<= Sigma(A,B); s<=Sigma(C,D) |] ==> (r^* Un s^*)^* = (r Un s)^*";
   7.210 -by (rtac rtrancl_subset 1);
   7.211 -by (blast_tac (claset() addDs [r_subset_rtrancl]) 1);
   7.212 -by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
   7.213 -qed "rtrancl_Un_rtrancl";
   7.214 -
   7.215 -(*** "converse" laws by Sidi Ould Ehmety ***)
   7.216 -
   7.217 -(** rtrancl **)
   7.218 -
   7.219 -Goal "<x,y>:converse(r)^* ==> <x,y>:converse(r^*)";
   7.220 -by (rtac converseI 1);
   7.221 -by (forward_tac [rtrancl_type RS subsetD] 1);
   7.222 -by (etac rtrancl_induct 1);
   7.223 -by (blast_tac (claset() addIs [rtrancl_refl]) 1);
   7.224 -by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
   7.225 -qed "rtrancl_converseD";
   7.226 -
   7.227 -Goal "<x,y>:converse(r^*) ==> <x,y>:converse(r)^*";
   7.228 -by (dtac converseD 1);
   7.229 -by (forward_tac [rtrancl_type RS subsetD] 1);
   7.230 -by (etac rtrancl_induct 1);
   7.231 -by (blast_tac (claset() addIs [rtrancl_refl]) 1);
   7.232 -by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
   7.233 -qed "rtrancl_converseI";
   7.234 -
   7.235 -Goal "converse(r)^* = converse(r^*)";
   7.236 -by (safe_tac (claset() addSIs [equalityI]));
   7.237 -by (forward_tac [rtrancl_type RS subsetD] 1);
   7.238 -by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
   7.239 -qed "rtrancl_converse";
   7.240 -
   7.241 -(** trancl **)
   7.242 -
   7.243 -Goal "<a, b>:converse(r)^+ ==> <a, b>:converse(r^+)";
   7.244 -by (etac trancl_induct 1);
   7.245 -by (auto_tac (claset() addIs [r_into_trancl, trancl_trans], simpset()));
   7.246 -qed "trancl_converseD";
   7.247 -
   7.248 -Goal "<x,y>:converse(r^+) ==> <x,y>:converse(r)^+";
   7.249 -by (dtac converseD 1);
   7.250 -by (etac trancl_induct 1);
   7.251 -by (auto_tac (claset() addIs [r_into_trancl, trancl_trans], simpset()));
   7.252 -qed "trancl_converseI";
   7.253 -
   7.254 -Goal "converse(r)^+ = converse(r^+)";
   7.255 -by (safe_tac (claset() addSIs [equalityI]));
   7.256 -by (forward_tac [trancl_type RS subsetD] 1);
   7.257 -by (safe_tac (claset() addSDs [trancl_converseD] addSIs [trancl_converseI]));
   7.258 -qed "trancl_converse";
   7.259 -
   7.260 -val major::prems = Goal 
   7.261 -"[| <a, b>:r^+; !!y. <y, b> :r ==> P(y); \
   7.262 -\     !!y z. [| <y, z> : r; <z, b> : r^+; P(z) |] ==> P(y) |] \
   7.263 -\      ==> P(a)";
   7.264 -by (cut_facts_tac [major] 1);
   7.265 -by (dtac converseI 1);
   7.266 -by (full_simp_tac (simpset() addsimps [trancl_converse RS sym]) 1);
   7.267 -by (etac trancl_induct 1);
   7.268 -by (auto_tac (claset() addIs prems, 
   7.269 -              simpset() addsimps [trancl_converse]));
   7.270 -qed "converse_trancl_induct";
     8.1 --- a/src/ZF/Trancl.thy	Fri Jun 21 18:40:06 2002 +0200
     8.2 +++ b/src/ZF/Trancl.thy	Sat Jun 22 18:28:46 2002 +0200
     8.3 @@ -3,15 +3,422 @@
     8.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.5      Copyright   1992  University of Cambridge
     8.6  
     8.7 -Transitive closure of a relation
     8.8 +1. General Properties of relations
     8.9 +2. Transitive closure of a relation
    8.10  *)
    8.11  
    8.12 -Trancl = Fixedpt + Perm + mono + Rel + 
    8.13 -consts
    8.14 -    rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
    8.15 -    trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
    8.16 +theory Trancl = Fixedpt + Perm + mono:
    8.17 +
    8.18 +constdefs
    8.19 +  refl     :: "[i,i]=>o"
    8.20 +    "refl(A,r) == (ALL x: A. <x,x> : r)"
    8.21 +
    8.22 +  irrefl   :: "[i,i]=>o"
    8.23 +    "irrefl(A,r) == ALL x: A. <x,x> ~: r"
    8.24 +
    8.25 +  equiv    :: "[i,i]=>o"
    8.26 +    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
    8.27 +
    8.28 +  sym      :: "i=>o"
    8.29 +    "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
    8.30 +
    8.31 +  asym     :: "i=>o"
    8.32 +    "asym(r) == ALL x y. <x,y>:r --> ~ <y,x>:r"
    8.33 +
    8.34 +  antisym  :: "i=>o"
    8.35 +    "antisym(r) == ALL x y.<x,y>:r --> <y,x>:r --> x=y"
    8.36 +
    8.37 +  trans    :: "i=>o"
    8.38 +    "trans(r) == ALL x y z. <x,y>: r --> <y,z>: r --> <x,z>: r"
    8.39 +
    8.40 +  trans_on :: "[i,i]=>o"  ("trans[_]'(_')")
    8.41 +    "trans[A](r) == ALL x:A. ALL y:A. ALL z:A.       
    8.42 +                          <x,y>: r --> <y,z>: r --> <x,z>: r"
    8.43 +
    8.44 +  rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
    8.45 +    "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
    8.46 +
    8.47 +  trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
    8.48 +    "r^+ == r O r^*"
    8.49 +
    8.50 +subsection{*General properties of relations*}
    8.51 +
    8.52 +subsubsection{*irreflexivity*}
    8.53 +
    8.54 +lemma irreflI:
    8.55 +    "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)"
    8.56 +by (simp add: irrefl_def); 
    8.57 +
    8.58 +lemma symI: "[| irrefl(A,r);  x:A |] ==>  <x,x> ~: r"
    8.59 +apply (simp add: irrefl_def)
    8.60 +done
    8.61 +
    8.62 +subsubsection{*symmetry*}
    8.63 +
    8.64 +lemma symI:
    8.65 +     "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)"
    8.66 +apply (unfold sym_def); 
    8.67 +apply (blast intro: elim:); 
    8.68 +done
    8.69 +
    8.70 +lemma antisymI: "[| sym(r); <x,y>: r |]  ==>  <y,x>: r"
    8.71 +apply (unfold sym_def)
    8.72 +apply blast
    8.73 +done
    8.74 +
    8.75 +subsubsection{*antisymmetry*}
    8.76 +
    8.77 +lemma antisymI:
    8.78 +     "[| !!x y.[| <x,y>: r;  <y,x>: r |] ==> x=y |] ==> antisym(r)"
    8.79 +apply (simp add: antisym_def) 
    8.80 +apply (blast intro: elim:); 
    8.81 +done
    8.82 +
    8.83 +lemma antisymE: "[| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y"
    8.84 +apply (simp add: antisym_def)
    8.85 +apply blast
    8.86 +done
    8.87 +
    8.88 +subsubsection{*transitivity*}
    8.89 +
    8.90 +lemma transD: "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r"
    8.91 +apply (unfold trans_def)
    8.92 +apply blast
    8.93 +done
    8.94 +
    8.95 +lemma trans_onD: 
    8.96 +    "[| trans[A](r);  <a,b>:r;  <b,c>:r;  a:A;  b:A;  c:A |] ==> <a,c>:r"
    8.97 +apply (unfold trans_on_def)
    8.98 +apply blast
    8.99 +done
   8.100 +
   8.101 +subsection{*Transitive closure of a relation*}
   8.102 +
   8.103 +lemma rtrancl_bnd_mono:
   8.104 +     "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))"
   8.105 +apply (rule bnd_monoI)
   8.106 +apply (blast intro: elim:)+
   8.107 +done
   8.108 +
   8.109 +lemma rtrancl_mono: "r<=s ==> r^* <= s^*"
   8.110 +apply (unfold rtrancl_def)
   8.111 +apply (rule lfp_mono)
   8.112 +apply (rule rtrancl_bnd_mono)+
   8.113 +apply (blast intro: elim:); 
   8.114 +done
   8.115 +
   8.116 +(* r^* = id(field(r)) Un ( r O r^* )    *)
   8.117 +lemmas rtrancl_unfold =
   8.118 +     rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold], standard]
   8.119 +
   8.120 +(** The relation rtrancl **)
   8.121 +
   8.122 +(*  r^* <= field(r) * field(r)  *)
   8.123 +lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset, standard]
   8.124 +
   8.125 +(*Reflexivity of rtrancl*)
   8.126 +lemma rtrancl_refl: "[| a: field(r) |] ==> <a,a> : r^*"
   8.127 +apply (rule rtrancl_unfold [THEN ssubst])
   8.128 +apply (erule idI [THEN UnI1])
   8.129 +done
   8.130 +
   8.131 +(*Closure under composition with r  *)
   8.132 +lemma rtrancl_into_rtrancl: "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*"
   8.133 +apply (rule rtrancl_unfold [THEN ssubst])
   8.134 +apply (rule compI [THEN UnI2])
   8.135 +apply assumption
   8.136 +apply assumption
   8.137 +done
   8.138 +
   8.139 +(*rtrancl of r contains all pairs in r  *)
   8.140 +lemma r_into_rtrancl: "<a,b> : r ==> <a,b> : r^*"
   8.141 +apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
   8.142 +apply (blast intro: elim:)+
   8.143 +done
   8.144 +
   8.145 +(*The premise ensures that r consists entirely of pairs*)
   8.146 +lemma r_subset_rtrancl: "r <= Sigma(A,B) ==> r <= r^*"
   8.147 +apply (blast intro: r_into_rtrancl)
   8.148 +done
   8.149 +
   8.150 +lemma rtrancl_field: "field(r^*) = field(r)"
   8.151 +apply (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD])
   8.152 +done
   8.153 +
   8.154 +
   8.155 +(** standard induction rule **)
   8.156 +
   8.157 +lemma rtrancl_full_induct:
   8.158 +  "[| <a,b> : r^*;  
   8.159 +      !!x. x: field(r) ==> P(<x,x>);  
   8.160 +      !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |]  
   8.161 +   ==>  P(<a,b>)"
   8.162 +apply (erule def_induct [OF rtrancl_def rtrancl_bnd_mono])
   8.163 +apply (blast intro: elim:); 
   8.164 +done
   8.165 +
   8.166 +(*nice induction rule.
   8.167 +  Tried adding the typing hypotheses y,z:field(r), but these
   8.168 +  caused expensive case splits!*)
   8.169 +lemma rtrancl_induct:
   8.170 +  "[| <a,b> : r^*;                                               
   8.171 +      P(a);                                                      
   8.172 +      !!y z.[| <a,y> : r^*;  <y,z> : r;  P(y) |] ==> P(z)        
   8.173 +   |] ==> P(b)"
   8.174 +(*by induction on this formula*)
   8.175 +apply (subgoal_tac "ALL y. <a,b> = <a,y> --> P (y) ")
   8.176 +(*now solve first subgoal: this formula is sufficient*)
   8.177 +apply (erule spec [THEN mp], rule refl)
   8.178 +(*now do the induction*)
   8.179 +apply (erule rtrancl_full_induct)
   8.180 +apply (blast)+
   8.181 +done
   8.182 +
   8.183 +(*transitivity of transitive closure!! -- by induction.*)
   8.184 +lemma trans_rtrancl: "trans(r^*)"
   8.185 +apply (unfold trans_def)
   8.186 +apply (intro allI impI)
   8.187 +apply (erule_tac b = "z" in rtrancl_induct)
   8.188 +apply assumption; 
   8.189 +apply (blast intro: rtrancl_into_rtrancl) 
   8.190 +done
   8.191 +
   8.192 +lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
   8.193 +
   8.194 +(*elimination of rtrancl -- by induction on a special formula*)
   8.195 +lemma rtranclE:
   8.196 +    "[| <a,b> : r^*;  (a=b) ==> P;                        
   8.197 +        !!y.[| <a,y> : r^*;   <y,b> : r |] ==> P |]       
   8.198 +     ==> P"
   8.199 +apply (subgoal_tac "a = b | (EX y. <a,y> : r^* & <y,b> : r) ")
   8.200 +(*see HOL/trancl*)
   8.201 +apply (blast intro: elim:); 
   8.202 +apply (erule rtrancl_induct)
   8.203 +apply (blast intro: elim:)+
   8.204 +done
   8.205 +
   8.206 +
   8.207 +(**** The relation trancl ****)
   8.208 +
   8.209 +(*Transitivity of r^+ is proved by transitivity of r^*  *)
   8.210 +lemma trans_trancl: "trans(r^+)"
   8.211 +apply (unfold trans_def trancl_def)
   8.212 +apply (blast intro: rtrancl_into_rtrancl
   8.213 +                    trans_rtrancl [THEN transD, THEN compI])
   8.214 +done
   8.215 +
   8.216 +lemmas trancl_trans = trans_trancl [THEN transD, standard]
   8.217 +
   8.218 +(** Conversions between trancl and rtrancl **)
   8.219  
   8.220 -defs
   8.221 -    rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
   8.222 -    trancl_def  "r^+ == r O r^*"
   8.223 +lemma trancl_into_rtrancl: "<a,b> : r^+ ==> <a,b> : r^*"
   8.224 +apply (unfold trancl_def)
   8.225 +apply (blast intro: rtrancl_into_rtrancl)
   8.226 +done
   8.227 +
   8.228 +(*r^+ contains all pairs in r  *)
   8.229 +lemma r_into_trancl: "<a,b> : r ==> <a,b> : r^+"
   8.230 +apply (unfold trancl_def)
   8.231 +apply (blast intro!: rtrancl_refl)
   8.232 +done
   8.233 +
   8.234 +(*The premise ensures that r consists entirely of pairs*)
   8.235 +lemma r_subset_trancl: "r <= Sigma(A,B) ==> r <= r^+"
   8.236 +apply (blast intro: r_into_trancl)
   8.237 +done
   8.238 +
   8.239 +(*intro rule by definition: from r^* and r  *)
   8.240 +lemma rtrancl_into_trancl1: "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+"
   8.241 +apply (unfold trancl_def)
   8.242 +apply blast
   8.243 +done
   8.244 +
   8.245 +(*intro rule from r and r^*  *)
   8.246 +lemma rtrancl_into_trancl2:
   8.247 +    "[| <a,b> : r;  <b,c> : r^* |]   ==>  <a,c> : r^+"
   8.248 +apply (erule rtrancl_induct)
   8.249 + apply (erule r_into_trancl)
   8.250 +apply (blast intro: r_into_trancl trancl_trans) 
   8.251 +done
   8.252 +
   8.253 +(*Nice induction rule for trancl*)
   8.254 +lemma trancl_induct:
   8.255 +  "[| <a,b> : r^+;                                       
   8.256 +      !!y.  [| <a,y> : r |] ==> P(y);                    
   8.257 +      !!y z.[| <a,y> : r^+;  <y,z> : r;  P(y) |] ==> P(z)        
   8.258 +   |] ==> P(b)"
   8.259 +apply (rule compEpair)
   8.260 +apply (unfold trancl_def, assumption)
   8.261 +(*by induction on this formula*)
   8.262 +apply (subgoal_tac "ALL z. <y,z> : r --> P (z) ")
   8.263 +(*now solve first subgoal: this formula is sufficient*)
   8.264 + apply blast
   8.265 +apply (erule rtrancl_induct)
   8.266 +apply (blast intro: rtrancl_into_trancl1)+
   8.267 +done
   8.268 +
   8.269 +(*elimination of r^+ -- NOT an induction rule*)
   8.270 +lemma tranclE:
   8.271 +    "[| <a,b> : r^+;   
   8.272 +        <a,b> : r ==> P;  
   8.273 +        !!y.[| <a,y> : r^+; <y,b> : r |] ==> P   
   8.274 +     |] ==> P"
   8.275 +apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ & <y,b> : r) ")
   8.276 +apply (blast intro: elim:); 
   8.277 +apply (rule compEpair)
   8.278 +apply (unfold trancl_def, assumption)
   8.279 +apply (erule rtranclE)
   8.280 +apply (blast intro: rtrancl_into_trancl1)+
   8.281 +done
   8.282 +
   8.283 +lemma trancl_type: "r^+ <= field(r)*field(r)"
   8.284 +apply (unfold trancl_def)
   8.285 +apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2])
   8.286 +done
   8.287 +
   8.288 +lemma trancl_mono: "r<=s ==> r^+ <= s^+"
   8.289 +by (unfold trancl_def, intro comp_mono rtrancl_mono)
   8.290 +
   8.291 +
   8.292 +(** Suggested by Sidi Ould Ehmety **)
   8.293 +
   8.294 +lemma rtrancl_idemp [simp]: "(r^*)^* = r^*"
   8.295 +apply (rule equalityI)
   8.296 +apply auto
   8.297 + prefer 2
   8.298 + apply (frule rtrancl_type [THEN subsetD])
   8.299 + apply (blast intro: r_into_rtrancl elim:); 
   8.300 +txt{*converse direction*}
   8.301 +apply (frule rtrancl_type [THEN subsetD])
   8.302 +apply (clarify ); 
   8.303 +apply (erule rtrancl_induct)
   8.304 +apply (simp add: rtrancl_refl rtrancl_field)
   8.305 +apply (blast intro: rtrancl_trans)
   8.306 +done
   8.307 +
   8.308 +lemma rtrancl_subset: "[| R <= S; S <= R^* |] ==> S^* = R^*"
   8.309 +apply (drule rtrancl_mono)
   8.310 +apply (drule rtrancl_mono)
   8.311 +apply simp_all
   8.312 +apply blast
   8.313 +done
   8.314 +
   8.315 +lemma rtrancl_Un_rtrancl:
   8.316 +     "[| r<= Sigma(A,B); s<=Sigma(C,D) |] ==> (r^* Un s^*)^* = (r Un s)^*"
   8.317 +apply (rule rtrancl_subset)
   8.318 +apply (blast dest: r_subset_rtrancl)
   8.319 +apply (blast intro: rtrancl_mono [THEN subsetD])
   8.320 +done
   8.321 +
   8.322 +(*** "converse" laws by Sidi Ould Ehmety ***)
   8.323 +
   8.324 +(** rtrancl **)
   8.325 +
   8.326 +lemma rtrancl_converseD: "<x,y>:converse(r)^* ==> <x,y>:converse(r^*)"
   8.327 +apply (rule converseI)
   8.328 +apply (frule rtrancl_type [THEN subsetD])
   8.329 +apply (erule rtrancl_induct)
   8.330 +apply (blast intro: rtrancl_refl)
   8.331 +apply (blast intro: r_into_rtrancl rtrancl_trans)
   8.332 +done
   8.333 +
   8.334 +lemma rtrancl_converseI: "<x,y>:converse(r^*) ==> <x,y>:converse(r)^*"
   8.335 +apply (drule converseD)
   8.336 +apply (frule rtrancl_type [THEN subsetD])
   8.337 +apply (erule rtrancl_induct)
   8.338 +apply (blast intro: rtrancl_refl)
   8.339 +apply (blast intro: r_into_rtrancl rtrancl_trans)
   8.340 +done
   8.341 +
   8.342 +lemma rtrancl_converse: "converse(r)^* = converse(r^*)"
   8.343 +apply (safe intro!: equalityI)
   8.344 +apply (frule rtrancl_type [THEN subsetD])
   8.345 +apply (safe dest!: rtrancl_converseD intro!: rtrancl_converseI)
   8.346 +done
   8.347 +
   8.348 +(** trancl **)
   8.349 +
   8.350 +lemma trancl_converseD: "<a, b>:converse(r)^+ ==> <a, b>:converse(r^+)"
   8.351 +apply (erule trancl_induct)
   8.352 +apply (auto intro: r_into_trancl trancl_trans)
   8.353 +done
   8.354 +
   8.355 +lemma trancl_converseI: "<x,y>:converse(r^+) ==> <x,y>:converse(r)^+"
   8.356 +apply (drule converseD)
   8.357 +apply (erule trancl_induct)
   8.358 +apply (auto intro: r_into_trancl trancl_trans)
   8.359 +done
   8.360 +
   8.361 +lemma trancl_converse: "converse(r)^+ = converse(r^+)"
   8.362 +apply (safe intro!: equalityI)
   8.363 +apply (frule trancl_type [THEN subsetD])
   8.364 +apply (safe dest!: trancl_converseD intro!: trancl_converseI)
   8.365 +done
   8.366 +
   8.367 +lemma converse_trancl_induct:
   8.368 +"[| <a, b>:r^+; !!y. <y, b> :r ==> P(y);  
   8.369 +      !!y z. [| <y, z> : r; <z, b> : r^+; P(z) |] ==> P(y) |]  
   8.370 +       ==> P(a)"
   8.371 +apply (drule converseI)
   8.372 +apply (simp (no_asm_use) add: trancl_converse [symmetric])
   8.373 +apply (erule trancl_induct)
   8.374 +apply (auto simp add: trancl_converse)
   8.375 +done
   8.376 +
   8.377 +ML
   8.378 +{*
   8.379 +val refl_def = thm "refl_def";
   8.380 +val irrefl_def = thm "irrefl_def";
   8.381 +val equiv_def = thm "equiv_def";
   8.382 +val sym_def = thm "sym_def";
   8.383 +val asym_def = thm "asym_def";
   8.384 +val antisym_def = thm "antisym_def";
   8.385 +val trans_def = thm "trans_def";
   8.386 +val trans_on_def = thm "trans_on_def";
   8.387 +
   8.388 +val irreflI = thm "irreflI";
   8.389 +val symI = thm "symI";
   8.390 +val symI = thm "symI";
   8.391 +val antisymI = thm "antisymI";
   8.392 +val antisymE = thm "antisymE";
   8.393 +val transD = thm "transD";
   8.394 +val trans_onD = thm "trans_onD";
   8.395 +
   8.396 +val rtrancl_bnd_mono = thm "rtrancl_bnd_mono";
   8.397 +val rtrancl_mono = thm "rtrancl_mono";
   8.398 +val rtrancl_unfold = thm "rtrancl_unfold";
   8.399 +val rtrancl_type = thm "rtrancl_type";
   8.400 +val rtrancl_refl = thm "rtrancl_refl";
   8.401 +val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
   8.402 +val r_into_rtrancl = thm "r_into_rtrancl";
   8.403 +val r_subset_rtrancl = thm "r_subset_rtrancl";
   8.404 +val rtrancl_field = thm "rtrancl_field";
   8.405 +val rtrancl_full_induct = thm "rtrancl_full_induct";
   8.406 +val rtrancl_induct = thm "rtrancl_induct";
   8.407 +val trans_rtrancl = thm "trans_rtrancl";
   8.408 +val rtrancl_trans = thm "rtrancl_trans";
   8.409 +val rtranclE = thm "rtranclE";
   8.410 +val trans_trancl = thm "trans_trancl";
   8.411 +val trancl_trans = thm "trancl_trans";
   8.412 +val trancl_into_rtrancl = thm "trancl_into_rtrancl";
   8.413 +val r_into_trancl = thm "r_into_trancl";
   8.414 +val r_subset_trancl = thm "r_subset_trancl";
   8.415 +val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1";
   8.416 +val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2";
   8.417 +val trancl_induct = thm "trancl_induct";
   8.418 +val tranclE = thm "tranclE";
   8.419 +val trancl_type = thm "trancl_type";
   8.420 +val trancl_mono = thm "trancl_mono";
   8.421 +val rtrancl_idemp = thm "rtrancl_idemp";
   8.422 +val rtrancl_subset = thm "rtrancl_subset";
   8.423 +val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl";
   8.424 +val rtrancl_converseD = thm "rtrancl_converseD";
   8.425 +val rtrancl_converseI = thm "rtrancl_converseI";
   8.426 +val rtrancl_converse = thm "rtrancl_converse";
   8.427 +val trancl_converseD = thm "trancl_converseD";
   8.428 +val trancl_converseI = thm "trancl_converseI";
   8.429 +val trancl_converse = thm "trancl_converse";
   8.430 +val converse_trancl_induct = thm "converse_trancl_induct";
   8.431 +*}
   8.432 +
   8.433  end