# HG changeset patch
# User nipkow
# Date 1008595390 -3600
# Node ID 66eb843b1d3519643cfb7cbbce5e1d632d5c4a5d
# Parent  0d8d5bf549b07995a64f22823fdc2e5c694b6e8d
mods due to mor powerful simprocs for 1-point rules (quantifier1).

diff -r 0d8d5bf549b0 -r 66eb843b1d35 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Mon Dec 17 14:21:59 2001 +0100
+++ b/src/HOL/MiniML/W.ML	Mon Dec 17 14:23:10 2001 +0100
@@ -171,17 +171,16 @@
     [free_tv_subst] addsplits [split_option_bind]) 1);
 by (strip_tac 1);
 by (case_tac "v : free_tv (A!nat)" 1);
-by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
 by (dtac free_tv_bound_typ_inst1 1);
-by (simp_tac (simpset() addsimps [o_def]) 1);
+ by (simp_tac (simpset() addsimps [o_def]) 1);
 by (etac exE 1);
-by (rotate_tac 3 1);
 by (Asm_full_simp_tac 1);
 (* case Abs e *)
 by (asm_full_simp_tac (simpset() addsimps
     [free_tv_subst] addsplits [split_option_bind] delsimps all_simps) 1);
 by (strip_tac 1);
-by (rename_tac "S t n1 S1 t1 m v" 1);
+by (rename_tac "S t n1 v" 1);
 by (eres_inst_tac [("x","Suc n")] allE 1);
 by (eres_inst_tac [("x","FVar n # A")] allE 1);
 by (eres_inst_tac [("x","S")] allE 1);
@@ -193,7 +192,7 @@
 (* case App e1 e2 *)
 by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1);
 by (strip_tac 1); 
-by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1);
+by (rename_tac "S t n1 S1 t1 n2 S2 v" 1);
 by (eres_inst_tac [("x","n")] allE 1);
 by (eres_inst_tac [("x","A")] allE 1);
 by (eres_inst_tac [("x","S")] allE 1);
@@ -208,11 +207,11 @@
 by (eres_inst_tac [("x","n2")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
 by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
-by (asm_full_simp_tac (simpset() addsimps [rotate_Some,o_def]) 1);
-by (dtac W_var_geD 1);
-by (dtac W_var_geD 1);
-by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
-by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
+ by (asm_full_simp_tac (simpset() addsimps [rotate_Some,o_def]) 1);
+ by (dtac W_var_geD 1);
+ by (dtac W_var_geD 1);
+ by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
+ by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
     codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD,
     less_le_trans,less_not_refl2,subsetD]
   addEs [UnE] 
@@ -229,14 +228,14 @@
 (* LET e1 e2 *)
 by (simp_tac (simpset() addsplits [split_option_bind] delsimps all_simps) 1);
 by (strip_tac 1); 
-by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
-by (eres_inst_tac [("x","nat")] allE 1);
+by (rename_tac "S1 t1 n2 S2 t2 n3 v" 1);
+by (eres_inst_tac [("x","n")] allE 1);
 by (eres_inst_tac [("x","A")] allE 1);
 by (eres_inst_tac [("x","S1")] allE 1);
 by (eres_inst_tac [("x","t1")] allE 1);
-by (rotate_tac 1 1);
+by (rotate_tac ~1 1);
 by (eres_inst_tac [("x","n2")] allE 1);
-by (rotate_tac 4 1);
+by (rotate_tac ~1 1);
 by (eres_inst_tac [("x","v")] allE 1);
 by (mp_tac 1);
 by (EVERY1 [etac allE,etac allE,etac allE,etac allE,etac allE,eres_inst_tac [("x","v")] allE]);
@@ -299,7 +298,6 @@
 by (ftac new_tv_W 1);
 by (assume_tac 1);
 by (dtac conjunct1 1);
-by (dtac conjunct1 1);
 by (ftac new_tv_subst_scheme_list 1);
 by (rtac new_scheme_list_le 1);
 by (rtac W_var_ge 1);
diff -r 0d8d5bf549b0 -r 66eb843b1d35 src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Mon Dec 17 14:21:59 2001 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy	Mon Dec 17 14:23:10 2001 +0100
@@ -106,43 +106,40 @@
 lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>\<^sub>e t \<longrightarrow> A |\<Turnstile>\<^sub>e t)"
 apply (tactic "split_all_tac 1", rename_tac P e Q)
 apply (rule hoare_ehoare.induct)
+(*18*)
 apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
 apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x :  hoare") *})
 apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : ehoare") *})
 apply (simp_all only: cnvalid1_eq cenvalid_def2)
