--- a/src/HOL/Finite_Set.thy Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/Finite_Set.thy Fri Nov 29 09:48:28 2002 +0100
@@ -11,20 +11,23 @@
subsection {* Collection of finite sets *}
consts Finites :: "'a set set"
+syntax
+ finite :: "'a set => bool"
+translations
+ "finite A" == "A : Finites"
inductive Finites
intros
emptyI [simp, intro!]: "{} : Finites"
insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
-syntax
- finite :: "'a set => bool"
-translations
- "finite A" == "A : Finites"
-
axclass finite \<subseteq> type
finite: "finite UNIV"
+lemma ex_new_if_finite: -- "does not depend on def of finite at all"
+ "\<lbrakk> ~finite(UNIV::'a set); finite A \<rbrakk> \<Longrightarrow> \<exists>a::'a. a ~: A"
+by(subgoal_tac "A ~= UNIV", blast, blast)
+
lemma finite_induct [case_names empty insert, induct set: Finites]:
"finite F ==>
--- a/src/HOL/Hoare/Examples.thy Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/Hoare/Examples.thy Fri Nov 29 09:48:28 2002 +0100
@@ -12,7 +12,7 @@
(** multiplication by successive addition **)
-lemma multiply_by_add: "|- VARS m s a b.
+lemma multiply_by_add: "VARS m s a b
{a=A & b=B}
m := 0; s := 0;
WHILE m~=a
@@ -24,7 +24,7 @@
(** Euclid's algorithm for GCD **)
-lemma Euclid_GCD: "|- VARS a b.
+lemma Euclid_GCD: "VARS a b
{0<A & 0<B}
a := A; b := B;
WHILE a~=b
@@ -49,7 +49,7 @@
lemmas distribs =
diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2
-lemma gcd_scm: "|- VARS a b x y.
+lemma gcd_scm: "VARS a b x y
{0<A & 0<B & a=A & b=B & x=B & y=A}
WHILE a ~= b
INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
@@ -64,7 +64,7 @@
(** Power by iterated squaring and multiplication **)
-lemma power_by_mult: "|- VARS a b c.
+lemma power_by_mult: "VARS a b c
{a=A & b=B}
c := (1::nat);
WHILE b ~= 0
@@ -83,7 +83,7 @@
(** Factorial **)
-lemma factorial: "|- VARS a b.
+lemma factorial: "VARS a b
{a=A}
b := 1;
WHILE a ~= 0
@@ -97,7 +97,7 @@
lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
by(induct i, simp_all)
-lemma "|- VARS i f.
+lemma "VARS i f
{True}
i := (1::nat); f := 1;
WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
@@ -113,7 +113,7 @@
(* the easy way: *)
-lemma sqrt: "|- VARS r x.
+lemma sqrt: "VARS r x
{True}
x := X; r := (0::nat);
WHILE (r+1)*(r+1) <= x
@@ -126,7 +126,7 @@
(* without multiplication *)
-lemma sqrt_without_multiplication: "|- VARS u w r x.
+lemma sqrt_without_multiplication: "VARS u w r x
{True}
x := X; u := 1; w := 1; r := (0::nat);
WHILE w <= x
@@ -140,7 +140,7 @@
(*** LISTS ***)
-lemma imperative_reverse: "|- VARS y x.
+lemma imperative_reverse: "VARS y x
{x=X}
y:=[];
WHILE x ~= []
@@ -152,7 +152,7 @@
apply auto
done
-lemma imperative_append: "|- VARS x y.
+lemma imperative_append: "VARS x y
{x=X & y=Y}
x := rev(x);
WHILE x~=[]
@@ -170,7 +170,7 @@
(*** ARRAYS ***)
(* Search for a key *)
-lemma zero_search: "|- VARS A i.
+lemma zero_search: "VARS A i
{True}
i := 0;
WHILE i < length A & A!i ~= key
@@ -198,7 +198,7 @@
lemma Partition:
"[| leq == %A i. !k. k<i --> A!k <= pivot;
geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
- |- VARS A u l.
+ VARS A u l
{0 < length(A::('a::order)list)}
l := 0; u := length A - Suc 0;
WHILE l <= u
--- a/src/HOL/Hoare/Hoare.thy Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/Hoare/Hoare.thy Fri Nov 29 09:48:28 2002 +0100
@@ -57,10 +57,10 @@
syntax
"@hoare_vars" :: "[vars, 'a assn,'a com,'a assn] => bool"
- ("|- VARS _.// {_} // _ // {_}" [0,0,55,0] 50)
+ ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
syntax ("" output)
"@hoare" :: "['a assn,'a com,'a assn] => bool"
- ("|- {_} // _ // {_}" [0,55,0] 50)
+ ("{_} // _ // {_}" [0,55,0] 50)
(** parse translations **)
--- a/src/HOL/Hoare/Pointers.thy Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/Hoare/Pointers.thy Fri Nov 29 09:48:28 2002 +0100
@@ -5,8 +5,6 @@
How to use Hoare logic to verify pointer manipulating programs.
The old idea: the store is a global mapping from pointers to values.
-Pointers are modelled by type 'a option, where None is Nil.
-Thus the heap is of type 'a \<leadsto> 'a (see theory Map).
The list reversal example is taken from Richard Bornat's paper
Proving pointer programs in Hoare logic
@@ -16,19 +14,20 @@
theory Pointers = Hoare:
-section "Syntactic sugar"
+subsection "References"
-types 'a ref = "'a option"
+datatype 'a ref = Null | Ref 'a
+
+lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
+ by (induct x) auto
-syntax Null :: "'a ref"
- Ref :: "'a \<Rightarrow> 'a ref"
- addr :: "'a ref \<Rightarrow> 'a"
-translations
- "Null" => "None"
- "Ref" => "Some"
- "addr" => "the"
+lemma not_Ref_eq [iff]: "(ALL y. x ~= Ref y) = (x = Null)"
+ by (induct x) auto
-text "Field access and update:"
+consts addr :: "'a ref \<Rightarrow> 'a"
+primrec "addr(Ref a) = a"
+
+subsection "Field access and update"
syntax
"@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
@@ -38,14 +37,14 @@
"@faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
("_^._" [65,1000] 65)
translations
- "f(r \<rightarrow> v)" == "f(the r := v)"
+ "f(r \<rightarrow> v)" == "f(addr r := v)"
"p^.f := e" => "f := f(p \<rightarrow> e)"
- "p^.f" == "f(the p)"
+ "p^.f" == "f(addr p)"
text "An example due to Suzuki:"
-lemma "|- VARS v n.
+lemma "VARS v n
{w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
distinct[w0,x0,y0,z0]}
w^.v := (1::int); w^.n := x;
@@ -61,7 +60,7 @@
subsection "Paths in the heap"
consts
- Path :: "('a \<leadsto> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
+ Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
primrec
"Path h x [] y = (x = y)"
"Path h x (a#as) y = (x = Ref a \<and> Path h (h a) as y)"
@@ -82,7 +81,7 @@
lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
by(induct as, simp+)
-lemma [simp]: "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u\<mapsto>v)) x as y = Path f x as y"
+lemma [simp]: "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
by(induct as, simp, simp add:eq_sym_conv)
subsection "Lists on the heap"
@@ -90,7 +89,7 @@
subsubsection "Relational abstraction"
constdefs
- List :: "('a \<leadsto> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> bool"
+ List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
"List h x as == Path h x as Null"
lemma [simp]: "List h x [] = (x = Null)"
@@ -157,16 +156,17 @@
apply fast
done
-lemma [simp]: "islist h None"
+lemma [simp]: "islist h Null"
+by(simp add:islist_def)
+
+lemma [simp]: "islist h (Ref a) = islist h (h a)"
by(simp add:islist_def)
-lemma [simp]: "islist h (Some a) = islist h (h a)"
-by(simp add:islist_def)
-
-lemma [simp]: "list h None = []"
+lemma [simp]: "list h Null = []"
by(simp add:list_def)
-lemma [simp]: "islist h (h a) \<Longrightarrow> list h (Some a) = a # list h (h a)"
+lemma list_Ref_conv[simp]:
+ "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
apply(insert List_Ref[of h])
apply(fastsimp simp:List_conv_islist_list)
done
@@ -176,13 +176,13 @@
apply(simp add:List_conv_islist_list)
done
-lemma [simp]:
+lemma list_upd_conv[simp]:
"islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
apply(drule notin_List_update[of _ _ h q p])
apply(simp add:List_conv_islist_list)
done
-lemma [simp]:
+lemma islist_upd[simp]:
"islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
apply(frule notin_List_update[of _ _ h q p])
apply(simp add:List_conv_islist_list)
@@ -195,7 +195,7 @@
text "A short but unreadable proof:"
-lemma "|- VARS tl p q r.
+lemma "VARS tl p q r
{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
WHILE p \<noteq> Null
INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
@@ -218,7 +218,7 @@
text "A longer readable version:"
-lemma "|- VARS tl p q r.
+lemma "VARS tl p q r
{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
WHILE p \<noteq> Null
INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
@@ -257,7 +257,7 @@
text{* Finaly, the functional version. A bit more verbose, but automatic! *}
-lemma "|- VARS tl p q r.
+lemma "VARS tl p q r
{islist tl p \<and> islist tl q \<and>
Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
WHILE p \<noteq> Null
@@ -281,7 +281,7 @@
We start with a proof based on the @{term List} predicate. This means it only
works for acyclic lists. *}
-lemma "|- VARS tl p.
+lemma "VARS tl p
{List tl p Ps \<and> X \<in> set Ps}
WHILE p \<noteq> Null \<and> p \<noteq> Ref X
INV {p \<noteq> Null \<and> (\<exists>ps. List tl p ps \<and> X \<in> set ps)}
@@ -299,7 +299,7 @@
text{*Using @{term Path} instead of @{term List} generalizes the correctness
statement to cyclic lists as well: *}
-lemma "|- VARS tl p.
+lemma "VARS tl p
{Path tl p Ps (Ref X)}
WHILE p \<noteq> Null \<and> p \<noteq> Ref X
INV {p \<noteq> Null \<and> (\<exists>ps. Path tl p ps (Ref X))}
@@ -332,7 +332,7 @@
apply simp
done
-lemma "|- VARS tl p.
+lemma "VARS tl p
{Ref X \<in> ({(Ref x,tl x) |x. True}^* `` {p})}
WHILE p \<noteq> Null \<and> p \<noteq> Ref X
INV {p \<noteq> Null \<and> Ref X \<in> ({(Ref x,tl x) |x. True}^* `` {p})}
@@ -351,10 +351,10 @@
text{*Finally, the simplest version, based on a relation on type @{typ 'a}:*}
-lemma "|- VARS tl p.
- {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {the p})}
+lemma "VARS tl p
+ {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {addr p})}
WHILE p \<noteq> Null \<and> p \<noteq> Ref X
- INV {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {the p})}
+ INV {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {addr p})}
DO p := p^.tl OD
{p = Ref X}"
apply vcg_simp
@@ -365,8 +365,11 @@
apply clarsimp
done
+
subsection "Merging two lists"
+text"This is still a bit rough, especially the proof."
+
consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
recdef merge "measure(%(xs,ys,f). size xs + size ys)"
@@ -381,7 +384,7 @@
declare imp_disjL[simp del] imp_disjCL[simp]
-lemma "|- VARS hd tl p q r s.
+lemma "VARS hd tl p q r s
{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
(p \<noteq> Null \<or> q \<noteq> Null)}
IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
@@ -450,6 +453,44 @@
apply(clarsimp simp add:List_app)
done
-(* TODO: functional version of merging *)
+(* TODO: merging with islist/list instead of List *)
+
+subsection "Storage allocation"
+
+constdefs new :: "'a set \<Rightarrow> 'a"
+"new A == SOME a. a \<notin> A"
+
+
+(* useful??*)
+syntax in_list :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("(_/ [\<in>] _)" [50, 51] 50)
+ notin_list :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("(_/ [\<notin>] _)" [50, 51] 50)
+translations
+ "x [\<in>] xs" == "x \<in> set xs"
+ "x [\<notin>] xs" == "x \<notin> set xs"
+
+lemma new_notin:
+ "\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> B"
+apply(unfold new_def)
+apply(rule someI2_ex)
+ apply (fast intro:ex_new_if_finite)
+apply (fast)
+done
+
+
+lemma "~finite(UNIV::'a set) \<Longrightarrow>
+ VARS xs elem next alloc p q
+ {Xs = xs \<and> p = (Null::'a ref)}
+ WHILE xs \<noteq> []
+ INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
+ map elem (rev(list next p)) @ xs = Xs}
+ DO q := Ref(new(set alloc)); alloc := (addr q)#alloc;
+ q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
+ OD
+ {islist next p \<and> map elem (rev(list next p)) = Xs}"
+apply vcg_simp
+ apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
+apply fastsimp
+done
+
end
--- a/src/HOL/Hoare/hoare.ML Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/Hoare/hoare.ML Fri Nov 29 09:48:28 2002 +0100
@@ -99,7 +99,7 @@
fun dest_Goal (Const ("Goal", _) $ P) = P;
(** maps a goal of the form:
- 1. [| P |] ==> |- VARS x1 ... xn. {._.} _ {._.} or to [x1,...,xn]**)
+ 1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**)
fun get_vars thm = let val c = dest_Goal (concl_of (thm));
val d = Logic.strip_assums_concl c;
val Const _ $ pre $ _ $ _ = dest_Trueprop d;
--- a/src/HOL/List.thy Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/List.thy Fri Nov 29 09:48:28 2002 +0100
@@ -431,10 +431,13 @@
lemma rev_map: "rev (map f xs) = map f (rev xs)"
by (induct xs) auto
+lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
+by (induct xs) auto
+
lemma map_cong [recdef_cong]:
"xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
-- {* a congruence rule for @{text map} *}
-by (clarify, induct ys) auto
+by simp
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
by (cases xs) auto
--- a/src/HOL/MicroJava/Comp/Index.thy Thu Nov 28 15:44:34 2002 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy Fri Nov 29 09:48:28 2002 +0100
@@ -75,7 +75,6 @@
apply (simp add: gl_def)
apply (intro strip, simp)
apply (simp add: galldefs del: set_append map_append)
-apply (auto simp: the_map_upd)
done