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 *}