# HG changeset patch # User oheimb # Date 891285244 -7200 # Node ID 9b3293646b5dbd4253ea86b54dc8cd8aae12a07f # Parent 56072b72d7309b701d64370b41bc191600b10e5f generalized appearance of trancl_into_rtrancl and r_into_trancl added irrefl_tranclI, reflcl_trancl, trancl_reflcl, trancl_empty, rtrancl_empty diff -r 56072b72d730 -r 9b3293646b5d src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Mon Mar 30 21:09:46 1998 +0200 +++ b/src/HOL/Trancl.ML Mon Mar 30 21:14:04 1998 +0200 @@ -1,9 +1,9 @@ -(* Title: HOL/trancl +(* Title: HOL/Trancl ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -For trancl.thy. Theorems about the transitive closure of a relation +For Trancl.thy. Theorems about the transitive closure of a relation *) open Trancl; @@ -208,15 +208,17 @@ (** Conversions between trancl and rtrancl **) -val [major] = goalw Trancl.thy [trancl_def] - "(a,b) : r^+ ==> (a,b) : r^*"; -by (resolve_tac [major RS compEpair] 1); +goalw Trancl.thy [trancl_def] + "!!p. p : r^+ ==> p : r^*"; +by (split_all_tac 1); +by (etac compEpair 1); by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1)); qed "trancl_into_rtrancl"; (*r^+ contains r*) -val [prem] = goalw Trancl.thy [trancl_def] - "[| (a,b) : r |] ==> (a,b) : r^+"; +goalw Trancl.thy [trancl_def] + "!!p. p : r ==> p : r^+"; +by (split_all_tac 1); by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1)); qed "r_into_trancl"; @@ -305,9 +307,17 @@ goalw Trancl.thy [trancl_def] "(r^-1)^+ = (r^+)^-1"; by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1); -by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,r_comp_rtrancl_eq]) 1); +by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,r_comp_rtrancl_eq])1); qed "trancl_converse"; +val irrefl_tranclI = prove_goal Trancl.thy + "!!r. r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+" (K [ + rtac allI 1, + subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1, + Fast_tac 1, + strip_tac 1, + etac trancl_induct 1, + auto_tac (claset() addEs [equals0D, r_into_trancl], simpset())]); val major::prems = goal Trancl.thy "[| (a,b) : r^*; r <= A Times A |] ==> a=b | a:A"; @@ -322,3 +332,37 @@ by (blast_tac (claset() addSDs [lemma]) 1); qed "trancl_subset_Sigma"; + +goal Trancl.thy "(r^+)^= = r^*"; +by Safe_tac; +by (etac trancl_into_rtrancl 1); +by (split_all_tac 1); +by (etac rtranclE 1); +auto(); +by (etac rtrancl_into_trancl1 1); +ba 1; +qed "reflcl_trancl"; +Addsimps[reflcl_trancl]; + +goal Trancl.thy "(r^=)^+ = r^*"; +by Safe_tac; +by (dtac trancl_into_rtrancl 1); +by (Asm_full_simp_tac 1); +by (split_all_tac 1); +by (etac rtranclE 1); +by Safe_tac; +by (rtac r_into_trancl 1); +by (Simp_tac 1); +by (rtac rtrancl_into_trancl1 1); +by (etac (rtrancl_reflcl RS equalityD2 RS subsetD) 1); +by (Fast_tac 1); +qed "trancl_reflcl"; +Addsimps[trancl_reflcl]; + +qed_goal "trancl_empty" Trancl.thy "{}^+ = {}" + (K [auto_tac (claset() addEs [trancl_induct], simpset())]); +Addsimps[trancl_empty]; + +qed_goal "rtrancl_empty" Trancl.thy "{}^* = id" + (K [rtac (reflcl_trancl RS subst) 1, Simp_tac 1]); +Addsimps[rtrancl_empty];