text:
(*  Title:      HOL/Auth/n_flash_nodata_cub_lemma_on_inv__41.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_nodata_cub Protocol Case Study*}

theory n_flash_nodata_cub_lemma_on_inv__41 imports n_flash_nodata_cub_base
begin
section{*All lemmas on causal relation between inv__41 and some rule r*}
lemma n_NI_Remote_Get_Nak_HomeVsinv__41:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Get_Nak_Home  dst)" and
a2: "(f=inv__41  )"
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
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Remote_Get_PutVsinv__41:
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: "(f=inv__41  )"
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
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Remote_Get_Put_HomeVsinv__41:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_Get_Put_Home  dst)" and
a2: "(f=inv__41  )"
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
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Remote_GetX_Nak_HomeVsinv__41:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_GetX_Nak_Home  dst)" and
a2: "(f=inv__41  )"
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
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Remote_GetX_PutXVsinv__41:
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: "(f=inv__41  )"
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
  have "?P3 s"
  apply (cut_tac a1 a2 , simp, rule_tac x="(neg (andForm (eqn (IVar (Field (Para (Field (Ident ''Sta'') ''Proc'') dst) ''CacheState'')) (Const CACHE_E)) (eqn (IVar (Field (Field (Ident ''Sta'') ''HomeUniMsg'') ''Cmd'')) (Const UNI_PutX))))" in exI, auto) done
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_Remote_GetX_PutX_HomeVsinv__41:
assumes a1: "(\<exists> dst. dst\<le>N\<and>r=n_NI_Remote_GetX_PutX_Home  dst)" and
a2: "(f=inv__41  )"
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
  have "?P3 s"
  apply (cut_tac a1 a2 , simp, rule_tac x="(neg (andForm (eqn (IVar (Field (Field (Ident ''Sta'') ''HomeUniMsg'') ''Cmd'')) (Const UNI_GetX)) (eqn (IVar (Field (Field (Ident ''Sta'') ''ShWbMsg'') ''Cmd'')) (Const SHWB_FAck))))" in exI, auto) done
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_PI_Local_Get_GetVsinv__41:
assumes a1: "(r=n_PI_Local_Get_Get  )" and
a2: "(f=inv__41  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  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__41:
assumes a1: "(r=n_PI_Local_GetX_GetX__part__0  )" and
a2: "(f=inv__41  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  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__41:
assumes a1: "(r=n_PI_Local_GetX_GetX__part__1  )" and
a2: "(f=inv__41  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  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__41:
assumes a1: "(r=n_NI_Nak_Home  )" and
a2: "(f=inv__41  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  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__41:
assumes a1: "(r=n_NI_Local_Put  )" and
a2: "(f=inv__41  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  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__41:
assumes a1: "(r=n_NI_Local_PutXAcksDone  )" and
a2: "(f=inv__41  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_FAckVsinv__41:
assumes a1: "(r=n_NI_FAck  )" and
a2: "(f=inv__41  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  have "?P1 s"
  proof(cut_tac a1 a2 , auto) qed
  then show "invHoldForRule s f r (invariants N)" by auto
qed

lemma n_NI_ShWbVsinv__41:
assumes a1: "(r=n_NI_ShWb N )" and
a2: "(f=inv__41  )"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
  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_Get_Get__part__1Vsinv__41:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_Local_Get_Get__part__1  src" and
  a2: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

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

lemma n_PI_Local_GetX_PutX__part__0Vsinv__41:
  assumes a1: "r=n_PI_Local_GetX_PutX__part__0  " and
  a2: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_WbVsinv__41:
  assumes a1: "r=n_NI_Wb  " and
  a2: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

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

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

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

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

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

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

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

lemma n_PI_Local_ReplaceVsinv__41:
  assumes a1: "r=n_PI_Local_Replace  " and
  a2: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

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

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

lemma n_NI_InvAck_existsVsinv__41:
  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: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

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

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

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

lemma n_PI_Local_PutXVsinv__41:
  assumes a1: "r=n_PI_Local_PutX  " and
  a2: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

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

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

lemma n_PI_Local_Get_PutVsinv__41:
  assumes a1: "r=n_PI_Local_Get_Put  " and
  a2: "(f=inv__41  )"
  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__41:
  assumes a1: "r=n_PI_Local_GetX_PutX_HeadVld__part__0 N " and
  a2: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

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

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

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

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

lemma n_NI_Remote_GetX_NakVsinv__41:
  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: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

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

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

lemma n_PI_Local_GetX_PutX__part__1Vsinv__41:
  assumes a1: "r=n_PI_Local_GetX_PutX__part__1  " and
  a2: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

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

lemma n_NI_Local_GetX_PutX_10Vsinv__41:
  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: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Local_GetX_PutX_8Vsinv__41:
  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: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

lemma n_NI_Local_GetX_PutX_8_NODE_GetVsinv__41:
  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: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

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

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

lemma n_NI_Replace_HomeVsinv__41:
  assumes a1: "r=n_NI_Replace_Home  " and
  a2: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

lemma n_NI_Remote_Get_NakVsinv__41:
  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: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_NI_Nak_ClearVsinv__41:
  assumes a1: "r=n_NI_Nak_Clear  " and
  a2: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

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

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

lemma n_NI_InvAck_2Vsinv__41:
  assumes a1: "\<exists> src. src\<le>N\<and>r=n_NI_InvAck_2 N src" and
  a2: "(f=inv__41  )"
  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__41:
  assumes a1: "r=n_PI_Local_GetX_PutX_HeadVld__part__1 N " and
  a2: "(f=inv__41  )"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

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

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

end

author: paraVerifier

repo: paraVerifier


text:
theory ex_LFIs
  imports topo_negation_conditions
begin
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)

section \<open>Example application: Logics of Formal Inconsistency (LFIs)\<close>
text\<open>\noindent{The LFIs \<^cite>\<open>LFI\<close> \<^cite>\<open>RLFI\<close> are a family of paraconsistent logics featuring a 'consistency'
operator @{text "\<^bold>\<circ>"} that can be used to recover some classical properties of negation (in particular ECQ).
We show how to semantically embed LFIs as extensions of Boolean algebras (here as frontier algebras).}\<close>

text\<open>\noindent{Logical validity can be defined as truth in all worlds/points (i.e. as denoting the top element)}\<close>
abbreviation gtrue::"\<sigma>\<Rightarrow>bool" ("[\<^bold>\<turnstile> _]") where  "[\<^bold>\<turnstile>  A] \<equiv> \<forall>w. A w"
lemma gtrue_def: "[\<^bold>\<turnstile> A] \<equiv> A \<^bold>\<approx> \<^bold>\<top>"  by (simp add: top_def)

text\<open>\noindent{When defining a logic over an existing algebra we have two choices: a global (truth preserving)
and a local (truth-degree preserving) notion of logical consequence. For LFIs we prefer the latter.}\<close>
abbreviation conseq_global1::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_ \<^bold>\<turnstile>\<^sub>g _]") where "[A \<^bold>\<turnstile>\<^sub>g B] \<equiv> [\<^bold>\<turnstile> A] \<longrightarrow> [\<^bold>\<turnstile> B]"
abbreviation conseq_global2::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_,_ \<^bold>\<turnstile>\<^sub>g _]") where "[A\<^sub>1, A\<^sub>2 \<^bold>\<turnstile>\<^sub>g B] \<equiv> [\<^bold>\<turnstile> A\<^sub>1] \<and> [\<^bold>\<turnstile> A\<^sub>2] \<longrightarrow> [\<^bold>\<turnstile> B]"
abbreviation conseq_global3::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_,_,_ \<^bold>\<turnstile>\<^sub>g _]") where "[A\<^sub>1, A\<^sub>2, A\<^sub>3 \<^bold>\<turnstile>\<^sub>g B] \<equiv> [\<^bold>\<turnstile> A\<^sub>1] \<and> [\<^bold>\<turnstile> A\<^sub>2] \<and> [\<^bold>\<turnstile> A\<^sub>3] \<longrightarrow> [\<^bold>\<turnstile> B]"
abbreviation conseq_local1::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_ \<^bold>\<turnstile> _]") where "[A \<^bold>\<turnstile> B] \<equiv> A \<^bold>\<preceq> B"
abbreviation conseq_local2::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_,_ \<^bold>\<turnstile> _]") where "[A\<^sub>1, A\<^sub>2 \<^bold>\<turnstile> B] \<equiv> A\<^sub>1 \<^bold>\<and> A\<^sub>2 \<^bold>\<preceq> B"
abbreviation conseq_local3::"\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool" ("[_,_,_ \<^bold>\<turnstile> _]") where "[A\<^sub>1, A\<^sub>2, A\<^sub>3 \<^bold>\<turnstile> B] \<equiv> A\<^sub>1 \<^bold>\<and> A\<^sub>2 \<^bold>\<and> A\<^sub>3 \<^bold>\<preceq> B"
(*add more as the need arises...*)

text\<open>\noindent{For LFIs we use the (paraconsistent) closure-based negation previously defined (taking frontier as primitive). }\<close>
abbreviation cneg::"\<sigma>\<Rightarrow>\<sigma>" ("\<^bold>\<not>") where "\<^bold>\<not>A \<equiv> \<^bold>\<not>\<^sup>CA"

text\<open>\noindent{In terms of the frontier operator the negation looks as follows:}\<close>
lemma "\<^bold>\<not>A \<^bold>\<approx> \<^bold>\<midarrow>A \<^bold>\<or> \<F>(\<^bold>\<midarrow>A)" by (simp add: neg_C_def pC2)
lemma cneg_prop: "Fr_2 \<F> \<Longrightarrow> \<^bold>\<not>A \<^bold>\<approx> \<^bold>\<midarrow>A \<^bold>\<or> \<F>(A)" using pC2 pF2 unfolding conn by blast

