Theory Pred

Up to index of Isabelle/HOL/Marvin99-1

Pred = Term +

types Rel = "string"

datatype
    pred = "&&" (  pred) (  pred) (infixr 35)
       | "||" (  pred) (  pred) (infixr 40)
       | "=>" (  pred) (  pred) (infixr 45)
       | "<=>" (  pred) (  pred) (infixr 50)
       | "==" ( rterm) ( rterm) (infixl 55)
       | "<<" ( rterm) ( rterm) (infixl 60)
       | relT Rel (rterm list)
       | lnot (  pred)
       | pex Var pred 
       | pall Var pred
       | ptrue
       | pfalse
       | isNat rterm
       | isList rterm
       | isBag rterm

consts
  bnds :: "pred => Bnds set"
  rapply :: "Rel => (Val list => bool)"
  everywhere :: "pred => bool" ("|[_]|")
  entails :: "[pred,pred] => bool"
  substp :: "[pred, Var, rterm] => pred"
  evalp :: "[pred, Bnds] => bool"
defs
  bnds_def "bnds(P) == {b. evalp P b}"
  everywhere_def "everywhere(P) == ! b . evalp P b"
  entails_def "entails p1 p2 == ! b. (evalp p1 b --> evalp p2 b)"
primrec
  "evalp (S && T) b = ((evalp S b) & (evalp T b))"
  "evalp (S || T) b = ((evalp S b) | (evalp T b))"
  "evalp (S => T) b = ((evalp S b) --> (evalp T b))"
  "evalp (lnot S) b = (~(evalp S b))"
  "evalp (S <=> T) b = ((evalp S b)  = (evalp T b))"
  "evalp (pex v P) b =  (? x. (evalp P (b(v:= x))))"
  "evalp (pall v P) b = (! x. (evalp P (b(v:= x))))"
  "evalp (relT r as) b = (rapply r (evallist as b))" 
  "evalp (s == t) b = ((eval s b) = (eval t b))"
  "evalp (s << t) b = ((eval s b) vless (eval t b))"
  "evalp (ptrue) b = True"
  "evalp (pfalse) b = False"
  "evalp (isNat t) b =  (? u. (eval t b) = (natV u))"
  "evalp (isList t) b =  (? u. (eval t b) = (listV u))"
  "evalp (isBag t) b =  (? u. (eval t b) = (bagV u))"
primrec
  substp_land "substp (P && Q) v t = ((substp P v t) && (substp Q v t))"
  substp_lor "substp (P || Q) v t = ((substp P v t) || (substp Q v t))"
  substp_implies "substp (P => Q) v t = ((substp P v t) => (substp Q v t))"
  substp_equiv "substp (P <=> Q) v t = ((substp P v t) <=> (substp Q v t))"
  substp_equal "substp (P == Q) v t = ((substt P v t) == (substt Q v t))"
  substp_less "substp (P << Q) v t = ((substt P v t) << (substt Q v t))"
  substp_lnot "substp (lnot P) v t = (lnot (substp P v t))"
  substp_exists "substp (pex x P) v t = (pex x (substp P v t))"
  substp_pall "substp (pall x P) v t = (pall x (substp P v t))"
  "substp (relT r as) v t = (relT r (substl as v t))"
  substp_nat "substp (isNat r) v t = (isNat (substt r v t))"
  "substp (isList r) v t =(isList (substt r v t))"
  "substp ptrue v t = ptrue"
  "substp pfalse v t = pfalse"
  (* rules  
  vless_first_pair "a vless c ==> apply pair [a,b] vless apply pair [c,d]" *)
syntax
  "@PEX" :: "[Var,pred] => pred" ("(3PEX _./ _)" 10)
translations
  "PEX x y. P" == "PEX x. PEX y. P"
  "PEX x. P" == "pex x P"
syntax (symbols)
  "op &&"        :: "[pred, pred] => pred"                (infixr "\<and>" 35)
  "op ||"        :: "[pred, pred] => pred"                (infixr "\<or>" 30)   "op =>"        :: "[pred, pred] => pred"  (infixr "\<Rightarrow>" 40)
  "op <=>"       :: "[pred, pred] => pred"  (infixr "\<equiv>" 45)
  "entails"      :: "[pred, pred] => pred"  ("_ \<equiv>> _")
  "everywhere"   :: "pred => bool"          ("\<lbrakk>_\<rbrakk>")
end
  

theorem bnds_land:

  bnds (P && Q) = bnds P Int bnds Q

theorem bnds_lnot:

  bnds (lnot P) = UNIV - bnds P

theorem bnds_equiv:

  bnds (p1 <=> p2) = bnds p1 Int bnds p2 Un (UNIV - (bnds p1 Un bnds p2))

theorem bnds_lor:

  bnds (p1 || p2) = bnds p1 Un bnds p2

theorem bnds_implies:

  bnds (p1 => p2) = UNIV - bnds p1 Un bnds p2

theorem bnds_equiv_every_eq:

  |[P <=> Q]| ==> bnds P = bnds Q

theorem bnds_implies_subset:

  |[P => Q]| ==> bnds P <= bnds Q

theorem entails_everywhere_imp:

  entails A P ==> |[A]| --> |[P]|

theorem remove_context:

  |[P]| ==> entails A P

theorem entails_trans:

  [| entails S T; entails T U |] ==> entails S U

theorem entails_and:

  [| entails X A; entails X B |] ==> entails X (A && B)

theorem everywhere_mp:

  [| entails A B; |[A]| |] ==> |[B]|

theorem entails_everywhere:

  |[A => B]| = entails A B

theorem entails_implies:

  entails A (B => C) = entails (A && B) C

theorem entails_landE1:

  entails A B ==> entails (A && C) B

theorem entails_landE2:

  entails A B ==> entails (C && A) B

theorem entails_trans2:

  [| entails T U; entails S T |] ==> entails S U