Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
authornipkow
Mon Jan 29 23:02:21 2001 +0100 (2001-01-29)
changeset 1099674e970389def
parent 10995 ef0b521698b7
child 10997 e14029f92770
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
src/HOL/Lex/RegExp2NAe.ML
src/HOL/MicroJava/J/Example.ML
src/HOL/MicroJava/J/WellForm.ML
src/HOL/Transitive_Closure.thy
src/HOL/Transitive_Closure_lemmas.ML
src/HOL/Wellfounded_Relations.ML
     1.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Mon Jan 29 22:25:45 2001 +0100
     1.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Mon Jan 29 23:02:21 2001 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4  
     1.5  Goal "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
     1.6  by (induct_tac "w" 1);
     1.7 - by (asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
     1.8 + by (asm_simp_tac (simpset() addsimps [start_atom,thm"rtrancl_empty"]) 1);
     1.9  by (asm_full_simp_tac (simpset()
    1.10       addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
    1.11  qed "start_fin_in_steps_atom";
     2.1 --- a/src/HOL/MicroJava/J/Example.ML	Mon Jan 29 22:25:45 2001 +0100
     2.2 +++ b/src/HOL/MicroJava/J/Example.ML	Mon Jan 29 23:02:21 2001 +0100
     2.3 @@ -60,7 +60,7 @@
     2.4  by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
     2.5  by (ftac class_tprgD 1);
     2.6  by (auto_tac (claset() addSDs [],simpset()));
     2.7 -bd rtranclD 1;
     2.8 +bd (thm"rtranclD") 1;
     2.9  by Auto_tac;
    2.10  qed "not_class_subcls_class";
    2.11  AddSEs [not_class_subcls_class];
    2.12 @@ -176,7 +176,7 @@
    2.13  by (fold_goals_tac [ExtC_def]);
    2.14  br (wf_foo_Ext RS conjI) 1;
    2.15  by Auto_tac;
    2.16 -bd rtranclD 1;
    2.17 +bd (thm"rtranclD") 1;
    2.18  by Auto_tac;
    2.19  qed "wf_ExtC";
    2.20  
     3.1 --- a/src/HOL/MicroJava/J/WellForm.ML	Mon Jan 29 22:25:45 2001 +0100
     3.2 +++ b/src/HOL/MicroJava/J/WellForm.ML	Mon Jan 29 23:02:21 2001 +0100
     3.3 @@ -27,8 +27,8 @@
     3.4  by(Clarify_tac 1);
     3.5  by( datac class_wf 1 1);
     3.6  by( rewtac wf_cdecl_def);
     3.7 -by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
     3.8 -				  delsimps [reflcl_trancl]) 1);
     3.9 +by(force_tac (claset(), simpset() addsimps [thm"reflcl_trancl" RS sym] 
    3.10 +				  delsimps [thm"reflcl_trancl"]) 1);
    3.11  qed "subcls1_wfD";
    3.12  
    3.13  Goalw [wf_cdecl_def] 
    3.14 @@ -234,7 +234,7 @@
    3.15  "[|field (G,C) fn = Some (fd, fT); G\\<turnstile>D\\<preceq>C C; wf_prog wf_mb G|]==> \
    3.16  \ map_of (fields (G,D)) (fn, fd) = Some fT";
    3.17  by (dtac field_fields 1);
    3.18 -by (dtac rtranclD 1);
    3.19 +by (dtac (thm"rtranclD") 1);
    3.20  by Safe_tac;
    3.21  by (ftac subcls_is_class 1);
    3.22  by (dtac trancl_into_rtrancl 1);
    3.23 @@ -268,7 +268,7 @@
    3.24  Goal "[|G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G|] ==> \
    3.25  \  \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) -->\
    3.26  \ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
    3.27 -by( dtac rtranclD 1);
    3.28 +by( dtac (thm"rtranclD") 1);
    3.29  by( etac disjE 1);
    3.30  by(  Fast_tac 1);
    3.31  by( etac conjE 1);
     4.1 --- a/src/HOL/Transitive_Closure.thy	Mon Jan 29 22:25:45 2001 +0100
     4.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Jan 29 23:02:21 2001 +0100
     4.3 @@ -35,4 +35,52 @@
     4.4  
     4.5  use "Transitive_Closure_lemmas.ML"
     4.6  
     4.7 +
     4.8 +lemma reflcl_trancl[simp]: "(r\<^sup>+)\<^sup>= = r\<^sup>*"
     4.9 +apply safe;
    4.10 +apply (erule trancl_into_rtrancl);
    4.11 +by (blast elim:rtranclE dest:rtrancl_into_trancl1)
    4.12 +
    4.13 +lemma trancl_reflcl[simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*"
    4.14 +apply safe
    4.15 + apply (drule trancl_into_rtrancl)
    4.16 + apply simp;
    4.17 +apply (erule rtranclE)
    4.18 + apply safe
    4.19 + apply(rule r_into_trancl)
    4.20 + apply simp
    4.21 +apply(rule rtrancl_into_trancl1)
    4.22 + apply(erule rtrancl_reflcl[THEN equalityD2, THEN subsetD])
    4.23 +apply fast
    4.24 +done
    4.25 +
    4.26 +lemma trancl_empty[simp]: "{}\<^sup>+ = {}"
    4.27 +by (auto elim:trancl_induct)
    4.28 +
    4.29 +lemma rtrancl_empty[simp]: "{}\<^sup>* = Id"
    4.30 +by(rule subst[OF reflcl_trancl], simp)
    4.31 +
    4.32 +lemma rtranclD: "(a,b) \<in> R\<^sup>* \<Longrightarrow> a=b \<or> a\<noteq>b \<and> (a,b) \<in> R\<^sup>+"
    4.33 +by(force simp add: reflcl_trancl[THEN sym] simp del: reflcl_trancl)
    4.34 +
    4.35 +(* should be merged with the main body of lemmas: *)
    4.36 +
    4.37 +lemma Domain_rtrancl[simp]: "Domain(R\<^sup>*) = UNIV"
    4.38 +by blast
    4.39 +
    4.40 +lemma Range_rtrancl[simp]: "Range(R\<^sup>*) = UNIV"
    4.41 +by blast
    4.42 +
    4.43 +lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R Un S)\<^sup>*"
    4.44 +by(rule rtrancl_Un_rtrancl[THEN subst], fast)
    4.45 +
    4.46 +lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* \<Longrightarrow> x \<in> (R \<union> S)\<^sup>*"
    4.47 +by (blast intro: subsetD[OF rtrancl_Un_subset])
    4.48 +
    4.49 +lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r"
    4.50 +by (unfold Domain_def, blast dest:tranclD)
    4.51 +
    4.52 +lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r"
    4.53 +by (simp add:Range_def trancl_converse[THEN sym])
    4.54 +
    4.55  end
     5.1 --- a/src/HOL/Transitive_Closure_lemmas.ML	Mon Jan 29 22:25:45 2001 +0100
     5.2 +++ b/src/HOL/Transitive_Closure_lemmas.ML	Mon Jan 29 23:02:21 2001 +0100
     5.3 @@ -365,42 +365,3 @@
     5.4  Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
     5.5  by (blast_tac (claset() addSDs [lemma]) 1);
     5.6  qed "trancl_subset_Sigma";
     5.7 -
     5.8 -
     5.9 -Goal "(r^+)^= = r^*";
    5.10 -by Safe_tac;
    5.11 -by  (etac trancl_into_rtrancl 1);
    5.12 -by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
    5.13 -qed "reflcl_trancl";
    5.14 -Addsimps[reflcl_trancl];
    5.15 -
    5.16 -Goal "(r^=)^+ = r^*";
    5.17 -by Safe_tac;
    5.18 -by  (dtac trancl_into_rtrancl 1);
    5.19 -by  (Asm_full_simp_tac 1);
    5.20 -by (etac rtranclE 1);
    5.21 -by  Safe_tac;
    5.22 -by  (rtac r_into_trancl 1);
    5.23 -by  (Simp_tac 1);
    5.24 -by (rtac rtrancl_into_trancl1 1);
    5.25 -by (etac (rtrancl_reflcl RS equalityD2 RS subsetD) 1);
    5.26 -by (Fast_tac 1);
    5.27 -qed "trancl_reflcl";
    5.28 -Addsimps[trancl_reflcl];
    5.29 -
    5.30 -Goal "{}^+ = {}";
    5.31 -by (auto_tac (claset() addEs [trancl_induct], simpset()));
    5.32 -qed "trancl_empty";
    5.33 -Addsimps[trancl_empty];
    5.34 -
    5.35 -Goal "{}^* = Id";
    5.36 -by (rtac (reflcl_trancl RS subst) 1);
    5.37 -by (Simp_tac 1);
    5.38 -qed "rtrancl_empty";
    5.39 -Addsimps[rtrancl_empty];
    5.40 -
    5.41 -Goal "(a,b):R^* ==> a=b | a~=b & (a,b):R^+";
    5.42 -by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
    5.43 -				  delsimps [reflcl_trancl]) 1);
    5.44 -qed "rtranclD";
    5.45 -
     6.1 --- a/src/HOL/Wellfounded_Relations.ML	Mon Jan 29 22:25:45 2001 +0100
     6.2 +++ b/src/HOL/Wellfounded_Relations.ML	Mon Jan 29 23:02:21 2001 +0100
     6.3 @@ -198,8 +198,8 @@
     6.4  (* special case: <= *)
     6.5  
     6.6  Goal "(m, n) : pred_nat^* = (m <= n)";
     6.7 -by (simp_tac (simpset() addsimps [less_eq, reflcl_trancl RS sym] 
     6.8 -                        delsimps [reflcl_trancl]) 1);
     6.9 +by (simp_tac (simpset() addsimps [less_eq, thm"reflcl_trancl" RS sym] 
    6.10 +                        delsimps [thm"reflcl_trancl"]) 1);
    6.11  by (arith_tac 1);
    6.12  qed "le_eq";
    6.13