-apply fast
-apply fast
-apply fast
-apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
-apply fast
-apply fast
-apply fast
-apply fast
-apply fast
-apply fast
-apply (clarsimp del: Meth_elim_cases) (* Call *)
-apply (tactic "smp_tac 1 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
-apply (tactic "smp_tac 2 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
-apply (tactic "smp_tac 4 1", tactic "smp_tac 2 1", fast)
-apply (force del: Impl_elim_cases) (* Meth *)
-defer
-prefer 4 apply blast (*  Conseq *)
-prefer 4 apply blast (* eConseq *)
-apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
-apply blast
-apply blast
-apply blast
-(* Impl *)
+                 apply fast
+                apply fast
+               apply fast
+              apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
+             apply fast
+            apply fast
+           apply fast
+          apply fast
+         apply fast
+        apply fast
+       apply (clarsimp del: Meth_elim_cases) (* Call *)
+      apply (force del: Impl_elim_cases)
+     defer
+     prefer 4 apply blast (*  Conseq *)
+    prefer 4 apply blast (* eConseq *)
+   apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
+   apply blast
+  apply blast
+ apply blast
 apply (rule allI)
 apply (rule_tac x=Z in spec)
 apply (induct_tac "n")
-apply  (clarify intro!: Impl_nvalid_0)
+ apply  (clarify intro!: Impl_nvalid_0)
 apply (clarify  intro!: Impl_nvalid_Suc)
 apply (drule nvalids_SucD)
 apply (simp only: all_simps)
 apply (erule (1) impE)
 apply (drule (2) Impl_sound_lemma)
-apply  blast
+ apply  blast
 apply assumption
 done
 
diff -r 0d8d5bf549b0 -r 66eb843b1d35 src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Mon Dec 17 14:21:59 2001 +0100
+++ b/src/HOL/W0/W.ML	Mon Dec 17 14:23:10 2001 +0100
@@ -157,40 +157,40 @@
 by (asm_full_simp_tac (simpset() addsimps
     [free_tv_subst] addsplits [split_bind]) 1);
 by (strip_tac 1);
-by (rename_tac "s t na sa ta m v" 1);
+by (rename_tac "s t n1 v" 1);
 by (eres_inst_tac [("x","Suc n")] allE 1);
 by (eres_inst_tac [("x","TVar n # a")] allE 1);
 by (eres_inst_tac [("x","s")] allE 1);
 by (eres_inst_tac [("x","t")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
 by (force_tac (claset() addSEs [allE] addIs [cod_app_subst], simpset()) 1);
 (** LEVEL 13 **)
 (* case App e1 e2 *)
 by (simp_tac (simpset() addsplits [split_bind]) 1);
-by (strip_tac 1); 
-by (rename_tac "s t na sa ta nb sb sc tb m v" 1);
+by (strip_tac 1);
+by (rename_tac "s t n1 s1 t1 n2 s3 v" 1);
 by (eres_inst_tac [("x","n")] allE 1);
 by (eres_inst_tac [("x","a")] allE 1);
 by (eres_inst_tac [("x","s")] allE 1);
 by (eres_inst_tac [("x","t")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
-by (eres_inst_tac [("x","na")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
+by (eres_inst_tac [("x","n1")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
 (** LEVEL 23 **)
 (* second case *)
 by (eres_inst_tac [("x","$ s a")] allE 1);
-by (eres_inst_tac [("x","sa")] allE 1);
-by (eres_inst_tac [("x","ta")] allE 1);
-by (eres_inst_tac [("x","nb")] allE 1);
+by (eres_inst_tac [("x","s1")] allE 1);
+by (eres_inst_tac [("x","t1")] allE 1);
+by (eres_inst_tac [("x","n2")] allE 1);
 by (eres_inst_tac [("x","v")] allE 1);
 by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
-by (asm_full_simp_tac (simpset() addsimps [rotate_Ok,o_def]) 1);
-by (dtac W_var_geD 1);
-by (dtac W_var_geD 1);
-by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
+ by (asm_full_simp_tac (simpset() addsimps [rotate_Ok,o_def]) 1);
+ by (dtac W_var_geD 1);
+ by (dtac W_var_geD 1);
+ by ( (ftac less_le_trans 1) THEN (assume_tac 1) );
 (** LEVEL 33 **)
-by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
+ by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
     codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,
     subsetD]
   addEs [UnE] 
diff -r 0d8d5bf549b0 -r 66eb843b1d35 src/HOL/Wellfounded_Relations.ML
--- a/src/HOL/Wellfounded_Relations.ML	Mon Dec 17 14:21:59 2001 +0100
+++ b/src/HOL/Wellfounded_Relations.ML	Mon Dec 17 14:23:10 2001 +0100
@@ -179,7 +179,6 @@
 by (rename_tac "a b" 1);
 by (case_tac "wf(R a)" 1);
  by (eres_inst_tac [("a","b")] wf_induct 1);
- by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
  by (Blast_tac 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "wf_same_fst";
diff -r 0d8d5bf549b0 -r 66eb843b1d35 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Mon Dec 17 14:21:59 2001 +0100
+++ b/src/HOL/simpdata.ML	Mon Dec 17 14:23:10 2001 +0100
@@ -81,6 +81,14 @@
 val iff_allI = allI RS
     prove_goal (the_context()) "!x. P x = Q x ==> (!x. P x) = (!x. Q x)"
                (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
+val iff_exI = allI RS
+    prove_goal (the_context()) "!x. P x = Q x ==> (? x. P x) = (? x. Q x)"
+               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
+
+val all_comm = prove_goal (the_context()) "(!x y. P x y) = (!y x. P x y)"
+               (fn _ => [Blast_tac 1])
+val ex_comm = prove_goal (the_context()) "(? x y. P x y) = (? y x. P x y)"
+               (fn _ => [Blast_tac 1])
 in
 
 (*** make simplification procedures for quantifier elimination ***)
@@ -99,6 +107,7 @@
   (*rules*)
   val iff_reflection = eq_reflection
   val iffI = iffI
+  val iff_trans = trans
   val conjI= conjI
   val conjE= conjE
   val impI = impI
@@ -107,15 +116,18 @@
   val exI  = exI
   val exE  = exE
   val iff_allI = iff_allI
+  val iff_exI = iff_exI
+  val all_comm = all_comm
+  val ex_comm = ex_comm
 end);
 
 end;
 
 local
 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
-    ("EX x. P(x) & Q(x)",HOLogic.boolT)
+    ("EX x. P(x)",HOLogic.boolT)
 val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
-    ("ALL x. P(x) --> Q(x)",HOLogic.boolT)
+    ("ALL x. P(x)",HOLogic.boolT)
 in
 val defEX_regroup = mk_simproc "defined EX" [ex_pattern]
       Quantifier1.rearrange_ex