src/HOL/Transitive_Closure.thy
 changeset 18372 2bffdf62fe7f parent 17876 b9c92f384109 child 19228 30fce6da8cbe
```     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Dec 08 20:15:41 2005 +0100
1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Dec 08 20:15:50 2005 +0100
1.3 @@ -81,7 +81,7 @@
1.4  lemmas rtrancl_induct2 =
1.5    rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
1.6                   consumes 1, case_names refl step]
1.7 -
1.8 +
1.9  lemma trans_rtrancl: "trans(r^*)"
1.10    -- {* transitivity of transitive closure!! -- by induction *}
1.11  proof (rule transI)
1.12 @@ -94,21 +94,17 @@
1.13  lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
1.14
1.15  lemma rtranclE:
1.16 -  "[| (a::'a,b) : r^*;  (a = b) ==> P;
1.17 -      !!y.[| (a,y) : r^*; (y,b) : r |] ==> P
1.18 -   |] ==> P"
1.19 +  assumes major: "(a::'a,b) : r^*"
1.20 +    and cases: "(a = b) ==> P"
1.21 +      "!!y. [| (a,y) : r^*; (y,b) : r |] ==> P"
1.22 +  shows P
1.23    -- {* elimination of @{text rtrancl} -- by induction on a special formula *}
1.24 -proof -
1.25 -  assume major: "(a::'a,b) : r^*"
1.26 -  case rule_context
1.27 -  show ?thesis
1.28 -    apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
1.29 -     apply (rule_tac [2] major [THEN rtrancl_induct])
1.30 -      prefer 2 apply (blast!)
1.31 -      prefer 2 apply (blast!)
1.32 -    apply (erule asm_rl exE disjE conjE prems)+
1.33 -    done
1.34 -qed
1.35 +  apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
1.36 +   apply (rule_tac [2] major [THEN rtrancl_induct])
1.37 +    prefer 2 apply blast
1.38 +   prefer 2 apply blast
1.39 +  apply (erule asm_rl exE disjE conjE cases)+
1.40 +  done
1.41
1.42  lemma converse_rtrancl_into_rtrancl:
1.43    "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
1.44 @@ -187,21 +183,16 @@
1.45                   consumes 1, case_names refl step]
1.46
1.47  lemma converse_rtranclE:
1.48 -  "[| (x,z):r^*;
1.49 -      x=z ==> P;
1.50 -      !!y. [| (x,y):r; (y,z):r^* |] ==> P
1.51 -   |] ==> P"
1.52 -proof -
1.53 -  assume major: "(x,z):r^*"
1.54 -  case rule_context
1.55 -  show ?thesis
1.56 -    apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
1.57 -     apply (rule_tac [2] major [THEN converse_rtrancl_induct])
1.58 -      prefer 2 apply iprover
1.59 -     prefer 2 apply iprover
1.60 -    apply (erule asm_rl exE disjE conjE prems)+
1.61 -    done
1.62 -qed
1.63 +  assumes major: "(x,z):r^*"
1.64 +    and cases: "x=z ==> P"
1.65 +      "!!y. [| (x,y):r; (y,z):r^* |] ==> P"
1.66 +  shows P
1.67 +  apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
1.68 +   apply (rule_tac [2] major [THEN converse_rtrancl_induct])
1.69 +    prefer 2 apply iprover
1.70 +   prefer 2 apply iprover
1.71 +  apply (erule asm_rl exE disjE conjE cases)+
1.72 +  done
1.73
1.74  ML_setup {*
1.75    bind_thm ("converse_rtranclE2", split_rule
1.76 @@ -258,17 +249,12 @@
1.77  qed
1.78
1.79  lemma trancl_trans_induct:
1.80 -  "[| (x,y) : r^+;
1.81 -      !!x y. (x,y) : r ==> P x y;
1.82 -      !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z
1.83 -   |] ==> P x y"
1.84 +  assumes major: "(x,y) : r^+"
1.85 +    and cases: "!!x y. (x,y) : r ==> P x y"
1.86 +      "!!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z"
1.87 +  shows "P x y"
1.88    -- {* Another induction rule for trancl, incorporating transitivity *}
1.89 -proof -
1.90 -  assume major: "(x,y) : r^+"
1.91 -  case rule_context
1.92 -  show ?thesis
1.93 -    by (iprover intro: r_into_trancl major [THEN trancl_induct] prems)
1.94 -qed
1.95 +  by (iprover intro: r_into_trancl major [THEN trancl_induct] cases)
1.96
1.97  inductive_cases tranclE: "(a, b) : r^+"
1.98
1.99 @@ -279,9 +265,9 @@
1.100    -- {* Transitivity of @{term "r^+"} *}
1.101  proof (rule transI)
1.102    fix x y z
1.103 -  assume "(x, y) \<in> r^+"
1.104 +  assume xy: "(x, y) \<in> r^+"
1.105    assume "(y, z) \<in> r^+"
1.106 -  thus "(x, z) \<in> r^+" by induct (iprover!)+
1.107 +  thus "(x, z) \<in> r^+" by induct (insert xy, iprover)+
1.108  qed
1.109
1.110  lemmas trancl_trans = trans_trancl [THEN transD, standard]
1.111 @@ -323,19 +309,15 @@
1.112      intro!: trancl_converseI trancl_converseD)
1.113
1.114  lemma converse_trancl_induct:
1.115 -  "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y);
1.116 -      !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]
1.117 -    ==> P(a)"
1.118 -proof -
1.119 -  assume major: "(a,b) : r^+"
1.120 -  case rule_context
1.121 -  show ?thesis
1.122 -    apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]])
1.123 -     apply (rule prems)
1.124 -     apply (erule converseD)
1.125 -    apply (blast intro: prems dest!: trancl_converseD)
1.126 -    done
1.127 -qed
1.128 +  assumes major: "(a,b) : r^+"
1.129 +    and cases: "!!y. (y,b) : r ==> P(y)"
1.130 +      "!!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y)"
1.131 +  shows "P a"
1.132 +  apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]])
1.133 +   apply (rule cases)
1.134 +   apply (erule converseD)
1.135 +  apply (blast intro: prems dest!: trancl_converseD)
1.136 +  done
1.137
1.138  lemma tranclD: "(x, y) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> R^*"
1.139    apply (erule converse_trancl_induct, auto)
1.140 @@ -343,15 +325,14 @@
1.141    done
1.142
1.143  lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
1.144 -by(blast elim: tranclE dest: trancl_into_rtrancl)
1.145 +  by (blast elim: tranclE dest: trancl_into_rtrancl)
1.146
1.147  lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
1.148    by (blast dest: r_into_trancl)
1.149
1.150  lemma trancl_subset_Sigma_aux:
1.151      "(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A"
1.152 -  apply (erule rtrancl_induct, auto)
1.153 -  done
1.154 +  by (induct rule: rtrancl_induct) auto
1.155
1.156  lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"
1.157    apply (rule subsetI)
1.158 @@ -477,16 +458,16 @@
1.159      val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
1.160      val rtrancl_trans = thm "rtrancl_trans";
1.161
1.162 -  fun decomp (Trueprop \$ t) =
1.163 -    let fun dec (Const ("op :", _) \$ (Const ("Pair", _) \$ a \$ b) \$ rel ) =
1.164 -	let fun decr (Const ("Transitive_Closure.rtrancl", _ ) \$ r) = (r,"r*")
1.165 -	      | decr (Const ("Transitive_Closure.trancl", _ ) \$ r)  = (r,"r+")
1.166 -	      | decr r = (r,"r");
1.167 -	    val (rel,r) = decr rel;
1.168 -	in SOME (a,b,rel,r) end
1.169 -      | dec _ =  NONE
1.170 +  fun decomp (Trueprop \$ t) =
1.171 +    let fun dec (Const ("op :", _) \$ (Const ("Pair", _) \$ a \$ b) \$ rel ) =
1.172 +        let fun decr (Const ("Transitive_Closure.rtrancl", _ ) \$ r) = (r,"r*")
1.173 +              | decr (Const ("Transitive_Closure.trancl", _ ) \$ r)  = (r,"r+")
1.174 +              | decr r = (r,"r");
1.175 +            val (rel,r) = decr rel;
1.176 +        in SOME (a,b,rel,r) end
1.177 +      | dec _ =  NONE
1.178      in dec t end;
1.179 -
1.180 +
1.181    end); (* struct *)
1.182
1.183  change_simpset (fn ss => ss
1.184 @@ -499,7 +480,7 @@
1.185
1.186  method_setup trancl =
1.187    {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trancl_tac)) *}
1.188 -  {* simple transitivity reasoner *}
1.189 +  {* simple transitivity reasoner *}
1.190  method_setup rtrancl =
1.191    {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (rtrancl_tac)) *}
1.192    {* simple transitivity reasoner *}
```