text:
theory SM_Ample_Impl
imports SM_Datastructures "../Analysis/SM_POR"
  "HOL-Library.RBT_Mapping"
begin

  text \<open>
    Given a sticky program, we implement
    a valid ample-function by picking the transitions from the first
    PID that qualifies as an ample-set\<close>
  context visible_prog
  begin
    definition ga_gample
      :: "(cmdc\<times>cmdc) set \<Rightarrow> pid_global_config \<Rightarrow> global_action set"
    where
      "ga_gample sticky_E gc \<equiv> let
        lcs = pid_global_config.processes gc;
        gs = pid_global_config.state gc;
        as = find_min_idx_f (\<lambda>lc.
          let
            c = local_config.command lc;
            ls = local_config.state lc;
            as = set (comp.succ_impl c)
          in
            if (\<forall>(a,_)\<in>as. read_globals a = {} \<and> write_globals a = {}) then
              let
                as = {(a,c')\<in>as. la_en' (ls,gs) a}
              in
                if as={} \<or> (\<exists>(a,c')\<in>as. (c,c')\<in>sticky_E) then
                  None
                else
                  Some (c,as)
            else
              None
        ) lcs
      in
        case as of
          Some (pid,c,as) \<Rightarrow> (\<lambda>(a,c'). (pid,c,a,c'))`as
        | None \<Rightarrow> ga_gen gc"

    definition "ga_ample sticky_E
      \<equiv> stutter_extend_en (ga_gample sticky_E)"

    lemma ga_gample_subset: "ga_gample sticky_E gc \<subseteq> ga_gen gc"
      unfolding ga_gample_def ga_gen_def
      by (auto
        simp: comp.astep_impl_def
        split: option.splits if_split_asm
        dest!: find_min_idx_f_SomeD)

    lemma ga_gample_empty_iff: "ga_gample sticky_E gc = {} \<longleftrightarrow> ga_gen gc = {}"
      unfolding ga_gample_def ga_gen_def
      by (fastforce
        simp: comp.astep_impl_def
        split: option.splits if_split_asm
        dest!: find_min_idx_f_SomeD)

    lemma ga_ample_None_iff: "None \<in> ga_ample sticky_E gc \<longleftrightarrow> None \<in> ga_en gc"
      by (auto
        simp: ga_ample_def ga_en_def stutter_extend_en_def ga_gample_empty_iff)

    lemma ga_ample_neq_en_eq:
      assumes "ga_ample sticky_E gc \<noteq> ga_en gc"
      shows "ga_ample sticky_E gc = Some`ga_gample sticky_E gc \<and> ga_en gc = Some`ga_gen gc"
      using assms ga_gample_subset
      unfolding ga_ample_def ga_en_def stutter_extend_en_def
      by (auto split: if_split_asm simp: ga_gample_empty_iff)

    lemma pid_pac_alt: "pid_pac pid = insert None (Some`{(pid',cac). pid'=pid})"
      apply (auto simp: pid_pac_def split: option.splits)
      apply (case_tac x)
      apply auto
      done
  end

  context sticky_prog begin
    sublocale ample_prog prog is_vis_var sticky_E "ga_ample sticky_E"
    proof -
      have aux: "Some ` A = Some ` B \<inter> pid_pac pid \<longleftrightarrow> A = {(pid', cac). (pid', cac) \<in> B \<and> pid' = pid}"
        for A B pid
      proof
        assume 1: "Some ` A = Some ` B \<inter> pid_pac pid"
        show "A = {(pid', cac). (pid', cac) \<in> B \<and> pid' = pid}"
          using 1
          apply (auto simp: pid_pac_alt)
          unfolding image_def
          apply auto
          using 1 by blast
      next
        show "Some ` A = Some ` B \<inter> pid_pac pid" if "A = {(pid', cac). (pid', cac) \<in> B \<and> pid' = pid}"
          using that by (auto simp: pid_pac_alt)
      qed
      show "ample_prog prog is_vis_var sticky_E (ga_ample sticky_E)"
        apply unfold_locales
        apply (frule ga_ample_neq_en_eq, clarsimp)
        apply (intro conjI)
        apply (auto
          simp: ga_gample_def sticky_ga_def
          dest!: find_min_idx_f_SomeD
          split: option.splits if_split_asm) []
        apply (fastforce
          simp: ga_gample_def sticky_ga_def
          dest!: find_min_idx_f_SomeD
          split: option.splits if_split_asm) []
        unfolding aux (* TODO: Clean up! *)
        apply (simp add: inj_image_eq_iff pid_pac_def)
        apply (thin_tac "ga_ample c a = b" for a b c)
        apply (simp add: ga_gample_def split: option.splits prod.splits)
        apply (thin_tac "a \<noteq> ga_gen b" for a b)
        apply (drule find_min_idx_f_SomeD)
        apply clarsimp
        apply (rename_tac gc pid c as)
        apply (rule_tac x=pid in exI)
        apply (auto
          split: if_split_asm prod.splits
          simp: ga_gen_def comp.astep_impl_def)
        unfolding is_ample_static_def comp.astep_impl_def
        apply force
        done
    qed

  end

  text \<open> The following locale expresses a correct ample-reduction on
    the level of subset and stuttering-equivalences of traces \<close>

  locale hl_reduction =
    visible_prog +
    ample: sa "\<lparr> g_V = UNIV, g_E = step, g_V0 = {pid_init_gc}, sa_L = pid_interp_gc \<rparr>"
    for step +
    assumes ample_accept_subset: "ample.accept w \<Longrightarrow> lv.sa.accept w"
    assumes ample_accept_stuttering: "lv.sa.accept w \<Longrightarrow> \<exists>w'. w\<approx>w' \<and> ample.accept w'"

  locale hl_ample_reduction =
    visible_prog +
    ample: sa "\<lparr> g_V = UNIV, g_E = rel_of_enex (ample, ga_ex), g_V0 = {pid_init_gc},
      sa_L = pid_interp_gc \<rparr>"
    for ample +
    assumes ample_accept_subset: "ample.accept w \<Longrightarrow> lv.sa.accept w"
    assumes ample_accept_stuttering: "lv.sa.accept w \<Longrightarrow> \<exists>w'. w\<approx>w' \<and> ample.accept w'"
  begin
    sublocale hl_reduction prog is_vis_var "rel_of_enex (ample, ga_ex)"
      apply unfold_locales
      using ample_accept_subset ample_accept_stuttering by auto
  end

  context sticky_prog
  begin
    sublocale hl_ample: hl_ample_reduction prog is_vis_var "ga_ample sticky_E"
      apply unfold_locales
      unfolding ample_rel_def[symmetric]
      unfolding reduced_automaton_def[symmetric]
      apply simp
      apply simp
      using ample_accept_subset
      apply simp
      apply (erule ample_accept_stuttering)
      apply blast
      done
  end

  text \<open>Next, we implement the selection of a set of sticky edges\<close>
  context visible_prog begin
    definition "cr_ample \<equiv> do {
      sticky_E \<leftarrow> find_fas_init cfgc_G vis_edges;
      RETURN (ga_ample (sticky_E))
    }"

    lemma cr_ample_reduction:
      "cr_ample \<le> SPEC (hl_ample_reduction prog is_vis_var)"
      unfolding cr_ample_def
      apply (refine_vcg order_trans[OF find_fas_init_correct])
      apply unfold_locales[]
      apply simp
    proof clarify
      fix sticky_E
      assume "is_fas cfgc_G sticky_E" "vis_edges \<subseteq> sticky_E"
      then interpret sticky_prog prog is_vis_var sticky_E
        by unfold_locales

      show "hl_ample_reduction prog is_vis_var (ga_ample sticky_E)" by unfold_locales
    qed
  end

  text \<open>We derive an implementation for finding the feedback arcs,
    and an efficient implementation for ga_gample.\<close>

  text \<open>We replace finding the sticky edges by an efficient algorithm\<close>

  context visible_prog begin
    definition ga_gample_m
      :: "_ \<Rightarrow> _ \<Rightarrow> pid_global_config \<Rightarrow> global_action set"
    where
      "ga_gample_m mem sticky_E gc \<equiv> let
        lcs = pid_global_config.processes gc;
        gs = pid_global_config.state gc;
        as = find_min_idx_f (\<lambda>lc.
          let
            c = local_config.command lc;
            ls = local_config.state lc;
            as = set (comp.succ_impl c)
          in
            if (\<forall>(a,_)\<in>as. read_globals a = {} \<and> write_globals a = {}) then
              let
                as = {(a,c')\<in>as. la_en' (ls,gs) a}
              in
                if as={} \<or> (\<exists>(a,c')\<in>as. mem (c,c') sticky_E) then
                  None
                else
                  Some (c,as)
            else
              None
        ) lcs
      in
        case as of
          Some (pid,c,as) \<Rightarrow> (\<lambda>(a,c'). (pid,c,a,c'))`as
        | None \<Rightarrow> ga_gen gc"

    lemma ga_gample_m_refine:
      fixes Rs :: "('si\<times>'s) set"
      shows "(ga_gample_m, ga_gample_m) \<in> (Id\<times>\<^sub>rId \<rightarrow> Rs \<rightarrow> bool_rel) \<rightarrow> Rs \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>set_rel"
    proof (intro fun_relI, simp)
      fix m :: "cmdc\<times>cmdc \<Rightarrow> 's \<Rightarrow> bool" and m' :: "cmdc\<times>cmdc \<Rightarrow> 'si \<Rightarrow> bool"
        and se se' gc
      assume "(m',m)\<in>Id \<rightarrow> Rs \<rightarrow> bool_rel" and "(se',se)\<in>Rs"
      hence "\<And>c c'. (m' (c,c') se', m (c,c') se)\<in>Id"
        by parametricity simp_all
      hence A: "\<And>c c'. m' (c,c') se' = m (c,c') se" by simp
      show "ga_gample_m m' se' gc = ga_gample_m m se gc"
        unfolding ga_gample_m_def
        by (subst A) (rule refl)
    qed

    lemma ga_gample_eq_gample_m: "ga_gample = ga_gample_m (\<in>)"
      unfolding ga_gample_def[abs_def] ga_gample_m_def[abs_def]
      by auto

    lemma stutter_extend_en_refine:
      "(stutter_extend_en, stutter_extend_en) \<in> (R \<rightarrow> \<langle>Id\<rangle>set_rel) \<rightarrow> R \<rightarrow> \<langle>\<langle>Id\<rangle>option_rel\<rangle>set_rel"
      unfolding stutter_extend_en_def[abs_def]
      apply parametricity
      by auto

    lemma is_vis_var_refine: "(is_vis_var, is_vis_var) \<in> Id \<rightarrow> bool_rel" by simp

    lemma vis_edges_refine: "(\<lambda>x. x\<in>vis_edges,vis_edges)\<in>\<langle>Id\<times>\<^sub>rId\<rangle>fun_set_rel"
      by (simp add: fun_set_rel_def br_def)

    lemma [autoref_op_pat_def]:
      "vis_edges \<equiv> Autoref_Tagging.OP vis_edges"
      "ga_gample_m \<equiv> Autoref_Tagging.OP ga_gample_m"
      "cfgc_G \<equiv> Autoref_Tagging.OP cfgc_G"
      by simp_all

    schematic_goal cr_ample_impl1_aux:
      notes [autoref_rules] =
        ga_gample_m_refine stutter_extend_en_refine is_vis_var_refine
        cfgc_G_impl_refine
        vis_edges_refine IdI[of prog]
      shows "(RETURN (?c::?'c),cr_ample)\<in>?R"
      unfolding cr_ample_def ga_ample_def ga_gample_eq_gample_m
      using [[autoref_trace_failed_id, autoref_trace_intf_unif]]
      by (autoref_monadic (plain, trace))
    concrete_definition cr_ample_impl1 uses cr_ample_impl1_aux

    lemma cr_ample_impl1_reduction:
      "hl_ample_reduction prog is_vis_var cr_ample_impl1"
    proof -
      note cr_ample_impl1.refine[THEN nres_relD]
      also note cr_ample_reduction
      finally show ?thesis by simp
    qed

  end

  text \<open>The efficient implementation of @{const visible_prog.ga_gample} uses
    the @{const collecti_index} function\<close>

  lemma collecti_index_cong:
    assumes C: "\<And>i. i<length l \<Longrightarrow> f i (l!i) = f' i (l'!i)"
    assumes [simp]: "l=l'"
    shows "collecti_index f l = collecti_index f' l'"
  proof -
    {
      fix i0 s0
      assume "\<forall>i<length l. f (i0+i) (l!i) = f' (i0+i) (l!i)"
      hence "collecti_index' i0 s0 f l = collecti_index' i0 s0 f' l"
      proof (induction l arbitrary: i0 s0)
        case (Cons a l)

        from Cons.prems[THEN spec, of 0] have
          [simp]: "f i0 a = f' i0 a" by simp

        from Cons.prems have
          IHP: "\<forall>i<length l. f (Suc i0+i) (l!i) = f' (Suc i0+i) (l!i)"
          by auto

        show ?case by (auto split: bool.splits simp: Cons.IH[OF IHP])
      qed simp
    } from this[of 0 "{}"] show ?thesis using assms by simp
  qed

  lemma find_min_idx_f_cong:
    assumes "\<And>x. x\<in>set l \<Longrightarrow> f x = f' x"
    assumes "l=l'"
    shows "find_min_idx_f f l = find_min_idx_f f' l'"
    unfolding assms(2)[symmetric]
    using assms(1)
    apply (induction l)
    apply (auto split: option.split)
    done

  lemma find_min_idx_impl_collecti: "(
      case find_min_idx_f f l of
        Some (i,r) \<Rightarrow> {i} \<times> s1 i r
      | None \<Rightarrow> {(i,r) | i r. i<length l \<and> r\<in>s2 i (l!i)}
    )
  = (
    collecti_index (\<lambda>i x.
      case f x of
        Some r \<Rightarrow> (True, s1 i r)
      | None \<Rightarrow> (False, s2 i x)
    ) l
  )" (is "?l=?r" is "_ = collecti_index ?fc l")
  proof (cases "\<exists>i<length l. f (l!i) \<noteq> None")
    define i where "i \<equiv> LEAST i. i < length l \<and> f (l ! i) \<noteq> None"

    have C_ALT: "(\<exists>i<length l. f (l!i) \<noteq> None)
      \<longleftrightarrow> (\<exists>i. i < length l \<and> fst (?fc i (l ! i)))"
      by (auto split: option.split)

    have i_alt: "i = (LEAST i. i < length l \<and> fst (?fc i (l ! i)))"
      unfolding i_def
      apply (fo_rule arg_cong)
      by (auto split: option.split)

    {
      case True

      from LeastI_ex[OF True] obtain r where [simp]: "i<length l" "f (l!i) = Some r"
        by (auto simp: i_def)

      from True find_min_idx_f_LEAST_eq[of f l]
        have "find_min_idx_f f l = Some (i, the (f (l ! i)))"
        by (simp add: i_def)
      hence LEQ: "?l = {i} \<times> s1 i r" by simp

      from collecti_index_collect[of ?fc l, folded i_alt] True C_ALT have
        REQ: "?r = {i} \<times> snd (?fc i (l!i))"
        by simp
      show "?l=?r" unfolding LEQ unfolding REQ by auto
    }
    {
      case False
      from False find_min_idx_f_LEAST_eq[of f l]
        have "find_min_idx_f f l = None" by simp
      hence LEQ: "?l = {(i,r) | i r. i<length l \<and> r\<in>s2 i (l!i)}" by simp

      from False C_ALT collecti_index_collect[of ?fc l] have
        REQ: "?r = {(i, x) |i x. i < length l \<and> x \<in> snd (?fc i (l ! i))}"
        by auto

      show "?l=?r" unfolding LEQ unfolding REQ using False by auto
    }
  qed

  lemma find_min_idx_impl_collecti_scheme:
    assumes "\<And>x. s11 x = (case x of (i,r) \<Rightarrow> {i} \<times> iss i r)"
    assumes "s12 = {(i,r) | i r. i<length l \<and> r\<in>isn i (l!i)}"
    assumes "\<And>i. i<length l \<Longrightarrow> f2 i (l!i) = (case f (l!i) of
        Some r \<Rightarrow> (True, iss i r)
      | None \<Rightarrow> (False, isn i (l!i)))"
    shows "(case find_min_idx_f f l of Some x \<Rightarrow> s11 x | None \<Rightarrow> s12)
      = (collecti_index f2 l)"
    apply (simp only: assms(1,2,3) cong: collecti_index_cong)
    apply (subst find_min_idx_impl_collecti)
    apply simp
    done

  schematic_goal stutter_extend_en_list_aux: "(?c, stutter_extend_en)
    \<in> (R \<rightarrow> \<langle>S\<rangle>list_set_rel) \<rightarrow> R \<rightarrow> \<langle>\<langle>S\<rangle>option_rel\<rangle>list_set_rel"
    unfolding stutter_extend_en_def[abs_def]
    apply (autoref)
    done
  concrete_definition stutter_extend_en_list uses stutter_extend_en_list_aux

  lemma succ_of_enex_impl_aux:
    "{s'. \<exists>a\<in>en s. s'=ex a s} = (\<lambda>a. ex a s)`en s" by auto

  schematic_goal succ_of_enex_list_aux: "(?c, succ_of_enex) \<in>
    (Id \<rightarrow> \<langle>Id\<rangle>list_set_rel) \<times>\<^sub>r (Id \<rightarrow> Id \<rightarrow> Id) \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>list_set_rel"
    unfolding succ_of_enex_def[abs_def]
    unfolding succ_of_enex_impl_aux
    by (autoref (trace, keep_goal))
  concrete_definition succ_of_enex_list uses succ_of_enex_list_aux

  schematic_goal pred_of_enex_list_aux: "(?c, pred_of_enex) \<in>
    (Id \<rightarrow> \<langle>Id\<rangle>list_set_rel) \<times>\<^sub>r (Id \<rightarrow> Id \<rightarrow> Id) \<rightarrow> Id \<rightarrow> Id \<rightarrow> bool_rel"
    unfolding pred_of_enex_def[abs_def]
    by (autoref (trace, keep_goal))
  concrete_definition pred_of_enex_list uses pred_of_enex_list_aux

  (* TODO: can this be defined using autoref? *)
  definition "rel_of_enex_list enex \<equiv> rel_of_pred (pred_of_enex_list enex)"
  lemma rel_of_enex_list_refine: "(rel_of_enex_list, rel_of_enex) \<in>
    (Id \<rightarrow> \<langle>Id\<rangle>list_set_rel) \<times>\<^sub>r (Id \<rightarrow> Id \<rightarrow> Id) \<rightarrow> \<langle>Id \<times>\<^sub>r Id\<rangle> set_rel"
  proof -
    have 1: "rel_of_enex_list = rel_of_pred \<circ> pred_of_enex_list" using rel_of_enex_list_def by force
    have 2: "rel_of_enex = rel_of_pred \<circ> pred_of_enex" by auto
    have 3: "(rel_of_pred, rel_of_pred) \<in> (Id \<rightarrow> Id \<rightarrow> bool_rel) \<rightarrow> \<langle>Id \<times>\<^sub>r Id\<rangle>set_rel" by auto
    show ?thesis unfolding 1 2 by (parametricity add: 3 pred_of_enex_list.refine)
  qed

  context visible_prog begin
    definition "ga_gample_mi2 mem sticky_E (gc::pid_global_config) = (
      let
        lcs = pid_global_config.processes gc;
        gs = pid_global_config.state gc
      in
        collecti_index (\<lambda>_ lc. let
            c = local_config.command lc;
            ls = local_config.state lc;
            as = set (comp.succ_impl c);
            s={(a,c')\<in>as. la_en' (ls,gs) a};
            ample =
              s\<noteq>{}
            \<and> (\<forall>(a,_)\<in>as. read_globals a = {} \<and> write_globals a = {})
            \<and> (\<forall>(a,c')\<in>s. \<not> mem (c,c') sticky_E)
          in
            (ample,{c}\<times>s)
        ) lcs
    )"

    lemma ga_gample_mi2_impl:
      "ga_gample_m mem sticky_E gc = ga_gample_mi2 mem sticky_E gc"
      unfolding ga_gample_m_def ga_gample_mi2_def
      apply simp
      apply (rule find_min_idx_impl_collecti_scheme[where
          iss="\<lambda>pid (c,S). (\<lambda>(a,c'). (c,a,c'))`S" and
          isn="\<lambda>pid lc. {(c,a,c'). cfgc c a c'
            \<and> c = cmd_of_pid gc pid
            \<and> la_en' (local_config.state lc, pid_global_config.state gc) a}"]
      )
      apply auto []
      unfolding ga_gen_def
      apply auto []
      apply (auto simp: comp.astep_impl_def)
      done

    definition "cr_ample_impl2 \<equiv>
      let sticky = find_fas_init_code (=) bounded_hashcode_nat
         (def_hashmap_size TYPE(nat)) cfgc_G_impl (\<lambda>x. x \<in> vis_edges)
      in stutter_extend_en (ga_gample_mi2 (\<lambda>x f. f x) sticky)"

    definition "ample_step_impl2 \<equiv> rel_of_enex (cr_ample_impl2,ga_ex)"

    lemma cr_ample_impl2_reduction:
      "hl_reduction prog is_vis_var ample_step_impl2"
    proof -
      from cr_ample_impl1_reduction
      interpret hl_ample_reduction prog is_vis_var cr_ample_impl1 .

      have 1: "ample_step_impl2 = rel_of_enex (cr_ample_impl1, ga_ex)"
        unfolding ample_step_impl2_def cr_ample_impl1_def cr_ample_impl2_def
        unfolding ga_gample_mi2_impl[abs_def]
        by simp

      show ?thesis
        apply unfold_locales
        unfolding 1
        apply simp
        apply simp
        apply (blast intro: ample_accept_subset ample_accept_stuttering)+
        done
    qed
  end

text \<open>Implementing the State\<close>
type_synonym valuation_impl = "(ident,uint32) mapping"

definition "vi_\<alpha> \<equiv> map_option Rep_uint32 \<circ>\<circ> Mapping.rep"
abbreviation "vi_rel \<equiv> br vi_\<alpha> (\<lambda>_. True)"

abbreviation "val_rel \<equiv> br Rep_uint32 (\<lambda>_. True)"

lemma vi_rel_rew:
  "(x = vi_\<alpha> y) \<longleftrightarrow> (y,x)\<in>vi_rel"
  "(vi_\<alpha> y = x) \<longleftrightarrow> (y,x)\<in>vi_rel"
  by (auto simp: br_def)

export_code Mapping.lookup Mapping.update Mapping.empty checking SML

lift_definition vi_empty :: "valuation_impl"
  is "Map.empty::valuation" .

lift_definition vi_lookup :: "valuation_impl \<Rightarrow> ident \<rightharpoonup> uint32"
  is "\<lambda>vi::valuation. \<lambda>x. vi x" .
lemma [code]: "vi_lookup = Mapping.lookup"
  apply (intro ext)
  unfolding vi_lookup_def Mapping.lookup_def map_fun_def[abs_def] o_def
    id_apply option.map_comp Rep_uint32_inverse option.map_ident
  by simp

lemma vi_lookup_correct: "vi_lookup v x = map_option Abs_uint32 (vi_\<alpha> v x)"
  unfolding vi_\<alpha>_def
  apply transfer
  apply (simp add: option.map_comp o_def option.map_ident)
  done

lift_definition vi_update :: "ident \<Rightarrow> uint32 \<Rightarrow> valuation_impl \<Rightarrow> valuation_impl"
  is "\<lambda>x v. \<lambda>vi::valuation. vi(x\<mapsto>v)" .
lemma [code]: "vi_update = Mapping.update"
  by transfer simp

lemma vi_update_correct: "vi_\<alpha> (vi_update k v m) = vi_\<alpha> m (k\<mapsto>Rep_uint32 v)"
  unfolding vi_\<alpha>_def
  by transfer simp

export_code vi_lookup vi_update vi_empty checking SML

record local_state_impl =
  variables :: valuation_impl

record global_state_impl =
  variables :: valuation_impl

type_synonym focused_state_impl = "local_state_impl \<times> global_state_impl"

type_synonym local_config_impl
  = "(cmdc,local_state_impl) Gen_Scheduler.local_config"
type_synonym pid_global_config_impl
  = "(cmdc,local_state_impl,global_state_impl) Pid_Scheduler.pid_global_config"

definition "local_state_rel \<equiv> {
  (\<lparr> local_state_impl.variables = vi \<rparr>, \<lparr> local_state.variables = v  \<rparr>) | vi v.
    v = vi_\<alpha> vi
  }"

definition "global_state_rel \<equiv> {
  (\<lparr> global_state_impl.variables = vi \<rparr>, \<lparr> global_state.variables = v  \<rparr>) | vi v.
    v = vi_\<alpha> vi
  }"

