Theory Partial_Evaluation

section "Partial States"

subsection ‹Partial evaluation of expressions›    
theory Partial_Evaluation
imports AExp Vars
begin

                      
type_synonym partstate = "(vname ⇒ val option)"

definition emb :: "partstate ⇒ state ⇒ state" where
   "emb ps s = (%v. (case (ps v) of (Some r) ⇒ r | None ⇒ s v))"
    
definition part :: "state ⇒ partstate" where
   "part s = (%v. Some (s v))"
   
lemma emb_part[simp]: "emb (part s) q = s" unfolding emb_def part_def by auto
    
lemma part_emb[simp]: "dom ps = UNIV ⟹ part (emb ps q) = ps" unfolding emb_def part_def apply(rule ext)
  by (simp add: domD option.case_eq_if) 
      
   
lemma dom_part[simp]: "dom (part s) = UNIV" unfolding part_def by auto
    
abbreviation optplus :: "int option ⇒ int option ⇒ int option"   where "optplus a b ≡ (case a of None ⇒ None | Some a' ⇒ (case b of None ⇒ None | Some b' ⇒ Some (a' + b'))) "
abbreviation opttimes :: "int option ⇒ int option ⇒ int option"   where "opttimes a b ≡ (case a of None ⇒ None | Some a' ⇒ (case b of None ⇒ None | Some b' ⇒ Some (a' * b'))) "
abbreviation optdiv :: "int option ⇒ int option ⇒ int option"   where "optdiv a b ≡ (case a of None ⇒ None | Some a' ⇒ (case b of None ⇒ None | Some b' ⇒ Some (a' div b'))) "
                                            
fun paval' :: "aexp ⇒ partstate ⇒ val option" where
"paval' (N n) s = Some n" |
"paval' (V x) s = s x" |
"paval' (Plus a⇩1 a⇩2) s = optplus (paval' a⇩1 s)   (paval' a⇩2 s)" |
"paval' (Times a⇩1 a⇩2) s = opttimes (paval' a⇩1 s)   (paval' a⇩2 s)" |
"paval' (Div a⇩1 a⇩2) s = optdiv (paval' a⇩1 s)   (paval' a⇩2 s)"
  

lemma "paval' a ps = Some v ⟹ vars a ⊆ dom ps"
proof(induct a arbitrary: v) 
  case (Plus a1 a2)
  from Plus(3) obtain v1 where 1: "paval' a1 ps = Some v1" 
    by fastforce
  with Plus(3) obtain v2 where 2: "paval' a2 ps = Some v2"
    by fastforce
  from Plus(1)[OF 1] Plus(2)[OF 2] show ?case by auto 
next
  case (Times a1 a2)
  from Times(3) obtain v1 where 1: "paval' a1 ps = Some v1" 
    by fastforce
  with Times(3) obtain v2 where 2: "paval' a2 ps = Some v2"
    by fastforce
  from Times(1)[OF 1] Times(2)[OF 2] show ?case by auto 
next
  case (Div a1 a2)
  from Div(3) obtain v1 where 1: "paval' a1 ps = Some v1" 
    by fastforce
  with Div(3) obtain v2 where 2: "paval' a2 ps = Some v2"
    by fastforce
  from Div(1)[OF 1] Div(2)[OF 2] show ?case by auto 
qed  (simp_all, blast)

lemma paval'_aval: "paval' a ps = Some v ⟹ aval a (emb ps s) = v"
proof(induct a arbitrary: v) 
  case (Plus a1 a2)
  from Plus(3) obtain v1 where 1: "paval' a1 ps = Some v1" 
    by fastforce
  with Plus(3) obtain v2 where 2: "paval' a2 ps = Some v2"
    by fastforce
  from Plus(1)[OF 1] Plus(2)[OF 2] Plus(3) 1 2 show ?case by auto
next
  case (Times a1 a2)
  from Times(3) obtain v1 where 1: "paval' a1 ps = Some v1" 
    by fastforce
  with Times(3) obtain v2 where 2: "paval' a2 ps = Some v2"
    by fastforce
  from Times(1)[OF 1] Times(2)[OF 2] Times(3) 1 2 show ?case by auto 
next  
  case (Div a1 a2)
  from Div(3) obtain v1 where 1: "paval' a1 ps = Some v1" 
    by fastforce
  with Div(3) obtain v2 where 2: "paval' a2 ps = Some v2"
    by fastforce
  from Div(1)[OF 1] Div(2)[OF 2] Div(3) 1 2 show ?case by auto 
