# HG changeset patch # User wenzelm # Date 1010594920 -3600 # Node ID d21db58bcdc23f2a41692460aeb65830cfc781e8 # Parent ac3fa7c05e5a9b8629aa659782cd698225eb00cb converted theory Transitive_Closure; diff -r ac3fa7c05e5a -r d21db58bcdc2 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jan 09 17:42:49 2002 +0100 +++ b/src/HOL/IsaMakefile Wed Jan 09 17:48:40 2002 +0100 @@ -18,7 +18,6 @@ HOL-CTL \ HOL-GroupTheory \ HOL-Real-HahnBanach \ - HOL-Real-Hyperreal \ HOL-Real-ex \ HOL-Hoare \ HOL-IMP \ @@ -101,7 +100,7 @@ Tools/primrec_package.ML Tools/recdef_package.ML Tools/recfun_codegen.ML \ Tools/record_package.ML Tools/split_rule.ML \ Tools/svc_funcs.ML Tools/typedef_package.ML \ - Transitive_Closure.thy Transitive_Closure_lemmas.ML Typedef.thy \ + Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \ Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \ Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \ document/root.tex equalities.ML hologic.ML meson_lemmas.ML mono.ML \ diff -r ac3fa7c05e5a -r d21db58bcdc2 src/HOL/Transitive_Closure.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Transitive_Closure.ML Wed Jan 09 17:48:40 2002 +0100 @@ -0,0 +1,50 @@ + +(* legacy ML bindings *) + +val converse_rtranclE = thm "converse_rtranclE"; +val converse_rtranclE2 = thm "converse_rtranclE2"; +val converse_rtrancl_induct = thm "converse_rtrancl_induct"; +val converse_rtrancl_induct2 = thm "converse_rtrancl_induct2"; +val converse_rtrancl_into_rtrancl = thm "converse_rtrancl_into_rtrancl"; +val converse_trancl_induct = thm "converse_trancl_induct"; +val irrefl_tranclI = thm "irrefl_tranclI"; +val irrefl_trancl_rD = thm "irrefl_trancl_rD"; +val r_comp_rtrancl_eq = thm "r_comp_rtrancl_eq"; +val r_into_rtrancl = thm "r_into_rtrancl"; +val r_into_trancl = thm "r_into_trancl"; +val rtranclE = thm "rtranclE"; +val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl"; +val rtrancl_converse = thm "rtrancl_converse"; +val rtrancl_converseD = thm "rtrancl_converseD"; +val rtrancl_converseI = thm "rtrancl_converseI"; +val rtrancl_idemp = thm "rtrancl_idemp"; +val rtrancl_idemp_self_comp = thm "rtrancl_idemp_self_comp"; +val rtrancl_induct = thm "rtrancl_induct"; +val rtrancl_induct2 = thm "rtrancl_induct2"; +val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl"; +val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1"; +val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2"; +val rtrancl_mono = thm "rtrancl_mono"; +val rtrancl_r_diff_Id = thm "rtrancl_r_diff_Id"; +val rtrancl_refl = thm "rtrancl_refl"; +val rtrancl_reflcl = thm "rtrancl_reflcl"; +val rtrancl_subset = thm "rtrancl_subset"; +val rtrancl_subset_rtrancl = thm "rtrancl_subset_rtrancl"; +val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl"; +val rtrancl_trans = thm "rtrancl_trans"; +val tranclD = thm "tranclD"; +val tranclE = thm "tranclE"; +val trancl_converse = thm "trancl_converse"; +val trancl_converseD = thm "trancl_converseD"; +val trancl_converseI = thm "trancl_converseI"; +val trancl_def = thm "trancl_def"; +val trancl_induct = thm "trancl_induct"; +val trancl_insert = thm "trancl_insert"; +val trancl_into_rtrancl = thm "trancl_into_rtrancl"; +val trancl_into_trancl2 = thm "trancl_into_trancl2"; +val trancl_mono = thm "trancl_mono"; +val trancl_subset_Sigma = thm "trancl_subset_Sigma"; +val trancl_trans = thm "trancl_trans"; +val trancl_trans_induct = thm "trancl_trans_induct"; +val trans_rtrancl = thm "trans_rtrancl"; +val trans_trancl = thm "trans_trancl"; diff -r ac3fa7c05e5a -r d21db58bcdc2 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Wed Jan 09 17:42:49 2002 +0100 +++ b/src/HOL/Transitive_Closure.thy Wed Jan 09 17:48:40 2002 +0100 @@ -2,48 +2,394 @@ ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge - -Relfexive and Transitive closure of a relation - -rtrancl is reflexive/transitive closure; -trancl is transitive closure -reflcl is reflexive closure - -These postfix operators have MAXIMUM PRIORITY, forcing their operands -to be atomic. *) -theory Transitive_Closure = Inductive -files ("Transitive_Closure_lemmas.ML"): +header {* Reflexive and Transitive closure of a relation *} + +theory Transitive_Closure = Inductive: + +text {* + @{text rtrancl} is reflexive/transitive closure, + @{text trancl} is transitive closure, + @{text reflcl} is reflexive closure. + + These postfix operators have \emph{maximum priority}, forcing their + operands to be atomic. +*} consts - rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_^*)" [1000] 999) + rtrancl :: "('a \ 'a) set => ('a \ 'a) set" ("(_^*)" [1000] 999) inductive "r^*" -intros - rtrancl_refl [intro!, simp]: "(a, a) : r^*" - rtrancl_into_rtrancl: "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*" + intros + rtrancl_refl [intro!, simp]: "(a, a) : r^*" + rtrancl_into_rtrancl: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*" constdefs - trancl :: "('a * 'a) set => ('a * 'a) set" ("(_^+)" [1000] 999) + trancl :: "('a \ 'a) set => ('a \ 'a) set" ("(_^+)" [1000] 999) "r^+ == r O rtrancl r" syntax - "_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_^=)" [1000] 999) + "_reflcl" :: "('a \ 'a) set => ('a \ 'a) set" ("(_^=)" [1000] 999) translations - "r^=" == "r Un Id" + "r^=" == "r \ Id" syntax (xsymbols) - rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>*)" [1000] 999) - trancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>+)" [1000] 999) - "_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>=)" [1000] 999) + rtrancl :: "('a \ 'a) set => ('a \ 'a) set" ("(_\\<^sup>*)" [1000] 999) + trancl :: "('a \ 'a) set => ('a \ 'a) set" ("(_\\<^sup>+)" [1000] 999) + "_reflcl" :: "('a \ 'a) set => ('a \ 'a) set" ("(_\\<^sup>=)" [1000] 999) + + +subsection {* Reflexive-transitive closure *} + +lemma r_into_rtrancl [intro]: "!!p. p \ r ==> p \ r^*" + -- {* @{text rtrancl} of @{text r} contains @{text r} *} + apply (simp only: split_tupled_all) + apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) + done + +lemma rtrancl_mono: "r \ s ==> r^* \ s^*" + -- {* monotonicity of @{text rtrancl} *} + apply (rule subsetI) + apply (simp only: split_tupled_all) + apply (erule rtrancl.induct) + apply (rule_tac [2] rtrancl_into_rtrancl) + apply blast+ + done + +theorem rtrancl_induct [consumes 1]: + (assumes a: "(a, b) : r^*" + and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z") + "P b" +proof - + from a have "a = a --> P b" + by (induct "%x y. x = a --> P y" a b rule: rtrancl.induct) + (rules intro: cases)+ + thus ?thesis by rules +qed + +ML_setup {* + bind_thm ("rtrancl_induct2", split_rule + (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] (thm "rtrancl_induct"))); +*} + +lemma trans_rtrancl: "trans(r^*)" + -- {* transitivity of transitive closure!! -- by induction *} + apply (unfold trans_def) + apply safe + apply (erule_tac b = z in rtrancl_induct) + apply (blast intro: rtrancl_into_rtrancl)+ + done + +lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard] + +lemma rtranclE: + "[| (a::'a,b) : r^*; (a = b) ==> P; + !!y.[| (a,y) : r^*; (y,b) : r |] ==> P + |] ==> P" + -- {* elimination of @{text rtrancl} -- by induction on a special formula *} +proof - + assume major: "(a::'a,b) : r^*" + case rule_context + show ?thesis + apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)") + apply (rule_tac [2] major [THEN rtrancl_induct]) + prefer 2 apply (blast!) + prefer 2 apply (blast!) + apply (erule asm_rl exE disjE conjE prems)+ + done +qed + +lemmas converse_rtrancl_into_rtrancl = r_into_rtrancl [THEN rtrancl_trans, standard] + +text {* + \medskip More @{term "r^*"} equations and inclusions. +*} + +lemma rtrancl_idemp [simp]: "(r^*)^* = r^*" + apply auto + apply (erule rtrancl_induct) + apply (rule rtrancl_refl) + apply (blast intro: rtrancl_trans) + done + +lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*" + apply (rule set_ext) + apply (simp only: split_tupled_all) + apply (blast intro: rtrancl_trans) + done + +lemma rtrancl_subset_rtrancl: "r \ s^* ==> r^* \ s^*" + apply (drule rtrancl_mono) + apply simp + done + +lemma rtrancl_subset: "R \ S ==> S \ R^* ==> S^* = R^*" + apply (drule rtrancl_mono) + apply (drule rtrancl_mono) + apply simp + apply blast + done + +lemma rtrancl_Un_rtrancl: "(R^* \ S^*)^* = (R \ S)^*" + by (blast intro!: rtrancl_subset intro: r_into_rtrancl rtrancl_mono [THEN subsetD]) + +lemma rtrancl_reflcl [simp]: "(R^=)^* = R^*" + by (blast intro!: rtrancl_subset intro: r_into_rtrancl) + +lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*" + apply (rule sym) + apply (rule rtrancl_subset) + apply blast + apply clarify + apply (rename_tac a b) + apply (case_tac "a = b") + apply blast + apply (blast intro!: r_into_rtrancl) + done + +lemma rtrancl_converseD: "(x, y) \ (r^-1)^* ==> (y, x) \ r^*" + apply (erule rtrancl_induct) + apply (rule rtrancl_refl) + apply (blast intro: rtrancl_trans) + done + +lemma rtrancl_converseI: "(y, x) \ r^* ==> (x, y) \ (r^-1)^*" + apply (erule rtrancl_induct) + apply (rule rtrancl_refl) + apply (blast intro: rtrancl_trans) + done + +lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1" + by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) + +lemma converse_rtrancl_induct: + "[| (a,b) : r^*; P(b); + !!y z.[| (y,z) : r; (z,b) : r^*; P(z) |] ==> P(y) |] + ==> P(a)" +proof - + assume major: "(a,b) : r^*" + case rule_context + show ?thesis + apply (rule major [THEN rtrancl_converseI, THEN rtrancl_induct]) + apply assumption + apply (blast! dest!: rtrancl_converseD) + done +qed + +ML_setup {* + bind_thm ("converse_rtrancl_induct2", split_rule + (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")] (thm "converse_rtrancl_induct"))); +*} + +lemma converse_rtranclE: + "[| (x,z):r^*; + x=z ==> P; + !!y. [| (x,y):r; (y,z):r^* |] ==> P + |] ==> P" +proof - + assume major: "(x,z):r^*" + case rule_context + show ?thesis + apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)") + apply (rule_tac [2] major [THEN converse_rtrancl_induct]) + prefer 2 apply (blast!) + prefer 2 apply (blast!) + apply (erule asm_rl exE disjE conjE prems)+ + done +qed + +ML_setup {* + bind_thm ("converse_rtranclE2", split_rule + (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] (thm "converse_rtranclE"))); +*} + +lemma r_comp_rtrancl_eq: "r O r^* = r^* O r" + by (blast elim: rtranclE converse_rtranclE + intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl) + + +subsection {* Transitive closure *} -use "Transitive_Closure_lemmas.ML" +lemma trancl_mono: "p \ r^+ ==> r \ s ==> p \ s^+" + apply (unfold trancl_def) + apply (blast intro: rtrancl_mono [THEN subsetD]) + done + +text {* + \medskip Conversions between @{text trancl} and @{text rtrancl}. +*} + +lemma trancl_into_rtrancl: "!!p. p \ r^+ ==> p \ r^*" + apply (unfold trancl_def) + apply (simp only: split_tupled_all) + apply (erule rel_compEpair) + apply (assumption | rule rtrancl_into_rtrancl)+ + done + +lemma r_into_trancl [intro]: "!!p. p \ r ==> p \ r^+" + -- {* @{text "r^+"} contains @{text r} *} + apply (unfold trancl_def) + apply (simp only: split_tupled_all) + apply (assumption | rule rel_compI rtrancl_refl)+ + done + +lemma rtrancl_into_trancl1: "(a, b) \ r^* ==> (b, c) \ r ==> (a, c) \ r^+" + -- {* intro rule by definition: from @{text rtrancl} and @{text r} *} + by (auto simp add: trancl_def) + +lemma rtrancl_into_trancl2: "[| (a,b) : r; (b,c) : r^* |] ==> (a,c) : r^+" + -- {* intro rule from @{text r} and @{text rtrancl} *} + apply (erule rtranclE) + apply (blast intro: r_into_trancl) + apply (rule rtrancl_trans [THEN rtrancl_into_trancl1]) + apply (assumption | rule r_into_rtrancl)+ + done + +lemma trancl_induct: + "[| (a,b) : r^+; + !!y. [| (a,y) : r |] ==> P(y); + !!y z.[| (a,y) : r^+; (y,z) : r; P(y) |] ==> P(z) + |] ==> P(b)" + -- {* Nice induction rule for @{text trancl} *} +proof - + assume major: "(a, b) : r^+" + case rule_context + show ?thesis + apply (rule major [unfolded trancl_def, THEN rel_compEpair]) + txt {* by induction on this formula *} + apply (subgoal_tac "ALL z. (y,z) : r --> P (z)") + txt {* now solve first subgoal: this formula is sufficient *} + apply blast + apply (erule rtrancl_induct) + apply (blast intro: rtrancl_into_trancl1 prems)+ + done +qed + +lemma trancl_trans_induct: + "[| (x,y) : r^+; + !!x y. (x,y) : r ==> P x y; + !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z + |] ==> P x y" + -- {* Another induction rule for trancl, incorporating transitivity *} +proof - + assume major: "(x,y) : r^+" + case rule_context + show ?thesis + by (blast intro: r_into_trancl major [THEN trancl_induct] prems) +qed + +lemma tranclE: + "[| (a::'a,b) : r^+; + (a,b) : r ==> P; + !!y.[| (a,y) : r^+; (y,b) : r |] ==> P + |] ==> P" + -- {* elimination of @{text "r^+"} -- \emph{not} an induction rule *} +proof - + assume major: "(a::'a,b) : r^+" + case rule_context + show ?thesis + apply (subgoal_tac "(a::'a, b) : r | (EX y. (a,y) : r^+ & (y,b) : r)") + apply (erule asm_rl disjE exE conjE prems)+ + apply (rule major [unfolded trancl_def, THEN rel_compEpair]) + apply (erule rtranclE) + apply blast + apply (blast intro!: rtrancl_into_trancl1) + done +qed +lemma trans_trancl: "trans(r^+)" + -- {* Transitivity of @{term "r^+"} *} + -- {* Proved by unfolding since it uses transitivity of @{text rtrancl} *} + apply (unfold trancl_def) + apply (rule transI) + apply (erule rel_compEpair)+ + apply (rule rtrancl_into_rtrancl [THEN rtrancl_trans [THEN rel_compI]]) + apply assumption+ + done + +lemmas trancl_trans = trans_trancl [THEN transD, standard] + +lemma rtrancl_trancl_trancl: "(x, y) \ r^* ==> (y, z) \ r^+ ==> (x, z) \ r^+" + apply (unfold trancl_def) + apply (blast intro: rtrancl_trans) + done + +lemma trancl_into_trancl2: "(a, b) \ r ==> (b, c) \ r^+ ==> (a, c) \ r^+" + by (erule transD [OF trans_trancl r_into_trancl]) + +lemma trancl_insert: + "(insert (y, x) r)^+ = r^+ \ {(a, b). (a, y) \ r^* \ (x, b) \ r^*}" + -- {* primitive recursion for @{text trancl} over finite relations *} + apply (rule equalityI) + apply (rule subsetI) + apply (simp only: split_tupled_all) + apply (erule trancl_induct) + apply blast + apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans) + apply (rule subsetI) + apply (blast intro: trancl_mono rtrancl_mono + [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) + done + +lemma trancl_converse: "(r^-1)^+ = (r^+)^-1" + apply (unfold trancl_def) + apply (simp add: rtrancl_converse converse_rel_comp) + apply (simp add: rtrancl_converse [symmetric] r_comp_rtrancl_eq) + done + +lemma trancl_converseI: "(x, y) \ (r^+)^-1 ==> (x,y) \ (r^-1)^+" + by (simp add: trancl_converse) + +lemma trancl_converseD: "(x, y) \ (r^-1)^+ ==> (x, y) \ (r^+)^-1" + by (simp add: trancl_converse) + +lemma converse_trancl_induct: + "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); + !!y z.[| (y,z) : r; (z,b) : r^+; P(z) |] ==> P(y) |] + ==> P(a)" +proof - + assume major: "(a,b) : r^+" + case rule_context + show ?thesis + apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]]) + apply (rule prems) + apply (erule converseD) + apply (blast intro: prems dest!: trancl_converseD) + done +qed + +lemma tranclD: "(x, y) \ R^+ ==> EX z. (x, z) \ R \ (z, y) \ R^*" + apply (erule converse_trancl_induct) + apply auto + apply (blast intro: rtrancl_trans) + done + +lemma irrefl_tranclI: "r^-1 \ r^+ = {} ==> (x, x) \ r^+" + apply (subgoal_tac "ALL y. (x, y) : r^+ --> x \ y") + apply fast + apply (intro strip) + apply (erule trancl_induct) + apply (auto intro: r_into_trancl) + done + +lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \ r^+ ==> (x, y) \ r ==> x \ y" + by (blast dest: r_into_trancl) + +lemma trancl_subset_Sigma_aux: + "(a, b) \ r^* ==> r \ A \ A ==> a = b \ a \ A" + apply (erule rtrancl_induct) + apply auto + done + +lemma trancl_subset_Sigma: "r \ A \ A ==> r^+ \ A \ A" + apply (unfold trancl_def) + apply (blast dest!: trancl_subset_Sigma_aux) + done lemma reflcl_trancl [simp]: "(r^+)^= = r^*" apply safe - apply (erule trancl_into_rtrancl) + apply (erule trancl_into_rtrancl) apply (blast elim: rtranclE dest: rtrancl_into_trancl1) done @@ -70,7 +416,7 @@ by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl) -(* should be merged with the main body of lemmas: *) +text {* @{text Domain} and @{text Range} *} lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV" by blast @@ -91,24 +437,26 @@ by (simp add: Range_def trancl_converse [symmetric]) lemma Not_Domain_rtrancl: - "x ~: Domain R ==> ((x, y) : R^*) = (x = y)" - apply (auto) - by (erule rev_mp, erule rtrancl_induct, auto) + "x ~: Domain R ==> ((x, y) : R^*) = (x = y)" + apply auto + by (erule rev_mp, erule rtrancl_induct, auto) + -(* more about converse rtrancl and trancl, should be merged with main body *) +text {* More about converse @{text rtrancl} and @{text trancl}, should + be merged with main body. *} -lemma r_r_into_trancl: "(a,b) \ R \ (b,c) \ R \ (a,c) \ R^+" +lemma r_r_into_trancl: "(a, b) \ R ==> (b, c) \ R ==> (a, c) \ R^+" by (fast intro: trancl_trans) lemma trancl_into_trancl [rule_format]: - "(a,b) \ r\<^sup>+ \ (b,c) \ r \ (a,c) \ r\<^sup>+" - apply (erule trancl_induct) + "(a, b) \ r\<^sup>+ ==> (b, c) \ r --> (a,c) \ r\<^sup>+" + apply (erule trancl_induct) apply (fast intro: r_r_into_trancl) apply (fast intro: r_r_into_trancl trancl_trans) done lemma trancl_rtrancl_trancl: - "(a,b) \ r\<^sup>+ \ (b,c) \ r\<^sup>* \ (a,c) \ r\<^sup>+" + "(a, b) \ r\<^sup>+ ==> (b, c) \ r\<^sup>* ==> (a, c) \ r\<^sup>+" apply (drule tranclD) apply (erule exE, erule conjE) apply (drule rtrancl_trans, assumption) @@ -116,10 +464,11 @@ apply assumption done -lemmas [trans] = r_r_into_trancl trancl_trans rtrancl_trans - trancl_into_trancl trancl_into_trancl2 - rtrancl_into_rtrancl converse_rtrancl_into_rtrancl - rtrancl_trancl_trancl trancl_rtrancl_trancl +lemmas transitive_closure_trans [trans] = + r_r_into_trancl trancl_trans rtrancl_trans + trancl_into_trancl trancl_into_trancl2 + rtrancl_into_rtrancl converse_rtrancl_into_rtrancl + rtrancl_trancl_trancl trancl_rtrancl_trancl declare trancl_into_rtrancl [elim] diff -r ac3fa7c05e5a -r d21db58bcdc2 src/HOL/Transitive_Closure_lemmas.ML --- a/src/HOL/Transitive_Closure_lemmas.ML Wed Jan 09 17:42:49 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,333 +0,0 @@ -(* Title: HOL/Transitive_Closure_lemmas.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Theorems about the transitive closure of a relation -*) - -val rtrancl_refl = thm "rtrancl_refl"; -val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl"; -val trancl_def = thm "trancl_def"; - - -(** The relation rtrancl **) - -section "^*"; - -(*rtrancl of r contains r*) -Goal "!!p. p : r ==> p : r^*"; -by (split_all_tac 1); -by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1); -qed "r_into_rtrancl"; - -AddIs [r_into_rtrancl]; - -(*monotonicity of rtrancl*) -Goal "r <= s ==> r^* <= s^*"; -by (rtac subsetI 1); -by (split_all_tac 1); -by (etac (thm "rtrancl.induct") 1); -by (rtac rtrancl_into_rtrancl 2); -by (ALLGOALS Blast_tac); -qed "rtrancl_mono"; - -(*nice induction rule*) -val major::prems = Goal - "[| (a::'a,b) : r^*; \ -\ P(a); \ -\ !!y z.[| (a,y) : r^*; (y,z) : r; P(y) |] ==> P(z) |] \ -\ ==> P(b)"; -by (rtac (read_instantiate [("P","%x y. x = a --> P y")] - (major RS thm "rtrancl.induct") RS mp) 1); -by (ALLGOALS (blast_tac (claset() addIs prems))); -qed "rtrancl_induct"; - -bind_thm ("rtrancl_induct2", split_rule - (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct)); - -(*transitivity of transitive closure!! -- by induction.*) -Goalw [trans_def] "trans(r^*)"; -by Safe_tac; -by (eres_inst_tac [("b","z")] rtrancl_induct 1); -by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl]))); -qed "trans_rtrancl"; - -bind_thm ("rtrancl_trans", trans_rtrancl RS transD); - - -(*elimination of rtrancl -- by induction on a special formula*) -val major::prems = Goal - "[| (a::'a,b) : r^*; (a = b) ==> P; \ -\ !!y.[| (a,y) : r^*; (y,b) : r |] ==> P \ -\ |] ==> P"; -by (subgoal_tac "(a::'a) = b | (? y. (a,y) : r^* & (y,b) : r)" 1); -by (rtac (major RS rtrancl_induct) 2); -by (blast_tac (claset() addIs prems) 2); -by (blast_tac (claset() addIs prems) 2); -by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1)); -qed "rtranclE"; - -bind_thm ("converse_rtrancl_into_rtrancl", r_into_rtrancl RS rtrancl_trans); - -(*** More r^* equations and inclusions ***) - -Goal "(r^*)^* = r^*"; -by Auto_tac; -by (etac rtrancl_induct 1); -by (rtac rtrancl_refl 1); -by (blast_tac (claset() addIs [rtrancl_trans]) 1); -qed "rtrancl_idemp"; -Addsimps [rtrancl_idemp]; - -Goal "R^* O R^* = R^*"; -by (rtac set_ext 1); -by (split_all_tac 1); -by (blast_tac (claset() addIs [rtrancl_trans]) 1); -qed "rtrancl_idemp_self_comp"; -Addsimps [rtrancl_idemp_self_comp]; - -Goal "r <= s^* ==> r^* <= s^*"; -by (dtac rtrancl_mono 1); -by (Asm_full_simp_tac 1); -qed "rtrancl_subset_rtrancl"; - -Goal "[| R <= S; S <= R^* |] ==> S^* = R^*"; -by (dtac rtrancl_mono 1); -by (dtac rtrancl_mono 1); -by (Asm_full_simp_tac 1); -by (Blast_tac 1); -qed "rtrancl_subset"; - -Goal "(R^* Un S^*)^* = (R Un S)^*"; -by (blast_tac (claset() addSIs [rtrancl_subset] - addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1); -qed "rtrancl_Un_rtrancl"; - -Goal "(R^=)^* = R^*"; -by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1); -qed "rtrancl_reflcl"; -Addsimps [rtrancl_reflcl]; - -Goal "(r - Id)^* = r^*"; -by (rtac sym 1); -by (rtac rtrancl_subset 1); - by (Blast_tac 1); -by (Clarify_tac 1); -by (rename_tac "a b" 1); -by (case_tac "a=b" 1); - by (Blast_tac 1); -by (blast_tac (claset() addSIs [r_into_rtrancl]) 1); -qed "rtrancl_r_diff_Id"; - -Goal "(x,y) : (r^-1)^* ==> (y,x) : r^*"; -by (etac rtrancl_induct 1); -by (rtac rtrancl_refl 1); -by (blast_tac (claset() addIs [rtrancl_trans]) 1); -qed "rtrancl_converseD"; - -Goal "(y,x) : r^* ==> (x,y) : (r^-1)^*"; -by (etac rtrancl_induct 1); -by (rtac rtrancl_refl 1); -by (blast_tac (claset() addIs [rtrancl_trans]) 1); -qed "rtrancl_converseI"; - -Goal "(r^-1)^* = (r^*)^-1"; -(*blast_tac fails: the split_all_tac wrapper must be called to convert - the set element to a pair*) -by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI])); -qed "rtrancl_converse"; - -val major::prems = Goal - "[| (a,b) : r^*; P(b); \ -\ !!y z.[| (y,z) : r; (z,b) : r^*; P(z) |] ==> P(y) |] \ -\ ==> P(a)"; -by (rtac (major RS rtrancl_converseI RS rtrancl_induct) 1); -by (resolve_tac prems 1); -by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1); -qed "converse_rtrancl_induct"; - -bind_thm ("converse_rtrancl_induct2", split_rule - (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")]converse_rtrancl_induct)); - -val major::prems = Goal - "[| (x,z):r^*; \ -\ x=z ==> P; \ -\ !!y. [| (x,y):r; (y,z):r^* |] ==> P \ -\ |] ==> P"; -by (subgoal_tac "x = z | (? y. (x,y) : r & (y,z) : r^*)" 1); -by (rtac (major RS converse_rtrancl_induct) 2); -by (blast_tac (claset() addIs prems) 2); -by (blast_tac (claset() addIs prems) 2); -by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1)); -qed "converse_rtranclE"; - -bind_thm ("converse_rtranclE2", split_rule - (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] converse_rtranclE)); - -Goal "r O r^* = r^* O r"; -by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] - addIs [rtrancl_into_rtrancl, converse_rtrancl_into_rtrancl]) 1); -qed "r_comp_rtrancl_eq"; - - -(**** The relation trancl ****) - -section "^+"; - -Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+"; -by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1); -qed "trancl_mono"; - -(** Conversions between trancl and rtrancl **) - -Goalw [trancl_def] - "!!p. p : r^+ ==> p : r^*"; -by (split_all_tac 1); -by (etac rel_compEpair 1); -by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1)); -qed "trancl_into_rtrancl"; - -(*r^+ contains r*) -Goalw [trancl_def] - "!!p. p : r ==> p : r^+"; -by (split_all_tac 1); -by (REPEAT (ares_tac [prem,rel_compI,rtrancl_refl] 1)); -qed "r_into_trancl"; -AddIs [r_into_trancl]; - -(*intro rule by definition: from rtrancl and r*) -Goalw [trancl_def] "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^+"; -by Auto_tac; -qed "rtrancl_into_trancl1"; - -(*intro rule from r and rtrancl*) -Goal "[| (a,b) : r; (b,c) : r^* |] ==> (a,c) : r^+"; -by (etac rtranclE 1); -by (blast_tac (claset() addIs [r_into_trancl]) 1); -by (rtac (rtrancl_trans RS rtrancl_into_trancl1) 1); -by (REPEAT (ares_tac [r_into_rtrancl] 1)); -qed "rtrancl_into_trancl2"; - -(*Nice induction rule for trancl*) -val major::prems = Goal - "[| (a,b) : r^+; \ -\ !!y. [| (a,y) : r |] ==> P(y); \ -\ !!y z.[| (a,y) : r^+; (y,z) : r; P(y) |] ==> P(z) \ -\ |] ==> P(b)"; -by (rtac (rewrite_rule [trancl_def] major RS rel_compEpair) 1); -(*by induction on this formula*) -by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1); -(*now solve first subgoal: this formula is sufficient*) -by (Blast_tac 1); -by (etac rtrancl_induct 1); -by (ALLGOALS (blast_tac (claset() addIs (rtrancl_into_trancl1::prems)))); -qed "trancl_induct"; - -(*Another induction rule for trancl, incorporating transitivity.*) -val major::prems = Goal - "[| (x,y) : r^+; \ -\ !!x y. (x,y) : r ==> P x y; \ -\ !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \ -\ |] ==> P x y"; -by (blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1); -qed "trancl_trans_induct"; - -(*elimination of r^+ -- NOT an induction rule*) -val major::prems = Goal - "[| (a::'a,b) : r^+; \ -\ (a,b) : r ==> P; \ -\ !!y.[| (a,y) : r^+; (y,b) : r |] ==> P \ -\ |] ==> P"; -by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+ & (y,b) : r)" 1); -by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1)); -by (rtac (rewrite_rule [trancl_def] major RS rel_compEpair) 1); -by (etac rtranclE 1); -by (Blast_tac 1); -by (blast_tac (claset() addSIs [rtrancl_into_trancl1]) 1); -qed "tranclE"; - -(*Transitivity of r^+. - Proved by unfolding since it uses transitivity of rtrancl. *) -Goalw [trancl_def] "trans(r^+)"; -by (rtac transI 1); -by (REPEAT (etac rel_compEpair 1)); -by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS rel_compI)) 1); -by (REPEAT (assume_tac 1)); -qed "trans_trancl"; - -bind_thm ("trancl_trans", trans_trancl RS transD); - -Goalw [trancl_def] "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+"; -by (blast_tac (claset() addIs [rtrancl_trans]) 1); -qed "rtrancl_trancl_trancl"; - -(* "[| (a,b) : r; (b,c) : r^+ |] ==> (a,c) : r^+" *) -bind_thm ("trancl_into_trancl2", [trans_trancl, r_into_trancl] MRS transD); - -(* primitive recursion for trancl over finite relations: *) -Goal "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}"; -by (rtac equalityI 1); - by (rtac subsetI 1); - by (split_all_tac 1); - by (etac trancl_induct 1); - by (blast_tac (claset() addIs [r_into_trancl]) 1); - by (blast_tac (claset() addIs - [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1); -by (rtac subsetI 1); -by (blast_tac (claset() addIs - [rtrancl_into_trancl2, rtrancl_trancl_trancl, - impOfSubs rtrancl_mono, trancl_mono]) 1); -qed "trancl_insert"; - -Goalw [trancl_def] "(r^-1)^+ = (r^+)^-1"; -by (simp_tac (simpset() addsimps [rtrancl_converse,converse_rel_comp]) 1); -by (simp_tac (simpset() addsimps [rtrancl_converse RS sym, - r_comp_rtrancl_eq]) 1); -qed "trancl_converse"; - -Goal "(x,y) : (r^+)^-1 ==> (x,y) : (r^-1)^+"; -by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1); -qed "trancl_converseI"; - -Goal "(x,y) : (r^-1)^+ ==> (x,y) : (r^+)^-1"; -by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1); -qed "trancl_converseD"; - -val major::prems = Goal - "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); \ -\ !!y z.[| (y,z) : r; (z,b) : r^+; P(z) |] ==> P(y) |] \ -\ ==> P(a)"; -by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1); - by (resolve_tac prems 1); - by (etac converseD 1); -by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1); -qed "converse_trancl_induct"; - -Goal "(x,y):R^+ ==> ? z. (x,z):R & (z,y):R^*"; -by (etac converse_trancl_induct 1); -by Auto_tac; -by (blast_tac (claset() addIs [rtrancl_trans]) 1); -qed "tranclD"; - -(*Unused*) -Goal "r^-1 Int r^+ = {} ==> (x, x) ~: r^+"; -by (subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1); -by (Fast_tac 1); -by (strip_tac 1); -by (etac trancl_induct 1); -by (auto_tac (claset() addIs [r_into_trancl], simpset())); -qed "irrefl_tranclI"; - -Goal "!!X. [| !x. (x, x) ~: r^+; (x,y) : r |] ==> x ~= y"; -by (blast_tac (claset() addDs [r_into_trancl]) 1); -qed "irrefl_trancl_rD"; - -Goal "[| (a,b) : r^*; r <= A <*> A |] ==> a=b | a:A"; -by (etac rtrancl_induct 1); -by Auto_tac; -val lemma = result(); - -Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A"; -by (blast_tac (claset() addSDs [lemma]) 1); -qed "trancl_subset_Sigma";