Quelle  AbsCFComp.thy

section ‹The abstract semantics is computable›

theory AbsCFComp
imports AbsCF Computability FixTransform CPSUtils MapSets
begin

default_sort type

text ‹
  point of the abstract semantics is that it is computable. To show this, we exploit the special structure of ‹🚫› and ‹🚫›: Each call adds some elements to the result set and joins this with the results from a number of recursive calls. So we separate these two actions into separate functions. These take as arguments the direct sum of ‹🚫› and ‹🚫›, i.e.\ we treat the two mutually recursive functions now as one.

 ‹abs_g› gives the local result for the given argument.
 ›

fixrec abs_g :: "('c::contour 🚫 + 'c 🚫) discr → 'c 🚫"
  where "abs_g⋅x = (case undiscr x of
              (Inl (PC (Lambda lab vs c, β), as, ve, b)) ==> {}
            | (Inl (PP (Plus c),[_,_,cnts],ve,b)) ==>
                     let b' = 🚫 b c;
                         β = [c ↦ b]
                     in {((c, β), cont) | cont . cont ∈ cnts}
            | (Inl (PP (prim.If ct cf),[_, cntts, cntfs],ve,b)) ==>
                  (( let b' = 🚫 b ct;
                            β = [ct ↦ b]
                        in {((ct, β), cnt) | cnt . cnt ∈ cntts}
                   )∪(
                       let b' = 🚫 b cf;
                            β = [cf ↦ b]
                        in {((cf, β), cnt) | cnt . cnt ∈ cntfs}
                   ))
            | (Inl (AStop,[_],_,_)) ==> {}
            | (Inl _) ==> ⊥
            | (Inr (App lab f vs,β,ve,b)) ==>
                 let fs = 🚫 f β ve;
                     as = map (λv. 🚫 v β ve) vs;
                     b' = 🚫 b lab
                  in {((lab, β),f') | f' . f'∈ fs}
            | (Inr (Let lab ls c',β,ve,b)) ==> {}
        )"

text ‹
 ‹abs_R› gives the set of arguments passed to the recursive calls.
 ›

fixrec abs_R :: "('c::contour 🚫 + 'c 🚫) discr → ('c::contour 🚫 + 'c 🚫) discr set"
  where "abs_R⋅x = (case undiscr x of
              (Inl (PC (Lambda lab vs c, β), as, ve, b)) ==>
               (if length vs = length as
                then let β' = β (lab ↦ b);
                         ve' = ve ∪. (∪. (map (λ(v,a). {(v,b) := a}.) (zip vs as)))
                     in {Discr (Inr (c,β',ve',b))}
                else ⊥)
            | (Inl (PP (Plus c),[_,_,cnts],ve,b)) ==>
                     let b' = 🚫 b c;
                         β = [c ↦ b]
                     in (∪cnt∈cnts. {Discr (Inl (cnt,[{}],ve,b'))})
            | (Inl (PP (prim.If ct cf),[_, cntts, cntfs],ve,b)) ==>
                  (( let b' = 🚫 b ct;
                            β = [ct ↦ b]
                        in (∪cnt∈cntts . {Discr (Inl (cnt,[],ve,b'))})
                   )∪(
                       let b' = 🚫 b cf;
                            β = [cf ↦ b]
                        in (∪cnt∈cntfs . {Discr (Inl (cnt,[],ve,b'))})
                   ))
            | (Inl (AStop,[_],_,_)) ==> {}
            | (Inl _) ==> ⊥
            | (Inr (App lab f vs,β,ve,b)) ==>
                 let fs = 🚫 f β ve;
                     as = map (λv. 🚫 v β ve) vs;
                     b' = 🚫 b lab
                  in (∪f' ∈ fs. {Discr (Inl (f',as,ve,b'))})
            | (Inr (Let lab ls c',β,ve,b)) ==>
                 let b' = 🚫 b lab;
                     β' = β (lab ↦ b');
                     ve' = ve ∪. (∪. (map (λ(v,l). {(v,b') := (🚫 (L l) β' ve)}.) ls))
                 in {Discr (Inr (c',β',ve',b'))}
        )"

text ‹
  initial argument vector, as created by ‹🚫›.
 ›

definition initial_r :: "prog ==> ('c::contour 🚫 + 'c 🚫) discr"
  where "initial_r prog = Discr (Inl
     (the_elem (🚫 (L prog) Map.empty {}.), [{AStop}], {}., 🚫))"

subsection ‹Towards finiteness›

text ‹
  need to show that the set of possible arguments for a given program ‹p› is finite. Therefore, we define the set of possible procedures, of possible arguments to ‹🚫›, or possible arguments to ‹🚫› and of possible arguments.
 ›

definition proc_poss :: "prog ==> 'c::contour proc set"
  where "proc_poss p = PC ` (lambdas p × maps_over (labels p) UNIV) ∪ PP ` prims p ∪ {AStop}"

definition fstate_poss :: "prog ==> 'c::contour a_fstate set"
  where "fstate_poss p = (proc_poss p × NList (Pow (proc_poss p)) (call_list_lengths p) × smaps_over (vars p × UNIV) (proc_poss p) × UNIV)"

definition cstate_poss :: "prog ==> 'c::contour a_cstate set"
  where "cstate_poss p = (calls p × maps_over (labels p) UNIV × smaps_over (vars p × UNIV) (proc_poss p) × UNIV)"

definition arg_poss :: "prog ==> ('c::contour a_fstate + 'c a_cstate) discr set"
  where "arg_poss p = Discr ` (fstate_poss p <+> cstate_poss p)"

text ‹
  the auxiliary results from @{theory "Shivers-CFA.CPSUtils"}, we see that the argument space as defined here is finite.
 ›

lemma finite_arg_space: "finite (arg_poss p)"
  unfolding arg_poss_def and cstate_poss_def and fstate_poss_def and proc_poss_def
  by (auto intro!: finite_cartesian_product finite_imageI maps_over_finite smaps_over_finite finite_UNIV finite_Nlist)


text ‹
  is it closed? I.e.\ if we pass a member of ‹arg_poss› to ‹abs_R›, are the generated recursive call arguments also in ‹arg_poss›? This is shown in ‹arg_space_complete›, after proving an auxiliary result about the possible outcome of a call to ‹🚫› and an admissibility lemma.
 ›

lemma evalV_possible:
  assumes f: "f ∈ 🚫 d β ve"
  and d: "d ∈ vals p"
  and ve: "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
  and β: "β ∈ maps_over (labels p) UNIV"
shows "f ∈ proc_poss p"
proof (cases "(d,β,ve)" rule: evalV_a.cases)
case (1 cl β' ve')
  thus ?thesis using f by auto next
case (2 prim β' ve')
  thus ?thesis using d f
    by (auto dest: vals1 simp add:proc_poss_def)
next
case (3 l var β' ve') 
  thus ?thesis using f d smaps_over_im[OF _ ve]
  by (auto split:option.split_asm dest: vals2)
next
case (4 l β ve)
  thus ?thesis using f d β
  by (auto dest!: vals3 simp add:proc_poss_def)
qed

lemma adm_subset: "cont (λx. f x) ==> adm (λx. f x ⊆ S)"
by (subst sqsubset_is_subset[THEN sym], intro adm_lemmas cont2cont)


lemma arg_space_complete:
  "state ∈ arg_poss p ==> abs_R⋅state ⊆ arg_poss p"
proof(induct rule: abs_R.induct[case_names Admissibility Bot Step])
case Admissibility show ?case
   by (intro adm_lemmas adm_subset cont2cont)
next
case Bot show ?case by simp next
case (Step abs_R) 
  note state = Step(2)
  show ?case
  proof (cases state)
  case (Discr state') show ?thesis
   proof (cases state')
     case (Inl fstate) show ?thesis
     using Inl Discr state
     proof (cases fstate rule: a_fstate_case, auto)
     txt ‹Case Lambda›
     fix l vs c β as ve b
     assume "Discr (Inl (PC (Lambda l vs c, β), as, ve, b)) ∈ arg_poss p"
       hence lam: "Lambda l vs c ∈ lambdas p"
       and  beta: "β ∈ maps_over (labels p) UNIV "
       and  ve: "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
       and  as: "as ∈ NList (Pow (proc_poss p)) (call_list_lengths p)"
       unfolding arg_poss_def fstate_poss_def proc_poss_def by auto

     from lam have "c ∈ calls p"
       by (rule lambdas1)

     moreover
     from lam have "l ∈ labels p"
       by (rule lambdas2)
     with beta have "β(l ↦ b) ∈ maps_over (labels p) UNIV"
       by (rule maps_over_upd, auto)

     moreover
     from lam have vs: "set vs ⊆ vars p" by (rule lambdas3)
     from as have "∀ x ∈ set as. x ∈ Pow (proc_poss p)"
        unfolding NList_def nList_def by auto
     with vs have "ve ∪. ∪.map (λ(v, y). { (v, b) := y}.) (zip vs as)
       ∈ smaps_over (vars p × UNIV) (proc_poss p)" (is "?ve' ∈ _")
       by (auto intro!: smaps_over_un[OF ve] smaps_over_Union smaps_over_singleton)
          (auto simp add:set_zip)

     ultimately
     have "(c, β(l ↦ b), ?ve', b) ∈ cstate_poss p" (is "?cstate ∈ _")
       unfolding cstate_poss_def by simp
     thus "Discr (Inr ?cstate) ∈ arg_poss p"
       unfolding arg_poss_def by auto
     next

     txt ‹Case Plus›
     fix ve b l v1 v2 cnts cnt
     assume "Discr (Inl (PP (prim.Plus l), [v1, v2, cnts], ve, b)) ∈ arg_poss p"
         and "cnt ∈ cnts"
     hence "cnt ∈ proc_poss p" 
         and "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
       unfolding arg_poss_def fstate_poss_def NList_def nList_def
       by auto
     moreover
     have "[{}] ∈ NList (Pow (proc_poss p)) (call_list_lengths p)"
       unfolding call_list_lengths_def NList_def nList_def by auto
     ultimately
     have "(cnt, [{}], ve, 🚫 b l) ∈ fstate_poss p"
       unfolding fstate_poss_def by auto
     thus "Discr (Inl (cnt, [{}], ve, 🚫 b l)) ∈ arg_poss p"
       unfolding arg_poss_def by auto
     next
  
     txt ‹Case If (true case)›
     fix ve b l1 l2 v cntst cntsf cnt
     assume "Discr (Inl (PP (prim.If l1 l2), [v, cntst, cntsf], ve, b)) ∈ arg_poss p"
         and "cnt ∈ cntst"
     hence "cnt ∈ proc_poss p"
         and "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
       unfolding arg_poss_def fstate_poss_def NList_def nList_def
       by auto
     moreover
     have "[] ∈ NList (Pow (proc_poss p)) (call_list_lengths p)"
       unfolding call_list_lengths_def NList_def nList_def by auto
     ultimately
     have "(cnt, [], ve, 🚫 b l1) ∈ fstate_poss p"
       unfolding fstate_poss_def by auto
     thus "Discr (Inl (cnt, [], ve, 🚫 b l1)) ∈ arg_poss p"
       unfolding arg_poss_def by auto
     next
  
     txt ‹Case If (false case)›
     fix ve b l1 l2 v cntst cntsf cnt
     assume "Discr (Inl (PP (prim.If l1 l2), [v, cntst, cntsf], ve, b)) ∈ arg_poss p"
         and "cnt ∈ cntsf"
     hence "cnt ∈ proc_poss p"
         and "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
       unfolding arg_poss_def fstate_poss_def NList_def nList_def
       by auto
     moreover
     have "[] ∈ NList (Pow (proc_poss p)) (call_list_lengths p)"
       unfolding call_list_lengths_def NList_def nList_def by auto
     ultimately
     have "(cnt, [], ve, 🚫 b l2) ∈ fstate_poss p"
       unfolding fstate_poss_def by auto
     thus "Discr (Inl (cnt, [], ve, 🚫 b l2)) ∈ arg_poss p"
       unfolding arg_poss_def by auto
    qed
  next
  case (Inr cstate)
  show ?thesis proof(cases cstate rule: prod_cases4)
   case (fields c β ve b)
   show ?thesis using Discr Inr fields state proof(cases c, auto simp add:HOL.Let_def simp del:evalV_a.simps)

     txt ‹Case App›
     fix l d ds f
     assume arg: "Discr (Inr (App l d ds, β, ve, b)) ∈ arg_poss p"
       and f: "f ∈ 🚫 d β ve"
     hence c: "App l d ds ∈ calls p"
       and d: "d ∈ vals p"
       and ds: "set ds ⊆ vals p"
       and beta: "β ∈ maps_over (labels p) UNIV"
       and ve: "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
     by (auto simp add: arg_poss_def cstate_poss_def call_list_lengths_def dest: app1 app2)

     have len: "length ds ∈ call_list_lengths p"
       by (auto intro: rev_image_eqI[OF c] simp add: call_list_lengths_def)

     have "f ∈ proc_poss p"
       using f d ve beta by (rule evalV_possible)
     moreover
     have "map (λv. 🚫 v β ve) ds ∈ NList (Pow (proc_poss p)) (call_list_lengths p)"
       using ds len
       unfolding NList_def by (auto simp add:nList_def intro!: evalV_possible[OF _ _ ve beta])
     ultimately 
     have "(f, map (λv. 🚫 v β ve) ds, ve, 🚫 b l) ∈ fstate_poss p" (is "?fstate ∈ _")
       using ve 
       unfolding fstate_poss_def by simp
     thus "Discr (Inl ?fstate) ∈ arg_poss p"
       unfolding arg_poss_def by auto

   next
     txt ‹Case Let›
     fix l binds c'
     assume arg: "Discr (Inr (Let l binds c', β, ve, b)) ∈ arg_poss p"
     hence l: "l ∈ labels p"
       and c': "c' ∈ calls p"
       and vars: "fst ` set binds ⊆ vars p"
       and ls: "snd ` set binds ⊆ lambdas p"
       and beta: "β ∈ maps_over (labels p) UNIV"
       and ve: "ve ∈ smaps_over (vars p × UNIV) (proc_poss p)"
     by (auto simp add: arg_poss_def cstate_poss_def call_list_lengths_def
              dest:let1 let2 let3 let4)

     have beta': "β(l ↦ 🚫 b l) ∈ maps_over (labels p) UNIV" (is "?β' ∈ _")
       by (auto intro: maps_over_upd[OF beta l])

     moreover
     have "ve ∪. ∪.map (λ(v, lam). { (v, 🚫 b l) := 🚫 (L lam) (β(l ↦ 🚫 b l)) ve }.)
                binds
       ∈ smaps_over (vars p × UNIV) (proc_poss p)" (is "?ve' ∈ _")
       using vars ls beta'
       by (auto intro!: smaps_over_un[OF ve] smaps_over_Union)
          (auto intro!:smaps_over_singleton simp add: proc_poss_def)

     ultimately
     have "(c', ?β', ?ve', 🚫 b l) ∈ cstate_poss p" (is "?cstate ∈ _")
     using c' unfolding cstate_poss_def by simp
     thus "Discr (Inr ?cstate) ∈ arg_poss p"
       unfolding arg_poss_def by auto
   qed
 qed
qed
qed
qed

text ‹
  result is now lifted to the powerset of ‹abs_R›.
 ›

lemma arg_space_complete_ps: "states ⊆ arg_poss p ==> (🚫abs_R)⋅states ⊆ arg_poss p"
using arg_space_complete unfolding powerset_lift_def by auto

text ‹
  are not so much interested in the finiteness of the set of possible arguments but rather of the the set of occurring arguments, when we start with the initial argument. But as this is of course a subset of the set of possible arguments, this is not hard to show.
 ›

lemma UN_iterate_less: 
  assumes start: "x ∈ S"
  and step: "∧y. y⊆S ==> (f⋅y) ⊆ S"
  shows "(∪i. iterate i⋅f⋅{x}) ⊆ S"
proof- {
  fix i
  have "iterate i⋅f⋅{x} ⊆ S"
  proof(induct i)
    case 0 show ?case using ‹x ∈ S› by simp next
    case (Suc i) thus ?case using step[of "iterate i⋅f⋅{x}"] by simp
  qed
  } thus ?thesis by auto
qed

lemma args_finite: "finite (∪i. iterate i⋅(🚫abs_R)⋅{initial_r p})" (is "finite ?S")
proof (rule finite_subset[OF _finite_arg_space])
  have [simp]:"p ∈ lambdas p" by (cases p, simp)
  show "?S ⊆ arg_poss p"
  unfolding initial_r_def
  by  (rule UN_iterate_less[OF _ arg_space_complete_ps])
      (auto simp add:arg_poss_def fstate_poss_def proc_poss_def call_list_lengths_def NList_def nList_def
         intro!: imageI)
qed

subsection ‹A decomposition›

text ‹
  functions ‹abs_g› and ‹abs_R› are derived from ‹🚫› and ‹🚫›. This connection has yet to expressed explicitly.
 ›

lemma Un_commute_helper:"(a ∪ b) ∪ (c ∪ d) = (a ∪ c) ∪ (b ∪ d)"
by auto

lemma a_evalF_decomp:
  "🚫 = fst (sum_to_tup⋅(fix⋅(Λ f x. (∪y∈abs_R⋅x. f⋅y) ∪ abs_g⋅x)))"
apply (subst a_evalF_def)
apply (subst fix_transform_pair_sum)
apply (rule arg_cong [of _ _ "λx. fst (sum_to_tup⋅(fix⋅x))"])
apply (simp)
apply (simp only: discr_app undiscr_Discr)
apply (rule cfun_eqI, rule cfun_eqI, simp)
apply (case_tac xa, rename_tac a, case_tac a, simp)
apply (case_tac aa rule:a_fstate_case, simp_all add: Un_commute_helper)
apply (case_tac b rule:prod_cases4)
apply (case_tac aa)
apply (simp_all add:HOL.Let_def)
done

subsection ‹The iterative equation›

text ‹
  of the special form of ‹🚫› (and thus ‹🚫›) derived in the previous lemma, we can apply our generic results from @{theory "Shivers-CFA.Computability"} and express the abstract semantics as the image of a finite set under a computable function.
 ›

lemma a_evalF_iterative:
  "🚫⋅(Discr x) = 🚫abs_g⋅(∪i. iterate i⋅(🚫abs_R)⋅{Discr (Inl x)})"
by (simp del:abs_R.simps abs_g.simps add: theorem12 Un_commute a_evalF_decomp)

lemma a_evalCPS_interative:
"🚫 prog = 🚫abs_g⋅(∪i. iterate i⋅(🚫abs_R)⋅{initial_r prog})"
unfolding evalCPS_a_def and initial_r_def
by(subst a_evalF_iterative, simp del:abs_R.simps abs_g.simps evalV_a.simps)

end