theory Ribbons_Completeness imports
  Ribbons_Graphical
begin

text {* We prove that the proof rules defined in ribbons_graphical.thy are complete with respect to the rules of separation logic defined in ribbons_basic.thy. *}

theorem completeness: 
  fixes p c q
  assumes "prov_triple (p,c,q)"
  shows "\<exists>G P Q. wf_dia G \<and> coms_dia G c \<and> p = ass P \<and> q = ass Q \<and> prov_dia G P Q" (is "\<exists>G P Q. ?\<Phi> G P Q")
proof -
  let ?V = "[v01,v02]"
  let ?\<Lambda> = "(\<lambda>v. Rib Emp) (v01 := Rib p, v02 := Rib q)"
  let ?E = "[([v01], Com c, [v02])]"
  let ?G = "Graph ?V ?\<Lambda> ?E"
  let ?P = "Emp_int \<otimes> Ribbon p"
  let ?Q = "Emp_int \<otimes> Ribbon q"
  let ?\<pi> = "[Inl v01, Inr ([v01], Com c, [v02]), Inl v02]"
  have "coms_dia ?G c"
  proof -
    have "coms_dia ?G (foldr (op ;;) [Skip, c, Skip] Skip)"
    proof (rule coms_main [where \<pi> = ?\<pi>])
      have yiecn: "distinct [Inl v01, Inr ([v01], Com c, [v02]), Inl v02]" by auto
      show "?\<pi> \<in> lins ?G"
      proof (unfold lins.simps[of ?V ?\<Lambda> ?E], intro CollectI conjI, simp)
        show "set [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] =
          Inl ` set [v01, v02] \<union> Inr ` set [([v01], Com c, [v02])]"
          by auto
      next
        show "\<forall>i j v e.
          i < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] \<and>
          j < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] \<and>
          [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! i = Inl v \<and>
          [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! j = Inr e \<and>
          v \<in> set (fst3 e) \<longrightarrow> i < j"
        proof (intro allI impI, elim conjE)
          fix i j v e
          assume 
            axvgk: "i < length ?\<pi>" and
            snuyc: "j < length ?\<pi>" and 
            bwrsk: "?\<pi> ! i = Inl v" and
            irnle: "?\<pi> ! j = Inr e" and  
            lpfbk: "v \<in> set (fst3 e)"
          from nth_in_set [OF snuyc irnle] have
            lsdkf: "e = ([v01], Com c, [v02])" by auto
          with lpfbk have cxtvo: "v = v01" unfolding fst3_def by auto
          have "i=0" 
          proof (rule ccontr)
            assume xiznn: "i \<noteq> 0"
            have gocuj: "0 < length ?\<pi>" by auto
            from distinct_conv_nth[of "?\<pi>"] yiecn have
              "\<And>i j.\<lbrakk> i<length ?\<pi> ; j<length ?\<pi> ; i \<noteq> j \<rbrakk> \<Longrightarrow> ?\<pi> ! i \<noteq> ?\<pi> ! j"
              by auto
            from this[OF axvgk gocuj xiznn] and bwrsk and cxtvo show 
              False by auto
          qed
          moreover have "j=1"
          proof (rule ccontr) 
            assume xiznn: "j \<noteq> 1"
            have gocuj: "1 < length ?\<pi>" by auto
            from distinct_conv_nth[of "?\<pi>"] yiecn have
              "\<And>i j.\<lbrakk> i<length ?\<pi> ; j<length ?\<pi> ; i \<noteq> j \<rbrakk> \<Longrightarrow> ?\<pi> ! i \<noteq> ?\<pi> ! j"
              by auto
            from this[OF snuyc gocuj xiznn] and irnle and lsdkf show
              False by auto
          qed
          ultimately show "i < j" by auto
        qed
      next
        show "\<forall>j k w e.
          j < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] \<and>
          k < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] \<and>
          [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! j = Inr e \<and>
          [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! k = Inl w \<and>
          w \<in> set (thd3 e) \<longrightarrow> j < k"
        proof (intro allI impI, elim conjE)
          fix j k w e
          assume 
            snuyc: "j < length ?\<pi>" and 
            rldms: "k < length ?\<pi>" and
            irnle: "?\<pi> ! j = Inr e" and 
            nthqn: "?\<pi> ! k = Inl w" and 
            hfmli: "w \<in> set (thd3 e)"
          from nth_in_set [OF snuyc irnle] have
            lsdkf: "e = ([v01], Com c, [v02])" by auto
          with hfmli have qtxuv: "w = v02" unfolding thd3_def by auto
          have "j=1"
          proof (rule ccontr) 
            assume xiznn: "j \<noteq> 1"
            have gocuj: "1 < length ?\<pi>" by auto
            from distinct_conv_nth[of "?\<pi>"] yiecn have
              "\<And>i j.\<lbrakk> i<length ?\<pi> ; j<length ?\<pi> ; i \<noteq> j \<rbrakk> \<Longrightarrow> ?\<pi> ! i \<noteq> ?\<pi> ! j"
              by auto
            from this[OF snuyc gocuj xiznn] and irnle and lsdkf show
              False by auto
          qed
          moreover have "k=2"
          proof (rule ccontr)
            assume xiznn: "k \<noteq> 2"
            have gocuj: "2 < length ?\<pi>" by auto
            from distinct_conv_nth[of "?\<pi>"] yiecn have
              "\<And>i j.\<lbrakk> i<length ?\<pi> ; j<length ?\<pi> ; i \<noteq> j \<rbrakk> \<Longrightarrow> ?\<pi> ! i \<noteq> ?\<pi> ! j"
              by auto
            from this[OF rldms gocuj xiznn] and nthqn and qtxuv show 
              False by auto
          qed
          ultimately show "j < k" by auto
        qed 
      qed
    next
      show "length [Skip, c, Skip] =
        length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02]"
        by auto
    next
      fix i
      assume 
        ukhof: "i < length ?\<pi>" and
        wfzta: "\<exists>v. ?\<pi> ! i = Inl v"
      have "i = 0 \<or> i = 2"
      proof (rule ccontr)
        assume "\<not> (i = 0 \<or> i = 2)"
        with ukhof have "i=1" by auto
        hence "?\<pi> ! i = Inr ([v01], Com c, [v02])" by auto
        with wfzta show False by auto
      qed
      hence "(?\<pi> ! i = Inl v01) \<or> (?\<pi> ! i = Inl v02)"
        and "[Skip, c, Skip] ! i = Skip" by auto
      moreover have "coms_ass (Rib p) Skip" and
        "coms_ass (Rib q) Skip" using coms_skip by auto
      ultimately show 
        "coms_ass (?\<Lambda> (Sum_Type.Projl (?\<pi> ! i))) ([Skip, c, Skip] ! i)"
        by auto
    next
      fix i
      assume 
        ukhof: "i < length ?\<pi>" and
        wfzta: "\<exists>e. ?\<pi> ! i = Inr e"
      have "i = 1"
      proof (rule ccontr)
        assume "\<not> (i = 1)"
        with ukhof have "i=0 \<or> i=2" by auto
        hence "?\<pi> ! i = Inl v01 \<or> ?\<pi> ! i = Inl v02" by auto
        with wfzta show False by auto
      qed
      hence ncdef: "?\<pi> ! i = Inr ([v01], Com c, [v02])" 
        and "[Skip, c, Skip] ! i = c" by auto
      moreover have "coms_com (Com c) c" using coms_basic by auto
      ultimately show
        "coms_com (snd3 (Sum_Type.Projr (?\<pi> ! i))) 
        ([Skip, c, Skip] ! i)"
        unfolding ncdef unfolding snd3_def by auto
    qed
    moreover have
      "c = foldr (op ;;) [Skip, c, Skip] Skip" 
      using seq_skip skip_seq by auto
    ultimately show "coms_dia ?G c" by auto
  qed
  moreover have "p = ass ?P" and "q = ass ?Q" 
    by (auto simp add: emp_star)
  moreover have bivui: "wf_dia ?G" 
  proof
    show "acyclicity ?E" 
      by (unfold acyclicity_def, auto simp add: fst3_def thd3_def, unfold acyclic_def, auto)
  next
    show "linearity ?E" by (unfold linearity_def, auto)
  qed (auto simp add: fst3_def thd3_def)
  moreover have "prov_dia ?G ?P ?Q"
  proof -
    have "?P = top_dia ?G" by (auto simp add: fst3_def thd3_def)
    moreover have "?Q = bot_dia ?G" by (auto simp add: fst3_def thd3_def)    
    moreover have "prov_dia ?G (top_dia ?G) (bot_dia ?G)"
      by (rule Main, auto simp add: Skip Basic emp_star assms fst3_def snd3_def thd3_def bivui)
    ultimately show "prov_dia ?G ?P ?Q" by auto
  qed  
  ultimately show "\<exists>G P Q. wf_dia G \<and> coms_dia G c \<and> p = ass P \<and> q = ass Q \<and> prov_dia G P Q" 
    using exI3[of "?\<Phi>" "?G" "?P" "?Q"] by auto
qed

end