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