src/HOL/Imperative_HOL/ex/Linked_Lists.thy
author haftmann
Fri Jul 23 10:58:13 2010 +0200 (2010-07-23)
changeset 37947 844977c7abeb
parent 37879 443909380077
child 37959 6fe5fa827f18
permissions -rw-r--r--
avoid unreliable Haskell Int type
     1 (*  Title:      HOL/Imperative_HOL/ex/Linked_Lists.thy
     2     Author:     Lukas Bulwahn, TU Muenchen
     3 *)
     4 
     5 header {* Linked Lists by ML references *}
     6 
     7 theory Linked_Lists
     8 imports Imperative_HOL Code_Integer
     9 begin
    10 
    11 section {* Definition of Linked Lists *}
    12 
    13 setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>type ref"}) *}
    14 datatype 'a node = Empty | Node 'a "('a node) ref"
    15 
    16 primrec
    17   node_encode :: "'a\<Colon>countable node \<Rightarrow> nat"
    18 where
    19   "node_encode Empty = 0"
    20   | "node_encode (Node x r) = Suc (to_nat (x, r))"
    21 
    22 instance node :: (countable) countable
    23 proof (rule countable_classI [of "node_encode"])
    24   fix x y :: "'a\<Colon>countable node"
    25   show "node_encode x = node_encode y \<Longrightarrow> x = y"
    26   by (induct x, auto, induct y, auto, induct y, auto)
    27 qed
    28 
    29 instance node :: (heap) heap ..
    30 
    31 primrec make_llist :: "'a\<Colon>heap list \<Rightarrow> 'a node Heap"
    32 where 
    33   [simp del]: "make_llist []     = return Empty"
    34             | "make_llist (x#xs) = do { tl \<leftarrow> make_llist xs;
    35                                         next \<leftarrow> ref tl;
    36                                         return (Node x next)
    37                                    }"
    38 
    39 
    40 text {* define traverse using the MREC combinator *}
    41 
    42 definition
    43   traverse :: "'a\<Colon>heap node \<Rightarrow> 'a list Heap"
    44 where
    45 [code del]: "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
    46                                 | Node x r \<Rightarrow> do { tl \<leftarrow> Ref.lookup r;
    47                                                   return (Inr tl) })
    48                    (\<lambda>n tl xs. case n of Empty \<Rightarrow> undefined
    49                                       | Node x r \<Rightarrow> return (x # xs))"
    50 
    51 
    52 lemma traverse_simps[code, simp]:
    53   "traverse Empty      = return []"
    54   "traverse (Node x r) = do { tl \<leftarrow> Ref.lookup r;
    55                               xs \<leftarrow> traverse tl;
    56                               return (x#xs)
    57                          }"
    58 unfolding traverse_def
    59 by (auto simp: traverse_def MREC_rule)
    60 
    61 
    62 section {* Proving correctness with relational abstraction *}
    63 
    64 subsection {* Definition of list_of, list_of', refs_of and refs_of' *}
    65 
    66 primrec list_of :: "heap \<Rightarrow> ('a::heap) node \<Rightarrow> 'a list \<Rightarrow> bool"
    67 where
    68   "list_of h r [] = (r = Empty)"
    69 | "list_of h r (a#as) = (case r of Empty \<Rightarrow> False | Node b bs \<Rightarrow> (a = b \<and> list_of h (Ref.get h bs) as))"
    70  
    71 definition list_of' :: "heap \<Rightarrow> ('a::heap) node ref \<Rightarrow> 'a list \<Rightarrow> bool"
    72 where
    73   "list_of' h r xs = list_of h (Ref.get h r) xs"
    74 
    75 primrec refs_of :: "heap \<Rightarrow> ('a::heap) node \<Rightarrow> 'a node ref list \<Rightarrow> bool"
    76 where
    77   "refs_of h r [] = (r = Empty)"
    78 | "refs_of h r (x#xs) = (case r of Empty \<Rightarrow> False | Node b bs \<Rightarrow> (x = bs) \<and> refs_of h (Ref.get h bs) xs)"
    79 
    80 primrec refs_of' :: "heap \<Rightarrow> ('a::heap) node ref \<Rightarrow> 'a node ref list \<Rightarrow> bool"
    81 where
    82   "refs_of' h r [] = False"
    83 | "refs_of' h r (x#xs) = ((x = r) \<and> refs_of h (Ref.get h x) xs)"
    84 
    85 
    86 subsection {* Properties of these definitions *}
    87 
    88 lemma list_of_Empty[simp]: "list_of h Empty xs = (xs = [])"
    89 by (cases xs, auto)
    90 
    91 lemma list_of_Node[simp]: "list_of h (Node x ps) xs = (\<exists>xs'. (xs = x # xs') \<and> list_of h (Ref.get h ps) xs')"
    92 by (cases xs, auto)
    93 
    94 lemma list_of'_Empty[simp]: "Ref.get h q = Empty \<Longrightarrow> list_of' h q xs = (xs = [])"
    95 unfolding list_of'_def by simp
    96 
    97 lemma list_of'_Node[simp]: "Ref.get h q = Node x ps \<Longrightarrow> list_of' h q xs = (\<exists>xs'. (xs = x # xs') \<and> list_of' h ps xs')"
    98 unfolding list_of'_def by simp
    99 
   100 lemma list_of'_Nil: "list_of' h q [] \<Longrightarrow> Ref.get h q = Empty"
   101 unfolding list_of'_def by simp
   102 
   103 lemma list_of'_Cons: 
   104 assumes "list_of' h q (x#xs)"
   105 obtains n where "Ref.get h q = Node x n" and "list_of' h n xs"
   106 using assms unfolding list_of'_def by (auto split: node.split_asm)
   107 
   108 lemma refs_of_Empty[simp] : "refs_of h Empty xs = (xs = [])"
   109   by (cases xs, auto)
   110 
   111 lemma refs_of_Node[simp]: "refs_of h (Node x ps) xs = (\<exists>prs. xs = ps # prs \<and> refs_of h (Ref.get h ps) prs)"
   112   by (cases xs, auto)
   113 
   114 lemma refs_of'_def': "refs_of' h p ps = (\<exists>prs. (ps = (p # prs)) \<and> refs_of h (Ref.get h p) prs)"
   115 by (cases ps, auto)
   116 
   117 lemma refs_of'_Node:
   118   assumes "refs_of' h p xs"
   119   assumes "Ref.get h p = Node x pn"
   120   obtains pnrs
   121   where "xs = p # pnrs" and "refs_of' h pn pnrs"
   122 using assms
   123 unfolding refs_of'_def' by auto
   124 
   125 lemma list_of_is_fun: "\<lbrakk> list_of h n xs; list_of h n ys\<rbrakk> \<Longrightarrow> xs = ys"
   126 proof (induct xs arbitrary: ys n)
   127   case Nil thus ?case by auto
   128 next
   129   case (Cons x xs')
   130   thus ?case
   131     by (cases ys,  auto split: node.split_asm)
   132 qed
   133 
   134 lemma refs_of_is_fun: "\<lbrakk> refs_of h n xs; refs_of h n ys\<rbrakk> \<Longrightarrow> xs = ys"
   135 proof (induct xs arbitrary: ys n)
   136   case Nil thus ?case by auto
   137 next
   138   case (Cons x xs')
   139   thus ?case
   140     by (cases ys,  auto split: node.split_asm)
   141 qed
   142 
   143 lemma refs_of'_is_fun: "\<lbrakk> refs_of' h p as; refs_of' h p bs \<rbrakk> \<Longrightarrow> as = bs"
   144 unfolding refs_of'_def' by (auto dest: refs_of_is_fun)
   145 
   146 
   147 lemma list_of_refs_of_HOL:
   148   assumes "list_of h r xs"
   149   shows "\<exists>rs. refs_of h r rs"
   150 using assms
   151 proof (induct xs arbitrary: r)
   152   case Nil thus ?case by auto
   153 next
   154   case (Cons x xs')
   155   thus ?case
   156     by (cases r, auto)
   157 qed
   158     
   159 lemma list_of_refs_of:
   160   assumes "list_of h r xs"
   161   obtains rs where "refs_of h r rs"
   162 using list_of_refs_of_HOL[OF assms]
   163 by auto
   164 
   165 lemma list_of'_refs_of'_HOL:
   166   assumes "list_of' h r xs"
   167   shows "\<exists>rs. refs_of' h r rs"
   168 proof -
   169   from assms obtain rs' where "refs_of h (Ref.get h r) rs'"
   170     unfolding list_of'_def by (rule list_of_refs_of)
   171   thus ?thesis unfolding refs_of'_def' by auto
   172 qed
   173 
   174 lemma list_of'_refs_of':
   175   assumes "list_of' h r xs"
   176   obtains rs where "refs_of' h r rs"
   177 using list_of'_refs_of'_HOL[OF assms]
   178 by auto
   179 
   180 lemma refs_of_list_of_HOL:
   181   assumes "refs_of h r rs"
   182   shows "\<exists>xs. list_of h r xs"
   183 using assms
   184 proof (induct rs arbitrary: r)
   185   case Nil thus ?case by auto
   186 next
   187   case (Cons r rs')
   188   thus ?case
   189     by (cases r, auto)
   190 qed
   191 
   192 lemma refs_of_list_of:
   193   assumes "refs_of h r rs"
   194   obtains xs where "list_of h r xs"
   195 using refs_of_list_of_HOL[OF assms]
   196 by auto
   197 
   198 lemma refs_of'_list_of'_HOL:
   199   assumes "refs_of' h r rs"
   200   shows "\<exists>xs. list_of' h r xs"
   201 using assms
   202 unfolding list_of'_def refs_of'_def'
   203 by (auto intro: refs_of_list_of)
   204 
   205 
   206 lemma refs_of'_list_of':
   207   assumes "refs_of' h r rs"
   208   obtains xs where "list_of' h r xs"
   209 using refs_of'_list_of'_HOL[OF assms]
   210 by auto
   211 
   212 lemma refs_of'E: "refs_of' h q rs \<Longrightarrow> q \<in> set rs"
   213 unfolding refs_of'_def' by auto
   214 
   215 lemma list_of'_refs_of'2:
   216   assumes "list_of' h r xs"
   217   shows "\<exists>rs'. refs_of' h r (r#rs')"
   218 proof -
   219   from assms obtain rs where "refs_of' h r rs" by (rule list_of'_refs_of')
   220   thus ?thesis by (auto simp add: refs_of'_def')
   221 qed
   222 
   223 subsection {* More complicated properties of these predicates *}
   224 
   225 lemma list_of_append:
   226   "list_of h n (as @ bs) \<Longrightarrow> \<exists>m. list_of h m bs"
   227 apply (induct as arbitrary: n)
   228 apply auto
   229 apply (case_tac n)
   230 apply auto
   231 done
   232 
   233 lemma refs_of_append: "refs_of h n (as @ bs) \<Longrightarrow> \<exists>m. refs_of h m bs"
   234 apply (induct as arbitrary: n)
   235 apply auto
   236 apply (case_tac n)
   237 apply auto
   238 done
   239 
   240 lemma refs_of_next:
   241 assumes "refs_of h (Ref.get h p) rs"
   242   shows "p \<notin> set rs"
   243 proof (rule ccontr)
   244   assume a: "\<not> (p \<notin> set rs)"
   245   from this obtain as bs where split:"rs = as @ p # bs" by (fastsimp dest: split_list)
   246   with assms obtain q where "refs_of h q (p # bs)" by (fast dest: refs_of_append)
   247   with assms split show "False"
   248     by (cases q,auto dest: refs_of_is_fun)
   249 qed
   250 
   251 lemma refs_of_distinct: "refs_of h p rs \<Longrightarrow> distinct rs"
   252 proof (induct rs arbitrary: p)
   253   case Nil thus ?case by simp
   254 next
   255   case (Cons r rs')
   256   thus ?case
   257     by (cases p, auto simp add: refs_of_next)
   258 qed
   259 
   260 lemma refs_of'_distinct: "refs_of' h p rs \<Longrightarrow> distinct rs"
   261   unfolding refs_of'_def'
   262   by (fastsimp simp add: refs_of_distinct refs_of_next)
   263 
   264 
   265 subsection {* Interaction of these predicates with our heap transitions *}
   266 
   267 lemma list_of_set_ref: "refs_of h q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> list_of (Ref.set p v h) q as = list_of h q as"
   268 using assms
   269 proof (induct as arbitrary: q rs)
   270   case Nil thus ?case by simp
   271 next
   272   case (Cons x xs)
   273   thus ?case
   274   proof (cases q)
   275     case Empty thus ?thesis by auto
   276   next
   277     case (Node a ref)
   278     from Cons(2) Node obtain rs' where 1: "refs_of h (Ref.get h ref) rs'" and rs_rs': "rs = ref # rs'" by auto
   279     from Cons(3) rs_rs' have "ref \<noteq> p" by fastsimp
   280     hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq)
   281     from rs_rs' Cons(3) have 2: "p \<notin> set rs'" by simp
   282     from Cons.hyps[OF 1 2] Node ref_eq show ?thesis by simp
   283   qed
   284 qed
   285 
   286 lemma refs_of_set_ref: "refs_of h q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> refs_of (Ref.set p v h) q as = refs_of h q as"
   287 proof (induct as arbitrary: q rs)
   288   case Nil thus ?case by simp
   289 next
   290   case (Cons x xs)
   291   thus ?case
   292   proof (cases q)
   293     case Empty thus ?thesis by auto
   294   next
   295     case (Node a ref)
   296     from Cons(2) Node obtain rs' where 1: "refs_of h (Ref.get h ref) rs'" and rs_rs': "rs = ref # rs'" by auto
   297     from Cons(3) rs_rs' have "ref \<noteq> p" by fastsimp
   298     hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq)
   299     from rs_rs' Cons(3) have 2: "p \<notin> set rs'" by simp
   300     from Cons.hyps[OF 1 2] Node ref_eq show ?thesis by auto
   301   qed
   302 qed
   303 
   304 lemma refs_of_set_ref2: "refs_of (Ref.set p v h) q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> refs_of (Ref.set p v h) q rs = refs_of h q rs"
   305 proof (induct rs arbitrary: q)
   306   case Nil thus ?case by simp
   307 next
   308   case (Cons x xs)
   309   thus ?case
   310   proof (cases q)
   311     case Empty thus ?thesis by auto
   312   next
   313     case (Node a ref)
   314     from Cons(2) Node have 1:"refs_of (Ref.set p v h) (Ref.get (Ref.set p v h) ref) xs" and x_ref: "x = ref" by auto
   315     from Cons(3) this have "ref \<noteq> p" by fastsimp
   316     hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq)
   317     from Cons(3) have 2: "p \<notin> set xs" by simp
   318     with Cons.hyps 1 2 Node ref_eq show ?thesis
   319       by simp
   320   qed
   321 qed
   322 
   323 lemma list_of'_set_ref:
   324   assumes "refs_of' h q rs"
   325   assumes "p \<notin> set rs"
   326   shows "list_of' (Ref.set p v h) q as = list_of' h q as"
   327 proof -
   328   from assms have "q \<noteq> p" by (auto simp only: dest!: refs_of'E)
   329   with assms show ?thesis
   330     unfolding list_of'_def refs_of'_def'
   331     by (auto simp add: list_of_set_ref)
   332 qed
   333 
   334 lemma list_of'_set_next_ref_Node[simp]:
   335   assumes "list_of' h r xs"
   336   assumes "Ref.get h p = Node x r'"
   337   assumes "refs_of' h r rs"
   338   assumes "p \<notin> set rs"
   339   shows "list_of' (Ref.set p (Node x r) h) p (x#xs) = list_of' h r xs"
   340 using assms
   341 unfolding list_of'_def refs_of'_def'
   342 by (auto simp add: list_of_set_ref Ref.noteq_sym)
   343 
   344 lemma refs_of'_set_ref:
   345   assumes "refs_of' h q rs"
   346   assumes "p \<notin> set rs"
   347   shows "refs_of' (Ref.set p v h) q as = refs_of' h q as"
   348 using assms
   349 proof -
   350   from assms have "q \<noteq> p" by (auto simp only: dest!: refs_of'E)
   351   with assms show ?thesis
   352     unfolding refs_of'_def'
   353     by (auto simp add: refs_of_set_ref)
   354 qed
   355 
   356 lemma refs_of'_set_ref2:
   357   assumes "refs_of' (Ref.set p v h) q rs"
   358   assumes "p \<notin> set rs"
   359   shows "refs_of' (Ref.set p v h) q as = refs_of' h q as"
   360 using assms
   361 proof -
   362   from assms have "q \<noteq> p" by (auto simp only: dest!: refs_of'E)
   363   with assms show ?thesis
   364     unfolding refs_of'_def'
   365     apply auto
   366     apply (subgoal_tac "prs = prsa")
   367     apply (insert refs_of_set_ref2[of p v h "Ref.get h q"])
   368     apply (erule_tac x="prs" in meta_allE)
   369     apply auto
   370     apply (auto dest: refs_of_is_fun)
   371     done
   372 qed
   373 
   374 lemma refs_of'_set_next_ref:
   375 assumes "Ref.get h1 p = Node x pn"
   376 assumes "refs_of' (Ref.set p (Node x r1) h1) p rs"
   377 obtains r1s where "rs = (p#r1s)" and "refs_of' h1 r1 r1s"
   378 using assms
   379 proof -
   380   from assms refs_of'_distinct[OF assms(2)] have "\<exists> r1s. rs = (p # r1s) \<and> refs_of' h1 r1 r1s"
   381     apply -
   382     unfolding refs_of'_def'[of _ p]
   383     apply (auto, frule refs_of_set_ref2) by (auto dest: Ref.noteq_sym)
   384   with prems show thesis by auto
   385 qed
   386 
   387 section {* Proving make_llist and traverse correct *}
   388 
   389 lemma refs_of_invariant:
   390   assumes "refs_of h (r::('a::heap) node) xs"
   391   assumes "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref \<in> set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)"
   392   shows "refs_of h' r xs"
   393 using assms
   394 proof (induct xs arbitrary: r)
   395   case Nil thus ?case by simp
   396 next
   397   case (Cons x xs')
   398   from Cons(2) obtain v where Node: "r = Node v x" by (cases r, auto)
   399   from Cons(2) Node have refs_of_next: "refs_of h (Ref.get h x) xs'" by simp
   400   from Cons(2-3) Node have ref_eq: "Ref.get h x = Ref.get h' x" by auto
   401   from ref_eq refs_of_next have 1: "refs_of h (Ref.get h' x) xs'" by simp
   402   from Cons(2) Cons(3) have "\<forall>ref \<in> set xs'. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref"
   403     by fastsimp
   404   with Cons(3) 1 have 2: "\<forall>refs. refs_of h (Ref.get h' x) refs \<longrightarrow> (\<forall>ref \<in> set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)"
   405     by (fastsimp dest: refs_of_is_fun)
   406   from Cons.hyps[OF 1 2] have "refs_of h' (Ref.get h' x) xs'" .
   407   with Node show ?case by simp
   408 qed
   409 
   410 lemma refs_of'_invariant:
   411   assumes "refs_of' h r xs"
   412   assumes "\<forall>refs. refs_of' h r refs \<longrightarrow> (\<forall>ref \<in> set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)"
   413   shows "refs_of' h' r xs"
   414 using assms
   415 proof -
   416   from assms obtain prs where refs:"refs_of h (Ref.get h r) prs" and xs_def: "xs = r # prs"
   417     unfolding refs_of'_def' by auto
   418   from xs_def assms have x_eq: "Ref.get h r = Ref.get h' r" by fastsimp
   419   from refs assms xs_def have 2: "\<forall>refs. refs_of h (Ref.get h r) refs \<longrightarrow>
   420      (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)" 
   421     by (fastsimp dest: refs_of_is_fun)
   422   from refs_of_invariant [OF refs 2] xs_def x_eq show ?thesis
   423     unfolding refs_of'_def' by auto
   424 qed
   425 
   426 lemma list_of_invariant:
   427   assumes "list_of h (r::('a::heap) node) xs"
   428   assumes "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref \<in> set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)"
   429   shows "list_of h' r xs"
   430 using assms
   431 proof (induct xs arbitrary: r)
   432   case Nil thus ?case by simp
   433 next
   434   case (Cons x xs')
   435 
   436   from Cons(2) obtain ref where Node: "r = Node x ref"
   437     by (cases r, auto)
   438   from Cons(2) obtain rs where rs_def: "refs_of h r rs" by (rule list_of_refs_of)
   439   from Node rs_def obtain rss where refs_of: "refs_of h r (ref#rss)" and rss_def: "rs = ref#rss" by auto
   440   from Cons(3) Node refs_of have ref_eq: "Ref.get h ref = Ref.get h' ref"
   441     by auto
   442   from Cons(2) ref_eq Node have 1: "list_of h (Ref.get h' ref) xs'" by simp
   443   from refs_of Node ref_eq have refs_of_ref: "refs_of h (Ref.get h' ref) rss" by simp
   444   from Cons(3) rs_def have rs_heap_eq: "\<forall>ref\<in>set rs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref" by simp
   445   from refs_of_ref rs_heap_eq rss_def have 2: "\<forall>refs. refs_of h (Ref.get h' ref) refs \<longrightarrow>
   446           (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)"
   447     by (auto dest: refs_of_is_fun)
   448   from Cons(1)[OF 1 2]
   449   have "list_of h' (Ref.get h' ref) xs'" .
   450   with Node show ?case
   451     unfolding list_of'_def
   452     by simp
   453 qed
   454 
   455 lemma crel_ref:
   456   assumes "crel (ref v) h h' x"
   457   obtains "Ref.get h' x = v"
   458   and "\<not> Ref.present h x"
   459   and "Ref.present h' x"
   460   and "\<forall>y. Ref.present h y \<longrightarrow> Ref.get h y = Ref.get h' y"
   461  (* and "lim h' = Suc (lim h)" *)
   462   and "\<forall>y. Ref.present h y \<longrightarrow> Ref.present h' y"
   463   using assms
   464   unfolding Ref.ref_def
   465   apply (elim crel_heapE)
   466   unfolding Ref.alloc_def
   467   apply (simp add: Let_def)
   468   unfolding Ref.present_def
   469   apply auto
   470   unfolding Ref.get_def Ref.set_def
   471   apply auto
   472   done
   473 
   474 lemma make_llist:
   475 assumes "crel (make_llist xs) h h' r"
   476 shows "list_of h' r xs \<and> (\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref \<in> (set rs). Ref.present h' ref))"
   477 using assms 
   478 proof (induct xs arbitrary: h h' r)
   479   case Nil thus ?case by (auto elim: crel_returnE simp add: make_llist.simps)
   480 next
   481   case (Cons x xs')
   482   from Cons.prems obtain h1 r1 r' where make_llist: "crel (make_llist xs') h h1 r1"
   483     and crel_refnew:"crel (ref r1) h1 h' r'" and Node: "r = Node x r'"
   484     unfolding make_llist.simps
   485     by (auto elim!: crel_bindE crel_returnE)
   486   from Cons.hyps[OF make_llist] have list_of_h1: "list_of h1 r1 xs'" ..
   487   from Cons.hyps[OF make_llist] obtain rs' where rs'_def: "refs_of h1 r1 rs'" by (auto intro: list_of_refs_of)
   488   from Cons.hyps[OF make_llist] rs'_def have refs_present: "\<forall>ref\<in>set rs'. Ref.present h1 ref" by simp
   489   from crel_refnew rs'_def refs_present have refs_unchanged: "\<forall>refs. refs_of h1 r1 refs \<longrightarrow>
   490          (\<forall>ref\<in>set refs. Ref.present h1 ref \<and> Ref.present h' ref \<and> Ref.get h1 ref = Ref.get h' ref)"
   491     by (auto elim!: crel_ref dest: refs_of_is_fun)
   492   with list_of_invariant[OF list_of_h1 refs_unchanged] Node crel_refnew have fstgoal: "list_of h' r (x # xs')"
   493     unfolding list_of.simps
   494     by (auto elim!: crel_refE)
   495   from refs_unchanged rs'_def have refs_still_present: "\<forall>ref\<in>set rs'. Ref.present h' ref" by auto
   496   from refs_of_invariant[OF rs'_def refs_unchanged] refs_unchanged Node crel_refnew refs_still_present
   497   have sndgoal: "\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref\<in>set rs. Ref.present h' ref)"
   498     by (fastsimp elim!: crel_refE dest: refs_of_is_fun)
   499   from fstgoal sndgoal show ?case ..
   500 qed
   501 
   502 lemma traverse: "list_of h n r \<Longrightarrow> crel (traverse n) h h r"
   503 proof (induct r arbitrary: n)
   504   case Nil
   505   thus ?case
   506     by (auto intro: crel_returnI)
   507 next
   508   case (Cons x xs)
   509   thus ?case
   510   apply (cases n, auto)
   511   by (auto intro!: crel_bindI crel_returnI crel_lookupI)
   512 qed
   513 
   514 lemma traverse_make_llist':
   515   assumes crel: "crel (make_llist xs \<guillemotright>= traverse) h h' r"
   516   shows "r = xs"
   517 proof -
   518   from crel obtain h1 r1
   519     where makell: "crel (make_llist xs) h h1 r1"
   520     and trav: "crel (traverse r1) h1 h' r"
   521     by (auto elim!: crel_bindE)
   522   from make_llist[OF makell] have "list_of h1 r1 xs" ..
   523   from traverse [OF this] trav show ?thesis
   524     using crel_deterministic by fastsimp
   525 qed
   526 
   527 section {* Proving correctness of in-place reversal *}
   528 
   529 subsection {* Definition of in-place reversal *}
   530 
   531 definition rev' :: "(('a::heap) node ref \<times> 'a node ref) \<Rightarrow> 'a node ref Heap"
   532 where "rev' = MREC (\<lambda>(q, p). do { v \<leftarrow> !p; (case v of Empty \<Rightarrow> (return (Inl q))
   533                             | Node x next \<Rightarrow> do {
   534                                     p := Node x q;
   535                                     return (Inr (p, next))
   536                                   })})
   537              (\<lambda>x s z. return z)"
   538 
   539 lemma rev'_simps [code]:
   540   "rev' (q, p) =
   541    do {
   542      v \<leftarrow> !p;
   543      (case v of
   544         Empty \<Rightarrow> return q
   545       | Node x next \<Rightarrow>
   546         do {
   547           p := Node x q;
   548           rev' (p, next)
   549         })
   550   }"
   551   unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric]
   552 thm arg_cong2
   553   by (auto simp add: expand_fun_eq intro: arg_cong2[where f = bind] split: node.split)
   554 
   555 primrec rev :: "('a:: heap) node \<Rightarrow> 'a node Heap" 
   556 where
   557   "rev Empty = return Empty"
   558 | "rev (Node x n) = do { q \<leftarrow> ref Empty; p \<leftarrow> ref (Node x n); v \<leftarrow> rev' (q, p); !v }"
   559 
   560 subsection {* Correctness Proof *}
   561 
   562 lemma rev'_invariant:
   563   assumes "crel (rev' (q, p)) h h' v"
   564   assumes "list_of' h q qs"
   565   assumes "list_of' h p ps"
   566   assumes "\<forall>qrs prs. refs_of' h q qrs \<and> refs_of' h p prs \<longrightarrow> set prs \<inter> set qrs = {}"
   567   shows "\<exists>vs. list_of' h' v vs \<and> vs = (List.rev ps) @ qs"
   568 using assms
   569 proof (induct ps arbitrary: qs p q h)
   570   case Nil
   571   thus ?case
   572     unfolding rev'_simps[of q p] list_of'_def
   573     by (auto elim!: crel_bindE crel_lookupE crel_returnE)
   574 next
   575   case (Cons x xs)
   576   (*"LinkedList.list_of h' (get_ref v h') (List.rev xs @ x # qsa)"*)
   577   from Cons(4) obtain ref where 
   578     p_is_Node: "Ref.get h p = Node x ref"
   579     (*and "ref_present ref h"*)
   580     and list_of'_ref: "list_of' h ref xs"
   581     unfolding list_of'_def by (cases "Ref.get h p", auto)
   582   from p_is_Node Cons(2) have crel_rev': "crel (rev' (p, ref)) (Ref.set p (Node x q) h) h' v"
   583     by (auto simp add: rev'_simps [of q p] elim!: crel_bindE crel_lookupE crel_updateE)
   584   from Cons(3) obtain qrs where qrs_def: "refs_of' h q qrs" by (elim list_of'_refs_of')
   585   from Cons(4) obtain prs where prs_def: "refs_of' h p prs" by (elim list_of'_refs_of')
   586   from qrs_def prs_def Cons(5) have distinct_pointers: "set qrs \<inter> set prs = {}" by fastsimp
   587   from qrs_def prs_def distinct_pointers refs_of'E have p_notin_qrs: "p \<notin> set qrs" by fastsimp
   588   from Cons(3) qrs_def this have 1: "list_of' (Ref.set p (Node x q) h) p (x#qs)"
   589     unfolding list_of'_def  
   590     apply (simp)
   591     unfolding list_of'_def[symmetric]
   592     by (simp add: list_of'_set_ref)
   593   from list_of'_refs_of'2[OF Cons(4)] p_is_Node prs_def obtain refs where refs_def: "refs_of' h ref refs" and prs_refs: "prs = p # refs"
   594     unfolding refs_of'_def' by auto
   595   from prs_refs prs_def have p_not_in_refs: "p \<notin> set refs"
   596     by (fastsimp dest!: refs_of'_distinct)
   597   with refs_def p_is_Node list_of'_ref have 2: "list_of' (Ref.set p (Node x q) h) ref xs"
   598     by (auto simp add: list_of'_set_ref)
   599   from p_notin_qrs qrs_def have refs_of1: "refs_of' (Ref.set p (Node x q) h) p (p#qrs)"
   600     unfolding refs_of'_def'
   601     apply (simp)
   602     unfolding refs_of'_def'[symmetric]
   603     by (simp add: refs_of'_set_ref)
   604   from p_not_in_refs p_is_Node refs_def have refs_of2: "refs_of' (Ref.set p (Node x q) h) ref refs"
   605     by (simp add: refs_of'_set_ref)
   606   from p_not_in_refs refs_of1 refs_of2 distinct_pointers prs_refs have 3: "\<forall>qrs prs. refs_of' (Ref.set p (Node x q) h) p qrs \<and> refs_of' (Ref.set p (Node x q) h) ref prs \<longrightarrow> set prs \<inter> set qrs = {}"
   607     apply - apply (rule allI)+ apply (rule impI) apply (erule conjE)
   608     apply (drule refs_of'_is_fun) back back apply assumption
   609     apply (drule refs_of'_is_fun) back back apply assumption
   610     apply auto done
   611   from Cons.hyps [OF crel_rev' 1 2 3] show ?case by simp
   612 qed
   613 
   614 
   615 lemma rev_correctness:
   616   assumes list_of_h: "list_of h r xs"
   617   assumes validHeap: "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>r \<in> set refs. Ref.present h r)"
   618   assumes crel_rev: "crel (rev r) h h' r'"
   619   shows "list_of h' r' (List.rev xs)"
   620 using assms
   621 proof (cases r)
   622   case Empty
   623   with list_of_h crel_rev show ?thesis
   624     by (auto simp add: list_of_Empty elim!: crel_returnE)
   625 next
   626   case (Node x ps)
   627   with crel_rev obtain p q h1 h2 h3 v where
   628     init: "crel (ref Empty) h h1 q"
   629     "crel (ref (Node x ps)) h1 h2 p"
   630     and crel_rev':"crel (rev' (q, p)) h2 h3 v"
   631     and lookup: "crel (!v) h3 h' r'"
   632     using rev.simps
   633     by (auto elim!: crel_bindE)
   634   from init have a1:"list_of' h2 q []"
   635     unfolding list_of'_def
   636     by (auto elim!: crel_ref)
   637   from list_of_h obtain refs where refs_def: "refs_of h r refs" by (rule list_of_refs_of)
   638   from validHeap init refs_def have heap_eq: "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h2 ref \<and> Ref.get h ref = Ref.get h2 ref)"
   639     by (fastsimp elim!: crel_ref dest: refs_of_is_fun)
   640   from list_of_invariant[OF list_of_h heap_eq] have "list_of h2 r xs" .
   641   from init this Node have a2: "list_of' h2 p xs"
   642     apply -
   643     unfolding list_of'_def
   644     apply (auto elim!: crel_refE)
   645     done
   646   from init have refs_of_q: "refs_of' h2 q [q]"
   647     by (auto elim!: crel_ref)
   648   from refs_def Node have refs_of'_ps: "refs_of' h ps refs"
   649     by (auto simp add: refs_of'_def'[symmetric])
   650   from validHeap refs_def have all_ref_present: "\<forall>r\<in>set refs. Ref.present h r" by simp
   651   from init refs_of'_ps Node this have heap_eq: "\<forall>refs. refs_of' h ps refs \<longrightarrow> (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h2 ref \<and> Ref.get h ref = Ref.get h2 ref)"
   652     by (fastsimp elim!: crel_ref dest: refs_of'_is_fun)
   653   from refs_of'_invariant[OF refs_of'_ps this] have "refs_of' h2 ps refs" .
   654   with init have refs_of_p: "refs_of' h2 p (p#refs)"
   655     by (auto elim!: crel_refE simp add: refs_of'_def')
   656   with init all_ref_present have q_is_new: "q \<notin> set (p#refs)"
   657     by (auto elim!: crel_refE intro!: Ref.noteq_I)
   658   from refs_of_p refs_of_q q_is_new have a3: "\<forall>qrs prs. refs_of' h2 q qrs \<and> refs_of' h2 p prs \<longrightarrow> set prs \<inter> set qrs = {}"
   659     by (fastsimp simp only: set.simps dest: refs_of'_is_fun)
   660   from rev'_invariant [OF crel_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" 
   661     unfolding list_of'_def by auto
   662   with lookup show ?thesis
   663     by (auto elim: crel_lookupE)
   664 qed
   665 
   666 
   667 section {* The merge function on Linked Lists *}
   668 text {* We also prove merge correct *}
   669 
   670 text{* First, we define merge on lists in a natural way. *}
   671 
   672 fun Lmerge :: "('a::ord) list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   673 where
   674   "Lmerge (x#xs) (y#ys) =
   675      (if x \<le> y then x # Lmerge xs (y#ys) else y # Lmerge (x#xs) ys)"
   676 | "Lmerge [] ys = ys"
   677 | "Lmerge xs [] = xs"
   678 
   679 subsection {* Definition of merge function *}
   680 
   681 definition merge' :: "(('a::{heap, ord}) node ref * ('a::{heap, ord})) * ('a::{heap, ord}) node ref * ('a::{heap, ord}) node ref \<Rightarrow> ('a::{heap, ord}) node ref Heap"
   682 where
   683 "merge' = MREC (\<lambda>(_, p, q). do { v \<leftarrow> !p; w \<leftarrow> !q;
   684   (case v of Empty \<Rightarrow> return (Inl q)
   685           | Node valp np \<Rightarrow>
   686             (case w of Empty \<Rightarrow> return (Inl p)
   687                      | Node valq nq \<Rightarrow>
   688                        if (valp \<le> valq) then
   689                          return (Inr ((p, valp), np, q))
   690                        else
   691                          return (Inr ((q, valq), p, nq)))) })
   692  (\<lambda> _ ((n, v), _, _) r. do { n := Node v r; return n })"
   693 
   694 definition merge where "merge p q = merge' (undefined, p, q)"
   695 
   696 lemma if_return: "(if P then return x else return y) = return (if P then x else y)"
   697 by auto
   698 
   699 lemma if_distrib_App: "(if P then f else g) x = (if P then f x else g x)"
   700 by auto
   701 lemma redundant_if: "(if P then (if P then x else z) else y) = (if P then x else y)"
   702   "(if P then x else (if P then z else y)) = (if P then x else y)"
   703 by auto
   704 
   705 
   706 
   707 lemma sum_distrib: "sum_case fl fr (case x of Empty \<Rightarrow> y | Node v n \<Rightarrow> (z v n)) = (case x of Empty \<Rightarrow> sum_case fl fr y | Node v n \<Rightarrow> sum_case fl fr (z v n))"
   708 by (cases x) auto
   709 
   710 lemma merge: "merge' (x, p, q) = merge p q"
   711 unfolding merge'_def merge_def
   712 apply (simp add: MREC_rule) done
   713 term "Ref.change"
   714 lemma merge_simps [code]:
   715 shows "merge p q =
   716 do { v \<leftarrow> !p;
   717    w \<leftarrow> !q;
   718    (case v of node.Empty \<Rightarrow> return q
   719     | Node valp np \<Rightarrow>
   720         case w of node.Empty \<Rightarrow> return p
   721         | Node valq nq \<Rightarrow>
   722             if valp \<le> valq then do { r \<leftarrow> merge np q;
   723                                    p := (Node valp r);
   724                                    return p
   725                                 }
   726             else do { r \<leftarrow> merge p nq;
   727                     q := (Node valq r);
   728                     return q
   729                  })
   730 }"
   731 proof -
   732   {fix v x y
   733     have case_return: "(case v of Empty \<Rightarrow> return x | Node v n \<Rightarrow> return (y v n)) = return (case v of Empty \<Rightarrow> x | Node v n \<Rightarrow> y v n)" by (cases v) auto
   734     } note case_return = this
   735 show ?thesis
   736 unfolding merge_def[of p q] merge'_def
   737 apply (simp add: MREC_rule[of _ _ "(undefined, p, q)"])
   738 unfolding bind_bind return_bind
   739 unfolding merge'_def[symmetric]
   740 unfolding if_return case_return bind_bind return_bind sum_distrib sum.cases
   741 unfolding if_distrib[symmetric, where f="Inr"]
   742 unfolding sum.cases
   743 unfolding if_distrib
   744 unfolding split_beta fst_conv snd_conv
   745 unfolding if_distrib_App redundant_if merge
   746 ..
   747 qed
   748 
   749 subsection {* Induction refinement by applying the abstraction function to our induct rule *}
   750 
   751 text {* From our original induction rule Lmerge.induct, we derive a new rule with our list_of' predicate *}
   752 
   753 lemma merge_induct2:
   754   assumes "list_of' h (p::'a::{heap, ord} node ref) xs"
   755   assumes "list_of' h q ys"
   756   assumes "\<And> ys p q. \<lbrakk> list_of' h p []; list_of' h q ys; Ref.get h p = Empty \<rbrakk> \<Longrightarrow> P p q [] ys"
   757   assumes "\<And> x xs' p q pn. \<lbrakk> list_of' h p (x#xs'); list_of' h q []; Ref.get h p = Node x pn; Ref.get h q = Empty \<rbrakk> \<Longrightarrow> P p q (x#xs') []"
   758   assumes "\<And> x xs' y ys' p q pn qn.
   759   \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys'); Ref.get h p = Node x pn; Ref.get h q = Node y qn;
   760   x \<le> y; P pn q xs' (y#ys') \<rbrakk>
   761   \<Longrightarrow> P p q (x#xs') (y#ys')"
   762   assumes "\<And> x xs' y ys' p q pn qn.
   763   \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys'); Ref.get h p = Node x pn; Ref.get h q = Node y qn;
   764   \<not> x \<le> y; P p qn (x#xs') ys'\<rbrakk>
   765   \<Longrightarrow> P p q (x#xs') (y#ys')"
   766   shows "P p q xs ys"
   767 using assms(1-2)
   768 proof (induct xs ys arbitrary: p q rule: Lmerge.induct)
   769   case (2 ys)
   770   from 2(1) have "Ref.get h p = Empty" unfolding list_of'_def by simp
   771   with 2(1-2) assms(3) show ?case by blast
   772 next
   773   case (3 x xs')
   774   from 3(1) obtain pn where Node: "Ref.get h p = Node x pn" by (rule list_of'_Cons)
   775   from 3(2) have "Ref.get h q = Empty" unfolding list_of'_def by simp
   776   with Node 3(1-2) assms(4) show ?case by blast
   777 next
   778   case (1 x xs' y ys')
   779   from 1(3) obtain pn where pNode:"Ref.get h p = Node x pn"
   780     and list_of'_pn: "list_of' h pn xs'" by (rule list_of'_Cons)
   781   from 1(4) obtain qn where qNode:"Ref.get h q = Node y qn"
   782     and  list_of'_qn: "list_of' h qn ys'" by (rule list_of'_Cons)
   783   show ?case
   784   proof (cases "x \<le> y")
   785     case True
   786     from 1(1)[OF True list_of'_pn 1(4)] assms(5) 1(3-4) pNode qNode True
   787     show ?thesis by blast
   788   next
   789     case False
   790     from 1(2)[OF False 1(3) list_of'_qn] assms(6) 1(3-4) pNode qNode False
   791     show ?thesis by blast
   792   qed
   793 qed
   794 
   795 
   796 text {* secondly, we add the crel statement in the premise, and derive the crel statements for the single cases which we then eliminate with our crel elim rules. *}
   797   
   798 lemma merge_induct3: 
   799 assumes  "list_of' h p xs"
   800 assumes  "list_of' h q ys"
   801 assumes  "crel (merge p q) h h' r"
   802 assumes  "\<And> ys p q. \<lbrakk> list_of' h p []; list_of' h q ys; Ref.get h p = Empty \<rbrakk> \<Longrightarrow> P p q h h q [] ys"
   803 assumes  "\<And> x xs' p q pn. \<lbrakk> list_of' h p (x#xs'); list_of' h q []; Ref.get h p = Node x pn; Ref.get h q = Empty \<rbrakk> \<Longrightarrow> P p q h h p (x#xs') []"
   804 assumes  "\<And> x xs' y ys' p q pn qn h1 r1 h'.
   805   \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys');Ref.get h p = Node x pn; Ref.get h q = Node y qn;
   806   x \<le> y; crel (merge pn q) h h1 r1 ; P pn q h h1 r1 xs' (y#ys'); h' = Ref.set p (Node x r1) h1 \<rbrakk>
   807   \<Longrightarrow> P p q h h' p (x#xs') (y#ys')"
   808 assumes "\<And> x xs' y ys' p q pn qn h1 r1 h'.
   809   \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys'); Ref.get h p = Node x pn; Ref.get h q = Node y qn;
   810   \<not> x \<le> y; crel (merge p qn) h h1 r1; P p qn h h1 r1 (x#xs') ys'; h' = Ref.set q (Node y r1) h1 \<rbrakk>
   811   \<Longrightarrow> P p q h h' q (x#xs') (y#ys')"
   812 shows "P p q h h' r xs ys"
   813 using assms(3)
   814 proof (induct arbitrary: h' r rule: merge_induct2[OF assms(1) assms(2)])
   815   case (1 ys p q)
   816   from 1(3-4) have "h = h' \<and> r = q"
   817     unfolding merge_simps[of p q]
   818     by (auto elim!: crel_lookupE crel_bindE crel_returnE)
   819   with assms(4)[OF 1(1) 1(2) 1(3)] show ?case by simp
   820 next
   821   case (2 x xs' p q pn)
   822   from 2(3-5) have "h = h' \<and> r = p"
   823     unfolding merge_simps[of p q]
   824     by (auto elim!: crel_lookupE crel_bindE crel_returnE)
   825   with assms(5)[OF 2(1-4)] show ?case by simp
   826 next
   827   case (3 x xs' y ys' p q pn qn)
   828   from 3(3-5) 3(7) obtain h1 r1 where
   829     1: "crel (merge pn q) h h1 r1" 
   830     and 2: "h' = Ref.set p (Node x r1) h1 \<and> r = p"
   831     unfolding merge_simps[of p q]
   832     by (auto elim!: crel_lookupE crel_bindE crel_returnE crel_ifE crel_updateE)
   833   from 3(6)[OF 1] assms(6) [OF 3(1-5)] 1 2 show ?case by simp
   834 next
   835   case (4 x xs' y ys' p q pn qn)
   836   from 4(3-5) 4(7) obtain h1 r1 where
   837     1: "crel (merge p qn) h h1 r1" 
   838     and 2: "h' = Ref.set q (Node y r1) h1 \<and> r = q"
   839     unfolding merge_simps[of p q]
   840     by (auto elim!: crel_lookupE crel_bindE crel_returnE crel_ifE crel_updateE)
   841   from 4(6)[OF 1] assms(7) [OF 4(1-5)] 1 2 show ?case by simp
   842 qed
   843 
   844 
   845 subsection {* Proving merge correct *}
   846 
   847 text {* As many parts of the following three proofs are identical, we could actually move the
   848 same reasoning into an extended induction rule *}
   849  
   850 lemma merge_unchanged:
   851   assumes "refs_of' h p xs"
   852   assumes "refs_of' h q ys"  
   853   assumes "crel (merge p q) h h' r'"
   854   assumes "set xs \<inter> set ys = {}"
   855   assumes "r \<notin> set xs \<union> set ys"
   856   shows "Ref.get h r = Ref.get h' r"
   857 proof -
   858   from assms(1) obtain ps where ps_def: "list_of' h p ps" by (rule refs_of'_list_of')
   859   from assms(2) obtain qs where qs_def: "list_of' h q qs" by (rule refs_of'_list_of')
   860   show ?thesis using assms(1) assms(2) assms(4) assms(5)
   861   proof (induct arbitrary: xs ys r rule: merge_induct3[OF ps_def qs_def assms(3)])
   862     case 1 thus ?case by simp
   863   next
   864     case 2 thus ?case by simp
   865   next
   866     case (3 x xs' y ys' p q pn qn h1 r1 h' xs ys r)
   867     from 3(9) 3(3) obtain pnrs
   868       where pnrs_def: "xs = p#pnrs"
   869       and refs_of'_pn: "refs_of' h pn pnrs"
   870       by (rule refs_of'_Node)
   871     with 3(12) have r_in: "r \<notin> set pnrs \<union> set ys" by auto
   872     from pnrs_def 3(12) have "r \<noteq> p" by auto
   873     with 3(11) 3(12) pnrs_def refs_of'_distinct[OF 3(9)] have p_in: "p \<notin> set pnrs \<union> set ys" by auto
   874     from 3(11) pnrs_def have no_inter: "set pnrs \<inter> set ys = {}" by auto
   875     from 3(7)[OF refs_of'_pn 3(10) this p_in] 3(3) have p_is_Node: "Ref.get h1 p = Node x pn"
   876       by simp
   877     from 3(7)[OF refs_of'_pn 3(10) no_inter r_in] 3(8) `r \<noteq> p` show ?case
   878       by simp
   879   next
   880     case (4 x xs' y ys' p q pn qn h1 r1 h' xs ys r)
   881     from 4(10) 4(4) obtain qnrs
   882       where qnrs_def: "ys = q#qnrs"
   883       and refs_of'_qn: "refs_of' h qn qnrs"
   884       by (rule refs_of'_Node)
   885     with 4(12) have r_in: "r \<notin> set xs \<union> set qnrs" by auto
   886     from qnrs_def 4(12) have "r \<noteq> q" by auto
   887     with 4(11) 4(12) qnrs_def refs_of'_distinct[OF 4(10)] have q_in: "q \<notin> set xs \<union> set qnrs" by auto
   888     from 4(11) qnrs_def have no_inter: "set xs \<inter> set qnrs = {}" by auto
   889     from 4(7)[OF 4(9) refs_of'_qn this q_in] 4(4) have q_is_Node: "Ref.get h1 q = Node y qn" by simp
   890     from 4(7)[OF 4(9) refs_of'_qn no_inter r_in] 4(8) `r \<noteq> q` show ?case
   891       by simp
   892   qed
   893 qed
   894 
   895 lemma refs_of'_merge:
   896   assumes "refs_of' h p xs"
   897   assumes "refs_of' h q ys"
   898   assumes "crel (merge p q) h h' r"
   899   assumes "set xs \<inter> set ys = {}"
   900   assumes "refs_of' h' r rs"
   901   shows "set rs \<subseteq> set xs \<union> set ys"
   902 proof -
   903   from assms(1) obtain ps where ps_def: "list_of' h p ps" by (rule refs_of'_list_of')
   904   from assms(2) obtain qs where qs_def: "list_of' h q qs" by (rule refs_of'_list_of')
   905   show ?thesis using assms(1) assms(2) assms(4) assms(5)
   906   proof (induct arbitrary: xs ys rs rule: merge_induct3[OF ps_def qs_def assms(3)])
   907     case 1
   908     from 1(5) 1(7) have "rs = ys" by (fastsimp simp add: refs_of'_is_fun)
   909     thus ?case by auto
   910   next
   911     case 2
   912     from 2(5) 2(8) have "rs = xs" by (auto simp add: refs_of'_is_fun)
   913     thus ?case by auto
   914   next
   915     case (3 x xs' y ys' p q pn qn h1 r1 h' xs ys rs)
   916     from 3(9) 3(3) obtain pnrs
   917       where pnrs_def: "xs = p#pnrs"
   918       and refs_of'_pn: "refs_of' h pn pnrs"
   919       by (rule refs_of'_Node)
   920     from 3(10) 3(9) 3(11) pnrs_def refs_of'_distinct[OF 3(9)] have p_in: "p \<notin> set pnrs \<union> set ys" by auto
   921     from 3(11) pnrs_def have no_inter: "set pnrs \<inter> set ys = {}" by auto
   922     from merge_unchanged[OF refs_of'_pn 3(10) 3(6) no_inter p_in] have p_stays: "Ref.get h1 p = Ref.get h p" ..
   923     from 3 p_stays obtain r1s
   924       where rs_def: "rs = p#r1s" and refs_of'_r1:"refs_of' h1 r1 r1s"
   925       by (auto elim: refs_of'_set_next_ref)
   926     from 3(7)[OF refs_of'_pn 3(10) no_inter refs_of'_r1] rs_def pnrs_def show ?case by auto
   927   next
   928     case (4 x xs' y ys' p q pn qn h1 r1 h' xs ys rs)
   929     from 4(10) 4(4) obtain qnrs
   930       where qnrs_def: "ys = q#qnrs"
   931       and refs_of'_qn: "refs_of' h qn qnrs"
   932       by (rule refs_of'_Node)
   933     from 4(10) 4(9) 4(11) qnrs_def refs_of'_distinct[OF 4(10)] have q_in: "q \<notin> set xs \<union> set qnrs" by auto
   934     from 4(11) qnrs_def have no_inter: "set xs \<inter> set qnrs = {}" by auto
   935     from merge_unchanged[OF 4(9) refs_of'_qn 4(6) no_inter q_in] have q_stays: "Ref.get h1 q = Ref.get h q" ..
   936     from 4 q_stays obtain r1s
   937       where rs_def: "rs = q#r1s" and refs_of'_r1:"refs_of' h1 r1 r1s"
   938       by (auto elim: refs_of'_set_next_ref)
   939     from 4(7)[OF 4(9) refs_of'_qn no_inter refs_of'_r1] rs_def qnrs_def show ?case by auto
   940   qed
   941 qed
   942 
   943 lemma
   944   assumes "list_of' h p xs"
   945   assumes "list_of' h q ys"
   946   assumes "crel (merge p q) h h' r"
   947   assumes "\<forall>qrs prs. refs_of' h q qrs \<and> refs_of' h p prs \<longrightarrow> set prs \<inter> set qrs = {}"
   948   shows "list_of' h' r (Lmerge xs ys)"
   949 using assms(4)
   950 proof (induct rule: merge_induct3[OF assms(1-3)])
   951   case 1
   952   thus ?case by simp
   953 next
   954   case 2
   955   thus ?case by simp
   956 next
   957   case (3 x xs' y ys' p q pn qn h1 r1 h')
   958   from 3(1) obtain prs where prs_def: "refs_of' h p prs" by (rule list_of'_refs_of')
   959   from 3(2) obtain qrs where qrs_def: "refs_of' h q qrs" by (rule list_of'_refs_of')
   960   from prs_def 3(3) obtain pnrs
   961     where pnrs_def: "prs = p#pnrs"
   962     and refs_of'_pn: "refs_of' h pn pnrs"
   963     by (rule refs_of'_Node)
   964   from prs_def qrs_def 3(9) pnrs_def refs_of'_distinct[OF prs_def] have p_in: "p \<notin> set pnrs \<union> set qrs" by fastsimp
   965   from prs_def qrs_def 3(9) pnrs_def have no_inter: "set pnrs \<inter> set qrs = {}" by fastsimp
   966   from no_inter refs_of'_pn qrs_def have no_inter2: "\<forall>qrs prs. refs_of' h q qrs \<and> refs_of' h pn prs \<longrightarrow> set prs \<inter> set qrs = {}"
   967     by (fastsimp dest: refs_of'_is_fun)
   968   from merge_unchanged[OF refs_of'_pn qrs_def 3(6) no_inter p_in] have p_stays: "Ref.get h1 p = Ref.get h p" ..
   969   from 3(7)[OF no_inter2] obtain rs where rs_def: "refs_of' h1 r1 rs" by (rule list_of'_refs_of')
   970   from refs_of'_merge[OF refs_of'_pn qrs_def 3(6) no_inter this] p_in have p_rs: "p \<notin> set rs" by auto
   971   with 3(7)[OF no_inter2] 3(1-5) 3(8) p_rs rs_def p_stays
   972   show ?case by auto
   973 next
   974   case (4 x xs' y ys' p q pn qn h1 r1 h')
   975   from 4(1) obtain prs where prs_def: "refs_of' h p prs" by (rule list_of'_refs_of')
   976   from 4(2) obtain qrs where qrs_def: "refs_of' h q qrs" by (rule list_of'_refs_of')
   977   from qrs_def 4(4) obtain qnrs
   978     where qnrs_def: "qrs = q#qnrs"
   979     and refs_of'_qn: "refs_of' h qn qnrs"
   980     by (rule refs_of'_Node)
   981   from prs_def qrs_def 4(9) qnrs_def refs_of'_distinct[OF qrs_def] have q_in: "q \<notin> set prs \<union> set qnrs" by fastsimp
   982   from prs_def qrs_def 4(9) qnrs_def have no_inter: "set prs \<inter> set qnrs = {}" by fastsimp
   983   from no_inter refs_of'_qn prs_def have no_inter2: "\<forall>qrs prs. refs_of' h qn qrs \<and> refs_of' h p prs \<longrightarrow> set prs \<inter> set qrs = {}"
   984     by (fastsimp dest: refs_of'_is_fun)
   985   from merge_unchanged[OF prs_def refs_of'_qn 4(6) no_inter q_in] have q_stays: "Ref.get h1 q = Ref.get h q" ..
   986   from 4(7)[OF no_inter2] obtain rs where rs_def: "refs_of' h1 r1 rs" by (rule list_of'_refs_of')
   987   from refs_of'_merge[OF prs_def refs_of'_qn 4(6) no_inter this] q_in have q_rs: "q \<notin> set rs" by auto
   988   with 4(7)[OF no_inter2] 4(1-5) 4(8) q_rs rs_def q_stays
   989   show ?case by auto
   990 qed
   991 
   992 section {* Code generation *}
   993 
   994 text {* A simple example program *}
   995 
   996 definition test_1 where "test_1 = (do { ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs })" 
   997 definition test_2 where "test_2 = (do { ll_xs <- make_llist [1..(15::int)]; ll_ys <- rev ll_xs; ys <- traverse ll_ys; return ys })"
   998 
   999 definition test_3 where "test_3 =
  1000   (do {
  1001     ll_xs \<leftarrow> make_llist (filter (%n. n mod 2 = 0) [2..8]);
  1002     ll_ys \<leftarrow> make_llist (filter (%n. n mod 2 = 1) [5..11]);
  1003     r \<leftarrow> ref ll_xs;
  1004     q \<leftarrow> ref ll_ys;
  1005     p \<leftarrow> merge r q;
  1006     ll_zs \<leftarrow> !p;
  1007     zs \<leftarrow> traverse ll_zs;
  1008     return zs
  1009   })"
  1010 
  1011 code_reserved SML upto
  1012 
  1013 ML {* @{code test_1} () *}
  1014 ML {* @{code test_2} () *}
  1015 ML {* @{code test_3} () *}
  1016 
  1017 export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
  1018 
  1019 end