--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Pointer_Examples.thy Mon Jan 06 11:22:54 2003 +0100
@@ -0,0 +1,253 @@
+(* Title: HOL/Hoare/Pointers.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2002 TUM
+
+Examples of verifications of pointer programs
+*)
+
+theory Pointer_Examples = Pointers:
+
+section "Verifications"
+
+subsection "List reversal"
+
+text "A short but unreadable proof:"
+
+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>
+ rev ps @ qs = rev Ps @ Qs}
+ DO r := p; p := p^.tl; r^.tl := q; q := r OD
+ {List tl q (rev Ps @ Qs)}"
+apply vcg_simp
+ apply fastsimp
+ apply(fastsimp intro:notin_List_update[THEN iffD2])
+(* explicit:
+ apply clarify
+ apply(rename_tac ps b qs)
+ apply clarsimp
+ apply(rename_tac ps')
+ apply(fastsimp intro:notin_List_update[THEN iffD2])
+ apply(rule_tac x = ps' in exI)
+ apply simp
+ apply(rule_tac x = "b#qs" in exI)
+ apply simp
+*)
+apply fastsimp
+done
+
+
+text "A longer readable version:"
+
+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>
+ rev ps @ qs = rev Ps @ Qs}
+ DO r := p; p := p^.tl; r^.tl := q; q := r OD
+ {List tl q (rev Ps @ Qs)}"
+proof vcg
+ fix tl p q r
+ assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
+ thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
+ rev ps @ qs = rev Ps @ Qs" by fastsimp
+next
+ fix tl p q r
+ assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
+ rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
+ (is "(\<exists>ps qs. ?I ps qs) \<and> _")
+ then obtain ps qs a where I: "?I ps qs \<and> p = Ref a"
+ by fast
+ then obtain ps' where "ps = a # ps'" by fastsimp
+ hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
+ List (tl(p \<rightarrow> q)) p (a#qs) \<and>
+ set ps' \<inter> set (a#qs) = {} \<and>
+ rev ps' @ (a#qs) = rev Ps @ Qs"
+ using I by fastsimp
+ thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
+ List (tl(p \<rightarrow> q)) p qs' \<and>
+ set ps' \<inter> set qs' = {} \<and>
+ rev ps' @ qs' = rev Ps @ Qs" by fast
+next
+ fix tl p q r
+ assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
+ rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
+ thus "List tl q (rev Ps @ Qs)" by fastsimp
+qed
+
+
+text{* Finaly, the functional version. A bit more verbose, but automatic! *}
+
+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
+ INV {islist tl p \<and> islist tl q \<and>
+ set(list tl p) \<inter> set(list tl q) = {} \<and>
+ rev(list tl p) @ (list tl q) = rev Ps @ Qs}
+ DO r := p; p := p^.tl; r^.tl := q; q := r OD
+ {islist tl q \<and> list tl q = rev Ps @ Qs}"
+apply vcg_simp
+ apply clarsimp
+ apply clarsimp
+apply clarsimp
+done
+
+
+subsection "Searching in a list"
+
+text{*What follows is a sequence of successively more intelligent proofs that
+a simple loop finds an element in a linked list.
+
+We start with a proof based on the @{term List} predicate. This means it only
+works for acyclic lists. *}
+
+lemma "VARS tl p
+ {List tl p Ps \<and> X \<in> set Ps}
+ WHILE p \<noteq> Null \<and> p \<noteq> Ref X
+ INV {\<exists>ps. List tl p ps \<and> X \<in> set ps}
+ DO p := p^.tl OD
+ {p = Ref X}"
+apply vcg_simp
+ apply blast
+ apply clarsimp
+apply clarsimp
+done
+
+text{*Using @{term Path} instead of @{term List} generalizes the correctness
+statement to cyclic lists as well: *}
+
+lemma "VARS tl p
+ {Path tl p Ps X}
+ WHILE p \<noteq> Null \<and> p \<noteq> X
+ INV {\<exists>ps. Path tl p ps X}
+ DO p := p^.tl OD
+ {p = X}"
+apply vcg_simp
+ apply blast
+ apply fastsimp
+apply clarsimp
+done
+
+text{*Now it dawns on us that we do not need the list witness at all --- it
+suffices to talk about reachability, i.e.\ we can use relations directly. The
+first version uses a relation on @{typ"'a ref"}: *}
+
+lemma "VARS tl p
+ {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
+ WHILE p \<noteq> Null \<and> p \<noteq> X
+ INV {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
+ DO p := p^.tl OD
+ {p = X}"
+apply vcg_simp
+ apply clarsimp
+ apply(erule converse_rtranclE)
+ apply simp
+ apply(clarsimp elim:converse_rtranclE)
+apply(fast elim:converse_rtranclE)
+done
+
+text{*Finally, a version based on a relation on type @{typ 'a}:*}
+
+lemma "VARS tl p
+ {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
+ WHILE p \<noteq> Null \<and> p \<noteq> Ref X
+ INV {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
+ DO p := p^.tl OD
+ {p = Ref X}"
+apply vcg_simp
+ apply clarsimp
+ apply(erule converse_rtranclE)
+ apply simp
+ apply clarsimp
+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)"
+"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
+ else y # merge(x#xs,ys,f))"
+"merge(x#xs,[],f) = x # merge(xs,[],f)"
+"merge([],y#ys,f) = y # merge([],ys,f)"
+"merge([],[],f) = []"
+
+lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"
+by blast
+
+declare imp_disjL[simp del] imp_disjCL[simp]
+
+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
+ THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
+ s := r;
+ WHILE p \<noteq> Null \<or> q \<noteq> Null
+ INV {EX rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
+ distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
+ merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
+ rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
+ (tl a = p \<or> tl a = q)}
+ DO IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
+ THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
+ s := s^.tl
+ OD
+ {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
+apply vcg_simp
+
+apply (fastsimp)
+
+(* One big fastsimp does not seem to converge: *)
+apply clarsimp
+apply(rule conjI)
+apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
+apply clarsimp
+apply(rule conjI)
+apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
+apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
+
+apply(clarsimp simp add:List_app)
+done
+
+(* merging with islist/list instead of List? Unlikely to be simpler *)
+
+subsection "Storage allocation"
+
+constdefs new :: "'a set \<Rightarrow> 'a"
+"new A == SOME a. a \<notin> A"
+
+
+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/Pointers.thy Sun Jan 05 21:03:14 2003 +0100
+++ b/src/HOL/Hoare/Pointers.thy Mon Jan 06 11:22:54 2003 +0100
@@ -5,11 +5,7 @@
How to use Hoare logic to verify pointer manipulating programs.
The old idea: the store is a global mapping from pointers to values.
-
-The list reversal example is taken from Richard Bornat's paper
-Proving pointer programs in Hoare logic
-What's new? We formalize the foundations, ie the abstraction from the pointer
-chains to HOL lists. This is merely axiomatized by Bornat.
+See the paper by Mehta and Nipkow.
*)
theory Pointers = Hoare:
@@ -81,9 +77,15 @@
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 := v)) x as y = Path f x as y"
+lemma Path_upd[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)
+lemma Path_snoc:
+ "Path (f(a := q)) p as (Ref a) \<Longrightarrow> Path (f(a := q)) p (as @ [a]) q"
+by simp
+
+
subsection "Lists on the heap"
subsubsection "Relational abstraction"
@@ -188,290 +190,4 @@
apply(simp add:List_conv_islist_list)
done
-
-section "Verifications"
-
-subsection "List reversal"
-
-text "A short but unreadable proof:"
-
-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>
- rev ps @ qs = rev Ps @ Qs}
- DO r := p; p := p^.tl; r^.tl := q; q := r OD
- {List tl q (rev Ps @ Qs)}"
-apply vcg_simp
- apply fastsimp
- apply(fastsimp intro:notin_List_update[THEN iffD2])
-(* explicit:
- apply clarify
- apply(rename_tac ps b qs)
- apply clarsimp
- apply(rename_tac ps')
- apply(fastsimp intro:notin_List_update[THEN iffD2])
- apply(rule_tac x = ps' in exI)
- apply simp
- apply(rule_tac x = "b#qs" in exI)
- apply simp
-*)
-apply fastsimp
-done
-
-
-text "A longer readable version:"
-
-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>
- rev ps @ qs = rev Ps @ Qs}
- DO r := p; p := p^.tl; r^.tl := q; q := r OD
- {List tl q (rev Ps @ Qs)}"
-proof vcg
- fix tl p q r
- assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
- thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
- rev ps @ qs = rev Ps @ Qs" by fastsimp
-next
- fix tl p q r
- assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
- rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
- (is "(\<exists>ps qs. ?I ps qs) \<and> _")
- then obtain ps qs a where I: "?I ps qs \<and> p = Ref a"
- by fast
- then obtain ps' where "ps = a # ps'" by fastsimp
- hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
- List (tl(p \<rightarrow> q)) p (a#qs) \<and>
- set ps' \<inter> set (a#qs) = {} \<and>
- rev ps' @ (a#qs) = rev Ps @ Qs"
- using I by fastsimp
- thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
- List (tl(p \<rightarrow> q)) p qs' \<and>
- set ps' \<inter> set qs' = {} \<and>
- rev ps' @ qs' = rev Ps @ Qs" by fast
-next
- fix tl p q r
- assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
- rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
- thus "List tl q (rev Ps @ Qs)" by fastsimp
-qed
-
-
-text{* Finaly, the functional version. A bit more verbose, but automatic! *}
-
-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
- INV {islist tl p \<and> islist tl q \<and>
- set(list tl p) \<inter> set(list tl q) = {} \<and>
- rev(list tl p) @ (list tl q) = rev Ps @ Qs}
- DO r := p; p := p^.tl; r^.tl := q; q := r OD
- {islist tl q \<and> list tl q = rev Ps @ Qs}"
-apply vcg_simp
- apply clarsimp
- apply clarsimp
-apply clarsimp
-done
-
-
-subsection "Searching in a list"
-
-text{*What follows is a sequence of successively more intelligent proofs that
-a simple loop finds an element in a linked list.
-
-We start with a proof based on the @{term List} predicate. This means it only
-works for acyclic lists. *}
-
-lemma "VARS tl p
- {List tl p Ps \<and> X \<in> set Ps}
- WHILE p \<noteq> Null \<and> p \<noteq> Ref X
- INV {\<exists>ps. List tl p ps \<and> X \<in> set ps}
- DO p := p^.tl OD
- {p = Ref X}"
-apply vcg_simp
- apply blast
- apply clarsimp
-apply clarsimp
-done
-
-text{*Using @{term Path} instead of @{term List} generalizes the correctness
-statement to cyclic lists as well: *}
-
-lemma "VARS tl p
- {Path tl p Ps X}
- WHILE p \<noteq> Null \<and> p \<noteq> X
- INV {\<exists>ps. Path tl p ps X}
- DO p := p^.tl OD
- {p = X}"
-apply vcg_simp
- apply blast
- apply fastsimp
-apply clarsimp
-done
-
-text{*Now it dawns on us that we do not need the list witness at all --- it
-suffices to talk about reachability, i.e.\ we can use relations directly. The
-first version uses a relation on @{typ"'a ref"}: *}
-
-lemma "VARS tl p
- {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
- WHILE p \<noteq> Null \<and> p \<noteq> X
- INV {(p,X) \<in> {(Ref x,tl x) |x. True}^*}
- DO p := p^.tl OD
- {p = X}"
-apply vcg_simp
- apply clarsimp
- apply(erule converse_rtranclE)
- apply simp
- apply(clarsimp elim:converse_rtranclE)
-apply(fast elim:converse_rtranclE)
-done
-
-text{*Finally, a version based on a relation on type @{typ 'a}:*}
-
-lemma "VARS tl p
- {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
- WHILE p \<noteq> Null \<and> p \<noteq> Ref X
- INV {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*}
- DO p := p^.tl OD
- {p = Ref X}"
-apply vcg_simp
- apply clarsimp
- apply(erule converse_rtranclE)
- apply simp
- apply clarsimp
-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)"
-"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
- else y # merge(x#xs,ys,f))"
-"merge(x#xs,[],f) = x # merge(xs,[],f)"
-"merge([],y#ys,f) = y # merge([],ys,f)"
-"merge([],[],f) = []"
-
-lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"
-by blast
-
-declare imp_disjL[simp del] imp_disjCL[simp]
-
-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
- THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
- s := r;
- WHILE p \<noteq> Null \<or> q \<noteq> Null
- INV {EX rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and>
- distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
- merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
- rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
- (tl a = p \<or> tl a = q)}
- DO IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
- THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
- s := s^.tl
- OD
- {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
-apply vcg_simp
-
-apply (fastsimp)
-
-apply clarsimp
-apply(rule conjI)
-apply clarsimp
-apply(simp add:eq_sym_conv)
-apply(rule_tac x = "rs @ [a]" in exI)
-apply simp
-apply(rule_tac x = "bs" in exI)
-apply (fastsimp simp:eq_sym_conv)
-
-apply clarsimp
-apply(rule conjI)
-apply clarsimp
-apply(rule_tac x = "rs @ [a]" in exI)
-apply simp
-apply(rule_tac x = "bsa" in exI)
-apply(rule conjI)
-apply (simp add:eq_sym_conv)
-apply(rule exI)
-apply(rule conjI)
-apply(rule_tac x = bs in exI)
-apply(rule conjI)
-apply(rule refl)
-apply (simp add:eq_sym_conv)
-apply (simp add:eq_sym_conv)
-apply (fast)
-
-apply(rule conjI)
-apply clarsimp
-apply(rule_tac x = "rs @ [a]" in exI)
-apply simp
-apply(rule_tac x = bs in exI)
-apply (simp add:eq_sym_conv)
-apply clarsimp
-apply(rule_tac x = "rs @ [a]" in exI)
-apply (simp add:eq_sym_conv)
-apply(rule exI)
-apply(rule conjI)
-apply(rule_tac x = bsa in exI)
-apply(rule conjI)
-apply(rule refl)
-apply (simp add:eq_sym_conv)
-apply(rule_tac x = bs in exI)
-apply (simp add:eq_sym_conv)
-apply fast
-
-apply(clarsimp simp add:List_app)
-done
-
-(* 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/ROOT.ML Sun Jan 05 21:03:14 2003 +0100
+++ b/src/HOL/Hoare/ROOT.ML Mon Jan 06 11:22:54 2003 +0100
@@ -6,4 +6,4 @@
time_use_thy "Examples";
time_use_thy "Pointers0";
-time_use_thy "Pointers";
+time_use_thy "Pointer_Examples";