# Theory AbsCFComp

Up to index of Isabelle/HOL/HOLCF/Shivers-CFA

theory AbsCFComp
imports AbsCF Computability FixTransform CPSUtils MapSets
`header {* The abstract semantics is computable *}theory AbsCFCompimports AbsCF Computability FixTransform CPSUtils MapSetsbegindefault_sort typetext {*The point of the abstract semantics is that it is computable. To show this, we exploit the special structure of @{text \<aF>} and @{text \<aC>}: 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 @{text \<afstate>} and @{text \<acstate>}, i.e.\ we treat the two mutually recursive functions now as one.@{text abs_g} gives the local result for the given argument.*}fixrec abs_g :: "('c::contour \<afstate> + 'c \<acstate>) discr -> 'c \<aans>"  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' = \<anb> b c;                         β  = [c \<mapsto> b]                     in {((c, β), cont) | cont . cont ∈ cnts}            | (Inl (PP (prim.If ct cf),[_, cntts, cntfs],ve,b)) =>                  ((   let b' = \<anb> b ct;                            β = [ct \<mapsto> b]                        in {((ct, β), cnt) | cnt . cnt ∈ cntts}                   )∪(                       let b' = \<anb> b cf;                            β = [cf \<mapsto> b]                        in {((cf, β), cnt) | cnt . cnt ∈ cntfs}                   ))            | (Inl (AStop,[_],_,_)) => {}            | (Inl _) => ⊥            | (Inr (App lab f vs,β,ve,b)) =>                 let fs = \<aA> f β ve;                     as = map (λv. \<aA> v β ve) vs;                     b' = \<anb> b lab                  in {((lab, β),f') | f' . f'∈ fs}            | (Inr (Let lab ls c',β,ve,b)) => {}        )"text {*@{text abs_R} gives the set of arguments passed to the recursive calls.*}fixrec abs_R :: "('c::contour \<afstate> + 'c \<acstate>) discr -> ('c::contour \<afstate> + 'c \<acstate>) 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 \<mapsto> b);                         ve' = ve ∪. (\<Union>. (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' = \<anb> b c;                         β  = [c \<mapsto> b]                     in (\<Union>cnt∈cnts. {Discr (Inl (cnt,[{}],ve,b'))})            | (Inl (PP (prim.If ct cf),[_, cntts, cntfs],ve,b)) =>                  ((   let b' = \<anb> b ct;                            β = [ct \<mapsto> b]                        in (\<Union>cnt∈cntts . {Discr (Inl (cnt,[],ve,b'))})                   )∪(                       let b' = \<anb> b cf;                            β = [cf \<mapsto> b]                        in (\<Union>cnt∈cntfs . {Discr (Inl (cnt,[],ve,b'))})                   ))            | (Inl (AStop,[_],_,_)) => {}            | (Inl _) => ⊥            | (Inr (App lab f vs,β,ve,b)) =>                 let fs = \<aA> f β ve;                     as = map (λv. \<aA> v β ve) vs;                     b' = \<anb> b lab                  in (\<Union>f' ∈ fs. {Discr (Inl (f',as,ve,b'))})            | (Inr (Let lab ls c',β,ve,b)) =>                 let b' = \<anb> b lab;                     β' = β (lab \<mapsto> b');                     ve' = ve ∪. (\<Union>. (map (λ(v,l). {(v,b') := (\<aA> (L l) β' ve)}.) ls))                 in {Discr (Inr (c',β',ve',b'))}        )"text {*The initial argument vector, as created by @{text \<aPR>}.*}definition initial_r :: "prog => ('c::contour \<afstate> + 'c \<acstate>) discr"  where "initial_r prog = Discr (Inl     (the_elem (\<aA> (L prog) empty {}.), [{AStop}], {}., \<abinit>))"subsection {* Towards finiteness *}text {*We need to show that the set of possible arguments for a given program @{text p} is finite. Therefore, we define the set of possible procedures, of possible arguments to @{text \<aF>}, or possible arguments to @{text \<aC>} 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 {*Using the auxiliary results from @{theory 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 {*But is it closed? I.e.\ if we pass a member of @{text arg_poss} to @{text abs_R}, are the generated recursive call arguments also in @{text arg_poss}? This is shown in @{text arg_space_complete}, after proving an auxiliary result about the possible outcome of a call to @{text \<aA>} and an admissibility lemma.*}lemma evalV_possible:  assumes f: "f ∈ \<aA> 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 nextcase (2 prim β' ve')  thus ?thesis using d f    by (auto dest: vals1 simp add:proc_poss_def)nextcase (3 l var β' ve')   thus ?thesis using f d smaps_over_im[OF _ ve]  by (auto split:option.split_asm dest: vals2)nextcase (4 l β ve)  thus ?thesis using f d β  by (auto dest!: vals3 simp add:proc_poss_def)qedlemma 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)nextcase Bot show ?case by simp nextcase (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 \<mapsto> 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 ∪. \<Union>.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 \<mapsto> 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, \<anb> b l) ∈ fstate_poss p"       unfolding fstate_poss_def by auto     thus "Discr (Inl (cnt, [{}], ve, \<anb> 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, \<anb> b l1) ∈ fstate_poss p"       unfolding fstate_poss_def by auto     thus "Discr (Inl (cnt, [], ve, \<anb> 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, \<anb> b l2) ∈ fstate_poss p"       unfolding fstate_poss_def by auto     thus "Discr (Inl (cnt, [], ve, \<anb> 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 ∈ \<aA> 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. \<aA> 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. \<aA> v β ve) ds, ve, \<anb> 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 \<mapsto> \<anb> b l) ∈ maps_over (labels p) UNIV" (is "?β' ∈ _")       by (auto intro: maps_over_upd[OF beta l])     moreover     have "ve ∪. \<Union>.map (λ(v, lam). { (v, \<anb> b l) := \<aA> (L lam) (β(l \<mapsto> \<anb> 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', \<anb> 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 qedqedqedqedtext {*This result is now lifted to the powerset of @{text abs_R}.*}lemma arg_space_complete_ps: "states ⊆ arg_poss p ==> (\<^ps>abs_R)·states ⊆ arg_poss p"using arg_space_complete unfolding powerset_lift_def by autotext {*We 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 "(\<Union>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 autoqedlemma args_finite: "finite (\<Union>i. iterate i·(\<^ps>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)qedsubsection {* A decomposition *}text {*The functions @{text abs_g} and @{text abs_R} are derived from @{text \<aF>} and @{text \<aC>}. This connection has yet to expressed explicitly. *}lemma Un_commute_helper:"(a ∪ b) ∪ (c ∪ d) = (a ∪ c) ∪ (b ∪ d)"by autolemma a_evalF_decomp:  "\<aF> = fst (sum_to_tup·(fix·(Λ f x. (\<Union>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, 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)donesubsection {* The iterative equation *}text {*Because of the special form of @{text \<aF>} (and thus @{text \<aPR>}) derived in the previous lemma, we can apply our generic results from @{theory Computability} and express the abstract semantics as the image of a finite set under a computable function.*}lemma a_evalF_iterative:  "\<aF>·(Discr x) = \<^ps>abs_g·(\<Union>i. iterate i·(\<^ps>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:"\<aPR> prog = \<^ps>abs_g·(\<Union>i. iterate i·(\<^ps>abs_R)·{initial_r prog})"unfolding evalCPS_a_def and initial_r_defby(subst a_evalF_iterative, simp del:abs_R.simps abs_g.simps evalV_a.simps)end`