# HG changeset patch
# User nipkow
# Date 980805741 -3600
# Node ID 74e970389def016e3b045fc35d9ffd902544d3ea
# Parent  ef0b521698b7c6f0e0497e5b4c7e6593b665378d
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy

diff -r ef0b521698b7 -r 74e970389def src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Mon Jan 29 22:25:45 2001 +0100
+++ b/src/HOL/Lex/RegExp2NAe.ML	Mon Jan 29 23:02:21 2001 +0100
@@ -38,7 +38,7 @@
 
 Goal "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
 by (induct_tac "w" 1);
- by (asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
+ by (asm_simp_tac (simpset() addsimps [start_atom,thm"rtrancl_empty"]) 1);
 by (asm_full_simp_tac (simpset()
      addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
 qed "start_fin_in_steps_atom";
diff -r ef0b521698b7 -r 74e970389def src/HOL/MicroJava/J/Example.ML
--- a/src/HOL/MicroJava/J/Example.ML	Mon Jan 29 22:25:45 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.ML	Mon Jan 29 23:02:21 2001 +0100
@@ -60,7 +60,7 @@
 by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
 by (ftac class_tprgD 1);
 by (auto_tac (claset() addSDs [],simpset()));
-bd rtranclD 1;
+bd (thm"rtranclD") 1;
 by Auto_tac;
 qed "not_class_subcls_class";
 AddSEs [not_class_subcls_class];
@@ -176,7 +176,7 @@
 by (fold_goals_tac [ExtC_def]);
 br (wf_foo_Ext RS conjI) 1;
 by Auto_tac;
-bd rtranclD 1;
+bd (thm"rtranclD") 1;
 by Auto_tac;
 qed "wf_ExtC";
 
diff -r ef0b521698b7 -r 74e970389def src/HOL/MicroJava/J/WellForm.ML
--- a/src/HOL/MicroJava/J/WellForm.ML	Mon Jan 29 22:25:45 2001 +0100
+++ b/src/HOL/MicroJava/J/WellForm.ML	Mon Jan 29 23:02:21 2001 +0100
@@ -27,8 +27,8 @@
 by(Clarify_tac 1);
 by( datac class_wf 1 1);
 by( rewtac wf_cdecl_def);
-by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
-				  delsimps [reflcl_trancl]) 1);
+by(force_tac (claset(), simpset() addsimps [thm"reflcl_trancl" RS sym] 
+				  delsimps [thm"reflcl_trancl"]) 1);
 qed "subcls1_wfD";
 
 Goalw [wf_cdecl_def] 
@@ -234,7 +234,7 @@
 "[|field (G,C) fn = Some (fd, fT); G\\<turnstile>D\\<preceq>C C; wf_prog wf_mb G|]==> \
 \ map_of (fields (G,D)) (fn, fd) = Some fT";
 by (dtac field_fields 1);
-by (dtac rtranclD 1);
+by (dtac (thm"rtranclD") 1);
 by Safe_tac;
 by (ftac subcls_is_class 1);
 by (dtac trancl_into_rtrancl 1);
@@ -268,7 +268,7 @@
 Goal "[|G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G|] ==> \
 \  \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) -->\
 \ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
-by( dtac rtranclD 1);
+by( dtac (thm"rtranclD") 1);
 by( etac disjE 1);
 by(  Fast_tac 1);
 by( etac conjE 1);
diff -r ef0b521698b7 -r 74e970389def src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Jan 29 22:25:45 2001 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Jan 29 23:02:21 2001 +0100
@@ -35,4 +35,52 @@
 
 use "Transitive_Closure_lemmas.ML"
 
+
+lemma reflcl_trancl[simp]: "(r\<^sup>+)\<^sup>= = r\<^sup>*"
+apply safe;
+apply (erule trancl_into_rtrancl);
+by (blast elim:rtranclE dest:rtrancl_into_trancl1)
+
+lemma trancl_reflcl[simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*"
+apply safe
+ apply (drule trancl_into_rtrancl)
+ apply simp;
+apply (erule rtranclE)
+ apply safe
+ apply(rule r_into_trancl)
+ apply simp
+apply(rule rtrancl_into_trancl1)
+ apply(erule rtrancl_reflcl[THEN equalityD2, THEN subsetD])
+apply fast
+done
+
+lemma trancl_empty[simp]: "{}\<^sup>+ = {}"
+by (auto elim:trancl_induct)
+
+lemma rtrancl_empty[simp]: "{}\<^sup>* = Id"
+by(rule subst[OF reflcl_trancl], simp)
+
+lemma rtranclD: "(a,b) \<in> R\<^sup>* \<Longrightarrow> a=b \<or> a\<noteq>b \<and> (a,b) \<in> R\<^sup>+"
+by(force simp add: reflcl_trancl[THEN sym] simp del: reflcl_trancl)
+
+(* should be merged with the main body of lemmas: *)
+
+lemma Domain_rtrancl[simp]: "Domain(R\<^sup>*) = UNIV"
+by blast
+
+lemma Range_rtrancl[simp]: "Range(R\<^sup>*) = UNIV"
+by blast
+
+lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R Un S)\<^sup>*"
+by(rule rtrancl_Un_rtrancl[THEN subst], fast)
+
+lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* \<Longrightarrow> x \<in> (R \<union> S)\<^sup>*"
+by (blast intro: subsetD[OF rtrancl_Un_subset])
+
+lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r"
+by (unfold Domain_def, blast dest:tranclD)
+
+lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r"
+by (simp add:Range_def trancl_converse[THEN sym])
+
 end
diff -r ef0b521698b7 -r 74e970389def src/HOL/Transitive_Closure_lemmas.ML
--- a/src/HOL/Transitive_Closure_lemmas.ML	Mon Jan 29 22:25:45 2001 +0100
+++ b/src/HOL/Transitive_Closure_lemmas.ML	Mon Jan 29 23:02:21 2001 +0100
@@ -365,42 +365,3 @@
 Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
 by (blast_tac (claset() addSDs [lemma]) 1);
 qed "trancl_subset_Sigma";
-
-
-Goal "(r^+)^= = r^*";
-by Safe_tac;
-by  (etac trancl_into_rtrancl 1);
-by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
-qed "reflcl_trancl";
-Addsimps[reflcl_trancl];
-
-Goal "(r^=)^+ = r^*";
-by Safe_tac;
-by  (dtac trancl_into_rtrancl 1);
-by  (Asm_full_simp_tac 1);
-by (etac rtranclE 1);
-by  Safe_tac;
-by  (rtac r_into_trancl 1);
-by  (Simp_tac 1);
-by (rtac rtrancl_into_trancl1 1);
-by (etac (rtrancl_reflcl RS equalityD2 RS subsetD) 1);
-by (Fast_tac 1);
-qed "trancl_reflcl";
-Addsimps[trancl_reflcl];
-
-Goal "{}^+ = {}";
-by (auto_tac (claset() addEs [trancl_induct], simpset()));
-qed "trancl_empty";
-Addsimps[trancl_empty];
-
-Goal "{}^* = Id";
-by (rtac (reflcl_trancl RS subst) 1);
-by (Simp_tac 1);
-qed "rtrancl_empty";
-Addsimps[rtrancl_empty];
-
-Goal "(a,b):R^* ==> a=b | a~=b & (a,b):R^+";
-by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
-				  delsimps [reflcl_trancl]) 1);
-qed "rtranclD";
-
diff -r ef0b521698b7 -r 74e970389def src/HOL/Wellfounded_Relations.ML
--- a/src/HOL/Wellfounded_Relations.ML	Mon Jan 29 22:25:45 2001 +0100
+++ b/src/HOL/Wellfounded_Relations.ML	Mon Jan 29 23:02:21 2001 +0100
@@ -198,8 +198,8 @@
 (* special case: <= *)
 
 Goal "(m, n) : pred_nat^* = (m <= n)";
-by (simp_tac (simpset() addsimps [less_eq, reflcl_trancl RS sym] 
-                        delsimps [reflcl_trancl]) 1);
+by (simp_tac (simpset() addsimps [less_eq, thm"reflcl_trancl" RS sym] 
+                        delsimps [thm"reflcl_trancl"]) 1);
 by (arith_tac 1);
 qed "le_eq";