# HG changeset patch # User berghofe # Date 1037197482 -3600 # Node ID 854501b1e957fc997791ea456746718543bf2ce2 # Parent a36a0d417133627322fae3880b2afac811b8d0ca Transitive closure is now defined inductively as well. diff -r a36a0d417133 -r 854501b1e957 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sat Nov 09 00:12:25 2002 +0100 +++ b/src/HOL/Finite_Set.thy Wed Nov 13 15:24:42 2002 +0100 @@ -304,7 +304,7 @@ apply (rule trancl_subset_Field2 [THEN finite_subset]) apply (rule finite_SigmaI) prefer 3 - apply (blast intro: r_into_trancl finite_subset) + apply (blast intro: r_into_trancl' finite_subset) apply (auto simp add: finite_Field) done diff -r a36a0d417133 -r 854501b1e957 src/HOL/Transitive_Closure.ML --- a/src/HOL/Transitive_Closure.ML Sat Nov 09 00:12:25 2002 +0100 +++ b/src/HOL/Transitive_Closure.ML Wed Nov 13 15:24:42 2002 +0100 @@ -37,10 +37,10 @@ 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_trancl = thm "trancl_into_trancl"; val trancl_into_trancl2 = thm "trancl_into_trancl2"; val trancl_mono = thm "trancl_mono"; val trancl_subset_Sigma = thm "trancl_subset_Sigma"; diff -r a36a0d417133 -r 854501b1e957 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Sat Nov 09 00:12:25 2002 +0100 +++ b/src/HOL/Transitive_Closure.thy Wed Nov 13 15:24:42 2002 +0100 @@ -25,9 +25,13 @@ rtrancl_refl [intro!, CPure.intro!, simp]: "(a, a) : r^*" rtrancl_into_rtrancl [CPure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*" -constdefs +consts trancl :: "('a \ 'a) set => ('a \ 'a) set" ("(_^+)" [1000] 999) - "r^+ == r O rtrancl r" + +inductive "r^+" + intros + r_into_trancl [intro, CPure.intro]: "(a, b) : r ==> (a, b) : r^+" + trancl_into_trancl [CPure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+" syntax "_reflcl" :: "('a \ 'a) set => ('a \ 'a) set" ("(_^=)" [1000] 999) @@ -213,59 +217,44 @@ subsection {* Transitive closure *} -lemma trancl_mono: "p \ r^+ ==> r \ s ==> p \ s^+" - apply (unfold trancl_def) - apply (blast intro: rtrancl_mono [THEN subsetD]) +lemma trancl_mono: "!!p. p \ r^+ ==> r \ s ==> p \ s^+" + apply (simp only: split_tupled_all) + apply (erule trancl.induct) + apply (rules dest: subsetD)+ done +lemma r_into_trancl': "!!p. p : r ==> p : r^+" + by (simp only: split_tupled_all) (erule r_into_trancl) + 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 trancl_into_rtrancl: "(a, b) \ r^+ ==> (a, b) \ r^*" + by (erule trancl.induct) rules+ -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_trancl1: assumes r: "(a, b) \ r^*" + shows "!!c. (b, c) \ r ==> (a, c) \ r^+" using r + by induct rules+ 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 rules 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)" +lemma trancl_induct [consumes 1, induct set: trancl]: + assumes a: "(a,b) : r^+" + and cases: "!!y. (a, y) : r ==> P y" + "!!y z. (a,y) : r^+ ==> (y, z) : r ==> P y ==> P z" + shows "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 + from a have "a = a --> P b" + by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+ + thus ?thesis by rules qed lemma trancl_trans_induct: @@ -278,44 +267,25 @@ assume major: "(x,y) : r^+" case rule_context show ?thesis - by (blast intro: r_into_trancl major [THEN trancl_induct] prems) + by (rules 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 +inductive_cases tranclE: "(a, b) : r^+" 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 +proof (rule transI) + fix x y z + assume "(x, y) \ r^+" + assume "(y, z) \ r^+" + thus "(x, z) \ r^+" by induct (rules!)+ +qed 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 rtrancl_trancl_trancl: assumes r: "(x, y) \ r^*" + shows "!!z. (y, z) \ r^+ ==> (x, z) \ r^+" using r + by induct (rules intro: trancl_trans)+ lemma trancl_into_trancl2: "(a, b) \ r ==> (b, c) \ r^+ ==> (a, c) \ r^+" by (erule transD [OF trans_trancl r_into_trancl]) @@ -334,17 +304,21 @@ [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) +lemma trancl_converseI: "(x, y) \ (r^+)^-1 ==> (x, y) \ (r^-1)^+" + apply (drule converseD) + apply (erule trancl.induct) + apply (rules intro: converseI trancl_trans)+ 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" + apply (rule converseI) + apply (erule trancl.induct) + apply (rules dest: converseD intro: trancl_trans)+ + done -lemma trancl_converseD: "(x, y) \ (r^-1)^+ ==> (x, y) \ (r^+)^-1" - by (simp add: trancl_converse) +lemma trancl_converse: "(r^-1)^+ = (r^+)^-1" + by (fastsimp simp add: split_tupled_all + intro!: trancl_converseI trancl_converseD) lemma converse_trancl_induct: "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); @@ -385,8 +359,10 @@ done lemma trancl_subset_Sigma: "r \ A \ A ==> r^+ \ A \ A" - apply (unfold trancl_def) - apply (blast dest!: trancl_subset_Sigma_aux) + apply (rule subsetI) + apply (simp only: split_tupled_all) + apply (erule tranclE) + apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+ done lemma reflcl_trancl [simp]: "(r^+)^= = r^*" @@ -475,7 +451,6 @@ declare trancl_into_rtrancl [elim] declare rtranclE [cases set: rtrancl] -declare trancl_induct [induct set: trancl] declare tranclE [cases set: trancl] end