qed (simp_all add: emb_def)
  
  
fun paval :: "aexp ⇒ partstate ⇒ val" where
"paval (N n) s = n" |
"paval (V x) s = the (s x)" |
"paval (Plus a⇩1 a⇩2) s = paval a⇩1 s + paval a⇩2 s" |
"paval (Times a⇩1 a⇩2) s = paval a⇩1 s * paval a⇩2 s" |
"paval (Div a⇩1 a⇩2) s = paval a⇩1 s div paval a⇩2 s"
  
lemma paval_aval: "vars a ⊆ dom ps ⟹ paval a ps = aval a (λv. case ps v of None ⇒ s v | Some r ⇒ r)"
  by (induct a, auto)

lemma paval'_paval: "vars a ⊆ dom ps ⟹ paval' a ps = Some (paval a ps)"
  by (induct a, auto)

lemma paval_paval': "paval' a ps = Some v ⟹ paval a ps = v"
proof(induct a arbitrary: v) 
  case (Plus a1 a2)
  from Plus(3) obtain v1 where 1: "paval' a1 ps = Some v1" 
    by fastforce
  with Plus(3) obtain v2 where 2: "paval' a2 ps = Some v2"
    by fastforce
  from Plus(1)[OF 1] Plus(2)[OF 2] Plus(3) 1 2 show ?case by auto 
next
  case (Times a1 a2)
  from Times(3) obtain v1 where 1: "paval' a1 ps = Some v1" 
    by fastforce
  with Times(3) obtain v2 where 2: "paval' a2 ps = Some v2"
    by fastforce
  from Times(1)[OF 1] Times(2)[OF 2] Times(3) 1 2 show ?case by auto 
next  
  case (Div a1 a2)
  from Div(3) obtain v1 where 1: "paval' a1 ps = Some v1" 
    by fastforce
  with Div(3) obtain v2 where 2: "paval' a2 ps = Some v2"
    by fastforce
  from Div(1)[OF 1] Div(2)[OF 2] Div(3) 1 2 show ?case by auto 
qed simp_all
      
  
fun pbval :: "bexp ⇒ partstate ⇒ bool" where
"pbval (Bc v) s = v" |
"pbval (Not b) s = (¬ pbval b s)" |
"pbval (And b⇩1 b⇩2) s = (pbval b⇩1 s ∧ pbval b⇩2 s)" |
"pbval (Less a⇩1 a⇩2) s = (paval a⇩1 s < paval a⇩2 s)"
  

abbreviation optnot  where "optnot a ≡ (case a of None ⇒ None | Some a' ⇒ Some (~a'))"
                                            
abbreviation optand  where "optand a b ≡ (case a of None ⇒ None | Some a' ⇒ (case b of None ⇒ None | Some b' ⇒ Some (a' ∧ b'))) "
abbreviation optless   where "optless a b ≡ (case a of None ⇒ None | Some a' ⇒ (case b of None ⇒ None | Some b' ⇒ Some (a' < b'))) "
                                            
fun pbval' :: "bexp ⇒ partstate ⇒ bool option" where
"pbval' (Bc v) s = Some v" |
"pbval' (Not b) s = (optnot (pbval' b s))" |
"pbval' (And b⇩1 b⇩2) s = (optand (pbval' b⇩1 s) (pbval' b⇩2 s))" |
"pbval' (Less a⇩1 a⇩2) s = (optless (paval' a⇩1 s) (paval' a⇩2 s))"
  

lemma pbval'_pbval: "vars a ⊆ dom ps ⟹ pbval' a ps = Some (pbval a ps)"
  apply(induct a) apply (auto simp: paval'_paval) done

lemma paval_aval_vars: "vars a ⊆ dom ps ⟹ paval a ps = aval a (emb ps s)"
  apply(induct a) by(auto simp: emb_def) 

lemma pbval_bval_vars: "vars b ⊆ dom ps ⟹ pbval b ps = bval b (emb ps s)"
  apply(induct b) apply (simp_all)
  using paval_aval_vars[where s=s] by auto
        
lemma paval'dom: "paval' a ps = Some v ⟹ vars a ⊆ dom ps"
proof (induct a arbitrary: v)
  case (Plus a1 a2)   
  then show ?case apply auto
    apply fastforce
    by (metis (no_types, lifting) domD option.case_eq_if option.collapse subset_iff) 
next  
  case (Times a1 a2)   
  then show ?case apply auto
    apply fastforce
    by (metis (no_types, lifting) domD option.case_eq_if option.collapse subset_iff) 
next
  case (Div a1 a2)     
  then show ?case apply auto
    apply fastforce
    by (metis (no_types, lifting) domD option.case_eq_if option.collapse subset_iff) 
qed auto

end