Theory Option_Monad_Add

theory Option_Monad_Add
imports "HOL-Library.Monad_Syntax"
begin
  definition "oassert Φ ≡ if Φ then Some () else None"

  fun omap :: "('a⇀'b) ⇒ 'a list ⇀ 'b list" where
    "omap f [] = Some []" 
  | "omap f (x#xs) = do { y ← f x; ys ← omap f xs; Some (y#ys) }"  
    
  lemma omap_cong[fundef_cong]:
    assumes "⋀x. x∈set l' ⟹ f x = f' x"
    assumes "l=l'"
    shows "omap f l = omap f' l'"
    unfolding assms(2) using assms(1) by (induction l') (auto)

  lemma assert_eq_iff[simp]: 
    "oassert Φ = None ⟷ ¬Φ"  
    "oassert Φ = Some u ⟷ Φ"  
    unfolding oassert_def by auto

  lemma omap_length[simp]: "omap f l = Some l' ⟹ length l' = length l" 
    apply (induction l arbitrary: l') 
    apply (auto split: Option.bind_splits)
    done 

  lemma omap_append[simp]: "omap f (xs@ys) = do {xs ← omap f xs; ys ← omap f ys; Some (xs@ys)}"
    by (induction xs) (auto)
    
        
  lemma omap_alt: "omap f l = Some l' ⟷ (l' = map (the o f) l ∧ (∀x∈set l. f x ≠ None))"  
    apply (induction l arbitrary: l')
    apply (auto split: Option.bind_splits)
    done
    
  lemma omap_alt_None: "omap f l = None ⟷ (∃x∈set l. f x = None)"
    apply (induction l)
    apply (auto split: Option.bind_splits)
    done
    
  lemma omap_nth: "⟦omap f l = Some l'; i<length l⟧ ⟹ f (l!i) = Some (l'!i)"
    apply (induction l arbitrary: l' i)
    apply (auto split: Option.bind_splits simp: nth_Cons split: nat.splits)
    done

  lemma omap_eq_Nil_conv[simp]: "omap f xs = Some [] ⟷ xs=[]"
    apply (cases xs) 
    apply (auto split: Option.bind_splits)
    done

  lemma omap_eq_Cons_conv[simp]: "omap f xs = Some (y#ys') ⟷ (∃x xs'. xs=x#xs' ∧ f x = Some y ∧ omap f xs' = Some ys')"  
    apply (cases xs) 
    apply (auto split: Option.bind_splits)
    done
        
  lemma omap_eq_append_conv[simp]: "omap f xs = Some (ys⇩1@ys⇩2) ⟷ (∃xs⇩1 xs⇩2. xs=xs⇩1@xs⇩2 ∧ omap f xs⇩1 = Some ys⇩1 ∧ omap f xs⇩2 = Some ys⇩2)"
    apply (induction ys⇩1 arbitrary: xs)
    apply (auto 0 3 split: Option.bind_splits)
    apply (metis append_Cons)
    done
  
  lemma omap_list_all2_conv: "omap f xs = Some ys ⟷ (list_all2 (λx y. f x = Some y)) xs ys"  
    apply (induction xs arbitrary: ys)
    apply (auto split: Option.bind_splits simp: )
    apply (simp add: list_all2_Cons1)
    apply (simp add: list_all2_Cons1)
    apply (simp add: list_all2_Cons1)
    apply clarsimp
    by (metis option.inject)
    
    
    
    
  fun omap_option where
    "omap_option f None = Some None"    
  | "omap_option f (Some x) = do { x ← f x; Some (Some x) }"
  
  lemma omap_option_conv:
    "omap_option f xx = None ⟷ (∃x. xx=Some x ∧ f x = None)" 
    "omap_option f xx = (Some (Some x')) ⟷ (∃x. xx=Some x ∧ f x = Some x')"
    "omap_option f xx = (Some None) ⟷ xx=None"
    by (cases xx;auto split: Option.bind_splits)+
  
  lemma omap_option_eq: "omap_option f x = (case x of None ⇒ Some None | Some x ⇒ do { x ← f x; Some (Some x) })"  
    by (auto split: option.split)
      
  fun omap_prod where
    "omap_prod f⇩1 f⇩2 (a,b) = do { a←f⇩1 a; b←f⇩2 b; Some (a,b) }"
    
      
  (* Extend map function for datatype to option monad.
    TODO: Show reasonable lemmas, like parametricity, etc. 
    Hopefully only depending on BNF-property of datatype
   *)
  definition "omap_dt setf mapf f obj ≡ do {
    oassert (∀x∈setf obj. f x ≠ None);
    Some (mapf (the o f) obj)
  }"
    
    
    
end