# HG changeset patch
# User nipkow
# Date 1538290811 -7200
# Node ID 9999d7823b8fe3671537870f9d72554cbf1e7425
# Parent  c7c38c901267c022b93cdb50235a593d24beeaf0
updated to new list_update precedence

diff -r c7c38c901267 -r 9999d7823b8f src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- 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 @@
       by (simp add: natpermute_def)
     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))"
diff -r c7c38c901267 -r 9999d7823b8f src/HOL/Imperative_HOL/ex/SatChecker.thy
--- 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
diff -r c7c38c901267 -r 9999d7823b8f src/HOL/Imperative_HOL/ex/Subarray.thy
--- 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
 by (simp add: nths'_update3)
 
diff -r c7c38c901267 -r 9999d7823b8f src/HOL/MicroJava/Comp/CorrCompTp.thy
--- 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+)
diff -r c7c38c901267 -r 9999d7823b8f src/HOL/MicroJava/Comp/Index.thy
--- 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)