Theory Computation

theory Computation imports Main begin

definition etran :: "(('p×'s) × ('p×'s)) set" where
  "etran ≡ {(c,c'). fst c = fst c'}"

declare etran_def[simp]

definition etran_p :: ‹('p×'s) ⇒ ('p×'s) ⇒ bool› ("_ ─e→ _" [81,81] 80)
  where ‹etran_p c c' ≡ (c,c') ∈ etran›

declare etran_p_def[simp]

inductive_set cpts :: ‹(('p×'s) × ('p×'s)) set ⇒ ('p×'s) list set›
  for tran :: "(('p×'s) × ('p×'s)) set" where
    CptsOne[intro]: "[(P,s)] ∈ cpts tran" |
    CptsEnv[intro]: "(P,t)#cs ∈ cpts tran ⟹ (P,s)#(P,t)#cs ∈ cpts tran" |
    CptsComp: "⟦ ((P,s),(Q,t)) ∈ tran; (Q,t)#cs ∈ cpts tran ⟧ ⟹ (P,s)#(Q,t)#cs ∈ cpts tran"

lemma cpts_snoc_env:
  assumes h: "cpt ∈ cpts tran"
  assumes tran: ‹last cpt ─e→ c›
  shows ‹cpt@[c] ∈ cpts tran›
  using h tran
proof(induct)
  case (CptsOne P s)
  then have ‹fst c = P› by simp
  then show ?case
    apply(subst surjective_pairing[of c])
    apply(erule ssubst)
    apply simp
    apply(rule CptsEnv)
    apply(rule cpts.CptsOne)
    done