abbreviation "focused_state_rel \<equiv> local_state_rel \<times>\<^sub>r global_state_rel"

definition "local_config_rel \<equiv> {
  (\<lparr> local_config.command = ci, local_config.state=lsi \<rparr>,
   \<lparr> local_config.command = c, local_config.state=ls  \<rparr>) | ci c lsi ls.
    (ci::cmdc,c)\<in>Id \<and> (lsi,ls)\<in>local_state_rel
  }"

definition "global_config_rel \<equiv> {
  (\<lparr> pid_global_config.processes = psi, pid_global_config.state = gsi \<rparr>,
   \<lparr> pid_global_config.processes = ps, pid_global_config.state = gs \<rparr>) | psi ps gsi gs.
   (psi,ps)\<in>\<langle>local_config_rel\<rangle>list_rel \<and> (gsi,gs)\<in>global_state_rel
}"

definition "init_valuation_impl vd \<equiv> fold (\<lambda>x v. vi_update x 0 v) vd (vi_empty)"

lemma init_valuation_impl:
  "(init_valuation_impl, init_valuation) \<in> \<langle>Id\<rangle>list_rel \<rightarrow> vi_rel"
proof -
  {
    fix vd m
    have "m ++ init_valuation vd = fold (\<lambda>x v. v(x\<mapsto>0)) vd m"
      apply (rule sym)
      apply (induction vd arbitrary: m)
      unfolding init_valuation_def[abs_def]
      apply (auto intro!: ext simp: Map.map_add_def)
      done
  } note aux=this
  have E1: "\<And>vd. init_valuation vd = fold (\<lambda>x v. v(x\<mapsto>0)) vd Map.empty"
    by (subst aux[symmetric]) simp

  have E2: "\<And>vdi vd. (vdi,vd)\<in>\<langle>Id\<rangle>list_rel
    \<Longrightarrow> (init_valuation_impl vdi, fold (\<lambda>x v. v(x\<mapsto>0)) vd Map.empty) \<in> vi_rel"
    unfolding init_valuation_impl_def
    apply parametricity
    apply (auto simp: vi_update_correct vi_empty_correct br_def zero_uint32.rep_eq)
    done

  show ?thesis
    apply (intro fun_relI)
    apply (subst E1)
    apply (rule E2)
    by auto
