# HG changeset patch
# User nipkow
# Date 1041946324 -3600
# Node ID 58dc4ab362d0b9eed3b46d39006497e08b08876d
# Parent  73d041cc6a667a69d75366c1dd5599d6342195e1
new versions of merge-example

diff -r 73d041cc6a66 -r 58dc4ab362d0 src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy	Mon Jan 06 11:22:54 2003 +0100
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Tue Jan 07 14:32:04 2003 +0100
@@ -170,6 +170,12 @@
 
 text"This is still a bit rough, especially the proof."
 
+constdefs
+ cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+"cor P Q == if P then True else Q"
+ cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+"cand P Q == if P then Q else False"
+
 consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
 
 recdef merge "measure(%(xs,ys,f). size xs + size ys)"
@@ -179,15 +185,19 @@
 "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))"
+text{* Simplifies the proof a little: *}
+
+lemma [simp]: "({} = insert a A \<inter> B) = (a \<notin> B & {} = A \<inter> B)"
 by blast
-
-declare imp_disjL[simp del] imp_disjCL[simp]
+lemma [simp]: "({} = A \<inter> insert b B) = (b \<notin> A & {} = A \<inter> B)"
+by blast
+lemma [simp]: "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B & {} = A \<inter> C)"
+by blast
 
 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
+ IF cor (q = Null) (cand (p \<noteq> Null) (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
@@ -196,28 +206,116 @@
       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
+ DO IF cor (q = Null) (cand (p \<noteq> Null) (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 (simp_all add: cand_def cor_def)
 
 apply (fastsimp)
 
-(* One big fastsimp does not seem to converge: *)
+apply clarsimp
+apply(rule conjI)
 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 (clarsimp)
+apply(rule_tac x = "rs @ [a]" in exI)
+apply(clarsimp simp:eq_sym_conv)
+apply(rule_tac x = "bs" in exI)
+apply(clarsimp simp:eq_sym_conv)
+apply(rule_tac x = "ya#bsa" in exI)
+apply(simp)
+apply(clarsimp simp:eq_sym_conv)
+apply(rule_tac x = "rs @ [a]" in exI)
+apply(clarsimp simp:eq_sym_conv)
+apply(rule_tac x = "y#bs" in exI)
+apply(clarsimp simp:eq_sym_conv)
+apply(rule_tac x = "bsa" in exI)
+apply(simp)
 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 *)
+
+text{* More of the proof can be automated, but the runtime goes up
+drastically. In general it is usually more efficient to give the
+witness directly than to have it found by proof.
+
+Now we try a functional version of the abstraction relation @{term
+Path}. Since the result is not that convincing, we do not prove any of
+the lemmas.*}
+
+consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
+       path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
+
+ML"set quick_and_dirty"
+
+text"First some basic lemmas:"
+
+lemma [simp]: "ispath f p p"
+sorry
+lemma [simp]: "path f p p = []"
+sorry
+lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q"
+sorry
+lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow>
+ path (f(a := r)) p q = path f p q"
+sorry
+
+text"Some more specific lemmas needed by the example:"
+
+lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q"
+sorry
+lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow>
+ path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]"
+sorry
+lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow>
+ b \<notin> set (path f p (Ref a))"
+sorry
+lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p"
+sorry
+lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]"
+sorry
+
+lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)"
+sorry
+ML"reset quick_and_dirty"
+
+lemma "VARS hd tl p q r s
+ {islist tl p & Ps = list tl p \<and> islist tl q & Qs = list tl q \<and>
+  set Ps \<inter> set Qs = {} \<and>
+  (p \<noteq> Null \<or> q \<noteq> Null)}
+ IF cor (q = Null) (cand (p \<noteq> Null) (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. ispath tl r s & rs = path tl r s \<and>
+      islist tl p & ps = list tl p \<and> islist tl q & qs = list tl q \<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 cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
+    THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
+    s := s^.tl
+ OD
+ {islist tl r & list tl r = (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
+apply vcg_simp
+
+apply (simp_all add: cand_def cor_def)
+  apply (fastsimp)
+ apply (fastsimp simp: eq_sym_conv)
+apply(clarsimp)
+done
+
+text"The proof is automatic, but requires a numbet of special lemmas."
+
 
 subsection "Storage allocation"