Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
This simplifies some proofs.
--- a/src/HOL/Library/While_Combinator.thy Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/Library/While_Combinator.thy Mon Jun 05 14:22:58 2006 +0200
@@ -130,7 +130,7 @@
apply (blast dest: monoD)
apply (fastsimp intro!: lfp_lowerbound)
apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
-apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
+apply (clarsimp simp add: finite_psubset_def order_less_le)
apply (blast intro!: finite_Diff dest: monoD)
done
--- a/src/HOL/Subst/Unify.thy Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/Subst/Unify.thy Mon Jun 05 14:22:58 2006 +0200
@@ -85,10 +85,7 @@
text{*The non-nested TC (terminiation condition).*}
recdef_tc unify_tc1: unify (1)
-apply (simp add: unifyRel_def wf_lex_prod wf_finite_psubset, safe)
-apply (simp add: finite_psubset_def finite_vars_of lex_prod_def inv_image_def)
-apply (rule monotone_vars_of [THEN subset_iff_psubset_eq [THEN iffD1]])
-done
+ by (auto simp: unifyRel_def finite_psubset_def finite_vars_of)
text{*Termination proof.*}
@@ -104,7 +101,7 @@
lemma Rassoc:
"((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) \<in> unifyRel ==>
((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \<in> unifyRel"
-by (simp add: less_eq inv_image_def add_assoc Un_assoc
+by (simp add: less_eq add_assoc Un_assoc
unifyRel_def lex_prod_def)
@@ -117,15 +114,14 @@
apply (case_tac "Var x = M", clarify, simp)
apply (case_tac "x \<in> (vars_of N1 Un vars_of N2)")
txt{*uterm_less case*}
-apply (simp add: less_eq unifyRel_def lex_prod_def inv_image_def)
+apply (simp add: less_eq unifyRel_def lex_prod_def)
apply blast
txt{*@{text finite_psubset} case*}
-apply (simp add: unifyRel_def lex_prod_def inv_image_def)
+apply (simp add: unifyRel_def lex_prod_def)
apply (simp add: finite_psubset_def finite_vars_of psubset_def)
apply blast
txt{*Final case, also @{text finite_psubset}*}
-apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def
- inv_image_def)
+apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def)
apply (cut_tac s = "[(x,M)]" and v = x and t = N2 in Var_elim)
apply (cut_tac [3] s = "[(x,M)]" and v = x and t = N1 in Var_elim)
apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq)
@@ -156,7 +152,7 @@
apply (rule_tac u = M1 and v = M2 in unify_induct0)
apply (simp_all (no_asm_simp) add: var_elimR unify_simps0)
txt{*Const-Const case*}
- apply (simp add: unifyRel_def lex_prod_def inv_image_def less_eq)
+ apply (simp add: unifyRel_def lex_prod_def less_eq)
txt{*Comb-Comb case*}
apply (simp (no_asm_simp) split add: option.split)
apply (intro strip)
--- a/src/HOL/UNITY/Simple/Token.thy Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/UNITY/Simple/Token.thy Mon Jun 05 14:22:58 2006 +0200
@@ -79,7 +79,7 @@
lemma (in Token) nodeOrder_eq:
"[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
-apply (unfold nodeOrder_def next_def measure_def inv_image_def)
+apply (unfold nodeOrder_def next_def)
apply (auto simp add: mod_Suc mod_geq)
apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
done
--- a/src/HOL/UNITY/SubstAx.thy Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/UNITY/SubstAx.thy Mon Jun 05 14:22:58 2006 +0200
@@ -363,7 +363,7 @@
==> F \<in> A LeadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
apply (rule_tac f = f and f1 = "%k. l - k"
in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
-apply (simp add: inv_image_def Image_singleton, clarify)
+apply (simp add: Image_singleton, clarify)
apply (case_tac "m<l")
apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
apply (blast intro: not_leE subset_imp_LeadsTo)
--- a/src/HOL/UNITY/WFair.thy Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/UNITY/WFair.thy Mon Jun 05 14:22:58 2006 +0200
@@ -492,7 +492,7 @@
==> F \<in> A leadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
apply (rule_tac f = f and f1 = "%k. l - k"
in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct])
-apply (simp (no_asm) add: inv_image_def Image_singleton)
+apply (simp (no_asm) add:Image_singleton)
apply clarify
apply (case_tac "m<l")
apply (blast intro: leadsTo_weaken_R diff_less_mono2)
--- a/src/HOL/Wellfounded_Relations.thy Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/Wellfounded_Relations.thy Mon Jun 05 14:22:58 2006 +0200
@@ -70,11 +70,13 @@
apply blast
done
+lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
+ by (auto simp:inv_image_def)
subsubsection{*Finally, All Measures are Wellfounded.*}
lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
-by (auto simp:measure_def inv_image_def)
+ by (simp add:measure_def)
lemma wf_measure [iff]: "wf (measure f)"
apply (unfold measure_def)
@@ -118,6 +120,10 @@
apply (drule spec, erule mp, blast)
done
+lemma in_lex_prod[simp]:
+ "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
+ by (auto simp:lex_prod_def)
+
text{*Transitivity of WF combinators.*}
lemma trans_lex_prod [intro!]:
"[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
--- a/src/HOL/ZF/Games.thy Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/ZF/Games.thy Mon Jun 05 14:22:58 2006 +0200
@@ -323,7 +323,7 @@
have option_of: "option_of = inv_image is_option_of Rep_game"
apply (rule set_ext)
apply (case_tac "x")
- by (simp add: inv_image_def option_to_is_option_of)
+ by (simp add: option_to_is_option_of)
show ?thesis
apply (simp add: option_of)
apply (auto intro: wf_inv_image wf_is_option_of)
--- a/src/HOL/ZF/LProd.thy Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/ZF/LProd.thy Mon Jun 05 14:22:58 2006 +0200
@@ -89,7 +89,7 @@
shows "wf (lprod R)"
proof -
have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) multiset_of"
- by (auto simp add: inv_image_def lprod_implies_mult trans_trancl)
+ by (auto simp add: lprod_implies_mult trans_trancl)
note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="multiset_of",
OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
@@ -122,7 +122,7 @@
assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
proof -
have "gprod_2_1 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
- by (auto simp add: inv_image_def gprod_2_1_def lprod_2_1 lprod_2_2)
+ by (auto simp add: gprod_2_1_def lprod_2_1 lprod_2_2)
with wfR show ?thesis
by (rule_tac wf_subset, auto)
qed
@@ -131,7 +131,7 @@
assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
proof -
have "gprod_2_2 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
- by (auto simp add: inv_image_def gprod_2_2_def lprod_2_3 lprod_2_4)
+ by (auto simp add: gprod_2_2_def lprod_2_3 lprod_2_4)
with wfR show ?thesis
by (rule_tac wf_subset, auto)
qed
--- a/src/HOL/ex/InductiveInvariant_examples.thy Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/ex/InductiveInvariant_examples.thy Mon Jun 05 14:22:58 2006 +0200
@@ -105,7 +105,7 @@
lemma ninety_one_inv: "n < ninety_one n + 11"
apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
apply force
-apply (auto simp add: indinv_def inv_image_def)
+apply (auto simp add: indinv_def)
apply (frule_tac x="x+11" in spec)
apply (frule_tac x="f (x + 11)" in spec)
by arith
@@ -125,6 +125,6 @@
then x - 10
else ninety_one (ninety_one (x+11)))"
by (subst ninety_one.simps,
- simp add: ninety_one_tc inv_image_def)
+ simp add: ninety_one_tc)
end
--- a/src/HOL/ex/Reflected_Presburger.thy Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Mon Jun 05 14:22:58 2006 +0200
@@ -834,12 +834,12 @@
{
assume nlini: "linearize i = None"
from nlini have "linearize (Add i j) = None"
- by (simp add: inv_image_def) then have ?thesis using prems by auto}
+ by simp then have ?thesis using prems by auto}
moreover
{ assume nlinj: "linearize j = None"
and lini: "\<exists> li. linearize i = Some li"
from nlinj lini have "linearize (Add i j) = None"
- by (simp add: inv_image_def, auto) with prems have ?thesis by auto}
+ by auto with prems have ?thesis by auto}
moreover
{ assume lini: "\<exists>li. linearize i = Some li"
and linj: "\<exists>lj. linearize j = Some lj"