new version of HOL/Integ with curried function application
authorclasohm
Fri Mar 03 12:04:45 1995 +0100 (1995-03-03)
changeset 92515539deb6863
parent 924 806721cfbf46
child 926 9d1348498c36
new version of HOL/Integ with curried function application
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Equiv.thy
src/HOL/Integ/Integ.ML
src/HOL/Integ/Integ.thy
src/HOL/Integ/ROOT.ML
src/HOL/Integ/Relation.ML
src/HOL/Integ/Relation.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/Equiv.ML	Fri Mar 03 12:04:45 1995 +0100
     1.3 @@ -0,0 +1,311 @@
     1.4 +(*  Title: 	Equiv.ML
     1.5 +    ID:         $Id$
     1.6 +    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
     1.7 +        	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Copyright   1994 Universita' di Firenze
     1.9 +    Copyright   1993  University of Cambridge
    1.10 +
    1.11 +Equivalence relations in HOL Set Theory 
    1.12 +*)
    1.13 +
    1.14 +open Equiv;
    1.15 +
    1.16 +(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***)
    1.17 +
    1.18 +(** first half: equiv A r ==> converse(r) O r = r **)
    1.19 +
    1.20 +goalw Equiv.thy [trans_def,sym_def,converse_def]
    1.21 +    "!!r. [| sym(r); trans(r) |] ==> converse(r) O r <= r";
    1.22 +by (fast_tac (comp_cs addSEs [converseD]) 1);
    1.23 +qed "sym_trans_comp_subset";
    1.24 +
    1.25 +val [major,minor]=goal Equiv.thy "[|<x,y>:r; z=<x,y>|] ==>  z:r";
    1.26 +by (simp_tac (prod_ss addsimps [minor]) 1);
    1.27 +by (rtac major 1);
    1.28 +qed "BreakPair";
    1.29 +
    1.30 +val [major]=goal Equiv.thy "[|? x y. <x,y>:r & z=<x,y>|] ==>  z:r";
    1.31 +by (resolve_tac [major RS exE] 1);
    1.32 +by (etac exE 1);
    1.33 +by (etac conjE 1);
    1.34 +by (asm_simp_tac (prod_ss addsimps [minor]) 1);
    1.35 +qed "BreakPair1";
    1.36 +
    1.37 +val [major,minor]=goal Equiv.thy "[|z:r; z=<x,y>|] ==> <x,y>:r";
    1.38 +by (simp_tac (prod_ss addsimps [minor RS sym]) 1);
    1.39 +by (rtac major 1);
    1.40 +qed "BuildPair";
    1.41 +
    1.42 +val [major]=goal Equiv.thy "[|? z:r. <x,y>=z|] ==> <x,y>:r";
    1.43 +by (resolve_tac [major RS bexE] 1);
    1.44 +by (asm_simp_tac (prod_ss addsimps []) 1);
    1.45 +qed "BuildPair1";
    1.46 +
    1.47 +val rel_pair_cs = rel_cs addIs [BuildPair1] 
    1.48 +                         addEs [BreakPair1];
    1.49 +
    1.50 +goalw Equiv.thy [refl_def,converse_def]
    1.51 +    "!!A r. refl A r ==> r <= converse(r) O r";
    1.52 +by (step_tac comp_cs 1);
    1.53 +by (dtac subsetD 1);
    1.54 +by (assume_tac 1);
    1.55 +by (etac SigmaE 1);
    1.56 +by (rtac BreakPair1 1);
    1.57 +by (fast_tac comp_cs 1);
    1.58 +qed "refl_comp_subset";
    1.59 +
    1.60 +goalw Equiv.thy [equiv_def]
    1.61 +    "!!A r. equiv A r ==> converse(r) O r = r";
    1.62 +by (rtac equalityI 1);
    1.63 +by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1
    1.64 +     ORELSE etac conjE 1));
    1.65 +qed "equiv_comp_eq";
    1.66 +
    1.67 +(*second half*)
    1.68 +goalw Equiv.thy [equiv_def,refl_def,sym_def,trans_def]
    1.69 +    "!!A r. [| converse(r) O r = r;  Domain(r) = A |] ==> equiv A r";
    1.70 +by (etac equalityE 1);
    1.71 +by (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r" 1);
    1.72 +by (safe_tac set_cs);
    1.73 +by (fast_tac (set_cs addSIs [converseI] addIs [compI]) 3);
    1.74 +by (fast_tac (set_cs addSIs [converseI] addIs [compI] addSEs [DomainE]) 2);
    1.75 +by (fast_tac (rel_pair_cs addSEs [SigmaE] addSIs [SigmaI]) 1);
    1.76 +by (dtac subsetD 1);
    1.77 +by (dtac subsetD 1);
    1.78 +by (fast_tac rel_cs 1);
    1.79 +by (fast_tac rel_cs 1);
    1.80 +by flexflex_tac;
    1.81 +by (dtac subsetD 1);
    1.82 +by (fast_tac converse_cs 2);
    1.83 +by (fast_tac converse_cs 1);
    1.84 +qed "comp_equivI";
    1.85 +
    1.86 +(** Equivalence classes **)
    1.87 +
    1.88 +(*Lemma for the next result*)
    1.89 +goalw Equiv.thy [equiv_def,trans_def,sym_def]
    1.90 +    "!!A r. [| equiv A r;  <a,b>: r |] ==> r^^{a} <= r^^{b}";
    1.91 +by (safe_tac rel_cs);
    1.92 +by (rtac ImageI 1);
    1.93 +by (fast_tac rel_cs 2);
    1.94 +by (fast_tac rel_cs 1);
    1.95 +qed "equiv_class_subset";
    1.96 +
    1.97 +goal Equiv.thy "!!A r. [| equiv A r;  <a,b>: r |] ==> r^^{a} = r^^{b}";
    1.98 +by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
    1.99 +by (rewrite_goals_tac [equiv_def,sym_def]);
   1.100 +by (fast_tac rel_cs 1);
   1.101 +qed "equiv_class_eq";
   1.102 +
   1.103 +val prems = goalw Equiv.thy [equiv_def,refl_def]
   1.104 +    "[| equiv A r;  a: A |] ==> a: r^^{a}";
   1.105 +by (cut_facts_tac prems 1);
   1.106 +by (fast_tac rel_cs 1);
   1.107 +qed "equiv_class_self";
   1.108 +
   1.109 +(*Lemma for the next result*)
   1.110 +goalw Equiv.thy [equiv_def,refl_def]
   1.111 +    "!!A r. [| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> <a,b>: r";
   1.112 +by (fast_tac rel_cs 1);
   1.113 +qed "subset_equiv_class";
   1.114 +
   1.115 +val prems = goal Equiv.thy
   1.116 +    "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> <a,b>: r";
   1.117 +by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1));
   1.118 +qed "eq_equiv_class";
   1.119 +
   1.120 +(*thus r^^{a} = r^^{b} as well*)
   1.121 +goalw Equiv.thy [equiv_def,trans_def,sym_def]
   1.122 +    "!!A r. [| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> <a,b>: r";
   1.123 +by (fast_tac rel_cs 1);
   1.124 +qed "equiv_class_nondisjoint";
   1.125 +
   1.126 +val [major] = goalw Equiv.thy [equiv_def,refl_def]
   1.127 +    "equiv A r ==> r <= Sigma A (%x.A)";
   1.128 +by (rtac (major RS conjunct1 RS conjunct1) 1);
   1.129 +qed "equiv_type";
   1.130 +
   1.131 +goal Equiv.thy
   1.132 +    "!!A r. equiv A r ==> (<x,y>: r) = (r^^{x} = r^^{y} & x:A & y:A)";
   1.133 +by (safe_tac rel_cs);
   1.134 +by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1));
   1.135 +by ((rtac eq_equiv_class 3) THEN 
   1.136 +    (assume_tac 4) THEN (assume_tac 4) THEN (assume_tac 3));
   1.137 +by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN
   1.138 +    (assume_tac 1) THEN (dtac SigmaD1 1) THEN (assume_tac 1));
   1.139 +by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN
   1.140 +    (assume_tac 1) THEN (dtac SigmaD2 1) THEN (assume_tac 1));
   1.141 +qed "equiv_class_eq_iff";
   1.142 +
   1.143 +goal Equiv.thy
   1.144 +    "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = (<x,y>: r)";
   1.145 +by (safe_tac rel_cs);
   1.146 +by ((rtac eq_equiv_class 1) THEN 
   1.147 +    (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1));
   1.148 +by ((rtac equiv_class_eq 1) THEN 
   1.149 +    (assume_tac 1) THEN (assume_tac 1));
   1.150 +qed "eq_equiv_class_iff";
   1.151 +
   1.152 +(*** Quotients ***)
   1.153 +
   1.154 +(** Introduction/elimination rules -- needed? **)
   1.155 +
   1.156 +val prems = goalw Equiv.thy [quotient_def] "x:A ==> r^^{x}: A/r";
   1.157 +by (rtac UN_I 1);
   1.158 +by (resolve_tac prems 1);
   1.159 +by (rtac singletonI 1);
   1.160 +qed "quotientI";
   1.161 +
   1.162 +val [major,minor] = goalw Equiv.thy [quotient_def]
   1.163 +    "[| X:(A/r);  !!x. [| X = r^^{x};  x:A |] ==> P |] 	\
   1.164 +\    ==> P";
   1.165 +by (resolve_tac [major RS UN_E] 1);
   1.166 +by (rtac minor 1);
   1.167 +by (assume_tac 2);
   1.168 +by (fast_tac rel_cs 1);
   1.169 +qed "quotientE";
   1.170 +
   1.171 +(** Not needed by Theory Integ --> bypassed **)
   1.172 +(**goalw Equiv.thy [equiv_def,refl_def,quotient_def]
   1.173 +    "!!A r. equiv A r ==> Union(A/r) = A";
   1.174 +by (fast_tac eq_cs 1);
   1.175 +qed "Union_quotient";
   1.176 +**)
   1.177 +
   1.178 +(** Not needed by Theory Integ --> bypassed **)
   1.179 +(*goalw Equiv.thy [quotient_def]
   1.180 +    "!!A r. [| equiv A r;  X: A/r;  Y: A/r |] ==> X=Y | (X Int Y <= 0)";
   1.181 +by (safe_tac (ZF_cs addSIs [equiv_class_eq]));
   1.182 +by (assume_tac 1);
   1.183 +by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
   1.184 +by (fast_tac ZF_cs 1);
   1.185 +qed "quotient_disj";
   1.186 +**)
   1.187 +
   1.188 +(**** Defining unary operations upon equivalence classes ****)
   1.189 +
   1.190 +(* theorem needed to prove UN_equiv_class *)
   1.191 +goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)";
   1.192 +by (fast_tac (eq_cs addSEs [equalityE]) 1);
   1.193 +qed "UN_singleton_lemma";
   1.194 +val UN_singleton = ballI RSN (2,UN_singleton_lemma);
   1.195 +
   1.196 +
   1.197 +(** These proofs really require as local premises
   1.198 +     equiv A r;  congruent r b
   1.199 +**)
   1.200 +
   1.201 +(*Conversion rule*)
   1.202 +val prems as [equivA,bcong,_] = goal Equiv.thy
   1.203 +    "[| equiv A r;  congruent r b;  a: A |] ==> (UN x:r^^{a}. b(x)) = b(a)";
   1.204 +by (cut_facts_tac prems 1);
   1.205 +by (rtac UN_singleton 1);
   1.206 +by (rtac equiv_class_self 1);
   1.207 +by (assume_tac 1);
   1.208 +by (assume_tac 1);
   1.209 +by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
   1.210 +by (fast_tac rel_cs 1);
   1.211 +qed "UN_equiv_class";
   1.212 +
   1.213 +(*Resolve th against the "local" premises*)
   1.214 +val localize = RSLIST [equivA,bcong];
   1.215 +
   1.216 +(*type checking of  UN x:r``{a}. b(x) *)
   1.217 +val _::_::prems = goalw Equiv.thy [quotient_def]
   1.218 +    "[| equiv A r;  congruent r b;  X: A/r;	\
   1.219 +\	!!x.  x : A ==> b(x) : B |] 	\
   1.220 +\    ==> (UN x:X. b(x)) : B";
   1.221 +by (cut_facts_tac prems 1);
   1.222 +by (safe_tac rel_cs);
   1.223 +by (rtac (localize UN_equiv_class RS ssubst) 1);
   1.224 +by (REPEAT (ares_tac prems 1));
   1.225 +qed "UN_equiv_class_type";
   1.226 +
   1.227 +(*Sufficient conditions for injectiveness.  Could weaken premises!
   1.228 +  major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
   1.229 +*)
   1.230 +val _::_::prems = goalw Equiv.thy [quotient_def]
   1.231 +    "[| equiv A r;   congruent r b;  \
   1.232 +\       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;  \
   1.233 +\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] 	\
   1.234 +\    ==> X=Y";
   1.235 +by (cut_facts_tac prems 1);
   1.236 +by (safe_tac rel_cs);
   1.237 +by (rtac (equivA RS equiv_class_eq) 1);
   1.238 +by (REPEAT (ares_tac prems 1));
   1.239 +by (etac box_equals 1);
   1.240 +by (REPEAT (ares_tac [localize UN_equiv_class] 1));
   1.241 +qed "UN_equiv_class_inject";
   1.242 +
   1.243 +
   1.244 +(**** Defining binary operations upon equivalence classes ****)
   1.245 +
   1.246 +
   1.247 +goalw Equiv.thy [congruent_def,congruent2_def,equiv_def,refl_def]
   1.248 +    "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> congruent r (b a)";
   1.249 +by (fast_tac rel_cs 1);
   1.250 +qed "congruent2_implies_congruent";
   1.251 +
   1.252 +val equivA::prems = goalw Equiv.thy [congruent_def]
   1.253 +    "[| equiv A r;  congruent2 r b;  a: A |] ==> \
   1.254 +\    congruent r (%x1. UN x2:r^^{a}. b x1 x2)";
   1.255 +by (cut_facts_tac (equivA::prems) 1);
   1.256 +by (safe_tac rel_cs);
   1.257 +by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
   1.258 +by (assume_tac 1);
   1.259 +by (asm_simp_tac (prod_ss addsimps [equivA RS UN_equiv_class,
   1.260 +				 congruent2_implies_congruent]) 1);
   1.261 +by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
   1.262 +by (fast_tac rel_cs 1);
   1.263 +qed "congruent2_implies_congruent_UN";
   1.264 +
   1.265 +val prems as equivA::_ = goal Equiv.thy
   1.266 +    "[| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
   1.267 +\    ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2";
   1.268 +by (cut_facts_tac prems 1);
   1.269 +by (asm_simp_tac (prod_ss addsimps [equivA RS UN_equiv_class,
   1.270 +				    congruent2_implies_congruent,
   1.271 +				    congruent2_implies_congruent_UN]) 1);
   1.272 +qed "UN_equiv_class2";
   1.273 +
   1.274 +(*type checking*)
   1.275 +val prems = goalw Equiv.thy [quotient_def]
   1.276 +    "[| equiv A r;  congruent2 r b;  \
   1.277 +\       X1: A/r;  X2: A/r;	\
   1.278 +\	!!x1 x2.  [| x1: A; x2: A |] ==> b x1 x2 : B |]    \
   1.279 +\    ==> (UN x1:X1. UN x2:X2. b x1 x2) : B";
   1.280 +by (cut_facts_tac prems 1);
   1.281 +by (safe_tac rel_cs);
   1.282 +by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
   1.283 +			     congruent2_implies_congruent_UN,
   1.284 +			     congruent2_implies_congruent, quotientI]) 1));
   1.285 +qed "UN_equiv_class_type2";
   1.286 +
   1.287 +
   1.288 +(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
   1.289 +  than the direct proof*)
   1.290 +val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def]
   1.291 +    "[| equiv A r;	\
   1.292 +\       !! y z w. [| w: A;  <y,z> : r |] ==> b y w = b z w;      \
   1.293 +\       !! y z w. [| w: A;  <y,z> : r |] ==> b w y = b w z       \
   1.294 +\    |] ==> congruent2 r b";
   1.295 +by (cut_facts_tac prems 1);
   1.296 +by (safe_tac rel_cs);
   1.297 +by (rtac trans 1);
   1.298 +by (REPEAT (ares_tac prems 1
   1.299 +     ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
   1.300 +qed "congruent2I";
   1.301 +
   1.302 +val [equivA,commute,congt] = goal Equiv.thy
   1.303 +    "[| equiv A r;	\
   1.304 +\       !! y z. [| y: A;  z: A |] ==> b y z = b z y;        \
   1.305 +\       !! y z w. [| w: A;  <y,z>: r |] ==> b w y = b w z	\
   1.306 +\    |] ==> congruent2 r b";
   1.307 +by (resolve_tac [equivA RS congruent2I] 1);
   1.308 +by (rtac (commute RS trans) 1);
   1.309 +by (rtac (commute RS trans RS sym) 3);
   1.310 +by (rtac sym 5);
   1.311 +by (REPEAT (ares_tac [congt] 1
   1.312 +     ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1));
   1.313 +qed "congruent2_commuteI";
   1.314 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Integ/Equiv.thy	Fri Mar 03 12:04:45 1995 +0100
     2.3 @@ -0,0 +1,28 @@
     2.4 +(*  Title: 	Equiv.thy
     2.5 +    ID:         $Id$
     2.6 +    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
     2.7 +        	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8 +    Copyright   1994 Universita' di Firenze
     2.9 +    Copyright   1993  University of Cambridge
    2.10 +
    2.11 +Equivalence relations in Higher-Order Set Theory 
    2.12 +*)
    2.13 +
    2.14 +Equiv = Relation +
    2.15 +consts
    2.16 +    refl,equiv 	::      "['a set,('a*'a) set]=>bool"
    2.17 +    sym         ::      "('a*'a) set=>bool"
    2.18 +    "'/"        ::      "['a set,('a*'a) set]=>'a set set"  (infixl 90) 
    2.19 +                        (*set of equiv classes*)
    2.20 +    congruent	::	"[('a*'a) set,'a=>'b]=>bool"
    2.21 +    congruent2  ::      "[('a*'a) set,['a,'a]=>'b]=>bool"
    2.22 +
    2.23 +defs
    2.24 +    refl_def      "refl A r == r <= Sigma A (%x.A) & (ALL x: A. <x,x> : r)"
    2.25 +    sym_def       "sym(r)    == ALL x y. <x,y>: r --> <y,x>: r"
    2.26 +    equiv_def     "equiv A r == refl A r & sym(r) & trans(r)"
    2.27 +    quotient_def  "A/r == UN x:A. {r^^{x}}"  
    2.28 +    congruent_def   "congruent r b  == ALL y z. <y,z>:r --> b(y)=b(z)"
    2.29 +    congruent2_def  "congruent2 r b == ALL y1 z1 y2 z2. \
    2.30 +\           <y1,z1>:r --> <y2,z2>:r --> b y1 y2 = b z1 z2"
    2.31 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Integ/Integ.ML	Fri Mar 03 12:04:45 1995 +0100
     3.3 @@ -0,0 +1,752 @@
     3.4 +(*  Title: 	Integ.ML
     3.5 +    ID:         $Id$
     3.6 +    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
     3.7 +        	Lawrence C Paulson, Cambridge University Computer Laboratory
     3.8 +    Copyright   1994 Universita' di Firenze
     3.9 +    Copyright   1993  University of Cambridge
    3.10 +
    3.11 +The integers as equivalence classes over nat*nat.
    3.12 +
    3.13 +Could also prove...
    3.14 +"znegative(z) ==> $# zmagnitude(z) = $~ z"
    3.15 +"~ znegative(z) ==> $# zmagnitude(z) = z"
    3.16 +< is a linear ordering
    3.17 ++ and * are monotonic wrt <
    3.18 +*)
    3.19 +
    3.20 +open Integ;
    3.21 +
    3.22 +
    3.23 +(*** Proving that intrel is an equivalence relation ***)
    3.24 +
    3.25 +val eqa::eqb::prems = goal Arith.thy 
    3.26 +    "[| (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> \
    3.27 +\       x1 + y3 = x3 + y1";
    3.28 +by (res_inst_tac [("k2","x2")] (add_left_cancel RS iffD1) 1);
    3.29 +by (rtac (add_left_commute RS trans) 1);
    3.30 +by (rtac (eqb RS ssubst) 1);
    3.31 +by (rtac (add_left_commute RS trans) 1);
    3.32 +by (rtac (eqa RS ssubst) 1);
    3.33 +by (rtac (add_left_commute) 1);
    3.34 +qed "integ_trans_lemma";
    3.35 +
    3.36 +(** Natural deduction for intrel **)
    3.37 +
    3.38 +val prems = goalw Integ.thy [intrel_def]
    3.39 +    "[| x1+y2 = x2+y1|] ==> \
    3.40 +\    <<x1,y1>,<x2,y2>>: intrel";
    3.41 +by (fast_tac (rel_cs addIs prems) 1);
    3.42 +qed "intrelI";
    3.43 +
    3.44 +(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
    3.45 +goalw Integ.thy [intrel_def]
    3.46 +  "p: intrel --> (EX x1 y1 x2 y2. \
    3.47 +\                  p = <<x1,y1>,<x2,y2>> & x1+y2 = x2+y1)";
    3.48 +by (fast_tac rel_cs 1);
    3.49 +qed "intrelE_lemma";
    3.50 +
    3.51 +val [major,minor] = goal Integ.thy
    3.52 +  "[| p: intrel;  \
    3.53 +\     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1+y2 = x2+y1|] ==> Q |] \
    3.54 +\  ==> Q";
    3.55 +by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
    3.56 +by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    3.57 +qed "intrelE";
    3.58 +
    3.59 +val intrel_cs = rel_cs addSIs [intrelI] addSEs [intrelE];
    3.60 +
    3.61 +goal Integ.thy "<<x1,y1>,<x2,y2>>: intrel = (x1+y2 = x2+y1)";
    3.62 +by (fast_tac intrel_cs 1);
    3.63 +qed "intrel_iff";
    3.64 +
    3.65 +goal Integ.thy "<x,x>: intrel";
    3.66 +by (rtac (surjective_pairing RS ssubst) 1 THEN rtac (refl RS intrelI) 1);
    3.67 +qed "intrel_refl";
    3.68 +
    3.69 +goalw Integ.thy [equiv_def, refl_def, sym_def, trans_def]
    3.70 +    "equiv {x::(nat*nat).True} intrel";
    3.71 +by (fast_tac (intrel_cs addSIs [intrel_refl] 
    3.72 +                        addSEs [sym, integ_trans_lemma]) 1);
    3.73 +qed "equiv_intrel";
    3.74 +
    3.75 +val equiv_intrel_iff =
    3.76 +    [TrueI, TrueI] MRS 
    3.77 +    ([CollectI, CollectI] MRS 
    3.78 +    (equiv_intrel RS eq_equiv_class_iff));
    3.79 +
    3.80 +goalw Integ.thy  [Integ_def,intrel_def,quotient_def] "intrel^^{<x,y>}:Integ";
    3.81 +by (fast_tac set_cs 1);
    3.82 +qed "intrel_in_integ";
    3.83 +
    3.84 +goal Integ.thy "inj_onto Abs_Integ Integ";
    3.85 +by (rtac inj_onto_inverseI 1);
    3.86 +by (etac Abs_Integ_inverse 1);
    3.87 +qed "inj_onto_Abs_Integ";
    3.88 +
    3.89 +val intrel_ss = 
    3.90 +    arith_ss addsimps [equiv_intrel_iff, inj_onto_Abs_Integ RS inj_onto_iff,
    3.91 +		       intrel_iff, intrel_in_integ, Abs_Integ_inverse];
    3.92 +
    3.93 +goal Integ.thy "inj(Rep_Integ)";
    3.94 +by (rtac inj_inverseI 1);
    3.95 +by (rtac Rep_Integ_inverse 1);
    3.96 +qed "inj_Rep_Integ";
    3.97 +
    3.98 +
    3.99 +
   3.100 +
   3.101 +(** znat: the injection from nat to Integ **)
   3.102 +
   3.103 +goal Integ.thy "inj(znat)";
   3.104 +by (rtac injI 1);
   3.105 +by (rewtac znat_def);
   3.106 +by (dtac (inj_onto_Abs_Integ RS inj_ontoD) 1);
   3.107 +by (REPEAT (rtac intrel_in_integ 1));
   3.108 +by (dtac eq_equiv_class 1);
   3.109 +by (rtac equiv_intrel 1);
   3.110 +by (fast_tac set_cs 1);
   3.111 +by (safe_tac intrel_cs);
   3.112 +by (asm_full_simp_tac arith_ss 1);
   3.113 +qed "inj_znat";
   3.114 +
   3.115 +
   3.116 +(**** zminus: unary negation on Integ ****)
   3.117 +
   3.118 +goalw Integ.thy [congruent_def]
   3.119 +  "congruent intrel (%p. split (%x y. intrel^^{<y,x>}) p)";
   3.120 +by (safe_tac intrel_cs);
   3.121 +by (asm_simp_tac (intrel_ss addsimps add_ac) 1);
   3.122 +qed "zminus_congruent";
   3.123 +
   3.124 +
   3.125 +(*Resolve th against the corresponding facts for zminus*)
   3.126 +val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   3.127 +
   3.128 +goalw Integ.thy [zminus_def]
   3.129 +      "$~ Abs_Integ(intrel^^{<x,y>}) = Abs_Integ(intrel ^^ {<y,x>})";
   3.130 +by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
   3.131 +by (simp_tac (set_ss addsimps 
   3.132 +   [intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1);
   3.133 +by (rewtac split_def);
   3.134 +by (simp_tac prod_ss 1);
   3.135 +qed "zminus";
   3.136 +
   3.137 +(*by lcp*)
   3.138 +val [prem] = goal Integ.thy
   3.139 +    "(!!x y. z = Abs_Integ(intrel^^{<x,y>}) ==> P) ==> P";
   3.140 +by (res_inst_tac [("x1","z")] 
   3.141 +    (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
   3.142 +by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
   3.143 +by (res_inst_tac [("p","x")] PairE 1);
   3.144 +by (rtac prem 1);
   3.145 +by (asm_full_simp_tac (HOL_ss addsimps [Rep_Integ_inverse]) 1);
   3.146 +qed "eq_Abs_Integ";
   3.147 +
   3.148 +goal Integ.thy "$~ ($~ z) = z";
   3.149 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.150 +by (asm_simp_tac (HOL_ss addsimps [zminus]) 1);
   3.151 +qed "zminus_zminus";
   3.152 +
   3.153 +goal Integ.thy "inj(zminus)";
   3.154 +by (rtac injI 1);
   3.155 +by (dres_inst_tac [("f","zminus")] arg_cong 1);
   3.156 +by (asm_full_simp_tac (HOL_ss addsimps [zminus_zminus]) 1);
   3.157 +qed "inj_zminus";
   3.158 +
   3.159 +goalw Integ.thy [znat_def] "$~ ($#0) = $#0";
   3.160 +by (simp_tac (arith_ss addsimps [zminus]) 1);
   3.161 +qed "zminus_0";
   3.162 +
   3.163 +
   3.164 +(**** znegative: the test for negative integers ****)
   3.165 +
   3.166 +goal Arith.thy "!!m x n::nat. n+m=x ==> m<=x";
   3.167 +by (dtac (disjI2 RS less_or_eq_imp_le) 1);
   3.168 +by (asm_full_simp_tac (arith_ss addsimps add_ac) 1);
   3.169 +by (dtac add_leD1 1);
   3.170 +by (assume_tac 1);
   3.171 +qed "not_znegative_znat_lemma";
   3.172 +
   3.173 +
   3.174 +goalw Integ.thy [znegative_def, znat_def]
   3.175 +    "~ znegative($# n)";
   3.176 +by (simp_tac intrel_ss 1);
   3.177 +by (safe_tac intrel_cs);
   3.178 +by (rtac ccontr 1);
   3.179 +by (etac notE 1);
   3.180 +by (asm_full_simp_tac arith_ss 1);
   3.181 +by (dtac not_znegative_znat_lemma 1);
   3.182 +by (fast_tac (HOL_cs addDs [leD]) 1);
   3.183 +qed "not_znegative_znat";
   3.184 +
   3.185 +goalw Integ.thy [znegative_def, znat_def] "znegative($~ $# Suc(n))";
   3.186 +by (simp_tac (intrel_ss addsimps [zminus]) 1);
   3.187 +by (REPEAT (ares_tac [exI, conjI] 1));
   3.188 +by (rtac (intrelI RS ImageI) 2);
   3.189 +by (rtac singletonI 3);
   3.190 +by (simp_tac arith_ss 2);
   3.191 +by (rtac less_add_Suc1 1);
   3.192 +qed "znegative_zminus_znat";
   3.193 +
   3.194 +
   3.195 +(**** zmagnitude: magnitide of an integer, as a natural number ****)
   3.196 +
   3.197 +goal Arith.thy "!!n::nat. n - Suc(n+m)=0";
   3.198 +by (nat_ind_tac "n" 1);
   3.199 +by (ALLGOALS(asm_simp_tac arith_ss));
   3.200 +qed "diff_Suc_add_0";
   3.201 +
   3.202 +goal Arith.thy "Suc((n::nat)+m)-n=Suc(m)";
   3.203 +by (nat_ind_tac "n" 1);
   3.204 +by (ALLGOALS(asm_simp_tac arith_ss));
   3.205 +qed "diff_Suc_add_inverse";
   3.206 +
   3.207 +goalw Integ.thy [congruent_def]
   3.208 +    "congruent intrel (split (%x y. intrel^^{<(y-x) + (x-(y::nat)),0>}))";
   3.209 +by (safe_tac intrel_cs);
   3.210 +by (asm_simp_tac intrel_ss 1);
   3.211 +by (etac rev_mp 1);
   3.212 +by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
   3.213 +by (asm_simp_tac (arith_ss addsimps [inj_Suc RS inj_eq]) 3);
   3.214 +by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 2);
   3.215 +by (asm_simp_tac arith_ss 1);
   3.216 +by (rtac impI 1);
   3.217 +by (etac subst 1);
   3.218 +by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1);
   3.219 +by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 1);
   3.220 +by (rtac impI 1);
   3.221 +by (asm_simp_tac (arith_ss addsimps
   3.222 +		  [diff_add_inverse, diff_add_0, diff_Suc_add_0,
   3.223 +		   diff_Suc_add_inverse]) 1);
   3.224 +qed "zmagnitude_congruent";
   3.225 +
   3.226 +(*Resolve th against the corresponding facts for zmagnitude*)
   3.227 +val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent];
   3.228 +
   3.229 +
   3.230 +goalw Integ.thy [zmagnitude_def]
   3.231 +    "zmagnitude (Abs_Integ(intrel^^{<x,y>})) = \
   3.232 +\    Abs_Integ(intrel^^{<(y - x) + (x - y),0>})";
   3.233 +by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
   3.234 +by (asm_simp_tac (intrel_ss addsimps [zmagnitude_ize UN_equiv_class]) 1);
   3.235 +qed "zmagnitude";
   3.236 +
   3.237 +goalw Integ.thy [znat_def] "zmagnitude($# n) = $#n";
   3.238 +by (asm_simp_tac (intrel_ss addsimps [zmagnitude]) 1);
   3.239 +qed "zmagnitude_znat";
   3.240 +
   3.241 +goalw Integ.thy [znat_def] "zmagnitude($~ $# n) = $#n";
   3.242 +by (asm_simp_tac (intrel_ss addsimps [zmagnitude, zminus]) 1);
   3.243 +qed "zmagnitude_zminus_znat";
   3.244 +
   3.245 +
   3.246 +(**** zadd: addition on Integ ****)
   3.247 +
   3.248 +(** Congruence property for addition **)
   3.249 +
   3.250 +goalw Integ.thy [congruent2_def]
   3.251 +    "congruent2 intrel (%p1 p2.                  \
   3.252 +\         split (%x1 y1. split (%x2 y2. intrel^^{<x1+x2, y1+y2>}) p2) p1)";
   3.253 +(*Proof via congruent2_commuteI seems longer*)
   3.254 +by (safe_tac intrel_cs);
   3.255 +by (asm_simp_tac (intrel_ss addsimps [add_assoc]) 1);
   3.256 +(*The rest should be trivial, but rearranging terms is hard*)
   3.257 +by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
   3.258 +by (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]) 1);
   3.259 +by (asm_simp_tac (arith_ss addsimps add_ac) 1);
   3.260 +qed "zadd_congruent2";
   3.261 +
   3.262 +(*Resolve th against the corresponding facts for zadd*)
   3.263 +val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
   3.264 +
   3.265 +goalw Integ.thy [zadd_def]
   3.266 +  "Abs_Integ(intrel^^{<x1,y1>}) + Abs_Integ(intrel^^{<x2,y2>}) = \
   3.267 +\  Abs_Integ(intrel^^{<x1+x2, y1+y2>})";
   3.268 +by (asm_simp_tac
   3.269 +    (intrel_ss addsimps [zadd_ize UN_equiv_class2]) 1);
   3.270 +qed "zadd";
   3.271 +
   3.272 +goalw Integ.thy [znat_def] "$#0 + z = z";
   3.273 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.274 +by (asm_simp_tac (arith_ss addsimps [zadd]) 1);
   3.275 +qed "zadd_0";
   3.276 +
   3.277 +goal Integ.thy "$~ (z + w) = $~ z + $~ w";
   3.278 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.279 +by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   3.280 +by (asm_simp_tac (arith_ss addsimps [zminus,zadd]) 1);
   3.281 +qed "zminus_zadd_distrib";
   3.282 +
   3.283 +goal Integ.thy "(z::int) + w = w + z";
   3.284 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.285 +by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   3.286 +by (asm_simp_tac (intrel_ss addsimps (add_ac @ [zadd])) 1);
   3.287 +qed "zadd_commute";
   3.288 +
   3.289 +goal Integ.thy "((z1::int) + z2) + z3 = z1 + (z2 + z3)";
   3.290 +by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
   3.291 +by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
   3.292 +by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
   3.293 +by (asm_simp_tac (arith_ss addsimps [zadd, add_assoc]) 1);
   3.294 +qed "zadd_assoc";
   3.295 +
   3.296 +(*For AC rewriting*)
   3.297 +goal Integ.thy "(x::int)+(y+z)=y+(x+z)";
   3.298 +by (rtac (zadd_commute RS trans) 1);
   3.299 +by (rtac (zadd_assoc RS trans) 1);
   3.300 +by (rtac (zadd_commute RS arg_cong) 1);
   3.301 +qed "zadd_left_commute";
   3.302 +
   3.303 +(*Integer addition is an AC operator*)
   3.304 +val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
   3.305 +
   3.306 +goalw Integ.thy [znat_def] "$# (m + n) = ($#m) + ($#n)";
   3.307 +by (asm_simp_tac (arith_ss addsimps [zadd]) 1);
   3.308 +qed "znat_add";
   3.309 +
   3.310 +goalw Integ.thy [znat_def] "z + ($~ z) = $#0";
   3.311 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.312 +by (asm_simp_tac (intrel_ss addsimps [zminus, zadd, add_commute]) 1);
   3.313 +qed "zadd_zminus_inverse";
   3.314 +
   3.315 +goal Integ.thy "($~ z) + z = $#0";
   3.316 +by (rtac (zadd_commute RS trans) 1);
   3.317 +by (rtac zadd_zminus_inverse 1);
   3.318 +qed "zadd_zminus_inverse2";
   3.319 +
   3.320 +goal Integ.thy "z + $#0 = z";
   3.321 +by (rtac (zadd_commute RS trans) 1);
   3.322 +by (rtac zadd_0 1);
   3.323 +qed "zadd_0_right";
   3.324 +
   3.325 +
   3.326 +(*Need properties of subtraction?  Or use $- just as an abbreviation!*)
   3.327 +
   3.328 +(**** zmult: multiplication on Integ ****)
   3.329 +
   3.330 +(** Congruence property for multiplication **)
   3.331 +
   3.332 +goal Integ.thy "((k::nat) + l) + (m + n) = (k + m) + (n + l)";
   3.333 +by (simp_tac (arith_ss addsimps add_ac) 1);
   3.334 +qed "zmult_congruent_lemma";
   3.335 +
   3.336 +goal Integ.thy 
   3.337 +    "congruent2 intrel (%p1 p2.  		\
   3.338 +\               split (%x1 y1. split (%x2 y2. 	\
   3.339 +\                   intrel^^{<x1*x2 + y1*y2, x1*y2 + y1*x2>}) p2) p1)";
   3.340 +by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   3.341 +by (safe_tac intrel_cs);
   3.342 +by (rewtac split_def);
   3.343 +by (simp_tac (arith_ss addsimps add_ac@mult_ac) 1);
   3.344 +by (asm_simp_tac (arith_ss addsimps add_ac@mult_ac) 1);
   3.345 +by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1);
   3.346 +by (rtac (zmult_congruent_lemma RS trans) 1);
   3.347 +by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
   3.348 +by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
   3.349 +by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
   3.350 +by (asm_simp_tac (HOL_ss addsimps [add_mult_distrib RS sym]) 1);
   3.351 +by (asm_simp_tac (arith_ss addsimps add_ac@mult_ac) 1);
   3.352 +qed "zmult_congruent2";
   3.353 +
   3.354 +(*Resolve th against the corresponding facts for zmult*)
   3.355 +val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
   3.356 +
   3.357 +goalw Integ.thy [zmult_def]
   3.358 +   "Abs_Integ((intrel^^{<x1,y1>})) * Abs_Integ((intrel^^{<x2,y2>})) = 	\
   3.359 +\   Abs_Integ(intrel ^^ {<x1*x2 + y1*y2, x1*y2 + y1*x2>})";
   3.360 +by (simp_tac (intrel_ss addsimps [zmult_ize UN_equiv_class2]) 1);
   3.361 +qed "zmult";
   3.362 +
   3.363 +goalw Integ.thy [znat_def] "$#0 * z = $#0";
   3.364 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.365 +by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
   3.366 +qed "zmult_0";
   3.367 +
   3.368 +goalw Integ.thy [znat_def] "$#Suc(0) * z = z";
   3.369 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.370 +by (asm_simp_tac (arith_ss addsimps [zmult, add_0_right]) 1);
   3.371 +qed "zmult_1";
   3.372 +
   3.373 +goal Integ.thy "($~ z) * w = $~ (z * w)";
   3.374 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.375 +by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   3.376 +by (asm_simp_tac (intrel_ss addsimps ([zminus, zmult] @ add_ac)) 1);
   3.377 +qed "zmult_zminus";
   3.378 +
   3.379 +
   3.380 +goal Integ.thy "($~ z) * ($~ w) = (z * w)";
   3.381 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.382 +by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   3.383 +by (asm_simp_tac (intrel_ss addsimps ([zminus, zmult] @ add_ac)) 1);
   3.384 +qed "zmult_zminus_zminus";
   3.385 +
   3.386 +goal Integ.thy "(z::int) * w = w * z";
   3.387 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.388 +by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   3.389 +by (asm_simp_tac (intrel_ss addsimps ([zmult] @ add_ac @ mult_ac)) 1);
   3.390 +qed "zmult_commute";
   3.391 +
   3.392 +goal Integ.thy "z * $# 0 = $#0";
   3.393 +by (rtac ([zmult_commute, zmult_0] MRS trans) 1);
   3.394 +qed "zmult_0_right";
   3.395 +
   3.396 +goal Integ.thy "z * $#Suc(0) = z";
   3.397 +by (rtac ([zmult_commute, zmult_1] MRS trans) 1);
   3.398 +qed "zmult_1_right";
   3.399 +
   3.400 +goal Integ.thy "((z1::int) * z2) * z3 = z1 * (z2 * z3)";
   3.401 +by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
   3.402 +by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
   3.403 +by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
   3.404 +by (asm_simp_tac (intrel_ss addsimps ([zmult] @ add_ac @ mult_ac)) 1);
   3.405 +qed "zmult_assoc";
   3.406 +
   3.407 +(*For AC rewriting*)
   3.408 +qed_goal "zmult_left_commute" Integ.thy
   3.409 +    "(z1::int)*(z2*z3) = z2*(z1*z3)"
   3.410 + (fn _ => [rtac (zmult_commute RS trans) 1, rtac (zmult_assoc RS trans) 1,
   3.411 +           rtac (zmult_commute RS arg_cong) 1]);
   3.412 +
   3.413 +(*Integer multiplication is an AC operator*)
   3.414 +val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
   3.415 +
   3.416 +goal Integ.thy "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
   3.417 +by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
   3.418 +by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
   3.419 +by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   3.420 +by (asm_simp_tac 
   3.421 +    (intrel_ss addsimps ([zadd, zmult, add_mult_distrib] @ 
   3.422 +			 add_ac @ mult_ac)) 1);
   3.423 +qed "zadd_zmult_distrib";
   3.424 +
   3.425 +val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
   3.426 +
   3.427 +goal Integ.thy "w * ($~ z) = $~ (w * z)";
   3.428 +by (simp_tac (HOL_ss addsimps [zmult_commute', zmult_zminus]) 1);
   3.429 +qed "zmult_zminus_right";
   3.430 +
   3.431 +goal Integ.thy "(w::int) * (z1 + z2) = (w * z1) + (w * z2)";
   3.432 +by (simp_tac (HOL_ss addsimps [zmult_commute',zadd_zmult_distrib]) 1);
   3.433 +qed "zadd_zmult_distrib2";
   3.434 +
   3.435 +val zadd_simps = 
   3.436 +    [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
   3.437 +
   3.438 +val zminus_simps = [zminus_zminus, zminus_0, zminus_zadd_distrib];
   3.439 +
   3.440 +val zmult_simps = [zmult_0, zmult_1, zmult_0_right, zmult_1_right, 
   3.441 +		   zmult_zminus, zmult_zminus_right];
   3.442 +
   3.443 +val integ_ss =
   3.444 +    arith_ss addsimps (zadd_simps @ zminus_simps @ zmult_simps @ 
   3.445 +		       [zmagnitude_znat, zmagnitude_zminus_znat]);
   3.446 +
   3.447 +
   3.448 +(**** Additional Theorems (by Mattolini; proofs mainly by lcp) ****)
   3.449 +
   3.450 +(* Some Theorems about zsuc and zpred *)
   3.451 +goalw Integ.thy [zsuc_def] "$#(Suc(n)) = zsuc($# n)";
   3.452 +by (simp_tac (arith_ss addsimps [znat_add RS sym]) 1);
   3.453 +qed "znat_Suc";
   3.454 +
   3.455 +goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zsuc(z) = zpred($~ z)";
   3.456 +by (simp_tac integ_ss 1);
   3.457 +qed "zminus_zsuc";
   3.458 +
   3.459 +goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zpred(z) = zsuc($~ z)";
   3.460 +by (simp_tac integ_ss 1);
   3.461 +qed "zminus_zpred";
   3.462 +
   3.463 +goalw Integ.thy [zsuc_def,zpred_def,zdiff_def]
   3.464 +   "zpred(zsuc(z)) = z";
   3.465 +by (simp_tac (integ_ss addsimps [zadd_assoc]) 1);
   3.466 +qed "zpred_zsuc";
   3.467 +
   3.468 +goalw Integ.thy [zsuc_def,zpred_def,zdiff_def]
   3.469 +   "zsuc(zpred(z)) = z";
   3.470 +by (simp_tac (integ_ss addsimps [zadd_assoc]) 1);
   3.471 +qed "zsuc_zpred";
   3.472 +
   3.473 +goal Integ.thy "(zpred(z)=w) = (z=zsuc(w))";
   3.474 +by (safe_tac HOL_cs);
   3.475 +by (rtac (zsuc_zpred RS sym) 1);
   3.476 +by (rtac zpred_zsuc 1);
   3.477 +qed "zpred_to_zsuc";
   3.478 +
   3.479 +goal Integ.thy "(zsuc(z)=w)=(z=zpred(w))";
   3.480 +by (safe_tac HOL_cs);
   3.481 +by (rtac (zpred_zsuc RS sym) 1);
   3.482 +by (rtac zsuc_zpred 1);
   3.483 +qed "zsuc_to_zpred";
   3.484 +
   3.485 +goal Integ.thy "($~ z = w) = (z = $~ w)";
   3.486 +by (safe_tac HOL_cs);
   3.487 +by (rtac (zminus_zminus RS sym) 1);
   3.488 +by (rtac zminus_zminus 1);
   3.489 +qed "zminus_exchange";
   3.490 +
   3.491 +goal Integ.thy"(zsuc(z)=zsuc(w)) = (z=w)";
   3.492 +by (safe_tac intrel_cs);
   3.493 +by (dres_inst_tac [("f","zpred")] arg_cong 1);
   3.494 +by (asm_full_simp_tac (HOL_ss addsimps [zpred_zsuc]) 1);
   3.495 +qed "bijective_zsuc";
   3.496 +
   3.497 +goal Integ.thy"(zpred(z)=zpred(w)) = (z=w)";
   3.498 +by (safe_tac intrel_cs);
   3.499 +by (dres_inst_tac [("f","zsuc")] arg_cong 1);
   3.500 +by (asm_full_simp_tac (HOL_ss addsimps [zsuc_zpred]) 1);
   3.501 +qed "bijective_zpred";
   3.502 +
   3.503 +(* Additional Theorems about zadd *)
   3.504 +
   3.505 +goalw Integ.thy [zsuc_def] "zsuc(z) + w = zsuc(z+w)";
   3.506 +by (simp_tac (arith_ss addsimps zadd_ac) 1);
   3.507 +qed "zadd_zsuc";
   3.508 +
   3.509 +goalw Integ.thy [zsuc_def] "w + zsuc(z) = zsuc(w+z)";
   3.510 +by (simp_tac (arith_ss addsimps zadd_ac) 1);
   3.511 +qed "zadd_zsuc_right";
   3.512 +
   3.513 +goalw Integ.thy [zpred_def,zdiff_def] "zpred(z) + w = zpred(z+w)";
   3.514 +by (simp_tac (arith_ss addsimps zadd_ac) 1);
   3.515 +qed "zadd_zpred";
   3.516 +
   3.517 +goalw Integ.thy [zpred_def,zdiff_def] "w + zpred(z) = zpred(w+z)";
   3.518 +by (simp_tac (arith_ss addsimps zadd_ac) 1);
   3.519 +qed "zadd_zpred_right";
   3.520 +
   3.521 +
   3.522 +(* Additional Theorems about zmult *)
   3.523 +
   3.524 +goalw Integ.thy [zsuc_def] "zsuc(w) * z = z + w * z";
   3.525 +by (simp_tac (integ_ss addsimps [zadd_zmult_distrib, zadd_commute]) 1);
   3.526 +qed "zmult_zsuc";
   3.527 +
   3.528 +goalw Integ.thy [zsuc_def] "z * zsuc(w) = z + w * z";
   3.529 +by (simp_tac 
   3.530 +    (integ_ss addsimps [zadd_zmult_distrib2, zadd_commute, zmult_commute]) 1);
   3.531 +qed "zmult_zsuc_right";
   3.532 +
   3.533 +goalw Integ.thy [zpred_def, zdiff_def] "zpred(w) * z = w * z - z";
   3.534 +by (simp_tac (integ_ss addsimps [zadd_zmult_distrib]) 1);
   3.535 +qed "zmult_zpred";
   3.536 +
   3.537 +goalw Integ.thy [zpred_def, zdiff_def] "z * zpred(w) = w * z - z";
   3.538 +by (simp_tac (integ_ss addsimps [zadd_zmult_distrib2, zmult_commute]) 1);
   3.539 +qed "zmult_zpred_right";
   3.540 +
   3.541 +(* Further Theorems about zsuc and zpred *)
   3.542 +goal Integ.thy "$#Suc(m) ~= $#0";
   3.543 +by (simp_tac (integ_ss addsimps [inj_znat RS inj_eq]) 1);
   3.544 +qed "znat_Suc_not_znat_Zero";
   3.545 +
   3.546 +bind_thm ("znat_Zero_not_znat_Suc", (znat_Suc_not_znat_Zero RS not_sym));
   3.547 +
   3.548 +
   3.549 +goalw Integ.thy [zsuc_def,znat_def] "w ~= zsuc(w)";
   3.550 +by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   3.551 +by (asm_full_simp_tac (intrel_ss addsimps [zadd]) 1);
   3.552 +qed "n_not_zsuc_n";
   3.553 +
   3.554 +val zsuc_n_not_n = n_not_zsuc_n RS not_sym;
   3.555 +
   3.556 +goal Integ.thy "w ~= zpred(w)";
   3.557 +by (safe_tac HOL_cs);
   3.558 +by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1);
   3.559 +by (asm_full_simp_tac (HOL_ss addsimps [zsuc_zpred,zsuc_n_not_n]) 1);
   3.560 +qed "n_not_zpred_n";
   3.561 +
   3.562 +val zpred_n_not_n = n_not_zpred_n RS not_sym;
   3.563 +
   3.564 +
   3.565 +(* Theorems about less and less_equal *)
   3.566 +
   3.567 +goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
   3.568 +    "!!w. w<z ==> ? n. z = w + $#(Suc(n))";
   3.569 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.570 +by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   3.571 +by (safe_tac intrel_cs);
   3.572 +by (asm_full_simp_tac (intrel_ss addsimps [zadd, zminus]) 1);
   3.573 +by (safe_tac (intrel_cs addSDs [less_eq_Suc_add]));
   3.574 +by (res_inst_tac [("x","k")] exI 1);
   3.575 +by (asm_full_simp_tac (HOL_ss addsimps ([add_Suc RS sym] @ add_ac)) 1);
   3.576 +(*To cancel x2, rename it to be first!*)
   3.577 +by (rename_tac "a b c" 1);
   3.578 +by (asm_full_simp_tac (HOL_ss addsimps (add_left_cancel::add_ac)) 1);
   3.579 +qed "zless_eq_zadd_Suc";
   3.580 +
   3.581 +goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
   3.582 +    "z < z + $#(Suc(n))";
   3.583 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.584 +by (safe_tac intrel_cs);
   3.585 +by (simp_tac (intrel_ss addsimps [zadd, zminus]) 1);
   3.586 +by (REPEAT_SOME (ares_tac [refl, exI, singletonI, ImageI, conjI, intrelI]));
   3.587 +by (rtac le_less_trans 1);
   3.588 +by (rtac lessI 2);
   3.589 +by (asm_simp_tac (arith_ss addsimps ([le_add1,add_left_cancel_le]@add_ac)) 1);
   3.590 +qed "zless_zadd_Suc";
   3.591 +
   3.592 +goal Integ.thy "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
   3.593 +by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
   3.594 +by (simp_tac 
   3.595 +    (arith_ss addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1);
   3.596 +qed "zless_trans";
   3.597 +
   3.598 +goalw Integ.thy [zsuc_def] "z<zsuc(z)";
   3.599 +by (rtac zless_zadd_Suc 1);
   3.600 +qed "zlessI";
   3.601 +
   3.602 +val zless_zsucI = zlessI RSN (2,zless_trans);
   3.603 +
   3.604 +goal Integ.thy "!!z w::int. z<w ==> ~w<z";
   3.605 +by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
   3.606 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.607 +by (safe_tac intrel_cs);
   3.608 +by (asm_full_simp_tac (intrel_ss addsimps ([znat_def, zadd])) 1);
   3.609 +by (asm_full_simp_tac
   3.610 + (HOL_ss addsimps [add_left_cancel, add_assoc, add_Suc_right RS sym]) 1);
   3.611 +by (resolve_tac [less_not_refl2 RS notE] 1);
   3.612 +by (etac sym 2);
   3.613 +by (REPEAT (resolve_tac [lessI, trans_less_add2, less_SucI] 1));
   3.614 +qed "zless_not_sym";
   3.615 +
   3.616 +(* [| n<m; m<n |] ==> R *)
   3.617 +bind_thm ("zless_asym", (zless_not_sym RS notE));
   3.618 +
   3.619 +goal Integ.thy "!!z::int. ~ z<z";
   3.620 +by (resolve_tac [zless_asym RS notI] 1);
   3.621 +by (REPEAT (assume_tac 1));
   3.622 +qed "zless_not_refl";
   3.623 +
   3.624 +(* z<z ==> R *)
   3.625 +bind_thm ("zless_anti_refl", (zless_not_refl RS notE));
   3.626 +
   3.627 +goal Integ.thy "!!w. z<w ==> w ~= (z::int)";
   3.628 +by(fast_tac (HOL_cs addEs [zless_anti_refl]) 1);
   3.629 +qed "zless_not_refl2";
   3.630 +
   3.631 +
   3.632 +(*"Less than" is a linear ordering*)
   3.633 +goalw Integ.thy [zless_def, znegative_def, zdiff_def] 
   3.634 +    "z<w | z=w | w<(z::int)";
   3.635 +by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   3.636 +by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   3.637 +by (safe_tac intrel_cs);
   3.638 +by (asm_full_simp_tac
   3.639 +    (intrel_ss addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
   3.640 +by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
   3.641 +by (etac disjE 2);
   3.642 +by (assume_tac 2);
   3.643 +by (DEPTH_SOLVE
   3.644 +    (swap_res_tac [exI] 1 THEN 
   3.645 +     swap_res_tac [exI] 1 THEN 
   3.646 +     etac conjI 1 THEN 
   3.647 +     simp_tac (arith_ss addsimps add_ac)  1));
   3.648 +qed "zless_linear";
   3.649 +
   3.650 +
   3.651 +(*** Properties of <= ***)
   3.652 +
   3.653 +goalw Integ.thy  [zless_def, znegative_def, zdiff_def, znat_def]
   3.654 +    "($#m < $#n) = (m<n)";
   3.655 +by (simp_tac
   3.656 +    (intrel_ss addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
   3.657 +by (fast_tac (HOL_cs addIs [add_commute] addSEs [less_add_eq_less]) 1);
   3.658 +qed "zless_eq_less";
   3.659 +
   3.660 +goalw Integ.thy [zle_def, le_def] "($#m <= $#n) = (m<=n)";
   3.661 +by (simp_tac (HOL_ss addsimps [zless_eq_less]) 1);
   3.662 +qed "zle_eq_le";
   3.663 +
   3.664 +goalw Integ.thy [zle_def] "!!w. ~(w<z) ==> z<=(w::int)";
   3.665 +by (assume_tac 1);
   3.666 +qed "zleI";
   3.667 +
   3.668 +goalw Integ.thy [zle_def] "!!w. z<=w ==> ~(w<(z::int))";
   3.669 +by (assume_tac 1);
   3.670 +qed "zleD";
   3.671 +
   3.672 +val zleE = make_elim zleD;
   3.673 +
   3.674 +goalw Integ.thy [zle_def] "!!z. ~ z <= w ==> w<(z::int)";
   3.675 +by (fast_tac HOL_cs 1);
   3.676 +qed "not_zleE";
   3.677 +
   3.678 +goalw Integ.thy [zle_def] "!!z. z < w ==> z <= (w::int)";
   3.679 +by (fast_tac (HOL_cs addEs [zless_asym]) 1);
   3.680 +qed "zless_imp_zle";
   3.681 +
   3.682 +goalw Integ.thy [zle_def] "!!z. z <= w ==> z < w | z=(w::int)";
   3.683 +by (cut_facts_tac [zless_linear] 1);
   3.684 +by (fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym]) 1);
   3.685 +qed "zle_imp_zless_or_eq";
   3.686 +
   3.687 +goalw Integ.thy [zle_def] "!!z. z<w | z=w ==> z <=(w::int)";
   3.688 +by (cut_facts_tac [zless_linear] 1);
   3.689 +by (fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym]) 1);
   3.690 +qed "zless_or_eq_imp_zle";
   3.691 +
   3.692 +goal Integ.thy "(x <= (y::int)) = (x < y | x=y)";
   3.693 +by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1));
   3.694 +qed "zle_eq_zless_or_eq";
   3.695 +
   3.696 +goal Integ.thy "w <= (w::int)";
   3.697 +by (simp_tac (HOL_ss addsimps [zle_eq_zless_or_eq]) 1);
   3.698 +qed "zle_refl";
   3.699 +
   3.700 +val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)";
   3.701 +by (dtac zle_imp_zless_or_eq 1);
   3.702 +by (fast_tac (HOL_cs addIs [zless_trans]) 1);
   3.703 +qed "zle_zless_trans";
   3.704 +
   3.705 +goal Integ.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::int)";
   3.706 +by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
   3.707 +	    rtac zless_or_eq_imp_zle, fast_tac (HOL_cs addIs [zless_trans])]);
   3.708 +qed "zle_trans";
   3.709 +
   3.710 +goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
   3.711 +by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
   3.712 +	    fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym])]);
   3.713 +qed "zle_anti_sym";
   3.714 +
   3.715 +
   3.716 +goal Integ.thy "!!w w' z::int. z + w' = z + w ==> w' = w";
   3.717 +by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1);
   3.718 +by (asm_full_simp_tac (integ_ss addsimps zadd_ac) 1);
   3.719 +qed "zadd_left_cancel";
   3.720 +
   3.721 +
   3.722 +(*** Monotonicity results ***)
   3.723 +
   3.724 +goal Integ.thy "!!v w z::int. v < w ==> v + z < w + z";
   3.725 +by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
   3.726 +by (simp_tac (HOL_ss addsimps zadd_ac) 1);
   3.727 +by (simp_tac (HOL_ss addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1);
   3.728 +qed "zadd_zless_mono1";
   3.729 +
   3.730 +goal Integ.thy "!!v w z::int. (v+z < w+z) = (v < w)";
   3.731 +by (safe_tac (HOL_cs addSEs [zadd_zless_mono1]));
   3.732 +by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1);
   3.733 +by (asm_full_simp_tac (integ_ss addsimps [zadd_assoc]) 1);
   3.734 +qed "zadd_left_cancel_zless";
   3.735 +
   3.736 +goal Integ.thy "!!v w z::int. (v+z <= w+z) = (v <= w)";
   3.737 +by (asm_full_simp_tac
   3.738 +    (integ_ss addsimps [zle_def, zadd_left_cancel_zless]) 1);
   3.739 +qed "zadd_left_cancel_zle";
   3.740 +
   3.741 +(*"v<=w ==> v+z <= w+z"*)
   3.742 +bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2);
   3.743 +
   3.744 +
   3.745 +goal Integ.thy "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
   3.746 +by (etac (zadd_zle_mono1 RS zle_trans) 1);
   3.747 +by (simp_tac (HOL_ss addsimps [zadd_commute]) 1);
   3.748 +(*w moves to the end because it is free while z', z are bound*)
   3.749 +by (etac zadd_zle_mono1 1);
   3.750 +qed "zadd_zle_mono";
   3.751 +
   3.752 +goal Integ.thy "!!w z::int. z<=$#0 ==> w+z <= w";
   3.753 +by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1);
   3.754 +by (asm_full_simp_tac (integ_ss addsimps [zadd_commute]) 1);
   3.755 +qed "zadd_zle_self";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Integ/Integ.thy	Fri Mar 03 12:04:45 1995 +0100
     4.3 @@ -0,0 +1,80 @@
     4.4 +(*  Title: 	Integ.thy
     4.5 +    ID:         $Id$
     4.6 +    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
     4.7 +        	Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8 +    Copyright   1994 Universita' di Firenze
     4.9 +    Copyright   1993  University of Cambridge
    4.10 +
    4.11 +The integers as equivalence classes over nat*nat.
    4.12 +*)
    4.13 +
    4.14 +Integ = Equiv + Arith +
    4.15 +consts
    4.16 +  intrel      :: "((nat * nat) * (nat * nat)) set"
    4.17 +
    4.18 +defs
    4.19 +  intrel_def
    4.20 +   "intrel == {p. ? x1 y1 x2 y2. p=<<x1::nat,y1>,<x2,y2>> & x1+y2 = x2+y1}"
    4.21 +
    4.22 +subtype (Integ)
    4.23 +  int = "{x::(nat*nat).True}/intrel"		("quotient_def")
    4.24 +
    4.25 +arities int :: ord
    4.26 +        int :: plus
    4.27 +        int :: times
    4.28 +        int :: minus
    4.29 +consts
    4.30 +  zNat        :: "nat set"
    4.31 +  znat	      :: "nat => int"	   ("$# _" [80] 80)
    4.32 +  zminus      :: "int => int"	   ("$~ _" [80] 80)
    4.33 +  znegative   :: "int => bool"
    4.34 +  zmagnitude  :: "int => int"
    4.35 +  zdiv,zmod   :: "[int,int]=>int"  (infixl 70)
    4.36 +  zpred,zsuc  :: "int=>int"
    4.37 +
    4.38 +defs
    4.39 +  zNat_def    "zNat == {x::nat. True}"
    4.40 +
    4.41 +  znat_def    "$# m == Abs_Integ(intrel ^^ {<m,0>})"
    4.42 +
    4.43 +  zminus_def
    4.44 +	"$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{<y,x>}) p)"
    4.45 +
    4.46 +  znegative_def
    4.47 +      "znegative(Z) == EX x y. x<y & <x,y::nat>:Rep_Integ(Z)"
    4.48 +
    4.49 +  zmagnitude_def
    4.50 +      "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{<(y-x) + (x-y),0>}) p)"
    4.51 +
    4.52 +  zadd_def
    4.53 +   "Z1 + Z2 == \
    4.54 +\       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2).   \
    4.55 +\           split (%x1 y1. split (%x2 y2. intrel^^{<x1+x2, y1+y2>}) p2) p1)"
    4.56 +
    4.57 +  zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)"
    4.58 +
    4.59 +  zless_def "Z1<Z2 == znegative(Z1 - Z2)"
    4.60 +
    4.61 +  zle_def   "Z1 <= (Z2::int) == ~(Z2 < Z1)"
    4.62 +
    4.63 +  zmult_def
    4.64 +   "Z1 * Z2 == \
    4.65 +\       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   \
    4.66 +\           split (%x2 y2. intrel^^{<x1*x2 + y1*y2, x1*y2 + y1*x2>}) p2) p1)"
    4.67 +
    4.68 +  zdiv_def
    4.69 +   "Z1 zdiv Z2 ==   \
    4.70 +\       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   \
    4.71 +\           split (%x2 y2. intrel^^{<(x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),   \
    4.72 +\           (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2)>}) p2) p1)"
    4.73 +
    4.74 +  zmod_def
    4.75 +   "Z1 zmod Z2 ==   \
    4.76 +\       Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1.   \
    4.77 +\           split (%x2 y2. intrel^^{<(x1-y1)mod((x2-y2)+(y2-x2)),   \
    4.78 +\           (x1-y1)mod((x2-y2)+(x2-y2))>}) p2) p1)"
    4.79 +
    4.80 +  zsuc_def     "zsuc(Z) == Z + $# Suc(0)"
    4.81 +
    4.82 +  zpred_def    "zpred(Z) == Z - $# Suc(0)"
    4.83 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Integ/ROOT.ML	Fri Mar 03 12:04:45 1995 +0100
     5.3 @@ -0,0 +1,12 @@
     5.4 +(*  Title:  	CHOL/Integ/ROOT
     5.5 +    ID:         $Id$
     5.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   1995  University of Cambridge
     5.8 +
     5.9 +The Integers in CHOL (ported from ZF by Riccardo Mattolini)
    5.10 +*)
    5.11 +
    5.12 +CHOL_build_completed;    (*Cause examples to fail if CHOL did*)
    5.13 +
    5.14 +loadpath := ["Integ"];
    5.15 +time_use_thy "Integ" handle _ => exit 1;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Integ/Relation.ML	Fri Mar 03 12:04:45 1995 +0100
     6.3 @@ -0,0 +1,98 @@
     6.4 +(*  Title: 	Relation.ML
     6.5 +    ID:         $Id$
     6.6 +    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
     6.7 +        	Lawrence C Paulson, Cambridge University Computer Laboratory
     6.8 +    Copyright   1994 Universita' di Firenze
     6.9 +    Copyright   1993  University of Cambridge
    6.10 +
    6.11 +Functions represented as relations in HOL Set Theory 
    6.12 +*)
    6.13 +
    6.14 +val RSLIST = curry (op MRS);
    6.15 +
    6.16 +open Relation;
    6.17 +
    6.18 +goalw Relation.thy [converse_def] "!!a b r. <a,b>:r ==> <b,a>:converse(r)";
    6.19 +by (simp_tac prod_ss 1);
    6.20 +by (fast_tac set_cs 1);
    6.21 +qed "converseI";
    6.22 +
    6.23 +goalw Relation.thy [converse_def] "!!a b r. <a,b> : converse(r) ==> <b,a> : r";
    6.24 +by (fast_tac comp_cs 1);
    6.25 +qed "converseD";
    6.26 +
    6.27 +qed_goalw "converseE" Relation.thy [converse_def]
    6.28 +    "[| yx : converse(r);  \
    6.29 +\       !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P \
    6.30 +\    |] ==> P"
    6.31 + (fn [major,minor]=>
    6.32 +  [ (rtac (major RS CollectE) 1),
    6.33 +    (REPEAT (eresolve_tac [bexE,exE, conjE, minor] 1)),
    6.34 +    (hyp_subst_tac 1),
    6.35 +    (assume_tac 1) ]);
    6.36 +
    6.37 +val converse_cs = comp_cs addSIs [converseI] 
    6.38 +			  addSEs [converseD,converseE];
    6.39 +
    6.40 +qed_goalw "Domain_iff" Relation.thy [Domain_def]
    6.41 +    "a: Domain(r) = (EX y. <a,y>: r)"
    6.42 + (fn _=> [ (fast_tac comp_cs 1) ]);
    6.43 +
    6.44 +qed_goal "DomainI" Relation.thy "!!a b r. <a,b>: r ==> a: Domain(r)"
    6.45 + (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
    6.46 +
    6.47 +qed_goal "DomainE" Relation.thy
    6.48 +    "[| a : Domain(r);  !!y. <a,y>: r ==> P |] ==> P"
    6.49 + (fn prems=>
    6.50 +  [ (rtac (Domain_iff RS iffD1 RS exE) 1),
    6.51 +    (REPEAT (ares_tac prems 1)) ]);
    6.52 +
    6.53 +qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.<a,b>: r ==> b : Range(r)"
    6.54 + (fn _ => [ (etac (converseI RS DomainI) 1) ]);
    6.55 +
    6.56 +qed_goalw "RangeE" Relation.thy [Range_def]
    6.57 +    "[| b : Range(r);  !!x. <x,b>: r ==> P |] ==> P"
    6.58 + (fn major::prems=>
    6.59 +  [ (rtac (major RS DomainE) 1),
    6.60 +    (resolve_tac prems 1),
    6.61 +    (etac converseD 1) ]);
    6.62 +
    6.63 +(*** Image of a set under a function/relation ***)
    6.64 +
    6.65 +qed_goalw "Image_iff" Relation.thy [Image_def]
    6.66 +    "b : r^^A = (? x:A. <x,b>:r)"
    6.67 + (fn _ => [ fast_tac (comp_cs addIs [RangeI]) 1 ]);
    6.68 +
    6.69 +qed_goal "Image_singleton_iff" Relation.thy
    6.70 +    "(b : r^^{a}) = (<a,b>:r)"
    6.71 + (fn _ => [ rtac (Image_iff RS trans) 1,
    6.72 +	    fast_tac comp_cs 1 ]);
    6.73 +
    6.74 +qed_goalw "ImageI" Relation.thy [Image_def]
    6.75 +    "!!a b r. [| <a,b>: r;  a:A |] ==> b : r^^A"
    6.76 + (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)),
    6.77 +            (resolve_tac [conjI ] 1),
    6.78 +            (resolve_tac [RangeI] 1),
    6.79 +            (REPEAT (fast_tac set_cs 1))]);
    6.80 +
    6.81 +qed_goalw "ImageE" Relation.thy [Image_def]
    6.82 +    "[| b: r^^A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
    6.83 + (fn major::prems=>
    6.84 +  [ (rtac (major RS CollectE) 1),
    6.85 +    (safe_tac set_cs),
    6.86 +    (etac RangeE 1),
    6.87 +    (rtac (hd prems) 1),
    6.88 +    (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
    6.89 +
    6.90 +qed_goal "Image_subset" Relation.thy
    6.91 +    "!!A B r. r <= Sigma A (%x.B) ==> r^^C <= B"
    6.92 + (fn _ =>
    6.93 +  [ (rtac subsetI 1),
    6.94 +    (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
    6.95 +
    6.96 +val rel_cs = converse_cs addSIs [converseI] 
    6.97 +                         addIs  [ImageI, DomainI, RangeI]
    6.98 +                         addSEs [ImageE, DomainE, RangeE];
    6.99 +
   6.100 +val rel_eq_cs = rel_cs addSIs [equalityI];
   6.101 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Integ/Relation.thy	Fri Mar 03 12:04:45 1995 +0100
     7.3 @@ -0,0 +1,24 @@
     7.4 +(*  Title: 	Relation.thy
     7.5 +    ID:         $Id$
     7.6 +    Author: 	Riccardo Mattolini, Dip. Sistemi e Informatica
     7.7 +        and	Lawrence C Paulson, Cambridge University Computer Laboratory
     7.8 +    Copyright   1994 Universita' di Firenze
     7.9 +    Copyright   1993  University of Cambridge
    7.10 +
    7.11 +Functions represented as relations in Higher-Order Set Theory 
    7.12 +*)
    7.13 +
    7.14 +Relation = Trancl +
    7.15 +consts
    7.16 +    converse    ::      "('a*'a) set => ('a*'a) set"
    7.17 +    "^^"        ::      "[('a*'a) set,'a set] => 'a set" (infixl 90)
    7.18 +    Domain      ::      "('a*'a) set => 'a set"
    7.19 +    Range       ::      "('a*'a) set => 'a set"
    7.20 +
    7.21 +defs
    7.22 +    converse_def  "converse(r) == {z. (? w:r. ? x y. w=<x,y> & z=<y,x>)}"
    7.23 +    Domain_def    "Domain(r) == {z. ! x. (z=x --> (? y. <x,y>:r))}"
    7.24 +    Range_def     "Range(r) == Domain(converse(r))"
    7.25 +    Image_def     "r ^^ s == {y. y:Range(r) &  (? x:s. <x,y>:r)}"
    7.26 +
    7.27 +end