src/HOL/Transitive_Closure.thy
changeset 13704 854501b1e957
parent 12937 0c4fd7529467
child 13726 9550a6f4ed4a
     1.1 --- a/src/HOL/Transitive_Closure.thy	Sat Nov 09 00:12:25 2002 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Nov 13 15:24:42 2002 +0100
     1.3 @@ -25,9 +25,13 @@
     1.4      rtrancl_refl [intro!, CPure.intro!, simp]: "(a, a) : r^*"
     1.5      rtrancl_into_rtrancl [CPure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
     1.6  
     1.7 -constdefs
     1.8 +consts
     1.9    trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
    1.10 -  "r^+ ==  r O rtrancl r"
    1.11 +
    1.12 +inductive "r^+"
    1.13 +  intros
    1.14 +    r_into_trancl [intro, CPure.intro]: "(a, b) : r ==> (a, b) : r^+"
    1.15 +    trancl_into_trancl [CPure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
    1.16  
    1.17  syntax
    1.18    "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
    1.19 @@ -213,59 +217,44 @@
    1.20  
    1.21  subsection {* Transitive closure *}
    1.22  
    1.23 -lemma trancl_mono: "p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
    1.24 -  apply (unfold trancl_def)
    1.25 -  apply (blast intro: rtrancl_mono [THEN subsetD])
    1.26 +lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
    1.27 +  apply (simp only: split_tupled_all)
    1.28 +  apply (erule trancl.induct)
    1.29 +  apply (rules dest: subsetD)+
    1.30    done
    1.31  
    1.32 +lemma r_into_trancl': "!!p. p : r ==> p : r^+"
    1.33 +  by (simp only: split_tupled_all) (erule r_into_trancl)
    1.34 +
    1.35  text {*
    1.36    \medskip Conversions between @{text trancl} and @{text rtrancl}.
    1.37  *}
    1.38  
    1.39 -lemma trancl_into_rtrancl: "!!p. p \<in> r^+ ==> p \<in> r^*"
    1.40 -  apply (unfold trancl_def)
    1.41 -  apply (simp only: split_tupled_all)
    1.42 -  apply (erule rel_compEpair)
    1.43 -  apply (assumption | rule rtrancl_into_rtrancl)+
    1.44 -  done
    1.45 +lemma trancl_into_rtrancl: "(a, b) \<in> r^+ ==> (a, b) \<in> r^*"
    1.46 +  by (erule trancl.induct) rules+
    1.47  
    1.48 -lemma r_into_trancl [intro]: "!!p. p \<in> r ==> p \<in> r^+"
    1.49 -  -- {* @{text "r^+"} contains @{text r} *}
    1.50 -  apply (unfold trancl_def)
    1.51 -  apply (simp only: split_tupled_all)
    1.52 -  apply (assumption | rule rel_compI rtrancl_refl)+
    1.53 -  done
    1.54 -
    1.55 -lemma rtrancl_into_trancl1: "(a, b) \<in> r^* ==> (b, c) \<in> r ==> (a, c) \<in> r^+"
    1.56 -  -- {* intro rule by definition: from @{text rtrancl} and @{text r} *}
    1.57 -  by (auto simp add: trancl_def)
    1.58 +lemma rtrancl_into_trancl1: assumes r: "(a, b) \<in> r^*"
    1.59 +  shows "!!c. (b, c) \<in> r ==> (a, c) \<in> r^+" using r
    1.60 +  by induct rules+
    1.61  
    1.62  lemma rtrancl_into_trancl2: "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+"
    1.63    -- {* intro rule from @{text r} and @{text rtrancl} *}
    1.64    apply (erule rtranclE)
    1.65 -   apply (blast intro: r_into_trancl)
    1.66 +   apply rules
    1.67    apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
    1.68     apply (assumption | rule r_into_rtrancl)+
    1.69    done
    1.70  
    1.71 -lemma trancl_induct:
    1.72 -  "[| (a,b) : r^+;
    1.73 -      !!y.  [| (a,y) : r |] ==> P(y);
    1.74 -      !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)
    1.75 -   |] ==> P(b)"
    1.76 +lemma trancl_induct [consumes 1, induct set: trancl]:
    1.77 +  assumes a: "(a,b) : r^+"
    1.78 +  and cases: "!!y. (a, y) : r ==> P y"
    1.79 +    "!!y z. (a,y) : r^+ ==> (y, z) : r ==> P y ==> P z"
    1.80 +  shows "P b"
    1.81    -- {* Nice induction rule for @{text trancl} *}
    1.82  proof -
    1.83 -  assume major: "(a, b) : r^+"
    1.84 -  case rule_context
    1.85 -  show ?thesis
    1.86 -    apply (rule major [unfolded trancl_def, THEN rel_compEpair])
    1.87 -    txt {* by induction on this formula *}
    1.88 -    apply (subgoal_tac "ALL z. (y,z) : r --> P (z)")
    1.89 -     txt {* now solve first subgoal: this formula is sufficient *}
    1.90 -     apply blast
    1.91 -    apply (erule rtrancl_induct)
    1.92 -    apply (blast intro: rtrancl_into_trancl1 prems)+
    1.93 -    done
    1.94 +  from a have "a = a --> P b"
    1.95 +    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
    1.96 +  thus ?thesis by rules
    1.97  qed
    1.98  
    1.99  lemma trancl_trans_induct:
   1.100 @@ -278,44 +267,25 @@
   1.101    assume major: "(x,y) : r^+"
   1.102    case rule_context
   1.103    show ?thesis
   1.104 -    by (blast intro: r_into_trancl major [THEN trancl_induct] prems)
   1.105 +    by (rules intro: r_into_trancl major [THEN trancl_induct] prems)
   1.106  qed
   1.107  
   1.108 -lemma tranclE:
   1.109 -  "[| (a::'a,b) : r^+;
   1.110 -      (a,b) : r ==> P;
   1.111 -      !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P
   1.112 -   |] ==> P"
   1.113 -  -- {* elimination of @{text "r^+"} -- \emph{not} an induction rule *}
   1.114 -proof -
   1.115 -  assume major: "(a::'a,b) : r^+"
   1.116 -  case rule_context
   1.117 -  show ?thesis
   1.118 -    apply (subgoal_tac "(a::'a, b) : r | (EX y. (a,y) : r^+ & (y,b) : r)")
   1.119 -     apply (erule asm_rl disjE exE conjE prems)+
   1.120 -    apply (rule major [unfolded trancl_def, THEN rel_compEpair])
   1.121 -    apply (erule rtranclE)
   1.122 -     apply blast
   1.123 -    apply (blast intro!: rtrancl_into_trancl1)
   1.124 -    done
   1.125 -qed
   1.126 +inductive_cases tranclE: "(a, b) : r^+"
   1.127  
   1.128  lemma trans_trancl: "trans(r^+)"
   1.129    -- {* Transitivity of @{term "r^+"} *}
   1.130 -  -- {* Proved by unfolding since it uses transitivity of @{text rtrancl} *}
   1.131 -  apply (unfold trancl_def)
   1.132 -  apply (rule transI)
   1.133 -  apply (erule rel_compEpair)+
   1.134 -  apply (rule rtrancl_into_rtrancl [THEN rtrancl_trans [THEN rel_compI]])
   1.135 -  apply assumption+
   1.136 -  done
   1.137 +proof (rule transI)
   1.138 +  fix x y z
   1.139 +  assume "(x, y) \<in> r^+"
   1.140 +  assume "(y, z) \<in> r^+"
   1.141 +  thus "(x, z) \<in> r^+" by induct (rules!)+
   1.142 +qed
   1.143  
   1.144  lemmas trancl_trans = trans_trancl [THEN transD, standard]
   1.145  
   1.146 -lemma rtrancl_trancl_trancl: "(x, y) \<in> r^* ==> (y, z) \<in> r^+ ==> (x, z) \<in> r^+"
   1.147 -  apply (unfold trancl_def)
   1.148 -  apply (blast intro: rtrancl_trans)
   1.149 -  done
   1.150 +lemma rtrancl_trancl_trancl: assumes r: "(x, y) \<in> r^*"
   1.151 +  shows "!!z. (y, z) \<in> r^+ ==> (x, z) \<in> r^+" using r
   1.152 +  by induct (rules intro: trancl_trans)+
   1.153  
   1.154  lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+"
   1.155    by (erule transD [OF trans_trancl r_into_trancl])
   1.156 @@ -334,17 +304,21 @@
   1.157      [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   1.158    done
   1.159  
   1.160 -lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"
   1.161 -  apply (unfold trancl_def)
   1.162 -  apply (simp add: rtrancl_converse converse_rel_comp)
   1.163 -  apply (simp add: rtrancl_converse [symmetric] r_comp_rtrancl_eq)
   1.164 +lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x, y) \<in> (r^-1)^+"
   1.165 +  apply (drule converseD)
   1.166 +  apply (erule trancl.induct)
   1.167 +  apply (rules intro: converseI trancl_trans)+
   1.168    done
   1.169  
   1.170 -lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x,y) \<in> (r^-1)^+"
   1.171 -  by (simp add: trancl_converse)
   1.172 +lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
   1.173 +  apply (rule converseI)
   1.174 +  apply (erule trancl.induct)
   1.175 +  apply (rules dest: converseD intro: trancl_trans)+
   1.176 +  done
   1.177  
   1.178 -lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
   1.179 -  by (simp add: trancl_converse)
   1.180 +lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"
   1.181 +  by (fastsimp simp add: split_tupled_all
   1.182 +    intro!: trancl_converseI trancl_converseD)
   1.183  
   1.184  lemma converse_trancl_induct:
   1.185    "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y);
   1.186 @@ -385,8 +359,10 @@
   1.187    done
   1.188  
   1.189  lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"
   1.190 -  apply (unfold trancl_def)
   1.191 -  apply (blast dest!: trancl_subset_Sigma_aux)
   1.192 +  apply (rule subsetI)
   1.193 +  apply (simp only: split_tupled_all)
   1.194 +  apply (erule tranclE)
   1.195 +  apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+
   1.196    done
   1.197  
   1.198  lemma reflcl_trancl [simp]: "(r^+)^= = r^*"
   1.199 @@ -475,7 +451,6 @@
   1.200  declare trancl_into_rtrancl [elim]
   1.201  
   1.202  declare rtranclE [cases set: rtrancl]
   1.203 -declare trancl_induct [induct set: trancl]
   1.204  declare tranclE [cases set: trancl]
   1.205  
   1.206  end