mods due to mor powerful simprocs for 1-point rules (quantifier1).
--- 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);
--- 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
--- 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]
--- 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";
--- 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