[ .. (] -> [ ..< ]
--- 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
--- 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
--- 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: *}
--- 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
--- 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:
--- 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
--- 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"
--- 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>