author nipkow Sun, 30 Sep 2018 09:00:11 +0200 changeset 69085 9999d7823b8f parent 69084 c7c38c901267 child 69086 2859dcdbc849
updated to new list_update precedence
```--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Sep 30 07:46:38 2018 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Sep 30 09:00:11 2018 +0200
@@ -2258,11 +2258,11 @@
from i have i': "i < length (replicate (k+1) 0)"   "i < k+1"
unfolding length_replicate by presburger+
-    have "xs = replicate (k+1) 0 [i := n]"
+    have "xs = (replicate (k+1) 0) [i := n]"
proof (rule nth_equalityI)
-      show "length xs = length (replicate (k + 1) 0[i := n])"
+      show "length xs = length ((replicate (k + 1) 0)[i := n])"
by (metis length_list_update length_replicate xsl)
-      show "xs ! j = replicate (k + 1) 0[i := n] ! j" if "j < length xs" for j
+      show "xs ! j = (replicate (k + 1) 0)[i := n] ! j" if "j < length xs" for j
proof (cases "j = i")
case True
then show ?thesis
@@ -2279,7 +2279,7 @@
proof
fix xs
assume "xs \<in> ?B"
-    then obtain i where i: "i \<in> {0..k}" and xs: "xs = replicate (k + 1) 0 [i:=n]"
+    then obtain i where i: "i \<in> {0..k}" and xs: "xs = (replicate (k + 1) 0) [i:=n]"
by auto
have nxs: "n \<in> set xs"
unfolding xs
@@ -2292,7 +2292,7 @@
unfolding sum_list_sum_nth xsl ..
also have "\<dots> = sum (\<lambda>j. if j = i then n else 0) {0..< k+1}"
by (rule sum.cong) (simp_all add: xs del: replicate.simps)
-    also have "\<dots> = n" using i by (simp add: sum.delta)
+    also have "\<dots> = n" using i by (simp)
finally have "xs \<in> natpermute n (k + 1)"
using xsl unfolding natpermute_def mem_Collect_eq by blast
then show "xs \<in> ?A"
@@ -2395,32 +2395,32 @@
shows "card {xs \<in> natpermute n (k + 1). n \<in> set xs} = k + 1"
unfolding natpermute_contain_maximal
proof -
-  let ?A = "\<lambda>i. {replicate (k + 1) 0[i := n]}"
+  let ?A = "\<lambda>i. {(replicate (k + 1) 0)[i := n]}"
let ?K = "{0 ..k}"
have fK: "finite ?K"
by simp
have fAK: "\<forall>i\<in>?K. finite (?A i)"
by auto
have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow>
-    {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
+    {(replicate (k + 1) 0)[i := n]} \<inter> {(replicate (k + 1) 0)[j := n]} = {}"
proof clarify
fix i j
assume i: "i \<in> ?K" and j: "j \<in> ?K" and ij: "i \<noteq> j"
-    have False if eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
+    have False if eq: "(replicate (k+1) 0)[i:=n] = (replicate (k+1) 0)[j:= n]"
proof -
-      have "(replicate (k+1) 0 [i:=n] ! i) = n"
+      have "(replicate (k+1) 0) [i:=n] ! i = n"
using i by (simp del: replicate.simps)
moreover
-      have "(replicate (k+1) 0 [j:=n] ! i) = 0"
+      have "(replicate (k+1) 0) [j:=n] ! i = 0"
using i ij by (simp del: replicate.simps)
ultimately show ?thesis
using eq n0 by (simp del: replicate.simps)
qed
-    then show "{replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
+    then show "{(replicate (k + 1) 0)[i := n]} \<inter> {(replicate (k + 1) 0)[j := n]} = {}"
by auto
qed
from card_UN_disjoint[OF fK fAK d]
-  show "card (\<Union>i\<in>{0..k}. {replicate (k + 1) 0[i := n]}) = k + 1"
+  show "card (\<Union>i\<in>{0..k}. {(replicate (k + 1) 0)[i := n]}) = k + 1"
by simp
qed

@@ -2712,7 +2712,7 @@
fix v assume v: "v \<in> {xs \<in> natpermute n (k + 1). n \<in> set xs}"
let ?ths = "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a \$ v ! j) =
fps_radical r (Suc k) a \$ n * r (Suc k) (a \$ 0) ^ k"
-          from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]"
+          from v obtain i where i: "i \<in> {0..k}" "v = (replicate (k+1) 0) [i:= n]"
unfolding natpermute_contain_maximal by auto
have "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a \$ v ! j) =
(\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a \$ n else r (Suc k) (a\$0))"
@@ -2847,7 +2847,7 @@
fix v
assume v: "v \<in> {xs \<in> natpermute n (Suc k). n \<in> set xs}"
let ?ths = "(\<Prod>j\<in>{0..k}. a \$ v ! j) = a \$ n * (?r\$0)^k"
-          from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]"
+          from v obtain i where i: "i \<in> {0..k}" "v = (replicate (k+1) 0) [i:= n]"
unfolding Suc_eq_plus1 natpermute_contain_maximal
by (auto simp del: replicate.simps)
have "(\<Prod>j\<in>{0..k}. a \$ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then a \$ n else r (Suc k) (b\$0))"```
```--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sun Sep 30 07:46:38 2018 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sun Sep 30 09:00:11 2018 +0200
@@ -130,7 +130,7 @@
assumes "cl \<in> array_ran a (Array.update a i (Some b) h)"
shows "cl \<in> array_ran a h \<or> cl = b"
proof -
-  have "set (Array.get h a[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert)
+  have "set ((Array.get h a)[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert)
with assms show ?thesis
unfolding array_ran_def Array.update_def by fastforce
qed
@@ -139,7 +139,7 @@
assumes "cl \<in> array_ran a (Array.update a i None h)"
shows "cl \<in> array_ran a h"
proof -
-  have "set (Array.get h a[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert)
+  have "set ((Array.get h a)[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert)
with assms show ?thesis
unfolding array_ran_def Array.update_def by auto
qed```
```--- a/src/HOL/Imperative_HOL/ex/Subarray.thy	Sun Sep 30 07:46:38 2018 +0200
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Sun Sep 30 09:00:11 2018 +0200
@@ -23,7 +23,7 @@
apply simp
done

-lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h[i - n := v]"
+lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.update a i v h) = (subarray n m a h)[i - n := v]"
unfolding subarray_def Array.update_def
```
```--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Sep 30 07:46:38 2018 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Sep 30 09:00:11 2018 +0200
@@ -174,7 +174,7 @@
\<lbrakk> G \<turnstile> T \<preceq> T'; is_type G T'; length pns = length pTs; distinct pns; unique lvars;
snd (local_env G C (mn, pTs) pns lvars) vname = Some T' \<rbrakk>
\<Longrightarrow>
-  comp G \<turnstile> inited_LT C pTs lvars [index (pns, lvars, blk, res) vname := OK T] <=l
+  comp G \<turnstile> (inited_LT C pTs lvars) [index (pns, lvars, blk, res) vname := OK T] <=l
inited_LT C pTs lvars"
apply (subgoal_tac " index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)")
apply (frule_tac blk=blk and res=res in local_env_inited_LT, assumption+)```
```--- a/src/HOL/MicroJava/Comp/Index.thy	Sun Sep 30 07:46:38 2018 +0200
+++ b/src/HOL/MicroJava/Comp/Index.thy	Sun Sep 30 09:00:11 2018 +0200
@@ -70,7 +70,7 @@
lemma update_at_index: "
\<lbrakk> distinct (gjmb_plns (gmb G C S));
x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow>
-  locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] =
+  (locvars_xstate G C S (Norm (h, l)))[index (gmb G C S) x := val] =
locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))"
apply (simp only: locvars_xstate_def locvars_locals_def index_def)
apply (case_tac "gmb G C S" rule: prod.exhaust, simp)```