--- a/src/CCL/CCL.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/CCL.thy Tue Mar 29 23:46:46 2011 +0200
@@ -85,6 +85,8 @@
apply_def: "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))"
bot_def: "bot == (lam x. x`x)`(lam x. x`x)"
+
+defs
fix_def: "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
(* The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *)
@@ -106,6 +108,7 @@
(** Partial Order **)
+axioms
po_refl: "a [= a"
po_trans: "[| a [= b; b [= c |] ==> a [= c"
po_cong: "a [= b ==> f(a) [= f(b)"
@@ -136,6 +139,7 @@
(*** Definitions of Termination and Divergence ***)
+defs
Dvg_def: "Dvg(t) == t = bot"
Trm_def: "Trm(t) == ~ Dvg(t)"
--- a/src/CCL/Fix.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Fix.thy Tue Mar 29 23:46:46 2011 +0200
@@ -9,17 +9,12 @@
imports Type
begin
-consts
- idgen :: "[i]=>i"
- INCL :: "[i=>o]=>o"
+definition idgen :: "i => i"
+ where "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
-defs
- idgen_def:
- "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
-
-axioms
- INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
- po_INCL: "INCL(%x. a(x) [= b(x))"
+axiomatization INCL :: "[i=>o]=>o" where
+ INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" and
+ po_INCL: "INCL(%x. a(x) [= b(x))" and
INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
--- a/src/CCL/Hered.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Hered.thy Tue Mar 29 23:46:46 2011 +0200
@@ -15,18 +15,13 @@
is. Not so useful for functions!
*}
-consts
- (*** Predicates ***)
- HTTgen :: "i set => i set"
- HTT :: "i set"
+definition HTTgen :: "i set => i set" where
+ "HTTgen(R) ==
+ {t. t=true | t=false | (EX a b. t= <a, b> & a : R & b : R) |
+ (EX f. t = lam x. f(x) & (ALL x. f(x) : R))}"
-axioms
- (*** Definitions of Hereditary Termination ***)
-
- HTTgen_def:
- "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b> & a : R & b : R) |
- (EX f. t=lam x. f(x) & (ALL x. f(x) : R))}"
- HTT_def: "HTT == gfp(HTTgen)"
+definition HTT :: "i set"
+ where "HTT == gfp(HTTgen)"
subsection {* Hereditary Termination *}
--- a/src/CCL/Set.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Set.thy Tue Mar 29 23:46:46 2011 +0200
@@ -46,9 +46,9 @@
"ALL x:A. P" == "CONST Ball(A, %x. P)"
"EX x:A. P" == "CONST Bex(A, %x. P)"
-axioms
- mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)"
- set_extension: "A=B <-> (ALL x. x:A <-> x:B)"
+axiomatization where
+ mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)" and
+ set_extension: "A = B <-> (ALL x. x:A <-> x:B)"
defs
Ball_def: "Ball(A, P) == ALL x. x:A --> P(x)"
--- a/src/CCL/Term.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Term.thy Tue Mar 29 23:46:46 2011 +0200
@@ -111,8 +111,7 @@
consts
napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56)
-axioms
-
+defs
one_def: "one == true"
if_def: "if b then t else u == case(b,t,u,% x y. bot,%v. bot)"
inl_def: "inl(a) == <true,a>"
--- a/src/CCL/Trancl.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Trancl.thy Tue Mar 29 23:46:46 2011 +0200
@@ -9,21 +9,20 @@
imports CCL
begin
-consts
- trans :: "i set => o" (*transitivity predicate*)
- id :: "i set"
- rtrancl :: "i set => i set" ("(_^*)" [100] 100)
- trancl :: "i set => i set" ("(_^+)" [100] 100)
- relcomp :: "[i set,i set] => i set" (infixr "O" 60)
+definition trans :: "i set => o" (*transitivity predicate*)
+ where "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
+
+definition id :: "i set" (*the identity relation*)
+ where "id == {p. EX x. p = <x,x>}"
-axioms
- trans_def: "trans(r) == (ALL x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
- relcomp_def: (*composition of relations*)
- "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
- id_def: (*the identity relation*)
- "id == {p. EX x. p = <x,x>}"
- rtrancl_def: "r^* == lfp(%s. id Un (r O s))"
- trancl_def: "r^+ == r O rtrancl(r)"
+definition relcomp :: "[i set,i set] => i set" (infixr "O" 60) (*composition of relations*)
+ where "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
+
+definition rtrancl :: "i set => i set" ("(_^*)" [100] 100)
+ where "r^* == lfp(%s. id Un (r O s))"
+
+definition trancl :: "i set => i set" ("(_^+)" [100] 100)
+ where "r^+ == r O rtrancl(r)"
subsection {* Natural deduction for @{text "trans(r)"} *}
--- a/src/CCL/Type.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/Type.thy Tue Mar 29 23:46:46 2011 +0200
@@ -50,7 +50,7 @@
(@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
*}
-axioms
+defs
Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"
Unit_def: "Unit == {x. x=one}"
Bool_def: "Bool == {x. x=true | x=false}"
--- a/src/CCL/ex/Flag.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/ex/Flag.thy Tue Mar 29 23:46:46 2011 +0200
@@ -10,24 +10,24 @@
imports List
begin
-consts
- Colour :: "i set"
- red :: "i"
- white :: "i"
- blue :: "i"
- ccase :: "[i,i,i,i]=>i"
- flag :: "i"
+definition Colour :: "i set"
+ where "Colour == Unit + Unit + Unit"
+
+definition red :: "i"
+ where "red == inl(one)"
+
+definition white :: "i"
+ where "white == inr(inl(one))"
-axioms
+definition blue :: "i"
+ where "blue == inr(inr(one))"
- Colour_def: "Colour == Unit + Unit + Unit"
- red_def: "red == inl(one)"
- white_def: "white == inr(inl(one))"
- blue_def: "blue == inr(inr(one))"
+definition ccase :: "[i,i,i,i]=>i"
+ where "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
- ccase_def: "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
-
- flag_def: "flag == lam l. letrec
+definition flag :: "i"
+ where
+ "flag == lam l. letrec
flagx l be lcase(l,<[],<[],[]>>,
%h t. split(flagx(t),%lr p. split(p,%lw lb.
ccase(h, <red$lr,<lw,lb>>,
@@ -35,13 +35,14 @@
<lr,<lw,blue$lb>>))))
in flagx(l)"
- Flag_def:
- "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour).
- x = <lr,<lw,lb>> -->
- (ALL c:Colour.(c mem lr = true --> c=red) &
- (c mem lw = true --> c=white) &
- (c mem lb = true --> c=blue)) &
- Perm(l,lr @ lw @ lb)"
+axiomatization Perm :: "i => i => o"
+definition Flag :: "i => i => o" where
+ "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour).
+ x = <lr,<lw,lb>> -->
+ (ALL c:Colour.(c mem lr = true --> c=red) &
+ (c mem lw = true --> c=white) &
+ (c mem lb = true --> c=blue)) &
+ Perm(l,lr @ lw @ lb)"
lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def
@@ -68,7 +69,7 @@
apply assumption
done
-lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}"
+lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).Flag(x,l)}"
apply (unfold flag_def)
apply (tactic {* gen_ccs_tac @{context}
[@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
--- a/src/CCL/ex/List.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/ex/List.thy Tue Mar 29 23:46:46 2011 +0200
@@ -9,46 +9,47 @@
imports Nat
begin
-consts
- map :: "[i=>i,i]=>i"
- comp :: "[i=>i,i=>i]=>i=>i" (infixr "o" 55)
- append :: "[i,i]=>i" (infixr "@" 55)
- member :: "[i,i]=>i" (infixr "mem" 55)
- filter :: "[i,i]=>i"
- flat :: "i=>i"
- partition :: "[i,i]=>i"
- insert :: "[i,i,i]=>i"
- isort :: "i=>i"
- qsort :: "i=>i"
+definition map :: "[i=>i,i]=>i"
+ where "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"
+
+definition comp :: "[i=>i,i=>i]=>i=>i" (infixr "\<circ>" 55)
+ where "f \<circ> g == (%x. f(g(x)))"
+
+definition append :: "[i,i]=>i" (infixr "@" 55)
+ where "l @ m == lrec(l,m,%x xs g. x$g)"
-axioms
+axiomatization member :: "[i,i]=>i" (infixr "mem" 55) (* FIXME dangling eq *)
+ where "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
- map_def: "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"
- comp_def: "f o g == (%x. f(g(x)))"
- append_def: "l @ m == lrec(l,m,%x xs g. x$g)"
- member_def: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
- filter_def: "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
- flat_def: "flat(l) == lrec(l,[],%h t g. h @ g)"
+definition filter :: "[i,i]=>i"
+ where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
- insert_def: "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
- isort_def: "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
+definition flat :: "i=>i"
+ where "flat(l) == lrec(l,[],%h t g. h @ g)"
- partition_def:
+definition partition :: "[i,i]=>i" where
"partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
if f`x then part(xs,x$a,b) else part(xs,a,x$b))
in part(l,[],[])"
- qsort_def: "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
+
+definition insert :: "[i,i,i]=>i"
+ where "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
+
+definition isort :: "i=>i"
+ where "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
+
+definition qsort :: "i=>i" where
+ "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
let p be partition(f`h,t)
in split(p,%x y. qsortx(x) @ h$qsortx(y)))
in qsortx(l)"
-
lemmas list_defs = map_def comp_def append_def filter_def flat_def
insert_def isort_def partition_def qsort_def
lemma listBs [simp]:
- "!!f g. (f o g) = (%a. f(g(a)))"
- "!!a f g. (f o g)(a) = f(g(a))"
+ "!!f g. (f \<circ> g) = (%a. f(g(a)))"
+ "!!a f g. (f \<circ> g)(a) = f(g(a))"
"!!f. map(f,[]) = []"
"!!f x xs. map(f,x$xs) = f(x)$map(f,xs)"
"!!m. [] @ m = m"
@@ -85,7 +86,7 @@
lemma appendTS:
"[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}"
- by (blast intro!: SubtypeI appendT elim!: SubtypeE)
+ by (blast intro!: appendT)
lemma filterT: "[| f:A->Bool; l : List(A) |] ==> filter(f,l) : List(A)"
apply (unfold filter_def)
@@ -105,7 +106,7 @@
lemma insertTS:
"[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==>
insert(f,a,l) : {x:List(A). P(x)}"
- by (blast intro!: SubtypeI insertT elim!: SubtypeE)
+ by (blast intro!: insertT)
lemma partitionT:
"[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)"
--- a/src/CCL/ex/Nat.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/ex/Nat.thy Tue Mar 29 23:46:46 2011 +0200
@@ -9,37 +9,44 @@
imports Wfd
begin
-consts
+definition not :: "i=>i"
+ where "not(b) == if b then false else true"
+
+definition add :: "[i,i]=>i" (infixr "#+" 60)
+ where "a #+ b == nrec(a,b,%x g. succ(g))"
- not :: "i=>i"
- add :: "[i,i]=>i" (infixr "#+" 60)
- mult :: "[i,i]=>i" (infixr "#*" 60)
- sub :: "[i,i]=>i" (infixr "#-" 60)
- div :: "[i,i]=>i" (infixr "##" 60)
- lt :: "[i,i]=>i" (infixr "#<" 60)
- le :: "[i,i]=>i" (infixr "#<=" 60)
- ackermann :: "[i,i]=>i"
+definition mult :: "[i,i]=>i" (infixr "#*" 60)
+ where "a #* b == nrec(a,zero,%x g. b #+ g)"
-defs
-
- not_def: "not(b) == if b then false else true"
+definition sub :: "[i,i]=>i" (infixr "#-" 60)
+ where
+ "a #- b ==
+ letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy)))
+ in sub(a,b)"
- add_def: "a #+ b == nrec(a,b,%x g. succ(g))"
- mult_def: "a #* b == nrec(a,zero,%x g. b #+ g)"
- sub_def: "a #- b == letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy)))
- in sub(a,b)"
- le_def: "a #<= b == letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy)))
- in le(a,b)"
- lt_def: "a #< b == not(b #<= a)"
+definition le :: "[i,i]=>i" (infixr "#<=" 60)
+ where
+ "a #<= b ==
+ letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy)))
+ in le(a,b)"
+
+definition lt :: "[i,i]=>i" (infixr "#<" 60)
+ where "a #< b == not(b #<= a)"
- div_def: "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y))
- in div(a,b)"
- ack_def:
- "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x.
- ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))
- in ack(a,b)"
+definition div :: "[i,i]=>i" (infixr "##" 60)
+ where
+ "a ## b ==
+ letrec div x y be if x #< y then zero else succ(div(x#-y,y))
+ in div(a,b)"
-lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ack_def napply_def
+definition ackermann :: "[i,i]=>i"
+ where
+ "ackermann(a,b) ==
+ letrec ack n m be ncase(n,succ(m),%x.
+ ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))
+ in ack(a,b)"
+
+lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ackermann_def napply_def
lemma natBs [simp]:
"not(true) = false"
@@ -94,7 +101,7 @@
lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]
lemma "[| a:Nat; b:Nat |] ==> ackermann(a,b) : Nat"
- apply (unfold ack_def)
+ apply (unfold ackermann_def)
apply (tactic {* gen_ccs_tac @{context} [] 1 *})
apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
done
--- a/src/CCL/ex/Stream.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/CCL/ex/Stream.thy Tue Mar 29 23:46:46 2011 +0200
@@ -9,15 +9,11 @@
imports List
begin
-consts
- iter1 :: "[i=>i,i]=>i"
- iter2 :: "[i=>i,i]=>i"
+definition iter1 :: "[i=>i,i]=>i"
+ where "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
-defs
-
- iter1_def: "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)"
- iter2_def: "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
-
+definition iter2 :: "[i=>i,i]=>i"
+ where "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)"
(*
Proving properties about infinite lists using coinduction:
@@ -30,9 +26,9 @@
lemma map_comp:
assumes 1: "l:Lists(A)"
- shows "map(f o g,l) = map(f,map(g,l))"
+ shows "map(f \<circ> g,l) = map(f,map(g,l))"
apply (tactic {* eq_coinduct3_tac @{context}
- "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f o g,l) & y=map (f,map (g,l)))}" 1 *})
+ "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f \<circ> g,l) & y=map (f,map (g,l)))}" 1 *})
apply (blast intro: 1)
apply safe
apply (drule ListsXH [THEN iffD1])
--- a/src/HOL/Hoare/Examples.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/Hoare/Examples.thy Tue Mar 29 23:46:46 2011 +0200
@@ -90,7 +90,7 @@
{c = A^B}"
apply vcg_simp
apply(case_tac "b")
- apply(simp add: mod_less)
+ apply simp
apply simp
done
--- a/src/HOL/Hoare/ExamplesAbort.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/Hoare/ExamplesAbort.thy Tue Mar 29 23:46:46 2011 +0200
@@ -14,8 +14,7 @@
lemma
"VARS a i j
{k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
-apply vcg_simp
-done
+by vcg_simp
lemma "VARS (a::int list) i
{True}
@@ -24,7 +23,6 @@
INV {i <= length a}
DO a[i] := 7; i := i+1 OD
{True}"
-apply vcg_simp
-done
+by vcg_simp
end
--- a/src/HOL/Hoare/Hoare_Logic.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy Tue Mar 29 23:46:46 2011 +0200
@@ -10,7 +10,7 @@
theory Hoare_Logic
imports Main
-uses ("hoare_tac.ML")
+uses ("hoare_syntax.ML") ("hoare_tac.ML")
begin
types
@@ -45,11 +45,8 @@
where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)"
-
-(** parse translations **)
-
syntax
- "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61)
+ "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61)
syntax
"_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
@@ -57,147 +54,11 @@
syntax ("" output)
"_hoare" :: "['a assn,'a com,'a assn] => bool"
("{_} // _ // {_}" [0,55,0] 50)
-ML {*
-
-local
-
-fun abs((a,T),body) =
- let val a = absfree(a, dummyT, body)
- in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end
-in
-
-fun mk_abstuple [x] body = abs (x, body)
- | mk_abstuple (x::xs) body =
- Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
-
-fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
- | mk_fbody a e ((b,_)::xs) =
- Syntax.const @{const_syntax Pair} $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs;
-
-fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
-end
-*}
-
-(* bexp_tr & assn_tr *)
-(*all meta-variables for bexp except for TRUE are translated as if they
- were boolean expressions*)
-ML{*
-fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *)
- | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
-
-fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
-*}
-(* com_tr *)
-ML{*
-fun com_tr (t as (Const(@{syntax_const "_assign"},_) $ x $ e)) xs =
- (case Syntax.strip_positions x of
- Free (a, _) => Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
- | _ => t)
- | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
- | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
- Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
- Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
- Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
- | com_tr t _ = t (* if t is just a Free/Var *)
-*}
-
-(* triple_tr *) (* FIXME does not handle "_idtdummy" *)
-ML{*
-local
-
-fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *)
- | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T);
-
-fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) =
- var_tr (Syntax.strip_positions idt) :: vars_tr vars
- | vars_tr t = [var_tr (Syntax.strip_positions t)]
-
-in
-fun hoare_vars_tr [vars, pre, prg, post] =
- let val xs = vars_tr vars
- in Syntax.const @{const_syntax Valid} $
- assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
- end
- | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
-end
-*}
-
-parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *}
-
-(*****************************************************************************)
-
-(*** print translations ***)
-ML{*
-fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
- subst_bound (Syntax.free v, dest_abstuple body)
- | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
- | dest_abstuple trm = trm;
-
-fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
- | abs2list (Abs(x,T,t)) = [Free (x, T)]
- | abs2list _ = [];
-
-fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
- | mk_ts (Abs(x,_,t)) = mk_ts t
- | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
- | mk_ts t = [t];
-
-fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
- ((Syntax.free x)::(abs2list t), mk_ts t)
- | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
- | mk_vts t = raise Match;
-
-fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
- | find_ch ((v,t)::vts) i xs =
- if t = Bound i then find_ch vts (i-1) xs
- else (true, (v, subst_bounds (xs, t)));
-
-fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
- | is_f (Abs(x,_,t)) = true
- | is_f t = false;
-*}
+use "hoare_syntax.ML"
+parse_translation {* [(@{syntax_const "_hoare_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
+print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare"})] *}
-(* assn_tr' & bexp_tr'*)
-ML{*
-fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
- | assn_tr' (Const (@{const_syntax inter}, _) $
- (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) =
- Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
- | assn_tr' t = t;
-
-fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
- | bexp_tr' t = t;
-*}
-
-(*com_tr' *)
-ML{*
-fun mk_assign f =
- let val (vs, ts) = mk_vts f;
- val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
- in
- if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
- else Syntax.const @{const_syntax annskip}
- end;
-
-fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
- if is_f f then mk_assign f
- else Syntax.const @{const_syntax Basic} $ f
- | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
- Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
- Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
- Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
- | com_tr' t = t;
-
-fun spec_tr' [p, c, q] =
- Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q
-*}
-
-print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp:Valid_def)
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Mar 29 23:46:46 2011 +0200
@@ -7,7 +7,7 @@
theory Hoare_Logic_Abort
imports Main
-uses ("hoare_tac.ML")
+uses ("hoare_syntax.ML") ("hoare_tac.ML")
begin
types
@@ -47,11 +47,8 @@
"Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
-
-(** parse translations **)
-
syntax
- "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61)
+ "_assign" :: "idt => 'b => 'a com" ("(2_ :=/ _)" [70, 65] 61)
syntax
"_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
@@ -59,146 +56,12 @@
syntax ("" output)
"_hoare_abort" :: "['a assn,'a com,'a assn] => bool"
("{_} // _ // {_}" [0,55,0] 50)
-ML {*
-
-local
-fun free a = Free(a,dummyT)
-fun abs((a,T),body) =
- let val a = absfree(a, dummyT, body)
- in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end
-in
-
-fun mk_abstuple [x] body = abs (x, body)
- | mk_abstuple (x::xs) body =
- Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
-
-fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
- | mk_fbody a e ((b,_)::xs) =
- Syntax.const @{const_syntax Pair} $ (if a=b then e else free b) $ mk_fbody a e xs;
-
-fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs)
-end
-*}
-
-(* bexp_tr & assn_tr *)
-(*all meta-variables for bexp except for TRUE are translated as if they
- were boolean expressions*)
-ML{*
-fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *)
- | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
-
-fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
-*}
-(* com_tr *)
-ML{*
-fun com_tr (t as (Const (@{syntax_const "_assign"},_) $ x $ e)) xs =
- (case Syntax.strip_positions x of
- Free (a, _) => Syntax.const @{const_syntax Basic} $ mk_fexp a e xs
- | _ => t)
- | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
- | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
- Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
- Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
- | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
- Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
- | com_tr t _ = t (* if t is just a Free/Var *)
-*}
-
-(* triple_tr *) (* FIXME does not handle "_idtdummy" *)
-ML{*
-local
-
-fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *)
- | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T);
-
-fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) =
- var_tr (Syntax.strip_positions idt) :: vars_tr vars
- | vars_tr t = [var_tr (Syntax.strip_positions t)]
-
-in
-fun hoare_vars_tr [vars, pre, prg, post] =
- let val xs = vars_tr vars
- in Syntax.const @{const_syntax Valid} $
- assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
- end
- | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
-end
-*}
-
-parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, hoare_vars_tr)] *}
-
-(*****************************************************************************)
-
-(*** print translations ***)
-ML{*
-fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
- subst_bound (Syntax.free v, dest_abstuple body)
- | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
- | dest_abstuple trm = trm;
-
-fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
- | abs2list (Abs(x,T,t)) = [Free (x, T)]
- | abs2list _ = [];
-
-fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
- | mk_ts (Abs(x,_,t)) = mk_ts t
- | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
- | mk_ts t = [t];
-
-fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
- ((Syntax.free x)::(abs2list t), mk_ts t)
- | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
- | mk_vts t = raise Match;
-
-fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))
- | find_ch ((v,t)::vts) i xs =
- if t = Bound i then find_ch vts (i-1) xs
- else (true, (v, subst_bounds (xs,t)));
-
-fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
- | is_f (Abs(x,_,t)) = true
- | is_f t = false;
-*}
+use "hoare_syntax.ML"
+parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
+print_translation
+ {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"})] *}
-(* assn_tr' & bexp_tr'*)
-ML{*
-fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
- | assn_tr' (Const (@{const_syntax inter},_) $ (Const (@{const_syntax Collect},_) $ T1) $
- (Const (@{const_syntax Collect},_) $ T2)) =
- Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
- | assn_tr' t = t;
-
-fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T
- | bexp_tr' t = t;
-*}
-
-(*com_tr' *)
-ML{*
-fun mk_assign f =
- let val (vs, ts) = mk_vts f;
- val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
- in
- if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
- else Syntax.const @{const_syntax annskip}
- end;
-
-fun com_tr' (Const (@{const_syntax Basic},_) $ f) =
- if is_f f then mk_assign f else Syntax.const @{const_syntax Basic} $ f
- | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
- Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) =
- Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
- | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) =
- Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
- | com_tr' t = t;
-
-fun spec_tr' [p, c, q] =
- Syntax.const @{syntax_const "_hoare_abort"} $ assn_tr' p $ com_tr' c $ assn_tr' q
-*}
-
-print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
(*** The proof rules ***)
--- a/src/HOL/Hoare/SchorrWaite.thy Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy Tue Mar 29 23:46:46 2011 +0200
@@ -40,7 +40,7 @@
done
lemma still_reachable: "\<lbrakk>B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Rb\<^sup>* `` B \<subseteq> Ra\<^sup>* `` A "
-apply (clarsimp simp only:Image_iff intro:subsetI)
+apply (clarsimp simp only:Image_iff)
apply (erule rtrancl_induct)
apply blast
apply (subgoal_tac "(y, z) \<in> Ra\<union>(Rb-Ra)")
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/hoare_syntax.ML Tue Mar 29 23:46:46 2011 +0200
@@ -0,0 +1,156 @@
+(* Title: HOL/Hoare/hoare_syntax.ML
+ Author: Leonor Prensa Nieto & Tobias Nipkow
+
+Syntax translations for Hoare logic.
+*)
+
+signature HOARE_SYNTAX =
+sig
+ val hoare_vars_tr: term list -> term
+ val spec_tr': string -> term list -> term
+end;
+
+structure Hoare_Syntax: HOARE_SYNTAX =
+struct
+
+(** parse translation **)
+
+local
+
+fun idt_name (Free (x, _)) = SOME x
+ | idt_name (Const ("_constrain", _) $ t $ _) = idt_name t
+ | idt_name _ = NONE;
+
+fun eq_idt tu =
+ (case pairself idt_name tu of
+ (SOME x, SOME y) => x = y
+ | _ => false);
+
+fun mk_abstuple [x] body = Syntax.abs_tr [x, body]
+ | mk_abstuple (x :: xs) body =
+ Syntax.const @{const_syntax prod_case} $ Syntax.abs_tr [x, mk_abstuple xs body];
+
+fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
+ | mk_fbody x e (y :: xs) =
+ Syntax.const @{const_syntax Pair} $
+ (if eq_idt (x, y) then e else y) $ mk_fbody x e xs;
+
+fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
+
+
+(* bexp_tr & assn_tr *)
+(*all meta-variables for bexp except for TRUE are translated as if they
+ were boolean expressions*)
+
+fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *)
+ | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b;
+
+fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r;
+
+
+(* com_tr *)
+
+fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs =
+ Syntax.const @{const_syntax Basic} $ mk_fexp x e xs
+ | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f
+ | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs =
+ Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs
+ | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs =
+ Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs
+ | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs =
+ Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs
+ | com_tr t _ = t;
+
+fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars
+ | vars_tr t = [t];
+
+in
+
+fun hoare_vars_tr [vars, pre, prg, post] =
+ let val xs = vars_tr vars
+ in Syntax.const @{const_syntax Valid} $
+ assn_tr pre xs $ com_tr prg xs $ assn_tr post xs
+ end
+ | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
+
+end;
+
+
+
+(** print translation **)
+
+local
+
+fun dest_abstuple
+ (Const (@{const_syntax prod_case}, _) $ Abs (v, _, body)) =
+ subst_bound (Syntax.free v, dest_abstuple body)
+ | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
+ | dest_abstuple tm = tm;
+
+fun abs2list (Const (@{const_syntax prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+ | abs2list (Abs (x, T, t)) = [Free (x, T)]
+ | abs2list _ = [];
+
+fun mk_ts (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = mk_ts t
+ | mk_ts (Abs (x, _, t)) = mk_ts t
+ | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b
+ | mk_ts t = [t];
+
+fun mk_vts (Const (@{const_syntax prod_case},_) $ Abs (x, _, t)) =
+ (Syntax.free x :: abs2list t, mk_ts t)
+ | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
+ | mk_vts t = raise Match;
+
+fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) (* FIXME no_ch!? *)
+ | find_ch ((v, t) :: vts) i xs =
+ if t = Bound i then find_ch vts (i - 1) xs
+ else (true, (v, subst_bounds (xs, t)));
+
+fun is_f (Const (@{const_syntax prod_case}, _) $ Abs (x, _, t)) = true
+ | is_f (Abs (x, _, t)) = true
+ | is_f t = false;
+
+
+(* assn_tr' & bexp_tr'*)
+
+fun assn_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
+ | assn_tr' (Const (@{const_syntax inter}, _) $
+ (Const (@{const_syntax Collect}, _) $ T1) $ (Const (@{const_syntax Collect}, _) $ T2)) =
+ Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2
+ | assn_tr' t = t;
+
+fun bexp_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T
+ | bexp_tr' t = t;
+
+
+(* com_tr' *)
+
+fun mk_assign f =
+ let
+ val (vs, ts) = mk_vts f;
+ val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
+ in
+ if ch
+ then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which
+ else Syntax.const @{const_syntax annskip}
+ end;
+
+fun com_tr' (Const (@{const_syntax Basic}, _) $ f) =
+ if is_f f then mk_assign f
+ else Syntax.const @{const_syntax Basic} $ f
+ | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) =
+ Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2
+ | com_tr' (Const (@{const_syntax Cond}, _) $ b $ c1 $ c2) =
+ Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2
+ | com_tr' (Const (@{const_syntax While}, _) $ b $ I $ c) =
+ Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c
+ | com_tr' t = t;
+
+in
+
+fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q
+
+end;
+
+end;
+
--- a/src/HOL/IsaMakefile Tue Mar 29 22:06:53 2011 +0200
+++ b/src/HOL/IsaMakefile Tue Mar 29 23:46:46 2011 +0200
@@ -650,12 +650,12 @@
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \
- Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy \
- Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \
+ Hoare/Hoare.thy Hoare/hoare_syntax.ML Hoare/hoare_tac.ML \
+ Hoare/Heap.thy Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \
Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \
Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \
- Hoare/SchorrWaite.thy Hoare/Separation.thy \
- Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib
+ Hoare/SchorrWaite.thy Hoare/Separation.thy Hoare/SepLogHeap.thy \
+ Hoare/document/root.tex Hoare/document/root.bib
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
--- a/src/Pure/Syntax/syn_trans.ML Tue Mar 29 22:06:53 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Tue Mar 29 23:46:46 2011 +0200
@@ -36,6 +36,7 @@
val non_typed_tr': (term list -> term) -> bool -> typ -> term list -> term
val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
val constrainAbsC: string
+ val abs_tr: term list -> term
val pure_trfuns:
(string * (Ast.ast list -> Ast.ast)) list *
(string * (term list -> term)) list *
@@ -97,7 +98,6 @@
fun idtypdummy_ast_tr (*"_idtypdummy"*) [ty] =
Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]
| idtypdummy_ast_tr (*"_idtypdummy"*) asts = raise Ast.AST ("idtyp_ast_tr", asts);
-
fun lambda_ast_tr (*"_lambda"*) [pats, body] =
Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
| lambda_ast_tr (*"_lambda"*) asts = raise Ast.AST ("lambda_ast_tr", asts);