Transitive closure is now defined inductively as well.
authorberghofe
Wed Nov 13 15:24:42 2002 +0100 (2002-11-13)
changeset 13704854501b1e957
parent 13703 a36a0d417133
child 13705 934d6c1421f2
Transitive closure is now defined inductively as well.
src/HOL/Finite_Set.thy
src/HOL/Transitive_Closure.ML
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Sat Nov 09 00:12:25 2002 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Nov 13 15:24:42 2002 +0100
     1.3 @@ -304,7 +304,7 @@
     1.4     apply (rule trancl_subset_Field2 [THEN finite_subset])
     1.5     apply (rule finite_SigmaI)
     1.6      prefer 3
     1.7 -    apply (blast intro: r_into_trancl finite_subset)
     1.8 +    apply (blast intro: r_into_trancl' finite_subset)
     1.9     apply (auto simp add: finite_Field)
    1.10    done
    1.11  
     2.1 --- a/src/HOL/Transitive_Closure.ML	Sat Nov 09 00:12:25 2002 +0100
     2.2 +++ b/src/HOL/Transitive_Closure.ML	Wed Nov 13 15:24:42 2002 +0100
     2.3 @@ -37,10 +37,10 @@
     2.4  val trancl_converse = thm "trancl_converse";
     2.5  val trancl_converseD = thm "trancl_converseD";
     2.6  val trancl_converseI = thm "trancl_converseI";
     2.7 -val trancl_def = thm "trancl_def";
     2.8  val trancl_induct = thm "trancl_induct";
     2.9  val trancl_insert = thm "trancl_insert";
    2.10  val trancl_into_rtrancl = thm "trancl_into_rtrancl";
    2.11 +val trancl_into_trancl = thm "trancl_into_trancl";
    2.12  val trancl_into_trancl2 = thm "trancl_into_trancl2";
    2.13  val trancl_mono = thm "trancl_mono";
    2.14  val trancl_subset_Sigma = thm "trancl_subset_Sigma";
     3.1 --- a/src/HOL/Transitive_Closure.thy	Sat Nov 09 00:12:25 2002 +0100
     3.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Nov 13 15:24:42 2002 +0100
     3.3 @@ -25,9 +25,13 @@
     3.4      rtrancl_refl [intro!, CPure.intro!, simp]: "(a, a) : r^*"
     3.5      rtrancl_into_rtrancl [CPure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
     3.6  
     3.7 -constdefs
     3.8 +consts
     3.9    trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
    3.10 -  "r^+ ==  r O rtrancl r"
    3.11 +
    3.12 +inductive "r^+"
    3.13 +  intros
    3.14 +    r_into_trancl [intro, CPure.intro]: "(a, b) : r ==> (a, b) : r^+"
    3.15 +    trancl_into_trancl [CPure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
    3.16  
    3.17  syntax
    3.18    "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
    3.19 @@ -213,59 +217,44 @@
    3.20  
    3.21  subsection {* Transitive closure *}
    3.22  
    3.23 -lemma trancl_mono: "p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
    3.24 -  apply (unfold trancl_def)
    3.25 -  apply (blast intro: rtrancl_mono [THEN subsetD])
    3.26 +lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
    3.27 +  apply (simp only: split_tupled_all)
    3.28 +  apply (erule trancl.induct)
    3.29 +  apply (rules dest: subsetD)+
    3.30    done
    3.31  
    3.32 +lemma r_into_trancl': "!!p. p : r ==> p : r^+"
    3.33 +  by (simp only: split_tupled_all) (erule r_into_trancl)
    3.34 +
    3.35  text {*
    3.36    \medskip Conversions between @{text trancl} and @{text rtrancl}.
    3.37  *}
    3.38  
    3.39 -lemma trancl_into_rtrancl: "!!p. p \<in> r^+ ==> p \<in> r^*"
    3.40 -  apply (unfold trancl_def)
    3.41 -  apply (simp only: split_tupled_all)
    3.42 -  apply (erule rel_compEpair)
    3.43 -  apply (assumption | rule rtrancl_into_rtrancl)+
    3.44 -  done
    3.45 +lemma trancl_into_rtrancl: "(a, b) \<in> r^+ ==> (a, b) \<in> r^*"
    3.46 +  by (erule trancl.induct) rules+
    3.47  
    3.48 -lemma r_into_trancl [intro]: "!!p. p \<in> r ==> p \<in> r^+"
    3.49 -  -- {* @{text "r^+"} contains @{text r} *}
    3.50 -  apply (unfold trancl_def)
    3.51 -  apply (simp only: split_tupled_all)
    3.52 -  apply (assumption | rule rel_compI rtrancl_refl)+
    3.53 -  done
    3.54 -
    3.55 -lemma rtrancl_into_trancl1: "(a, b) \<in> r^* ==> (b, c) \<in> r ==> (a, c) \<in> r^+"
    3.56 -  -- {* intro rule by definition: from @{text rtrancl} and @{text r} *}
    3.57 -  by (auto simp add: trancl_def)
    3.58 +lemma rtrancl_into_trancl1: assumes r: "(a, b) \<in> r^*"
    3.59 +  shows "!!c. (b, c) \<in> r ==> (a, c) \<in> r^+" using r
    3.60 +  by induct rules+
    3.61  
    3.62  lemma rtrancl_into_trancl2: "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+"
    3.63    -- {* intro rule from @{text r} and @{text rtrancl} *}
    3.64    apply (erule rtranclE)
    3.65 -   apply (blast intro: r_into_trancl)
    3.66 +   apply rules
    3.67    apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
    3.68     apply (assumption | rule r_into_rtrancl)+
    3.69    done
    3.70  
    3.71 -lemma trancl_induct:
    3.72 -  "[| (a,b) : r^+;
    3.73 -      !!y.  [| (a,y) : r |] ==> P(y);
    3.74 -      !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)
    3.75 -   |] ==> P(b)"
    3.76 +lemma trancl_induct [consumes 1, induct set: trancl]:
    3.77 +  assumes a: "(a,b) : r^+"
    3.78 +  and cases: "!!y. (a, y) : r ==> P y"
    3.79 +    "!!y z. (a,y) : r^+ ==> (y, z) : r ==> P y ==> P z"
    3.80 +  shows "P b"
    3.81    -- {* Nice induction rule for @{text trancl} *}
    3.82  proof -
    3.83 -  assume major: "(a, b) : r^+"
    3.84 -  case rule_context
    3.85 -  show ?thesis
    3.86 -    apply (rule major [unfolded trancl_def, THEN rel_compEpair])
    3.87 -    txt {* by induction on this formula *}
    3.88 -    apply (subgoal_tac "ALL z. (y,z) : r --> P (z)")
    3.89 -     txt {* now solve first subgoal: this formula is sufficient *}
    3.90 -     apply blast
    3.91 -    apply (erule rtrancl_induct)
    3.92 -    apply (blast intro: rtrancl_into_trancl1 prems)+
    3.93 -    done
    3.94 +  from a have "a = a --> P b"
    3.95 +    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
    3.96 +  thus ?thesis by rules
    3.97  qed
    3.98  
    3.99  lemma trancl_trans_induct:
   3.100 @@ -278,44 +267,25 @@
   3.101    assume major: "(x,y) : r^+"
   3.102    case rule_context
   3.103    show ?thesis
   3.104 -    by (blast intro: r_into_trancl major [THEN trancl_induct] prems)
   3.105 +    by (rules intro: r_into_trancl major [THEN trancl_induct] prems)
   3.106  qed
   3.107  
   3.108 -lemma tranclE:
   3.109 -  "[| (a::'a,b) : r^+;
   3.110 -      (a,b) : r ==> P;
   3.111 -      !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P
   3.112 -   |] ==> P"
   3.113 -  -- {* elimination of @{text "r^+"} -- \emph{not} an induction rule *}
   3.114 -proof -
   3.115 -  assume major: "(a::'a,b) : r^+"
   3.116 -  case rule_context
   3.117 -  show ?thesis
   3.118 -    apply (subgoal_tac "(a::'a, b) : r | (EX y. (a,y) : r^+ & (y,b) : r)")
   3.119 -     apply (erule asm_rl disjE exE conjE prems)+
   3.120 -    apply (rule major [unfolded trancl_def, THEN rel_compEpair])
   3.121 -    apply (erule rtranclE)
   3.122 -     apply blast
   3.123 -    apply (blast intro!: rtrancl_into_trancl1)
   3.124 -    done
   3.125 -qed
   3.126 +inductive_cases tranclE: "(a, b) : r^+"
   3.127  
   3.128  lemma trans_trancl: "trans(r^+)"
   3.129    -- {* Transitivity of @{term "r^+"} *}
   3.130 -  -- {* Proved by unfolding since it uses transitivity of @{text rtrancl} *}
   3.131 -  apply (unfold trancl_def)
   3.132 -  apply (rule transI)
   3.133 -  apply (erule rel_compEpair)+
   3.134 -  apply (rule rtrancl_into_rtrancl [THEN rtrancl_trans [THEN rel_compI]])
   3.135 -  apply assumption+
   3.136 -  done
   3.137 +proof (rule transI)
   3.138 +  fix x y z
   3.139 +  assume "(x, y) \<in> r^+"
   3.140 +  assume "(y, z) \<in> r^+"
   3.141 +  thus "(x, z) \<in> r^+" by induct (rules!)+
   3.142 +qed
   3.143  
   3.144  lemmas trancl_trans = trans_trancl [THEN transD, standard]
   3.145  
   3.146 -lemma rtrancl_trancl_trancl: "(x, y) \<in> r^* ==> (y, z) \<in> r^+ ==> (x, z) \<in> r^+"
   3.147 -  apply (unfold trancl_def)
   3.148 -  apply (blast intro: rtrancl_trans)
   3.149 -  done
   3.150 +lemma rtrancl_trancl_trancl: assumes r: "(x, y) \<in> r^*"
   3.151 +  shows "!!z. (y, z) \<in> r^+ ==> (x, z) \<in> r^+" using r
   3.152 +  by induct (rules intro: trancl_trans)+
   3.153  
   3.154  lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+"
   3.155    by (erule transD [OF trans_trancl r_into_trancl])
   3.156 @@ -334,17 +304,21 @@
   3.157      [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   3.158    done
   3.159  
   3.160 -lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"
   3.161 -  apply (unfold trancl_def)
   3.162 -  apply (simp add: rtrancl_converse converse_rel_comp)
   3.163 -  apply (simp add: rtrancl_converse [symmetric] r_comp_rtrancl_eq)
   3.164 +lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x, y) \<in> (r^-1)^+"
   3.165 +  apply (drule converseD)
   3.166 +  apply (erule trancl.induct)
   3.167 +  apply (rules intro: converseI trancl_trans)+
   3.168    done
   3.169  
   3.170 -lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x,y) \<in> (r^-1)^+"
   3.171 -  by (simp add: trancl_converse)
   3.172 +lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
   3.173 +  apply (rule converseI)
   3.174 +  apply (erule trancl.induct)
   3.175 +  apply (rules dest: converseD intro: trancl_trans)+
   3.176 +  done
   3.177  
   3.178 -lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
   3.179 -  by (simp add: trancl_converse)
   3.180 +lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"
   3.181 +  by (fastsimp simp add: split_tupled_all
   3.182 +    intro!: trancl_converseI trancl_converseD)
   3.183  
   3.184  lemma converse_trancl_induct:
   3.185    "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y);
   3.186 @@ -385,8 +359,10 @@
   3.187    done
   3.188  
   3.189  lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"
   3.190 -  apply (unfold trancl_def)
   3.191 -  apply (blast dest!: trancl_subset_Sigma_aux)
   3.192 +  apply (rule subsetI)
   3.193 +  apply (simp only: split_tupled_all)
   3.194 +  apply (erule tranclE)
   3.195 +  apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+
   3.196    done
   3.197  
   3.198  lemma reflcl_trancl [simp]: "(r^+)^= = r^*"
   3.199 @@ -475,7 +451,6 @@
   3.200  declare trancl_into_rtrancl [elim]
   3.201  
   3.202  declare rtranclE [cases set: rtrancl]
   3.203 -declare trancl_induct [induct set: trancl]
   3.204  declare tranclE [cases set: trancl]
   3.205  
   3.206  end