text\<open>\noindent{This negation is of course boldly paraconsistent.}\<close>
lemma "[a, \<^bold>\<not>a \<^bold>\<turnstile> b]" nitpick oops (*countermodel*)
lemma "[a, \<^bold>\<not>a \<^bold>\<turnstile> \<^bold>\<not>b]" nitpick oops (*countermodel*)
lemma "[a, \<^bold>\<not>a \<^bold>\<turnstile>\<^sub>g b]" nitpick oops (*countermodel*)
lemma "[a, \<^bold>\<not>a \<^bold>\<turnstile>\<^sub>g \<^bold>\<not>b]" nitpick oops (*countermodel*)

text\<open>\noindent{We define two pairs of in/consistency operators and show how they relate to each other.
Using LFIs terminology, the minimal logic so encoded corresponds to 'RmbC-ciw' (cf. \<^cite>\<open>RLFI\<close>).}\<close>
abbreviation op_inc_a::"\<sigma>\<Rightarrow>\<sigma>" ("\<bullet>\<^sup>A_" [57]58) where "\<bullet>\<^sup>AA \<equiv> A \<^bold>\<and> \<^bold>\<not>A"
abbreviation op_con_a::"\<sigma>\<Rightarrow>\<sigma>" ("\<^bold>\<circ>\<^sup>A_" [57]58) where "\<^bold>\<circ>\<^sup>AA \<equiv> \<^bold>\<midarrow>\<bullet>\<^sup>AA"
abbreviation op_inc_b::"\<sigma>\<Rightarrow>\<sigma>" ("\<bullet>\<^sup>B_" [57]58) where "\<bullet>\<^sup>BA \<equiv> \<B> A"
abbreviation op_con_b::"\<sigma>\<Rightarrow>\<sigma>" ("\<^bold>\<circ>\<^sup>B_" [57]58) where "\<^bold>\<circ>\<^sup>BA \<equiv> \<B>\<^sup>c A"

text\<open>\noindent{Observe that assumming condition Fr-2 are we allowed to exchange A and B variants.}\<close>
lemma pincAB: "Fr_2 \<F> \<Longrightarrow> \<bullet>\<^sup>AA \<^bold>\<approx> \<bullet>\<^sup>BA" using Br_fr_def Cl_fr_def pF2 conn by auto
lemma pconAB: "Fr_2 \<F> \<Longrightarrow> \<^bold>\<circ>\<^sup>AA \<^bold>\<approx> \<^bold>\<circ>\<^sup>BA" using pincAB unfolding conn by simp

text\<open>\noindent{Variants A and B give us slightly different properties.}\<close>
lemma Prop1: "\<^bold>\<circ>\<^sup>BA \<^bold>\<approx> \<I>\<^sup>f\<^sup>p A" using fp1 unfolding conn equal_op_def by metis
lemma "\<^bold>\<circ>\<^sup>AA \<^bold>\<approx> A \<^bold>\<rightarrow> \<I> A" nitpick oops (*countermodel*)
lemma Prop2: "Cl A \<longleftrightarrow> \<^bold>\<circ>\<^sup>A\<^bold>\<midarrow>A \<^bold>\<approx> \<^bold>\<top>" using pC2 unfolding conn by auto
lemma "Cl A \<longrightarrow> \<^bold>\<circ>\<^sup>B\<^bold>\<midarrow>A \<^bold>\<approx> \<^bold>\<top>" nitpick oops (*countermodel*)
lemma Prop3: "Cl A \<longleftrightarrow> \<bullet>\<^sup>A\<^bold>\<midarrow>A \<^bold>\<approx> \<^bold>\<bottom>" using Cl_fr_def unfolding conn by auto
lemma "Cl A \<longrightarrow> \<bullet>\<^sup>B\<^bold>\<midarrow>A \<^bold>\<approx> \<^bold>\<bottom>" nitpick oops (*countermodel*)
lemma Prop4: "Op A \<longleftrightarrow> \<^bold>\<circ>\<^sup>BA \<^bold>\<approx> \<^bold>\<top>" using Op_Bzero unfolding conn by simp
lemma "Op A \<longrightarrow> \<^bold>\<circ>\<^sup>AA \<^bold>\<approx> \<^bold>\<top>" nitpick oops (*countermodel*)
lemma Prop5: "Op A \<longleftrightarrow> \<bullet>\<^sup>BA \<^bold>\<approx> \<^bold>\<bottom>" using Op_Bzero by simp
lemma "Op A \<longrightarrow> \<bullet>\<^sup>AA \<^bold>\<approx> \<^bold>\<bottom>" nitpick oops (*countermodel*)

text\<open>\noindent{Importantly, LFIs must satisfy the so-called 'principle of gentle explosion'. Only variant A works here:}\<close>
lemma "[\<^bold>\<circ>\<^sup>Aa, a, \<^bold>\<not>a \<^bold>\<turnstile> b]" using compl_def meet_def by auto
lemma "[\<^bold>\<circ>\<^sup>Aa, a, \<^bold>\<not>a \<^bold>\<turnstile>\<^sub>g b]" using compl_def meet_def by auto
lemma "[\<^bold>\<circ>\<^sup>Ba, a, \<^bold>\<not>a \<^bold>\<turnstile> b]" nitpick oops (*countermodel*)
lemma "[\<^bold>\<circ>\<^sup>Ba, a, \<^bold>\<not>a \<^bold>\<turnstile>\<^sub>g b]" nitpick oops (*countermodel*)

text\<open>\noindent{In what follows we employ the (minimal) A-variant and verify some properties.}\<close>
abbreviation op_inc :: "\<sigma>\<Rightarrow>\<sigma>" ("\<bullet>_" [57]58) where "\<bullet>A  \<equiv> \<bullet>\<^sup>AA"
abbreviation op_con :: "\<sigma>\<Rightarrow>\<sigma>" ("\<^bold>\<circ>_" [57]58) where "\<^bold>\<circ>A  \<equiv> \<^bold>\<midarrow>\<bullet>A"

