src/HOL/Imperative_HOL/ex/Linked_Lists.thy

 (*  Title:      HOL/Imperative_HOL/ex/Linked_Lists.thy
     Author:     Lukas Bulwahn, TU Muenchen
 *)
 
-section {* Linked Lists by ML references *}
+section \<open>Linked Lists by ML references\<close>
 
 theory Linked_Lists
 imports "../Imperative_HOL" "~~/src/HOL/Library/Code_Target_Int"
 begin
 
-section {* Definition of Linked Lists *}
-
-setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a::type ref"}) *}
+section \<open>Definition of Linked Lists\<close>
+
+setup \<open>Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a::type ref"})\<close>
 datatype 'a node = Empty | Node 'a "'a node ref"
 
 primrec
   node_encode :: "'a::countable node \<Rightarrow> nat"
 where

                               return (x#xs)
                          }"
 by (simp_all add: traverse.simps[of "Empty"] traverse.simps[of "Node x r"])
 
 
-section {* Proving correctness with relational abstraction *}
-
-subsection {* Definition of list_of, list_of', refs_of and refs_of' *}
+section \<open>Proving correctness with relational abstraction\<close>
+
+subsection \<open>Definition of list_of, list_of', refs_of and refs_of'\<close>
 
 primrec list_of :: "heap \<Rightarrow> ('a::heap) node \<Rightarrow> 'a list \<Rightarrow> bool"
 where
   "list_of h r [] = (r = Empty)"
 | "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))"

 where
   "refs_of' h r [] = False"
 | "refs_of' h r (x#xs) = ((x = r) \<and> refs_of h (Ref.get h x) xs)"
 
 
-subsection {* Properties of these definitions *}
+subsection \<open>Properties of these definitions\<close>
 
 lemma list_of_Empty[simp]: "list_of h Empty xs = (xs = [])"
 by (cases xs, auto)
 
 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')"

 proof -
   from assms obtain rs where "refs_of' h r rs" by (rule list_of'_refs_of')
   thus ?thesis by (auto simp add: refs_of'_def')
 qed
 
-subsection {* More complicated properties of these predicates *}
+subsection \<open>More complicated properties of these predicates\<close>
 
 lemma list_of_append:
   "list_of h n (as @ bs) \<Longrightarrow> \<exists>m. list_of h m bs"
 apply (induct as arbitrary: n)
 apply auto

 lemma refs_of'_distinct: "refs_of' h p rs \<Longrightarrow> distinct rs"
   unfolding refs_of'_def'
   by (fastforce simp add: refs_of_distinct refs_of_next)
 
 
-subsection {* Interaction of these predicates with our heap transitions *}
+subsection \<open>Interaction of these predicates with our heap transitions\<close>
 
 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"
 proof (induct as arbitrary: q rs)
   case Nil thus ?case by simp
 next

     unfolding refs_of'_def'[of _ p]
     apply (auto, frule refs_of_set_ref2) by (auto dest: Ref.noteq_sym)
   with assms that show thesis by auto
 qed
 
-section {* Proving make_llist and traverse correct *}
+section \<open>Proving make_llist and traverse correct\<close>
 
 lemma refs_of_invariant:
   assumes "refs_of h (r::('a::heap) node) xs"
   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)"
   shows "refs_of h' r xs"

   from make_llist[OF makell] have "list_of h1 r1 xs" ..
   from traverse [OF this] trav show ?thesis
     using effect_deterministic by fastforce
 qed
 
