Transitive closure is now defined via "inductive".
authorberghofe
Tue May 22 15:12:11 2001 +0200 (2001-05-22)
changeset 11327cd2c27a23df1
parent 11326 680ebd093cfe
child 11328 956ec01b46e0
Transitive closure is now defined via "inductive".
src/HOL/Transitive_Closure.thy
src/HOL/Transitive_Closure_lemmas.ML
     1.1 --- a/src/HOL/Transitive_Closure.thy	Tue May 22 15:11:43 2001 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Tue May 22 15:12:11 2001 +0200
     1.3 @@ -13,13 +13,18 @@
     1.4  to be atomic.
     1.5  *)
     1.6  
     1.7 -theory Transitive_Closure = Lfp + Relation
     1.8 +theory Transitive_Closure = Inductive
     1.9  files ("Transitive_Closure_lemmas.ML"):
    1.10  
    1.11 +consts
    1.12 +  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    1.13 +
    1.14 +inductive "r^*"
    1.15 +intros
    1.16 +  rtrancl_refl [intro!, simp]: "(a, a) : r^*"
    1.17 +  rtrancl_into_rtrancl:        "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*"
    1.18 +
    1.19  constdefs
    1.20 -  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    1.21 -  "r^* == lfp (%s. Id Un (r O s))"
    1.22 -
    1.23    trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
    1.24    "r^+ ==  r O rtrancl r"
    1.25  
    1.26 @@ -89,5 +94,11 @@
    1.27  	"x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
    1.28   apply (auto)
    1.29   by (erule rev_mp, erule rtrancl_induct, auto)
    1.30 - 
    1.31 +
    1.32 +
    1.33 +declare rtrancl_induct [induct set: rtrancl]
    1.34 +declare rtranclE [cases set: rtrancl]
    1.35 +declare trancl_induct [induct set: trancl]
    1.36 +declare tranclE [cases set: trancl]
    1.37 +
    1.38  end
     2.1 --- a/src/HOL/Transitive_Closure_lemmas.ML	Tue May 22 15:11:43 2001 +0200
     2.2 +++ b/src/HOL/Transitive_Closure_lemmas.ML	Tue May 22 15:12:11 2001 +0200
     2.3 @@ -6,7 +6,8 @@
     2.4  Theorems about the transitive closure of a relation
     2.5  *)
     2.6  
     2.7 -val rtrancl_def = thm "rtrancl_def";
     2.8 +val rtrancl_refl = thm "rtrancl_refl";
     2.9 +val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
    2.10  val trancl_def = thm "trancl_def";
    2.11  
    2.12  
    2.13 @@ -14,29 +15,6 @@
    2.14  
    2.15  section "^*";
    2.16  
    2.17 -Goal "mono(%s. Id Un (r O s))";
    2.18 -by (rtac monoI 1);
    2.19 -by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
    2.20 -qed "rtrancl_fun_mono";
    2.21 -
    2.22 -bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_unfold));
    2.23 -
    2.24 -(*Reflexivity of rtrancl*)
    2.25 -Goal "(a,a) : r^*";
    2.26 -by (stac rtrancl_unfold 1);
    2.27 -by (Blast_tac 1);
    2.28 -qed "rtrancl_refl";
    2.29 -
    2.30 -Addsimps [rtrancl_refl];
    2.31 -AddSIs   [rtrancl_refl];
    2.32 -
    2.33 -
    2.34 -(*Closure under composition with r*)
    2.35 -Goal "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
    2.36 -by (stac rtrancl_unfold 1);
    2.37 -by (Blast_tac 1);
    2.38 -qed "rtrancl_into_rtrancl";
    2.39 -
    2.40  (*rtrancl of r contains r*)
    2.41  Goal "!!p. p : r ==> p : r^*";
    2.42  by (split_all_tac 1);
    2.43 @@ -46,35 +24,23 @@
    2.44  AddIs [r_into_rtrancl];
    2.45  
    2.46  (*monotonicity of rtrancl*)
    2.47 -Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
    2.48 -by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
    2.49 +Goal "r <= s ==> r^* <= s^*";
    2.50 +by (rtac subsetI 1);
    2.51 +by (split_all_tac 1);
    2.52 +by (etac (thm "rtrancl.induct") 1);
    2.53 +by (rtac rtrancl_into_rtrancl 2);
    2.54 +by (ALLGOALS Blast_tac);
    2.55  qed "rtrancl_mono";
    2.56  
    2.57 -(** standard induction rule **)
    2.58 -
    2.59 -val major::prems = Goal 
    2.60 -  "[| (a,b) : r^*; \
    2.61 -\     !!x. P(x,x); \
    2.62 -\     !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |]  ==>  P(x,z) |] \
    2.63 -\  ==>  P(a,b)";
    2.64 -by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_lfp_induct) 1);
    2.65 -by (blast_tac (claset() addIs prems) 1);
    2.66 -qed "rtrancl_full_induct";
    2.67 -
    2.68  (*nice induction rule*)
    2.69  val major::prems = Goal
    2.70      "[| (a::'a,b) : r^*;    \
    2.71  \       P(a); \
    2.72  \       !!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
    2.73  \     ==> P(b)";
    2.74 -(*by induction on this formula*)
    2.75 -by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
    2.76 -(*now solve first subgoal: this formula is sufficient*)
    2.77 -by (Blast_tac 1);
    2.78 -(*now do the induction*)
    2.79 -by (resolve_tac [major RS rtrancl_full_induct] 1);
    2.80 -by (blast_tac (claset() addIs prems) 1);
    2.81 -by (blast_tac (claset() addIs prems) 1);
    2.82 +by (rtac (read_instantiate [("P","%x y. x = a --> P y")]
    2.83 +  (major RS thm "rtrancl.induct") RS mp) 1);
    2.84 +by (ALLGOALS (blast_tac (claset() addIs prems)));
    2.85  qed "rtrancl_induct";
    2.86  
    2.87  bind_thm ("rtrancl_induct2", split_rule