lemma "TND(\<^bold>\<not>)" by (simp add: TND_C)
lemma "ECQm(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> LNC(\<^bold>\<not>)" by (simp add: LNC_C PF6)
lemma "\<FF> \<F> \<Longrightarrow> DNI(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "\<FF> \<F> \<Longrightarrow> DNE(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> CoPw(\<^bold>\<not>)" by (simp add: CoPw_C PF6)
lemma "\<FF> \<F> \<Longrightarrow> CoP1(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "\<FF> \<F> \<Longrightarrow> CoP2(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "\<FF> \<F> \<Longrightarrow> CoP3(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "Fr_1a \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> DM3(\<^bold>\<not>)" by (simp add: DM3_C)
lemma "\<FF> \<F> \<Longrightarrow> DM4(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "nNor(\<^bold>\<not>)" by (simp add: nNor_C)
lemma "Fr_3 \<F> \<Longrightarrow> nDNor(\<^bold>\<not>)" by (simp add: nDNor_C)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> MT0(\<^bold>\<not>)" by (simp add: MT0_C PF6)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> MT1(\<^bold>\<not>)" by (simp add: MT1_C PF6)
lemma "\<FF> \<F> \<Longrightarrow> MT2(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> Fr_3 \<F> \<Longrightarrow> MT3(\<^bold>\<not>)" using MT3_C by auto

text\<open>\noindent{We show how all local contraposition variants (lCoP) can be recovered using the consistency operator.
Observe that we can recover in the same way other (weaker) properties: CoP, MT and DNI/DNE (local \& global).}\<close>
lemma "\<FF> \<F> \<Longrightarrow> lCoPw(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma cons_lcop1: "[\<^bold>\<circ>b, a \<^bold>\<rightarrow> b \<^bold>\<turnstile> \<^bold>\<not>b \<^bold>\<rightarrow> \<^bold>\<not>a]" using Cl_fr_def conn by auto
lemma "\<FF> \<F> \<Longrightarrow> lCoP1(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma cons_lcop2: "[\<^bold>\<circ>b, a \<^bold>\<rightarrow> \<^bold>\<not>b \<^bold>\<turnstile> b \<^bold>\<rightarrow> \<^bold>\<not>a]" using Cl_fr_def conn by auto
lemma "\<FF> \<F> \<Longrightarrow> lCoP2(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma cons_lcop3: "[\<^bold>\<circ>b, \<^bold>\<not>a \<^bold>\<rightarrow> b \<^bold>\<turnstile> \<^bold>\<not>b \<^bold>\<rightarrow> a]" using Cl_fr_def conn by auto
lemma "\<FF> \<F> \<Longrightarrow> lCoP3(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma cons_lcop4: "[\<^bold>\<circ>b, \<^bold>\<not>a \<^bold>\<rightarrow> \<^bold>\<not>b \<^bold>\<turnstile> b \<^bold>\<rightarrow> a]" using Cl_fr_def conn by auto
text\<open>\noindent{Disjunctive syllogism (DS).}\<close>
lemma "\<FF> \<F> \<Longrightarrow> DS1(\<^bold>\<rightarrow>)(\<^bold>\<not>)" nitpick oops (*countermodel*)
lemma cons_ds1: "[\<^bold>\<circ>a, a \<^bold>\<or> b \<^bold>\<turnstile> \<^bold>\<not>a \<^bold>\<rightarrow> b]" using conn by auto
lemma "DS2(\<^bold>\<rightarrow>)(\<^bold>\<not>)" by (metis Cl_fr_def DS2_def compl_def impl_def join_def neg_C_def)
text\<open>\noindent{Further properties.}\<close>
lemma "[a \<^bold>\<and> \<^bold>\<not>a \<^bold>\<turnstile> \<^bold>\<not>(\<^bold>\<circ>a)]" by (simp add: pC2 conn)
lemma "\<FF> \<F> \<Longrightarrow> [\<^bold>\<not>(\<^bold>\<circ>a) \<^bold>\<turnstile> a \<^bold>\<and> \<^bold>\<not>a]" nitpick oops (* countermodel found *)
lemma "[\<^bold>\<circ>a \<^bold>\<turnstile> \<^bold>\<not>(a \<^bold>\<and> \<^bold>\<not>a)]" by (simp add: pC2 conn)
lemma "\<FF> \<F> \<Longrightarrow> [\<^bold>\<not>(a \<^bold>\<and> \<^bold>\<not>a) \<^bold>\<turnstile> \<^bold>\<circ>a]" nitpick oops (* countermodel found *)

text\<open>\noindent{The following axioms are commonly employed in the literature on LFIs to obtain stronger logics.
We explore under which conditions they can be assumed while keeping the logic boldly paraconsistent.}\<close>
abbreviation cf where "cf \<equiv> DNE(\<^bold>\<not>)"
abbreviation ce where "ce \<equiv> DNI(\<^bold>\<not>)"
abbreviation ciw where "ciw \<equiv> \<forall>P. [\<^bold>\<turnstile> \<^bold>\<circ>P \<^bold>\<or> \<bullet>P]"
abbreviation ci  where  "ci \<equiv> \<forall>P.  [\<^bold>\<not>(\<^bold>\<circ>P) \<^bold>\<turnstile> \<bullet>P]"
abbreviation cl  where  "cl \<equiv> \<forall>P.  [\<^bold>\<not>(\<bullet>P) \<^bold>\<turnstile> \<^bold>\<circ>P]"
abbreviation ca_conj where "ca_conj \<equiv> \<forall>P Q. [\<^bold>\<circ>P,\<^bold>\<circ>Q \<^bold>\<turnstile> \<^bold>\<circ>(P \<^bold>\<and> Q)]"
abbreviation ca_disj where "ca_disj \<equiv> \<forall>P Q. [\<^bold>\<circ>P,\<^bold>\<circ>Q \<^bold>\<turnstile> \<^bold>\<circ>(P \<^bold>\<or> Q)]"
abbreviation ca_impl where "ca_impl \<equiv> \<forall>P Q. [\<^bold>\<circ>P,\<^bold>\<circ>Q \<^bold>\<turnstile> \<^bold>\<circ>(P \<^bold>\<rightarrow> Q)]"
abbreviation ca where "ca \<equiv> ca_conj \<and> ca_disj \<and> ca_impl"

text\<open>\noindent{cf}\<close>
lemma "\<FF> \<F> \<Longrightarrow> cf" nitpick oops
lemma "\<FF> \<F> \<and> cf \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
text\<open>\noindent{ce}\<close>
lemma "\<FF> \<F> \<Longrightarrow> ce" nitpick oops
lemma "Fr_1 \<F> \<and> Fr_2 \<F> \<and> Fr_4 \<F> \<and> ce \<and> \<sim>ECQ(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> ce \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1a \<F> \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> ce \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> ce \<longrightarrow> ECQm(\<^bold>\<not>)" unfolding Defs  using CoP1_XCoP CoP1_def2 CoPw_C DNI_def ECQw_def PF6 XCoP_def2 by auto
text\<open>\noindent{ciw}\<close>
lemma ciw by (simp add:conn)
text\<open>\noindent{ci}\<close>
lemma "\<FF> \<F> \<Longrightarrow> ci" nitpick oops
lemma "\<FF> \<F> \<and> ci \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
text\<open>\noindent{cl}\<close>
lemma "\<FF> \<F> \<Longrightarrow> cl" nitpick oops
lemma "Fr_1 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cl \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1a \<F> \<and> Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cl \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> cl \<longrightarrow> ECQ(\<^bold>\<not>)" unfolding Defs  by (metis BC_rel Br_Border Br_cl_def bottom_def compl_def eq_ext' meet_def neg_C_def)
text\<open>\noindent{ca-conj/disj}\<close>
lemma "Fr_1a \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> ca_conj" using DM3_C DM3_def conn by auto
lemma "Fr_1b \<F> \<Longrightarrow> Fr_2 \<F> \<Longrightarrow> ca_disj" using ADDI_b_def MONO_ADDIb monI pB1 pincAB unfolding conn by metis
lemma "\<FF> \<F> \<Longrightarrow> ca_impl" nitpick oops
text\<open>\noindent{ca-impl}\<close>
lemma "ca_impl \<and> \<sim>ECQ(\<^bold>\<not>)" (*nitpick[satisfy]*) oops (*cannot find finite model*)
lemma "ca_impl \<longrightarrow> ECQm(\<^bold>\<not>)" oops (*nor proof yet*)
text\<open>\noindent{cf \& ci}\<close>
lemma "Fr_1 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cf \<and> ci \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cf \<and> ci \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1b \<F> \<and> Fr_2 \<F> \<and> cf \<and> ci \<and> \<sim>ECQ(\<^bold>\<not>)" (*nitpick[satisfy]*) oops (*cannot find finite model*)
lemma "\<FF> \<F> \<and> cf \<and> ci \<longrightarrow> ECQm(\<^bold>\<not>)" oops (*nor proof yet*)
text\<open>\noindent{cf \& cl}\<close>
lemma "Fr_1 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cf \<and> cl \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_2 \<F> \<and> Fr_3 \<F> \<and> Fr_4 \<F> \<and> cf \<and> cl \<and> \<sim>ECQm(\<^bold>\<not>)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1b \<F> \<and> Fr_2 \<F> \<and> cf \<and> cl \<longrightarrow> ECQ(\<^bold>\<not>)" unfolding Defs by (smt Br_fr_def Fr_1b_def Prop2 Prop3 pF3 cneg_prop conn)

end

author: isabelle-prover

repo: mirror-afp-devel


text:
(* Author: Alexander Maletzky *)

section \<open>Zariski Topology\<close>

theory Zariski_Topology
  imports Nullstellensatz
begin

text \<open>The Zariski topology on a vector space \<open>K^n\<close> is the topology where the closed sets are precisely
  the algebraic sets, i.e. sets of the form @{term "\<V> F"} for some set @{term F} of polynomials.\<close>

definition Zariski_open :: "'x set \<Rightarrow> ('x \<Rightarrow> 'a::comm_semiring_1) set \<Rightarrow> bool"
  where "Zariski_open X A \<longleftrightarrow> - A \<in> \<V> ` Pow P[X]"

lemma Zariski_openI: "A = - \<V> F \<Longrightarrow> F \<subseteq> P[X] \<Longrightarrow> Zariski_open X A"
  by (auto simp: Zariski_open_def)

lemma Zariski_openE:
  assumes "Zariski_open X A"
  obtains F where "F \<subseteq> P[X]" and "A = - \<V> F"
  using assms by (auto simp: Zariski_open_def)

lemma Zariski_open_UNIV: "Zariski_open UNIV A \<longleftrightarrow> - A \<in> range \<V>"
  by (simp add: Zariski_open_def)

interpretation Zariski: topological_space "(Zariski_open X :: ('x \<Rightarrow> 'a::idom) set \<Rightarrow> _)"
proof
  show "Zariski_open X (UNIV::(_ \<Rightarrow> 'a) set)"
  proof (rule Zariski_openI)
    have "\<V> {1::('x \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a} = \<V> (ideal {1})" by simp
    also have "\<dots> = \<V> UNIV"
      by (rule arg_cong[where f=\<V>]) (simp add: ideal_eq_UNIV_iff_contains_one ideal.span_base)
    finally show "UNIV = - \<V> {1::('x \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a}" by simp
  qed (simp add: one_in_Polys)
next
  fix A B :: "('x \<Rightarrow> 'a) set"
  assume "Zariski_open X A"
  then obtain FA where "FA \<subseteq> P[X]" and A: "A = - \<V> FA" by (rule Zariski_openE)
  assume "Zariski_open X B"
  then obtain FB where "FB \<subseteq> P[X]" and B: "B = - \<V> FB" by (rule Zariski_openE)
  show "Zariski_open X (A \<inter> B)"
  proof (rule Zariski_openI)
    have "A \<inter> B = - (\<V> FA \<union> \<V> FB)" by (simp add: A B)
    also have "\<V> FA \<union> \<V> FB = \<V> (case_prod (*) ` (FA \<times> FB))"
      by (auto simp: variety_of_def poly_eval_times)
    finally show "A \<inter> B = - \<V> (case_prod (*) ` (FA \<times> FB))" .
  next
    from \<open>FA \<subseteq> P[X]\<close> \<open>FB \<subseteq> P[X]\<close> show "case_prod (*) ` (FA \<times> FB) \<subseteq> P[X]"
      by (auto intro: Polys_closed_times)
  qed
next
  fix K :: "('x \<Rightarrow> 'a) set set"
  assume *: "\<forall>A\<in>K. Zariski_open X A"
  define F where "F = (\<lambda>A::('x \<Rightarrow> 'a) set. SOME F'. F' \<subseteq> P[X] \<and> A = - \<V> F')"
  have "F A \<subseteq> P[X] \<and> A = - \<V> (F A)" if "A \<in> K" for A
  proof -
    from * that have "Zariski_open X A" ..
    then obtain F' where "F' \<subseteq> P[X]" and "A = - \<V> F'" by (rule Zariski_openE)
    hence "F' \<subseteq> P[X] \<and> A = - \<V> F'" ..
    thus ?thesis unfolding F_def by (rule someI)
  qed
  hence F_sub: "F A \<subseteq> P[X]" and A: "A = - \<V> (F A)" if "A \<in> K" for A using that by simp_all
  show "Zariski_open X (\<Union> K)"
  proof (rule Zariski_openI)
    from A have "\<Union> K = - \<Inter> ((\<V> \<circ> F) ` K)" by auto
    also have "\<Inter> ((\<V> \<circ> F) ` K) = \<V> (\<Union> (F ` K))" by (auto simp: variety_of_def)
    finally show "\<Union> K = - \<V> (\<Union> (F ` K))" .
  next
    from F_sub show "\<Union> (F ` K) \<subseteq> P[X]" by auto
  qed
qed

lemma Zariski_closed_alt: "Zariski.closed X A \<longleftrightarrow> A \<in> \<V> ` Pow P[X]"
  by (simp add: Zariski.closed_def Zariski_open_def)

lemma Zariski_closedI: "A = \<V> F \<Longrightarrow> F \<subseteq> P[X] \<Longrightarrow> Zariski.closed X A"
  by (auto simp: Zariski_closed_alt)

lemma Zariski_closedE:
  assumes "Zariski.closed X A"
  obtains F where "F \<subseteq> P[X]" and "A = \<V> F"
  using assms by (auto simp: Zariski_closed_alt)

lemma Zariski_closed_singleton: "Zariski.closed UNIV {a::'x \<Rightarrow> 'a::idom}"
proof -
  define F where "F = range (\<lambda>x::'x. monomial 1 (Poly_Mapping.single x (1::nat)) - monomial (a x) 0)"
  show ?thesis
  proof (rule Zariski_closedI)
    have "a \<in> \<V> F" by (rule variety_ofI) (auto simp: F_def poly_eval_minus poly_eval_monomial)
    moreover have "b = a" if "b \<in> \<V> F" for b
    proof (rule ccontr)
      assume "b \<noteq> a"
      then obtain x where "b x \<noteq> a x" by blast
      have "monomial 1 (Poly_Mapping.single x 1) - monomial (a x) 0 \<in> F"
        by (simp add: F_def)
      with that have "poly_eval b (monomial 1 (Poly_Mapping.single x 1) - monomial (a x) 0) = 0"
        by (rule variety_ofD)
      with \<open>b x \<noteq> a x\<close> show False by (simp add: poly_eval_minus poly_eval_monomial)
    qed
    ultimately show "{a} = \<V> F" by blast
  qed simp
qed

interpretation Zariski: t1_space "(Zariski_open UNIV :: ('x \<Rightarrow> 'a::idom) set \<Rightarrow> _)"
proof
  fix a b :: "'x \<Rightarrow> 'a"
  assume "a \<noteq> b"
  show "\<exists>U. Zariski_open UNIV U \<and> a \<in> U \<and> b \<notin> U"
  proof (intro exI conjI)
    show "Zariski_open UNIV (- {b})" by (simp add: Zariski.open_closed Zariski_closed_singleton)
  next
    from \<open>a \<noteq> b\<close> show "a \<in> - {b}" by simp
  qed simp
qed

interpretation Zariski: t2_space "(Zariski_open UNIV :: ('x::finite \<Rightarrow> 'a::{finite,idom}) set \<Rightarrow> _)"
proof
  fix a b :: "'x \<Rightarrow> 'a"
  assume "a \<noteq> b"
  show "\<exists>U V. Zariski_open UNIV U \<and> Zariski_open UNIV V \<and> a \<in> U \<and> b \<in> V \<and> U \<inter> V = {}"
  proof (intro exI conjI)
    show "Zariski_open UNIV (- (\<Union>c\<in>{c'. c' \<noteq> a}. {c}))"
      by (intro Zariski.open_Compl Zariski.closed_UN Zariski_closed_singleton ballI) simp
  next
    show "Zariski_open UNIV (- (\<Union>c\<in>{c'. c' \<noteq> b}. {c}))"
      by (intro Zariski.open_Compl Zariski.closed_UN Zariski_closed_singleton ballI) simp
  next
    from \<open>a \<noteq> b\<close> show "- (\<Union>c\<in>{c'. c' \<noteq> a}. {c}) \<inter> - (\<Union>c\<in>{c'. c' \<noteq> b}. {c}) = {}" by blast
  qed simp_all
qed

lemma Zariski_closure: "\<V> (\<I> A \<inter> P[X]) = (\<Inter> {C. Zariski.closed X C \<and> A \<subseteq> C})" (is "?L = ?R")
proof
  have "A \<subseteq> ?R" by blast
  have "Zariski.closed X ?R" by (rule Zariski.closed_Inter) simp
  then obtain F where "F \<subseteq> P[X]" and R: "?R = \<V> F" by (rule Zariski_closedE)
  from \<open>A \<subseteq> _\<close> have A_sub: "A \<subseteq> \<V> F" by (simp only: R)
  have "F \<subseteq> \<I> A"
  proof (intro subsetI ideal_ofI)
    fix f a
    assume "a \<in> A"
    with A_sub have "a \<in> \<V> F" ..
    moreover assume "f \<in> F"
    ultimately show "poly_eval a f = 0" by (rule variety_ofD)
  qed
  with \<open>F \<subseteq> P[X]\<close> have "F \<subseteq> \<I> A \<inter> P[X]" by blast
  thus "?L \<subseteq> ?R" unfolding R by (rule variety_of_antimono)
next
  from refl have "Zariski.closed X ?L" by (rule Zariski_closedI) simp
  moreover have "A \<subseteq> ?L" by (meson Int_lower1 ideal_ofD subset_eq variety_ofI)
  ultimately show "?R \<subseteq> ?L" by blast
qed

end (* theory *)

author: amaletzk

repo: Isabelle-Groebner


text:
(*  Title:      HOL/MicroJava/BV/Kildall.thy
    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM

Kildall's algorithm.
*)

section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>

theory Kildall_1
imports SemilatAlg
begin

primrec merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list"
where
  "merges f []      \<tau>s = \<tau>s"
| "merges f (p'#ps) \<tau>s = (let (p,\<tau>) = p' in merges f ps (\<tau>s[p := \<tau> \<squnion>\<^bsub>f\<^esub> \<tau>s!p]))"

lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric]

lemma (in Semilat) nth_merges:
 "\<And>ss. \<lbrakk>p < length ss; ss \<in> nlists n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
  (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] \<Squnion>\<^bsub>f\<^esub> ss!p"
  (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
(*<*)
proof (induct ps)
  show "\<And>ss. ?P ss []" by simp

  fix ss p' ps'
  assume ss: "ss \<in> nlists n A"
  assume l:  "p < length ss"
  assume "?steptype (p'#ps')"
  then obtain a b where
    p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and ps': "?steptype ps'"
    by (cases p') auto
  assume "\<And>ss. p< length ss \<Longrightarrow> ss \<in> nlists n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"
  hence IH: "\<And>ss. ss \<in> nlists n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" using ps' by iprover

  from ss ab
  have "ss[a := b \<squnion>\<^bsub>f\<^esub> ss!a] \<in> nlists n A" by (simp add: closedD)
  moreover
  with l have "p < length (ss[a := b \<squnion>\<^bsub>f\<^esub> ss!a])" by simp
  ultimately
  have "?P (ss[a := b \<squnion>\<^bsub>f\<^esub> ss!a]) ps'" by (rule IH)
  with p' l
  show "?P ss (p'#ps')" by simp
qed
(*>*)

(** merges **)

lemma length_merges [simp]:
  "\<And>ss. size(merges f ps ss) = size ss"
(*<*) by (induct ps, auto) (*>*)

lemma (in Semilat) merges_preserves_type_lemma:
shows "\<forall>xs. xs \<in> nlists n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
         \<longrightarrow> merges f ps xs \<in> nlists n A"
(*<*)
apply (insert closedI)
apply (unfold closed_def)
apply (induct ps)
 apply simp
apply clarsimp
done
(*>*)

lemma (in Semilat) merges_preserves_type [simp]:
 "\<lbrakk> xs \<in> nlists n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
  \<Longrightarrow> merges f ps xs \<in> nlists n A"
by (simp add: merges_preserves_type_lemma)

lemma (in Semilat) list_update_le_listI [rule_format]:
  "set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<longrightarrow> p < size xs \<longrightarrow>
   x \<sqsubseteq>\<^bsub>r\<^esub> ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x \<squnion>\<^bsub>f\<^esub> xs!p] [\<sqsubseteq>\<^bsub>r\<^esub>] ys"
(*<*)
  apply (insert semilat)
  apply (simp only: Listn.le_def lesub_def semilat_def)
  apply (simp add: list_all2_conv_all_nth nth_list_update)
  done
(*>*)

lemma (in Semilat) merges_pres_le_ub:
  assumes "set ts \<subseteq> A"  "set ss \<subseteq> A"
    "\<forall>(p,t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts!p \<and> t \<in> A \<and> p < size ts"  "ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts"
  shows "merges f ps ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts"
(*<*)
proof -
  { fix t ts ps
    have
    "\<And>qs. \<lbrakk>set ts \<subseteq> A; \<forall>(p,t)\<in>set ps. t \<sqsubseteq>\<^bsub>r\<^esub> ts!p \<and> t \<in> A \<and> p< size ts \<rbrakk> \<Longrightarrow>
    set qs \<subseteq> set ps  \<longrightarrow>
    (\<forall>ss. set ss \<subseteq> A \<longrightarrow> ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts \<longrightarrow> merges f qs ss [\<sqsubseteq>\<^bsub>r\<^esub>] ts)"
    apply (induct_tac qs)
     apply simp
    apply (simp (no_asm_simp))
    apply clarify
    apply simp
    apply (erule allE, erule impE, erule_tac [2] mp)
     apply (drule bspec, assumption)
     apply (simp add: closedD)
    apply (drule bspec, assumption)
    apply (simp add: list_update_le_listI)
    done
  } note this [dest]
  from assms show ?thesis by blast
qed
(*>*)

end


text:
(*  Title:       TLList_CCPO_Examples.thy
    Author:      Andreas Lochbihler, ETH Zurich
*)

header {* Example definitions using the CCPO structure on terminated lazy lists *}

theory TLList_CCPO_Examples imports
   "../TLList_CCPO"
begin

context fixes b :: 'b begin
interpretation tllist_pf b .

context fixes P :: "'a \<Rightarrow> bool" begin

partial_function (tllist) tfilter :: "('a, 'b) tllist \<Rightarrow> ('a, 'b) tllist"
where
  "tfilter xs = (case xs of TNil b' \<Rightarrow> TNil b' | TCons x xs' \<Rightarrow> if P x then TCons x (tfilter xs') else tfilter xs')"

end

simps_of_case tfilter_simps [simp]: tfilter.simps

lemma is_TNil_tfilter: "is_TNil (tfilter P xs) \<longleftrightarrow> (\<forall>x \<in> tset xs. \<not> P x)" (is "?lhs \<longleftrightarrow> ?rhs")
proof(rule iffI ballI)+
  fix x
  assume "x \<in> tset xs" ?lhs
  thus "\<not> P x"
  proof(induct rule: tllist_set_induct)
    case (find xs)
    thus ?case by(cases xs)(simp_all split: split_if_asm)
  next
    case (step xs x)
    thus ?case by(cases xs)(simp_all split: split_if_asm)
  qed
next
  assume ?rhs
  thus ?lhs
    by(induct arbitrary: xs rule: tfilter.fixp_induct)(simp_all split: tllist.split)
qed

end

lemma mcont2mcont_tfilter[THEN tllist.mcont2mcont, simp, cont_intro]:
  shows mcont_tfilter: "mcont (tSup b) (tllist_ord b) (tSup b) (tllist_ord b) (tfilter b P)"
apply(rule tllist.fixp_preserves_mcont1[OF tfilter.mono tfilter_def])
apply(rule mcont_lprefix_case_aux)
apply simp_all
done

lemma tfilter_tfilter:
  "tfilter b P (tfilter b Q xs) = tfilter b (\<lambda>x. P x \<and> Q x) xs" (is "?lhs xs = ?rhs xs")
proof(rule tllist.leq_antisym)
  have "\<forall>xs. tllist_ord b (?lhs xs) (?rhs xs)"
    by(rule tfilter.fixp_induct[where Pa="\<lambda>f. \<forall>xs. tllist_ord b (tfilter b P (f xs)) (?rhs xs)"])(auto split: tllist.split)
  thus "tllist_ord b (?lhs xs) (?rhs xs)" ..

  have "\<forall>xs. tllist_ord b (?rhs xs) (?lhs xs)"
    by(rule tfilter.fixp_induct[where Pa="\<lambda>f. \<forall>xs. tllist_ord b (f xs) (?lhs xs)"])(auto split: tllist.split)
  thus "tllist_ord b (?rhs xs) (?lhs xs)" ..
qed

declare ccpo.admissible_leI[OF complete_lattice_ccpo, cont_intro, simp]

lemma tset_tfilter: "tset (tfilter b P xs) = {x\<in>tset xs. P x}"
proof(rule equalityI[OF _ subsetI])
  show "tset (tfilter b P xs) \<subseteq> {x \<in> tset xs. P x}"
    by(induct arbitrary: xs rule: tfilter.fixp_induct)(auto split: tllist.split)
  fix x
  assume "x \<in> {x \<in> tset xs. P x}"
  hence "x \<in> tset xs" "P x" by simp_all
  thus "x \<in> tset (tfilter b P xs)"
    by(induct rule: tset_induct) simp_all
qed

context fixes b :: 'b begin
interpretation tllist_pf b .

partial_function (tllist) tconcat :: "('a llist, 'b) tllist \<Rightarrow> ('a, 'b) tllist"
where
  "tconcat xs = (case xs of TNil b \<Rightarrow> TNil b | TCons x xs' \<Rightarrow> lappendt x (tconcat xs'))"

end

simps_of_case tconcat2_simps [simp]: tconcat.simps

end

author: Josh-Tilles

repo: AFP

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


text:
(*
  Title:  Example Completeness Proof for a Propositional Sequent Calculus
  Author: Asta Halkjær From
*)

chapter \<open>Example: Propositional Sequent Calculus\<close>

theory Example_Propositional_SC imports Derivations begin

section \<open>Syntax\<close>

datatype 'p fm
  = Fls (\<open>\<^bold>\<bottom>\<close>)
  | Pro 'p (\<open>\<^bold>\<ddagger>\<close>)
  | Imp \<open>'p fm\<close> \<open>'p fm\<close> (infixr \<open>\<^bold>\<longrightarrow>\<close> 55)

abbreviation Neg (\<open>\<^bold>\<not> _\<close> [70] 70) where \<open>\<^bold>\<not> p \<equiv> p \<^bold>\<longrightarrow> \<^bold>\<bottom>\<close>

section \<open>Semantics\<close>

type_synonym 'p model = \<open>'p \<Rightarrow> bool\<close>

fun semantics :: \<open>'p model \<Rightarrow> 'p fm \<Rightarrow> bool\<close> (\<open>\<lbrakk>_\<rbrakk>\<close>) where
  \<open>\<lbrakk>_\<rbrakk> \<^bold>\<bottom> \<longleftrightarrow> False\<close>
| \<open>\<lbrakk>I\<rbrakk> (\<^bold>\<ddagger>P) \<longleftrightarrow> I P\<close>
| \<open>\<lbrakk>I\<rbrakk> (p \<^bold>\<longrightarrow> q) \<longleftrightarrow> \<lbrakk>I\<rbrakk> p \<longrightarrow> \<lbrakk>I\<rbrakk> q\<close>

section \<open>Calculus\<close>

inductive Calculus :: \<open>'p fm list \<Rightarrow> 'p fm list \<Rightarrow> bool\<close> (\<open>_ \<turnstile>\<^sub>S _\<close> [50, 50] 50) where
  Axiom [intro]: \<open>p # A \<turnstile>\<^sub>S p # B\<close>
| FlsL [intro]: \<open>\<^bold>\<bottom> # A \<turnstile>\<^sub>S B\<close>
| FlsR [dest]: \<open>A \<turnstile>\<^sub>S \<^bold>\<bottom> # B \<Longrightarrow> A \<turnstile>\<^sub>S B\<close>
| ImpL [intro]: \<open>A \<turnstile>\<^sub>S p # B \<Longrightarrow> q # A \<turnstile>\<^sub>S B \<Longrightarrow> (p \<^bold>\<longrightarrow> q) # A \<turnstile>\<^sub>S B\<close>
| ImpR [intro]: \<open>p # A \<turnstile>\<^sub>S q # B \<Longrightarrow> A \<turnstile>\<^sub>S (p \<^bold>\<longrightarrow> q) # B\<close>
| Cut [elim]: \<open>A \<turnstile>\<^sub>S p # B \<Longrightarrow> p # C \<turnstile>\<^sub>S D \<Longrightarrow> A @ C \<turnstile>\<^sub>S B @ D\<close>
| WeakenL: \<open>A \<turnstile>\<^sub>S B \<Longrightarrow> set A \<subseteq> set A' \<Longrightarrow> A' \<turnstile>\<^sub>S B\<close>
| WeakenR: \<open>A \<turnstile>\<^sub>S B \<Longrightarrow> set B \<subseteq> set B' \<Longrightarrow> A \<turnstile>\<^sub>S B'\<close>

lemma Boole: \<open>\<^bold>\<not> p # A \<turnstile>\<^sub>S [] \<Longrightarrow> A \<turnstile>\<^sub>S [p]\<close>
  by (metis Axiom Cut ImpR WeakenR append_self_conv2 self_append_conv set_subset_Cons)

section \<open>Soundness\<close>

theorem soundness: \<open>A \<turnstile>\<^sub>S B \<Longrightarrow> \<forall>q \<in> set A. \<lbrakk>I\<rbrakk> q \<Longrightarrow> \<exists>p \<in> set B. \<lbrakk>I\<rbrakk> p\<close>
  by (induct A B rule: Calculus.induct) auto

corollary soundness': \<open>[] \<turnstile>\<^sub>S [p] \<Longrightarrow> \<lbrakk>I\<rbrakk> p\<close>
  using soundness by fastforce

corollary \<open>\<not> ([] \<turnstile>\<^sub>S [])\<close>
  using soundness by fastforce

section \<open>Maximal Consistent Sets\<close>

definition consistent :: \<open>'p fm set \<Rightarrow> bool\<close> where
  \<open>consistent S \<equiv> \<nexists>S'. set S' \<subseteq> S \<and> S' \<turnstile>\<^sub>S [\<^bold>\<bottom>]\<close>

interpretation MCS_No_Saturation consistent
proof
  fix S S' :: \<open>'p fm set\<close>
  assume \<open>consistent S\<close> \<open>S' \<subseteq> S\<close>
  then show \<open>consistent S'\<close>
    unfolding consistent_def by fast
next
  fix S :: \<open>'p fm set\<close>
  assume \<open>\<not> consistent S\<close>
  then show \<open>\<exists>S'\<subseteq>S. finite S' \<and> \<not> consistent S'\<close>
    unfolding consistent_def by blast
next
  show \<open>infinite (UNIV :: 'p fm set)\<close>
    using infinite_UNIV_size[of \<open>\<lambda>p. p \<^bold>\<longrightarrow> p\<close>] by simp
qed

interpretation Derivations_MCS_Cut \<open>\<lambda>A p. A \<turnstile>\<^sub>S [p]\<close> consistent \<open>\<^bold>\<bottom>\<close>
proof
  fix A B and p :: \<open>'p fm\<close>
  assume \<open>A \<turnstile>\<^sub>S [p]\<close> \<open>set A \<subseteq> set B\<close>
  then show \<open>B \<turnstile>\<^sub>S [p]\<close>
    using WeakenL by blast
next
  fix S :: \<open>'p fm set\<close>
  show \<open>consistent S \<longleftrightarrow> (\<nexists>S'. set S' \<subseteq> S \<and> S' \<turnstile>\<^sub>S [\<^bold>\<bottom>])\<close>
    unfolding consistent_def ..
next
  fix A and p :: \<open>'p fm\<close>
  assume \<open>p \<in> set A\<close>
  then show \<open>A \<turnstile>\<^sub>S [p]\<close>
    by (metis Axiom WeakenL set_ConsD subsetI)
next
  fix A B and p q :: \<open>'p fm\<close>
  assume \<open>A \<turnstile>\<^sub>S [p]\<close> \<open>p # B \<turnstile>\<^sub>S [q]\<close>
  then show \<open>A @ B \<turnstile>\<^sub>S [q]\<close>
    using Cut by fastforce
qed

section \<open>Truth Lemma\<close>

abbreviation hmodel :: \<open>'p fm set \<Rightarrow> 'p model\<close> where
  \<open>hmodel H \<equiv> \<lambda>P. \<^bold>\<ddagger>P \<in> H\<close>

fun semics :: \<open>'p model \<Rightarrow> ('p model \<Rightarrow> 'p fm \<Rightarrow> bool) \<Rightarrow> 'p fm \<Rightarrow> bool\<close> where
  \<open>semics _ _ \<^bold>\<bottom> \<longleftrightarrow> False\<close>
| \<open>semics I _ (\<^bold>\<ddagger>P) \<longleftrightarrow> I P\<close>
| \<open>semics I rel (p \<^bold>\<longrightarrow> q) \<longleftrightarrow> rel I p \<longrightarrow> rel I q\<close>

fun rel :: \<open>'p fm set \<Rightarrow> 'p model \<Rightarrow> 'p fm \<Rightarrow> bool\<close> where
  \<open>rel H _ p = (p \<in> H)\<close>

theorem Hintikka_model':
  assumes \<open>\<And>p. semics (hmodel H) (rel H) p \<longleftrightarrow> p \<in> H\<close>
  shows \<open>p \<in> H \<longleftrightarrow> \<lbrakk>hmodel H\<rbrakk> p\<close>
proof (induct p rule: wf_induct[where r=\<open>measure size\<close>])
  case 1
  then show ?case ..
next
  case (2 x)
  then show ?case
    using assms[of x] by (cases x) simp_all
qed

lemma Hintikka_Extend:
  assumes \<open>consistent H\<close> \<open>maximal H\<close>
  shows \<open>semics (hmodel H) (rel H) p \<longleftrightarrow> p \<in> H\<close>
proof (cases p)
  case Fls
  have \<open>\<^bold>\<bottom> \<notin> H\<close>
    using assms MCS_derive consistent_def by blast
  then show ?thesis
    using Fls by simp
next
  case (Imp p q)
  have \<open>A \<turnstile>\<^sub>S [q] \<Longrightarrow> A \<turnstile>\<^sub>S [p \<^bold>\<longrightarrow> q]\<close> for A
    by (meson ImpR WeakenL set_subset_Cons)
  moreover have \<open>p # A \<turnstile>\<^sub>S [\<^bold>\<bottom>] \<Longrightarrow> A \<turnstile>\<^sub>S [p \<^bold>\<longrightarrow> q]\<close> for A
    by (meson FlsR ImpR WeakenR set_subset_Cons)
  moreover have \<open>A \<turnstile>\<^sub>S [p \<^bold>\<longrightarrow> q] \<Longrightarrow> B \<turnstile>\<^sub>S [p] \<Longrightarrow> A @ B \<turnstile>\<^sub>S [q]\<close> for A B
    using Cut by (metis Axiom ImpL append_Nil append_Nil2)
  ultimately have \<open>(p \<in> H \<longrightarrow> q \<in> H) \<longleftrightarrow> p \<^bold>\<longrightarrow> q \<in> H\<close>
    using assms MCS_derive MCS_derive_fls Axiom
    by (metis append_Cons append_Nil insert_subset list.simps(15))
  then show ?thesis
    using Imp by simp
qed simp

interpretation Truth_No_Saturation consistent semics semantics \<open>\<lambda>H. {hmodel H}\<close> rel
proof
  fix p and M :: \<open>'p model\<close>
  show \<open>\<lbrakk>M\<rbrakk> p \<longleftrightarrow> semics M semantics p\<close>
    by (induct p) auto
next
  fix p and H :: \<open>'p fm set\<close> and M :: \<open>'p model\<close>
  assume \<open>\<forall>M \<in> {hmodel H}. \<forall>p. semics M (rel H) p \<longleftrightarrow> rel H M p\<close> \<open>M \<in> {hmodel H}\<close>
  then show \<open>\<lbrakk>M\<rbrakk> p \<longleftrightarrow> rel H M p\<close>
    using Hintikka_model' by auto
next
  fix H :: \<open>'p fm set\<close>
  assume \<open>consistent H\<close> \<open>maximal H\<close>
  then show \<open>\<forall>M \<in> {hmodel H}. \<forall>p. semics M (rel H) p \<longleftrightarrow> rel H M p\<close>
    using Hintikka_Extend by auto
qed

section \<open>Completeness\<close>

theorem strong_completeness:
  assumes \<open>\<forall>M :: 'p model. (\<forall>q \<in> X. \<lbrakk>M\<rbrakk> q) \<longrightarrow> \<lbrakk>M\<rbrakk> p\<close>
  shows \<open>\<exists>A. set A \<subseteq> X \<and> A \<turnstile>\<^sub>S [p]\<close>
proof (rule ccontr)
  assume \<open>\<nexists>A. set A \<subseteq> X \<and> A \<turnstile>\<^sub>S [p]\<close>
  then have \<open>\<nexists>A. set A \<subseteq> X \<and> \<^bold>\<not> p # A \<turnstile>\<^sub>S []\<close>
    using Boole by blast
  then have \<open>\<nexists>A. set A \<subseteq> X \<and> \<^bold>\<not> p # A \<turnstile>\<^sub>S [\<^bold>\<bottom>]\<close>
    by fast
  then have *: \<open>\<nexists>A. set A \<subseteq> {\<^bold>\<not> p} \<union> X \<and> A \<turnstile>\<^sub>S [\<^bold>\<bottom>]\<close>
    using derive_split1 by blast

  let ?S = \<open>{\<^bold>\<not> p} \<union> X\<close>
  let ?H = \<open>Extend ?S\<close>

  have \<open>consistent ?S\<close>
    unfolding consistent_def using * by blast
  then have \<open>consistent ?H\<close> \<open>maximal ?H\<close>
    using MCS_Extend' by blast+
  then have \<open>p \<in> ?H \<longleftrightarrow> \<lbrakk>hmodel ?H\<rbrakk> p\<close> for p
    using truth_lemma_no_saturation by fastforce
  then have \<open>p \<in> ?S \<longrightarrow> \<lbrakk>hmodel ?H\<rbrakk> p\<close> for p
    using Extend_subset by blast
  then have \<open>\<lbrakk>hmodel ?H\<rbrakk> (\<^bold>\<not> p)\<close> \<open>\<forall>q \<in> X. \<lbrakk>hmodel ?H\<rbrakk> q\<close>
    by blast+
  moreover from this have \<open>\<lbrakk>hmodel ?H\<rbrakk> p\<close>
    using assms(1) by blast
  ultimately show False
    by simp
qed

abbreviation valid :: \<open>'p fm \<Rightarrow> bool\<close> where
  \<open>valid p \<equiv> \<forall>M. \<lbrakk>M\<rbrakk> p\<close>

theorem completeness:
  assumes \<open>valid p\<close>
  shows \<open>[] \<turnstile>\<^sub>S [p]\<close>
  using assms strong_completeness[where X=\<open>{}\<close>] by auto

theorem main: \<open>valid p \<longleftrightarrow> [] \<turnstile>\<^sub>S [p]\<close>
  using completeness soundness' by blast

end


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

theory ArchPasUpdates
imports PasUpdates
begin

context Arch begin global_naming ARM

named_theorems PasUpdates_assms

crunches arch_post_cap_deletion, arch_finalise_cap, prepare_thread_delete
  for domain_fields[PasUpdates_assms, wp]: "domain_fields P"
  (    wp: syscall_valid select_wp crunch_wps rec_del_preservation cap_revoke_preservation modify_wp
     simp: crunch_simps check_cap_at_def filterM_mapM unless_def
   ignore: without_preemption filterM rec_del check_cap_at cap_revoke
   ignore_del: retype_region_ext create_cap_ext cap_insert_ext ethread_set cap_move_ext
               empty_slot_ext cap_swap_ext set_thread_state_ext tcb_sched_action reschedule_required)

end

global_interpretation PasUpdates_1?: PasUpdates_1
proof goal_cases
  interpret Arch .
  case 1 show ?case
    by (unfold_locales; (fact PasUpdates_assms)?)
qed

context Arch begin global_naming ARM

declare init_arch_objects_exst[PasUpdates_assms]

crunches arch_perform_invocation, arch_post_modify_registers,
         arch_invoke_irq_control, arch_invoke_irq_handler, handle_arch_fault_reply
  for domain_fields[PasUpdates_assms, wp]: "domain_fields P"
  (wp: syscall_valid crunch_wps mapME_x_inv_wp
   simp: crunch_simps check_cap_at_def detype_def detype_ext_def mapM_x_defsym
   ignore: check_cap_at syscall
   ignore_del: set_domain set_priority possible_switch_to
   rule: transfer_caps_loop_pres)

lemma state_asids_to_policy_aux_pasSubject_update:
  "state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs =
   state_asids_to_policy_aux aag caps asid vrefs"
  apply (rule equalityI)
   apply clarify
   apply (erule state_asids_to_policy_aux.cases
          | simp
          | fastforce intro: state_asids_to_policy_aux.intros)+
  apply clarify
  apply (erule state_asids_to_policy_aux.cases)
    apply (simp, subst pasObjectAbs_pasSubject_update[symmetric]
               , subst pasASIDAbs_pasSubject_update[symmetric]
               , rule state_asids_to_policy_aux.intros
               , assumption+)+
  done

lemma state_asids_to_policy_pasSubject_update[PasUpdates_assms]:
  "state_asids_to_policy (aag\<lparr>pasSubject := x\<rparr>) s =
   state_asids_to_policy aag s"
  by (simp add: state_asids_to_policy_aux_pasSubject_update)

lemma state_asids_to_policy_aux_pasMayActivate_update:
  "state_asids_to_policy_aux (aag\<lparr>pasMayActivate := x\<rparr>) caps asid_tab vrefs =
   state_asids_to_policy_aux aag caps asid_tab vrefs"
  apply (rule equalityI)
   apply clarify
   apply (erule state_asids_to_policy_aux.cases
          | simp
          | fastforce intro: state_asids_to_policy_aux.intros)+
  apply clarify
  apply (erule state_asids_to_policy_aux.cases)
    apply (simp, subst pasObjectAbs_pasMayActivate_update[symmetric]
               , subst pasASIDAbs_pasMayActivate_update[symmetric]
               , rule state_asids_to_policy_aux.intros
               , assumption+)+
  done

lemma state_asids_to_policy_pasMayActivate_update[PasUpdates_assms]:
  "state_asids_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s =
   state_asids_to_policy aag s"
  by (simp add: state_asids_to_policy_aux_pasMayActivate_update)

lemma state_asids_to_policy_aux_pasMayEditReadyQueues_update:
  "state_asids_to_policy_aux (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) caps asid_tab vrefs =
   state_asids_to_policy_aux aag caps asid_tab vrefs"
  apply (rule equalityI)
   apply (clarify)
   apply (erule state_asids_to_policy_aux.cases
          | simp
          | fastforce intro: state_asids_to_policy_aux.intros)+
  apply (clarify)
  apply (erule state_asids_to_policy_aux.cases)
    apply (simp, subst pasObjectAbs_pasMayEditReadyQueues_update[symmetric]
               , subst pasASIDAbs_pasMayEditReadyQueues_update[symmetric]
               , rule state_asids_to_policy_aux.intros
               , assumption+)+
  done

lemma state_asids_to_policy_pasMayEditReadyQueues_update[PasUpdates_assms]:
  "state_asids_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s =
   state_asids_to_policy aag s"
  by (simp add: state_asids_to_policy_aux_pasMayEditReadyQueues_update)

end

global_interpretation PasUpdates_2?: PasUpdates_2
proof goal_cases
  interpret Arch .
  case 1 show ?case
    by (unfold_locales; (fact PasUpdates_assms)?)
qed

end


text:
theory Graph
  imports Main

begin

subsection \<open>Transitions\<close>

type_synonym 'a transition = "'a \<times> 'a"

type_synonym 'a tss = "'a transition set"

definition tss_sources :: "'a tss \<Rightarrow> 'a set" where
  "tss_sources T \<equiv> {fst t | t. t\<in>T}"

definition tss_targets :: "'a tss \<Rightarrow> 'a set" where
  "tss_targets T \<equiv> {snd t | t. t\<in>T}"

abbreviation (import) tss_nodes :: "'a tss \<Rightarrow> 'a set" where
  "tss_nodes T \<equiv> tss_sources T \<union> tss_targets T"

subsection \<open>Graph with labelled nodes\<close>

type_synonym ('n,'l) node_set = "('n \<rightharpoonup> 'l)"
type_synonym ('n,'l) graph = "('n,'l) node_set \<times> 'n tss"

definition graph_nodes :: "('n,'l) graph \<Rightarrow> 'n set" where
  "graph_nodes G \<equiv> dom(fst G)"

abbreviation graph_labels :: "('n,'l) graph \<Rightarrow> 'l set" where
  "graph_labels G \<equiv> ran(fst G) "

definition graph_transitions :: "('n,'l) graph \<Rightarrow> 'n tss" where
  "graph_transitions G \<equiv> snd G"

(* maybe get rid of it *)
definition is_graph :: "('n,'l) graph \<Rightarrow> bool" where
  "is_graph G \<equiv> tss_nodes(snd G) \<subseteq> dom(fst G)"

lemma is_graph_var:
  "is_graph G \<equiv> tss_nodes(graph_transitions G) \<subseteq> graph_nodes G"
  by (simp add: is_graph_def graph_nodes_def graph_transitions_def)

lemma nodes_is_graph:
  assumes "is_graph G"
  shows "tss_sources(graph_transitions G) \<subseteq> graph_nodes G"
  and "tss_targets(graph_transitions G) \<subseteq> graph_nodes G"
  by (metis assms is_graph_var sup.bounded_iff)+

abbreviation empty :: "('n,'l) graph" where
  "empty \<equiv> (Map.empty,{})"

lemma empty_isgraph:
  "is_graph empty"
  by (simp add: is_graph_def graph_transitions_def tss_sources_def tss_targets_def)

end

author: hoefner


text:
(*  Title:      HOL/MicroJava/BV/Err.thy
    Author:     Tobias Nipkow
    Copyright   2000 TUM

The error type.
*)

header {* \isaheader{The Error Type} *}

theory Err
imports Semilat
begin

datatype 'a err = Err | OK 'a

type_synonym 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
type_synonym 'a esl = "'a set \<times> 'a ord \<times> 'a ebinop"

primrec ok_val :: "'a err \<Rightarrow> 'a"
where
  "ok_val (OK x) = x"

definition lift :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
where
  "lift f e = (case e of Err \<Rightarrow> Err | OK x \<Rightarrow> f x)"

definition lift2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a err \<Rightarrow> 'b err \<Rightarrow> 'c err"
where
  "lift2 f e\<^sub>1 e\<^sub>2 =
  (case e\<^sub>1 of Err  \<Rightarrow> Err | OK x \<Rightarrow> (case e\<^sub>2 of Err \<Rightarrow> Err | OK y \<Rightarrow> f x y))"

definition le :: "'a ord \<Rightarrow> 'a err ord"
where
  "le r e\<^sub>1 e\<^sub>2 =
  (case e\<^sub>2 of Err \<Rightarrow> True | OK y \<Rightarrow> (case e\<^sub>1 of Err \<Rightarrow> False | OK x \<Rightarrow> x \<sqsubseteq>\<^sub>r y))"

definition sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> 'c err)"
where
  "sup f = lift2 (\<lambda>x y. OK (x \<squnion>\<^sub>f y))"

definition err :: "'a set \<Rightarrow> 'a err set"
where
  "err A = insert Err {OK x|x. x\<in>A}"

definition esl :: "'a sl \<Rightarrow> 'a esl"
where
  "esl = (\<lambda>(A,r,f). (A, r, \<lambda>x y. OK(f x y)))"

definition sl :: "'a esl \<Rightarrow> 'a err sl"
where
  "sl = (\<lambda>(A,r,f). (err A, le r, lift2 f))"

abbreviation
  err_semilat :: "'a esl \<Rightarrow> bool" where
  "err_semilat L == semilat(sl L)"

primrec strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
where
  "strict f Err    = Err"
| "strict f (OK x) = f x"

lemma err_def':
  "err A = insert Err {x. \<exists>y\<in>A. x = OK y}"
(*<*)
proof -
  have eq: "err A = insert Err {x. \<exists>y\<in>A. x = OK y}"
    by (unfold err_def) blast
  show "err A = insert Err {x. \<exists>y\<in>A. x = OK y}" by (simp add: eq)
qed
(*>*)

lemma strict_Some [simp]:
  "(strict f x = OK y) = (\<exists>z. x = OK z \<and> f z = OK y)"
(*<*) by (cases x, auto) (*>*)

lemma not_Err_eq: "(x \<noteq> Err) = (\<exists>a. x = OK a)"
(*<*) by (cases x) auto (*>*)

lemma not_OK_eq: "(\<forall>y. x \<noteq> OK y) = (x = Err)"
(*<*) by (cases x) auto   (*>*)

lemma unfold_lesub_err: "e1 \<sqsubseteq>\<^bsub>le r\<^esub> e2 = le r e1 e2"
(*<*) by (simp add: lesub_def) (*>*)

lemma le_err_refl: "\<forall>x. x \<sqsubseteq>\<^sub>r x \<Longrightarrow> e \<sqsubseteq>\<^bsub>le r\<^esub> e"
(*<*)
apply (unfold lesub_def le_def)
apply (simp split: err.split)
done
(*>*)

lemma le_err_trans [rule_format]:
  "order r \<Longrightarrow> e1 \<sqsubseteq>\<^bsub>le r\<^esub> e2 \<longrightarrow> e2 \<sqsubseteq>\<^bsub>le r\<^esub> e3 \<longrightarrow> e1 \<sqsubseteq>\<^bsub>le r\<^esub> e3"
(*<*)
apply (unfold unfold_lesub_err le_def)
apply (simp split: err.split)
apply (blast intro: order_trans)
done
(*>*)

lemma le_err_antisym [rule_format]:
  "order r \<Longrightarrow> e1 \<sqsubseteq>\<^bsub>le r\<^esub> e2 \<longrightarrow> e2 \<sqsubseteq>\<^bsub>le r\<^esub> e1 \<longrightarrow> e1=e2"
(*<*)
apply (unfold unfold_lesub_err le_def)
apply (simp split: err.split)
apply (blast intro: order_antisym)
done
(*>*)

lemma OK_le_err_OK: "(OK x \<sqsubseteq>\<^bsub>le r\<^esub> OK y) = (x \<sqsubseteq>\<^sub>r y)"
(*<*) by (simp add: unfold_lesub_err le_def) (*>*)

lemma order_le_err [iff]: "order(le r) = order r"
(*<*)
apply (rule iffI)
 apply (subst order_def)
 apply (blast dest: order_antisym OK_le_err_OK [THEN iffD2]
              intro: order_trans OK_le_err_OK [THEN iffD1])
apply (subst order_def)
apply (blast intro: le_err_refl le_err_trans le_err_antisym
             dest: order_refl)
done
(*>*)

lemma le_Err [iff]: "e \<sqsubseteq>\<^bsub>le r\<^esub> Err"
(*<*) by (simp add: unfold_lesub_err le_def) (*>*)

lemma Err_le_conv [iff]: "Err \<sqsubseteq>\<^bsub>le r\<^esub> e  = (e = Err)"
(*<*) by (simp add: unfold_lesub_err le_def  split: err.split) (*>*)

lemma le_OK_conv [iff]: "e \<sqsubseteq>\<^bsub>le r\<^esub> OK x  =  (\<exists>y. e = OK y \<and> y \<sqsubseteq>\<^sub>r x)"
(*<*) by (simp add: unfold_lesub_err le_def split: err.split) (*>*)

lemma OK_le_conv: "OK x \<sqsubseteq>\<^bsub>le r\<^esub> e = (e = Err \<or> (\<exists>y. e = OK y \<and> x \<sqsubseteq>\<^sub>r y))"
(*<*) by (simp add: unfold_lesub_err le_def split: err.split) (*>*)

lemma top_Err [iff]: "top (le r) Err"
(*<*) by (simp add: top_def) (*>*)

lemma OK_less_conv [rule_format, iff]:
  "OK x \<sqsubset>\<^bsub>le r\<^esub> e = (e=Err \<or> (\<exists>y. e = OK y \<and> x \<sqsubset>\<^sub>r y))"
(*<*) by (simp add: lesssub_def lesub_def le_def split: err.split) (*>*)

lemma not_Err_less [rule_format, iff]: "\<not>(Err \<sqsubset>\<^bsub>le r\<^esub> x)"
(*<*) by (simp add: lesssub_def lesub_def le_def split: err.split) (*>*)

lemma semilat_errI [intro]: assumes "Semilat A r f"
shows "semilat(err A, le r, lift2(\<lambda>x y. OK(f x y)))"
(*<*)
proof -
  interpret Semilat A r f by fact
  show ?thesis
    apply(insert semilat)
    apply (unfold semilat_Def closed_def plussub_def lesub_def
              lift2_def le_def)
    apply (simp add: err_def' split: err.split)
    done
qed
(*>*)

lemma err_semilat_eslI_aux:
assumes "Semilat A r f" shows "err_semilat(esl(A,r,f))"
(*<*)
proof -
  interpret Semilat A r f by fact
  show ?thesis
    apply (unfold sl_def esl_def)
    apply (simp add: semilat_errI [OF `Semilat A r f`])
    done
qed
(*>*)

lemma err_semilat_eslI [intro, simp]:
  "semilat L \<Longrightarrow> err_semilat (esl L)"
(*<*) apply (cases L) apply simp
apply (drule Semilat.intro)
apply (simp add: err_semilat_eslI_aux split_tupled_all)
done (*>*)

lemma acc_err [simp, intro!]:  "acc A r \<Longrightarrow> acc (err A) (le r)"
(*<*)
apply (unfold acc_def lesub_def le_def lesssub_def)
apply (simp add: wf_eq_minimal split: err.split)
apply clarify
apply (case_tac "Err : Q")
 apply blast
apply (erule_tac x = "{a . OK a : Q}" in allE)
apply (case_tac "x")
 apply fast
apply (auto simp: err_def)
done
(*>*)

lemma Err_in_err [iff]: "Err : err A"
(*<*) by (simp add: err_def') (*>*)

lemma Ok_in_err [iff]: "(OK x \<in> err A) = (x\<in>A)"
(*<*) by (auto simp add: err_def') (*>*)

section {* lift *}

lemma lift_in_errI:
  "\<lbrakk> e \<in> err S; \<forall>x\<in>S. e = OK x \<longrightarrow> f x \<in> err S \<rbrakk> \<Longrightarrow> lift f e \<in> err S"
(*<*)
apply (unfold lift_def)
apply (simp split: err.split)
apply blast
done
(*>*)

lemma Err_lift2 [simp]: "Err \<squnion>\<^bsub>lift2 f\<^esub> x = Err"
(*<*) by (simp add: lift2_def plussub_def) (*>*)

lemma lift2_Err [simp]: "x \<squnion>\<^bsub>lift2 f\<^esub> Err = Err"
(*<*) by (simp add: lift2_def plussub_def split: err.split) (*>*)

lemma OK_lift2_OK [simp]: "OK x \<squnion>\<^bsub>lift2 f\<^esub> OK y = x \<squnion>\<^sub>f y"
(*<*) by (simp add: lift2_def plussub_def split: err.split) (*>*)

section {* sup *}

lemma Err_sup_Err [simp]: "Err \<squnion>\<^bsub>sup f\<^esub> x = Err"
(*<*) by (simp add: plussub_def sup_def lift2_def) (*>*)

lemma Err_sup_Err2 [simp]: "x \<squnion>\<^bsub>sup f\<^esub> Err = Err"
(*<*) by (simp add: plussub_def sup_def lift2_def split: err.split) (*>*)

lemma Err_sup_OK [simp]: "OK x \<squnion>\<^bsub>sup f\<^esub> OK y = OK (x \<squnion>\<^sub>f y)"
(*<*) by (simp add: plussub_def sup_def lift2_def) (*>*)

lemma Err_sup_eq_OK_conv [iff]:
  "(sup f ex ey = OK z) = (\<exists>x y. ex = OK x \<and> ey = OK y \<and> f x y = z)"
(*<*)
apply (unfold sup_def lift2_def plussub_def)
apply (rule iffI)
 apply (simp split: err.split_asm)
apply clarify
apply simp
done
(*>*)

lemma Err_sup_eq_Err [iff]: "(sup f ex ey = Err) = (ex=Err \<or> ey=Err)"
(*<*)
apply (unfold sup_def lift2_def plussub_def)
apply (simp split: err.split)
done
(*>*)

section {* semilat (err A) (le r) f *}

lemma semilat_le_err_Err_plus [simp]:
  "\<lbrakk> x\<in> err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err \<squnion>\<^sub>f x = Err"
(*<*) by (blast intro: Semilat.le_iff_plus_unchanged [THEN iffD1, OF Semilat.intro]
                   Semilat.le_iff_plus_unchanged2 [THEN iffD1, OF Semilat.intro]) (*>*)

lemma semilat_le_err_plus_Err [simp]:
  "\<lbrakk> x\<in> err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f Err = Err"
(*<*) by (blast intro: Semilat.le_iff_plus_unchanged [THEN iffD1, OF Semilat.intro]
                   Semilat.le_iff_plus_unchanged2 [THEN iffD1, OF Semilat.intro]) (*>*)

lemma semilat_le_err_OK1:
  "\<lbrakk> x\<in>A; y\<in>A; semilat(err A, le r, f); OK x \<squnion>\<^sub>f OK y = OK z \<rbrakk>
  \<Longrightarrow> x \<sqsubseteq>\<^sub>r z"
(*<*)
apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst)
apply (simp add: Semilat.ub1 [OF Semilat.intro])
done
(*>*)

lemma semilat_le_err_OK2:
  "\<lbrakk> x\<in>A; y\<in>A; semilat(err A, le r, f); OK x \<squnion>\<^sub>f OK y = OK z \<rbrakk>
  \<Longrightarrow> y \<sqsubseteq>\<^sub>r z"
(*<*)
apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst)
apply (simp add: Semilat.ub2 [OF Semilat.intro])
done
(*>*)

lemma eq_order_le:
  "\<lbrakk> x=y; order r \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r y"
(*<*)
apply (unfold order_def)
apply blast
done
(*>*)

lemma OK_plus_OK_eq_Err_conv [simp]:
  assumes "x\<in>A"  "y\<in>A"  "semilat(err A, le r, fe)"
  shows "(OK x \<squnion>\<^bsub>fe\<^esub> OK y = Err) = (\<not>(\<exists>z\<in>A. x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z))"
(*<*)
proof -
  have plus_le_conv3: "\<And>A x y z f r.
    \<lbrakk> semilat (A,r,f); x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z; x\<in>A; y\<in>A; z\<in>A \<rbrakk>
    \<Longrightarrow> x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z"
(*<*) by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1]) (*>*)
  from assms show ?thesis
  apply (rule_tac iffI)
   apply clarify
   apply (drule OK_le_err_OK [THEN iffD2])
   apply (drule OK_le_err_OK [THEN iffD2])
   apply (drule Semilat.lub[OF Semilat.intro, of _ _ _ "OK x" _ "OK y"])
        apply assumption
       apply assumption
      apply simp
     apply simp
    apply simp
   apply simp
  apply (case_tac "OK x \<squnion>\<^bsub>fe\<^esub> OK y")
   apply assumption
  apply (rename_tac z)
  apply (subgoal_tac "OK z\<in> err A")
  apply (drule eq_order_le)
    apply (erule Semilat.orderI [OF Semilat.intro])
   apply (blast dest: plus_le_conv3)
  apply (erule subst)
  apply (blast intro: Semilat.closedI [OF Semilat.intro] closedD)
  done
qed
(*>*)

section {* semilat (err(Union AS)) *}

(* FIXME? *)
lemma all_bex_swap_

text {*
  If @{term "AS = {}"} the thm collapses to
  @{prop "order r \<and> closed {Err} f \<and> Err \<squnion>\<^sub>f Err = Err"}
  which may not hold
*}
lemma err_semilat_UnionI:
  "\<lbrakk> \<forall>A\<in>AS. err_semilat(A, r, f); AS \<noteq> {};
      \<forall>A\<in>AS.\<forall>B\<in>AS. A\<noteq>B \<longrightarrow> (\<forall>a\<in>A.\<forall>b\<in>B. \<not>a \<sqsubseteq>\<^sub>r b \<and> a \<squnion>\<^sub>f b = Err) \<rbrakk>
  \<Longrightarrow> err_semilat(Union AS, r, f)"
(*<*)
apply (unfold semilat_def sl_def)
apply (simp add: closed_err_Union_lift2I)
apply (rule conjI)
 apply blast
apply (simp add: err_def')
apply (rule conjI)
 apply clarify
 apply (rename_tac A a u B b)
 apply (case_tac "A = B")
  apply simp
 apply simp
apply (rule conjI)
 apply clarify
 apply (rename_tac A a u B b)
 apply (case_tac "A = B")
  apply simp
 apply simp
apply clarify
apply (rename_tac A ya yb B yd z C c a b)
apply (case_tac "A = B")
 apply (case_tac "A = C")
  apply simp
 apply simp
apply (case_tac "B = C")
 apply simp
apply simp
done
(*>*)

end