qed

context cprog begin

  definition init_pc_impl :: "proc_decl \<Rightarrow> local_config_impl" where
    "init_pc_impl pd \<equiv> \<lparr>
      local_config.command = comp.\<gamma> (proc_decl.body pd),
      local_config.state = \<lparr>
        local_state_impl.variables = init_valuation_impl (proc_decl.local_vars pd)
      \<rparr>
    \<rparr>"

  lemma init_pc_impl: "(init_pc_impl, init_pc) \<in> Id \<rightarrow> local_config_rel"
    apply (rule fun_relI)
    unfolding init_pc_impl_def init_pc_def local_config_rel_def local_state_rel_def
    apply (simp del: pair_in_Id_conv, intro conjI)
    apply simp
    apply (simp only: vi_rel_rew)
    apply (parametricity add: init_valuation_impl)
    apply simp
    done

  definition pid_init_gc_impl :: "pid_global_config_impl" where
    "pid_init_gc_impl \<equiv> \<lparr>
      pid_global_config.processes = (map init_pc_impl (program.processes prog)),
      pid_global_config.state = \<lparr>
        global_state_impl.variables = init_valuation_impl (program.global_vars prog)
      \<rparr>
    \<rparr>"

  lemma pid_init_gc_impl: "(pid_init_gc_impl, pid_init_gc) \<in> global_config_rel"
    unfolding pid_init_gc_impl_def pid_init_gc_def global_config_rel_def global_state_rel_def
    apply (simp del: pair_in_Id_conv, intro conjI)
    apply (parametricity add: init_pc_impl)
    apply simp
    apply (simp only: vi_rel_rew)
    apply (parametricity add: init_valuation_impl)
    apply simp
    done

end

lift_definition val_of_bool_impl :: "bool \<Rightarrow> uint32" is val_of_bool .
lemma [code]: "val_of_bool_impl b = (if b then 1 else 0)"
  by transfer auto

lift_definition bool_of_val_impl :: "uint32 \<Rightarrow> bool" is bool_of_val .
lemma [code]: "bool_of_val_impl v = (v\<noteq>0)"
  by transfer (auto simp: bool_of_val_def)

definition "set_of_rel R \<equiv> {(a,b) . R b a}"
definition "rel_of_set S \<equiv> \<lambda>b a. (a,b)\<in>S"

lemma [simp]:
  "set_of_rel (rel_of_set S) = S"
  "rel_of_set (set_of_rel R) = R"
  unfolding rel_of_set_def set_of_rel_def
  by auto

lemma rel_fun_2set: "rel_fun A B = rel_of_set (set_of_rel A \<rightarrow> set_of_rel B)"
  unfolding rel_fun_def fun_rel_def
  unfolding rel_of_set_def set_of_rel_def
  by (auto)

lemma [simp]:
  "set_of_rel cr_uint32 = val_rel"
  "set_of_rel (=) = Id"
  by (auto simp: br_def cr_uint32_def)

lemma bool_of_val_impl: "(bool_of_val_impl, bool_of_val) \<in> val_rel \<rightarrow> bool_rel"
  using bool_of_val_impl.transfer
  by (simp add: rel_fun_2set)

lemma smod_by_div_abs: "a smod b = a - a sdiv b * b"
  using sdiv_smod_id[of a b]
  by (metis add_diff_cancel2)

lift_definition sdiv_impl :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(sdiv)" .
lift_definition smod_impl :: "uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" is "(smod)" .

(* TODO: Is there a more efficient way? *)
lemma [code]: "sdiv_impl x y = Abs_uint32' (Rep_uint32' x sdiv Rep_uint32' y)"
  apply transfer
  by simp

lemma [code]: "smod_impl a b = a - sdiv_impl a b * b"
  apply transfer
  using sdiv_smod_id
  by (metis add_diff_cancel2)

primrec eval_bin_op_impl_aux :: "bin_op \<Rightarrow> uint32 \<Rightarrow> uint32 \<Rightarrow> uint32" where
  "eval_bin_op_impl_aux bo_plus v1 v2 = v1+v2"
