# HG changeset patch
# User nipkow
# Date 1103711793 -3600
# Node ID 6356d2523f73d0271e131a2e794eeb7379a52f27
# Parent  7a91490c1b04db1bcf50b0a6fe3af9311e2776bd
[ .. (] -> [ ..< ]

diff -r 7a91490c1b04 -r 6356d2523f73 src/HOL/HoareParallel/OG_Syntax.thy
--- a/src/HOL/HoareParallel/OG_Syntax.thy	Mon Dec 20 18:25:22 2004 +0100
+++ b/src/HOL/HoareParallel/OG_Syntax.thy	Wed Dec 22 11:36:33 2004 +0100
@@ -1,5 +1,6 @@
-
-theory OG_Syntax = OG_Tactics + Quote_Antiquote:
+theory OG_Syntax
+imports OG_Tactics Quote_Antiquote
+begin
 
 text{* Syntax for commands and for assertions and boolean expressions in 
  commands @{text com} and annotated commands @{text ann_com}. *}
@@ -71,7 +72,7 @@
   "_prgs c q ps" \<rightleftharpoons> "(Some c, q) # ps"
   "_PAR ps" \<rightleftharpoons> "Parallel ps"
 
-  "_prg_scheme j i k c q" \<rightleftharpoons> "(map (\<lambda>i. (Some c, q)) [j..k(])"
+  "_prg_scheme j i k c q" \<rightleftharpoons> "map (\<lambda>i. (Some c, q)) [j..<k]"
 
 print_translation {*
   let
diff -r 7a91490c1b04 -r 6356d2523f73 src/HOL/HoareParallel/OG_Tactics.thy
--- a/src/HOL/HoareParallel/OG_Tactics.thy	Mon Dec 20 18:25:22 2004 +0100
+++ b/src/HOL/HoareParallel/OG_Tactics.thy	Wed Dec 22 11:36:33 2004 +0100
@@ -1,7 +1,7 @@
-
 header {* \section{Generation of Verification Conditions} *}
 
-theory OG_Tactics = OG_Hoare:
+theory OG_Tactics imports OG_Hoare
+begin
 
 lemmas ann_hoare_intros=AnnBasic AnnSeq AnnCond1 AnnCond2 AnnWhile AnnAwait AnnConseq
 lemmas oghoare_intros=Parallel Basic Seq Cond While Conseq
@@ -186,7 +186,7 @@
 
 lemma interfree_swap_Map: "\<forall>k. i\<le>k \<and> k<j \<longrightarrow> interfree_aux (com x, post x, c k) 
  \<and> interfree_aux (c k, Q k, com x)   
- \<Longrightarrow> interfree_swap (x, map (\<lambda>k. (c k, Q k)) [i..j(])"
+ \<Longrightarrow> interfree_swap (x, map (\<lambda>k. (c k, Q k)) [i..<j])"
 by(force simp add: interfree_swap_def less_diff_conv)
 
 lemma interfree_Empty: "interfree []"
@@ -204,7 +204,7 @@
 
 lemma interfree_Map: 
   "(\<forall>i j. a\<le>i \<and> i<b \<and> a\<le>j \<and> j<b  \<and> i\<noteq>j \<longrightarrow> interfree_aux (c i, Q i, c j))  
-  \<Longrightarrow> interfree (map (\<lambda>k. (c k, Q k)) [a..b(])"
+  \<Longrightarrow> interfree (map (\<lambda>k. (c k, Q k)) [a..<b])"
 by(force simp add: interfree_def less_diff_conv)
 
 constdefs map_ann_hoare :: "(('a ann_com_op * 'a assn) list) \<Rightarrow> bool " ("[\<turnstile>] _" [0] 45)
@@ -220,7 +220,7 @@
 done
 
 lemma MapAnnMap: 
-  "\<forall>k. i\<le>k \<and> k<j \<longrightarrow> \<turnstile> (c k) (Q k) \<Longrightarrow> [\<turnstile>] map (\<lambda>k. (Some (c k), Q k)) [i..j(]"
+  "\<forall>k. i\<le>k \<and> k<j \<longrightarrow> \<turnstile> (c k) (Q k) \<Longrightarrow> [\<turnstile>] map (\<lambda>k. (Some (c k), Q k)) [i..<j]"
 apply(simp add: map_ann_hoare_def less_diff_conv)
 done
 
diff -r 7a91490c1b04 -r 6356d2523f73 src/HOL/HoareParallel/RG_Syntax.thy
--- a/src/HOL/HoareParallel/RG_Syntax.thy	Mon Dec 20 18:25:22 2004 +0100
+++ b/src/HOL/HoareParallel/RG_Syntax.thy	Wed Dec 22 11:36:33 2004 +0100
@@ -1,7 +1,8 @@
-
 header {* \section{Concrete Syntax} *}
 
-theory RG_Syntax = RG_Hoare + Quote_Antiquote:
+theory RG_Syntax
+imports RG_Hoare Quote_Antiquote
+begin
 
 syntax
   "_Assign"    :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"                     ("(\<acute>_ :=/ _)" [70, 65] 61)
@@ -42,7 +43,7 @@
   "_prg_scheme" :: "['a, 'a, 'a, 'a] \<Rightarrow> prgs"  ("SCHEME [_ \<le> _ < _] _" [0,0,0,60] 57)
 
 translations
-  "_prg_scheme j i k c" \<rightleftharpoons> "(map (\<lambda>i. c) [j..k(])"
+  "_prg_scheme j i k c" \<rightleftharpoons> "(map (\<lambda>i. c) [j..<k])"
 
 text {* Translations for variables before and after a transition: *}
 
diff -r 7a91490c1b04 -r 6356d2523f73 src/HOL/HoareParallel/RG_Tran.thy
--- a/src/HOL/HoareParallel/RG_Tran.thy	Mon Dec 20 18:25:22 2004 +0100
+++ b/src/HOL/HoareParallel/RG_Tran.thy	Wed Dec 22 11:36:33 2004 +0100
@@ -1,6 +1,8 @@
 header {* \section{Operational Semantics} *}
 
-theory RG_Tran = RG_Com:
+theory RG_Tran
+imports RG_Com
+begin
 
 subsection {* Semantics of Component Programs *}
 
@@ -770,7 +772,7 @@
   (\<forall>i<length xs. (xs!i,s)#(clist!i) \<in> cptn))"
 apply(induct ys)
  apply(clarify)
- apply(rule_tac x="map (\<lambda>i. []) [0..length xs(]" in exI)
+ apply(rule_tac x="map (\<lambda>i. []) [0..<length xs]" in exI)
  apply(simp add: conjoin_def same_length_def same_state_def same_program_def compat_label_def)
  apply(rule conjI)
   apply(rule nth_equalityI,simp,simp)
@@ -781,7 +783,7 @@
  apply(erule_tac x="xs" in allE)
  apply(erule_tac x="t" in allE,simp)
  apply clarify
- apply(rule_tac x="(map (\<lambda>j. (P!j, t)#(clist!j)) [0..length P(])" in exI,simp)
+ apply(rule_tac x="(map (\<lambda>j. (P!j, t)#(clist!j)) [0..<length P])" in exI,simp)
  apply(rule conjI)
   prefer 2
   apply clarify
@@ -813,7 +815,7 @@
 apply(erule_tac x="Ps[i:=r]" in allE)
 apply(erule_tac x="ta" in allE,simp)
 apply clarify
-apply(rule_tac x="(map (\<lambda>j. (Ps!j, ta)#(clist!j)) [0..length Ps(]) [i:=((r, ta)#(clist!i))]" in exI,simp)
+apply(rule_tac x="(map (\<lambda>j. (Ps!j, ta)#(clist!j)) [0..<length Ps]) [i:=((r, ta)#(clist!i))]" in exI,simp)
 apply(rule conjI)
  prefer 2
  apply clarify
diff -r 7a91490c1b04 -r 6356d2523f73 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Dec 20 18:25:22 2004 +0100
+++ b/src/HOL/List.thy	Wed Dec 22 11:36:33 2004 +0100
@@ -38,7 +38,7 @@
   dropWhile :: "('a => bool) => 'a list => 'a list"
   rev :: "'a list => 'a list"
   zip :: "'a list => 'b list => ('a * 'b) list"
-  upt :: "nat => nat => nat list" ("(1[_../_'(])")
+  upt :: "nat => nat => nat list" ("(1[_..</_'])")
   remdups :: "'a list => 'a list"
   remove1 :: "'a => 'a list => 'a list"
   null:: "'a list => bool"
@@ -74,7 +74,7 @@
   "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
   "xs[i:=x]" == "list_update xs i x"
 
-  "[i..j]" == "[i..(Suc j)(]"
+  "[i..j]" == "[i..<(Suc j)]"
 
 
 syntax (xsymbols)
@@ -193,8 +193,8 @@
        theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
 
 primrec
-  upt_0: "[i..0(] = []"
-  upt_Suc: "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
+  upt_0: "[i..<0] = []"
+  upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
 
 primrec
   "distinct [] = True"
@@ -221,7 +221,7 @@
   length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)"
 
 sublist_def:
- "sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..size xs(]))"
+ "sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..<size xs]))"
 
 
 lemma not_Cons_self [simp]: "xs \<noteq> x # xs"
@@ -619,7 +619,7 @@
 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
 by (induct xs) auto
 
-lemma set_upt [simp]: "set[i..j(] = {k. i \<le> k \<and> k < j}"
+lemma set_upt [simp]: "set[i..<j] = {k. i \<le> k \<and> k < j}"
 apply (induct j, simp_all)
 apply (erule ssubst, auto)
 done
@@ -1365,47 +1365,47 @@
 
 subsubsection {* @{text upto} *}
 
-lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])"
+lemma upt_rec: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
 -- {* Does not terminate! *}
 by (induct j) auto
 
-lemma upt_conv_Nil [simp]: "j <= i ==> [i..j(] = []"
+lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
 by (subst upt_rec) simp
 
-lemma upt_eq_Nil_conv[simp]: "([i..j(] = []) = (j = 0 \<or> j <= i)"
+lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
 by(induct j)simp_all
 
 lemma upt_eq_Cons_conv:
- "!!x xs. ([i..j(] = x#xs) = (i < j & i = x & [i+1..j(] = xs)"
+ "!!x xs. ([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
 apply(induct j)
  apply simp
 apply(clarsimp simp add: append_eq_Cons_conv)
 apply arith
 done
 
-lemma upt_Suc_append: "i <= j ==> [i..(Suc j)(] = [i..j(]@[j]"
+lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
 -- {* Only needed if @{text upt_Suc} is deleted from the simpset. *}
 by simp
 
-lemma upt_conv_Cons: "i < j ==> [i..j(] = i # [Suc i..j(]"
+lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
 apply(rule trans)
 apply(subst upt_rec)
  prefer 2 apply (rule refl, simp)
 done
 
-lemma upt_add_eq_append: "i<=j ==> [i..j+k(] = [i..j(]@[j..j+k(]"
+lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
 -- {* LOOPS as a simprule, since @{text "j <= j"}. *}
 by (induct k) auto
 
-lemma length_upt [simp]: "length [i..j(] = j - i"
+lemma length_upt [simp]: "length [i..<j] = j - i"
 by (induct j) (auto simp add: Suc_diff_le)
 
-lemma nth_upt [simp]: "i + k < j ==> [i..j(] ! k = i + k"
+lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
 apply (induct j)
 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
 done
 
-lemma take_upt [simp]: "!!i. i+m <= n ==> take m [i..n(] = [i..i+m(]"
+lemma take_upt [simp]: "!!i. i+m <= n ==> take m [i..<n] = [i..<i+m]"
 apply (induct m, simp)
 apply (subst upt_rec)
 apply (rule sym)
@@ -1413,10 +1413,10 @@
 apply (simp del: upt.simps)
 done
 
-lemma map_Suc_upt: "map Suc [m..n(] = [Suc m..n]"
+lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..n]"
 by (induct n) auto
 
-lemma nth_map_upt: "!!i. i < n-m ==> (map f [m..n(]) ! i = f(m+i)"
+lemma nth_map_upt: "!!i. i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
 apply (induct n m rule: diff_induct)
 prefer 3 apply (subst map_Suc_upt[symmetric])
 apply (auto simp add: less_diff_conv nth_upt)
@@ -1745,8 +1745,8 @@
 done
 
 lemma sublist_shift_lemma:
-     "map fst [p:zip xs [i..i + length xs(] . snd p : A] =
-      map fst [p:zip xs [0..length xs(] . snd p + i : A]"
+     "map fst [p:zip xs [i..<i + length xs] . snd p : A] =
+      map fst [p:zip xs [0..<length xs] . snd p + i : A]"
 by (induct xs rule: rev_induct) (simp_all add: add_commute)
 
 lemma sublist_append:
diff -r 7a91490c1b04 -r 6356d2523f73 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Mon Dec 20 18:25:22 2004 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Dec 22 11:36:33 2004 +0100
@@ -15,7 +15,7 @@
 
   make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate"
   "make_cert step phi B \<equiv> 
-     map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..length phi(] @ [B]"
+     map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"
 
 constdefs
   list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
@@ -26,7 +26,7 @@
 
 lemma [code]:
   "is_target step phi pc' =
-  list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..length phi(]"
+  list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]"
   apply (simp add: list_ex_def is_target_def set_mem_eq)
   apply force
   done
diff -r 7a91490c1b04 -r 6356d2523f73 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Mon Dec 20 18:25:22 2004 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Dec 22 11:36:33 2004 +0100
@@ -15,7 +15,7 @@
   fixes phi :: "'a list" ("\<phi>")
   defines phi_def:
   "\<phi> \<equiv> map (\<lambda>pc. if c!pc = \<bottom> then wtl (take pc ins) c 0 s0 else c!pc) 
-       [0..length ins(]"
+       [0..<length ins]"
 
   assumes bounded: "bounded step (length ins)"
   assumes cert: "cert_ok c (length ins) \<top> \<bottom> A"
diff -r 7a91490c1b04 -r 6356d2523f73 src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Mon Dec 20 18:25:22 2004 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Wed Dec 22 11:36:33 2004 +0100
@@ -22,7 +22,7 @@
 "map_snd f \<equiv> map (\<lambda>(x,y). (x, f y))"
 
 error :: "nat \<Rightarrow> (nat \<times> 'a err) list"
-"error n \<equiv> map (\<lambda>x. (x,Err)) [0..n(]"
+"error n \<equiv> map (\<lambda>x. (x,Err)) [0..<n]"
 
 err_step :: "nat \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's err step_type"
 "err_step n app step p t \<equiv>