Theory Snippets

chapter ‹Code Snippets›
theory Snippets
imports "lib/VTcomp"
begin

  section ‹Find Element in Array (Arrays)›

  definition "find_elem (x::int) xs ≡ doN {
    WHILEIT (λi. i≤length xs ∧ x∉set (take i xs)) (λi. i<length xs ∧ xs!i≠x) (λi. RETURN (i+1)) 0
  }"
  
  lemma find_elem_correct: "find_elem x xs ≤ SPEC (λi. i≤length xs ∧ (i<length xs ⟶ xs!i = x))"
    unfolding find_elem_def
    apply refine_vcg
    apply (rule wf_measure[of "λi. length xs - i"])
    apply (auto simp: in_set_conv_nth)
    (*sledgehammer*)
    using less_Suc_eq by blast
    
  sepref_definition find_elem_impl is "uncurry find_elem" :: "int_assn⇧k *⇩a (array_assn int_assn)⇧k →⇩a nat_assn"
    unfolding find_elem_def short_circuit_conv
    by sepref
  
  export_code find_elem_impl in Haskell module_name test

  
  subsection ‹Combined Correctness Theorem›  
  lemma find_elem_r1: "(find_elem, λ x xs. SPEC (λi. i≤length xs ∧ (i<length xs ⟶ xs!i = x))) ∈ Id → Id → ⟨Id⟩nres_rel"
    using find_elem_correct by (auto intro: nres_relI)
  
  thm find_elem_impl.refine[FCOMP find_elem_r1]
  

  section ‹Check Prefix (Arrays, Exceptions: Check)›
    
  definition "check_prefix xs ys ≡ doE {
    CHECK (length xs ≤ length ys) ();
    EWHILEIT (λi. i≤length xs ∧ take i xs = take i ys) (λi. i<length xs) (λi. doE { 
      EASSERT (i<length xs ∧ i<length ys); 
      CHECK (xs!i = ys!i) (); 
      ERETURN (i+1) 
    } ) 0;
    ERETURN ()
  }"
  
  (* ESPEC Exc Normal ! *)
  lemma check_prefix_correct: "check_prefix xs ys ≤ ESPEC (λ_. xs ≠ take (length xs) ys) (λ_. xs = take (length xs) ys)"
    unfolding check_prefix_def
    apply (refine_vcg EWHILEIT_rule[where R="measure (λi. length xs - i)"])
    apply auto []
    apply auto []
    apply auto []
    apply auto []
    apply auto []
    apply auto []
    subgoal
      by (simp add: take_Suc_conv_app_nth)
    apply auto []
    apply auto []
    subgoal 
      by (metis nth_take)
    subgoal 
      by force
    apply auto []
    done
  
  synth_definition check_prefix_bd is [enres_unfolds]: "check_prefix xs ys = ⌑"
    apply (rule CNV_eqD)
    unfolding check_prefix_def
    apply opt_enres_unfold
    apply (rule CNV_I)
    done
    
  sepref_definition check_prefix_impl is "uncurry check_prefix_bd" 
    :: "(array_assn int_assn)⇧k *⇩a (array_assn int_assn)⇧k →⇩a (unit_assn +⇩a unit_assn)"
    unfolding check_prefix_bd_def
    by sepref
  
  export_code check_prefix_impl checking SML_imp

  subsection ‹Modularity›
    
  lemmas [refine_vcg] = check_prefix_correct[THEN ESPEC_trans]
  thm SPEC_trans (* for plain nres-monad without exceptions *)
    
  (* TODO: I remember to have automated the order_trans transformation, but cannot find it right now. *)
  

  definition "is_prefix' xs ys ≡ CATCH (doE {check_prefix xs ys; ERETURN True }) (λ_. ERETURN False)"  
  
  lemma is_prefix'_correct: "is_prefix' xs ys ≤ ESPEC (λ_. False) (λr. r ⟷ xs = take (length xs) ys)"
    unfolding is_prefix'_def
    apply refine_vcg
    by auto
  
  lemmas [sepref_fr_rules] = check_prefix_impl.refine  
  sepref_register check_prefix_bd :: "'a list ⇒ 'a list ⇒ (unit+unit) nres"
    (* Optional interface type. Required if interfaces used that do not match Isabelle types, e.g. i_map, i_mtx, …*)

  synth_definition is_prefix_bd' is [enres_unfolds]: "is_prefix' xs ys = ⌑"
    apply (rule CNV_eqD)
    unfolding is_prefix'_def
    apply opt_enres_unfold
    apply (rule CNV_I)
    done
    
  sepref_definition is_prefix_impl' is "uncurry is_prefix_bd'" 
    :: "(array_assn int_assn)⇧k *⇩a (array_assn int_assn)⇧k →⇩a (unit_assn +⇩a bool_assn)"
    unfolding is_prefix_bd'_def
    by sepref
  
  export_code is_prefix_impl' checking SML_imp
  
  
      

  section ‹Is Prefix (Arrays, Exceptions: Catch)›
  
  definition "is_prefix xs ys ≡ CATCH (doE {
    CHECK (length xs ≤ length ys) False;
    EWHILEIT (λi. i≤length xs ∧ take i xs = take i ys) (λi. i<length xs) (λi. doE { 
      EASSERT (i<length xs ∧ i<length ys); 
      CHECK (xs!i = ys!i) False;
      ERETURN (i+1) 
    } ) 0;
    THROW True
  }) (ERETURN)"
  
  (* ESPEC Exc Normal ! *)
  lemma "is_prefix xs ys ≤ ESPEC (λ_. False) (λr. r ⟷ xs = take (length xs) ys)"
    unfolding is_prefix_def
    apply (refine_vcg EWHILEIT_rule[where R="measure (λi. length xs - i)"])
    apply auto []
    apply auto []
    apply auto []
    apply auto []
    apply auto []
    apply auto []
    subgoal
      by (simp add: take_Suc_conv_app_nth)
    apply auto []
    apply auto []
    subgoal 
      by (metis nth_take)
    subgoal 
      by force
    apply auto []
    done
  
  synth_definition is_prefix_bd is [enres_unfolds]: "is_prefix xs ys = ⌑"
    apply (rule CNV_eqD)
    unfolding is_prefix_def
    apply opt_enres_unfold
    apply (rule CNV_I)
    done
    
  sepref_definition is_prefix_impl is "uncurry is_prefix_bd" 
    :: "(array_assn int_assn)⇧k *⇩a (array_assn int_assn)⇧k →⇩a (unit_assn +⇩a bool_assn)"
    unfolding is_prefix_bd_def
    by sepref
  
  export_code is_prefix_impl checking SML_imp
  
  
  
  
  
  
  
  
  
  section ‹Copy Array (Arrays, For i=l..u)›  
  
  definition "cp_array xs ≡ doN {
    let ys = op_array_replicate (length xs) 0;   ― ‹Use proper constructors›
    
    ys ← nfoldli [0..<length xs] (λ_. True) (λi ys. doN {  ― ‹Ensure linearity! ‹ys←…››
      ASSERT (i<length xs ∧ i<length ys); 
      RETURN (ys[i:=xs!i]) 
    }) ys;
    
    RETURN ys
  }"

  
  lemma "cp_array xs ≤ SPEC (λys. ys=xs)"
    unfolding cp_array_def
    supply nfoldli_rule nfoldli_rule[where I="λl1 l2 ys. length ys = length xs ∧ (∀i∈set l1. ys!i = xs!i)", refine_vcg]
    apply refine_vcg
    apply auto
    subgoal 
      using upt_eq_lel_conv by blast
    subgoal
      using upt_eq_lel_conv by blast
    subgoal 
      by (simp add: nth_list_update)
    subgoal 
      by (simp add: nth_equalityI)
    done  
    

  term arl_assn  
    
  subsection ‹Proof with ‹nfoldli_upt_rule››  
  lemma "cp_array xs ≤ SPEC (λys. ys=xs)"
    unfolding cp_array_def
    supply nfoldli_upt_rule nfoldli_upt_rule[where I="λi ys. length ys = length xs ∧ (∀j<i. ys!j = xs!j)", refine_vcg]
    apply refine_vcg
    apply auto
    subgoal
      using less_Suc_eq by auto 
    subgoal
      by (simp add: nth_equalityI)
    done
      
  
    
  sepref_definition cp_array_impl is cp_array :: "(array_assn nat_assn)⇧k →⇩a array_assn nat_assn"
    unfolding cp_array_def
    by sepref
  
  
  
end