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