added lemma in_measure
authornipkow
Fri May 12 11:19:41 2006 +0200 (2006-05-12)
changeset 1962312e6cc4382ae
parent 19622 ab08841928b4
child 19624 3b6629701a79
added lemma in_measure
src/HOL/List.thy
src/HOL/Subst/Unify.thy
src/HOL/Transitive_Closure.thy
src/HOL/Wellfounded_Relations.thy
src/HOL/ex/InductiveInvariant_examples.thy
src/HOL/ex/Reflected_Presburger.thy
     1.1 --- a/src/HOL/List.thy	Fri May 12 10:38:00 2006 +0200
     1.2 +++ b/src/HOL/List.thy	Fri May 12 11:19:41 2006 +0200
     1.3 @@ -2428,7 +2428,7 @@
     1.4  lemma lenlex_conv:
     1.5      "lenlex r = {(xs,ys). length xs < length ys |
     1.6                   length xs = length ys \<and> (xs, ys) : lex r}"
     1.7 -by (simp add: lenlex_def diag_def lex_prod_def measure_def inv_image_def)
     1.8 +by (simp add: lenlex_def diag_def lex_prod_def inv_image_def)
     1.9  
    1.10  lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
    1.11  by (simp add: lex_conv)
     2.1 --- a/src/HOL/Subst/Unify.thy	Fri May 12 10:38:00 2006 +0200
     2.2 +++ b/src/HOL/Subst/Unify.thy	Fri May 12 11:19:41 2006 +0200
     2.3 @@ -86,8 +86,7 @@
     2.4  text{*The non-nested TC (terminiation condition).*}
     2.5  recdef_tc unify_tc1: unify (1)
     2.6  apply (simp add: unifyRel_def wf_lex_prod wf_finite_psubset, safe)
     2.7 -apply (simp add: finite_psubset_def finite_vars_of lex_prod_def measure_def
     2.8 -                 inv_image_def)
     2.9 +apply (simp add: finite_psubset_def finite_vars_of lex_prod_def inv_image_def)
    2.10  apply (rule monotone_vars_of [THEN subset_iff_psubset_eq [THEN iffD1]])
    2.11  done
    2.12  
    2.13 @@ -105,7 +104,7 @@
    2.14  lemma Rassoc:
    2.15    "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) \<in> unifyRel  ==>
    2.16     ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \<in> unifyRel"
    2.17 -by (simp add: measure_def less_eq inv_image_def add_assoc Un_assoc
    2.18 +by (simp add: less_eq inv_image_def add_assoc Un_assoc
    2.19                unifyRel_def lex_prod_def)
    2.20  
    2.21  
    2.22 @@ -118,15 +117,15 @@
    2.23  apply (case_tac "Var x = M", clarify, simp)
    2.24  apply (case_tac "x \<in> (vars_of N1 Un vars_of N2)")
    2.25  txt{*uterm_less case*}
    2.26 -apply (simp add: less_eq unifyRel_def lex_prod_def measure_def inv_image_def)
    2.27 +apply (simp add: less_eq unifyRel_def lex_prod_def inv_image_def)
    2.28  apply blast
    2.29  txt{*@{text finite_psubset} case*}
    2.30 -apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def)
    2.31 +apply (simp add: unifyRel_def lex_prod_def inv_image_def)
    2.32  apply (simp add: finite_psubset_def finite_vars_of psubset_def)
    2.33  apply blast
    2.34  txt{*Final case, also @{text finite_psubset}*}
    2.35  apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def
    2.36 -                 measure_def inv_image_def)
    2.37 +                 inv_image_def)
    2.38  apply (cut_tac s = "[(x,M)]" and v = x and t = N2 in Var_elim)
    2.39  apply (cut_tac [3] s = "[(x,M)]" and v = x and t = N1 in Var_elim)
    2.40  apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq)
    2.41 @@ -157,7 +156,7 @@
    2.42  apply (rule_tac u = M1 and v = M2 in unify_induct0)
    2.43        apply (simp_all (no_asm_simp) add: var_elimR unify_simps0)
    2.44   txt{*Const-Const case*}
    2.45 - apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def less_eq)
    2.46 + apply (simp add: unifyRel_def lex_prod_def inv_image_def less_eq)
    2.47  txt{*Comb-Comb case*}
    2.48  apply (simp (no_asm_simp) split add: option.split)
    2.49  apply (intro strip)
     3.1 --- a/src/HOL/Transitive_Closure.thy	Fri May 12 10:38:00 2006 +0200
     3.2 +++ b/src/HOL/Transitive_Closure.thy	Fri May 12 11:19:41 2006 +0200
     3.3 @@ -267,7 +267,7 @@
     3.4  lemma trancl_unfold: "r^+ = r Un (r O r^+)"
     3.5    by (auto intro: trancl_into_trancl elim: tranclE)
     3.6  
     3.7 -lemma trans_trancl: "trans(r^+)"
     3.8 +lemma trans_trancl[simp]: "trans(r^+)"
     3.9    -- {* Transitivity of @{term "r^+"} *}
    3.10  proof (rule transI)
    3.11    fix x y z
    3.12 @@ -278,6 +278,14 @@
    3.13  
    3.14  lemmas trancl_trans = trans_trancl [THEN transD, standard]
    3.15  
    3.16 +lemma trancl_id[simp]: "trans r \<Longrightarrow> r^+ = r"
    3.17 +apply(auto)
    3.18 +apply(erule trancl_induct)
    3.19 +apply assumption
    3.20 +apply(unfold trans_def)
    3.21 +apply(blast)
    3.22 +done
    3.23 +
    3.24  lemma rtrancl_trancl_trancl: assumes r: "(x, y) \<in> r^*"
    3.25    shows "!!z. (y, z) \<in> r^+ ==> (x, z) \<in> r^+" using r
    3.26    by induct (iprover intro: trancl_trans)+
     4.1 --- a/src/HOL/Wellfounded_Relations.thy	Fri May 12 10:38:00 2006 +0200
     4.2 +++ b/src/HOL/Wellfounded_Relations.thy	Fri May 12 11:19:41 2006 +0200
     4.3 @@ -73,6 +73,9 @@
     4.4  
     4.5  subsubsection{*Finally, All Measures are Wellfounded.*}
     4.6  
     4.7 +lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
     4.8 +by (auto simp:measure_def inv_image_def)
     4.9 +
    4.10  lemma wf_measure [iff]: "wf (measure f)"
    4.11  apply (unfold measure_def)
    4.12  apply (rule wf_less_than [THEN wf_inv_image])
    4.13 @@ -91,9 +94,8 @@
    4.14      proof (rule step)
    4.15        fix y
    4.16        assume "f y < f x"
    4.17 -      then have "(y, x) \<in> measure f"
    4.18 -        by (simp add: measure_def inv_image_def)
    4.19 -      then show "P y" by (rule less)
    4.20 +      hence "(y, x) \<in> measure f" by simp
    4.21 +      thus "P y" by (rule less)
    4.22      qed
    4.23    qed
    4.24  qed
     5.1 --- a/src/HOL/ex/InductiveInvariant_examples.thy	Fri May 12 10:38:00 2006 +0200
     5.2 +++ b/src/HOL/ex/InductiveInvariant_examples.thy	Fri May 12 11:19:41 2006 +0200
     5.3 @@ -105,7 +105,7 @@
     5.4  lemma ninety_one_inv: "n < ninety_one n + 11"
     5.5  apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
     5.6  apply force
     5.7 -apply (auto simp add: indinv_def measure_def inv_image_def)
     5.8 +apply (auto simp add: indinv_def inv_image_def)
     5.9  apply (frule_tac x="x+11" in spec)
    5.10  apply (frule_tac x="f (x + 11)" in spec)
    5.11  by arith
    5.12 @@ -125,6 +125,6 @@
    5.13                     then x - 10
    5.14                     else ninety_one (ninety_one (x+11)))"
    5.15  by (subst ninety_one.simps,
    5.16 -    simp add: ninety_one_tc measure_def inv_image_def)
    5.17 +    simp add: ninety_one_tc inv_image_def)
    5.18  
    5.19  end
     6.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Fri May 12 10:38:00 2006 +0200
     6.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Fri May 12 11:19:41 2006 +0200
     6.3 @@ -832,12 +832,12 @@
     6.4      {
     6.5        assume nlini: "linearize i = None"
     6.6        from nlini have "linearize (Add i j) = None" 
     6.7 -	by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto}
     6.8 +	by (simp add: inv_image_def) then have ?thesis using prems by auto}
     6.9      moreover 
    6.10      { assume nlinj: "linearize j = None"
    6.11  	and lini: "\<exists> li. linearize i = Some li"
    6.12 -      from nlinj lini have "linearize (Add i j) = None" 
    6.13 -	by (simp add: Let_def measure_def inv_image_def, auto) with prems  have ?thesis by auto}
    6.14 +      from nlinj lini have "linearize (Add i j) = None"
    6.15 +	by (simp add: inv_image_def, auto) with prems  have ?thesis by auto}
    6.16      moreover 
    6.17      { assume lini: "\<exists>li. linearize i = Some li"
    6.18  	and linj: "\<exists>lj. linearize j = Some lj"
    6.19 @@ -846,7 +846,7 @@
    6.20        from linj obtain "lj" where  "linearize j = Some lj" by blast
    6.21        have linlj: "islinintterm lj" by (simp!)
    6.22        moreover from lini linj have "linearize (Add i j) = Some (lin_add (li,lj))" 
    6.23 -	by (simp add: measure_def inv_image_def, auto!)
    6.24 +	by (auto!)
    6.25        moreover from linli linlj have "islinintterm(lin_add (li,lj))" by (simp add: lin_add_lin)
    6.26        ultimately have ?thesis by simp  }
    6.27      ultimately show ?thesis by blast
    6.28 @@ -858,14 +858,14 @@
    6.29      moreover 
    6.30      {
    6.31        assume nlini: "linearize i = None"
    6.32 -      from nlini have "linearize (Sub i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis by (auto!)
    6.33 +      from nlini have "linearize (Sub i j) = None" by simp then have ?thesis by (auto!)
    6.34      }
    6.35      moreover 
    6.36      {
    6.37        assume lini: "\<exists> li. linearize i = Some li"
    6.38  	and nlinj: "linearize j = None"
    6.39        from nlinj lini have "linearize (Sub i j) = None" 
    6.40 -	by (simp add: Let_def measure_def inv_image_def, auto) then have ?thesis by (auto!)
    6.41 +	by auto then have ?thesis by (auto!)
    6.42      }
    6.43      moreover 
    6.44      {
    6.45 @@ -876,7 +876,7 @@
    6.46        from linj obtain "lj" where  "linearize j = Some lj" by blast
    6.47        have linlj: "islinintterm lj" by (simp!)
    6.48        moreover from lini linj have "linearize (Sub i j) = Some (lin_add (li,lin_neg lj))" 
    6.49 -	by (simp add: measure_def inv_image_def, auto!)
    6.50 +	by (auto!)
    6.51        moreover from linli linlj have "islinintterm(lin_add (li,lin_neg lj))" by (simp add: lin_add_lin lin_neg_lin)
    6.52        ultimately have ?thesis by simp
    6.53      }
    6.54 @@ -893,8 +893,7 @@
    6.55      moreover 
    6.56      {
    6.57        assume nlini: "linearize i = None"
    6.58 -      from nlini have "linearize (Mult i j) = None" 
    6.59 -	by (simp add: Let_def measure_def inv_image_def)  
    6.60 +      from nlini have "linearize (Mult i j) = None" by (simp)
    6.61        with prems have ?thesis by auto }
    6.62      moreover 
    6.63      {  assume lini: "\<exists> li. linearize i = Some li"
    6.64 @@ -902,7 +901,7 @@
    6.65        from lini obtain "li" where "linearize i = Some li" by blast 
    6.66        moreover from nlinj lini have "linearize (Mult i j) = None"
    6.67  	using prems
    6.68 -	by (cases li ) (auto simp add: Let_def measure_def inv_image_def)
    6.69 +	by (cases li) (auto)
    6.70        with prems have ?thesis by auto}
    6.71      moreover 
    6.72      { assume lini: "\<exists>li. linearize i = Some li"
    6.73 @@ -914,7 +913,7 @@
    6.74        have linlj: "islinintterm (Cst bj)" by simp 
    6.75        moreover from lini linj prems 
    6.76        have "linearize (Mult i j) = Some (lin_mul (bj,li))"
    6.77 -	by (cases li) (auto simp add: measure_def inv_image_def)
    6.78 +	by (cases li) auto
    6.79        moreover from linli linlj have "islinintterm(lin_mul (bj,li))" by (simp add: lin_mul_lin)
    6.80        ultimately have ?thesis by simp  }
    6.81      moreover 
    6.82 @@ -926,7 +925,7 @@
    6.83        from linj  obtain "lj" where  "linearize j = Some lj" by blast
    6.84        from prems have linlj: "islinintterm lj" by simp
    6.85        moreover from lini linj prems have "linearize (Mult i j) = Some (lin_mul (bi,lj))" 
    6.86 -	by (simp add: measure_def inv_image_def) 
    6.87 +	by simp 
    6.88        moreover from linli linlj have "islinintterm(lin_mul (bi,lj))" by (simp add: lin_mul_lin)
    6.89        ultimately have ?thesis by simp }
    6.90      moreover 
    6.91 @@ -936,7 +935,7 @@
    6.92        moreover 
    6.93        from ljnc obtain "lj" where "linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)" by blast
    6.94        ultimately have "linearize (Mult i j) = None"
    6.95 -	by (cases li, auto simp add: measure_def inv_image_def) (cases lj, auto)+
    6.96 +	by (cases li, auto) (cases lj, auto)+
    6.97        with prems have ?thesis by simp }
    6.98      ultimately show ?thesis by blast
    6.99    qed
   6.100 @@ -987,14 +986,13 @@
   6.101      moreover 
   6.102      {
   6.103        assume nlini: "linearize i = None"
   6.104 -      from nlini have "linearize (Add i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto
   6.105 +      from nlini have "linearize (Add i j) = None" by simp then have ?thesis using prems by auto
   6.106      }
   6.107      moreover 
   6.108      {
   6.109        assume nlinj: "linearize j = None"
   6.110  	and lini: "\<exists> li. linearize i = Some li"
   6.111 -      from nlinj lini have "linearize (Add i j) = None" 
   6.112 -	by (simp add: Let_def measure_def inv_image_def, auto) 
   6.113 +      from nlinj lini have "linearize (Add i j) = None"	by auto 
   6.114        then have ?thesis using prems by auto
   6.115      }
   6.116      moreover 
   6.117 @@ -1010,7 +1008,7 @@
   6.118        from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1)
   6.119        then have linlj: "islinintterm lj" using prems by simp
   6.120        moreover from lini linj have "linearize (Add i j) = Some (lin_add (li,lj))"
   6.121 -	using prems by (simp add: measure_def inv_image_def)
   6.122 +	using prems by simp
   6.123        moreover from linli linlj have "I_intterm ats (lin_add (li,lj)) = I_intterm ats (Add li lj)" by (simp add: lin_add_corr)
   6.124        ultimately have ?thesis using prems by simp
   6.125      }
   6.126 @@ -1023,14 +1021,14 @@
   6.127      moreover 
   6.128      {
   6.129        assume nlini: "linearize i = None"
   6.130 -      from nlini have "linearize (Sub i j) = None" by (simp add: Let_def measure_def inv_image_def) then have ?thesis using prems by auto
   6.131 +      from nlini have "linearize (Sub i j) = None" by simp then have ?thesis using prems by auto
   6.132      }
   6.133      moreover 
   6.134      {
   6.135        assume lini: "\<exists> li. linearize i = Some li"
   6.136  	and nlinj: "linearize j = None"
   6.137        from nlinj lini have "linearize (Sub i j) = None" 
   6.138 -	by (simp add: Let_def measure_def inv_image_def, auto) with prems have ?thesis by auto
   6.139 +	by auto with prems have ?thesis by auto
   6.140      }
   6.141      moreover 
   6.142      {
   6.143 @@ -1045,7 +1043,7 @@
   6.144        from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1)
   6.145        with prems have linlj: "islinintterm lj" by simp
   6.146        moreover from prems have "linearize (Sub i j) = Some (lin_add (li,lin_neg lj))" 
   6.147 -	by (simp add: measure_def inv_image_def)
   6.148 +	by simp
   6.149        moreover from linlj have linnlj:"islinintterm (lin_neg lj)" by (simp add: lin_neg_lin)
   6.150        moreover from linli linnlj have "I_intterm ats (lin_add (li,lin_neg lj)) = I_intterm ats (Add li (lin_neg lj))" by (simp only: lin_add_corr[OF linli linnlj])
   6.151        moreover from linli linlj linnlj have "I_intterm ats (Add li (lin_neg lj)) = I_intterm ats (Sub li lj)" 
   6.152 @@ -1065,7 +1063,7 @@
   6.153      moreover 
   6.154      {
   6.155        assume nlini: "linearize i = None"
   6.156 -      from nlini have "linearize (Mult i j) = None" by (simp add: Let_def measure_def inv_image_def) with prems  have ?thesis by auto
   6.157 +      from nlini have "linearize (Mult i j) = None" by simp with prems  have ?thesis by auto
   6.158      }
   6.159      moreover 
   6.160      {
   6.161 @@ -1074,7 +1072,7 @@
   6.162  
   6.163        from lini obtain "li" where "linearize i = Some li" by blast 
   6.164        moreover from prems have "linearize (Mult i j) = None" 
   6.165 -	by (cases li) (simp_all add: Let_def measure_def inv_image_def)
   6.166 +	by (cases li) simp_all
   6.167        with prems have ?thesis by auto
   6.168      }
   6.169      moreover 
   6.170 @@ -1090,7 +1088,7 @@
   6.171        from linj  obtain "bj" where  "linearize j = Some (Cst bj)" by blast
   6.172        have linlj: "islinintterm (Cst bj)" by simp
   6.173        moreover from prems have "linearize (Mult i j) = Some (lin_mul (bj,li))"
   6.174 - 	by (cases li) (auto simp add: measure_def inv_image_def) 
   6.175 + 	by (cases li) auto
   6.176        then have lm1: "I_intterm ats (the(linearize (Mult i j))) = I_intterm ats (lin_mul (bj,li))" by simp
   6.177        moreover from linli linlj have "I_intterm ats (lin_mul(bj,li)) = I_intterm ats (Mult li (Cst bj))" by (simp add: lin_mul_corr)
   6.178        with prems 
   6.179 @@ -1100,7 +1098,7 @@
   6.180        moreover have "I_intterm ats i = I_intterm ats (the (linearize i))"  
   6.181  	using lini2 lini "6.hyps" by simp
   6.182  	moreover have "I_intterm ats j = I_intterm ats (the (linearize j))"
   6.183 -	  using prems by (cases li) (auto simp add: measure_def inv_image_def)
   6.184 +	  using prems by (cases li) auto
   6.185        ultimately have ?thesis by auto }
   6.186      moreover 
   6.187      { assume lini: "\<exists>bi. linearize i = Some (Cst bi)"
   6.188 @@ -1113,8 +1111,8 @@
   6.189        from linj  obtain "lj" where  "linearize j = Some lj" by blast
   6.190        from linj2 have "islinintterm (the (linearize j))" by (simp add: linearize_linear1) 
   6.191        then have linlj: "islinintterm lj" by (simp!)
   6.192 -      moreover from linli lini linj have "linearize (Mult i j) = Some (lin_mul (bi,lj))" 	apply (simp add: measure_def inv_image_def) 
   6.193 -	apply auto by (case_tac "li::intterm",auto!)
   6.194 +      moreover from linli lini linj have "linearize (Mult i j) = Some (lin_mul (bi,lj))"
   6.195 +	by (case_tac "li::intterm",auto!)
   6.196        then have lm1: "I_intterm ats (the(linearize (Mult i j))) = I_intterm ats (lin_mul (bi,lj))" by simp
   6.197        moreover from linli linlj have "I_intterm ats (lin_mul(bi,lj)) = I_intterm ats (Mult (Cst bi) lj)" by (simp add: lin_mul_corr)
   6.198        then have "I_intterm ats (lin_mul(bi,lj)) = I_intterm ats (Mult (the (linearize i)) lj)" by (auto!)
   6.199 @@ -1132,7 +1130,7 @@
   6.200        moreover 
   6.201        from ljnc obtain "lj" where "\<exists> lj. linearize j = Some lj \<and> \<not> (\<exists> bj. lj = Cst bj)" by blast
   6.202        ultimately have "linearize (Mult i j) = None"
   6.203 -	apply (simp add: measure_def inv_image_def)
   6.204 +	apply simp
   6.205  	apply (case_tac "linearize i", auto)
   6.206  	apply (case_tac a)
   6.207  	apply (auto!)
   6.208 @@ -4495,12 +4493,12 @@
   6.209    with prems have nv0a':"novar0I a'" by simp
   6.210    have lina': "islinintterm a'" using prems by (simp add: linearize_linear)
   6.211    from linab have "\<exists> b'. ?lb = Some b'"
   6.212 -    by (cases ?la, auto simp add: measure_def inv_image_def) (cases ?lb, auto)
   6.213 +    by (cases ?la, auto) (cases ?lb, auto)
   6.214    then obtain "b'" where "?lb = Some b'" by blast
   6.215    with prems have nv0b':"novar0I b'" by simp
   6.216    have linb': "islinintterm b'" using prems by (simp add: linearize_linear)
   6.217    then show ?case using prems lina' linb' nv0a' nv0b'
   6.218 -    by (auto simp add: measure_def inv_image_def lin_add_novar0)
   6.219 +    by (auto simp add: lin_add_novar0)
   6.220  next 
   6.221    case (Sub a b)
   6.222      let ?la = "linearize a"
   6.223 @@ -4511,32 +4509,30 @@
   6.224    with prems have nv0a':"novar0I a'" by simp
   6.225    have lina': "islinintterm a'" using prems by (simp add: linearize_linear)
   6.226    from linab have "\<exists> b'. ?lb = Some b'"
   6.227 -    by (cases ?la, auto simp add: measure_def inv_image_def) (cases ?lb, auto)
   6.228 +    by (cases ?la, auto) (cases ?lb, auto)
   6.229    then obtain "b'" where "?lb = Some b'" by blast
   6.230    with prems have nv0b':"novar0I b'" by simp
   6.231    have linb': "islinintterm b'" using prems by (simp add: linearize_linear)
   6.232    then show ?case using prems lina' linb' nv0a' nv0b'
   6.233 -    by (auto simp add: 
   6.234 -      measure_def inv_image_def lin_add_novar0 lin_neg_novar0 lin_neg_lin)
   6.235 +    by (auto simp add: lin_add_novar0 lin_neg_novar0 lin_neg_lin)
   6.236  next 
   6.237    case (Mult a b)     
   6.238    let ?la = "linearize a"
   6.239    let ?lb = "linearize b"
   6.240    from prems have linab: "linearize (Mult a b) = Some t'" by simp
   6.241 -  then have "\<exists> a'. ?la = Some a'"
   6.242 -    by (cases ?la, auto simp add: measure_def inv_image_def)
   6.243 +  then have "\<exists> a'. ?la = Some a'" by (cases ?la, auto)
   6.244    then obtain "a'" where "?la = Some a'" by blast
   6.245    with prems have nv0a':"novar0I a'" by simp
   6.246    have lina': "islinintterm a'" using prems by (simp add: linearize_linear)
   6.247    from prems linab have "\<exists> b'. ?lb = Some b'"
   6.248 -    apply (cases ?la, auto simp add: measure_def inv_image_def) 
   6.249 -    by (cases "a'",auto simp add: measure_def inv_image_def) (cases ?lb, auto)+
   6.250 +    apply (cases ?la, auto)
   6.251 +    by (cases "a'",auto) (cases ?lb, auto)+
   6.252    then obtain "b'" where "?lb = Some b'" by blast
   6.253    with prems have nv0b':"novar0I b'" by simp
   6.254    have linb': "islinintterm b'" using prems by (simp add: linearize_linear)
   6.255    then show ?case using prems lina' linb' nv0a' nv0b' 
   6.256 -    by (cases "a'",auto simp add: measure_def inv_image_def lin_mul_novar0)
   6.257 -  (cases "b'",auto simp add: measure_def inv_image_def lin_mul_novar0)
   6.258 +    by (cases "a'",auto simp add: lin_mul_novar0)
   6.259 +  (cases "b'",auto simp add: lin_mul_novar0)
   6.260  qed auto
   6.261  
   6.262  
   6.263 @@ -4650,7 +4646,7 @@
   6.264  	  assume lxcst: "\<exists> i. lx = Cst i"
   6.265  	  from lxcst obtain "i" where lxi: "lx = Cst i" by blast
   6.266  	  with feq have "qinterp ats (Le l r) = (i \<le> 0)" by simp
   6.267 -	  then have ?case using prems by (simp add: measure_def inv_image_def)
   6.268 +	  then have ?case using prems by simp
   6.269  	}
   6.270  	moreover 
   6.271  	{
   6.272 @@ -4659,7 +4655,7 @@
   6.273  	    Cst i \<Rightarrow> (if i \<le> 0 then T else F)
   6.274  	    | _ \<Rightarrow> (Le lx (Cst 0))) = (Le lx (Cst 0))" 
   6.275  	    by (case_tac "lx::intterm", auto)
   6.276 -	  with prems lxlin feq have ?case by (auto simp add: measure_def inv_image_def)
   6.277 +	  with prems lxlin feq have ?case by auto
   6.278  	}
   6.279  	ultimately show ?thesis  by blast
   6.280        qed
   6.281 @@ -4690,7 +4686,7 @@
   6.282  	  assume lxcst: "\<exists> i. lx = Cst i"
   6.283  	  from lxcst obtain "i" where lxi: "lx = Cst i" by blast
   6.284  	  with feq have "qinterp ats (Eq l r) = (i = 0)" by simp
   6.285 -	  then have ?case using prems by (simp add: measure_def inv_image_def)
   6.286 +	  then have ?case using prems by simp
   6.287  	}
   6.288  	moreover 
   6.289  	{
   6.290 @@ -4699,7 +4695,7 @@
   6.291  	    Cst i \<Rightarrow> (if i = 0 then T else F)
   6.292  	    | _ \<Rightarrow> (Eq lx (Cst 0))) = (Eq lx (Cst 0))" 
   6.293  	    by (case_tac "lx::intterm", auto)
   6.294 -	  with prems lxlin feq have ?case by (auto simp add: measure_def inv_image_def)
   6.295 +	  with prems lxlin feq have ?case by auto
   6.296  	}
   6.297  	ultimately show ?thesis  by blast
   6.298        qed
   6.299 @@ -4738,14 +4734,13 @@
   6.300      let ?sf = "psimpl f"
   6.301    let ?sg = "psimpl g"
   6.302    show ?case using prems 
   6.303 -    by (cases ?sf, simp_all add: Let_def measure_def inv_image_def) 
   6.304 -  (cases ?sg, simp_all)+
   6.305 +    by (cases ?sf, simp_all add: Let_def) (cases ?sg, simp_all)+
   6.306  next
   6.307    case (5 f g)
   6.308        let ?sf = "psimpl f"
   6.309    let ?sg = "psimpl g"
   6.310    show ?case using prems
   6.311 -    apply (cases ?sf, simp_all add: Let_def measure_def inv_image_def) 
   6.312 +    apply (cases ?sf, simp_all add: Let_def) 
   6.313      apply (cases ?sg, simp_all)
   6.314      apply (cases ?sg, simp_all)
   6.315      apply (cases ?sg, simp_all)
   6.316 @@ -4765,9 +4760,9 @@
   6.317    let ?sf = "psimpl f"
   6.318    let ?sg = "psimpl g"
   6.319    show ?case using prems 
   6.320 -    apply(simp add: Let_def measure_def inv_image_def)
   6.321 +    apply(simp add: Let_def)
   6.322      apply(cases ?sf,simp_all)
   6.323 -    apply (simp_all add: Let_def measure_def inv_image_def)
   6.324 +    apply (simp_all add: Let_def)
   6.325      apply(cases ?sg, simp_all)
   6.326      apply(cases ?sg, simp_all)
   6.327      apply(cases ?sg, simp_all)
   6.328 @@ -4820,8 +4815,7 @@
   6.329    have "?ls = None \<or> (\<exists> x. ?ls = Some x)" by auto
   6.330    moreover
   6.331    {
   6.332 -    assume "?ls = None" then have ?case 
   6.333 -      using prems by (simp add: measure_def inv_image_def)
   6.334 +    assume "?ls = None" then have ?case using prems by simp
   6.335    }
   6.336    moreover {
   6.337      assume "\<exists> x. ?ls = Some x"
   6.338 @@ -4833,7 +4827,7 @@
   6.339        by (simp add: linearize_novar0[OF nv0s, where t'="x"])
   6.340      then have ?case
   6.341        using prems
   6.342 -      by (cases "x") (auto simp add: measure_def inv_image_def)
   6.343 +      by (cases "x") auto
   6.344    }
   6.345    ultimately show ?case by blast
   6.346  next
   6.347 @@ -4842,8 +4836,7 @@
   6.348    have "?ls = None \<or> (\<exists> x. ?ls = Some x)" by auto
   6.349    moreover
   6.350    {
   6.351 -    assume "?ls = None" then have ?case 
   6.352 -      using prems by (simp add: measure_def inv_image_def)
   6.353 +    assume "?ls = None" then have ?case using prems by simp
   6.354    }
   6.355    moreover {
   6.356      assume "\<exists> x. ?ls = Some x"
   6.357 @@ -4853,9 +4846,7 @@
   6.358      ultimately have nv0s: "novar0I (Sub l r)" by simp
   6.359      from prems have "novar0I x" 
   6.360        by (simp add: linearize_novar0[OF nv0s, where t'="x"])
   6.361 -    then have ?case
   6.362 -      using prems
   6.363 -      by (cases "x") (auto simp add: measure_def inv_image_def)
   6.364 +    then have ?case using prems by (cases "x") auto
   6.365    }
   6.366    ultimately show ?case by blast
   6.367  next
   6.368 @@ -4878,41 +4869,31 @@
   6.369    case (4 f g)
   6.370    let ?sf = "psimpl f"
   6.371    let ?sg = "psimpl g"
   6.372 -  show ?case 
   6.373 -    using prems 
   6.374 -    by (cases ?sf, simp_all add: Let_def measure_def inv_image_def)
   6.375 -  (cases ?sg,simp_all)+
   6.376 +  show ?case using prems 
   6.377 +    by (cases ?sf, simp_all add: Let_def) (cases ?sg,simp_all)+
   6.378  next
   6.379    case (5 f g)
   6.380    let ?sf = "psimpl f"
   6.381    let ?sg = "psimpl g"
   6.382 -  show ?case 
   6.383 -    using prems 
   6.384 -    by (cases ?sf, simp_all add: Let_def measure_def inv_image_def)
   6.385 -  (cases ?sg,simp_all)+
   6.386 +  show ?case using prems
   6.387 +    by (cases ?sf, simp_all add: Let_def) (cases ?sg,simp_all)+
   6.388  next
   6.389    case (6 f g)
   6.390    let ?sf = "psimpl f"
   6.391    let ?sg = "psimpl g"
   6.392 -  show ?case 
   6.393 -    using prems 
   6.394 -    by (cases ?sf, simp_all add: Let_def measure_def inv_image_def)
   6.395 -  (cases ?sg,simp_all)+
   6.396 +  show ?case using prems
   6.397 +    by (cases ?sf, simp_all add: Let_def) (cases ?sg,simp_all)+
   6.398  next
   6.399    case (7 f g)
   6.400    let ?sf = "psimpl f"
   6.401    let ?sg = "psimpl g"
   6.402 -  show ?case 
   6.403 -    using prems 
   6.404 -    by (cases ?sf, simp_all add: Let_def measure_def inv_image_def)
   6.405 -  (cases ?sg,simp_all)+
   6.406 -
   6.407 +  show ?case using prems
   6.408 +    by (cases ?sf, simp_all add: Let_def) (cases ?sg,simp_all)+
   6.409  next
   6.410    case (8 f)
   6.411    let ?sf = "psimpl f"
   6.412    from prems have nv0sf:"novar0 ?sf" by simp
   6.413 -  show ?case using prems nv0sf 
   6.414 -    by (cases ?sf, auto simp add: Let_def measure_def inv_image_def)
   6.415 +  show ?case using prems nv0sf by (cases ?sf, auto simp add: Let_def)
   6.416  qed simp_all
   6.417  
   6.418  (* implements a disj of p applied to all elements of the list*)
   6.419 @@ -5554,7 +5535,7 @@
   6.420  
   6.421  lemma psimpl_qfree: "isqfree p \<Longrightarrow> isqfree (psimpl p)"
   6.422  apply(induct p rule: isqfree.induct)
   6.423 -apply(auto simp add: Let_def measure_def inv_image_def)
   6.424 +apply(auto simp add: Let_def)
   6.425  apply (simp_all cong del: QF.weak_case_cong add: Let_def)
   6.426  apply (case_tac "psimpl p", auto)
   6.427  apply (case_tac "psimpl q", auto)
   6.428 @@ -5670,7 +5651,7 @@
   6.429      | (Some lj) \<Rightarrow> (case lj of 
   6.430          Cst b \<Rightarrow> Some (lin_mul (b,li))
   6.431        | _ \<Rightarrow> None))))"
   6.432 -by (simp add: measure_def inv_image_def)
   6.433 +by simp
   6.434  
   6.435  lemma [code]: "psimpl (And p q) = 
   6.436    (let p'= psimpl p
   6.437 @@ -5683,7 +5664,7 @@
   6.438                     | T \<Rightarrow> p'
   6.439                     | _ \<Rightarrow> (And p' q'))))"
   6.440  
   6.441 -by (simp add: measure_def inv_image_def)
   6.442 +by simp
   6.443  
   6.444  lemma [code]: "psimpl (Or p q) = 
   6.445    (let p'= psimpl p
   6.446 @@ -5696,7 +5677,7 @@
   6.447                     | F \<Rightarrow> p'
   6.448                     | _ \<Rightarrow> (Or p' q'))))"
   6.449  
   6.450 -by (simp add: measure_def inv_image_def)
   6.451 +by simp
   6.452  
   6.453  lemma [code]: "psimpl (Imp p q) = 
   6.454    (let p'= psimpl p
   6.455 @@ -5713,7 +5694,7 @@
   6.456                       F \<Rightarrow> NOT p'
   6.457                     | T \<Rightarrow> T
   6.458                     | _ \<Rightarrow> (Imp p' q'))))"
   6.459 -by (simp add: measure_def inv_image_def)
   6.460 +by simp
   6.461  
   6.462  declare zdvd_iff_zmod_eq_0 [code]
   6.463