new versions of merge-example
authornipkow
Tue Jan 07 14:32:04 2003 +0100 (2003-01-07)
changeset 1377358dc4ab362d0
parent 13772 73d041cc6a66
child 13774 77a1e723151d
new versions of merge-example
src/HOL/Hoare/Pointer_Examples.thy
     1.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Mon Jan 06 11:22:54 2003 +0100
     1.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Tue Jan 07 14:32:04 2003 +0100
     1.3 @@ -170,6 +170,12 @@
     1.4  
     1.5  text"This is still a bit rough, especially the proof."
     1.6  
     1.7 +constdefs
     1.8 + cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
     1.9 +"cor P Q == if P then True else Q"
    1.10 + cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
    1.11 +"cand P Q == if P then Q else False"
    1.12 +
    1.13  consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
    1.14  
    1.15  recdef merge "measure(%(xs,ys,f). size xs + size ys)"
    1.16 @@ -179,15 +185,19 @@
    1.17  "merge([],y#ys,f) = y # merge([],ys,f)"
    1.18  "merge([],[],f) = []"
    1.19  
    1.20 -lemma imp_disjCL: "(P|Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (~P \<longrightarrow> Q \<longrightarrow> R))"
    1.21 +text{* Simplifies the proof a little: *}
    1.22 +
    1.23 +lemma [simp]: "({} = insert a A \<inter> B) = (a \<notin> B & {} = A \<inter> B)"
    1.24  by blast
    1.25 -
    1.26 -declare imp_disjL[simp del] imp_disjCL[simp]
    1.27 +lemma [simp]: "({} = A \<inter> insert b B) = (b \<notin> A & {} = A \<inter> B)"
    1.28 +by blast
    1.29 +lemma [simp]: "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B & {} = A \<inter> C)"
    1.30 +by blast
    1.31  
    1.32  lemma "VARS hd tl p q r s
    1.33   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
    1.34    (p \<noteq> Null \<or> q \<noteq> Null)}
    1.35 - IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
    1.36 + IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
    1.37   THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
    1.38   s := r;
    1.39   WHILE p \<noteq> Null \<or> q \<noteq> Null
    1.40 @@ -196,28 +206,116 @@
    1.41        merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
    1.42        rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
    1.43        (tl a = p \<or> tl a = q)}
    1.44 - DO IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
    1.45 + DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
    1.46      THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
    1.47      s := s^.tl
    1.48   OD
    1.49   {List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
    1.50  apply vcg_simp
    1.51 +apply (simp_all add: cand_def cor_def)
    1.52  
    1.53  apply (fastsimp)
    1.54  
    1.55 -(* One big fastsimp does not seem to converge: *)
    1.56 +apply clarsimp
    1.57 +apply(rule conjI)
    1.58  apply clarsimp
    1.59  apply(rule conjI)
    1.60  apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
    1.61  apply clarsimp
    1.62  apply(rule conjI)
    1.63 -apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
    1.64 +apply (clarsimp)
    1.65 +apply(rule_tac x = "rs @ [a]" in exI)
    1.66 +apply(clarsimp simp:eq_sym_conv)
    1.67 +apply(rule_tac x = "bs" in exI)
    1.68 +apply(clarsimp simp:eq_sym_conv)
    1.69 +apply(rule_tac x = "ya#bsa" in exI)
    1.70 +apply(simp)
    1.71 +apply(clarsimp simp:eq_sym_conv)
    1.72 +apply(rule_tac x = "rs @ [a]" in exI)
    1.73 +apply(clarsimp simp:eq_sym_conv)
    1.74 +apply(rule_tac x = "y#bs" in exI)
    1.75 +apply(clarsimp simp:eq_sym_conv)
    1.76 +apply(rule_tac x = "bsa" in exI)
    1.77 +apply(simp)
    1.78  apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
    1.79  
    1.80  apply(clarsimp simp add:List_app)
    1.81  done
    1.82  
    1.83 -(* merging with islist/list instead of List? Unlikely to be simpler *)
    1.84 +
    1.85 +text{* More of the proof can be automated, but the runtime goes up
    1.86 +drastically. In general it is usually more efficient to give the
    1.87 +witness directly than to have it found by proof.
    1.88 +
    1.89 +Now we try a functional version of the abstraction relation @{term
    1.90 +Path}. Since the result is not that convincing, we do not prove any of
    1.91 +the lemmas.*}
    1.92 +
    1.93 +consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
    1.94 +       path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
    1.95 +
    1.96 +ML"set quick_and_dirty"
    1.97 +
    1.98 +text"First some basic lemmas:"
    1.99 +
   1.100 +lemma [simp]: "ispath f p p"
   1.101 +sorry
   1.102 +lemma [simp]: "path f p p = []"
   1.103 +sorry
   1.104 +lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q"
   1.105 +sorry
   1.106 +lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow>
   1.107 + path (f(a := r)) p q = path f p q"
   1.108 +sorry
   1.109 +
   1.110 +text"Some more specific lemmas needed by the example:"
   1.111 +
   1.112 +lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q"
   1.113 +sorry
   1.114 +lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow>
   1.115 + path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]"
   1.116 +sorry
   1.117 +lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow>
   1.118 + b \<notin> set (path f p (Ref a))"
   1.119 +sorry
   1.120 +lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p"
   1.121 +sorry
   1.122 +lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]"
   1.123 +sorry
   1.124 +
   1.125 +lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)"
   1.126 +sorry
   1.127 +ML"reset quick_and_dirty"
   1.128 +
   1.129 +lemma "VARS hd tl p q r s
   1.130 + {islist tl p & Ps = list tl p \<and> islist tl q & Qs = list tl q \<and>
   1.131 +  set Ps \<inter> set Qs = {} \<and>
   1.132 +  (p \<noteq> Null \<or> q \<noteq> Null)}
   1.133 + IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   1.134 + THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI;
   1.135 + s := r;
   1.136 + WHILE p \<noteq> Null \<or> q \<noteq> Null
   1.137 + INV {EX rs ps qs a. ispath tl r s & rs = path tl r s \<and>
   1.138 +      islist tl p & ps = list tl p \<and> islist tl q & qs = list tl q \<and>
   1.139 +      distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and>
   1.140 +      merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) =
   1.141 +      rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and>
   1.142 +      (tl a = p \<or> tl a = q)}
   1.143 + DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd))
   1.144 +    THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI;
   1.145 +    s := s^.tl
   1.146 + OD
   1.147 + {islist tl r & list tl r = (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
   1.148 +apply vcg_simp
   1.149 +
   1.150 +apply (simp_all add: cand_def cor_def)
   1.151 +  apply (fastsimp)
   1.152 + apply (fastsimp simp: eq_sym_conv)
   1.153 +apply(clarsimp)
   1.154 +done
   1.155 +
   1.156 +text"The proof is automatic, but requires a numbet of special lemmas."
   1.157 +
   1.158  
   1.159  subsection "Storage allocation"
   1.160