Theory Automation_Setup

theory Automation_Setup
  imports System_Specification
begin

lemma add_prop:
  assumes "PROP (T)"
  shows "A ==> PROP (T)"
  using assms .


lemmas exhaust_elim =
   sActt.exhaust[of x, THEN add_prop[where A="a=Sact x"], rotated -1]
   cActt.exhaust[of x, THEN add_prop[where A="a=Cact x"], rotated -1]
   uActt.exhaust[of x, THEN add_prop[where A="a=Uact x"], rotated -1]
   rActt.exhaust[of x, THEN add_prop[where A="a=Ract x"], rotated -1]
   lActt.exhaust[of x, THEN add_prop[where A="a=Lact x"], rotated -1]
   comActt.exhaust[of x, THEN add_prop[where A="a=COMact x"], rotated -1]
  for x a


lemma state_cong:
fixes s::state
assumes
"pendingUReqs s = pendingUReqs s1 ∧ userReq s = userReq s1 ∧ userIDs s = userIDs s1 ∧
 postIDs s = postIDs s1 ∧ admin s = admin s1 ∧
 user s = user s1 ∧ pass s = pass s1 ∧ pendingFReqs s = pendingFReqs s1 ∧ friendReq s = friendReq s1 ∧ friendIDs s = friendIDs s1 ∧
 sentOuterFriendIDs s = sentOuterFriendIDs s1 ∧
 recvOuterFriendIDs s = recvOuterFriendIDs s1 ∧
 post s = post s1 ∧
 owner s = owner s1 ∧ vis s = vis s1 ∧
 pendingSApiReqs s = pendingSApiReqs s1 ∧ sApiReq s = sApiReq s1 ∧ serverApiIDs s = serverApiIDs s1 ∧ serverPass s = serverPass s1 ∧
 outerPostIDs s = outerPostIDs s1 ∧ outerPost s = outerPost s1 ∧
 outerOwner s = outerOwner s1 ∧ outerVis s = outerVis s1 ∧
 pendingCApiReqs s = pendingCApiReqs s1 ∧ cApiReq s = cApiReq s1 ∧ clientApiIDs s = clientApiIDs s1 ∧ clientPass s = clientPass s1 ∧
 sharedWith s = sharedWith s1"
shows "s = s1"
using assms apply (cases s, cases s1) by auto

(*
lemma Paper_dest_conv:
  "(p =
        Paper title abstract content reviews dis decs fcontent) ⟷
  title = titlePaper p ∧
  abstract = abstractPaper p ∧
  content = contentPaper p ∧
  reviews = reviewsPaper p ∧
  dis = disPaper p ∧
  decs = decsPaper p ∧
  fcontent = fcontentPaper p
  "
  by (cases p) auto
*)

end