# HG changeset patch
# User krauss
# Date 1149510178 -7200
# Node ID c40ce2de20209af3a01ccc44c329c3f3b12680b3
# Parent  9afd9b9c47d08c1b20abfc2c9b132851ca3fc041
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
This simplifies some proofs.

diff -r 9afd9b9c47d0 -r c40ce2de2020 src/HOL/Library/While_Combinator.thy
--- 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
 
diff -r 9afd9b9c47d0 -r c40ce2de2020 src/HOL/Subst/Unify.thy
--- 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)
diff -r 9afd9b9c47d0 -r c40ce2de2020 src/HOL/UNITY/Simple/Token.thy
--- 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
diff -r 9afd9b9c47d0 -r c40ce2de2020 src/HOL/UNITY/SubstAx.thy
--- 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)
diff -r 9afd9b9c47d0 -r c40ce2de2020 src/HOL/UNITY/WFair.thy
--- 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)
diff -r 9afd9b9c47d0 -r c40ce2de2020 src/HOL/Wellfounded_Relations.thy
--- 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)"
diff -r 9afd9b9c47d0 -r c40ce2de2020 src/HOL/ZF/Games.thy
--- 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)
diff -r 9afd9b9c47d0 -r c40ce2de2020 src/HOL/ZF/LProd.thy
--- 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
diff -r 9afd9b9c47d0 -r c40ce2de2020 src/HOL/ex/InductiveInvariant_examples.thy
--- 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
diff -r 9afd9b9c47d0 -r c40ce2de2020 src/HOL/ex/Reflected_Presburger.thy
--- 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"