--- a/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 11:50:22 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 12:00:11 2010 +0200
@@ -407,25 +407,25 @@
by (simp add: upd'_def upd_return)
lemma [code]:
- "map_entry i f a = (do
+ "map_entry i f a = do {
x \<leftarrow> nth a i;
upd i (f x) a
- done)"
+ }"
by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps)
lemma [code]:
- "swap i x a = (do
+ "swap i x a = do {
y \<leftarrow> nth a i;
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
+ "freeze a = do {
n \<leftarrow> len a;
Heap_Monad.fold_map (\<lambda>i. nth a i) [0..<n]
- done)"
+ }"
proof (rule Heap_eqI)
fix h
have *: "List.map
@@ -440,15 +440,15 @@
apply (simp_all add: nth_def guard_def *)
apply (simp add: length_def map_nth)
done
- then have "execute (do
+ then have "execute (do {
n \<leftarrow> len a;
Heap_Monad.fold_map (Array.nth a) [0..<n]
- done) h = Some (get_array a h, h)"
+ }) h = Some (get_array a h, h)"
by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
- then show "execute (freeze a) h = execute (do
+ then show "execute (freeze a) h = execute (do {
n \<leftarrow> len a;
Heap_Monad.fold_map (Array.nth a) [0..<n]
- done) h" by (simp add: execute_simps)
+ }) 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:50:22 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 13 12:00:11 2010 +0200
@@ -5,7 +5,7 @@
header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
theory Heap_Monad
-imports Heap
+imports Heap Monad_Syntax
begin
subsection {* The monad *}
@@ -259,12 +259,16 @@
obtains "False"
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'"
@@ -314,92 +318,6 @@
lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
by (rule Heap_eqI) (simp add: execute_simps)
-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;
-*}
-
subsection {* Generic combinators *}
@@ -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)))"
@@ -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:50:22 2010 +0200
+++ b/src/HOL/Imperative_HOL/Mrec.thy Tue Jul 13 12:00:11 2010 +0200
@@ -64,13 +64,12 @@
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
--- a/src/HOL/Imperative_HOL/Ref.thy Tue Jul 13 11:50:22 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Tue Jul 13 12:00:11 2010 +0200
@@ -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 *}
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 11:50:22 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 12:00:11 2010 +0200
@@ -12,14 +12,14 @@
definition swap :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
where
- "swap arr i j = (
- do
+ "swap arr i j =
+ do {
x \<leftarrow> nth arr i;
y \<leftarrow> nth arr j;
upd i y arr;
upd j x arr;
return ()
- done)"
+ }"
lemma crel_swapI [crel_intros]:
assumes "i < Array.length a h" "j < Array.length a h"
@@ -40,12 +40,12 @@
where
"part1 a left right p = (
if (right \<le> left) then return right
- else (do
+ else do {
v \<leftarrow> 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
+ "partition a left right = do {
pivot \<leftarrow> nth a right;
middle \<leftarrow> part1 a left (right - 1) pivot;
v \<leftarrow> 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]
@@ -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
+definition "qsort a = do {
k \<leftarrow> 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:50:22 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 12:00:11 2010 +0200
@@ -11,19 +11,19 @@
hide_const (open) swap rev
fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
- "swap a i j = (do
+ "swap a i j = do {
x \<leftarrow> nth a i;
y \<leftarrow> nth a j;
upd i y a;
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")
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Jul 13 11:50:22 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Jul 13 12:00:11 2010 +0200
@@ -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:50:22 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Jul 13 12:00:11 2010 +0200
@@ -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> 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;
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 { upd cid None a; return rcs }"
+| "doProofStep2 a (Root cid clause) rcs = do { 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 *}