# HG changeset patch # User nipkow # Date 801504707 -7200 # Node ID 64b30e3cc6d4721c86fb3b4d3d6ec84cbb28d03a # Parent 42ec82147d838fba2da6c7b3e940d1cc93065af3 Trancl is now based on Relation which used to be in Integ. diff -r 42ec82147d83 -r 64b30e3cc6d4 src/HOL/Relation.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Relation.ML Fri May 26 18:11:47 1995 +0200 @@ -0,0 +1,173 @@ +(* Title: Relation.ML + ID: $Id$ + Authors: Riccardo Mattolini, Dip. Sistemi e Informatica + Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 Universita' di Firenze + Copyright 1993 University of Cambridge +*) + +val RSLIST = curry (op MRS); + +open Relation; + +(** Identity relation **) + +goalw Relation.thy [id_def] "(a,a) : id"; +by (rtac CollectI 1); +by (rtac exI 1); +by (rtac refl 1); +qed "idI"; + +val major::prems = goalw Relation.thy [id_def] + "[| p: id; !!x.[| p = (x,x) |] ==> P \ +\ |] ==> P"; +by (rtac (major RS CollectE) 1); +by (etac exE 1); +by (eresolve_tac prems 1); +qed "idE"; + +goalw Relation.thy [id_def] "(a,b):id = (a=b)"; +by(fast_tac prod_cs 1); +qed "pair_in_id_conv"; + + +(** Composition of two relations **) + +val prems = goalw Relation.thy [comp_def] + "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s"; +by (fast_tac (set_cs addIs prems) 1); +qed "compI"; + +(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*) +val prems = goalw Relation.thy [comp_def] + "[| xz : r O s; \ +\ !!x y z. [| xz = (x,z); (x,y):s; (y,z):r |] ==> P \ +\ |] ==> P"; +by (cut_facts_tac prems 1); +by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1)); +qed "compE"; + +val prems = goal Relation.thy + "[| (a,c) : r O s; \ +\ !!y. [| (a,y):s; (y,c):r |] ==> P \ +\ |] ==> P"; +by (rtac compE 1); +by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1)); +qed "compEpair"; + +val comp_cs = prod_cs addIs [compI, idI] addSEs [compE, idE]; + +goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; +by (fast_tac comp_cs 1); +qed "comp_mono"; + +goal Relation.thy + "!!r s. [| s <= Sigma A (%x.B); r <= Sigma B (%x.C) |] ==> \ +\ (r O s) <= Sigma A (%x.C)"; +by (fast_tac comp_cs 1); +qed "comp_subset_Sigma"; + +(** Natural deduction for trans(r) **) + +val prems = goalw Relation.thy [trans_def] + "(!! x y z. [| (x,y):r; (y,z):r |] ==> (x,z):r) ==> trans(r)"; +by (REPEAT (ares_tac (prems@[allI,impI]) 1)); +qed "transI"; + +val major::prems = goalw Relation.thy [trans_def] + "[| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r"; +by (cut_facts_tac [major] 1); +by (fast_tac (HOL_cs addIs prems) 1); +qed "transD"; + +(** Natural deduction for converse(r) **) + +goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)"; +by (simp_tac prod_ss 1); +by (fast_tac set_cs 1); +qed "converseI"; + +goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r"; +by (fast_tac comp_cs 1); +qed "converseD"; + +qed_goalw "converseE" Relation.thy [converse_def] + "[| yx : converse(r); \ +\ !!x y. [| yx=(y,x); (x,y):r |] ==> P \ +\ |] ==> P" + (fn [major,minor]=> + [ (rtac (major RS CollectE) 1), + (REPEAT (eresolve_tac [bexE,exE, conjE, minor] 1)), + (hyp_subst_tac 1), + (assume_tac 1) ]); + +val converse_cs = comp_cs addSIs [converseI] + addSEs [converseD,converseE]; + +(** Domain **) + +qed_goalw "Domain_iff" Relation.thy [Domain_def] + "a: Domain(r) = (EX y. (a,y): r)" + (fn _=> [ (fast_tac comp_cs 1) ]); + +qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)" + (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]); + +qed_goal "DomainE" Relation.thy + "[| a : Domain(r); !!y. (a,y): r ==> P |] ==> P" + (fn prems=> + [ (rtac (Domain_iff RS iffD1 RS exE) 1), + (REPEAT (ares_tac prems 1)) ]); + +(** Range **) + +qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)" + (fn _ => [ (etac (converseI RS DomainI) 1) ]); + +qed_goalw "RangeE" Relation.thy [Range_def] + "[| b : Range(r); !!x. (x,b): r ==> P |] ==> P" + (fn major::prems=> + [ (rtac (major RS DomainE) 1), + (resolve_tac prems 1), + (etac converseD 1) ]); + +(*** Image of a set under a relation ***) + +qed_goalw "Image_iff" Relation.thy [Image_def] + "b : r^^A = (? x:A. (x,b):r)" + (fn _ => [ fast_tac (comp_cs addIs [RangeI]) 1 ]); + +qed_goal "Image_singleton_iff" Relation.thy + "(b : r^^{a}) = ((a,b):r)" + (fn _ => [ rtac (Image_iff RS trans) 1, + fast_tac comp_cs 1 ]); + +qed_goalw "ImageI" Relation.thy [Image_def] + "!!a b r. [| (a,b): r; a:A |] ==> b : r^^A" + (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)), + (resolve_tac [conjI ] 1), + (resolve_tac [RangeI] 1), + (REPEAT (fast_tac set_cs 1))]); + +qed_goalw "ImageE" Relation.thy [Image_def] + "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P" + (fn major::prems=> + [ (rtac (major RS CollectE) 1), + (safe_tac set_cs), + (etac RangeE 1), + (rtac (hd prems) 1), + (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]); + +qed_goal "Image_subset" Relation.thy + "!!A B r. r <= Sigma A (%x.B) ==> r^^C <= B" + (fn _ => + [ (rtac subsetI 1), + (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]); + +val rel_cs = converse_cs addSIs [converseI] + addIs [ImageI, DomainI, RangeI] + addSEs [ImageE, DomainE, RangeE]; + +val rel_eq_cs = rel_cs addSIs [equalityI]; + +val rel_ss = prod_ss addsimps [pair_in_id_conv]; diff -r 42ec82147d83 -r 64b30e3cc6d4 src/HOL/Relation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Relation.thy Fri May 26 18:11:47 1995 +0200 @@ -0,0 +1,27 @@ +(* Title: Relation.thy + ID: $Id$ + Author: Riccardo Mattolini, Dip. Sistemi e Informatica + and Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 Universita' di Firenze + Copyright 1993 University of Cambridge +*) + +Relation = Prod + +consts + id :: "('a * 'a)set" (*the identity relation*) + O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60) + trans :: "('a * 'a)set => bool" (*transitivity predicate*) + converse :: "('a*'a) set => ('a*'a) set" + "^^" :: "[('a*'a) set,'a set] => 'a set" (infixl 90) + Domain :: "('a*'a) set => 'a set" + Range :: "('a*'a) set => 'a set" +defs + id_def "id == {p. ? x. p = (x,x)}" + comp_def (*composition of relations*) + "r O s == {xz. ? x y z. xz = (x,z) & (x,y):s & (y,z):r}" + trans_def "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)" + converse_def "converse(r) == {z. (? w:r. ? x y. w=(x,y) & z=(y,x))}" + Domain_def "Domain(r) == {z. ! x. (z=x --> (? y. (x,y):r))}" + Range_def "Range(r) == Domain(converse(r))" + Image_def "r ^^ s == {y. y:Range(r) & (? x:s. (x,y):r)}" +end diff -r 42ec82147d83 -r 64b30e3cc6d4 src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Fri May 26 11:20:08 1995 +0200 +++ b/src/HOL/Trancl.ML Fri May 26 18:11:47 1995 +0200 @@ -8,76 +8,6 @@ open Trancl; -(** Natural deduction for trans(r) **) - -val prems = goalw Trancl.thy [trans_def] - "(!! x y z. [| (x,y):r; (y,z):r |] ==> (x,z):r) ==> trans(r)"; -by (REPEAT (ares_tac (prems@[allI,impI]) 1)); -qed "transI"; - -val major::prems = goalw Trancl.thy [trans_def] - "[| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r"; -by (cut_facts_tac [major] 1); -by (fast_tac (HOL_cs addIs prems) 1); -qed "transD"; - -(** Identity relation **) - -goalw Trancl.thy [id_def] "(a,a) : id"; -by (rtac CollectI 1); -by (rtac exI 1); -by (rtac refl 1); -qed "idI"; - -val major::prems = goalw Trancl.thy [id_def] - "[| p: id; !!x.[| p = (x,x) |] ==> P \ -\ |] ==> P"; -by (rtac (major RS CollectE) 1); -by (etac exE 1); -by (eresolve_tac prems 1); -qed "idE"; - -goalw Trancl.thy [id_def] "(a,b):id = (a=b)"; -by(fast_tac prod_cs 1); -qed "pair_in_id_conv"; - -(** Composition of two relations **) - -val prems = goalw Trancl.thy [comp_def] - "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s"; -by (fast_tac (set_cs addIs prems) 1); -qed "compI"; - -(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*) -val prems = goalw Trancl.thy [comp_def] - "[| xz : r O s; \ -\ !!x y z. [| xz = (x,z); (x,y):s; (y,z):r |] ==> P \ -\ |] ==> P"; -by (cut_facts_tac prems 1); -by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1)); -qed "compE"; - -val prems = goal Trancl.thy - "[| (a,c) : r O s; \ -\ !!y. [| (a,y):s; (y,c):r |] ==> P \ -\ |] ==> P"; -by (rtac compE 1); -by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1)); -qed "compEpair"; - -val comp_cs = prod_cs addIs [compI, idI] addSEs [compE, idE]; - -goal Trancl.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; -by (fast_tac comp_cs 1); -qed "comp_mono"; - -goal Trancl.thy - "!!r s. [| s <= Sigma A (%x.B); r <= Sigma B (%x.C) |] ==> \ -\ (r O s) <= Sigma A (%x.C)"; -by (fast_tac comp_cs 1); -qed "comp_subset_Sigma"; - - (** The relation rtrancl **) goal Trancl.thy "mono(%s. id Un (r O s))"; @@ -90,14 +20,14 @@ (*Reflexivity of rtrancl*) goal Trancl.thy "(a,a) : r^*"; by (stac rtrancl_unfold 1); -by (fast_tac comp_cs 1); +by (fast_tac rel_cs 1); qed "rtrancl_refl"; (*Closure under composition with r*) val prems = goal Trancl.thy "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*"; by (stac rtrancl_unfold 1); -by (fast_tac (comp_cs addIs prems) 1); +by (fast_tac (rel_cs addIs prems) 1); qed "rtrancl_into_rtrancl"; (*rtrancl of r contains r*) @@ -119,7 +49,7 @@ \ !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |] ==> P((x,z)) |] \ \ ==> P((a,b))"; by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1); -by (fast_tac (comp_cs addIs prems) 1); +by (fast_tac (rel_cs addIs prems) 1); qed "rtrancl_full_induct"; (*nice induction rule*) @@ -134,8 +64,8 @@ by (fast_tac HOL_cs 1); (*now do the induction*) by (resolve_tac [major RS rtrancl_full_induct] 1); -by (fast_tac (comp_cs addIs prems) 1); -by (fast_tac (comp_cs addIs prems) 1); +by (fast_tac (rel_cs addIs prems) 1); +by (fast_tac (rel_cs addIs prems) 1); qed "rtrancl_induct"; (*transitivity of transitive closure!! -- by induction.*) @@ -199,8 +129,8 @@ by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1)); by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1); by (etac rtranclE 1); -by (fast_tac comp_cs 1); -by (fast_tac (comp_cs addSIs [rtrancl_into_trancl1]) 1); +by (fast_tac rel_cs 1); +by (fast_tac (rel_cs addSIs [rtrancl_into_trancl1]) 1); qed "tranclE"; (*Transitivity of r^+. @@ -237,12 +167,10 @@ by (cut_facts_tac prems 1); by (rtac (major RS rtrancl_induct) 1); by (rtac (refl RS disjI1) 1); -by (fast_tac (comp_cs addSEs [SigmaE2]) 1); +by (fast_tac (rel_cs addSEs [SigmaE2]) 1); qed "trancl_subset_Sigma_lemma"; goalw Trancl.thy [trancl_def] "!!r. r <= Sigma A (%x.A) ==> trancl(r) <= Sigma A (%x.A)"; -by (fast_tac (comp_cs addSDs [trancl_subset_Sigma_lemma]) 1); +by (fast_tac (rel_cs addSDs [trancl_subset_Sigma_lemma]) 1); qed "trancl_subset_Sigma"; - -val prod_ss = prod_ss addsimps [pair_in_id_conv]; diff -r 42ec82147d83 -r 64b30e3cc6d4 src/HOL/Trancl.thy --- a/src/HOL/Trancl.thy Fri May 26 11:20:08 1995 +0200 +++ b/src/HOL/Trancl.thy Fri May 26 18:11:47 1995 +0200 @@ -3,24 +3,16 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -Transitive closure of a relation +Relfexive and Transitive closure of a relation -rtrancl is refl/transitive closure; trancl is transitive closure +rtrancl is refl&transitive closure; trancl is transitive closure *) -Trancl = Lfp + Prod + +Trancl = Lfp + Relation + consts - trans :: "('a * 'a)set => bool" (*transitivity predicate*) - id :: "('a * 'a)set" rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [100] 100) trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100) - O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60) defs -trans_def "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)" -comp_def (*composition of relations*) - "r O s == {xz. ? x y z. xz = (x,z) & (x,y):s & (y,z):r}" -id_def (*the identity relation*) - "id == {p. ? x. p = (x,x)}" rtrancl_def "r^* == lfp(%s. id Un (r O s))" trancl_def "r^+ == r O rtrancl(r)" end