Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
authorkrauss
Mon Jun 05 14:22:58 2006 +0200 (2006-06-05)
changeset 19769c40ce2de2020
parent 19768 9afd9b9c47d0
child 19770 be5c23ebe1eb
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
This simplifies some proofs.
src/HOL/Library/While_Combinator.thy
src/HOL/Subst/Unify.thy
src/HOL/UNITY/Simple/Token.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/WFair.thy
src/HOL/Wellfounded_Relations.thy
src/HOL/ZF/Games.thy
src/HOL/ZF/LProd.thy
src/HOL/ex/InductiveInvariant_examples.thy
src/HOL/ex/Reflected_Presburger.thy
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Sun Jun 04 10:52:47 2006 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Mon Jun 05 14:22:58 2006 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4    apply (blast dest: monoD)
     1.5   apply (fastsimp intro!: lfp_lowerbound)
     1.6   apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
     1.7 -apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
     1.8 +apply (clarsimp simp add: finite_psubset_def order_less_le)
     1.9  apply (blast intro!: finite_Diff dest: monoD)
    1.10  done
    1.11  
     2.1 --- a/src/HOL/Subst/Unify.thy	Sun Jun 04 10:52:47 2006 +0200
     2.2 +++ b/src/HOL/Subst/Unify.thy	Mon Jun 05 14:22:58 2006 +0200
     2.3 @@ -85,10 +85,7 @@
     2.4  
     2.5  text{*The non-nested TC (terminiation condition).*}
     2.6  recdef_tc unify_tc1: unify (1)
     2.7 -apply (simp add: unifyRel_def wf_lex_prod wf_finite_psubset, safe)
     2.8 -apply (simp add: finite_psubset_def finite_vars_of lex_prod_def inv_image_def)
     2.9 -apply (rule monotone_vars_of [THEN subset_iff_psubset_eq [THEN iffD1]])
    2.10 -done
    2.11 +  by (auto simp: unifyRel_def finite_psubset_def finite_vars_of)
    2.12  
    2.13  
    2.14  text{*Termination proof.*}
    2.15 @@ -104,7 +101,7 @@
    2.16  lemma Rassoc:
    2.17    "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) \<in> unifyRel  ==>
    2.18     ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \<in> unifyRel"
    2.19 -by (simp add: less_eq inv_image_def add_assoc Un_assoc
    2.20 +by (simp add: less_eq add_assoc Un_assoc
    2.21                unifyRel_def lex_prod_def)
    2.22  
    2.23  
    2.24 @@ -117,15 +114,14 @@
    2.25  apply (case_tac "Var x = M", clarify, simp)
    2.26  apply (case_tac "x \<in> (vars_of N1 Un vars_of N2)")
    2.27  txt{*uterm_less case*}
    2.28 -apply (simp add: less_eq unifyRel_def lex_prod_def inv_image_def)
    2.29 +apply (simp add: less_eq unifyRel_def lex_prod_def)
    2.30  apply blast
    2.31  txt{*@{text finite_psubset} case*}
    2.32 -apply (simp add: unifyRel_def lex_prod_def inv_image_def)
    2.33 +apply (simp add: unifyRel_def lex_prod_def)
    2.34  apply (simp add: finite_psubset_def finite_vars_of psubset_def)
    2.35  apply blast
    2.36  txt{*Final case, also @{text finite_psubset}*}
    2.37 -apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def
    2.38 -                 inv_image_def)
    2.39 +apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def)
    2.40  apply (cut_tac s = "[(x,M)]" and v = x and t = N2 in Var_elim)
    2.41  apply (cut_tac [3] s = "[(x,M)]" and v = x and t = N1 in Var_elim)
    2.42  apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq)
    2.43 @@ -156,7 +152,7 @@
    2.44  apply (rule_tac u = M1 and v = M2 in unify_induct0)
    2.45        apply (simp_all (no_asm_simp) add: var_elimR unify_simps0)
    2.46   txt{*Const-Const case*}
    2.47 - apply (simp add: unifyRel_def lex_prod_def inv_image_def less_eq)
    2.48 + apply (simp add: unifyRel_def lex_prod_def less_eq)
    2.49  txt{*Comb-Comb case*}
    2.50  apply (simp (no_asm_simp) split add: option.split)
    2.51  apply (intro strip)
     3.1 --- a/src/HOL/UNITY/Simple/Token.thy	Sun Jun 04 10:52:47 2006 +0200
     3.2 +++ b/src/HOL/UNITY/Simple/Token.thy	Mon Jun 05 14:22:58 2006 +0200
     3.3 @@ -79,7 +79,7 @@
     3.4  
     3.5  lemma (in Token) nodeOrder_eq: 
     3.6       "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
     3.7 -apply (unfold nodeOrder_def next_def measure_def inv_image_def)
     3.8 +apply (unfold nodeOrder_def next_def)
     3.9  apply (auto simp add: mod_Suc mod_geq)
    3.10  apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
    3.11  done
     4.1 --- a/src/HOL/UNITY/SubstAx.thy	Sun Jun 04 10:52:47 2006 +0200
     4.2 +++ b/src/HOL/UNITY/SubstAx.thy	Mon Jun 05 14:22:58 2006 +0200
     4.3 @@ -363,7 +363,7 @@
     4.4        ==> F \<in> A LeadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
     4.5  apply (rule_tac f = f and f1 = "%k. l - k" 
     4.6         in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
     4.7 -apply (simp add: inv_image_def Image_singleton, clarify)
     4.8 +apply (simp add: Image_singleton, clarify)
     4.9  apply (case_tac "m<l")
    4.10   apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
    4.11  apply (blast intro: not_leE subset_imp_LeadsTo)
     5.1 --- a/src/HOL/UNITY/WFair.thy	Sun Jun 04 10:52:47 2006 +0200
     5.2 +++ b/src/HOL/UNITY/WFair.thy	Mon Jun 05 14:22:58 2006 +0200
     5.3 @@ -492,7 +492,7 @@
     5.4        ==> F \<in> A leadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
     5.5  apply (rule_tac f = f and f1 = "%k. l - k" 
     5.6         in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct])
     5.7 -apply (simp (no_asm) add: inv_image_def Image_singleton)
     5.8 +apply (simp (no_asm) add:Image_singleton)
     5.9  apply clarify
    5.10  apply (case_tac "m<l")
    5.11   apply (blast intro: leadsTo_weaken_R diff_less_mono2)
     6.1 --- a/src/HOL/Wellfounded_Relations.thy	Sun Jun 04 10:52:47 2006 +0200
     6.2 +++ b/src/HOL/Wellfounded_Relations.thy	Mon Jun 05 14:22:58 2006 +0200
     6.3 @@ -70,11 +70,13 @@
     6.4  apply blast
     6.5  done
     6.6  
     6.7 +lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
     6.8 +  by (auto simp:inv_image_def)
     6.9  
    6.10  subsubsection{*Finally, All Measures are Wellfounded.*}
    6.11  
    6.12  lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
    6.13 -by (auto simp:measure_def inv_image_def)
    6.14 +  by (simp add:measure_def)
    6.15  
    6.16  lemma wf_measure [iff]: "wf (measure f)"
    6.17  apply (unfold measure_def)
    6.18 @@ -118,6 +120,10 @@
    6.19  apply (drule spec, erule mp, blast) 
    6.20  done
    6.21  
    6.22 +lemma in_lex_prod[simp]: 
    6.23 +  "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
    6.24 +  by (auto simp:lex_prod_def)
    6.25 +
    6.26  text{*Transitivity of WF combinators.*}
    6.27  lemma trans_lex_prod [intro!]: 
    6.28      "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
     7.1 --- a/src/HOL/ZF/Games.thy	Sun Jun 04 10:52:47 2006 +0200
     7.2 +++ b/src/HOL/ZF/Games.thy	Mon Jun 05 14:22:58 2006 +0200
     7.3 @@ -323,7 +323,7 @@
     7.4    have option_of: "option_of = inv_image is_option_of Rep_game"
     7.5      apply (rule set_ext)
     7.6      apply (case_tac "x")
     7.7 -    by (simp add: inv_image_def option_to_is_option_of) 
     7.8 +    by (simp add: option_to_is_option_of) 
     7.9    show ?thesis
    7.10      apply (simp add: option_of)
    7.11      apply (auto intro: wf_inv_image wf_is_option_of)
     8.1 --- a/src/HOL/ZF/LProd.thy	Sun Jun 04 10:52:47 2006 +0200
     8.2 +++ b/src/HOL/ZF/LProd.thy	Mon Jun 05 14:22:58 2006 +0200
     8.3 @@ -89,7 +89,7 @@
     8.4    shows "wf (lprod R)"
     8.5  proof -
     8.6    have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) multiset_of"
     8.7 -    by (auto simp add: inv_image_def lprod_implies_mult trans_trancl)
     8.8 +    by (auto simp add: lprod_implies_mult trans_trancl)
     8.9    note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="multiset_of", 
    8.10      OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
    8.11    note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
    8.12 @@ -122,7 +122,7 @@
    8.13    assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
    8.14  proof -
    8.15    have "gprod_2_1 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
    8.16 -    by (auto simp add: inv_image_def gprod_2_1_def lprod_2_1 lprod_2_2)
    8.17 +    by (auto simp add: gprod_2_1_def lprod_2_1 lprod_2_2)
    8.18    with wfR show ?thesis
    8.19      by (rule_tac wf_subset, auto)
    8.20  qed
    8.21 @@ -131,7 +131,7 @@
    8.22    assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
    8.23  proof -
    8.24    have "gprod_2_2 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
    8.25 -    by (auto simp add: inv_image_def gprod_2_2_def lprod_2_3 lprod_2_4)
    8.26 +    by (auto simp add: gprod_2_2_def lprod_2_3 lprod_2_4)
    8.27    with wfR show ?thesis
    8.28      by (rule_tac wf_subset, auto)
    8.29  qed
     9.1 --- a/src/HOL/ex/InductiveInvariant_examples.thy	Sun Jun 04 10:52:47 2006 +0200
     9.2 +++ b/src/HOL/ex/InductiveInvariant_examples.thy	Mon Jun 05 14:22:58 2006 +0200
     9.3 @@ -105,7 +105,7 @@
     9.4  lemma ninety_one_inv: "n < ninety_one n + 11"
     9.5  apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
     9.6  apply force
     9.7 -apply (auto simp add: indinv_def inv_image_def)
     9.8 +apply (auto simp add: indinv_def)
     9.9  apply (frule_tac x="x+11" in spec)
    9.10  apply (frule_tac x="f (x + 11)" in spec)
    9.11  by arith
    9.12 @@ -125,6 +125,6 @@
    9.13                     then x - 10
    9.14                     else ninety_one (ninety_one (x+11)))"
    9.15  by (subst ninety_one.simps,
    9.16 -    simp add: ninety_one_tc inv_image_def)
    9.17 +    simp add: ninety_one_tc)
    9.18  
    9.19  end
    10.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Sun Jun 04 10:52:47 2006 +0200
    10.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Jun 05 14:22:58 2006 +0200
    10.3 @@ -834,12 +834,12 @@
    10.4      {
    10.5        assume nlini: "linearize i = None"
    10.6        from nlini have "linearize (Add i j) = None" 
    10.7 -	by (simp add: inv_image_def) then have ?thesis using prems by auto}
    10.8 +	by simp then have ?thesis using prems by auto}
    10.9      moreover 
   10.10      { assume nlinj: "linearize j = None"
   10.11  	and lini: "\<exists> li. linearize i = Some li"
   10.12        from nlinj lini have "linearize (Add i j) = None"
   10.13 -	by (simp add: inv_image_def, auto) with prems  have ?thesis by auto}
   10.14 +	by auto with prems have ?thesis by auto}
   10.15      moreover 
   10.16      { assume lini: "\<exists>li. linearize i = Some li"
   10.17  	and linj: "\<exists>lj. linearize j = Some lj"