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. xset 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  (xset l. f x  None))"  
    apply (induction l arbitrary: l')
    apply (auto split: Option.bind_splits)
    done
    
  lemma omap_alt_None: "omap f l = None  (xset 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 (ys1@ys2)  (xs1 xs2. xs=xs1@xs2  omap f xs1 = Some ys1  omap f xs2 = Some ys2)"
    apply (induction ys1 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 f1 f2 (a,b) = do { af1 a; bf2 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 (xsetf obj. f x  None);
    Some (mapf (the o f) obj)
  }"
    
    
    
end