Made some proofs constructive.
authorberghofe
Mon Jan 21 14:45:00 2002 +0100 (2002-01-21)
changeset 128239d3f5056296b
parent 12822 073116d65bb9
child 12824 cdf586d56b8a
Made some proofs constructive.
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Jan 21 14:43:38 2002 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Jan 21 14:45:00 2002 +0100
     1.3 @@ -22,8 +22,8 @@
     1.4  
     1.5  inductive "r^*"
     1.6    intros
     1.7 -    rtrancl_refl [intro!, simp]: "(a, a) : r^*"
     1.8 -    rtrancl_into_rtrancl: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
     1.9 +    rtrancl_refl [intro!, CPure.intro!, simp]: "(a, a) : r^*"
    1.10 +    rtrancl_into_rtrancl [CPure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
    1.11  
    1.12  constdefs
    1.13    trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
    1.14 @@ -57,14 +57,13 @@
    1.15      apply blast+
    1.16    done
    1.17  
    1.18 -theorem rtrancl_induct [consumes 1]:
    1.19 +theorem rtrancl_induct [consumes 1, induct set: rtrancl]:
    1.20    (assumes a: "(a, b) : r^*"
    1.21      and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z")
    1.22    "P b"
    1.23  proof -
    1.24    from a have "a = a --> P b"
    1.25 -    by (induct "%x y. x = a --> P y" a b rule: rtrancl.induct)
    1.26 -      (rules intro: cases)+
    1.27 +    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
    1.28    thus ?thesis by rules
    1.29  qed
    1.30  
    1.31 @@ -75,11 +74,12 @@
    1.32  
    1.33  lemma trans_rtrancl: "trans(r^*)"
    1.34    -- {* transitivity of transitive closure!! -- by induction *}
    1.35 -  apply (unfold trans_def)
    1.36 -  apply safe
    1.37 -  apply (erule_tac b = z in rtrancl_induct)
    1.38 -   apply (blast intro: rtrancl_into_rtrancl)+
    1.39 -  done
    1.40 +proof (rule transI)
    1.41 +  fix x y z
    1.42 +  assume "(x, y) \<in> r\<^sup>*"
    1.43 +  assume "(y, z) \<in> r\<^sup>*"
    1.44 +  thus "(x, z) \<in> r\<^sup>*" by induct (rules!)+
    1.45 +qed
    1.46  
    1.47  lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
    1.48  
    1.49 @@ -100,7 +100,9 @@
    1.50      done
    1.51  qed
    1.52  
    1.53 -lemmas converse_rtrancl_into_rtrancl = r_into_rtrancl [THEN rtrancl_trans, standard]
    1.54 +lemma converse_rtrancl_into_rtrancl:
    1.55 +  "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
    1.56 +  by (rule rtrancl_trans) rules+
    1.57  
    1.58  text {*
    1.59    \medskip More @{term "r^*"} equations and inclusions.
    1.60 @@ -148,33 +150,31 @@
    1.61    apply (blast intro!: r_into_rtrancl)
    1.62    done
    1.63  
    1.64 -lemma rtrancl_converseD: "(x, y) \<in> (r^-1)^* ==> (y, x) \<in> r^*"
    1.65 -  apply (erule rtrancl_induct)
    1.66 -   apply (rule rtrancl_refl)
    1.67 -  apply (blast intro: rtrancl_trans)
    1.68 -  done
    1.69 +theorem rtrancl_converseD:
    1.70 +  (assumes r: "(x, y) \<in> (r^-1)^*") "(y, x) \<in> r^*"
    1.71 +proof -
    1.72 +  from r show ?thesis
    1.73 +    by induct (rules intro: rtrancl_trans dest!: converseD)+
    1.74 +qed
    1.75  
    1.76 -lemma rtrancl_converseI: "(y, x) \<in> r^* ==> (x, y) \<in> (r^-1)^*"
    1.77 -  apply (erule rtrancl_induct)
    1.78 -   apply (rule rtrancl_refl)
    1.79 -  apply (blast intro: rtrancl_trans)
    1.80 -  done
    1.81 +theorem rtrancl_converseI:
    1.82 +  (assumes r: "(y, x) \<in> r^*") "(x, y) \<in> (r^-1)^*"
    1.83 +proof -
    1.84 +  from r show ?thesis
    1.85 +    by induct (rules intro: rtrancl_trans converseI)+
    1.86 +qed
    1.87  
    1.88  lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
    1.89    by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
    1.90  
    1.91 -lemma converse_rtrancl_induct:
    1.92 -  "[| (a,b) : r^*; P(b);
    1.93 -      !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]
    1.94 -    ==> P(a)"
    1.95 +theorem converse_rtrancl_induct:
    1.96 +  (assumes major: "(a, b) : r^*"
    1.97 +   and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y")
    1.98 +    "P a"
    1.99  proof -
   1.100 -  assume major: "(a,b) : r^*"
   1.101 -  case rule_context
   1.102 +  from rtrancl_converseI [OF major]
   1.103    show ?thesis
   1.104 -    apply (rule major [THEN rtrancl_converseI, THEN rtrancl_induct])
   1.105 -     apply assumption
   1.106 -    apply (blast! dest!: rtrancl_converseD)
   1.107 -  done
   1.108 +    by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
   1.109  qed
   1.110  
   1.111  ML_setup {*
   1.112 @@ -472,7 +472,6 @@
   1.113  
   1.114  declare trancl_into_rtrancl [elim]
   1.115  
   1.116 -declare rtrancl_induct [induct set: rtrancl]
   1.117  declare rtranclE [cases set: rtrancl]
   1.118  declare trancl_induct [induct set: trancl]
   1.119  declare tranclE [cases set: trancl]