| "eval_bin_op_impl_aux bo_minus v1 v2 = v1-v2"
| "eval_bin_op_impl_aux bo_mul v1 v2 = v1*v2"
| "eval_bin_op_impl_aux bo_div v1 v2 = sdiv_impl v1 v2"
| "eval_bin_op_impl_aux bo_mod v1 v2 = smod_impl v1 v2"
| "eval_bin_op_impl_aux bo_less v1 v2 = val_of_bool_impl (v1 < v2)"
| "eval_bin_op_impl_aux bo_less_eq v1 v2 = val_of_bool_impl (v1 \<le> v2)"
| "eval_bin_op_impl_aux bo_eq v1 v2 = val_of_bool_impl (v1 = v2)"
| "eval_bin_op_impl_aux bo_and v1 v2 = v1 AND v2"
| "eval_bin_op_impl_aux bo_or v1 v2 = v1 OR v2"
| "eval_bin_op_impl_aux bo_xor v1 v2 = v1 XOR v2"

lift_definition eval_bin_op_impl :: "bin_op \<Rightarrow> uint32 \<Rightarrow> uint32 \<Rightarrow> uint32"
  is eval_bin_op .
print_theorems

lemma [code]: "eval_bin_op_impl bop v1 v2 = eval_bin_op_impl_aux bop v1 v2"
  apply (cases bop)
  apply simp_all
  apply (transfer, simp)+
  done

primrec eval_un_op_impl_aux :: "un_op \<Rightarrow> uint32 \<Rightarrow> uint32" where
  "eval_un_op_impl_aux uo_minus v = -v"
| "eval_un_op_impl_aux uo_not v = NOT v"

lift_definition eval_un_op_impl :: "un_op \<Rightarrow> uint32 \<Rightarrow> uint32"
  is eval_un_op .

lemma [code]: "eval_un_op_impl uop v = eval_un_op_impl_aux uop v"
  apply (cases uop)
  apply simp_all
  apply (transfer, simp)+
  done

fun eval_exp_impl :: "exp \<Rightarrow> focused_state_impl \<rightharpoonup> uint32" where
  "eval_exp_impl (e_var x) (ls,gs) = do {
    let lv = local_state_impl.variables ls;
    let gv = global_state_impl.variables gs;
    case vi_lookup lv x of
      Some v \<Rightarrow> Some v
    | None \<Rightarrow> (case vi_lookup gv x of
        Some v \<Rightarrow> Some v
      | None \<Rightarrow> None)
  }"
| "eval_exp_impl (e_localvar x) (ls,gs) = vi_lookup (local_state_impl.variables ls) x"
| "eval_exp_impl (e_globalvar x) (ls,gs) = vi_lookup (global_state_impl.variables gs) x"
| "eval_exp_impl (e_const n) fs = do {
    assert_option (n\<ge>min_signed \<and> n\<le>max_signed);
    Some (uint32_of_int n)
  }"
| "eval_exp_impl (e_bin bop e1 e2) fs = do {
    v1\<leftarrow>eval_exp_impl e1 fs;
    v2\<leftarrow>eval_exp_impl e2 fs;
    Some (eval_bin_op_impl bop v1 v2)
    }"
| "eval_exp_impl (e_un uop e) fs = do {
    v\<leftarrow>eval_exp_impl e fs;
    Some (eval_un_op_impl uop v)
    }"

(* TODO: Move *)
lemma map_option_bind: "map_option f (m\<bind>g) = m \<bind> (map_option f o g)"
  by (auto split: Option.bind_split)

lemma val_option_rel_as_eq: "(a,b)\<in>\<langle>val_rel\<rangle>option_rel \<longleftrightarrow> map_option Rep_uint32 a = b"
  unfolding br_def
  apply (cases a)
  apply (cases b, simp_all)
  apply (cases b, auto)
  done

lemma eval_exp_impl: "(eval_exp_impl, eval_exp) \<in> Id \<rightarrow> focused_state_rel \<rightarrow> \<langle>val_rel\<rangle>option_rel"
proof -
  {
    fix e ls gs lsi gsi
    assume "(lsi,ls)\<in>local_state_rel" "(gsi,gs)\<in>global_state_rel"
    hence "map_option Rep_uint32 (eval_exp_impl e (lsi,gsi)) = eval_exp e (ls,gs)"
      apply (induction e)
      apply (auto
        simp: local_state_rel_def global_state_rel_def br_def
        simp: vi_lookup_correct vi_update_correct
        simp: Abs_uint32_inverse[simplified] uint32_of_int.rep_eq signed_of_int_def
        simp: option.map_comp option.map_ident o_def map_option_bind
        simp: eval_bin_op_impl.rep_eq eval_un_op_impl.rep_eq
        split: option.splits)
      apply (drule sym)
      apply (drule sym)
      apply (simp split: Option.bind_split)

      apply (drule sym)
      apply (simp split: Option.bind_split)
      done
  } thus ?thesis
    by (auto simp: val_option_rel_as_eq)
qed

text \<open>Enabledness and effects of actions\<close>
primrec la_en_impl :: "focused_state_impl \<Rightarrow> action \<rightharpoonup> bool" where
  "la_en_impl fs (AAssign e _ _) = do {
    v \<leftarrow> eval_exp_impl e fs;
    Some (bool_of_val_impl v)}"
| "la_en_impl fs (AAssign_local e _ _) = do {
    v \<leftarrow> eval_exp_impl e fs;
    Some (bool_of_val_impl v)}"
| "la_en_impl fs (AAssign_global e _ _) = do {
    v \<leftarrow> eval_exp_impl e fs;
    Some (bool_of_val_impl v)}"
| "la_en_impl fs (ATest e) = do {
    v \<leftarrow> eval_exp_impl e fs;
    Some (bool_of_val_impl v)}"
| "la_en_impl _ (ASkip) = Some True"

lemma param_rec_action[param]: "(rec_action, rec_action) \<in> (Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> A)
    \<rightarrow> (Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> A)
       \<rightarrow> (Id \<rightarrow> Id \<rightarrow> Id \<rightarrow> A) \<rightarrow> (Id \<rightarrow> A) \<rightarrow> A \<rightarrow> Id \<rightarrow> A"
  apply (intro fun_relI)
  subgoal for fi1 f1 fi2 f2 fi3 f3 fi4 f4 fi5 f5 ai a
    apply simp
    apply (induction a)
    apply simp_all
    apply (parametricity, simp_all?)+
    done
  done

(* TODO: Move *)
lemma param_option_bind[param]:
  "(Option.bind, Option.bind) \<in> \<langle>A\<rangle>option_rel \<rightarrow> (A \<rightarrow> \<langle>B\<rangle>option_rel) \<rightarrow> \<langle>B\<rangle>option_rel"
  unfolding Option.bind_def by parametricity

lemma la_en_impl: "(la_en_impl,la_en) \<in> focused_state_rel \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>option_rel"
  unfolding la_en_impl_def la_en_def
  by (parametricity add: eval_exp_impl bool_of_val_impl)

definition "la_en'_impl fs a \<equiv> case la_en_impl fs a of Some b \<Rightarrow> b | None \<Rightarrow> False"

lemma la_en'_impl: "(la_en'_impl,la_en') \<in> focused_state_rel \<rightarrow> Id \<rightarrow> bool_rel"
  unfolding la_en'_impl_def[abs_def] la_en'_def[abs_def]
  by (parametricity add: la_en_impl)

abbreviation "exists_var_impl v x \<equiv> vi_lookup v x \<noteq> None"

fun la_ex_impl :: "focused_state_impl \<Rightarrow> action \<rightharpoonup> focused_state_impl" where
  "la_ex_impl (ls,gs) (AAssign ge x e) = do {
    v \<leftarrow> eval_exp_impl ge (ls,gs);
    assert_option (bool_of_val_impl v);
    v \<leftarrow> eval_exp_impl e (ls,gs);
    if exists_var_impl (local_state_impl.variables ls) x then do {
      let ls = local_state_impl.variables_update (vi_update x v) ls;
      Some (ls,gs)
    } else do {
      assert_option (exists_var_impl (global_state_impl.variables gs) x);
      let gs = global_state_impl.variables_update (vi_update x v) gs;
      Some (ls,gs)
    }
  }"
| "la_ex_impl (ls,gs) (AAssign_local ge x e) = do {
    v \<leftarrow> eval_exp_impl ge (ls,gs);
    assert_option (bool_of_val_impl v);
    v \<leftarrow> eval_exp_impl e (ls,gs);
    assert_option (exists_var_impl (local_state_impl.variables ls) x);
    let ls = local_state_impl.variables_update (vi_update x v) ls;
    Some (ls,gs)
  }"
| "la_ex_impl (ls,gs) (AAssign_global ge x e) = do {
    v \<leftarrow> eval_exp_impl ge (ls,gs);
    assert_option (bool_of_val_impl v);
    v \<leftarrow> eval_exp_impl e (ls,gs);
    assert_option (exists_var_impl (global_state_impl.variables gs) x);
    let gs = global_state_impl.variables_update (vi_update x v) gs;
    Some (ls,gs)
  }"
| "la_ex_impl fs (ATest e) = do {
    v \<leftarrow> eval_exp_impl e fs;
    assert_option (bool_of_val_impl v);
    Some fs
  }"
| "la_ex_impl fs ASkip = Some fs"

(* TODO: Move *)
lemma param_assert_option[param]:
  "(assert_option, assert_option) \<in> bool_rel \<rightarrow> \<langle>unit_rel\<rangle>option_rel"
  unfolding assert_option_def by parametricity

lemma la_ex_impl: "(la_ex_impl, la_ex)
  \<in> focused_state_rel \<rightarrow> Id \<rightarrow> \<langle>focused_state_rel\<rangle>option_rel"
proof (intro fun_relI)
  fix fsi fs and ai a :: action
  assume "(fsi,fs)\<in>focused_state_rel" "(ai,a)\<in>Id"
  thus "(la_ex_impl fsi ai, la_ex fs a)\<in>\<langle>focused_state_rel\<rangle>option_rel"
    apply (cases fs, cases fsi, clarsimp)
    apply (cases a)
    apply simp_all
    apply (parametricity add: eval_exp_impl bool_of_val_impl)
    apply (auto
      simp: local_state_rel_def global_state_rel_def
      simp: vi_lookup_correct vi_update_correct
      simp: br_def
      intro: domI) [7]
    apply (parametricity add: eval_exp_impl bool_of_val_impl)
    apply (auto
      simp: local_state_rel_def global_state_rel_def
      simp: vi_lookup_correct vi_update_correct
      br_def intro: domI) [9]
    apply (parametricity add: eval_exp_impl bool_of_val_impl)
    apply (auto
      simp: local_state_rel_def global_state_rel_def
      simp: vi_lookup_correct vi_update_correct
      br_def intro: domI) [4]
    apply (parametricity add: eval_exp_impl bool_of_val_impl)
    apply simp
    done
