text:
(*  Title:      HOL/Auth/n_flash_lemma_on_inv__95.thy
    Author:     Yongjian Li and Kaiqiang Duan, State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
    Copyright    2016 State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
*)

header{*The n_flash Protocol Case Study*}

theory n_flash_lemma_on_inv__95 imports n_flash_base
begin
section{*All lemmas on causal relation between inv__95 and some rule r*}
lemma n_PI_Remote_GetVsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_PI_Remote_Get  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_PI_Remote_Get  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_PI_Remote_GetXVsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_PI_Remote_GetX  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_PI_Remote_GetX  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_NakVsinv__95:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Nak  dst)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain dst where a1:"dst\<le>N\<and>r=n_NI_Nak  dst" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(dst=p__Inv4)\<or>(dst~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(dst=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(dst~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_Get_Nak__part__0Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__0  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_Get_Nak__part__0  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_Get_Nak__part__1Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__1  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_Get_Nak__part__1  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_Get_Nak__part__2Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Nak__part__2  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_Get_Nak__part__2  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_Get_Get__part__0Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Get__part__0  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_Get_Get__part__0  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_Get_Get__part__1Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Get__part__1  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_Get_Get__part__1  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P3 s"
  apply (cut_tac a1 a2 b1, simp, rule_tac x="(neg (andForm (eqn (IVar (Field (Field (Ident ''Sta'') ''HomeUniMsg'') ''Cmd'')) (Const UNI_Put)) (eqn (IVar (Field (Field (Ident ''Sta'') ''Dir'') ''Pending'')) (Const false))))" in exI, auto) done
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_Get_Put_HeadVsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put_Head N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_Get_Put_Head N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_Get_PutVsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_Get_Put  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_Get_Put_DirtyVsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Put_Dirty  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_Get_Put_Dirty  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Remote_Get_NakVsinv__95:
assumes a1: "(\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_Get_Nak  src dst)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src dst where a1:"src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_Get_Nak  src dst" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4\<and>dst~=p__Inv4)\<or>(src~=p__Inv4\<and>dst=p__Inv4)\<or>(src~=p__Inv4\<and>dst~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4\<and>dst~=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>dst=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>dst~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Remote_Get_Nak_HomeVsinv__95:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Get_Nak_Home  dst)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain dst where a1:"dst\<le>N\<and>r=n_NI_Remote_Get_Nak_Home  dst" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(dst=p__Inv4)\<or>(dst~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(dst=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(dst~=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Remote_Get_PutVsinv__95:
assumes a1: "(\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_Get_Put  src dst)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src dst where a1:"src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_Get_Put  src dst" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4\<and>dst~=p__Inv4)\<or>(src~=p__Inv4\<and>dst=p__Inv4)\<or>(src~=p__Inv4\<and>dst~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4\<and>dst~=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>dst=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>dst~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Remote_Get_Put_HomeVsinv__95:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Get_Put_Home  dst)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain dst where a1:"dst\<le>N\<and>r=n_NI_Remote_Get_Put_Home  dst" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(dst=p__Inv4)\<or>(dst~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(dst=p__Inv4)"
  have "?P3 s"
  apply (cut_tac a1 a2 b1, simp, rule_tac x="(neg (andForm (eqn (IVar (Field (Para (Field (Ident ''Sta'') ''UniMsg'') p__Inv4) ''Cmd'')) (Const UNI_Get)) (eqn (IVar (Field (Para (Field (Ident ''Sta'') ''Proc'') p__Inv4) ''CacheState'')) (Const CACHE_E))))" in exI, auto) done
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(dst~=p__Inv4)"
  have "?P3 s"
  apply (cut_tac a1 a2 b1, simp, rule_tac x="(neg (andForm (andForm (eqn (IVar (Field (Field (Ident ''Sta'') ''HomeUniMsg'') ''Cmd'')) (Const UNI_Get)) (eqn (IVar (Field (Para (Field (Ident ''Sta'') ''UniMsg'') p__Inv4) ''Cmd'')) (Const UNI_Get))) (eqn (IVar (Field (Para (Field (Ident ''Sta'') ''UniMsg'') p__Inv4) ''HomeProc'')) (Const false))))" in exI, auto) done
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_Nak__part__0Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__0  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__0  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_Nak__part__1Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__1  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__1  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_Nak__part__2Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__2  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_Nak__part__2  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_GetX__part__0Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_GetX__part__0  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_GetX__part__0  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_GetX__part__1Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_GetX__part__1  src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_GetX__part__1  src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_1Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_1 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_1 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_2Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_2 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_2 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_3Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_3 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_3 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_4Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_4 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_4 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_5Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_5 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_5 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_6Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_6 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_6 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_7__part__0Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__0 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__0 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_7__part__1Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__1 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_7__part__1 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_7_NODE_Get__part__0Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__0 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__0 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_7_NODE_Get__part__1Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__1 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_7_NODE_Get__part__1 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_8_HomeVsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_8_Home_NODE_GetVsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home_NODE_Get N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_8_Home_NODE_Get N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_8Vsinv__95:
assumes a1: "(\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8 N src pp)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src pp where a1:"src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8 N src pp" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4\<and>pp~=p__Inv4)\<or>(src~=p__Inv4\<and>pp=p__Inv4)\<or>(src~=p__Inv4\<and>pp~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4\<and>pp~=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>pp=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>pp~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_8_NODE_GetVsinv__95:
assumes a1: "(\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8_NODE_Get N src pp)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src pp where a1:"src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_8_NODE_Get N src pp" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4\<and>pp~=p__Inv4)\<or>(src~=p__Inv4\<and>pp=p__Inv4)\<or>(src~=p__Inv4\<and>pp~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4\<and>pp~=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>pp=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>pp~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_9__part__0Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__0 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__0 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_9__part__1Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__1 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_9__part__1 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_10_HomeVsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_10_Home N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_10_Home N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_10Vsinv__95:
assumes a1: "(\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_10 N src pp)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src pp where a1:"src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_Local_GetX_PutX_10 N src pp" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4\<and>pp~=p__Inv4)\<or>(src~=p__Inv4\<and>pp=p__Inv4)\<or>(src~=p__Inv4\<and>pp~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4\<and>pp~=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>pp=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>pp~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Local_GetX_PutX_11Vsinv__95:
assumes a1: "(\<exists> src. src\<le>N\<and>r=n_NI_Local_GetX_PutX_11 N src)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src where a1:"src\<le>N\<and>r=n_NI_Local_GetX_PutX_11 N src" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4)\<or>(src~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Remote_GetX_NakVsinv__95:
assumes a1: "(\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_GetX_Nak  src dst)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src dst where a1:"src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_GetX_Nak  src dst" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4\<and>dst~=p__Inv4)\<or>(src~=p__Inv4\<and>dst=p__Inv4)\<or>(src~=p__Inv4\<and>dst~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4\<and>dst~=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>dst=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>dst~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Remote_GetX_Nak_HomeVsinv__95:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_GetX_Nak_Home  dst)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain dst where a1:"dst\<le>N\<and>r=n_NI_Remote_GetX_Nak_Home  dst" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(dst=p__Inv4)\<or>(dst~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(dst=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(dst~=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Remote_GetX_PutXVsinv__95:
assumes a1: "(\<exists> src dst. src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_GetX_PutX  src dst)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain src dst where a1:"src\<le>N\<and>dst\<le>N\<and>src~=dst\<and>r=n_NI_Remote_GetX_PutX  src dst" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(src=p__Inv4\<and>dst~=p__Inv4)\<or>(src~=p__Inv4\<and>dst=p__Inv4)\<or>(src~=p__Inv4\<and>dst~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(src=p__Inv4\<and>dst~=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>dst=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(src~=p__Inv4\<and>dst~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Remote_GetX_PutX_HomeVsinv__95:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_GetX_PutX_Home  dst)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain dst where a1:"dst\<le>N\<and>r=n_NI_Remote_GetX_PutX_Home  dst" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(dst=p__Inv4)\<or>(dst~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(dst=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(dst~=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Remote_PutVsinv__95:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Put  dst)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain dst where a1:"dst\<le>N\<and>r=n_NI_Remote_Put  dst" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(dst=p__Inv4)\<or>(dst~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(dst=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(dst~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_NI_Remote_PutXVsinv__95:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_PutX  dst)" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain dst where a1:"dst\<le>N\<and>r=n_NI_Remote_PutX  dst" apply fastforce done
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
have "(dst=p__Inv4)\<or>(dst~=p__Inv4)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(dst=p__Inv4)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(dst~=p__Inv4)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_PI_Local_Get_GetVsinv__95:
assumes a1: "(r=n_PI_Local_Get_Get  )" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_PI_Local_GetX_GetX__part__0Vsinv__95:
assumes a1: "(r=n_PI_Local_GetX_GetX__part__0  )" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_PI_Local_GetX_GetX__part__1Vsinv__95:
assumes a1: "(r=n_PI_Local_GetX_GetX__part__1  )" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Nak_HomeVsinv__95:
assumes a1: "(r=n_NI_Nak_Home  )" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_PutVsinv__95:
assumes a1: "(r=n_NI_Local_Put  )" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Local_PutXAcksDoneVsinv__95:
assumes a1: "(r=n_NI_Local_PutXAcksDone  )" and
a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a2 obtain p__Inv4 where a2:"p__Inv4\<le>N\<and>f=inv__95  p__Inv4" apply fastforce done
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_PI_Local_GetX_PutX__part__0Vsinv__95:
  assumes a1: "r=n_PI_Local_GetX_PutX__part__0  " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_WbVsinv__95:
  assumes a1: "r=n_NI_Wb  " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_StoreVsinv__95:
  assumes a1: "\<exists> src data. src\<le>N\<and>data\<le>N\<and>r=n_Store  src data" and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvAck_3Vsinv__95:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_InvAck_3 N src" and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvAck_1Vsinv__95:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_InvAck_1 N src" and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Remote_ReplaceVsinv__95:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_PI_Remote_Replace  src" and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_Store_HomeVsinv__95:
  assumes a1: "\<exists> data. data\<le>N\<and>r=n_Store_Home  data" and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Local_ReplaceVsinv__95:
  assumes a1: "r=n_PI_Local_Replace  " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvAck_existsVsinv__95:
  assumes a1: "\<exists> src pp. src\<le>N\<and>pp\<le>N\<and>src~=pp\<and>r=n_NI_InvAck_exists  src pp" and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Remote_PutXVsinv__95:
  assumes a1: "\<exists> dst. dst\<le>N\<and>r=n_PI_Remote_PutX  dst" and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvVsinv__95:
  assumes a1: "\<exists> dst. dst\<le>N\<and>r=n_NI_Inv  dst" and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Local_PutXVsinv__95:
  assumes a1: "r=n_PI_Local_PutX  " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Local_Get_PutVsinv__95:
  assumes a1: "r=n_PI_Local_Get_Put  " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_ShWbVsinv__95:
  assumes a1: "r=n_NI_ShWb N " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Local_GetX_PutX_HeadVld__part__0Vsinv__95:
  assumes a1: "r=n_PI_Local_GetX_PutX_HeadVld__part__0 N " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_ReplaceVsinv__95:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Replace  src" and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Local_GetX_PutX__part__1Vsinv__95:
  assumes a1: "r=n_PI_Local_GetX_PutX__part__1  " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvAck_exists_HomeVsinv__95:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_InvAck_exists_Home  src" and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Replace_HomeVsinv__95:
  assumes a1: "r=n_NI_Replace_Home  " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Nak_ClearVsinv__95:
  assumes a1: "r=n_NI_Nak_Clear  " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_InvAck_2Vsinv__95:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_InvAck_2 N src" and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_PI_Local_GetX_PutX_HeadVld__part__1Vsinv__95:
  assumes a1: "r=n_PI_Local_GetX_PutX_HeadVld__part__1 N " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_FAckVsinv__95:
  assumes a1: "r=n_NI_FAck  " and
  a2: "(\<exists> p__Inv4. p__Inv4\<le>N\<and>f=inv__95  p__Inv4)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

end

author: paraVerifier

repo: paraVerifier


text:
theory T152
imports Main
begin
lemma "(
(\<forall> x::nat. \<forall> y::nat. meet(x, y) = meet(y, x)) &
(\<forall> x::nat. \<forall> y::nat. join(x, y) = join(y, x)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, meet(y, z)) = meet(meet(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(x, join(y, z)) = join(join(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. meet(x, join(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. join(x, meet(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(x, join(y, z)) = join(mult(x, y), mult(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(join(x, y), z) = join(mult(x, z), mult(y, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, over(join(mult(x, y), z), y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(y, undr(x, join(mult(x, y), z))) = y) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(over(x, y), y), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(y, undr(y, x)), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(x, meet(y, z)) = meet(mult(x, y), mult(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. undr(x, join(y, z)) = join(undr(x, y), undr(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. over(join(x, y), z) = join(over(x, z), over(y, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. undr(meet(x, y), z) = join(undr(x, z), undr(y, z))) &
(\<forall> x::nat. \<forall> y::nat. invo(join(x, y)) = meet(invo(x), invo(y))) &
(\<forall> x::nat. \<forall> y::nat. invo(meet(x, y)) = join(invo(x), invo(y))) &
(\<forall> x::nat. invo(invo(x)) = x)
) \<longrightarrow>
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. over(x, meet(y, z)) = join(over(x, y), over(x, z)))
"
nitpick[card nat=8,timeout=86400]
oops
end

author: inpefess

repo: residuated-binars


text:
(*
 * Copyright (C) 2014 NICTA
 * All rights reserved.
 *)

(* Author: David Cock - David.Cock@nicta.com.au *)

header "The Monty Hall Problem"

theory Monty imports "../pGCL" begin

text {*
We now tackle a more substantial example, allowing us to demonstrate
the tools for compositional reasoning and the use of invariants in
non-recursive programs.  Our example is the well-known Monty Hall puzzle
in statistical inference \citep{Selvin_75}.

The setting is a game show:  There is a prize hidden behind one
of three doors, and the contestant is invited to choose one.  Once
the guess is made, the host than opens one of the remaining two
doors, revealing a goat and showing that the prize is elsewhere.  The
contestent is then given the choice of switching their guess to the
other unopened door, or sticking to their first guess.

The puzzle is whether the contestant is better off switching or
staying put; or indeed whether it makes a difference at all.  Most people's
intuition suggests that it make no difference, whereas in fact,
switching raises the chance of success from 1/3 to 2/3.
*}

subsection {* The State Space *}

text {* The game state consists of the prize location, the guess,
and the clue (the door the host opens).  These are not constrained a
priori to the range @{term "{1::real,2,3}"}, but are simply natural numbers:
We instead show that this is in fact an invariant.
*}

record game =
  prize  :: nat
 "guess" :: nat
  clue   :: nat

text {* The victory condition: The player wins if they have guessed the
  correct door, when the game ends. *}
definition player_wins :: "game \<Rightarrow> bool"
where "player_wins g \<equiv> guess g = prize g"

subsubsection {* Invariants *}

text {* We prove explicitly that only valid doors are ever chosen. *}

definition inv_prize :: "game \<Rightarrow> bool"
where "inv_prize g \<equiv> prize g \<in> {1,2,3}"

definition inv_clue :: "game \<Rightarrow> bool"
where "inv_clue g \<equiv> clue g \<in> {1,2,3}"

definition inv_guess :: "game \<Rightarrow> bool"
where "inv_guess g \<equiv> guess g \<in> {1,2,3}"

subsection {* The Game *}

text {* Hide the prize behind door @{term D}. *}
definition hide_behind :: "nat \<Rightarrow> game prog"
where "hide_behind D \<equiv> Apply (prize_update (\<lambda>x. D))"

text {* Choose door @{term D}. *}
definition guess_behind :: "nat \<Rightarrow> game prog"
where "guess_behind D \<equiv> Apply (guess_update (\<lambda>x. D))"

text {* Open door @{term D} and reveal what's behind. *}
definition open_door :: "nat \<Rightarrow> game prog"
where "open_door D \<equiv> Apply (clue_update (\<lambda>x. D))"

text {* Hide the prize behind door 1, 2 or 3, demonically i.e.~according
  to any probability distribution (or none). *}
definition hide_prize :: "game prog"
where "hide_prize \<equiv> hide_behind 1 \<Sqinter> hide_behind 2 \<Sqinter> hide_behind 3"

text {* Guess uniformly at random. *}
definition make_guess :: "game prog"
where "make_guess \<equiv> guess_behind 1 \<^bsub>(\<lambda>s. 1/3)\<^esub>\<oplus>
                    guess_behind 2 \<^bsub>(\<lambda>s. 1/2)\<^esub>\<oplus> guess_behind 3"

text {* Open one of the two doors that \emph{doesn't} hide the prize. *}
definition reveal :: "game prog"
where "reveal \<equiv> \<Sqinter>d\<in>(\<lambda>s. {1,2,3} - {prize s, guess s}). open_door d"

text {* Switch your guess to the other unopened door. *}
definition switch_guess :: "game prog"
where "switch_guess \<equiv> \<Sqinter>d\<in>(\<lambda>s. {1,2,3} - {clue s, guess s}). guess_behind d"

text {* The complete game, either with or without switching guesses. *}
definition monty :: "bool \<Rightarrow> game prog"
where
  "monty switch \<equiv> hide_prize ;;
                  make_guess ;;
                  reveal ;;
                  (if switch then switch_guess else Skip)"

subsection {* A Brute Force Solution *}

text {* For sufficiently simple programs, we can calculate the exact weakest
  pre-expectation by unfolding. *}

lemma eval_win[simp]:
  "p = g \<Longrightarrow> \<guillemotleft>player_wins\<guillemotright> (s\<lparr> prize := p, guess := g, clue := c \<rparr>) = 1"
  by(simp add:embed_bool_def player_wins_def)

lemma eval_loss[simp]:
  "p \<noteq> g \<Longrightarrow> \<guillemotleft>player_wins\<guillemotright> (s\<lparr> prize := p, guess := g, clue := c \<rparr>) = 0"
  by(simp add:embed_bool_def player_wins_def)

text {* If they stick to their guns, the player wins with $p=1/3$. *}
lemma wp_monty_noswitch:
  "(\<lambda>s. 1/3) = wp (monty False) \<guillemotleft>player_wins\<guillemotright>"
  unfolding monty_def hide_prize_def make_guess_def reveal_def
            hide_behind_def guess_behind_def open_door_def
            switch_guess_def
  by(simp add:wp_eval insert_Diff_if o_def)

lemma swap_upd:
  "s\<lparr> prize := p, clue := c, guess := g \<rparr> =
   s\<lparr> prize := p, guess := g, clue := c \<rparr>"
  by(simp)

text {* If they switch, they win with $p=2/3$.  Brute force here
  takes longer, but is still feasible.  On larger programs,
  this will rapidly become impossible, as the size of the terms
  (generally) grows exponentially with the length of the program. *}

lemma wp_monty_switch_bruteforce:
  "(\<lambda>s. 2/3) = wp (monty True) \<guillemotleft>player_wins\<guillemotright>"
  unfolding monty_def hide_prize_def make_guess_def reveal_def
            hide_behind_def guess_behind_def open_door_def
            switch_guess_def
  -- "Note that this is getting slow"
  by(simp add:wp_eval insert_Diff_if swap_upd o_def)

subsection {* A Modular Approach *}

text {* We can solve the problem more efficiently, at the cost of
  a little more user effort, by breaking up the problem and annotating
  each step of the game separately.  While this is not strictly necessary
  for this program, it will scale to larger examples, as the work in
  annotation only increases linearly with the length of the program. *}

subsubsection {* Healthiness *}

text {* We first establish healthiness for each step. This follows
  straightforwardly by applying the supplied rulesets. *}

lemma wd_hide_prize:
  "well_def hide_prize"
  unfolding hide_prize_def hide_behind_def
  by(simp add:wd_intros)

lemma wd_make_guess:
  "well_def make_guess"
  unfolding make_guess_def guess_behind_def
  by(simp add:wd_intros)

lemma wd_reveal:
  "well_def reveal"
proof -
  txt {* Here, we do need a subsidiary lemma: that there is always
    a `fresh' door available.  The rest of the healthiness proof follows
    as usual. *}
  have "\<And>s. {1, 2, 3} - {prize s, guess s} \<noteq> {}"
    by(auto simp:insert_Diff_if)
  thus ?thesis
    unfolding reveal_def open_door_def
    by(intro wd_intros, auto)
qed

lemma wd_switch_guess:
  "well_def switch_guess"
proof -
  have "\<And>s. {1, 2, 3} - {clue s, guess s} \<noteq> {}"
    by(auto simp:insert_Diff_if)
  thus ?thesis
    unfolding switch_guess_def guess_behind_def
    by(intro wd_intros, auto)
qed

lemmas monty_healthy =
  wd_switch_guess wd_reveal wd_make_guess wd_hide_prize

subsubsection {* Annotations *}

text {* We now annotate each step individually, and then combine them to
  produce an annotation for the entire program. *}

text {* @{term hide_prize} chooses a valid door. *}
lemma wp_hide_prize:
  "(\<lambda>s. 1) \<tturnstile> wp hide_prize \<guillemotleft>inv_prize\<guillemotright>"
  unfolding hide_prize_def hide_behind_def wp_eval o_def
  by(simp add:embed_bool_def inv_prize_def)

text {* Given the prize invariant, @{term make_guess} chooses a valid
  door, and guesses incorrectly with probability at least 2/3. *}
lemma wp_make_guess:
  "(\<lambda>s. 2/3 * \<guillemotleft>\<lambda>g. inv_prize g\<guillemotright> s) \<tturnstile>
   wp make_guess \<guillemotleft>\<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g\<guillemotright>"
  unfolding make_guess_def guess_behind_def wp_eval o_def
  by(auto simp:embed_bool_def inv_prize_def inv_guess_def)

lemma last_one:
  assumes "a \<noteq> b" and "a \<in> {1::nat,2,3}" and "b \<in> {1,2,3}"
  shows "\<exists>!c. {1,2,3} - {b,a} = {c}"
  apply(simp add:insert_Diff_if)
  using assms by(auto intro:assms)

text {* Given the composed invariants, and an incorrect guess, @{term reveal}
  will give a clue that is neither the prize, nor the guess. *}
lemma wp_reveal:
  "\<guillemotleft>\<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g\<guillemotright> \<tturnstile>
   wp reveal \<guillemotleft>\<lambda>g. guess g \<noteq> prize g \<and>
                  clue g \<noteq> prize g \<and>
                  clue g \<noteq> guess g \<and>
                  inv_prize g \<and> inv_guess g \<and> inv_clue g\<guillemotright>"
  (is "?X \<tturnstile> wp reveal ?Y")
proof(rule use_premise, rule well_def_wp_healthy[OF wd_reveal], clarify)
  fix s
  assume "guess s \<noteq> prize s"
     and "inv_prize s"
     and "inv_guess s"
  moreover then obtain c
    where singleton: "{Suc 0,2,3} -  {prize s, guess s} = {c}"
      and "c \<noteq> prize s"
      and "c \<noteq> guess s"
      and "c \<in> {Suc 0,2,3}"
    unfolding inv_prize_def inv_guess_def
    by(force dest:last_one elim!:ex1E)
  ultimately show "1 \<le> wp reveal ?Y s"
    by(simp add:reveal_def open_door_def wp_eval singleton o_def
                embed_bool_def inv_prize_def inv_guess_def inv_clue_def)
qed

text {* Showing that the three doors are all district is a largeish
  first-order problem, for which sledgehammer gives us a reasonable
  script. *}
lemma distinct_game:
  "\<lbrakk> guess g \<noteq> prize g; clue g \<noteq> prize g; clue g \<noteq> guess g;
     inv_prize g; inv_guess g; inv_clue g \<rbrakk> \<Longrightarrow>
   {1, 2, 3} = {guess g, prize g, clue g}"
  unfolding inv_prize_def inv_guess_def inv_clue_def
  apply(rule set_eqI)
  apply(rule iffI)
   apply(clarify)
   apply(metis (full_types) empty_iff insert_iff)
  apply(metis insert_iff)
  done

text {* Given the invariants, switching from the wrong guess gives
  the right one. *}
lemma wp_switch_guess:
  "\<guillemotleft>\<lambda>g. guess g \<noteq> prize g \<and> clue g \<noteq> prize g \<and> clue g \<noteq> guess g \<and>
        inv_prize g \<and> inv_guess g \<and> inv_clue g\<guillemotright> \<tturnstile>
   wp switch_guess \<guillemotleft>player_wins\<guillemotright>"
proof(rule use_premise, safe)
  from wd_switch_guess show "healthy (wp switch_guess)" by(auto)

  fix s
  assume "guess s \<noteq> prize s" and "clue s \<noteq> prize s"
     and "clue s \<noteq> guess s" and "inv_prize s"
     and "inv_guess s" and "inv_clue s"
  note state = this
  hence "1 \<le> Inf ((\<lambda>a. \<guillemotleft> player_wins \<guillemotright> (s\<lparr>guess := a\<rparr>)) `
    ({guess s, prize s, clue s} - {clue s, guess s}))"
    by(auto simp:insert_Diff_if player_wins_def)
  also from state
  have "... = Inf ((\<lambda>a. \<guillemotleft> player_wins \<guillemotright> (s\<lparr>guess := a\<rparr>)) `
                  ({1, 2, 3} - {clue s, guess s}))"
    by(simp add:distinct_game[symmetric])
  also have "... = wp switch_guess \<guillemotleft>player_wins\<guillemotright> s"
    by(simp add:switch_guess_def guess_behind_def wp_eval o_def)
  finally show "1 \<le> wp switch_guess \<guillemotleft> player_wins \<guillemotright> s" .
qed

text {* Given componentwise specifications, we can glue them together
with calculational reasoning to get our result. *}
lemma wp_monty_switch_modular:
  "(\<lambda>s. 2/3) \<tturnstile> wp (monty True) \<guillemotleft>player_wins\<guillemotright>"
proof(rule wp_validD)  -- "Work in probabilistic Hoare triples"
  note wp_validI[OF wp_scale, OF wp_hide_prize, simplified]
    -- "Here we apply scaling to match our pre-expectation"
  also note wp_validI[OF wp_make_guess]
  also note wp_validI[OF wp_reveal]
  also note wp_validI[OF wp_switch_guess]
  finally show "\<lbrace>\<lambda>s. 2/3\<rbrace> monty True \<lbrace>\<guillemotleft>player_wins\<guillemotright>\<rbrace>p"
    unfolding monty_def
    by(simp add:wd_intros sound_intros monty_healthy)
qed

subsubsection {* Using the VCG *}

lemmas scaled_hide = wp_scale[OF wp_hide_prize, simplified]
declare scaled_hide[pwp] wp_make_guess[pwp] wp_reveal[pwp] wp_switch_guess[pwp]
declare wd_hide_prize[wd] wd_make_guess[wd] wd_reveal[wd] wd_switch_guess[wd]

text {* Alternatively, the VCG will get this using the same annotations. *}
lemma wp_monty_switch_vcg:
  "(\<lambda>s. 2/3) \<tturnstile> wp (monty True) \<guillemotleft>player_wins\<guillemotright>"
  unfolding monty_def
  by(simp, pvcg)

end

author: Josh-Tilles

repo: AFP

save_path: github-repos/isabelle/Josh-Tilles-AFP


text:
theory T59
imports Main
begin
lemma "(
(\<forall> x::nat. \<forall> y::nat. meet(x, y) = meet(y, x)) &
(\<forall> x::nat. \<forall> y::nat. join(x, y) = join(y, x)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, meet(y, z)) = meet(meet(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(x, join(y, z)) = join(join(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. meet(x, join(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. join(x, meet(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(x, join(y, z)) = join(mult(x, y), mult(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(join(x, y), z) = join(mult(x, z), mult(y, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, over(join(mult(x, y), z), y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(y, undr(x, join(mult(x, y), z))) = y) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(over(x, y), y), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(y, undr(y, x)), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(x, meet(y, z)) = meet(mult(x, y), mult(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. over(join(x, y), z) = join(over(x, z), over(y, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. over(x, meet(y, z)) = join(over(x, y), over(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. undr(meet(x, y), z) = join(undr(x, z), undr(y, z))) &
(\<forall> x::nat. \<forall> y::nat. invo(join(x, y)) = meet(invo(x), invo(y))) &
(\<forall> x::nat. \<forall> y::nat. invo(meet(x, y)) = join(invo(x), invo(y))) &
(\<forall> x::nat. invo(invo(x)) = x)
) \<longrightarrow>
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(meet(x, y), z) = meet(mult(x, z), mult(y, z)))
"
nitpick[card nat=4,timeout=86400]
oops
end


text:
section \<open>Notions of Equivalence\<close>

subsection \<open>Strong Simulation and Bisimulation\<close>

theory Strong_Relations
  imports Transition_Systems
begin

context lts
begin

definition simulation ::
  \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
where
  \<open>simulation R \<equiv> \<forall> p q. R p q \<longrightarrow>
    (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
      (\<exists> q'. R p' q' \<and> (q \<longmapsto>a q')))\<close>

definition bisimulation ::
  \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
where
  \<open>bisimulation R \<equiv> \<forall> p q. R p q \<longrightarrow>
    (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow>
      (\<exists> q'. R p' q' \<and> (q \<longmapsto>a q'))) \<and>
    (\<forall> q' a. q \<longmapsto>a q' \<longrightarrow>
      (\<exists> p'. R p' q' \<and> (p \<longmapsto>a p')))\<close>

lemma bisim_ruleformat:
  assumes \<open>bisimulation R\<close>
    and \<open>R p q\<close>
  shows
    \<open>p \<longmapsto>a p' \<Longrightarrow> (\<exists> q'. R p' q' \<and> (q \<longmapsto>a q'))\<close>
    \<open>q \<longmapsto>a q' \<Longrightarrow> (\<exists> p'. R p' q' \<and> (p \<longmapsto>a p'))\<close>
  using assms unfolding bisimulation_def by auto

end \<comment>\<open>context lts\<close>

end

author: luisamontanari

repo: ContrasimGame


text:
(*  Title:      HOL/ex/Case_Product.thy
    Author:     Lars Noschinski
    Copyright   2011 TU Muenchen
*)

section \<open>Examples for the 'case_product' attribute\<close>

theory Case_Product
imports MainRLT
begin

text \<open>
  The @{attribute case_product} attribute combines multiple case distinction
  lemmas into a single case distinction lemma by building the product of all
  these case distinctions.
\<close>

lemmas nat_list_exhaust = nat.exhaust [case_product list.exhaust]

text \<open>The attribute honours preconditions.\<close>

lemmas trancl_acc_cases = trancl.cases [case_product acc.cases]

text \<open>Also, case names are generated based on the old names.\<close>

end

author: dtraytel

repo: HOLRLT

save_path: github-repos/isabelle/dtraytel-HOLRLT


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

theory ArchBCorres2_AI
imports
  BCorres2_AI
begin

context Arch begin global_naming AARCH64

named_theorems BCorres2_AI_assms

crunch (bcorres)bcorres[wp, BCorres2_AI_assms]: invoke_cnode truncate_state
  (simp: swp_def ignore: clearMemory without_preemption filterM ethread_set)

crunch (bcorres)bcorres[wp]: create_cap,init_arch_objects,retype_region,delete_objects truncate_state
  (ignore: freeMemory clearMemory retype_region_ext)

crunch (bcorres)bcorres[wp]: set_extra_badge,derive_cap truncate_state (ignore: storeWord)

crunch (bcorres)bcorres[wp]: invoke_untyped truncate_state
  (ignore: sequence_x)

crunch (bcorres)bcorres[wp]: set_mcpriority truncate_state

crunch (bcorres)bcorres[wp, BCorres2_AI_assms]: arch_get_sanitise_register_info, arch_post_modify_registers truncate_state

lemma invoke_tcb_bcorres[wp]:
  fixes a
  shows "bcorres (invoke_tcb a) (invoke_tcb a)"
  apply (cases a)
        apply (wp | wpc | simp add: set_mcpriority_def)+
  apply (rename_tac option)
  apply (case_tac option)
   apply (wp | wpc | simp)+
  done

lemma transfer_caps_loop_bcorres[wp]:
 "bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi)"
  apply (induct caps arbitrary: slots n mi ep)
   apply simp
   apply wp
  apply (case_tac a)
  apply simp
  apply (intro impI conjI)
             apply (wp | simp)+
  done

lemma invoke_irq_control_bcorres[wp]: "bcorres (invoke_irq_control a) (invoke_irq_control a)"
  apply (cases a)
   apply wpsimp
  apply (rename_tac acap)
  apply (case_tac acap)
  apply wpsimp
  done

lemma invoke_irq_handler_bcorres[wp]: "bcorres (invoke_irq_handler a) (invoke_irq_handler a)"
  by (cases a; wpsimp)

lemma make_arch_fault_msg_bcorres[wp,BCorres2_AI_assms]:
  "bcorres (make_arch_fault_msg a b) (make_arch_fault_msg a b)"
  by (cases a; simp ; wp)

lemma  handle_arch_fault_reply_bcorres[wp,BCorres2_AI_assms]:
  "bcorres ( handle_arch_fault_reply a b c d) (handle_arch_fault_reply a b c d)"
  by (cases a; simp add: handle_arch_fault_reply_def; wp)

crunch (bcorres)bcorres[wp, BCorres2_AI_assms]:
    arch_switch_to_thread,arch_switch_to_idle_thread truncate_state

end

interpretation BCorres2_AI?: BCorres2_AI
  proof goal_cases
  interpret Arch .
  case 1 show ?case by (unfold_locales; (fact BCorres2_AI_assms)?)
  qed

lemmas schedule_bcorres[wp] = schedule_bcorres1[OF BCorres2_AI_axioms]

context Arch begin global_naming AARCH64

crunch (bcorres)bcorres[wp]: send_ipc,send_signal,do_reply_transfer,arch_perform_invocation truncate_state
  (simp: gets_the_def swp_def
   ignore: freeMemory clearMemory loadWord cap_fault_on_failure
           storeWord lookup_error_on_failure getRestartPC getRegister mapME )

lemma perform_invocation_bcorres[wp]: "bcorres (perform_invocation a b c) (perform_invocation a b c)"
  apply (cases c)
  apply (wp | wpc | simp)+
  done

lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (decode_cnode_invocation a b c d)"
  apply (simp add: decode_cnode_invocation_def)
  apply (wp | wpc | simp add: split_def | intro impI conjI)+
  done

crunch (bcorres)bcorres[wp]:
  decode_set_ipc_buffer, decode_set_space, decode_set_priority,
  decode_set_mcpriority, decode_set_sched_params, decode_bind_notification,
  decode_unbind_notification, decode_set_tls_base truncate_state

lemma decode_tcb_configure_bcorres[wp]:
  "bcorres (decode_tcb_configure b (ThreadCap c) d e)
           (decode_tcb_configure b (ThreadCap c) d e)"
  apply (simp add: decode_tcb_configure_def | wp)+
  done

lemma decode_tcb_invocation_bcorres[wp]:
  "bcorres (decode_tcb_invocation a b (ThreadCap c) d e)
           (decode_tcb_invocation a b (ThreadCap c) d e)"
  unfolding decode_tcb_invocation_def by wpsimp

crunch (bcorres)bcorres[wp]: arch_decode_invocation truncate_state
  (simp: crunch_simps)

crunch (bcorres) bcorres[wp]: handle_invocation truncate_state
  (simp: syscall_def Let_def gets_the_def
   ignore: syscall cap_fault_on_failure without_preemption const_on_failure
           decode_tcb_invocation)

crunch (bcorres)bcorres[wp]: receive_ipc,receive_signal,delete_caller_cap truncate_state

lemma handle_vm_fault_bcorres[wp]: "bcorres (handle_vm_fault a b) (handle_vm_fault a b)"
  unfolding handle_vm_fault_def by (cases b; wpsimp)

lemma vgic_maintenance_bcorres[wp]:
  "bcorres vgic_maintenance vgic_maintenance"
  unfolding vgic_maintenance_def
  by (wpsimp simp: vgic_update_lr_bcorres)

lemma vppi_event_bcorres[wp]:
  "bcorres (vppi_event irq) (vppi_event irq)"
  unfolding vppi_event_def
  by wpsimp

lemma handle_reserved_irq_bcorres[wp]: "bcorres (handle_reserved_irq a) (handle_reserved_irq a)"
  unfolding handle_reserved_irq_def by wpsimp

lemma handle_hypervisor_fault_bcorres[wp]: "bcorres (handle_hypervisor_fault a b) (handle_hypervisor_fault a b)"
  by (cases b; wpsimp)

lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
  apply (cases e)
  apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def
                   handle_interrupt_def Let_def handle_reserved_irq_def arch_mask_irq_signal_def
         | intro impI conjI allI | wp | wpc)+
  done

crunch (bcorres)bcorres[wp]: guarded_switch_to,switch_to_idle_thread truncate_state (ignore: storeWord)

lemma choose_switch_or_idle:
  "((), s') \<in> fst (choose_thread s) \<Longrightarrow>
       (\<exists>word. ((),s') \<in> fst (guarded_switch_to word s)) \<or>
       ((),s') \<in> fst (switch_to_idle_thread s)"
  apply (simp add: choose_thread_def)
  apply (clarsimp simp add: switch_to_idle_thread_def bind_def gets_def
                   arch_switch_to_idle_thread_def in_monad
                   return_def get_def modify_def put_def
                    get_thread_state_def
                   thread_get_def
                   split: if_split_asm)
  apply force
  done

end

end


theory Nlist
imports "ZF-Induct.ListN" ListExt NatExt
begin

definition nlist :: "[i, i] \<Rightarrow> i" ("(nlist[_]/_)" [0, 1000] 85)
where
  "nlist[n]A == {p:listn(A). EX l. p = <n, l>}"

definition nnil :: "i"
where
  "nnil == <0, Nil>"

definition ncons :: "[i, i, i] => i"
where
  "ncons(n, a, l) == <succ(n), Cons(a, snd(l))>"

definition napp :: "[i, i, i, i] \<Rightarrow> i"
where
  "napp(n1, n2, l1, l2) == <n1 #+ n2, snd(l1) @ snd(l2)>"

definition nhd :: "i \<Rightarrow> i"
where
  "nhd(l) == hd(snd(l))"

definition ntl :: "[i, i] \<Rightarrow> i"
where
  "ntl(n, l) == <n #- 1, tl(snd(l))>"

definition nlast :: "i \<Rightarrow> i"
where
  "nlast(l) == hd(rev(snd(l)))"

definition nfront :: "[i, i] \<Rightarrow> i"
where
  "nfront(n, l) == <n #- 1, front(snd(l))>"

definition nsnoc :: "[i, i, i] \<Rightarrow> i"
where
  "nsnoc(n, l, a) == napp(n, 1, l, ncons(0, a, nnil))"

definition nnth :: "[i, i] \<Rightarrow> i"
where
  "nnth(i, l) == hd(drop(i, snd(l)))"

definition nbuild :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
where
  "nbuild(n, p) == rec(n, nnil, %m r. nsnoc(m, r, p(m)))"

theorem listn_sub: "c:listn(A) \<Longrightarrow> c : nat * list(A)"
apply(insert dom_subset[of A])
apply(blast)
done

theorem nlistE:
  "\<lbrakk> l:nlist[n]A;
    \<And>la. \<lbrakk> l:listn(A); l = <n, la>; n:nat; la:list(A) \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
apply(simp only: nlist_def)
apply(simp, erule conjE)
apply(erule exE)
apply(frule listn_sub, simp)
done

lemma nlist_is_Part: "nlist[n]A = Part(listn(A), %m. <n, m>)"
apply(simp add: nlist_def)
apply(insert Part_def[of "listn(A)" "%m. <n, m>"])
proof -
  assume a: "Part(listn(A), \<lambda>m. \<langle>n, m\<rangle>) \<equiv> {x \<in> listn(A) . \<exists>z. x = \<langle>n, z\<rangle>}"
  then have "Part(listn(A), \<lambda>m. \<langle>n, m\<rangle>) = {p \<in> listn(A) . \<exists>z. p = \<langle>n, z\<rangle>}" by simp
  then show "{p \<in> listn(A) . \<exists>l. p = \<langle>n, l\<rangle>} = Part(listn(A), \<lambda>m. \<langle>n, m\<rangle>)" by simp
qed

theorem nlist_mono: "A \<subseteq> B \<Longrightarrow> nlist[n]A \<subseteq> nlist[n]B"
apply(subst nlist_is_Part)
apply(subst nlist_is_Part)
apply(rule Part_mono)
apply(rule listn_mono, simp)
done

theorem nlist_nat: "x:nlist[n]A \<Longrightarrow> n:nat"
apply(simp add: nlist_def)
apply(erule conjE)
apply(erule exE)
apply(drule listn_sub)
apply(simp)
done

theorem listn_append_induct_lemma:
  "\<lbrakk> <xa, x> : listn(A); P_listn(0, []);
    \<And>a n l. \<lbrakk> a:A; <n, l>: listn(A); P_listn(n, l); n:nat;
      l:list(A) \<rbrakk> \<Longrightarrow> P_listn(succ(n), l @ [a]) \<rbrakk> \<Longrightarrow> P_listn(xa, x)"
apply(insert listn_iff[of xa x A], simp, erule conjE)
apply(insert listn_iff[of _ _ A], simp)
apply(insert list_append_induct[of x A "%m. P_listn(length(m), m)"], simp)
done

theorem nnil_type: "nnil : nlist[0]A"
apply(simp add: nnil_def)
apply(simp add: nlist_is_Part)
apply(rule PartI)
apply(rule NilI)
done

theorem ncons_type: "\<lbrakk> l:nlist[n]A; a:A \<rbrakk> \<Longrightarrow> ncons(n, a, l):nlist[succ(n)]A"
apply(erule nlistE)
apply(simp add: nlist_is_Part ncons_def)
apply(rule PartI)
apply(rule ConsI, simp_all)
done

theorem napp_type:
  "\<lbrakk> la:nlist[na]A; lb:nlist[nb]A \<rbrakk>
    \<Longrightarrow> napp(na, nb, la, lb):nlist[na #+ nb]A"
apply(elim nlistE)
apply(rename_tac as bs)
apply(simp add: nlist_is_Part napp_def)
apply(rule PartI)
apply(rule listn_append, simp_all)
done

theorem nhd_type: "\<lbrakk> l:nlist[succ(n)]A \<rbrakk> \<Longrightarrow> nhd(l):A"
apply(elim nlistE)
apply(simp add: nhd_def)
apply(rule hd_type, simp)
apply(insert listn_iff[of "succ(n)"], simp)
done

theorem ntl_type: "\<lbrakk> l:nlist[n]A \<rbrakk> \<Longrightarrow> ntl(n, l):nlist[n #- 1]A"
apply(elim nlistE)
apply(simp add: nlist_is_Part ntl_def)
apply(rule PartI)
apply(subst listn_iff, auto)
apply(subst (asm) listn_iff)
apply(frule length_tl, simp)
done

theorem ntl_type2: "\<lbrakk> l:nlist[succ(n)]A \<rbrakk> \<Longrightarrow> ntl(succ(n), l):nlist[n]A"
apply(frule ntl_type)
apply(frule nlist_nat, simp)
done

theorem nlast_type: "\<lbrakk> l:nlist[succ(n)]A \<rbrakk> \<Longrightarrow> nlast(l):A"
apply(elim nlistE)
apply(simp add: nlast_def)
apply(rule hd_type)
apply(rule rev_type, simp)
apply(subst length_rev, auto)
apply(subst (asm) listn_iff, simp)
done

theorem nfront_type: "\<lbrakk> l:nlist[n]A \<rbrakk> \<Longrightarrow> nfront(n, l):nlist[n #- 1]A"
apply(elim nlistE)
apply(simp add: nlist_is_Part nfront_def)
apply(rule PartI)
apply(subst listn_iff, auto)
apply(subst (asm) listn_iff)
apply(insert length_front[of _ A], auto)
done

theorem nfront_type2: "\<lbrakk> l:nlist[succ(n)]A \<rbrakk> \<Longrightarrow> nfront(succ(n), l):nlist[n]A"
apply(frule nfront_type)
apply(frule nlist_nat, simp)
done

theorem nsnoc_type: "\<lbrakk> l:nlist[n]A; a:A \<rbrakk> \<Longrightarrow> nsnoc(n, l, a):nlist[succ(n)]A"
apply(erule nlistE)
apply(simp add: nlist_is_Part nsnoc_def napp_def ncons_def nnil_def)
apply(rule PartI)
apply(subst listn_iff, auto)
apply(subst (asm) listn_iff, auto)
done

theorem nnil_elem: "\<lbrakk> nnil:nlist[n]A; n=0 \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
apply(simp add: nnil_def)
apply(elim nlistE, auto)
done

theorem zero_nlist: "\<lbrakk> x:nlist[0]A; x=nnil \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
apply(elim nlistE)
apply(simp add: nnil_def)
apply(subst (asm) listn_iff, auto)
done

lemma cons_hd_tl: "\<lbrakk> x:list(A); 0 < length(x) \<rbrakk> \<Longrightarrow> x = Cons(hd(x), tl(x))"
apply(case_tac x, simp+)
done

theorem succ_nlist:
  "\<lbrakk> x:nlist[succ(n)]A;
    \<And>a l. \<lbrakk> a:A; l:nlist[n]A; x=ncons(n, a, l) \<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
apply(frule nhd_type)
apply(frule ntl_type)
apply(frule nlist_nat, simp)
apply(subgoal_tac "x = ncons(n, nhd(x), ntl(succ(n), x))", simp)
apply(elim nlistE)
apply(simp add: ncons_def nhd_def ntl_def listn_iff)
proof -
  fix la laa
  assume a: "la:list(A)" "tl(la) = laa" "length(la) = succ(n)"
  then have "0 < length(la)" by simp
  then have "la = Cons(hd(la), tl(la))" using cons_hd_tl[of la A] a by simp
  then show "la = Cons(hd(la), laa)" using a by simp
qed

lemma hd_length_gt_0: "x:list(A) \<Longrightarrow> 0 < length([hd(x)])"
apply(auto)
done

lemma app_front_last: "\<lbrakk> x:list(A)\<rbrakk> \<Longrightarrow> (x = [] \<longrightarrow> True) & (x \<noteq> [] \<longrightarrow> x = front(x) @ [hd(rev(x))])"
apply(erule list_append_induct, auto)
apply(frule rev_type)
apply(case_tac y, auto)
apply(subst app_Cons[THEN sym])
apply(rule front_app_end[THEN sym], auto)
apply(subst rev_app_distrib, auto)
done

theorem succ_nlist_app:
  "\<lbrakk> x:nlist[succ(n)]A;
    \<And> a l. \<lbrakk> a:A; l:nlist[n]A; x = nsnoc(n, l, a) \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
apply(frule nfront_type)
apply(frule nlast_type)
apply(frule nlist_nat, simp)
apply(subgoal_tac "x = nsnoc(n, nfront(succ(n), x), nlast(x))", simp)
apply(elim nlistE)
apply(simp add: nsnoc_def ncons_def napp_def nlast_def nnil_def nfront_def)
proof -
  fix la laa
  assume a: "la:list(A)" "front(la) = laa" "\<langle>succ(n), la\<rangle> : listn(A)"
  then have "length(la) = succ(n)" using listn_iff by simp
  then have "la ~= []" using a by(auto)
  then have "la = front(la) @ [hd(rev(la))]" using app_front_last[of la A] a by simp
  then show "la = laa @ [hd(rev(la))]" using a by simp
qed

theorem ncons_iff:
  "\<lbrakk> l:nlist[n]A; l':nlist[n]B \<rbrakk>
    \<Longrightarrow> (ncons(n, a, l) = ncons(n, a', l') \<longleftrightarrow> (l = l' & a = a'))"
apply(elim nlistE)
apply(simp add: ncons_def, auto)
done

theorem ncons_inject:
  "\<lbrakk> ncons(n, a, l) = ncons(n, a', l'); l:nlist[n]A; l':nlist[n]B;
    \<lbrakk> l = l'; a = a' \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
apply(frule ncons_iff[of l n A "l'" B], auto)
done

lemma ncons_n_iff_lemma: "\<lbrakk>l \<in> nlist[n]A; l' \<in> nlist[n']B; ncons(n, a, l) = ncons(n', a', l')\<rbrakk> \<Longrightarrow> n = n'"
apply(elim nlistE)
apply(simp add: ncons_def)
done

theorem ncons_iff2:
  "\<lbrakk> l:nlist[n]A; l':nlist[n']B \<rbrakk> \<Longrightarrow> (ncons(n, a, l) = ncons(n', a', l')) \<longleftrightarrow> (l = l' & a = a' & n = n')"
apply(auto)
apply(frule ncons_n_iff_lemma[of l n A "l'" "n'" B], auto)
apply(insert ncons_iff, auto)
apply(frule ncons_n_iff_lemma[of l n A "l'" "n'" B], auto)
apply(insert ncons_iff, auto)
apply(rule ncons_n_iff_lemma, auto)
done

theorem ncons_inject2:
  "\<lbrakk> ncons(n, a, l) = ncons(n', a', l'); l:nlist[n]A; l':nlist[n']B;
    \<lbrakk> l = l'; a = a'; n = n' \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
apply(frule ncons_iff2[of l n A "l'" "n'" B], auto)
done

theorem ncons_inj1: "\<lbrakk> ncons(n, a, l) = ncons(n, a', l') \<rbrakk> \<Longrightarrow> a = a'"
apply(simp add: ncons_def)
done

theorem ncons_inj2: "\<lbrakk> ncons(n, a, l) = ncons(n, a', l'); l:nlist[n]A; l':nlist[n]B \<rbrakk> \<Longrightarrow> l = l'"
apply(frule ncons_iff2[of l n A "l'" "n" B], auto)
done

theorem nsnoc_inject:
  "\<lbrakk> nsnoc(n, l, a) = nsnoc(n, l', a'); a:A; a':B; l:nlist[n]C; l':nlist[n]E;
    \<lbrakk> l = l'; a = a' \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
apply(simp add: nsnoc_def napp_def)
apply(elim nlistE, simp add: ncons_def nnil_def)
proof -
  fix la laa
  assume a: "la @ [a] = laa @ [a']" "la:list(C)" "laa:list(E)" "a:A" "a':B"
      and b: "\<lbrakk>la = laa; a = a'\<rbrakk> \<Longrightarrow> R"
  then have "rev(la @ [a]) = rev(laa @ [a'])" by simp
  then have "la = laa & a = a'" using rev_app_end[of la C laa E a A "a'" B] a by simp
  then show R using b by simp
qed

theorem nsnoc_iff:
  "\<lbrakk> l:nlist[n]A; l':nlist[n]B; a:C; a':E \<rbrakk> \<Longrightarrow>
    (nsnoc(n, l, a) = nsnoc(n, l', a')) \<longleftrightarrow> (l = l' & a = a')"
apply(auto)
apply(erule nsnoc_inject, auto)
apply(erule nsnoc_inject, auto)
done

theorem nhd_ncons: "l:nlist[n]A \<Longrightarrow> nhd(ncons(n, a, l)) = a"
apply(elim nlistE)
apply(simp add: nhd_def ncons_def)
done

theorem ntl_nnil: "ntl(0, nnil) = nnil"
apply(simp add: ntl_def nnil_def)
done

theorem ntl_ncons: "\<lbrakk> l:nlist[n]A \<rbrakk> \<Longrightarrow> ntl(succ(n), ncons(n, a, l)) = l"
apply(elim nlistE)
apply(simp add: ntl_def ncons_def)
done

theorem napp_nnil: "l:nlist[n]A \<Longrightarrow> napp(0, n, nnil, l) = l"
apply(elim nlistE)
apply(simp add: napp_def nnil_def)
done

theorem napp_ncons:
  "\<lbrakk> la:nlist[na]A; lb:nlist[nb]B \<rbrakk> \<Longrightarrow>
    napp(succ(na), nb, ncons(na, a, la), lb) = ncons(na #+ nb, a, napp(na, nb, la, lb))"
apply(elim nlistE)
apply(simp add: napp_def ncons_def )
done

theorem nfront_nnil: "nfront(0, nnil) = nnil"
apply(simp add: nfront_def nnil_def)
done

theorem nfront_ncons1: "nfront(1, ncons(0, a, nnil)) = nnil"
apply(simp add: nfront_def nnil_def ncons_def)
done

theorem nfront_ncons2: "nfront(succ(1), ncons(1, a, ncons(0, b, nnil))) = ncons(0, a, nnil)"
apply(simp add: nfront_def nnil_def ncons_def)
done

theorem nfront_napp_end:
  "\<lbrakk> l:nlist[n]A; a:A; b:A \<rbrakk>
    \<Longrightarrow> nfront(succ(n) #+ 1, nsnoc(succ(n), ncons(n, a, l), b)) = ncons(n, a, l)"
apply(elim nlistE)
apply(simp add: nfront_def nsnoc_def ncons_def nnil_def napp_def)
apply(subst app_Cons[THEN sym])
apply(rule front_app_end, auto)
done

theorem nfront_ncons3:
  "\<lbrakk> l:nlist[n]A; a:A; b:A \<rbrakk> \<Longrightarrow>
    nfront(succ(succ(n)), ncons(succ(n), a, ncons(n, b, l))) =
    ncons(n, a, nfront(succ(n), ncons(n, b, l)))"
apply(elim nlistE)
apply(simp add: nfront_def nsnoc_def ncons_def nnil_def napp_def)
done

theorem ncons_nsnoc: "a:A \<Longrightarrow> ncons(0, a, nnil) = nsnoc(0, nnil, a)"
apply(simp add: ncons_def nsnoc_def nnil_def napp_def)
done

theorem nsnoc_nfront_nlast:
  "\<lbrakk> l:nlist[n]A; a:A \<rbrakk>
    \<Longrightarrow> nsnoc(n, nfront(succ(n), ncons(n, a, l)), nlast(ncons(n, a, l))) = ncons(n, a, l)"
apply(elim nlistE)
apply(simp add: nsnoc_def nfront_def ncons_def napp_def nnil_def)
apply(unfold nlast_def snd_conv)
apply(insert app_front_last[of "Cons(a, _)"], auto)
done

theorem nnth_type: "\<lbrakk> 0 < n; l:nlist[n]A; i:nats(n) \<rbrakk> \<Longrightarrow> nnth(i, l):A"
apply(elim nlistE)
apply(simp add: nnth_def)
apply(rule hd_type)
apply(rule drop_type, auto)
apply(subst (asm) listn_iff, simp)
done

theorem nnth_0_nsnoc: "p:A \<Longrightarrow> nnth(0, nsnoc(0, nnil, p)) = p"
apply(simp add: nnth_def nsnoc_def nnil_def napp_def ncons_def)
done

theorem nnth_nsnoc: "\<lbrakk> l:nlist[n]A; a:A \<rbrakk> \<Longrightarrow> nnth(n, nsnoc(n, l, a)) = a"
apply(elim nlistE)
apply(simp add: nnth_def nsnoc_def nnil_def napp_def ncons_def)
apply(subst (asm) listn_iff, simp)
apply(subst drop_append, auto)
done

theorem nnth_nsnoc_lt: "\<lbrakk> l:nlist[n]A; a:A; j < n \<rbrakk> \<Longrightarrow> nnth(j, nsnoc(n, l, a)) = nnth(j, l)"
apply(elim nlistE)
apply(simp add: nnth_def nsnoc_def nnil_def napp_def ncons_def)
apply(subst (asm) listn_iff, simp)
apply(subgoal_tac "j:nat")
apply(subst drop_append[of j _ A], auto)
apply(subgoal_tac "j #- length(la) = 0", auto)
apply(rule hd_append, auto)
apply(subgoal_tac "\<exists>z zs. drop(j, la) = Cons(z, zs)", simp)
apply(rule drop_length[of _ A], simp)
apply(erule ltD)
apply(rule nat_lt_imp_diff_eq_0, auto)
apply(rule lt_nat_in_nat, simp+)
done

theorem nbuild_type: "\<lbrakk> n:nat; \<And>j. j:nat \<Longrightarrow> p(j):A \<rbrakk> \<Longrightarrow> nbuild(n, p):nlist[n]A"
apply(subst nlist_is_Part)
apply(simp add: nbuild_def)
apply(rule rec_type[of n _ "%m. Part(listn(A), Pair(m))"], auto)
apply(subst nlist_is_Part[THEN sym], simp add: nnil_type)
apply(subst nlist_is_Part[THEN sym])
apply(rule nsnoc_type)
apply(subst nlist_is_Part)
apply(rule PartI, simp+)
done

theorem build_0: "nbuild(0, p) = nnil"
apply(simp add: nbuild_def)
done

theorem build_succ: "nbuild(succ(n), p) = nsnoc(n, nbuild(n, p), p(n))"
apply(simp add: nbuild_def)
done

lemma nbuild_def_equality: "nbuild(n, p) = rec(n, nnil, \<lambda>m r. nsnoc(m, r, p(m)))"
apply(simp add: nbuild_def)
done

theorem build_succ_lt:
  "\<lbrakk> 0 < n; j < n; n:nat; \<And>j. j:nat \<Longrightarrow> p(j):A \<rbrakk>
    \<Longrightarrow> nnth(j, nbuild(succ(n), p)) = nnth(j, nbuild(n, p))"
apply(simp add: nbuild_def)
apply(insert nnth_nsnoc_lt[of "rec(n, nnil, \<lambda>m r. nsnoc(m, r, p(m)))" "n" A "p(n)" j])
apply(subgoal_tac "rec(n, nnil, \<lambda>m r. nsnoc(m, r, p(m))) \<in> nlist[n]A")
apply(frule leI) back
apply(simp)
apply(insert nbuild_def_equality[of n p, THEN sym], simp)
apply(rule nbuild_type, simp+)
done

theorem build_succ_eq:
  "\<lbrakk> n:nat; \<And>j. j:nat \<Longrightarrow> p(j):A \<rbrakk>
    \<Longrightarrow> nnth(n, nbuild(succ(n), p)) = p(n)"
apply(simp add: nbuild_def)
apply(rule nnth_nsnoc)
apply(insert nbuild_def_equality[of n p, THEN sym], simp)
apply(rule nbuild_type, auto)
done

lemma nnth_build_lemma:
  "\<lbrakk> n:nat; \<And>j. j:nat \<Longrightarrow> p(j):A \<rbrakk>
    \<Longrightarrow> (n \<le> j \<longrightarrow> True) & (j < n \<longrightarrow>nnth(j, nbuild(n, p)) = p(j))"
apply(induct_tac n, simp_all)
apply(rule impI)
apply(insert le_iff[of j ], simp, erule disjE)
apply(simp)
proof -
  fix x
  assume a: "\<And>j. j \<in> nat \<Longrightarrow> p(j) \<in> A" "x \<in> nat" "j < x"
    and b: "nnth(j, nbuild(x, p)) = p(j)"
  then have "0 < x" using lt_imp_0_lt[of j x] by simp
  then have "nnth(j, nbuild(succ(x), p)) = nnth(j, nbuild(x, p))"
    using build_succ_lt[of x j p A] using a by simp
  then show "nnth(j, nbuild(succ(x), p)) = p(j)" using b by simp
next
  fix x
  assume a: "\<And>j. j \<in> nat \<Longrightarrow> p(j) \<in> A" "x \<in> nat" "j = x"
  then have "nnth(x, nbuild(succ(x), p)) = p(x)" using build_succ_eq[of x p A] by simp
  then show "nnth(j, nbuild(succ(x), p)) = p(j)" using a by simp
qed

theorem nnth_build:
  "\<lbrakk> n:nat; 0 < n; j:nats(n); \<And>j. j:nat \<Longrightarrow> p(j):A \<rbrakk>
    \<Longrightarrow> nnth(j, nbuild(n, p)) = p(j)"
apply(simp)
apply(frule nnth_build_lemma[of n p A j], simp+)
done

lemma nnth_nlist_lemma:
  "n:nat \<Longrightarrow> ALL xa x. ( 0 < n & xa:nlist[n]A & x:nlist[n]A &
    (ALL j:nats(n). nnth(j, xa) = nnth(j, x)) ) \<longrightarrow> xa = x"
apply(induct_tac n, simp)
apply(intro allI)
apply(rule impI)
apply(elim conjE)
apply(elim succ_nlist_app)
apply(simp only: nsnoc_iff)
apply(rule conjI)
apply(erule leE)
prefer 2
apply(simp)
apply(elim zero_nlist, simp)
proof -
  fix x xa xb a l aa la
  assume a: "x:nat" "0 < x" "a:A" "l:nlist[x]A" "aa:A" "la:nlist[x]A"
      and b: "xa = nsnoc(x, l, a)" "xb = nsnoc(x, la, aa)"
      and c: "\<forall>j\<in>nats(succ(x)). nnth(j, nsnoc(x, l, a)) = nnth(j, nsnoc(x, la, aa))"
      and h: "\<forall>xa xb. 0 < x \<and> xa \<in> nlist[x]A \<and> xb \<in> nlist[x]A \<and> (\<forall>j\<in>nats(x). nnth(j, xa) = nnth(j, xb)) \<longrightarrow> xa = xb"
  have d: "\<forall>j\<in>nat. j < succ(x) \<longrightarrow> nnth(j, nsnoc(x, l, a)) = nnth(j, nsnoc(x, la, aa))" using c by simp
  {
    fix j
    assume aa: "j:nat" "j < x"
    then have "j < succ(x)" using add_lt_larger_side_help[of x j 1] a by simp
    then have "nnth(j, nsnoc(x, l, a)) = nnth(j, nsnoc(x, la, aa))" using d aa by simp
    then have "nnth(j, l) = nnth(j, nsnoc(x, la, aa))"
      using nnth_nsnoc_lt[of l x A a j] aa a by simp
    then have "nnth(j, l) = nnth(j, la)"
      using nnth_nsnoc_lt[of la x A aa j] aa a by simp
  } then have "\<forall>j\<in>nats(x). nnth(j, l) = nnth(j, la)" by simp
  then show "l = la" using h a by(auto)
next
  fix x xa xb a l aa la
  assume a: "x:nat" "a:A" "l:nlist[x]A" "aa:A" "la:nlist[x]A"
      and b: "\<forall>j\<in>nats(succ(x)). nnth(j, nsnoc(x, l, a)) = nnth(j, nsnoc(x, la, aa))"
  then have "x < succ(x)" by simp
  then have "nnth(x, nsnoc(x, l, a)) = nnth(x, nsnoc(x, la, aa))" using b a by simp
  then have "a = nnth(x, nsnoc(x, la, aa))" using nnth_nsnoc[of l x A a] a by simp
  then show "a = aa" using nnth_nsnoc[of la x A aa] a by simp
qed

theorem nnth_nlist:
  "\<lbrakk> n:nat; 0 < n; xa:nlist[n]A; x:nlist[n]A;
    ALL j:nats(n). nnth(j, xa) = nnth(j, x) \<rbrakk> \<Longrightarrow> xa = x"
apply(insert nnth_nlist_lemma[of n A], blast)
done

theorem nhd_ntl: "\<lbrakk> l:nlist[succ(n)]A \<rbrakk> \<Longrightarrow> l = ncons(n, nhd(l), ntl(succ(n), l))"
apply(elim nlistE)
apply(simp add: ncons_def nhd_def ntl_def)
apply(rule cons_hd_tl[of _ A], simp)
apply(subst (asm) listn_iff, simp)
done

theorem nlist_into_univ: "\<lbrakk> l:nlist[n]A; A \<subseteq> univ(B) \<rbrakk> \<Longrightarrow> l:univ(B)"
apply(elim nlistE)
apply(drule list_into_univ, simp)
apply(insert nat_subset_univ[of B])
apply(subgoal_tac "n:univ(B)")
apply(subgoal_tac "<n, la>: univ(B) \<times> univ(B)")
apply(subgoal_tac "<n, la>: univ(B)")
apply(simp)
apply(insert product_univ[of B])
apply(insert subsetD[of "univ(B) \<times> univ(B)" "univ(B)" "<n, _>"], simp)
apply(simp)
apply(insert subsetD, simp)
done

theorem nnil_ncons_iff: "~nnil = ncons(n, a, l)"
apply(simp add: nnil_def ncons_def)
done

theorem nlistE2:
  "\<lbrakk> x:nlist[n]A; \<lbrakk> n = 0; x = nnil \<rbrakk> \<Longrightarrow> P;
    \<And> n' a l. \<lbrakk> x = ncons(n', a, l); n=succ(n'); a:A; l:nlist[n']A \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
apply(subgoal_tac "n = 0 | n ~= 0")
apply(erule disjE)
apply(simp_all)
apply(erule zero_nlist, simp)
apply(frule nlist_nat)
apply(case_tac n, simp)
apply(simp)
apply(erule succ_nlist, simp)
done

theorem nlist_n_eq_n': "\<lbrakk> l:nlist[n]A; l:nlist[n']A' \<rbrakk> \<Longrightarrow> n = n'"
apply(elim nlistE)
apply(simp)
done

lemmas nlist_types =
  ncons_type nnil_type napp_type nhd_type nsnoc_type
  ntl_type2 ntl_type nlast_type nfront_type2 nfront_type

lemmas Ruby_type =
  nlist_types

lemmas nlist_simps =
  nhd_ncons ntl_nnil ntl_ncons napp_nnil napp_ncons
  nfront_nnil nfront_ncons1 nfront_ncons2 nfront_ncons3

lemmas nlist_ss =
  nlist_simps nlist_types

declare nlist_ss [simp]

end


text:
(* Author: Tobias Nipkow *)

theory Abs_State_den
imports Abs_Int_den0_fun
  "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
  (* Library import merely to allow string lists to be sorted for output *)
begin

subsection "Abstract State with Computable Ordering"

text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}

datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"

fun "fun" where "fun (FunDom f _) = f"
fun dom where "dom (FunDom _ A) = A"

definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"

definition "list S = [(x,fun S x). x \<leftarrow> sort(dom S)]"

definition "lookup F x = (if x : set(dom F) then fun F x else Top)"

definition "update F x y =
  FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"

lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
by(rule ext)(auto simp: lookup_def update_def)

instantiation astate :: (SL_top) SL_top
begin

definition "le_astate F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"

definition
"join_astate F G =
 FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"

definition "Top = FunDom (\<lambda>x. Top) []"

instance
proof
  case goal2 thus ?case
    apply(auto simp: le_astate_def)
    by (metis lookup_def preord_class.le_trans top)
qed (auto simp: le_astate_def lookup_def join_astate_def Top_astate_def)

end

end

repo: isabelle