Theory itp_2010

section ‹\isaheader{Examples from ITP-2010 slides (adopted to ICF v2)}›
theory itp_2010
imports 
  Collections.Collections 
  Collections.Code_Target_ICF
begin

text ‹
  Illustrates the various possibilities how to use the ICF in your own 
  algorithms by simple examples. The examples all use the data refinement
  scheme, and either define a generic algorithm or fix the operations.
›


subsection "List to Set"
text ‹
  In this simple example we do conversion from a list to a set.
  We define an abstract algorithm.
  This is then refined by a generic algorithm using a locale and by a generic 
  algorithm fixing its operations as parameters.
›
  subsubsection "Straightforward version"
  ― ‹Abstract algorithm›
  fun set_a where
    "set_a [] s = s" |
    "set_a (a#l) s = set_a l (insert a s)"

  ― ‹Correctness of aa›
  lemma set_a_correct: "set_a l s = set l ∪ s"
    by (induct l arbitrary: s) auto

  ― ‹Generic algorithm›

  setup Locale_Code.open_block ― ‹Required to make definitions inside locales
    executable›
  fun (in StdSetDefs) set_i where
    "set_i [] s = s" |
    "set_i (a#l) s = set_i l (ins a s)"
  setup Locale_Code.close_block

  ― ‹Correct implementation of ca›
  lemma (in StdSet) set_i_impl: "invar s ⟹ invar (set_i l s) ∧ α (set_i l s) = set_a l (α s)"
    by (induct l arbitrary: s) (auto simp add: correct)

  ― ‹Instantiation›
  (* We need to declare a constant to make the code generator work *)

  definition "hs_seti == hs.set_i"
  (*declare hs.set_i.simps[folded hs_seti_def, code]*)

  lemmas hs_set_i_impl = hs.set_i_impl[folded hs_seti_def]

export_code hs_seti checking SML

  ― ‹Code generation›
  ML ‹@{code hs_seti}› 
  (*value "hs_seti [1,2,3::nat] hs_empty"*)

  subsubsection "Tail-Recursive version"
  ― ‹Abstract algorithm›
  fun set_a2 where
    "set_a2 [] = {}" |
    "set_a2 (a#l) = (insert a (set_a2 l))"

  ― ‹Correctness of aa›
  lemma set_a2_correct: "set_a2 l = set l"
    by (induct l) auto

  ― ‹Generic algorithm›
  setup Locale_Code.open_block
  fun (in StdSetDefs) set_i2 where
    "set_i2 [] = empty ()" |
    "set_i2 (a#l) = (ins a (set_i2 l))"
  setup Locale_Code.close_block

  ― ‹Correct implementation of ca›
  lemma (in StdSet) set_i2_impl: "invar s ⟹ invar (set_i2 l) ∧ α (set_i2 l) = set_a2 l"
    by (induct l) (auto simp add: correct)

  ― ‹Instantiation›
  definition "hs_seti2 == hs.set_i2"
  (*declare hsr.set_i2.simps[folded hs_seti2_def, code]*)

  lemmas hs_set_i2_impl = hs.set_i2_impl[folded hs_seti2_def]

  ― ‹Code generation›
  ML ‹@{code hs_seti2}› 
  (*value "hs_seti [1,2,3::nat] hs_empty"*)

