--- a/Admin/isatest/crontab.macbroy28 Tue Jul 13 11:26:16 2010 +0100
+++ b/Admin/isatest/crontab.macbroy28 Tue Jul 13 11:27:19 2010 +0100
@@ -1,5 +1,6 @@
-17 10 * * 1-6 $HOME/afp/devel/admin/regression -
-32 12 * * 0 $HOME/afp/release/admin/regression Isabelle2009-2
+# now on macbroy2:
+#17 10 * * 1-6 $HOME/afp/devel/admin/regression -
+#32 12 * * 0 $HOME/afp/release/admin/regression Isabelle2009-2
03 00 * * * $HOME/bin/checkout-admin
17 00 * * * $HOME/bin/isatest-makedist
@@ -9,4 +10,3 @@
04 23 31 1,3,5,7,8,10,12 * $HOME/bin/logmove
04 23 30 4,6,9,11 * $HOME/bin/logmove
04 23 28 2 * $HOME/bin/logmove
-
--- a/src/HOL/Extraction/Higman.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Extraction/Higman.thy Tue Jul 13 11:27:19 2010 +0100
@@ -350,15 +350,14 @@
end
function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
- "mk_word_aux k = (do
+ "mk_word_aux k = (do {
i \<leftarrow> Random.range 10;
(if i > 7 \<and> k > 2 \<or> k > 1000 then return []
- else do
+ else do {
let l = (if i mod 2 = 0 then A else B);
ls \<leftarrow> mk_word_aux (Suc k);
return (l # ls)
- done)
- done)"
+ })})"
by pat_completeness auto
termination by (relation "measure ((op -) 1001)") auto
@@ -367,10 +366,10 @@
primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
"mk_word_s 0 = mk_word"
- | "mk_word_s (Suc n) = (do
+ | "mk_word_s (Suc n) = (do {
_ \<leftarrow> mk_word;
mk_word_s n
- done)"
+ })"
definition g1 :: "nat \<Rightarrow> letter list" where
"g1 s = fst (mk_word_s s (20000, 1))"
--- a/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 11:27:19 2010 +0100
@@ -35,9 +35,8 @@
length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
"length a h = List.length (get_array a h)"
-definition (*FIXME update*)
- change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
- "change a i x h = set_array a ((get_array a h)[i:=x]) h"
+definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
+ "update a i x h = set_array a ((get_array a h)[i:=x]) h"
definition (*FIXME noteq*)
noteq_arrs :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where
@@ -64,15 +63,15 @@
definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where
[code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
- (\<lambda>h. (a, change a i x h))"
+ (\<lambda>h. (a, update a i x h))"
definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where
[code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length a h)
- (\<lambda>h. (a, change a i (f (get_array a h ! i)) h))"
+ (\<lambda>h. (a, update a i (f (get_array a h ! i)) h))"
definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where
[code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
- (\<lambda>h. (get_array a h ! i, change a i x h))"
+ (\<lambda>h. (get_array a h ! i, update a i x h))"
definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
[code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
@@ -109,27 +108,27 @@
"r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
-lemma get_array_change_eq [simp]:
- "get_array a (change a i v h) = (get_array a h) [i := v]"
- by (simp add: change_def)
+lemma get_array_update_eq [simp]:
+ "get_array a (update a i v h) = (get_array a h) [i := v]"
+ by (simp add: update_def)
-lemma nth_change_array_neq_array [simp]:
- "a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i"
- by (simp add: change_def noteq_arrs_def)
+lemma nth_update_array_neq_array [simp]:
+ "a =!!= b \<Longrightarrow> get_array a (update b j v h) ! i = get_array a h ! i"
+ by (simp add: update_def noteq_arrs_def)
-lemma get_arry_array_change_elem_neqIndex [simp]:
- "i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i"
+lemma get_arry_array_update_elem_neqIndex [simp]:
+ "i \<noteq> j \<Longrightarrow> get_array a (update a j v h) ! i = get_array a h ! i"
by simp
-lemma length_change [simp]:
- "length a (change b i v h) = length a h"
- by (simp add: change_def length_def set_array_def get_array_def)
+lemma length_update [simp]:
+ "length a (update b i v h) = length a h"
+ by (simp add: update_def length_def set_array_def get_array_def)
-lemma change_swap_neqArray:
+lemma update_swap_neqArray:
"a =!!= a' \<Longrightarrow>
- change a i v (change a' i' v' h)
- = change a' i' v' (change a i v h)"
-apply (unfold change_def)
+ update a i v (update a' i' v' h)
+ = update a' i' v' (update a i v h)"
+apply (unfold update_def)
apply simp
apply (subst array_set_set_swap, assumption)
apply (subst array_get_set_neq)
@@ -137,9 +136,9 @@
apply (simp)
done
-lemma change_swap_neqIndex:
- "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)"
- by (auto simp add: change_def array_set_set_swap list_update_swap)
+lemma update_swap_neqIndex:
+ "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)"
+ by (auto simp add: update_def array_set_set_swap list_update_swap)
lemma get_array_init_array_list:
"get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
@@ -151,9 +150,9 @@
= snd (array new_ls h)"
by (simp add: Let_def split_def array_def)
-lemma array_present_change [simp]:
- "array_present a (change b i v h) = array_present a h"
- by (simp add: change_def array_present_def set_array_def get_array_def)
+lemma array_present_update [simp]:
+ "array_present a (update b i v h) = array_present a h"
+ by (simp add: update_def array_present_def set_array_def get_array_def)
lemma array_present_array [simp]:
"array_present (fst (array xs h)) (snd (array xs h))"
@@ -166,80 +165,80 @@
text {* Monad operations *}
-lemma execute_new [simp, execute_simps]:
+lemma execute_new [execute_simps]:
"execute (new n x) h = Some (array (replicate n x) h)"
- by (simp add: new_def)
+ by (simp add: new_def execute_simps)
-lemma success_newI [iff, success_intros]:
+lemma success_newI [success_intros]:
"success (new n x) h"
- by (simp add: new_def)
+ by (auto intro: success_intros simp add: new_def)
lemma crel_newI [crel_intros]:
assumes "(a, h') = array (replicate n x) h"
shows "crel (new n x) h h' a"
- by (rule crelI) (simp add: assms)
+ by (rule crelI) (simp add: assms execute_simps)
lemma crel_newE [crel_elims]:
assumes "crel (new n x) h h' r"
obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)"
"get_array r h' = replicate n x" "array_present r h'" "\<not> array_present r h"
- using assms by (rule crelE) (simp add: get_array_init_array_list)
+ using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
-lemma execute_of_list [simp, execute_simps]:
+lemma execute_of_list [execute_simps]:
"execute (of_list xs) h = Some (array xs h)"
- by (simp add: of_list_def)
+ by (simp add: of_list_def execute_simps)
-lemma success_of_listI [iff, success_intros]:
+lemma success_of_listI [success_intros]:
"success (of_list xs) h"
- by (simp add: of_list_def)
+ by (auto intro: success_intros simp add: of_list_def)
lemma crel_of_listI [crel_intros]:
assumes "(a, h') = array xs h"
shows "crel (of_list xs) h h' a"
- by (rule crelI) (simp add: assms)
+ by (rule crelI) (simp add: assms execute_simps)
lemma crel_of_listE [crel_elims]:
assumes "crel (of_list xs) h h' r"
obtains "r = fst (array xs h)" "h' = snd (array xs h)"
"get_array r h' = xs" "array_present r h'" "\<not> array_present r h"
- using assms by (rule crelE) (simp add: get_array_init_array_list)
+ using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
-lemma execute_make [simp, execute_simps]:
+lemma execute_make [execute_simps]:
"execute (make n f) h = Some (array (map f [0 ..< n]) h)"
- by (simp add: make_def)
+ by (simp add: make_def execute_simps)
-lemma success_makeI [iff, success_intros]:
+lemma success_makeI [success_intros]:
"success (make n f) h"
- by (simp add: make_def)
+ by (auto intro: success_intros simp add: make_def)
lemma crel_makeI [crel_intros]:
assumes "(a, h') = array (map f [0 ..< n]) h"
shows "crel (make n f) h h' a"
- by (rule crelI) (simp add: assms)
+ by (rule crelI) (simp add: assms execute_simps)
lemma crel_makeE [crel_elims]:
assumes "crel (make n f) h h' r"
obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)"
"get_array r h' = map f [0 ..< n]" "array_present r h'" "\<not> array_present r h"
- using assms by (rule crelE) (simp add: get_array_init_array_list)
+ using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
-lemma execute_len [simp, execute_simps]:
+lemma execute_len [execute_simps]:
"execute (len a) h = Some (length a h, h)"
- by (simp add: len_def)
+ by (simp add: len_def execute_simps)
-lemma success_lenI [iff, success_intros]:
+lemma success_lenI [success_intros]:
"success (len a) h"
- by (simp add: len_def)
+ by (auto intro: success_intros simp add: len_def)
lemma crel_lengthI [crel_intros]:
assumes "h' = h" "r = length a h"
shows "crel (len a) h h' r"
- by (rule crelI) (simp add: assms)
+ by (rule crelI) (simp add: assms execute_simps)
lemma crel_lengthE [crel_elims]:
assumes "crel (len a) h h' r"
obtains "r = length a h'" "h' = h"
- using assms by (rule crelE) simp
+ using assms by (rule crelE) (simp add: execute_simps)
lemma execute_nth [execute_simps]:
"i < length a h \<Longrightarrow>
@@ -264,7 +263,7 @@
lemma execute_upd [execute_simps]:
"i < length a h \<Longrightarrow>
- execute (upd i x a) h = Some (a, change a i x h)"
+ execute (upd i x a) h = Some (a, update a i x h)"
"i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None"
by (simp_all add: upd_def execute_simps)
@@ -273,20 +272,20 @@
by (auto intro: success_intros simp add: upd_def)
lemma crel_updI [crel_intros]:
- assumes "i < length a h" "h' = change a i v h"
+ assumes "i < length a h" "h' = update a i v h"
shows "crel (upd i v a) h h' a"
by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_updE [crel_elims]:
assumes "crel (upd i v a) h h' r"
- obtains "r = a" "h' = change a i v h" "i < length a h"
+ obtains "r = a" "h' = update a i v h" "i < length a h"
using assms by (rule crelE)
(erule successE, cases "i < length a h", simp_all add: execute_simps)
lemma execute_map_entry [execute_simps]:
"i < length a h \<Longrightarrow>
execute (map_entry i f a) h =
- Some (a, change a i (f (get_array a h ! i)) h)"
+ Some (a, update a i (f (get_array a h ! i)) h)"
"i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None"
by (simp_all add: map_entry_def execute_simps)
@@ -295,20 +294,20 @@
by (auto intro: success_intros simp add: map_entry_def)
lemma crel_map_entryI [crel_intros]:
- assumes "i < length a h" "h' = change a i (f (get_array a h ! i)) h" "r = a"
+ assumes "i < length a h" "h' = update a i (f (get_array a h ! i)) h" "r = a"
shows "crel (map_entry i f a) h h' r"
by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_map_entryE [crel_elims]:
assumes "crel (map_entry i f a) h h' r"
- obtains "r = a" "h' = change a i (f (get_array a h ! i)) h" "i < length a h"
+ obtains "r = a" "h' = update a i (f (get_array a h ! i)) h" "i < length a h"
using assms by (rule crelE)
(erule successE, cases "i < length a h", simp_all add: execute_simps)
lemma execute_swap [execute_simps]:
"i < length a h \<Longrightarrow>
execute (swap i x a) h =
- Some (get_array a h ! i, change a i x h)"
+ Some (get_array a h ! i, update a i x h)"
"i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None"
by (simp_all add: swap_def execute_simps)
@@ -317,23 +316,23 @@
by (auto intro: success_intros simp add: swap_def)
lemma crel_swapI [crel_intros]:
- assumes "i < length a h" "h' = change a i x h" "r = get_array a h ! i"
+ assumes "i < length a h" "h' = update a i x h" "r = get_array a h ! i"
shows "crel (swap i x a) h h' r"
by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_swapE [crel_elims]:
assumes "crel (swap i x a) h h' r"
- obtains "r = get_array a h ! i" "h' = change a i x h" "i < length a h"
+ obtains "r = get_array a h ! i" "h' = update a i x h" "i < length a h"
using assms by (rule crelE)
(erule successE, cases "i < length a h", simp_all add: execute_simps)
-lemma execute_freeze [simp, execute_simps]:
+lemma execute_freeze [execute_simps]:
"execute (freeze a) h = Some (get_array a h, h)"
- by (simp add: freeze_def)
+ by (simp add: freeze_def execute_simps)
-lemma success_freezeI [iff, success_intros]:
+lemma success_freezeI [success_intros]:
"success (freeze a) h"
- by (simp add: freeze_def)
+ by (auto intro: success_intros simp add: freeze_def)
lemma crel_freezeI [crel_intros]:
assumes "h' = h" "r = get_array a h"
@@ -343,21 +342,21 @@
lemma crel_freezeE [crel_elims]:
assumes "crel (freeze a) h h' r"
obtains "h' = h" "r = get_array a h"
- using assms by (rule crelE) simp
+ using assms by (rule crelE) (simp add: execute_simps)
lemma upd_return:
"upd i x a \<guillemotright> return a = upd i x a"
- by (rule Heap_eqI) (simp add: bind_def guard_def upd_def)
+ by (rule Heap_eqI) (simp add: bind_def guard_def upd_def execute_simps)
lemma array_make:
"new n x = make n (\<lambda>_. x)"
- by (rule Heap_eqI) (simp add: map_replicate_trivial)
+ by (rule Heap_eqI) (simp add: map_replicate_trivial execute_simps)
lemma array_of_list_make:
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
- by (rule Heap_eqI) (simp add: map_nth)
+ by (rule Heap_eqI) (simp add: map_nth execute_simps)
-hide_const (open) new
+hide_const (open) update new of_list make len nth upd map_entry swap freeze
subsection {* Code generator setup *}
@@ -407,25 +406,25 @@
by (simp add: upd'_def upd_return)
lemma [code]:
- "map_entry i f a = (do
- x \<leftarrow> nth a i;
- upd i (f x) a
- done)"
+ "Array.map_entry i f a = do {
+ x \<leftarrow> Array.nth a i;
+ Array.upd i (f x) a
+ }"
by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps)
lemma [code]:
- "swap i x a = (do
- y \<leftarrow> nth a i;
- upd i x a;
+ "Array.swap i x a = do {
+ y \<leftarrow> Array.nth a i;
+ Array.upd i x a;
return y
- done)"
+ }"
by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps)
lemma [code]:
- "freeze a = (do
- n \<leftarrow> len a;
- Heap_Monad.fold_map (\<lambda>i. nth a i) [0..<n]
- done)"
+ "Array.freeze a = do {
+ n \<leftarrow> Array.len a;
+ Heap_Monad.fold_map (\<lambda>i. Array.nth a i) [0..<n]
+ }"
proof (rule Heap_eqI)
fix h
have *: "List.map
@@ -440,15 +439,15 @@
apply (simp_all add: nth_def guard_def *)
apply (simp add: length_def map_nth)
done
- then have "execute (do
- n \<leftarrow> len a;
+ then have "execute (do {
+ n \<leftarrow> Array.len a;
Heap_Monad.fold_map (Array.nth a) [0..<n]
- done) h = Some (get_array a h, h)"
- by (auto intro: execute_bind_eq_SomeI)
- then show "execute (freeze a) h = execute (do
- n \<leftarrow> len a;
+ }) h = Some (get_array a h, h)"
+ by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
+ then show "execute (Array.freeze a) h = execute (do {
+ n \<leftarrow> Array.len a;
Heap_Monad.fold_map (Array.nth a) [0..<n]
- done) h" by simp
+ }) h" by (simp add: execute_simps)
qed
hide_const (open) new' of_list' make' len' nth' upd'
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 13 11:27:19 2010 +0100
@@ -1,11 +1,11 @@
-(* Title: HOL/Library/Heap_Monad.thy
+(* Title: HOL/Imperative_HOL/Heap_Monad.thy
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)
header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
theory Heap_Monad
-imports Heap
+imports Heap Monad_Syntax
begin
subsection {* The monad *}
@@ -40,7 +40,7 @@
setup Execute_Simps.setup
-lemma execute_Let [simp, execute_simps]:
+lemma execute_Let [execute_simps]:
"execute (let x = t in f x) = (let x = t in execute (f x))"
by (simp add: Let_def)
@@ -50,14 +50,14 @@
definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
[code del]: "tap f = Heap (\<lambda>h. Some (f h, h))"
-lemma execute_tap [simp, execute_simps]:
+lemma execute_tap [execute_simps]:
"execute (tap f) h = Some (f h, h)"
by (simp add: tap_def)
definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
[code del]: "heap f = Heap (Some \<circ> f)"
-lemma execute_heap [simp, execute_simps]:
+lemma execute_heap [execute_simps]:
"execute (heap f) = Some \<circ> f"
by (simp add: heap_def)
@@ -93,13 +93,13 @@
setup Success_Intros.setup
-lemma success_tapI [iff, success_intros]:
+lemma success_tapI [success_intros]:
"success (tap f) h"
- by (rule successI) simp
+ by (rule successI) (simp add: execute_simps)
-lemma success_heapI [iff, success_intros]:
+lemma success_heapI [success_intros]:
"success (heap f) h"
- by (rule successI) simp
+ by (rule successI) (simp add: execute_simps)
lemma success_guardI [success_intros]:
"P h \<Longrightarrow> success (guard P f) h"
@@ -196,22 +196,22 @@
lemma crel_tapI [crel_intros]:
assumes "h' = h" "r = f h"
shows "crel (tap f) h h' r"
- by (rule crelI) (simp add: assms)
+ by (rule crelI) (simp add: assms execute_simps)
lemma crel_tapE [crel_elims]:
assumes "crel (tap f) h h' r"
obtains "h' = h" and "r = f h"
- using assms by (rule crelE) auto
+ using assms by (rule crelE) (auto simp add: execute_simps)
lemma crel_heapI [crel_intros]:
assumes "h' = snd (f h)" "r = fst (f h)"
shows "crel (heap f) h h' r"
- by (rule crelI) (simp add: assms)
+ by (rule crelI) (simp add: assms execute_simps)
lemma crel_heapE [crel_elims]:
assumes "crel (heap f) h h' r"
obtains "h' = snd (f h)" and "r = fst (f h)"
- using assms by (rule crelE) simp
+ using assms by (rule crelE) (simp add: execute_simps)
lemma crel_guardI [crel_intros]:
assumes "P h" "h' = snd (f h)" "r = fst (f h)"
@@ -230,41 +230,45 @@
definition return :: "'a \<Rightarrow> 'a Heap" where
[code del]: "return x = heap (Pair x)"
-lemma execute_return [simp, execute_simps]:
+lemma execute_return [execute_simps]:
"execute (return x) = Some \<circ> Pair x"
- by (simp add: return_def)
+ by (simp add: return_def execute_simps)
-lemma success_returnI [iff, success_intros]:
+lemma success_returnI [success_intros]:
"success (return x) h"
- by (rule successI) simp
+ by (rule successI) (simp add: execute_simps)
lemma crel_returnI [crel_intros]:
"h = h' \<Longrightarrow> crel (return x) h h' x"
- by (rule crelI) simp
+ by (rule crelI) (simp add: execute_simps)
lemma crel_returnE [crel_elims]:
assumes "crel (return x) h h' r"
obtains "r = x" "h' = h"
- using assms by (rule crelE) simp
+ using assms by (rule crelE) (simp add: execute_simps)
definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
[code del]: "raise s = Heap (\<lambda>_. None)"
-lemma execute_raise [simp, execute_simps]:
+lemma execute_raise [execute_simps]:
"execute (raise s) = (\<lambda>_. None)"
by (simp add: raise_def)
lemma crel_raiseE [crel_elims]:
assumes "crel (raise x) h h' r"
obtains "False"
- using assms by (rule crelE) (simp add: success_def)
+ using assms by (rule crelE) (simp add: success_def execute_simps)
-definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
- [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
+definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" where
+ [code del]: "bind f g = Heap (\<lambda>h. case execute f h of
Some (x, h') \<Rightarrow> execute (g x) h'
| None \<Rightarrow> None)"
-notation bind (infixl "\<guillemotright>=" 54)
+setup {*
+ Adhoc_Overloading.add_variant
+ @{const_name Monad_Syntax.bindM} @{const_name Heap_Monad.bind}
+*}
+
lemma execute_bind [execute_simps]:
"execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
@@ -303,102 +307,16 @@
using assms by (simp add: bind_def)
lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
- by (rule Heap_eqI) (simp add: execute_bind)
+ by (rule Heap_eqI) (simp add: execute_bind execute_simps)
lemma bind_return [simp]: "f \<guillemotright>= return = f"
- by (rule Heap_eqI) (simp add: bind_def split: option.splits)
+ by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
- by (rule Heap_eqI) (simp add: bind_def split: option.splits)
+ by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
- by (rule Heap_eqI) (simp add: execute_bind)
-
-abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where
- "f >> g \<equiv> f >>= (\<lambda>_. g)"
-
-notation chain (infixl "\<guillemotright>" 54)
-
-
-subsubsection {* do-syntax *}
-
-text {*
- We provide a convenient do-notation for monadic expressions
- well-known from Haskell. @{const Let} is printed
- specially in do-expressions.
-*}
-
-nonterminals do_expr
-
-syntax
- "_do" :: "do_expr \<Rightarrow> 'a"
- ("(do (_)//done)" [12] 100)
- "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
- ("_ <- _;//_" [1000, 13, 12] 12)
- "_chain" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
- ("_;//_" [13, 12] 12)
- "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
- ("let _ = _;//_" [1000, 13, 12] 12)
- "_nil" :: "'a \<Rightarrow> do_expr"
- ("_" [12] 12)
-
-syntax (xsymbols)
- "_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
- ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
-
-translations
- "_do f" => "f"
- "_bind x f g" => "f \<guillemotright>= (\<lambda>x. g)"
- "_chain f g" => "f \<guillemotright> g"
- "_let x t f" => "CONST Let t (\<lambda>x. f)"
- "_nil f" => "f"
-
-print_translation {*
-let
- fun dest_abs_eta (Abs (abs as (_, ty, _))) =
- let
- val (v, t) = Syntax.variant_abs abs;
- in (Free (v, ty), t) end
- | dest_abs_eta t =
- let
- val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
- in (Free (v, dummyT), t) end;
- fun unfold_monad (Const (@{const_syntax bind}, _) $ f $ g) =
- let
- val (v, g') = dest_abs_eta g;
- val vs = fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) v [];
- val v_used = fold_aterms
- (fn Free (w, _) => (fn s => s orelse member (op =) vs w) | _ => I) g' false;
- in if v_used then
- Const (@{syntax_const "_bind"}, dummyT) $ v $ f $ unfold_monad g'
- else
- Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g'
- end
- | unfold_monad (Const (@{const_syntax chain}, _) $ f $ g) =
- Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g
- | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
- let
- val (v, g') = dest_abs_eta g;
- in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
- | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
- Const (@{const_syntax return}, dummyT) $ f
- | unfold_monad f = f;
- fun contains_bind (Const (@{const_syntax bind}, _) $ _ $ _) = true
- | contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
- contains_bind t;
- fun bind_monad_tr' (f::g::ts) = list_comb
- (Const (@{syntax_const "_do"}, dummyT) $
- unfold_monad (Const (@{const_syntax bind}, dummyT) $ f $ g), ts);
- fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
- if contains_bind g' then list_comb
- (Const (@{syntax_const "_do"}, dummyT) $
- unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
- else raise Match;
-in
- [(@{const_syntax bind}, bind_monad_tr'),
- (@{const_syntax Let}, Let_monad_tr')]
-end;
-*}
+ by (rule Heap_eqI) (simp add: execute_simps)
subsection {* Generic combinators *}
@@ -411,7 +329,7 @@
lemma execute_assert [execute_simps]:
"P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
"\<not> P x \<Longrightarrow> execute (assert P x) h = None"
- by (simp_all add: assert_def)
+ by (simp_all add: assert_def execute_simps)
lemma success_assertI [success_intros]:
"P x \<Longrightarrow> success (assert P x) h"
@@ -451,11 +369,11 @@
primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
"fold_map f [] = return []"
-| "fold_map f (x # xs) = do
+| "fold_map f (x # xs) = do {
y \<leftarrow> f x;
ys \<leftarrow> fold_map f xs;
return (y # ys)
- done"
+ }"
lemma fold_map_append:
"fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
@@ -466,14 +384,14 @@
shows "execute (fold_map f xs) h =
Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
using assms proof (induct xs)
- case Nil show ?case by simp
+ case Nil show ?case by (simp add: execute_simps)
next
case (Cons x xs)
from Cons.prems obtain y
where y: "execute (f x) h = Some (y, h)" by auto
moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
- ultimately show ?case by (simp, simp only: execute_bind(1), simp)
+ ultimately show ?case by (simp, simp only: execute_bind(1), simp add: execute_simps)
qed
subsection {* Code generator setup *}
@@ -611,7 +529,7 @@
text {* Monad *}
code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
-code_monad "op \<guillemotright>=" Haskell
+code_monad bind Haskell
code_const return (Haskell "return")
code_const Heap_Monad.raise' (Haskell "error/ _")
--- a/src/HOL/Imperative_HOL/Mrec.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Imperative_HOL/Mrec.thy Tue Jul 13 11:27:19 2010 +0100
@@ -64,19 +64,18 @@
lemma MREC_rule:
"MREC x =
- (do y \<leftarrow> f x;
+ do { y \<leftarrow> f x;
(case y of
Inl r \<Rightarrow> return r
| Inr s \<Rightarrow>
- do z \<leftarrow> MREC s ;
- g x s z
- done) done)"
+ do { z \<leftarrow> MREC s ;
+ g x s z })}"
unfolding MREC_def
unfolding bind_def return_def
apply simp
apply (rule ext)
apply (unfold mrec_rule[of x])
- by (auto split: option.splits prod.splits sum.splits)
+ by (auto simp add: execute_simps split: option.splits prod.splits sum.splits)
lemma MREC_pinduct:
assumes "execute (MREC x) h = Some (r, h')"
--- a/src/HOL/Imperative_HOL/Ref.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy Tue Jul 13 11:27:19 2010 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Ref.thy
+(* Title: HOL/Imperative_HOL/Ref.thy
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)
@@ -48,12 +48,12 @@
[code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))"
definition change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" where
- "change f r = (do
+ "change f r = do {
x \<leftarrow> ! r;
let y = f x;
r := y;
return y
- done)"
+ }"
subsection {* Properties *}
@@ -135,77 +135,77 @@
text {* Monad operations *}
-lemma execute_ref [simp, execute_simps]:
+lemma execute_ref [execute_simps]:
"execute (ref v) h = Some (alloc v h)"
- by (simp add: ref_def)
+ by (simp add: ref_def execute_simps)
-lemma success_refI [iff, success_intros]:
+lemma success_refI [success_intros]:
"success (ref v) h"
- by (auto simp add: ref_def)
+ by (auto intro: success_intros simp add: ref_def)
lemma crel_refI [crel_intros]:
assumes "(r, h') = alloc v h"
shows "crel (ref v) h h' r"
- by (rule crelI) (insert assms, simp)
+ by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_refE [crel_elims]:
assumes "crel (ref v) h h' r"
- obtains "Ref.get h' r = v" and "Ref.present h' r" and "\<not> Ref.present h r"
- using assms by (rule crelE) simp
+ obtains "get h' r = v" and "present h' r" and "\<not> present h r"
+ using assms by (rule crelE) (simp add: execute_simps)
-lemma execute_lookup [simp, execute_simps]:
+lemma execute_lookup [execute_simps]:
"Heap_Monad.execute (lookup r) h = Some (get h r, h)"
- by (simp add: lookup_def)
+ by (simp add: lookup_def execute_simps)
-lemma success_lookupI [iff, success_intros]:
+lemma success_lookupI [success_intros]:
"success (lookup r) h"
- by (auto simp add: lookup_def)
+ by (auto intro: success_intros simp add: lookup_def)
lemma crel_lookupI [crel_intros]:
- assumes "h' = h" "x = Ref.get h r"
+ assumes "h' = h" "x = get h r"
shows "crel (!r) h h' x"
- by (rule crelI) (insert assms, simp)
+ by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_lookupE [crel_elims]:
assumes "crel (!r) h h' x"
- obtains "h' = h" "x = Ref.get h r"
- using assms by (rule crelE) simp
+ obtains "h' = h" "x = get h r"
+ using assms by (rule crelE) (simp add: execute_simps)
-lemma execute_update [simp, execute_simps]:
+lemma execute_update [execute_simps]:
"Heap_Monad.execute (update r v) h = Some ((), set r v h)"
- by (simp add: update_def)
+ by (simp add: update_def execute_simps)
-lemma success_updateI [iff, success_intros]:
+lemma success_updateI [success_intros]:
"success (update r v) h"
- by (auto simp add: update_def)
+ by (auto intro: success_intros simp add: update_def)
lemma crel_updateI [crel_intros]:
- assumes "h' = Ref.set r v h"
+ assumes "h' = set r v h"
shows "crel (r := v) h h' x"
- by (rule crelI) (insert assms, simp)
+ by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_updateE [crel_elims]:
assumes "crel (r' := v) h h' r"
- obtains "h' = Ref.set r' v h"
- using assms by (rule crelE) simp
+ obtains "h' = set r' v h"
+ using assms by (rule crelE) (simp add: execute_simps)
-lemma execute_change [simp, execute_simps]:
+lemma execute_change [execute_simps]:
"Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
- by (simp add: change_def bind_def Let_def)
+ by (simp add: change_def bind_def Let_def execute_simps)
-lemma success_changeI [iff, success_intros]:
+lemma success_changeI [success_intros]:
"success (change f r) h"
by (auto intro!: success_intros crel_intros simp add: change_def)
lemma crel_changeI [crel_intros]:
- assumes "h' = Ref.set r (f (Ref.get h r)) h" "x = f (Ref.get h r)"
- shows "crel (Ref.change f r) h h' x"
- by (rule crelI) (insert assms, simp)
+ assumes "h' = set r (f (get h r)) h" "x = f (get h r)"
+ shows "crel (change f r) h h' x"
+ by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_changeE [crel_elims]:
- assumes "crel (Ref.change f r') h h' r"
- obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
- using assms by (rule crelE) simp
+ assumes "crel (change f r') h h' r"
+ obtains "h' = set r' (f (get h r')) h" "r = f (get h r')"
+ using assms by (rule crelE) (simp add: execute_simps)
lemma lookup_chain:
"(!r \<guillemotright> f) = f"
@@ -226,17 +226,17 @@
"get_array a (set r v h) ! i = get_array a h ! i"
by simp
-lemma get_change [simp]:
- "get (Array.change a i v h) r = get h r"
- by (simp add: get_def Array.change_def set_array_def)
+lemma get_update [simp]:
+ "get (Array.update a i v h) r = get h r"
+ by (simp add: get_def Array.update_def set_array_def)
-lemma alloc_change:
- "fst (alloc v (Array.change a i v' h)) = fst (alloc v h)"
- by (simp add: Array.change_def get_array_def set_array_def alloc_def Let_def)
+lemma alloc_update:
+ "fst (alloc v (Array.update a i v' h)) = fst (alloc v h)"
+ by (simp add: Array.update_def get_array_def set_array_def alloc_def Let_def)
-lemma change_set_swap:
- "Array.change a i v (set r v' h) = set r v' (Array.change a i v h)"
- by (simp add: Array.change_def get_array_def set_array_def set_def)
+lemma update_set_swap:
+ "Array.update a i v (set r v' h) = set r v' (Array.update a i v h)"
+ by (simp add: Array.update_def get_array_def set_array_def set_def)
lemma length_alloc [simp]:
"Array.length a (snd (alloc v h)) = Array.length a h"
@@ -246,9 +246,9 @@
"get_array a (snd (alloc v h)) = get_array a h"
by (simp add: get_array_def alloc_def set_def Let_def)
-lemma present_change [simp]:
- "present (Array.change a i v h) = present h"
- by (simp add: Array.change_def set_array_def expand_fun_eq present_def)
+lemma present_update [simp]:
+ "present (Array.update a i v h) = present h"
+ by (simp add: Array.update_def set_array_def expand_fun_eq present_def)
lemma array_present_set [simp]:
"array_present a (set r v h) = array_present a h"
@@ -262,7 +262,7 @@
"set_array a xs (set r x' h) = set r x' (set_array a xs h)"
by (simp add: set_array_def set_def)
-hide_const (open) present get set alloc lookup update change
+hide_const (open) present get set alloc noteq lookup update change
subsection {* Code generator setup *}
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 11:27:19 2010 +0100
@@ -12,19 +12,19 @@
definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
where
- "swap arr i j = (
- do
- x \<leftarrow> nth arr i;
- y \<leftarrow> nth arr j;
- upd i y arr;
- upd j x arr;
+ "swap arr i j =
+ do {
+ x \<leftarrow> Array.nth arr i;
+ y \<leftarrow> Array.nth arr j;
+ Array.upd i y arr;
+ Array.upd j x arr;
return ()
- done)"
+ }"
lemma crel_swapI [crel_intros]:
assumes "i < Array.length a h" "j < Array.length a h"
"x = get_array a h ! i" "y = get_array a h ! j"
- "h' = Array.change a j x (Array.change a i y h)"
+ "h' = Array.update a j x (Array.update a i y h)"
shows "crel (swap a i j) h h' r"
unfolding swap_def using assms by (auto intro!: crel_intros)
@@ -40,12 +40,12 @@
where
"part1 a left right p = (
if (right \<le> left) then return right
- else (do
- v \<leftarrow> nth a left;
+ else do {
+ v \<leftarrow> Array.nth a left;
(if (v \<le> p) then (part1 a (left + 1) right p)
- else (do swap a left right;
- part1 a left (right - 1) p done))
- done))"
+ else (do { swap a left right;
+ part1 a left (right - 1) p }))
+ })"
by pat_completeness auto
termination
@@ -227,14 +227,14 @@
fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
where
- "partition a left right = (do
- pivot \<leftarrow> nth a right;
+ "partition a left right = do {
+ pivot \<leftarrow> Array.nth a right;
middle \<leftarrow> part1 a left (right - 1) pivot;
- v \<leftarrow> nth a middle;
+ v \<leftarrow> Array.nth a middle;
m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
swap a m right;
return m
- done)"
+ }"
declare partition.simps[simp del]
@@ -294,8 +294,8 @@
else middle)"
unfolding partition.simps
by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
- from swap have h'_def: "h' = Array.change a r (get_array a h1 ! rs)
- (Array.change a rs (get_array a h1 ! r) h1)"
+ from swap have h'_def: "h' = Array.update a r (get_array a h1 ! rs)
+ (Array.update a rs (get_array a h1 ! r) h1)"
unfolding swap_def
by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
@@ -326,7 +326,7 @@
with part_partitions[OF part] right_remains True
have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
- unfolding Array.change_def Array.length_def by simp
+ unfolding Array.update_def Array.length_def by simp
}
moreover
{
@@ -352,7 +352,7 @@
by fastsimp
with i_is True rs_equals right_remains h'_def
show ?thesis using in_bounds
- unfolding Array.change_def Array.length_def
+ unfolding Array.update_def Array.length_def
by auto
qed
}
@@ -368,7 +368,7 @@
from part_partitions[OF part] rs_equals right_remains i_is_left
have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
- unfolding Array.change_def by simp
+ unfolding Array.update_def by simp
}
moreover
{
@@ -388,7 +388,7 @@
assume i_is: "i = r"
from i_is False rs_equals right_remains h'_def
show ?thesis using in_bounds
- unfolding Array.change_def Array.length_def
+ unfolding Array.update_def Array.length_def
by auto
qed
}
@@ -402,12 +402,12 @@
where
"quicksort arr left right =
(if (right > left) then
- do
+ do {
pivotNewIndex \<leftarrow> partition arr left right;
pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
quicksort arr left (pivotNewIndex - 1);
quicksort arr (pivotNewIndex + 1) right
- done
+ }
else return ())"
by pat_completeness auto
@@ -645,11 +645,11 @@
subsection {* Example *}
-definition "qsort a = do
- k \<leftarrow> len a;
+definition "qsort a = do {
+ k \<leftarrow> Array.len a;
quicksort a 0 (k - 1);
return a
- done"
+ }"
code_reserved SML upto
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 11:27:19 2010 +0100
@@ -8,27 +8,22 @@
imports Imperative_HOL Subarray
begin
-hide_const (open) swap rev
-
fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
- "swap a i j = (do
- x \<leftarrow> nth a i;
- y \<leftarrow> nth a j;
- upd i y a;
- upd j x a;
+ "swap a i j = do {
+ x \<leftarrow> Array.nth a i;
+ y \<leftarrow> Array.nth a j;
+ Array.upd i y a;
+ Array.upd j x a;
return ()
- done)"
+ }"
fun rev :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
- "rev a i j = (if (i < j) then (do
+ "rev a i j = (if (i < j) then do {
swap a i j;
rev a (i + 1) (j - 1)
- done)
+ }
else return ())"
-notation (output) swap ("swap")
-notation (output) rev ("rev")
-
declare swap.simps [simp del] rev.simps [simp del]
lemma swap_pointwise: assumes "crel (swap a i j) h h' r"
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Jul 13 11:27:19 2010 +0100
@@ -31,10 +31,10 @@
primrec make_llist :: "'a\<Colon>heap list \<Rightarrow> 'a node Heap"
where
[simp del]: "make_llist [] = return Empty"
- | "make_llist (x#xs) = do tl \<leftarrow> make_llist xs;
- next \<leftarrow> ref tl;
- return (Node x next)
- done"
+ | "make_llist (x#xs) = do { tl \<leftarrow> make_llist xs;
+ next \<leftarrow> ref tl;
+ return (Node x next)
+ }"
text {* define traverse using the MREC combinator *}
@@ -43,18 +43,18 @@
traverse :: "'a\<Colon>heap node \<Rightarrow> 'a list Heap"
where
[code del]: "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
- | Node x r \<Rightarrow> (do tl \<leftarrow> Ref.lookup r;
- return (Inr tl) done))
+ | Node x r \<Rightarrow> do { tl \<leftarrow> Ref.lookup r;
+ return (Inr tl) })
(\<lambda>n tl xs. case n of Empty \<Rightarrow> undefined
| Node x r \<Rightarrow> return (x # xs))"
lemma traverse_simps[code, simp]:
"traverse Empty = return []"
- "traverse (Node x r) = do tl \<leftarrow> Ref.lookup r;
- xs \<leftarrow> traverse tl;
- return (x#xs)
- done"
+ "traverse (Node x r) = do { tl \<leftarrow> Ref.lookup r;
+ xs \<leftarrow> traverse tl;
+ return (x#xs)
+ }"
unfolding traverse_def
by (auto simp: traverse_def MREC_rule)
@@ -529,25 +529,25 @@
subsection {* Definition of in-place reversal *}
definition rev' :: "(('a::heap) node ref \<times> 'a node ref) \<Rightarrow> 'a node ref Heap"
-where "rev' = MREC (\<lambda>(q, p). do v \<leftarrow> !p; (case v of Empty \<Rightarrow> (return (Inl q))
- | Node x next \<Rightarrow> do
+where "rev' = MREC (\<lambda>(q, p). do { v \<leftarrow> !p; (case v of Empty \<Rightarrow> (return (Inl q))
+ | Node x next \<Rightarrow> do {
p := Node x q;
return (Inr (p, next))
- done) done)
+ })})
(\<lambda>x s z. return z)"
lemma rev'_simps [code]:
"rev' (q, p) =
- do
+ do {
v \<leftarrow> !p;
(case v of
Empty \<Rightarrow> return q
| Node x next \<Rightarrow>
- do
+ do {
p := Node x q;
rev' (p, next)
- done)
- done"
+ })
+ }"
unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric]
thm arg_cong2
by (auto simp add: expand_fun_eq intro: arg_cong2[where f = "op \<guillemotright>="] split: node.split)
@@ -555,7 +555,7 @@
primrec rev :: "('a:: heap) node \<Rightarrow> 'a node Heap"
where
"rev Empty = return Empty"
-| "rev (Node x n) = (do q \<leftarrow> ref Empty; p \<leftarrow> ref (Node x n); v \<leftarrow> rev' (q, p); !v done)"
+| "rev (Node x n) = do { q \<leftarrow> ref Empty; p \<leftarrow> ref (Node x n); v \<leftarrow> rev' (q, p); !v }"
subsection {* Correctness Proof *}
@@ -680,7 +680,7 @@
definition merge' :: "(('a::{heap, ord}) node ref * ('a::{heap, ord})) * ('a::{heap, ord}) node ref * ('a::{heap, ord}) node ref \<Rightarrow> ('a::{heap, ord}) node ref Heap"
where
-"merge' = MREC (\<lambda>(_, p, q). (do v \<leftarrow> !p; w \<leftarrow> !q;
+"merge' = MREC (\<lambda>(_, p, q). do { v \<leftarrow> !p; w \<leftarrow> !q;
(case v of Empty \<Rightarrow> return (Inl q)
| Node valp np \<Rightarrow>
(case w of Empty \<Rightarrow> return (Inl p)
@@ -688,8 +688,8 @@
if (valp \<le> valq) then
return (Inr ((p, valp), np, q))
else
- return (Inr ((q, valq), p, nq)))) done))
- (\<lambda> _ ((n, v), _, _) r. do n := Node v r; return n done)"
+ return (Inr ((q, valq), p, nq)))) })
+ (\<lambda> _ ((n, v), _, _) r. do { n := Node v r; return n })"
definition merge where "merge p q = merge' (undefined, p, q)"
@@ -713,21 +713,21 @@
term "Ref.change"
lemma merge_simps [code]:
shows "merge p q =
-do v \<leftarrow> !p;
+do { v \<leftarrow> !p;
w \<leftarrow> !q;
(case v of node.Empty \<Rightarrow> return q
| Node valp np \<Rightarrow>
case w of node.Empty \<Rightarrow> return p
| Node valq nq \<Rightarrow>
- if valp \<le> valq then do r \<leftarrow> merge np q;
+ if valp \<le> valq then do { r \<leftarrow> merge np q;
p := (Node valp r);
return p
- done
- else do r \<leftarrow> merge p nq;
+ }
+ else do { r \<leftarrow> merge p nq;
q := (Node valq r);
return q
- done)
-done"
+ })
+}"
proof -
{fix v x y
have case_return: "(case v of Empty \<Rightarrow> return x | Node v n \<Rightarrow> return (y v n)) = return (case v of Empty \<Rightarrow> x | Node v n \<Rightarrow> y v n)" by (cases v) auto
@@ -997,11 +997,11 @@
text {* A simple example program *}
-definition test_1 where "test_1 = (do ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs done)"
-definition test_2 where "test_2 = (do ll_xs <- make_llist [1..(15::int)]; ll_ys <- rev ll_xs; ys <- traverse ll_ys; return ys done)"
+definition test_1 where "test_1 = (do { ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs })"
+definition test_2 where "test_2 = (do { ll_xs <- make_llist [1..(15::int)]; ll_ys <- rev ll_xs; ys <- traverse ll_ys; return ys })"
definition test_3 where "test_3 =
- (do
+ (do {
ll_xs \<leftarrow> make_llist (filter (%n. n mod 2 = 0) [2..8]);
ll_ys \<leftarrow> make_llist (filter (%n. n mod 2 = 1) [5..11]);
r \<leftarrow> ref ll_xs;
@@ -1010,7 +1010,7 @@
ll_zs \<leftarrow> !p;
zs \<leftarrow> traverse ll_zs;
return zs
- done)"
+ })"
code_reserved SML upto
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Jul 13 11:27:19 2010 +0100
@@ -127,21 +127,21 @@
unfolding array_ran_def Array.length_def by simp
lemma array_ran_upd_array_Some:
- assumes "cl \<in> array_ran a (Array.change a i (Some b) h)"
+ 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 (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
with assms show ?thesis
- unfolding array_ran_def Array.change_def by fastsimp
+ unfolding array_ran_def Array.update_def by fastsimp
qed
lemma array_ran_upd_array_None:
- assumes "cl \<in> array_ran a (Array.change a i None h)"
+ assumes "cl \<in> array_ran a (Array.update a i None h)"
shows "cl \<in> array_ran a h"
proof -
have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
with assms show ?thesis
- unfolding array_ran_def Array.change_def by auto
+ unfolding array_ran_def Array.update_def by auto
qed
definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool"
@@ -152,7 +152,7 @@
lemma correctArray_update:
assumes "correctArray rcs a h"
assumes "correctClause rcs c" "sorted c" "distinct c"
- shows "correctArray rcs a (Array.change a i (Some c) h)"
+ shows "correctArray rcs a (Array.update a i (Some c) h)"
using assms
unfolding correctArray_def
by (auto dest:array_ran_upd_array_Some)
@@ -174,15 +174,15 @@
primrec res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap"
where
"res_mem l [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
-| "res_mem l (x#xs) = (if (x = l) then return xs else (do v \<leftarrow> res_mem l xs; return (x # v) done))"
+| "res_mem l (x#xs) = (if (x = l) then return xs else do { v \<leftarrow> res_mem l xs; return (x # v) })"
fun resolve1 :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap"
where
"resolve1 l (x#xs) (y#ys) =
(if (x = l) then return (merge xs (y#ys))
- else (if (x < y) then (do v \<leftarrow> resolve1 l xs (y#ys); return (x # v) done)
- else (if (x > y) then (do v \<leftarrow> resolve1 l (x#xs) ys; return (y # v) done)
- else (do v \<leftarrow> resolve1 l xs ys; return (x # v) done))))"
+ else (if (x < y) then do { v \<leftarrow> resolve1 l xs (y#ys); return (x # v) }
+ else (if (x > y) then do { v \<leftarrow> resolve1 l (x#xs) ys; return (y # v) }
+ else do { v \<leftarrow> resolve1 l xs ys; return (x # v) })))"
| "resolve1 l [] ys = raise ''MiniSatChecked.res_thm: Cannot find literal''"
| "resolve1 l xs [] = res_mem l xs"
@@ -190,9 +190,9 @@
where
"resolve2 l (x#xs) (y#ys) =
(if (y = l) then return (merge (x#xs) ys)
- else (if (x < y) then (do v \<leftarrow> resolve2 l xs (y#ys); return (x # v) done)
- else (if (x > y) then (do v \<leftarrow> resolve2 l (x#xs) ys; return (y # v) done)
- else (do v \<leftarrow> resolve2 l xs ys; return (x # v) done))))"
+ else (if (x < y) then do { v \<leftarrow> resolve2 l xs (y#ys); return (x # v) }
+ else (if (x > y) then do { v \<leftarrow> resolve2 l (x#xs) ys; return (y # v) }
+ else do { v \<leftarrow> resolve2 l xs ys; return (x # v) })))"
| "resolve2 l xs [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
| "resolve2 l [] ys = res_mem l ys"
@@ -413,10 +413,10 @@
definition get_clause :: "Clause option array \<Rightarrow> ClauseId \<Rightarrow> Clause Heap"
where
"get_clause a i =
- (do c \<leftarrow> nth a i;
+ do { c \<leftarrow> Array.nth a i;
(case c of None \<Rightarrow> raise (''Clause not found'')
| Some x \<Rightarrow> return x)
- done)"
+ }"
primrec res_thm2 :: "Clause option array \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap"
@@ -424,9 +424,9 @@
"res_thm2 a (l, j) cli =
( if l = 0 then raise(''Illegal literal'')
else
- (do clj \<leftarrow> get_clause a j;
+ do { clj \<leftarrow> get_clause a j;
res_thm' l cli clj
- done))"
+ })"
primrec
foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
@@ -437,27 +437,27 @@
fun doProofStep2 :: "Clause option array \<Rightarrow> ProofStep \<Rightarrow> Clause list \<Rightarrow> Clause list Heap"
where
"doProofStep2 a (Conflict saveTo (i, rs)) rcs =
- (do
+ do {
cli \<leftarrow> get_clause a i;
result \<leftarrow> foldM (res_thm2 a) rs cli;
- upd saveTo (Some result) a;
+ Array.upd saveTo (Some result) a;
return rcs
- done)"
-| "doProofStep2 a (Delete cid) rcs = (do upd cid None a; return rcs done)"
-| "doProofStep2 a (Root cid clause) rcs = (do upd cid (Some (remdups (sort clause))) a; return (clause # rcs) done)"
+ }"
+| "doProofStep2 a (Delete cid) rcs = do { Array.upd cid None a; return rcs }"
+| "doProofStep2 a (Root cid clause) rcs = do { Array.upd cid (Some (remdups (sort clause))) a; return (clause # rcs) }"
| "doProofStep2 a (Xstep cid1 cid2) rcs = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
| "doProofStep2 a (ProofDone b) rcs = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
definition checker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
where
"checker n p i =
- (do
+ do {
a \<leftarrow> Array.new n None;
rcs \<leftarrow> foldM (doProofStep2 a) p [];
ec \<leftarrow> Array.nth a i;
(if ec = Some [] then return rcs
else raise(''No empty clause''))
- done)"
+ }"
lemma crel_option_case:
assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
@@ -651,10 +651,10 @@
"ldoProofStep (Conflict saveTo (i, rs)) (xs, rcl) =
(case (xs ! i) of
None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
- | Some cli \<Rightarrow> (do
+ | Some cli \<Rightarrow> do {
result \<leftarrow> foldM (lres_thm xs) rs cli ;
return ((xs[saveTo:=Some result]), rcl)
- done))"
+ })"
| "ldoProofStep (Delete cid) (xs, rcl) = return (xs[cid:=None], rcl)"
| "ldoProofStep (Root cid clause) (xs, rcl) = return (xs[cid:=Some (sort clause)], (remdups(sort clause)) # rcl)"
| "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
@@ -663,11 +663,11 @@
definition lchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
where
"lchecker n p i =
- (do
+ do {
rcs \<leftarrow> foldM (ldoProofStep) p ([], []);
(if (fst rcs ! i) = Some [] then return (snd rcs)
else raise(''No empty clause''))
- done)"
+ }"
section {* Functional version with RedBlackTrees *}
@@ -684,10 +684,10 @@
"tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) =
(case (RBT_Impl.lookup t i) of
None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
- | Some cli \<Rightarrow> (do
+ | Some cli \<Rightarrow> do {
result \<leftarrow> foldM (tres_thm t) rs cli;
return ((RBT_Impl.insert saveTo result t), rcl)
- done))"
+ })"
| "tdoProofStep (Delete cid) (t, rcl) = return ((RBT_Impl.delete cid t), rcl)"
| "tdoProofStep (Root cid clause) (t, rcl) = return (RBT_Impl.insert cid (sort clause) t, (remdups(sort clause)) # rcl)"
| "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
@@ -696,11 +696,11 @@
definition tchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
where
"tchecker n p i =
- (do
+ do {
rcs \<leftarrow> foldM (tdoProofStep) p (RBT_Impl.Empty, []);
(if (RBT_Impl.lookup (fst rcs) i) = Some [] then return (snd rcs)
else raise(''No empty clause''))
- done)"
+ }"
section {* Code generation setup *}
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Tue Jul 13 11:27:19 2010 +0100
@@ -11,20 +11,20 @@
definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
"subarray n m a h \<equiv> sublist' n m (get_array a h)"
-lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
-apply (simp add: subarray_def Array.change_def)
+lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
+apply (simp add: subarray_def Array.update_def)
apply (simp add: sublist'_update1)
done
-lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
-apply (simp add: subarray_def Array.change_def)
+lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
+apply (simp add: subarray_def Array.update_def)
apply (subst sublist'_update2)
apply fastsimp
apply simp
done
-lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h[i - n := v]"
-unfolding subarray_def Array.change_def
+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: sublist'_update3)
lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
--- a/src/HOL/IsaMakefile Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/IsaMakefile Tue Jul 13 11:27:19 2010 +0100
@@ -397,7 +397,7 @@
$(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML \
$(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \
- Library/Abstract_Rat.thy Library/AssocList.thy \
+ Library/Abstract_Rat.thy Library/Adhoc_Overloading.thy Library/AssocList.thy \
Library/BigO.thy Library/Binomial.thy Library/Bit.thy \
Library/Boolean_Algebra.thy Library/Cardinality.thy \
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
@@ -414,8 +414,8 @@
Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \
Library/Lattice_Syntax.thy Library/Library.thy \
Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
- Library/More_List.thy Library/More_Set.thy Library/Multiset.thy \
- Library/Nat_Bijection.thy Library/Nat_Infinity.thy \
+ Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \
+ Library/Multiset.thy Library/Nat_Bijection.thy Library/Nat_Infinity.thy \
Library/Nested_Environment.thy Library/Numeral_Type.thy \
Library/OptionalSugar.thy Library/Order_Relation.thy \
Library/Permutation.thy Library/Permutations.thy \
@@ -434,8 +434,8 @@
Library/Sum_Of_Squares/sum_of_squares.ML \
Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \
Library/While_Combinator.thy Library/Zorn.thy \
- Library/positivstellensatz.ML Library/reflection.ML \
- Library/reify_data.ML \
+ Library/adhoc_overloading.ML Library/positivstellensatz.ML \
+ Library/reflection.ML Library/reify_data.ML \
Library/document/root.bib Library/document/root.tex
@cd Library; $(ISABELLE_TOOL) usedir -b -f HOL_Library_ROOT.ML $(OUT)/HOL HOL-Library
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Adhoc_Overloading.thy Tue Jul 13 11:27:19 2010 +0100
@@ -0,0 +1,14 @@
+(* Author: Alexander Krauss, TU Muenchen
+ Author: Christian Sternagel, University of Innsbruck
+*)
+
+header {* Ad-hoc overloading of constants based on their types *}
+
+theory Adhoc_Overloading
+imports Main
+uses "adhoc_overloading.ML"
+begin
+
+setup Adhoc_Overloading.setup
+
+end
--- a/src/HOL/Library/Library.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Library/Library.thy Tue Jul 13 11:27:19 2010 +0100
@@ -2,6 +2,7 @@
theory Library
imports
Abstract_Rat
+ Adhoc_Overloading
AssocList
BigO
Binomial
@@ -31,6 +32,7 @@
ListVector
Kleene_Algebra
Mapping
+ Monad_Syntax
More_List
Multiset
Nat_Infinity
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Monad_Syntax.thy Tue Jul 13 11:27:19 2010 +0100
@@ -0,0 +1,66 @@
+(* Author: Alexander Krauss, TU Muenchen
+ Author: Christian Sternagel, University of Innsbruck
+*)
+
+header {* Monad notation for arbitrary types *}
+
+theory Monad_Syntax
+imports Adhoc_Overloading
+begin
+
+text {*
+ We provide a convenient do-notation for monadic expressions
+ well-known from Haskell. @{const Let} is printed
+ specially in do-expressions.
+*}
+
+consts
+ bindM :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
+
+notation (xsymbols)
+ bindM (infixr "\<guillemotright>=" 54)
+
+abbreviation (do_notation)
+ bindM_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
+where
+ "bindM_do \<equiv> bindM"
+
+notation (output)
+ bindM_do (infixr ">>=" 54)
+
+notation (xsymbols output)
+ bindM_do (infixr "\<guillemotright>=" 54)
+
+nonterminals
+ do_binds do_bind
+
+syntax
+ "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2 _)//}" [12] 62)
+ "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
+ "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
+ "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
+ "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
+ "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
+ "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
+
+syntax (xsymbols)
+ "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
+ "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
+
+translations
+ "_do_block (_do_cons (_do_then t) (_do_final e))"
+ == "CONST bindM_do t (\<lambda>_. e)"
+ "_do_block (_do_cons (_do_bind p t) (_do_final e))"
+ == "CONST bindM_do t (\<lambda>p. e)"
+ "_do_block (_do_cons (_do_let p t) bs)"
+ == "let p = t in _do_block bs"
+ "_do_block (_do_cons b (_do_cons c cs))"
+ == "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
+ "_do_cons (_do_let p t) (_do_final s)"
+ == "_do_final (let p = t in s)"
+ "_do_block (_do_final e)" => "e"
+ "(m >> n)" => "(m >>= (\<lambda>_. n))"
+
+setup {* Adhoc_Overloading.add_overloaded @{const_name bindM} *}
+
+end
--- a/src/HOL/Library/State_Monad.thy Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Library/State_Monad.thy Tue Jul 13 11:27:19 2010 +0100
@@ -5,7 +5,7 @@
header {* Combinator syntax for generic, open state monads (single threaded monads) *}
theory State_Monad
-imports Main
+imports Monad_Syntax
begin
subsection {* Motivation *}
@@ -112,86 +112,8 @@
lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
-
-subsection {* Syntax *}
-
-text {*
- We provide a convenient do-notation for monadic expressions
- well-known from Haskell. @{const Let} is printed
- specially in do-expressions.
-*}
-
-nonterminals do_expr
-
-syntax
- "_do" :: "do_expr \<Rightarrow> 'a"
- ("do _ done" [12] 12)
- "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
- ("_ <- _;// _" [1000, 13, 12] 12)
- "_fcomp" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
- ("_;// _" [13, 12] 12)
- "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
- ("let _ = _;// _" [1000, 13, 12] 12)
- "_done" :: "'a \<Rightarrow> do_expr"
- ("_" [12] 12)
-
-syntax (xsymbols)
- "_scomp" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
- ("_ \<leftarrow> _;// _" [1000, 13, 12] 12)
-
-translations
- "_do f" => "f"
- "_scomp x f g" => "f \<circ>\<rightarrow> (\<lambda>x. g)"
- "_fcomp f g" => "f \<circ>> g"
- "_let x t f" => "CONST Let t (\<lambda>x. f)"
- "_done f" => "f"
-
-print_translation {*
-let
- fun dest_abs_eta (Abs (abs as (_, ty, _))) =
- let
- val (v, t) = Syntax.variant_abs abs;
- in (Free (v, ty), t) end
- | dest_abs_eta t =
- let
- val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);
- in (Free (v, dummyT), t) end;
- fun unfold_monad (Const (@{const_syntax scomp}, _) $ f $ g) =
- let
- val (v, g') = dest_abs_eta g;
- in Const (@{syntax_const "_scomp"}, dummyT) $ v $ f $ unfold_monad g' end
- | unfold_monad (Const (@{const_syntax fcomp}, _) $ f $ g) =
- Const (@{syntax_const "_fcomp"}, dummyT) $ f $ unfold_monad g
- | unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =
- let
- val (v, g') = dest_abs_eta g;
- in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end
- | unfold_monad (Const (@{const_syntax Pair}, _) $ f) =
- Const (@{const_syntax "return"}, dummyT) $ f
- | unfold_monad f = f;
- fun contains_scomp (Const (@{const_syntax scomp}, _) $ _ $ _) = true
- | contains_scomp (Const (@{const_syntax fcomp}, _) $ _ $ t) =
- contains_scomp t
- | contains_scomp (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) =
- contains_scomp t;
- fun scomp_monad_tr' (f::g::ts) = list_comb
- (Const (@{syntax_const "_do"}, dummyT) $
- unfold_monad (Const (@{const_syntax scomp}, dummyT) $ f $ g), ts);
- fun fcomp_monad_tr' (f::g::ts) =
- if contains_scomp g then list_comb
- (Const (@{syntax_const "_do"}, dummyT) $
- unfold_monad (Const (@{const_syntax fcomp}, dummyT) $ f $ g), ts)
- else raise Match;
- fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) =
- if contains_scomp g' then list_comb
- (Const (@{syntax_const "_do"}, dummyT) $
- unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts)
- else raise Match;
-in
- [(@{const_syntax scomp}, scomp_monad_tr'),
- (@{const_syntax fcomp}, fcomp_monad_tr'),
- (@{const_syntax Let}, Let_monad_tr')]
-end;
+setup {*
+ Adhoc_Overloading.add_variant @{const_name bindM} @{const_name scomp}
*}
text {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/adhoc_overloading.ML Tue Jul 13 11:27:19 2010 +0100
@@ -0,0 +1,140 @@
+(* Author: Alexander Krauss, TU Muenchen
+ Author: Christian Sternagel, University of Innsbruck
+
+Ad-hoc overloading of constants based on their types.
+*)
+
+signature ADHOC_OVERLOADING =
+sig
+
+ val add_overloaded: string -> theory -> theory
+ val add_variant: string -> string -> theory -> theory
+
+ val show_variants: bool Unsynchronized.ref
+ val setup: theory -> theory
+
+end
+
+
+structure Adhoc_Overloading: ADHOC_OVERLOADING =
+struct
+
+val show_variants = Unsynchronized.ref false;
+
+
+(* errors *)
+
+fun duplicate_variant_err int_name ext_name =
+ error ("Constant " ^ quote int_name ^ " is already a variant of " ^ quote ext_name);
+
+fun not_overloaded_err name =
+ error ("Constant " ^ quote name ^ " is not declared as overloaded");
+
+fun already_overloaded_err name =
+ error ("Constant " ^ quote name ^ " is already declared as overloaded");
+
+fun unresolved_err ctxt (c, T) t reason =
+ error ("Unresolved overloading of " ^ quote c ^ " :: " ^
+ quote (Syntax.string_of_typ ctxt T) ^ " in " ^
+ quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
+
+
+(* theory data *)
+
+structure Overload_Data = Theory_Data
+(
+ type T =
+ { internalize : (string * typ) list Symtab.table,
+ externalize : string Symtab.table };
+ val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
+ val extend = I;
+
+ fun merge_ext int_name (ext_name1, ext_name2) =
+ if ext_name1 = ext_name2 then ext_name1
+ else duplicate_variant_err int_name ext_name1;
+
+ fun merge ({internalize=int1, externalize=ext1},
+ {internalize=int2, externalize=ext2}) =
+ {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
+ externalize=Symtab.join merge_ext (ext1, ext2)};
+);
+
+fun map_tables f g =
+ Overload_Data.map (fn {internalize=int, externalize=ext} =>
+ {internalize=f int, externalize=g ext});
+
+val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
+val get_variants = Symtab.lookup o #internalize o Overload_Data.get;
+val get_external = Symtab.lookup o #externalize o Overload_Data.get;
+
+fun add_overloaded ext_name thy =
+ let val _ = not (is_overloaded thy ext_name) orelse already_overloaded_err ext_name;
+ in map_tables (Symtab.update (ext_name, [])) I thy end;
+
+fun add_variant ext_name name thy =
+ let
+ val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name;
+ val _ = case get_external thy name of
+ NONE => ()
+ | SOME gen' => duplicate_variant_err name gen';
+ val T = Sign.the_const_type thy name;
+ in
+ map_tables (Symtab.cons_list (ext_name, (name, T)))
+ (Symtab.update (name, ext_name)) thy
+ end
+
+
+(* check / uncheck *)
+
+fun unifiable_with ctxt T1 (c, T2) =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val maxidx1 = Term.maxidx_of_typ T1;
+ val T2' = Logic.incr_tvar (maxidx1 + 1) T2;
+ val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2');
+ in
+ (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c)
+ handle Type.TUNIFY => NONE
+ end;
+
+fun insert_internal_same ctxt t (Const (c, T)) =
+ (case map_filter (unifiable_with ctxt T)
+ (Same.function (get_variants (ProofContext.theory_of ctxt)) c) of
+ [] => unresolved_err ctxt (c, T) t "no instances"
+ | [c'] => Const (c', dummyT)
+ | _ => raise Same.SAME)
+ | insert_internal_same _ _ _ = raise Same.SAME;
+
+fun insert_external_same ctxt _ (Const (c, T)) =
+ Const (Same.function (get_external (ProofContext.theory_of ctxt)) c, T)
+ | insert_external_same _ _ _ = raise Same.SAME;
+
+fun gen_check_uncheck replace ts ctxt =
+ Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts
+ |> Option.map (rpair ctxt);
+
+val check = gen_check_uncheck insert_internal_same;
+fun uncheck ts ctxt =
+ if !show_variants then NONE
+ else gen_check_uncheck insert_external_same ts ctxt;
+
+fun reject_unresolved ts ctxt =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ fun check_unresolved t =
+ case filter (is_overloaded thy o fst) (Term.add_consts t []) of
+ [] => ()
+ | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances";
+
+ val _ = map check_unresolved ts;
+ in NONE end;
+
+
+(* setup *)
+
+val setup = Context.theory_map
+ (Syntax.add_term_check 0 "adhoc_overloading" check
+ #> Syntax.add_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
+ #> Syntax.add_term_uncheck 0 "adhoc_overloading" uncheck);
+
+end
--- a/src/HOL/Matrix/CplexMatrixConverter.ML Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Matrix/CplexMatrixConverter.ML Tue Jul 13 11:27:19 2010 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Matrix/cplex/CplexMatrixConverter.ML
+(* Title: HOL/Matrix/CplexMatrixConverter.ML
Author: Steven Obua
*)
--- a/src/HOL/Matrix/Cplex_tools.ML Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Matrix/Cplex_tools.ML Tue Jul 13 11:27:19 2010 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Matrix/cplex/Cplex_tools.ML
+(* Title: HOL/Matrix/Cplex_tools.ML
Author: Steven Obua
*)
--- a/src/HOL/Matrix/FloatSparseMatrixBuilder.ML Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Matrix/FloatSparseMatrixBuilder.ML Tue Jul 13 11:27:19 2010 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
+(* Title: HOL/Matrix/FloatSparseMatrixBuilder.ML
Author: Steven Obua
*)
--- a/src/HOL/Matrix/fspmlp.ML Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Matrix/fspmlp.ML Tue Jul 13 11:27:19 2010 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Matrix/cplex/fspmlp.ML
+(* Title: HOL/Matrix/fspmlp.ML
Author: Steven Obua
*)
--- a/src/HOL/Matrix/matrixlp.ML Tue Jul 13 11:26:16 2010 +0100
+++ b/src/HOL/Matrix/matrixlp.ML Tue Jul 13 11:27:19 2010 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Matrix/cplex/matrixlp.ML
+(* Title: HOL/Matrix/matrixlp.ML
Author: Steven Obua
*)