# HG changeset patch
# User nipkow
# Date 1037896811 -3600
# Node ID c7d1045502050d037ceca560c5c6aa3df396aa8b
# Parent  e03747c2ca58406726a9afb63f8a57929a501fd5
*** empty log message ***

diff -r e03747c2ca58 -r c7d104550205 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Nov 20 10:43:20 2002 +0100
+++ b/src/HOL/HOL.thy	Thu Nov 21 17:40:11 2002 +0100
@@ -512,6 +512,9 @@
 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
 setup Splitter.setup setup Clasimp.setup
 
+lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"
+by blast+
+
 theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"
   apply (rule iffI)
   apply (rule_tac a = "%x. THE y. P x y" in ex1I)
diff -r e03747c2ca58 -r c7d104550205 src/HOL/Hoare/Pointers.thy
--- a/src/HOL/Hoare/Pointers.thy	Wed Nov 20 10:43:20 2002 +0100
+++ b/src/HOL/Hoare/Pointers.thy	Thu Nov 21 17:40:11 2002 +0100
@@ -87,6 +87,8 @@
 
 subsection "Lists on the heap"
 
+subsubsection "Relational abstraction"
+
 constdefs
  list :: "('a \<leadsto> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> bool"
 "list h x as == path h x as Null"
@@ -100,7 +102,7 @@
 lemma [simp]: "list h Null as = (as = [])"
 by(case_tac as, simp_all)
 
-lemma [simp]: "list h (Ref a) as = (\<exists>bs. as = a#bs \<and> list h (h a) bs)"
+lemma list_Ref[simp]: "list h (Ref a) as = (\<exists>bs. as = a#bs \<and> list h (h a) bs)"
 by(case_tac as, simp_all, fast)
 
 
@@ -109,13 +111,16 @@
 lemma list_unique: "\<And>x bs. list h x as \<Longrightarrow> list h x bs \<Longrightarrow> as = bs"
 by(induct as, simp, clarsimp)
 
+lemma list_unique1: "list h p as \<Longrightarrow> \<exists>!as. list h p as"
+by(blast intro:list_unique)
+
 lemma list_app: "\<And>x. list h x (as@bs) = (\<exists>y. path h x as y \<and> list h y bs)"
 by(induct as, simp, clarsimp)
 
 lemma list_hd_not_in_tl[simp]: "list h (h a) as \<Longrightarrow> a \<notin> set as"
 apply (clarsimp simp add:in_set_conv_decomp)
 apply(frule list_app[THEN iffD1])
-apply(fastsimp dest:list_app[THEN iffD1] list_unique)
+apply(fastsimp dest: list_unique)
 done
 
 lemma list_distinct[simp]: "\<And>x. list h x as \<Longrightarrow> distinct as"
@@ -123,20 +128,66 @@
 apply(fastsimp dest:list_hd_not_in_tl)
 done
 
-theorem notin_list_update[rule_format,simp]:
- "\<forall>x. a \<notin> set as \<longrightarrow> list (h(a := y)) x as = list h x as"
-apply(induct_tac as)
+theorem notin_list_update[simp]:
+ "\<And>x. a \<notin> set as \<Longrightarrow> list (h(a := y)) x as = list h x as"
+apply(induct as)
 apply simp
-apply(simp add:fun_upd_apply)
+apply(clarsimp simp add:fun_upd_apply)
+done
+
+subsection "Functional abstraction"
+
+constdefs
+ islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
+"islist h p == \<exists>as. list h p as"
+ mklist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
+"mklist h p == SOME as. list h p as"
+
+lemma list_conv_islist_mklist: "list h p as = (islist h p \<and> as = mklist h p)"
+apply(simp add:islist_def mklist_def)
+apply(rule iffI)
+apply(rule conjI)
+apply blast
+apply(subst some1_equality)
+  apply(erule list_unique1)
+ apply assumption
+apply(rule refl)
+apply simp
+apply(rule someI_ex)
+apply fast
 done
 
-lemma [simp]: "list h (h a) as \<Longrightarrow> list (h(a := y)) (h a) as"
-by(simp add:list_hd_not_in_tl)
-(* Note that the opposite direction does NOT hold:
-   If    h = (a \<mapsto> Ref a)
-   then  list (h(a := Null)) (h a) [a]
-   but   not list h (h a) [] (because h is cyclic)
-*)
+lemma [simp]: "islist h None"
+by(simp add:islist_def)
+
+lemma [simp]: "islist h (Some a) = islist h (h a)"
+by(simp add:islist_def)
+
+lemma [simp]: "mklist h None = []"
+by(simp add:mklist_def)
+
+lemma [simp]: "islist h (h a) \<Longrightarrow> mklist h (Some a) = a # mklist h (h a)"
+apply(insert list_Ref[of h])
+apply(fastsimp simp:list_conv_islist_mklist)
+done
+
+lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(mklist h (h a))"
+apply(insert list_hd_not_in_tl[of h])
+apply(simp add:list_conv_islist_mklist)
+done
+
+lemma [simp]:
+ "islist h p \<Longrightarrow> y \<notin> set(mklist h p) \<Longrightarrow> mklist (h(y := q)) p = mklist h p"
+apply(drule notin_list_update[of _ _ h q p])
+apply(simp add:list_conv_islist_mklist)
+done
+
+lemma [simp]:
+ "islist h p \<Longrightarrow> y \<notin> set(mklist h p) \<Longrightarrow> islist (h(y := q)) p"
+apply(frule notin_list_update[of _ _ h q p])
+apply(simp add:list_conv_islist_mklist)
+done
+
 
 section "Verifications"
 
@@ -204,6 +255,24 @@
 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 = mklist tl p \<and> Qs = mklist tl q \<and> set Ps \<inter> set Qs = {}}
+  WHILE p \<noteq> Null
+  INV {islist tl p \<and> islist tl q \<and>
+       set(mklist tl p) \<inter> set(mklist tl q) = {} \<and>
+       rev(mklist tl p) @ (mklist tl q) = rev Ps @ Qs}
+  DO r := p; p := p^.tl; r^.tl := q; q := r OD
+  {islist tl q \<and> mklist 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
@@ -381,4 +450,6 @@
 apply(clarsimp simp add:list_app)
 done
 
+(* TODO: functional version of merging *)
+
 end