-section {* Proving correctness of in-place reversal *}
-
-subsection {* Definition of in-place reversal *}
+section \<open>Proving correctness of in-place reversal\<close>
+
+subsection \<open>Definition of in-place reversal\<close>
 
 partial_function (heap) rev' :: "('a::heap) node ref \<Rightarrow> 'a node ref \<Rightarrow> 'a node ref Heap"
 where
   [code]: "rev' q p =
    do {

 primrec rev :: "('a:: heap) node \<Rightarrow> 'a node Heap" 
 where
   "rev Empty = return Empty"
 | "rev (Node x n) = do { q \<leftarrow> ref Empty; p \<leftarrow> ref (Node x n); v \<leftarrow> rev' q p; !v }"
 
-subsection {* Correctness Proof *}
+subsection \<open>Correctness Proof\<close>
 
 lemma rev'_invariant:
   assumes "effect (rev' q p) h h' v"
   assumes "list_of' h q qs"
   assumes "list_of' h p ps"

   with lookup show ?thesis
     by (auto elim: effect_lookupE)
 qed
 
 
-section {* The merge function on Linked Lists *}
-text {* We also prove merge correct *}
-
-text{* First, we define merge on lists in a natural way. *}
+section \<open>The merge function on Linked Lists\<close>
+text \<open>We also prove merge correct\<close>
+
+text\<open>First, we define merge on lists in a natural way.\<close>
 
 fun Lmerge :: "('a::ord) list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "Lmerge (x#xs) (y#ys) =
      (if x \<le> y then x # Lmerge xs (y#ys) else y # Lmerge (x#xs) ys)"
 | "Lmerge [] ys = ys"
 | "Lmerge xs [] = xs"
 
-subsection {* Definition of merge function *}
+subsection \<open>Definition of merge function\<close>
 
 partial_function (heap) merge :: "('a::{heap, ord}) node ref \<Rightarrow> 'a node ref \<Rightarrow> 'a node ref Heap"
 where
 [code]: "merge p q = (do { v \<leftarrow> !p; w \<leftarrow> !q;
   (case v of Empty \<Rightarrow> return q

 
 
 lemma sum_distrib: "case_sum fl fr (case x of Empty \<Rightarrow> y | Node v n \<Rightarrow> (z v n)) = (case x of Empty \<Rightarrow> case_sum fl fr y | Node v n \<Rightarrow> case_sum fl fr (z v n))"
 by (cases x) auto
 
-subsection {* Induction refinement by applying the abstraction function to our induct rule *}
-
-text {* From our original induction rule Lmerge.induct, we derive a new rule with our list_of' predicate *}
+subsection \<open>Induction refinement by applying the abstraction function to our induct rule\<close>
+
+text \<open>From our original induction rule Lmerge.induct, we derive a new rule with our list_of' predicate\<close>
 
 lemma merge_induct2:
   assumes "list_of' h (p::'a::{heap, ord} node ref) xs"
   assumes "list_of' h q ys"
   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"

     show ?thesis by blast
   qed
 qed
 
 
-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. *}
+text \<open>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.\<close>
   
 lemma merge_induct3: 
 assumes  "list_of' h p xs"
 assumes  "list_of' h q ys"
 assumes  "effect (merge p q) h h' r"

     by (auto elim!: effect_lookupE effect_bindE effect_returnE effect_ifE effect_updateE)
   from 4(6)[OF 1] assms(7) [OF 4(1-5)] 1 2 show ?case by simp
 qed
 
 
-subsection {* Proving merge correct *}
-
-text {* As many parts of the following three proofs are identical, we could actually move the
-same reasoning into an extended induction rule *}
+subsection \<open>Proving merge correct\<close>
+
+text \<open>As many parts of the following three proofs are identical, we could actually move the
+same reasoning into an extended induction rule\<close>
  
 lemma merge_unchanged:
   assumes "refs_of' h p xs"
   assumes "refs_of' h q ys"  
   assumes "effect (merge p q) h h' r'"

     from pnrs_def 3(12) have "r \<noteq> p" by auto
     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
     from 3(11) pnrs_def have no_inter: "set pnrs \<inter> set ys = {}" by auto
     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"
       by simp
-    from 3(7)[OF refs_of'_pn 3(10) no_inter r_in] 3(8) `r \<noteq> p` show ?case
+    from 3(7)[OF refs_of'_pn 3(10) no_inter r_in] 3(8) \<open>r \<noteq> p\<close> show ?case
       by simp
   next
     case (4 x xs' y ys' p q pn qn h1 r1 h' xs ys r)
     from 4(10) 4(4) obtain qnrs
       where qnrs_def: "ys = q#qnrs"

     with 4(12) have r_in: "r \<notin> set xs \<union> set qnrs" by auto
     from qnrs_def 4(12) have "r \<noteq> q" by auto
     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
     from 4(11) qnrs_def have no_inter: "set xs \<inter> set qnrs = {}" by auto
     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
-    from 4(7)[OF 4(9) refs_of'_qn no_inter r_in] 4(8) `r \<noteq> q` show ?case
+    from 4(7)[OF 4(9) refs_of'_qn no_inter r_in] 4(8) \<open>r \<noteq> q\<close> show ?case
       by simp
   qed
 qed
 
 lemma refs_of'_merge:

   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
   with 4(7)[OF no_inter2] 4(1-5) 4(8) q_rs rs_def q_stays
   show ?case by (auto simp: list_of'_set_ref)
 qed
 
-section {* Code generation *}
-
-text {* A simple example program *}
+section \<open>Code generation\<close>
+
+text \<open>A simple example program\<close>
 
 definition test_1 where "test_1 = (do { ll_xs \<leftarrow> make_llist [1..(15::int)]; xs \<leftarrow> traverse ll_xs; return xs })" 
 definition test_2 where "test_2 = (do { ll_xs \<leftarrow> make_llist [1..(15::int)]; ll_ys \<leftarrow> rev ll_xs; ys \<leftarrow> traverse ll_ys; return ys })"
 
 definition test_3 where "test_3 =

     return zs
   })"
 
 code_reserved SML upto
 
-ML_val {* @{code test_1} () *}
-ML_val {* @{code test_2} () *}
-ML_val {* @{code test_3} () *}
+ML_val \<open>@{code test_1} ()\<close>
+ML_val \<open>@{code test_2} ()\<close>
+ML_val \<open>@{code test_3} ()\<close>
 
 export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end