next
  case (CptsEnv P t cs s)
  then have ‹last ((P, t) # cs) ─e→ c› by simp
  with CptsEnv(2) have ‹((P, t) # cs) @ [c] ∈ cpts tran› by blast
  then show ?case using cpts.CptsEnv by fastforce
next
  case (CptsComp P s Q t cs)
  then have ‹((Q, t) # cs) @ [c] ∈ cpts tran› by fastforce
  with CptsComp(1) show ?case using cpts.CptsComp by fastforce
qed

lemma cpts_snoc_comp:
  assumes h: "cpt ∈ cpts tran"
  assumes tran: ‹(last cpt, c) ∈ tran›
  shows ‹cpt@[c] ∈ cpts tran›
  using h tran
proof(induct)
  case (CptsOne P s)
  then show ?case apply simp
    apply(subst (asm) surjective_pairing[of c])
    apply(subst surjective_pairing[of c])
    apply(rule CptsComp)
     apply simp
    apply(rule cpts.CptsOne)
    done
next
  case (CptsEnv P t cs s)
  then have ‹((P, t) # cs) @ [c] ∈ cpts tran› by fastforce
  then show ?case using cpts.CptsEnv by fastforce
next
  case (CptsComp P s Q t cs)
  then have ‹((Q, t) # cs) @ [c] ∈ cpts tran› by fastforce
  with CptsComp(1) show ?case using cpts.CptsComp by fastforce
qed

lemma cpts_nonnil:
  assumes h: ‹cpt ∈ cpts tran›
  shows ‹cpt ≠ []›
  using h by (induct; simp)

lemma cpts_def': ‹cpt ∈ cpts tran ⟷ cpt ≠ [] ∧ (∀i. Suc i < length cpt ⟶ (cpt!i, cpt!Suc i) ∈ tran ∨ cpt!i ─e→ cpt!Suc i)›
proof
  assume cpt: ‹cpt ∈ cpts tran›
  show ‹cpt ≠ [] ∧ (∀i. Suc i < length cpt ⟶ (cpt!i, cpt!Suc i) ∈ tran ∨ cpt!i ─e→ cpt!Suc i)›
  proof
    show ‹cpt ≠ []› by (rule cpts_nonnil[OF cpt])
  next
    show ‹∀i. Suc i < length cpt ⟶ (cpt!i, cpt!Suc i) ∈ tran ∨ cpt!i ─e→ cpt!Suc i›
    proof
      fix i
      show ‹Suc i < length cpt ⟶ (cpt!i, cpt!Suc i) ∈ tran ∨ cpt!i ─e→ cpt!Suc i›
      proof
        assume i_lt: ‹Suc i < length cpt›
        show ‹(cpt!i, cpt!Suc i) ∈ tran ∨ cpt!i ─e→ cpt!Suc i›
          using cpt i_lt
        proof(induct arbitrary:i)
          case (CptsOne P s)
          then show ?case by simp
        next
          case (CptsEnv P t cs s)
          show ?case
          proof(cases i)
            case 0
            then show ?thesis apply-
              apply(rule disjI2)
              apply(erule ssubst)
              apply simp
              done
          next
            case (Suc i')
            then show ?thesis using CptsEnv(2)[of i'] CptsEnv(3) by force
          qed
        next
          case (CptsComp P s Q t cs)
          show ?case
          proof(cases i)
            case 0
            then show ?thesis apply-
              apply(rule disjI1)
              apply(erule ssubst)
              apply simp
              by (rule CptsComp(1))
          next
            case (Suc i')
            then show ?thesis using CptsComp(3)[of i'] CptsComp(4) by force
          qed
        qed
      qed
    qed
  qed
next
  assume h: ‹cpt ≠ [] ∧ (∀i. Suc i < length cpt ⟶ (cpt!i, cpt!Suc i) ∈ tran ∨ cpt!i ─e→ cpt!Suc i)›
  from h have cpt_nonnil: ‹cpt ≠ []› by (rule conjunct1)
  from h have ct_et: ‹∀i. Suc i < length cpt ⟶ (cpt!i, cpt!Suc i) ∈ tran ∨ cpt!i ─e→ cpt!Suc i› by (rule conjunct2)
  show ‹cpt ∈ cpts tran› using cpt_nonnil ct_et
  proof(induct cpt)
    case Nil
    then show ?case by simp
  next
    case (Cons c cs)
    have IH: ‹cs ≠ [] ⟹ ∀i. Suc i < length cs ⟶ (cs ! i, cs ! Suc i) ∈ tran ∨ cs ! i ─e→ cs ! Suc i ⟹ cs ∈ cpts tran›
      by (rule Cons(1))
    have ct_et': ‹∀i. Suc i < length (c # cs) ⟶ ((c # cs) ! i, (c # cs) ! Suc i) ∈ tran ∨ (c # cs) ! i ─e→ (c # cs) ! Suc i›
      by (rule Cons(3))
    show ?case
    proof(cases cs)
      case Nil
      then show ?thesis apply-
        apply(erule ssubst)
        apply(subst surjective_pairing[of c])
        by (rule CptsOne)
    next
      case (Cons c' cs')
      then have ‹cs ≠ []› by simp
      moreover have ‹∀i. Suc i < length cs ⟶ (cs ! i, cs ! Suc i) ∈ tran ∨ cs ! i ─e→ cs ! Suc i›
        using ct_et' by auto
      ultimately have cs_cpts: ‹cs ∈ cpts tran› using IH by fast
      show ?thesis apply (rule ct_et'[THEN allE, of 0])
        apply(simp add: Cons)
      proof-
        assume ‹(c, c') ∈ tran ∨ fst c = fst c'›
        then show ‹c # c' # cs' ∈ cpts tran›
        proof
          assume h: ‹(c, c') ∈ tran›
          show ‹c # c' # cs' ∈ cpts tran›
            apply(subst surjective_pairing[of c])
            apply(subst surjective_pairing[of c'])
            apply(rule CptsComp)
             apply simp
             apply (rule h)
            using cs_cpts by (simp add: Cons)
        next
          assume h: ‹fst c = fst c'›
          show ‹c # c' # cs' ∈ cpts tran›
            apply(subst surjective_pairing[of c])
            apply(subst surjective_pairing[of c'])
            apply(subst h)
            apply(rule CptsEnv)
            apply simp
            using cs_cpts by (simp add: Cons)
        qed
      qed
    qed
  qed
qed

lemma cpts_tran:
  ‹cpt ∈ cpts tran ⟹
   ∀i. Suc i < length cpt ⟶
   (cpt!i, cpt!Suc i) ∈ tran ∨ cpt!i ─e→ cpt!Suc i›
  using cpts_def' by blast

definition cpts_from :: ‹(('p×'s) × ('p×'s)) set ⇒ ('p×'s) ⇒ ('p×'s) list set› where
  "cpts_from tran c0 ≡ {cpt. cpt ∈ cpts tran ∧ hd cpt = c0}"

declare cpts_from_def[simp]

lemma cpts_from_def':
  "cpt ∈ cpts_from tran c0 ⟷ cpt ∈ cpts tran ∧ hd cpt = c0" by simp

definition cpts_from_ctran_only :: ‹(('p×'s) × ('p×'s)) set ⇒ ('p×'s) ⇒ ('p×'s) list set› where
  "cpts_from_ctran_only tran c0 ≡ {cpt. cpt ∈ cpts_from tran c0 ∧ (∀i. Suc i < length cpt ⟶ (cpt!i, cpt!Suc i) ∈ tran)}"

lemma cpts_tl':
  assumes h: ‹cpt ∈ cpts tran›
    and cpt: ‹cpt = c0#c1#cs›
  shows "c1#cs ∈ cpts tran"
  using h cpt apply- apply(erule cpts.cases, auto) done

lemma cpts_tl:
  ‹cpt ∈ cpts tran ⟹ tl cpt ≠ [] ⟹ tl cpt ∈ cpts tran›
  using cpts_tl' by (metis cpts_nonnil list.exhaust_sel)

lemma cpts_from_tl:
  assumes h: ‹cpt ∈ cpts_from tran (P,s)›
    and cpt: ‹cpt = (P,s)#(P,t)#cs›
  shows "(P,t)#cs ∈ cpts_from tran (P,t)"
proof-
  from h have "cpt ∈ cpts tran" by simp
  with cpt show ?thesis apply- apply(erule cpts.cases, auto) done
qed

lemma cpts_drop:
  assumes h: "cpt ∈ cpts tran"
    and i: "i < length cpt"
  shows "drop i cpt ∈ cpts tran"
  using i
proof(induct i)
  case 0
  then show ?case using h by simp
next
  case (Suc i')
  then show ?case
  proof-
    assume h1: ‹i' < length cpt ⟹ drop i' cpt ∈ cpts tran›
    assume h2: ‹(Suc i') < length cpt›
    with h1 have ‹drop i' cpt ∈ cpts tran› by fastforce
    let ?cpt' = ‹drop i' cpt›
    have ‹drop (Suc i') cpt = tl ?cpt'›
      by (simp add: drop_Suc drop_tl)
    with h2 have ‹tl ?cpt' ≠ []› by auto
    then show ‹drop (Suc i') cpt ∈ cpts tran› using cpts_tl[of ?cpt']
      by (simp add: ‹drop (Suc i') cpt = tl (drop i' cpt)› ‹drop i' cpt ∈ cpts tran› cpts_tl)
  qed
qed

lemma cpts_take':
  assumes h: "cpt ∈ cpts tran"
  shows "take (Suc i) cpt ∈ cpts tran"
  using h
proof(induct i)
  case 0
  have "[(fst (hd cpt), snd (hd cpt))] ∈ cpts tran" using CptsOne by fast
  then show ?case
    using "0.prems" cpts_def' by fastforce
next
  case (Suc i)
  then have cpt': ‹take (Suc i) cpt ∈ cpts tran› by blast
  let ?cpt' = "take (Suc i) cpt"
  show ?case
  proof(cases ‹Suc i < length cpt›)
    case True
    with cpts_drop have drop_i: ‹drop i cpt ∈ cpts tran›
      using Suc_lessD h by blast
    have ‹?cpt' @ [cpt!Suc i] ∈ cpts tran› using drop_i
    proof(cases)
      case (CptsOne P s)
      then show ?thesis using h
        by (metis Cons_nth_drop_Suc Suc_lessD True append.right_neutral append_eq_append_conv append_take_drop_id list.simps(3) nth_via_drop take_Suc_conv_app_nth)
    next
      case (CptsEnv P t cs s)
      then show ?thesis apply-
        apply(rule cpts_snoc_env)
        apply(rule cpt')
      proof-
        assume h1: ‹drop i cpt = (P, s) # (P, t) # cs›
        assume h2: ‹(P, t) # cs ∈ cpts tran›
        from h1 h2 have ‹last (take (Suc i) cpt) = (P, s)›
          by (metis Suc_lessD True hd_drop_conv_nth list.sel(1) snoc_eq_iff_butlast take_Suc_conv_app_nth)
        moreover from h1 h2 have "cpt!Suc i = (P,t)"
          by (metis Cons_nth_drop_Suc Suc_lessD True list.sel(1) list.sel(3))
        ultimately show ‹last (take (Suc i) cpt) ─e→ cpt ! Suc i› by force
      qed
    next
      case (CptsComp P s Q t cs)
      then show ?thesis apply-
        apply(rule cpts_snoc_comp)
         apply(rule cpt')
      proof-
        assume h1: ‹drop i cpt = (P, s) # (Q, t) # cs›
        assume h2: ‹(Q, t) # cs ∈ cpts tran›
        assume h3: ‹((P, s), (Q, t)) ∈ tran›
        from h1 h2 have ‹last (take (Suc i) cpt) = (P, s)›
          by (metis Suc_lessD True hd_drop_conv_nth list.sel(1) snoc_eq_iff_butlast take_Suc_conv_app_nth)
        moreover from h1 h2 have "cpt!Suc i = (Q,t)"
          by (metis Cons_nth_drop_Suc Suc_lessD True list.sel(1) list.sel(3))
        ultimately show ‹(last (take (Suc i) cpt), cpt ! Suc i) ∈ tran› using h3 by simp
      qed
    qed
    with True show ?thesis
      by (simp add: take_Suc_conv_app_nth)
  next
    case False
    then show ?thesis using cpt' by simp
  qed
qed

lemma cpts_take:
  assumes h: "cpt ∈ cpts tran"
  assumes i: "i ≠ 0"
  shows "take i cpt ∈ cpts tran"
proof-
  from i obtain i' where ‹i = Suc i'› using not0_implies_Suc by blast
  with h cpts_take' show ?thesis by blast
qed

lemma cpts_from_take:
  assumes h: "cpt ∈ cpts_from tran c"
  assumes i: "i ≠ 0"
  shows "take i cpt ∈ cpts_from tran c"
  apply simp
proof
  from h have "cpt ∈ cpts tran" by simp
  with i cpts_take show ‹take i cpt ∈ cpts tran› by blast
next
  from h have "hd cpt = c" by simp
  with i show ‹hd (take i cpt) = c› by simp
qed

type_synonym 'a tran = ‹'a × 'a›

lemma cpts_prepend:
  ‹[c0,c1]∈cpts tran ⟹ c1#cs ∈ cpts tran ⟹ c0#c1#cs ∈ cpts tran›
  apply(erule cpts.cases, auto)
  apply(rule CptsComp, auto)
  done

lemma all_etran_same_prog:
  assumes all_etran: ‹∀i. Suc i < length cpt ⟶ cpt!i ─e→ cpt!Suc i›
    and fst_hd_cpt: ‹fst (hd cpt) = P›
    and ‹cpt≠[]›
  shows ‹∀i<length cpt. fst (cpt!i) = P›
proof
  fix i
  show ‹i < length cpt ⟶ fst (cpt ! i) = P›
  proof(induct i)
    case 0
    then show ?case
      apply(rule impI)
      apply(subst hd_conv_nth[THEN sym])
       apply(rule ‹cpt≠[]›)
      apply(rule fst_hd_cpt)
      done
  next
    case (Suc i)
    have 1: "Suc i < length cpt ⟶ cpt ! i ─e→ cpt ! Suc i"
      by (rule all_etran[THEN spec[where x=i]])
    show ?case
    proof
      assume Suc_i_lt: ‹Suc i < length cpt›
      with 1 have ‹cpt ! i ─e→ cpt ! Suc i› by blast
      moreover from Suc Suc_i_lt[THEN Suc_lessD] have ‹fst (cpt ! i) = P› by blast
      ultimately show ‹fst (cpt ! Suc i) = P› by simp
    qed
  qed
qed

lemma cpts_append_comp:
  ‹cs1 ∈ cpts tran ⟹ cs2 ∈ cpts tran ⟹ (last cs1, hd cs2) ∈ tran ⟹ cs1@cs2 ∈ cpts tran›
proof-
  assume c1: ‹cs1∈cpts tran›
  assume c2: ‹cs2∈cpts tran›
  assume tran: ‹(last cs1, hd cs2) ∈ tran›
  show ?thesis using c1 tran
  proof(induct)
    case (CptsOne P s)
    then show ?case
      apply simp
      apply(cases cs2)
      using cpts_nonnil c2 apply fast
      apply simp
      apply(rename_tac c cs)
      apply(subst surjective_pairing[of c])
      apply(rule CptsComp)
       apply simp
      using c2 by simp
  next
    case (CptsEnv P t cs s)
    then show ?case
      apply simp
      apply(rule cpts.CptsEnv)
      by simp
  next
    case (CptsComp P s Q t cs)
    then show ?case
      apply simp
      apply(rule cpts.CptsComp)
      apply blast
      by blast
  qed
qed

lemma cpts_append_env:
  assumes c1: ‹cs1∈cpts tran› and c2: ‹cs2∈cpts tran›
    and etran: ‹fst (last cs1) = fst (hd cs2)›
  shows ‹cs1@cs2 ∈ cpts tran›
  using c1 etran
proof(induct)
  case (CptsOne P s)
  then show ?case
    apply simp
    apply(subst hd_Cons_tl[OF cpts_nonnil[OF c2], symmetric]) back
    apply(subst surjective_pairing[of ‹hd cs2›]) back
    apply(rule CptsEnv)
    using hd_Cons_tl[OF cpts_nonnil[OF c2]] c2 by simp
next
  case (CptsEnv P t cs s)
  then show ?case
    apply simp
    apply(rule cpts.CptsEnv)
    by simp
next
  case (CptsComp P s Q t cs)
  then show ?case
    apply simp
    apply(rule cpts.CptsComp)
     apply blast
    by blast
qed

lemma cpts_remove_last:
  assumes ‹c#cs@[c'] ∈ cpts tran›
  shows ‹c#cs ∈ cpts tran›
proof-
  from assms cpts_def' have 1: ‹∀i. Suc i < length (c#cs@[c']) ⟶ ((c#cs@[c']) ! i, (c#cs@[c']) ! Suc i) ∈ tran ∨ (c#cs@[c']) ! i ─e→ (c#cs@[c']) ! Suc i› by blast
  have ‹∀i. Suc i < length (c#cs) ⟶ ((c#cs) ! i, (c#cs) ! Suc i) ∈ tran ∨ (c#cs) ! i ─e→ (c#cs) ! Suc i› (is ‹∀i. ?P i›)
  proof
    fix i
    show ‹?P i›
    proof
      assume Suc_i_lt: ‹Suc i < length (c # cs)›
      show ‹((c # cs) ! i, (c # cs) ! Suc i) ∈ tran ∨ (c # cs) ! i ─e→ (c # cs) ! Suc i›
        using 1[THEN spec[where x=i]] Suc_i_lt
        by (metis (no_types, hide_lams) Suc_lessD Suc_less_eq Suc_mono append_Cons length_Cons length_append_singleton nth_Cons_Suc nth_butlast snoc_eq_iff_butlast)
    qed
  qed
  then show ?thesis using cpts_def' by blast
qed

(* this is "obvious" *)
lemma cpts_append:
  assumes a1: ‹cs@[c] ∈ cpts tran›
    and a2: ‹c#cs' ∈ cpts tran›
  shows ‹cs@c#cs' ∈ cpts tran›
proof-
  from a1 cpts_def' have a1': ‹∀i. Suc i < length (cs@[c]) ⟶ ((cs@[c]) ! i, (cs@[c]) ! Suc i) ∈ tran ∨ (cs@[c]) ! i ─e→ (cs@[c]) ! Suc i› by blast
  from a2 cpts_def' have a2': ‹∀i. Suc i < length (c#cs') ⟶ ((c#cs') ! i, (c#cs') ! Suc i) ∈ tran ∨ (c#cs') ! i ─e→ (c#cs') ! Suc i› by blast
  have ‹∀i. Suc i < length (cs@c#cs') ⟶ ((cs@c#cs') ! i, (cs@c#cs') ! Suc i) ∈ tran ∨ (cs@c#cs') ! i ─e→ (cs@c#cs') ! Suc i›
  proof
    fix i
    show ‹Suc i < length (cs@c#cs') ⟶ ((cs@c#cs') ! i, (cs@c#cs') ! Suc i) ∈ tran ∨ (cs@c#cs') ! i ─e→ (cs@c#cs') ! Suc i›
    proof
      assume Suc_i_lt: ‹Suc i < length (cs@c#cs')›
      show ‹((cs@c#cs') ! i, (cs@c#cs') ! Suc i) ∈ tran ∨ (cs@c#cs') ! i ─e→ (cs@c#cs') ! Suc i›
      proof(cases ‹Suc i < length (cs@[c])›)
        case True
        with a1'[THEN spec[where x=i]] show ?thesis
          by (metis Suc_less_eq length_append_singleton less_antisym nth_append nth_append_length)
      next
        case False
        with a2'[THEN spec[where x="i - length cs"]] show ?thesis
          (* smt ... *)
          by (smt Suc_diff_Suc Suc_i_lt Suc_lessD add_diff_cancel_left' diff_Suc_Suc diff_less_mono length_append length_append_singleton less_Suc_eq_le not_less_eq nth_append)
      qed
    qed
  qed
  with cpts_def' show ?thesis by blast
qed

end