qed

definition "la_ex'_impl fs a \<equiv> case la_ex_impl fs a of Some fs' \<Rightarrow> fs' | None \<Rightarrow> fs"
lemma la_ex'_impl: "(la_ex'_impl,la_ex') \<in> focused_state_rel \<rightarrow> Id \<rightarrow> focused_state_rel"
  unfolding la_ex'_impl_def[abs_def] la_ex'_def[abs_def]
  by (parametricity add: la_ex_impl)

lemma param_collecti_index: "(collecti_index, collecti_index) \<in>
    (nat_rel \<rightarrow> B \<rightarrow> bool_rel \<times>\<^sub>r \<langle>Id\<rangle>set_rel) \<rightarrow> \<langle>B\<rangle>list_rel \<rightarrow> \<langle>nat_rel \<times>\<^sub>r Id\<rangle>set_rel"
  unfolding collecti_index'_def
  apply parametricity
  apply auto
  done

export_code la_ex_impl la_en_impl checking SML

context visible_prog
begin

  definition "ga_gample_mi3 mem sticky_E (gc::pid_global_config_impl) = (
    let
      lcs = pid_global_config.processes gc;
      gs = pid_global_config.state gc
    in
      collecti_index (\<lambda>_ lc. let
          c = local_config.command lc;
          ls = local_config.state lc;
          as = set (comp.succ_impl c);
          s={(a,c')\<in>as. la_en'_impl (ls,gs) a};
          ample =
            s\<noteq>{}
          \<and> (\<forall>(a,_)\<in>as. read_globals a = {} \<and> write_globals a = {})
          \<and> (\<forall>(a,c')\<in>s. \<not> mem (c,c') sticky_E)
        in
          (ample,{c}\<times>s)
      ) lcs
  )"

  lemma ga_gample_mi3_refine:
    "(ga_gample_mi3, ga_gample_mi2)\<in>
      Id \<rightarrow> Id \<rightarrow> global_config_rel \<rightarrow> \<langle>nat_rel \<times>\<^sub>r Id\<rangle>set_rel"
  proof -
    have [param]: "(comp.succ_impl,comp.succ_impl)\<in>Id\<rightarrow>\<langle>Id\<times>\<^sub>rId\<rangle>list_rel"
      by simp

    from la_en'_impl have aux1: "\<And>fsi fs a. (fsi,fs)\<in>focused_state_rel \<Longrightarrow>
      la_en'_impl fsi a = la_en' fs a"
      apply (rule_tac IdD)
      apply parametricity
      by auto

    show ?thesis
      using [[goals_limit=1]]
      apply (intro fun_relI)
      unfolding ga_gample_mi3_def ga_gample_mi2_def
      apply (parametricity add: param_collecti_index la_en'_impl)
      apply (auto simp add: global_config_rel_def local_config_rel_def) []
      apply (auto simp add: global_config_rel_def local_config_rel_def) []
      apply (auto simp add: global_config_rel_def local_config_rel_def) []
      apply (auto simp add: global_config_rel_def local_config_rel_def) []
      apply simp
      using aux1
      apply (auto simp add: global_config_rel_def local_config_rel_def) []
      apply simp_all
      done

  qed

  definition (in cprog) "is_vis_edge is_vis_var \<equiv> \<lambda>(c,c').
    \<exists>(a,cc')\<in>set (comp.succ_impl c). c'=cc' \<and> (\<exists>v\<in>write_globals a. is_vis_var v)"

  lemma is_vis_edge_correct: "is_vis_edge is_vis_var = (\<lambda>x. x\<in>vis_edges)"
    unfolding is_vis_edge_def vis_edges_def
    by (auto intro!: ext simp: comp.astep_impl_def)

  definition "cr_ample_impl3 \<equiv>
    let sticky = find_fas_init_code (=) bounded_hashcode_nat
         (def_hashmap_size TYPE(nat)) cfgc_G_impl (\<lambda>x. x \<in> vis_edges)
    in stutter_extend_en (ga_gample_mi3 (\<lambda>x f. f x) sticky)"

  lemma cr_ample_impl3_refine: "(cr_ample_impl3, cr_ample_impl2)
    \<in> global_config_rel \<rightarrow> \<langle>\<langle>nat_rel\<times>\<^sub>rId\<rangle>option_rel\<rangle>set_rel"
  proof -
    have [param]: "\<And>R S. S=Id \<Longrightarrow>
      (stutter_extend_en, stutter_extend_en)
        \<in> (R \<rightarrow> \<langle>S\<rangle>set_rel) \<rightarrow> R \<rightarrow> \<langle>\<langle>S\<rangle>option_rel\<rangle>set_rel"
      apply (simp only: )
      by (rule stutter_extend_en_refine)

    show ?thesis
      unfolding cr_ample_impl3_def cr_ample_impl2_def is_vis_edge_correct
      apply (parametricity add: stutter_extend_en_refine ga_gample_mi3_refine)
      apply (rule IdI)
      by auto
  qed

(* TODO: The current Pid_Scheduler-locale is focused on refinement.
  We cannot use it to get an instantiation of ga_gex_impl.*)

  definition (in -) ga_gex_impl
    :: "global_action \<Rightarrow> pid_global_config_impl \<Rightarrow> pid_global_config_impl"
  where
    "ga_gex_impl ga gc \<equiv> let
      (pid,c,a,c') = ga;
      fs = fs_of_pid gc pid;
      (ls',gs') = la_ex'_impl fs a;
      gc' = \<lparr>
          pid_global_config.processes = (pid_global_config.processes gc)
            [pid :=
              \<lparr> local_config.command = c', local_config.state = ls'\<rparr>
            ],
          pid_global_config.state = gs'\<rparr>
    in
      gc'"

  lemma lc_of_pid_refine:
    assumes V: "pid_valid gc pid"
    assumes [param]: "(pidi,pid)\<in>nat_rel"
    assumes GCI: "(gci,gc)\<in>global_config_rel"
    shows "(lc_of_pid gci pidi, lc_of_pid gc pid)\<in>local_config_rel"
    apply parametricity
    apply fact
    using GCI by (auto simp: global_config_rel_def)

  lemma ls_of_pid_refine:
    assumes "pid_valid gc pid"
    assumes "(pidi,pid)\<in>nat_rel"
    assumes "(gci,gc)\<in>global_config_rel"
    shows "(ls_of_pid gci pidi, ls_of_pid gc pid)\<in>local_state_rel"
    using lc_of_pid_refine[OF assms] unfolding local_config_rel_def by auto

  lemma ga_gex_impl:
    assumes V: "pid_valid gc pid"
    assumes [param]: "(pidi,pid)\<in>Id" "(ci,c)\<in>Id"
      "(ai,a)\<in>Id" and CI'I: "(ci',c')\<in>Id" and GCI[param]: "(gci,gc)\<in>global_config_rel"
    shows "(ga_gex_impl (pidi,ci,ai,ci') gci, ga_gex (pid,c,a,c') gc) \<in> global_config_rel"
    unfolding ga_gex_impl_def[abs_def] ga_gex_def[abs_def]
    apply simp
    apply (parametricity add: la_ex'_impl ls_of_pid_refine[OF V])
    using GCI CI'I
    apply (auto simp: global_config_rel_def local_config_rel_def) []
    apply parametricity
    apply auto []
    using GCI
    apply (auto simp: global_config_rel_def) []
    done

  definition (in -) "ga_ex_impl \<equiv> stutter_extend_ex ga_gex_impl"

  fun ga_valid where
    "ga_valid gc None = True"
  | "ga_valid gc (Some (pid,c,a,c')) = pid_valid gc pid"

  lemma ga_ex_impl:
    assumes V: "ga_valid gc ga"
    assumes P: "(gai,ga)\<in>Id" "(gci,gc)\<in>global_config_rel"
    shows "(ga_ex_impl gai gci, ga_ex ga gc) \<in> global_config_rel"
    using assms
    apply (cases "(gc,ga)" rule: ga_valid.cases)
    using P
    apply (simp add: ga_ex_impl_def)

    apply (simp add: ga_ex_impl_def ga_ex_def)
    apply (parametricity add: ga_gex_impl)
    by auto

  definition "ample_step_impl3 \<equiv> rel_of_enex (cr_ample_impl3,ga_ex_impl)"

  definition (in -) pid_interp_gc_impl
    :: "(ident \<Rightarrow> bool) \<Rightarrow> pid_global_config_impl \<Rightarrow> exp set"
  where
    "pid_interp_gc_impl is_vis_var gci \<equiv> sm_props (
    vi_\<alpha> (global_state_impl.variables (pid_global_config.state gci)) |` Collect is_vis_var
  )"

  lemma pid_interp_gc_impl:
    "(pid_interp_gc_impl is_vis_var, pid_interp_gc) \<in> global_config_rel \<rightarrow> Id"
    apply rule
    unfolding pid_interp_gc_impl_def pid_interp_gc_def
    apply (auto simp: global_config_rel_def global_state_rel_def
      interp_gs_def sm_props_def br_def)
    done

  lemma cr_ample_impl3_sim_aux:
    assumes GCI: "(gci, gc) \<in> global_config_rel"
    assumes GA: "ga \<in> cr_ample_impl3 gci"
    shows "\<exists>gc'. ga\<in>cr_ample_impl2 gc
      \<and> gc'=ga_ex ga gc
      \<and> (ga_ex_impl ga gci, gc')\<in>global_config_rel"
  proof (clarsimp, safe)
    show G1: "ga\<in>cr_ample_impl2 gc"
      using cr_ample_impl3_refine[param_fo, OF GCI] GA by auto

    { (* TODO: We are re-proving the validity of the action, due
        to the lack of a clean refinement argumentation *)
      fix mem sticky_E gc pid c
      assume "(pid,c)\<in>ga_gample_m mem sticky_E gc"
      hence "pid_valid gc pid"
        unfolding ga_gample_m_def
        apply (auto split: option.splits)
        apply (auto simp: ga_gen_def) []
        apply (auto dest: find_min_idx_f_SomeD)
        done
    } note aux=this
    from G1 have "ga_valid gc ga"
      unfolding cr_ample_impl2_def stutter_extend_en_def
      apply (simp split: if_split_asm)
      unfolding ga_gample_mi2_impl[symmetric]
      apply (auto dest: aux)
      done
    thus "(ga_ex_impl ga gci, ga_ex ga gc)\<in>global_config_rel"
      by (parametricity add: ga_ex_impl GCI IdI[of ga])
  qed

  lemma cr_ample_impl3_sim_aux2:
    assumes GCI: "(gci, gc) \<in> global_config_rel"
    assumes GA: "ga \<in> cr_ample_impl2 gc"
    shows "ga\<in>cr_ample_impl3 gci
      \<and> (ga_ex_impl ga gci, ga_ex ga gc) \<in> global_config_rel"
  proof
    show G1: "ga\<in>cr_ample_impl3 gci"
      using cr_ample_impl3_refine[param_fo, OF GCI] GA by auto

    from cr_ample_impl3_sim_aux[OF GCI G1] show
      "(ga_ex_impl ga gci, ga_ex ga gc) \<in> global_config_rel"
      by auto
  qed

  sublocale impl3: sa "\<lparr> g_V = UNIV, g_E = ample_step_impl3, g_V0 = {pid_init_gc_impl},
      sa_L = pid_interp_gc_impl is_vis_var \<rparr>" by unfold_locales auto

  sublocale impl3_sim: lbisimulation
    global_config_rel
    "\<lparr> g_V = UNIV, g_E = ample_step_impl3, g_V0 = {pid_init_gc_impl},
      sa_L = pid_interp_gc_impl is_vis_var \<rparr>"
    "\<lparr> g_V = UNIV, g_E = ample_step_impl2, g_V0 = {pid_init_gc},
      sa_L = pid_interp_gc \<rparr>"
    apply unfold_locales
    apply simp
    apply simp
    apply simp
    using pid_init_gc_impl
    apply (auto dest: fun_relD) []
    unfolding ample_step_impl2_def ample_step_impl3_def
    apply (auto dest: cr_ample_impl3_sim_aux) []
    using pid_interp_gc_impl
    apply (auto dest: fun_relD) []
    apply simp

    using pid_init_gc_impl
    apply (auto dest: fun_relD) []
    defer
    using pid_interp_gc_impl
    apply (auto dest: fun_relD) []
    apply auto

    apply (auto dest: cr_ample_impl3_sim_aux2) []
    done

  text \<open>Correctness of impl3\<close>
  (* TODO: Locale hl_reduction seems very special, and we cannot use it here*)
  lemma impl3_accept_subset: "impl3.accept w \<Longrightarrow> lv.sa.accept w"
    using impl3_sim.accept_bisim cr_ample_impl2_reduction hl_reduction.ample_accept_subset
    by simp

  lemma impl3_accept_stuttering: "lv.sa.accept w \<Longrightarrow> \<exists>w'. w\<approx>w' \<and> impl3.accept w'"
    using impl3_sim.accept_bisim cr_ample_impl2_reduction hl_reduction.ample_accept_stuttering
    by simp

  text \<open>Next, we go from sets of actions to lists of actions\<close>
  definition (in cprog) "ga_gample_mil4 mem sticky_Ei (gc::pid_global_config_impl) = (
    let
      lcs = pid_global_config.processes gc;
      gs = pid_global_config.state gc
    in
      collecti_index_list (\<lambda>_ lc. let
          c = local_config.command lc;
          ls = local_config.state lc;
          as = comp.succ_impl c;
          s = filter (la_en'_impl (ls,gs) o fst) as;
          ample = s\<noteq>[]
          \<and> (\<forall>(a,_)\<in>set as. read_globals a = {} \<and> write_globals a = {})
          \<and> (\<forall>(a,c')\<in>set s. \<not>mem (c,c') sticky_Ei)
        in
          (ample,map (Pair c) s)
      ) lcs
  )"

  lemma ga_gample_mil4_refine:
    "(ga_gample_mil4, ga_gample_mi3)
    \<in> (Id\<times>\<^sub>rId \<rightarrow> Id \<rightarrow> bool_rel) \<rightarrow> Id \<rightarrow> Id \<rightarrow> \<langle>nat_rel \<times>\<^sub>r Id\<rangle>list_set_rel"
    apply (intro fun_relI)
    unfolding ga_gample_mil4_def ga_gample_mi3_def
    apply (parametricity)
    apply simp
    apply (rule IdI)
    apply simp
    apply (rule IdI)
    apply (intro fun_relI)
    apply (rule collecti_index_list_refine[param_fo])
    apply (intro fun_relI)
    apply (simp add: list_set_rel_def br_def distinct_map
      comp.succ_impl_invar)
    apply (auto simp: filter_empty_conv)
    apply force
    done

  definition (in cprog) "cr_ample_impl4 is_vis_var \<equiv>
    let sticky = find_fas_init_code (=) bounded_hashcode_nat
         (def_hashmap_size TYPE(nat)) cfgc_G_impl (is_vis_edge is_vis_var)
    in stutter_extend_en_list (ga_gample_mil4 (\<lambda>x f. f x) sticky)"

  lemma cr_ample_impl4_refine:
    "(cr_ample_impl4 is_vis_var, cr_ample_impl3)\<in>Id \<rightarrow> \<langle>\<langle>nat_rel \<times>\<^sub>r Id\<rangle>option_rel\<rangle>list_set_rel"
    unfolding cr_ample_impl4_def cr_ample_impl3_def
    apply (parametricity add: stutter_extend_en_list.refine ga_gample_mil4_refine)
    apply (simp_all add: is_vis_edge_correct)
    done

  text \<open>Finally, we combine the ample-implementation and the executable implementation
    to get a step function\<close>
  definition (in cprog) "ample_step_impl4 is_vis_var \<equiv>
    rel_of_enex_list (cr_ample_impl4 is_vis_var,ga_ex_impl)"

  lemma ample_step_impl4:
    "(ample_step_impl4 is_vis_var, ample_step_impl3) \<in> \<langle>Id \<times>\<^sub>r Id\<rangle> set_rel"
    unfolding ample_step_impl4_def ample_step_impl3_def rel_of_pred_def
    apply (parametricity add: rel_of_enex_list_refine cr_ample_impl4_refine[simplified])
    by auto

  sublocale impl4: sa "\<lparr> g_V = UNIV, g_E = ample_step_impl4 is_vis_var,
    g_V0 = {pid_init_gc_impl}, sa_L = pid_interp_gc_impl is_vis_var \<rparr>" by unfold_locales auto

  lemma impl4_accept_subset: "impl4.accept w \<Longrightarrow> lv.sa.accept w"
    using impl3_accept_subset ample_step_impl4
    by simp

  lemma impl4_accept_stuttering: "lv.sa.accept w \<Longrightarrow> \<exists>w'. w\<approx>w' \<and> impl4.accept w'"
    using impl3_accept_stuttering ample_step_impl4
    by simp

  lemma (in -) pred_of_succ_of_enex_list:
    fixes enex :: "('c \<Rightarrow> 'a list) \<times> ('a \<Rightarrow> 'c \<Rightarrow> 'c)"
    shows "pred_of_succ (set o succ_of_enex_list enex) = pred_of_enex_list enex"
  proof -
    { fix x and l
      have "glist_member (=) x l \<longleftrightarrow> x\<in>set l"
        by (induction l) auto
    } note [simp] = this

    {
      fix l :: "'a list" and g and l0
      have "set (foldli l (\<lambda>_. True) (\<lambda>x. glist_insert (=) (g x)) l0) = set l0 \<union> g`set l"
        by (induction l arbitrary: l0) (auto simp: glist_insert_def)
    } note [simp] = this

    {
      fix l::"'a list" and P i
      have "foldli l Not (\<lambda>x _. P x) i \<longleftrightarrow> i \<or> (\<exists>x\<in>set l. P x)"
        by (induction l arbitrary: i) auto
    } note [simp] = this

    show ?thesis
      unfolding succ_of_enex_list_def[abs_def] pred_of_enex_list_def[abs_def]
      by (auto simp: pred_of_succ_def gen_image_def gen_bex_def intro!: ext)
  qed
  lemma (in -) rel_of_succ_of_enex_list:
    fixes enex :: "('c \<Rightarrow> 'a list) \<times> ('a \<Rightarrow> 'c \<Rightarrow> 'c)"
    shows "rel_of_succ (set o succ_of_enex_list enex) = rel_of_enex_list enex"
    unfolding rel_of_enex_list_def
    unfolding pred_of_succ_of_enex_list[symmetric]
    by simp

  definition (in cprog) "impl4_succ is_vis_var
    \<equiv> succ_of_enex_list (cr_ample_impl4 is_vis_var,ga_ex_impl)"
  lemma impl4_succ_pred:
    "rel_of_succ (set o (impl4_succ is_vis_var)) = ample_step_impl4 is_vis_var"
    unfolding impl4_succ_def ample_step_impl4_def
    by (simp add: rel_of_succ_of_enex_list)

end

export_code ga_ex_impl checking SML

definition "ccfg_E_succ_impl mst \<equiv> remdups o map snd o ccfg_succ_impl mst"

lemma (in cprog) ccfg_E_succ_impl: "ccfg_E_succ_impl (comp_info_of prog) = cfgc_E_succ"
  apply (intro ext)
  unfolding ccfg_E_succ_impl_def cfgc_E_succ_def
  by (simp add: ccfg_succ_impl)

definition init_pc_impl_impl :: "comp_info \<Rightarrow> proc_decl \<Rightarrow> local_config_impl" where
  "init_pc_impl_impl mst pd \<equiv> \<lparr>
    local_config.command = comp_\<gamma>_impl mst (proc_decl.body pd),
    local_config.state = \<lparr>
      local_state_impl.variables = init_valuation_impl (proc_decl.local_vars pd)
    \<rparr>
  \<rparr>"

lemma (in cprog) init_pc_impl_impl: "init_pc_impl_impl (comp_info_of prog) = init_pc_impl"
  apply (intro ext)
  unfolding init_pc_impl_impl_def init_pc_impl_def
  by (simp add: comp_\<gamma>_impl)

definition pid_init_gc_impl_impl :: "program \<Rightarrow> comp_info \<Rightarrow> pid_global_config_impl" where
  "pid_init_gc_impl_impl prog mst \<equiv> \<lparr>
    pid_global_config.processes = (map (init_pc_impl_impl mst) (program.processes prog)),
    pid_global_config.state = \<lparr>
      global_state_impl.variables = init_valuation_impl (program.global_vars prog)
    \<rparr>
  \<rparr>"

lemma (in cprog) pid_init_gc_impl_impl:
  "pid_init_gc_impl_impl prog (comp_info_of prog) = pid_init_gc_impl"
  unfolding pid_init_gc_impl_impl_def pid_init_gc_impl_def
  by (simp add: init_pc_impl_impl)

definition "ccfg_V0_impl prog mst \<equiv> map (comp_\<gamma>_impl mst) (cfg_V0_list prog)"

lemma (in cprog) ccfg_V0_impl: "ccfg_V0_impl prog (comp_info_of prog) = cfgc_V0_list"
  unfolding ccfg_V0_impl_def cfgc_V0_list_def
  by (simp add: comp_\<gamma>_impl)

definition "ccfg_G_impl_impl prog mst \<equiv>
  \<lparr> gi_V = \<lambda> _. True, gi_E = ccfg_E_succ_impl mst, gi_V0 = ccfg_V0_impl prog mst \<rparr>"

lemma (in cprog) ccfg_G_impl_impl: "ccfg_G_impl_impl prog (comp_info_of prog) = cfgc_G_impl"
  unfolding ccfg_G_impl_impl_def cfgc_G_impl_def
  unfolding ccfg_E_succ_impl ccfg_V0_impl
  by rule

definition "is_vis_edge_impl mst is_vis_var \<equiv> \<lambda>(c,c').
  \<exists>(a,cc')\<in>set (ccfg_succ_impl mst c). c'=cc' \<and> (\<exists>v\<in>write_globals a. is_vis_var v)"

lemma (in cprog) is_vis_edge_impl: "is_vis_edge_impl (comp_info_of prog) = is_vis_edge"
  apply (intro ext)
  unfolding is_vis_edge_impl_def is_vis_edge_def
  by (simp add: ccfg_succ_impl)

definition "ga_gample_mil4_impl mst mem sticky_Ei (gc::pid_global_config_impl) = (
  let
    lcs = pid_global_config.processes gc;
    gs = pid_global_config.state gc
  in
    collecti_index_list (\<lambda>_ lc. let
        c = local_config.command lc;
        ls = local_config.state lc;
        as = ccfg_succ_impl mst c;
        s = filter (la_en'_impl (ls,gs) o fst) as;
        ample = s\<noteq>[]
        \<and> (\<forall>(a,_)\<in>set as. read_globals a = {} \<and> write_globals a = {})
        \<and> (\<forall>(a,c')\<in>set s. \<not>mem (c,c') sticky_Ei)
      in
        (ample,map (Pair c) s)
    ) lcs
)"

lemma (in cprog) ga_gample_mil4_impl: "ga_gample_mil4_impl (comp_info_of prog) = ga_gample_mil4"
  apply (intro ext)
  unfolding ga_gample_mil4_impl_def ga_gample_mil4_def
  by (simp add: ccfg_succ_impl)

definition "cr_ample_impl4_impl prog mst is_vis_var \<equiv>
  let sticky = find_fas_init_code (=) bounded_hashcode_nat
       (def_hashmap_size TYPE(nat)) (ccfg_G_impl_impl prog mst)
       (is_vis_edge_impl mst is_vis_var)
  in stutter_extend_en_list (ga_gample_mil4_impl mst (\<lambda>x f. f x) sticky)"

lemma (in cprog) cr_ample_impl4_impl: "cr_ample_impl4_impl prog (comp_info_of prog) = cr_ample_impl4"
  apply (intro ext)
  unfolding cr_ample_impl4_impl_def cr_ample_impl4_def
  by (simp add: ga_gample_mil4_impl ccfg_G_impl_impl is_vis_edge_impl)

definition "impl4_succ_impl prog mst is_vis_var
    \<equiv> succ_of_enex_list (cr_ample_impl4_impl prog mst is_vis_var,ga_ex_impl)"

lemma (in cprog) impl4_succ_impl:
  "impl4_succ_impl prog (comp_info_of prog) = impl4_succ"
  apply (intro ext)
  unfolding impl4_succ_impl_def impl4_succ_def
  by (simp add: cr_ample_impl4_impl)

definition "ample_step_impl4_impl prog mst is_vis_var
  \<equiv> rel_of_enex_list (cr_ample_impl4_impl prog mst is_vis_var,ga_ex_impl)"

lemma (in cprog) ample_step_impl4_impl:
  "ample_step_impl4_impl prog (comp_info_of prog) = ample_step_impl4"
  apply (intro ext)
  unfolding ample_step_impl4_impl_def ample_step_impl4_def
  by (simp add: cr_ample_impl4_impl)

export_code impl4_succ_impl pid_init_gc_impl_impl comp_info_of checking SML

end

repo: PSL


(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

theory Deterministic_AC
imports
  "AInvs.ArchDetSchedSchedule_AI"
begin

(*This theory defines an abstract "integrity" property over
  the extensible specification that the deterministic specification
  is shown to preserve. Essentially it demonstrates that the only
  elements altered in the cdt_list are the given parameters and
  their descendants. *)

(* Analagous to the Control edges that pas_refined imposes. *)
definition all_children where
"all_children P m \<equiv> (\<forall>c p. m c = Some p \<longrightarrow> P p \<longrightarrow> P c)"

primrec list_filter :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list" where
  "list_filter [] P = []" |
  "list_filter (x # xs) P = (if (P x) then (list_filter xs P)
                             else x # (list_filter xs P))"

abbreviation
"filtered_eq P list list' \<equiv> list_filter list P = list_filter list' P"

lemma list_filter_distr[simp]: "list_filter (list @ list') P = (list_filter list P) @ (list_filter list' P)"
  apply (induct list,simp+)
  done

lemma list_filter_empty[simp]: "\<forall>x \<in> set list. P x \<Longrightarrow> list_filter list P = []"
  apply (induct list,simp+)
  done

lemma list_filter_replace_list: "\<forall>x \<in> set list'. P x \<Longrightarrow> P a \<Longrightarrow>
 filtered_eq P (list_replace_list list a list') list"
  apply (induct list,simp+)
  done

lemma list_filter_insert_after: "P b \<Longrightarrow>
 filtered_eq P (list_insert_after list a b) list"
  apply (induct list,simp+)
  done

lemma list_filter_swap: "P b \<Longrightarrow> P a \<Longrightarrow>
 filtered_eq P (list_swap list a b) list"
  apply (induct list,(simp add: list_swap_def)+)
  done

lemma list_filter_replace: "P b \<Longrightarrow> P a \<Longrightarrow>
 filtered_eq P (list_replace list a b) list"
  apply (induct list,(simp add: list_replace_def)+)
  done

lemma list_filter_remove: "P a \<Longrightarrow>
 filtered_eq P (list_remove list a) list"
  apply (induct list,simp+)
  done

(* Here P is meant to decide whether a cslot_ptr is part of the current
   subject. Integrity is said to hold of two cdt_lists if either an
   entry is part of the current subject, or their lists are equivalent
   with all entries from the current subject removed.

   We use this to reason that changes to a non-subject entry are only allowed
   if that entry's list contains a child that is part of the current subject.
   It is stated in this way so that the property can be shown to be transitive.*)

definition list_integ where
"list_integ P t t' \<equiv>  \<forall>x. P x \<or> (filtered_eq P (cdt_list t x) (cdt_list t' x))"

lemmas list_integI = list_integ_def[THEN meta_eq_to_obj_eq,THEN iffD2,rule_format]
lemma list_integE:
  assumes hyp: "list_integ P t t'"
  obtains "P x" | "(filtered_eq P (cdt_list t x) (cdt_list t' x))"
  using hyp list_integ_def by blast

lemma update_cdt_list_wp:
  "\<lbrace>(\<lambda>s. P (s\<lparr>cdt_list := f (cdt_list s)\<rparr>))\<rbrace> update_cdt_list f \<lbrace>\<lambda>_.P\<rbrace>"
  apply (simp add: update_cdt_list_def set_cdt_list_def)
  apply wp
  done

lemma cap_move_list_integrity:
  notes split_paired_All[simp del]
  shows
  "\<lbrace>list_integ P st and K(P src) and K(P dest)\<rbrace> cap_move_ext src dest src_p dest_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>"
  apply (simp add: cap_move_ext_def split del: if_split)
  apply (wp update_cdt_list_wp)
  apply (intro impI conjI allI | simp add: list_filter_replace list_filter_remove split: option.splits | elim conjE | simp add: list_integ_def)+
  done

lemma cap_insert_list_integrity:
  notes split_paired_All[simp del]
  shows
  "\<lbrace>list_integ P st and K(P dest)\<rbrace> cap_insert_ext src_parent src dest src_p dest_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>"
  apply (simp add: cap_insert_ext_def split del: if_split)
  apply (wp update_cdt_list_wp)
  by (intro impI conjI allI |
      simp add: list_filter_insert_after list_filter_remove split: option.splits |
      elim conjE | simp add: list_integ_def)+

lemma create_cap_list_integrity:
  notes split_paired_All[simp del]
  shows
  "\<lbrace>list_integ P st and K(P dest)\<rbrace> create_cap_ext untyped dest dest_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>"
  apply (simp add: create_cap_ext_def split del: if_split)
  apply (wp update_cdt_list_wp)
  by (intro impI conjI allI |
      simp add: list_filter_replace list_filter_remove split: option.splits |
      elim conjE | simp add: list_integ_def)+

lemma empty_slot_list_integrity:
  notes split_paired_All[simp del]
  shows
  "\<lbrace>list_integ P st and (\<lambda>s. valid_list_2 (cdt_list s) m) and K(P slot) and K( all_children P m)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>"
  apply (simp add: empty_slot_ext_def split del: if_split)
  apply (wp update_cdt_list_wp)
  apply (intro impI conjI allI | simp add: list_filter_replace_list list_filter_remove split: option.splits | elim conjE  | simp add: list_integ_def)+
  apply (drule_tac x="the slot_p" in spec)
  apply (elim disjE)
   apply (simp add: all_children_def valid_list_2_def list_filter_replace_list)+
  done

lemma cap_swap_list_integrity:
  notes split_paired_All[simp del]
  shows
  "\<lbrace>list_integ P st and K(P slot1) and K(P slot2)\<rbrace> cap_swap_ext slot1 slot2 slot1_p slot2_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>"
  apply (simp add: cap_swap_ext_def split del: if_split)
  apply (wp update_cdt_list_wp)
  by (intro impI conjI allI |
      simp add: list_filter_replace list_filter_swap split: option.splits |
      elim conjE | simp add: list_integ_def)+ (* slow *)

lemma null_filter: "\<forall>x \<in> set list. \<not> P x \<Longrightarrow> list_filter list P = list"
  apply (induct list,simp+)
  done

lemma neq_filtered_ex: "list \<noteq> list' \<Longrightarrow> filtered_eq P list list' \<Longrightarrow> \<exists>x \<in> set list \<union> set list'. P x"
  apply (rule ccontr)
  apply (simp add: null_filter)
  done

lemma weaken_filter: "(\<forall>s. P s \<longrightarrow> T s) \<Longrightarrow> filtered_eq T (list_filter list P) list"
  apply (induct list,simp+)
  done

lemmas weaken_filter' = weaken_filter[rule_format,rotated]

lemma weaken_filter_eq: "(\<forall>s. P s \<longrightarrow> T s) \<Longrightarrow> filtered_eq P list list' \<Longrightarrow> filtered_eq T list list'"
  apply (subst weaken_filter[symmetric],assumption)
  apply (simp add: weaken_filter)
  done

lemmas weaken_filter_eq' = weaken_filter_eq[rule_format,rotated]

end


text:
theory Successor
  imports SetCombinators
begin

context GZF begin

subsection \<open>Set Concatenation\<close>

definition cons :: "['a, 'a] \<Rightarrow> 'a"
  where "cons b x \<equiv> {b} \<union> x"

lemma cons_typ : "cons : SetMem \<rightarrow> Set \<rightarrow> Set"
  unfolding cons_def
  by (rule funI[OF funI], rule un_set, rule sng_set)

lemmas cons_set = funE[OF funE[OF cons_typ]]

lemma cons_iff :
  assumes b:"b : SetMem" and x:"x : Set"
    shows "c \<in> cons b x \<longleftrightarrow> (c = b \<or> c \<in> x)"
  unfolding cons_def un_iff[OF sng_set[OF b] x] sng_iff[OF b]
  by (rule)

lemma consI1 :
  assumes b:"b : SetMem" and x:"x : Set"
    shows "b \<in> cons b x"
  using cons_iff[OF b x] by simp

lemma consI2 :
  assumes b:"b : SetMem" and x:"x : Set"
     and c:"c \<in> x"
   shows "c \<in> cons b x"
  using cons_iff[OF b x] c by simp

(*Classical introduction rule*)
lemma consCI :
  assumes b:"b : SetMem" and x:"x : Set"
     and c:"c \<notin> x \<Longrightarrow> c = b"
   shows "c \<in> cons b x"
  using cons_iff[OF b x] c by auto

lemma consE :
  assumes b:"b : SetMem" and x:"x : Set"
      and c:"c \<in> cons b x"
  obtains "c = b" | "c \<in> x"
  using cons_iff[OF b x] c by auto

(*Stronger version of \<open>consE\<close>*)
lemma consE' :
  assumes b:"b : SetMem" and x:"x : Set"
      and c:"c \<in> cons b x"
  obtains "c = b" | "c \<in> x" "c \<noteq> b"
  using cons_iff[OF b x] c by auto

lemma cons_not_emp :
  assumes b:"b : SetMem" and x:"x : Set"
    shows "cons b x \<noteq> \<emptyset>"
  by (rule not_emptyI[OF consI1[OF b x]])

subsection \<open>Unique existence of von Neumann successor operation\<close>

lemmas succ_set = funE[OF Succ_typ]

subsection \<open>Rules for von Neumann successor operation\<close>

lemma vsucc_iff :
  assumes x:"x : Set"
    shows "y \<in> Succ x \<longleftrightarrow> (y \<in> x \<or> y = x)"
  using succ x
  by auto

lemma vsuccI1 :
  assumes "x : Set"
    shows "y \<in> x \<Longrightarrow> y \<in> Succ x"
  using vsucc_iff[OF assms] by simp

lemma vsuccI2 :
  assumes "x : Set"
    shows "x \<in> Succ x"
  using vsucc_iff[OF assms] by simp

lemma vsuccE :
  assumes "x : Set"
    shows "y \<in> Succ x \<Longrightarrow> (y \<in> x \<or> y = x)"
  using vsucc_iff[OF assms] by simp

end
end

author: ultra-group

repo: isabelle-gst


text:
theory Model_Theory
imports "../basic_theory/Entailment" Proof_System
begin

section \<open>Decidability, Model-Theoretical\<close>
text \<open>This section contains proofs from the corresponding section 3 in \cite{JoshBerdine.2004} about
      decidability, soundness and completeness.\<close>

text \<open>Entailments without ls in the antecedent are decidable, cf. Lemma 3 \cite{JoshBerdine.2004}.\<close>
theorem entailment_decidable_simple: "\<And>\<Pi> \<Sigma> \<Pi>' \<Sigma>'. \<nexists>E\<^sub>1 E\<^sub>2. ls(E\<^sub>1,E\<^sub>2) \<in> set \<Sigma>
  \<Longrightarrow> \<Pi>\<bar>\<Sigma> \<turnstile> \<Pi>'\<bar>\<Sigma>' \<or> \<not>(\<Pi>\<bar>\<Sigma> \<turnstile> \<Pi>'\<bar>\<Sigma>')"
  unfolding entails_def by blast
(* I'm pretty sure that this is not how decidability would actually be formalized, yet I lack ideas
   of how this would be possible otherwise. I suppose pretty much every predicate defined in Isabelle
   is in fact decidable as it would otherwise not be accepted by the system.*)

subsection \<open>Proof of the above theorem as in \cite{JoshBerdine.2004}, A.2.\<close>
definition state_equiv :: "state \<Rightarrow> var set \<Rightarrow> state \<Rightarrow> bool" where
  "state_equiv sh X sh' \<equiv> \<exists>s h s' h'. sh = (s,h) \<and> sh' = (s',h') \<and> (\<exists>r. bij r \<and> r Nilval = Nilval
    \<and> (\<forall>x \<in> X. r (s x) = s' x) \<and> (\<forall>l l'. (l \<notin> dom h \<and> r (Val l) = Val l' \<and> l' \<notin> dom h')
      \<or> ((r (Val l))) = Val l' \<and> r (the (h l)) = the (h' l')))"
notation state_equiv ("_ \<approx>\<^sub>_ _" [60,61,61] 61)

text \<open>cf Lemma 19 in \cite{JoshBerdine.2004}, A.2\<close>
(* This lemma seems to be rather simple to prove yet very tedious.
   Therefore (and because I'm writing this on 2021-01-09), I will not finish it. *)
lemma "\<lbrakk>X=fv A; (s,h)\<approx>\<^sub>X(s',h')\<rbrakk> \<Longrightarrow> ((s,h)\<Turnstile>A) = ((s',h')\<Turnstile>A)"
proof
  assume X: "X=fv A"
  assume equiv: "(s,h)\<approx>\<^sub>X(s',h')"
  assume lhs: "(s,h)\<Turnstile>A"
  from lhs equiv X show "(s',h')\<Turnstile>A" proof (induction rule: sat_induct)
    case (EqSat e1 s e2 h)
    then obtain r where r: "(bij r \<and> r Nilval = Nilval
      \<and> (\<forall>x \<in> X. r (s x) = s' x) \<and> (\<forall>l l'. (l \<notin> dom h \<and> r (Val l) = Val l' \<and> l' \<notin> dom h')
        \<or> ((r (Val l))) = Val l' \<and> r (the (h l)) = the (h' l')))" using state_equiv_def by auto
    with EqSat.prems(2) have r_eq: "\<forall>x \<in> fv e1 \<union> fv e2. r (s x) = s' x" by simp
    show ?case proof (cases e1)
      case Nil
      hence e1_nil: "\<lbrakk>e1\<rbrakk>s' = Nilval" by simp
      from Nil have s_e1_nil: "\<lbrakk>e1\<rbrakk>s = Nilval" by simp
      then show ?thesis proof (cases e2)
        case Nil
        hence "\<lbrakk>e2\<rbrakk>s' = Nilval" by simp
        with e1_nil show ?thesis by fastforce
      next
        case (Var x2)
        with s_e1_nil EqSat.hyps have "s x2 = Nilval" by simp
        moreover with r_eq have "r (s x2) = s' x2" by (simp add: Var)
        ultimately have "\<lbrakk>e2\<rbrakk>s' = Nilval" using r Var by simp
        with e1_nil show ?thesis by fastforce
      qed
    next
      case (Var a)
      with r_eq have "r (s a) = s' a" by simp
      hence e1_eq: "\<lbrakk>e1\<rbrakk>s' = r (\<lbrakk>e1\<rbrakk>s)" using Var by simp
      then show ?thesis proof (cases e2)
        case Nil
        hence "\<lbrakk>e2\<rbrakk>s = Nilval" by simp
        with EqSat.hyps have "\<lbrakk>e1\<rbrakk>s = Nilval" by simp
        with e1_eq r have "\<lbrakk>e1\<rbrakk>s' = Nilval" by simp
        moreover from Nil have "\<lbrakk>e2\<rbrakk>s' = Nilval" by fastforce
        ultimately show ?thesis by fastforce
      next
        case (Var b)
        with r_eq have "r (s b) = s' b" by simp
        hence "\<lbrakk>e2\<rbrakk>s' = r (\<lbrakk>e2\<rbrakk>s)" using Var by simp
        with e1_eq EqSat.hyps show ?thesis by auto
      qed
    qed
  next
    case (NeqSat e1 s e2 h)
    then show ?case sorry
  next
    case (TrueSat s h)
    then show ?case sorry
  next
    case (ConjSat s h P \<Pi>)
    then show ?case sorry
  next
    case (PointsToSat e1 s v h e2)
    then show ?case sorry
  next
    case (EmpSat h s)
    then show ?case sorry
  next
    case (SepConjSat h1 h2 h s S \<Sigma>)
    then show ?case sorry
  next
    case (FormSat s h \<Pi> \<Sigma>)
    then show ?case sorry
  next
    case (LsSat s h n e1 e2)
    then show ?case sorry
  qed
next
  assume X: "X=fv A"
  assume equiv: "(s,h)\<approx>\<^sub>X(s',h')"
  assume rhs: "(s',h')\<Turnstile>A"
  show "(s,h)\<Turnstile>A" \<comment> \<open>Works pretty much the same as above, but one has to reverse r.\<close>
  sorry
qed
end

author: firefighterduck

repo: SepLogFrag