subsubsection "With explicit operation parameters"

  ― ‹Alternative for few operation parameters›
  fun set_i' where
    "!!ins. set_i' ins [] s = s" |
    "!!ins. set_i' ins (a#l) s = set_i' ins l (ins a s)"

  lemma (in StdSet) set_i'_impl:
    "invar s ⟹ invar (set_i' ins l s) ∧ α (set_i' ins l s) = set_a l (α s)"
    by (induct l arbitrary: s) (auto simp add: correct)

  ― ‹Instantiation›
  definition "hs_seti' == set_i' hs.ins"
  lemmas hs_set_i'_impl = hs.set_i'_impl[folded hs_seti'_def]

  ― ‹Code generation›
  ML ‹@{code hs_seti'}› 
  (*value "hs_seti' [1,2,3::nat] hs_empty"*)


subsection "Filter Average"
text ‹
  In this more complex example, we develop a function that filters from a set all
  numbers that are above the average of the set.
 
  First, we formulate this as a generic algorithm using a locale.
  This solution shows how the ICF v2 overcomes some technical problems that
  ICF v1 had: 
  \begin{itemize}
    \item Iterators are now polymorphic in the type, even inside locales.
      Hence, there is no special handling of iterators, as it was required
      in ICF v1.
    \item The Locale-Code package handles code generation for the instantiated
      locale. There is no need for lengthy boilerplate code as it was required
      in ICF v1.
  \end{itemize}


  Another possibility is to fix the used 
  implementations beforehand. Changing the implementation is still easy by
  changing the used operations. In this example, all used operations are 
  introduced by abbbreviations, localizing the required changes to a small part
  of the theory. This approach is more powerful, as operations are now 
  polymorphic also in the element type. However, it only allows as single 
  instantiation at a time, which is no option for generic algorithms.
›

  abbreviation "average S == ∑S div card S"

subsubsection "Generic Algorithm"
  locale MyContext =
    StdSet ops for ops :: "(nat,'s,'more) set_ops_scheme"
  begin
    definition avg_aux :: "'s ⇒ nat×nat" 
      where
      "avg_aux s == iterate s (λx (c,s). (c+1, s+x)) (0,0)"

    definition "avg s == case avg_aux s of (c,s) ⇒ s div c"

    definition "filter_le_avg s == let a=avg s in
      iterate s (λx s. if x≤a then ins x s else s) (empty ())"

    lemma avg_aux_correct: "invar s ⟹ avg_aux s = (card (α s), ∑(α s) )"
      apply (unfold avg_aux_def)
      apply (rule_tac 
        I="λit (c,sum). c=card (α s - it) ∧ sum=∑(α s - it)" 
        in iterate_rule_P)
      apply auto
      apply (subgoal_tac "α s - (it - {x}) = insert x (α s - it)")
      apply auto
      apply (subgoal_tac "α s - (it - {x}) = insert x (α s - it)")
      apply auto
      done

    lemma avg_correct: "invar s ⟹ avg s = average (α s)"
      unfolding avg_def
      using avg_aux_correct
      by auto

    lemma filter_le_avg_correct: 
      "invar s ⟹ 
        invar (filter_le_avg s) ∧ 
        α (filter_le_avg s) = {x∈α s. x≤average (α s)}"
      unfolding filter_le_avg_def Let_def
      apply (rule_tac
        I="λit r. invar r ∧ α r = {x∈α s - it. x≤average (α s)}"
        in iterate_rule_P)
      apply (auto simp add: correct avg_correct)
      done
  end

  setup Locale_Code.open_block
  interpretation hs_ctx: MyContext hs_ops by unfold_locales
  interpretation rs_ctx: MyContext rs_ops by unfold_locales
  setup Locale_Code.close_block

  definition "hs_flt_avg_test ≡ hs.to_list 
    o hs_ctx.filter_le_avg 
    o hs.from_list"
  definition "rs_flt_avg_test ≡ rs.to_list 
    o rs_ctx.filter_le_avg 
    o rs.from_list"

  
  text "Code generation"
  ML_val ‹
    if @{code hs_flt_avg_test} (map @{code nat_of_integer} [1,2,3,4,6,7])
    <> @{code rs_flt_avg_test} (map @{code nat_of_integer} [1,2,3,4,6,7])
    then error "Oops"
    else ()
› 
  

subsubsection "Using abbreviations"

  type_synonym 'a my_set = "'a hs"
  abbreviation "my_α == hs.α"
  abbreviation "my_invar == hs.invar"
  abbreviation "my_empty == hs.empty"
  abbreviation "my_ins == hs.ins"
  abbreviation "my_iterate == hs.iteratei"
  lemmas my_correct = hs.correct
  lemmas my_iterate_rule_P = hs.iterate_rule_P

  definition avg_aux :: "nat my_set ⇒ nat×nat" 
    where
    "avg_aux s == my_iterate s (λ_. True) (λx (c,s). (c+1, s+x)) (0,0)"

  definition "avg s == case avg_aux s of (c,s) ⇒ s div c"

  definition "filter_le_avg s == let a=avg s in
    my_iterate s (λ_. True) (λx s. if x≤a then my_ins x s else s) (my_empty ())"

  lemma avg_aux_correct: "my_invar s ⟹ avg_aux s = (card (my_α s), ∑(my_α s) )"
    apply (unfold avg_aux_def)
    apply (rule_tac 
      I="λit (c,sum). c=card (my_α s - it) ∧ sum=∑(my_α s - it)" 
      in my_iterate_rule_P)
    apply auto
    apply (subgoal_tac "my_α s - (it - {x}) = insert x (my_α s - it)")
    apply auto
    apply (subgoal_tac "my_α s - (it - {x}) = insert x (my_α s - it)")
    apply auto
    done

  lemma avg_correct: "my_invar s ⟹ avg s = average (my_α s)"
    unfolding avg_def
    using avg_aux_correct
    by auto

  lemma filter_le_avg_correct: 
    "my_invar s ⟹ 
    my_invar (filter_le_avg s) ∧ 
    my_α (filter_le_avg s) = {x∈my_α s. x≤average (my_α s)}"
    unfolding filter_le_avg_def Let_def
    apply (rule_tac
      I="λit r. my_invar r ∧ my_α r = {x∈my_α s - it. x≤average (my_α s)}"
      in my_iterate_rule_P)
    apply (auto simp add: my_correct avg_correct)
    done


  definition "test_set == my_ins (1::nat) (my_ins 2 (my_ins 3 (my_empty ())))"

  export_code avg_aux avg filter_le_avg test_set in SML module_name Test

end