Cross Reference: /seL4-l4v-master/HOL4/src/tfl/examples/proplog

(*---------------------------------------------------------------------------
      A type of propositions and a few algorithms on it.
 ---------------------------------------------------------------------------*)

app load ["bossLib"]; open bossLib;


Hol_datatype `prop = VAR of 'a
                   | NOT of prop
                   | AND of prop => prop
                   | OR  of prop => prop`;


(*---------------------------------------------------------------------------
       Wang's algorithm (implements the sequent calculus).
 ---------------------------------------------------------------------------*)

val Pr_def =
 Hol_defn "Pr"
    `(Pr vl [] (VAR v::r)   vr = Pr vl [] r (v::vr))
 /\  (Pr vl [] (NOT x::r)   vr = Pr vl [x] r vr)
 /\  (Pr vl [] (OR x y::r)  vr = Pr vl [] (x::y::r) vr)
 /\  (Pr vl [] (AND x y::r) vr = Pr vl [] (x::r) vr /\ Pr vl [] (y::r) vr)

 /\  (Pr vl (VAR v::l)    r vr = Pr (v::vl) l r vr)
 /\  (Pr vl (NOT x::l)    r vr = Pr vl l (x::r) vr)
 /\  (Pr vl (AND x y::l)  r vr = Pr vl (x::y::l) r vr)
 /\  (Pr vl (OR x y::l)   r vr = Pr vl (x::l) r vr /\ Pr vl (y::l) r vr)
 /\  (Pr vl [] [] vr           = EXISTS (\y. MEM y vl) vr)`;


val Wang_def = Define `Wang P = Pr [] [] [P] []`;

set_fixity "OR" (Infixr 300);
set_fixity "AND" (Infixr 400);

(*---------------------------------------------------------------------------
     Termination of Pr. We need a subsidiary measure function on
     propositions which makes a 2-argument proposition bigger than a
     list of 2 propositions.
 ---------------------------------------------------------------------------*)

val Meas_def =
 Define
    `(Meas (VAR v)   = 0)
 /\  (Meas (NOT x)   = SUC (Meas x))
 /\  (Meas (x AND y) = Meas x + Meas y + 2)
 /\  (Meas (x OR y)  = Meas x + Meas y + 2)`;

(*---------------------------------------------------------------------------*
 *  Termination of Pr.                                                       *
 *---------------------------------------------------------------------------*)

val (Pr_eqns, Pr_ind) =
 Defn.tprove (Pr_def,
   WF_REL_TAC
      `measure \(w:'a list, x:'a prop list, y:'a prop list, z:'a list).
          list_size Meas x + list_size Meas y`
     THEN RW_TAC arith_ss [Meas_def,listTheory.list_size_def]);

(*---------------------------------------------------------------------------
      Examples.
 ---------------------------------------------------------------------------*)

val x = Term`VAR x`; val y = Term`VAR y`; val z = Term`VAR z`;
val p = Term`VAR p`; val q = Term`VAR q`; val r = Term`VAR r`;
val s = Term`VAR s`;

fun imp x y = Term`(NOT ^x) OR ^y`;
fun iff x y = Term`^(imp x y) AND ^(imp y x)`;

val BOOL_CASES = Term `^x OR (NOT ^x)`;
val NOT_BCASES = Term `^x OR (NOT ^y)`;
val IMP_REFL   = Term `(NOT ^x) OR ^x`;
val DISTRIB    = iff (Term`^x AND (^y OR ^z)`)
                     (Term`(^x AND ^y) OR (^x AND ^z)`);
val PEIRCE     = imp (imp (imp p q) p) p;
val ANDREWS    = imp (Term`^(imp p (Term`^q AND (^r OR ^s)`))
                            AND ((NOT ^q) OR (NOT ^r))`)
                     (imp p s);
val CLASSIC    = imp (imp (Term`^p AND ^q`) r)
                     (Term `^(imp p r) OR ^(imp q r)`);

(*---------------------------------------------------------------------------
      The following are adapted from jrh's tautology collection
      in the examples directory.
 ---------------------------------------------------------------------------*)

val v0 = Term`VAR v0`; val v1 = Term`VAR v1`; val v2 = Term`VAR v2`;
val v3 = Term`VAR v3`; val v4 = Term`VAR v4`; val v5 = Term`VAR v5`;
val v6 = Term`VAR v6`; val v7 = Term`VAR v7`; val v8 = Term`VAR v8`;
val v9 = Term`VAR v9`;

val syn323_1 = Term
       `NOT((^v0 OR ^v1) AND
            (NOT ^v0 OR ^v1) AND
            (NOT ^v1 OR ^v0) AND
            (NOT ^v0 OR NOT ^v1))`;


val syn029_1 = Term
   `NOT((NOT ^v2 OR NOT ^v1) AND
        ^v0 AND
        (NOT ^v0 OR NOT ^v1 OR ^v2) AND
        (NOT ^v2 OR ^v1) AND (^v1 OR ^v2))`;


val syn052_1 = Term
   `NOT((NOT ^v1 OR ^v0) AND
        (NOT ^v0 OR ^v1) AND
        (^v1 OR ^v0)     AND
        (NOT ^v1 OR ^v1) AND
        (NOT ^v0 OR NOT ^v1))`;

val syn051_1 = Term
  `NOT(( ^v1 OR ^v0) AND
       (^v1 OR ^v2) AND
       (NOT ^v0 OR NOT ^v1) AND
       (NOT ^v2 OR NOT ^v1) AND
       (NOT ^v0 OR ^v1) AND
       (NOT ^v1 OR ^v2))`;

val syn044_1 = Term
  `NOT((^v0 OR ^v1) AND
       (NOT ^v0 OR NOT ^v1) AND
       (NOT ^v0 OR ^v1 OR ^v2) AND
       (NOT ^v2 OR ^v1) AND
       (NOT ^v2 OR ^v0) AND
       (NOT ^v1 OR ^v2))`;

val syn011_1 = Term
  `NOT(^v6 AND
       (NOT ^v0 OR NOT ^v2) AND
       (^v0 OR ^v1 OR ^v5) AND
       (NOT ^v2 OR NOT ^v1) AND
       (NOT ^v4 OR ^v2) AND
       (NOT ^v3 OR ^v2) AND
       (^v3 OR ^v4 OR ^v5) AND
       (NOT ^v5 OR NOT ^v6))`;

val syn032_1 = Term
  `NOT((NOT ^v5 OR NOT ^v1) AND
       (NOT ^v4 OR NOT ^v0) AND
       (NOT ^v4 OR ^v0) AND
       (NOT ^v5 OR ^v1) AND
       (NOT ^v2 OR ^v4 OR ^v3) AND
       (^v4 OR ^v2 OR ^v3) AND
       (NOT ^v3 OR ^v4 OR ^v5))`;

val syn030_1 = Term
   `NOT((NOT ^v4 OR NOT ^v0 OR NOT ^v1) AND
        (NOT ^v3 OR NOT ^v4 OR ^v0) AND
        (NOT ^v1 OR ^v0) AND
        (^v0 OR ^v1) AND
        (NOT ^v0 OR ^v1) AND
        (NOT ^v1 OR NOT ^v0 OR ^v2) AND
        (NOT ^v2 OR ^v1) AND
        (NOT ^v1 OR ^v3) AND
        (NOT ^v2 OR NOT ^v3 OR ^v4))`;

val syn054_1 = Term
  `NOT((NOT ^v1 OR NOT ^v7) AND
       (NOT ^v2 OR NOT ^v0) AND
       (NOT ^v3 OR ^v7 OR ^v4) AND
       (NOT ^v6 OR ^v0 OR ^v5) AND
       (NOT ^v7 OR ^v1) AND
       (NOT ^v0 OR ^v2) AND
       (NOT ^v4 OR ^v1) AND
       (NOT ^v5 OR ^v2) AND
       (NOT ^v3 OR NOT ^v4) AND
       (NOT ^v6 OR NOT ^v5) AND
       (^v6 OR ^v7))`;

val gra001_1 = Term
  `NOT((NOT ^v1 OR ^v0) AND
       (NOT ^v0 OR ^v1) AND
       (NOT ^v4 OR NOT ^v2 OR NOT ^v0) AND
       (NOT ^v4 OR ^v2 OR ^v0) AND
       (NOT ^v2 OR ^v4 OR ^v0) AND
       (NOT ^v0 OR ^v4 OR ^v2) AND
       (NOT ^v3 OR NOT ^v2 OR NOT ^v1) AND
       (NOT ^v3 OR ^v2 OR ^v1) AND
       (NOT ^v2 OR ^v3 OR ^v1) AND
       (NOT ^v1 OR ^v3 OR ^v2) AND
       (NOT ^v3 OR NOT ^v4) AND
       (^v3 OR ^v4))`;


val syn321_1 =  Term
  `NOT((NOT ^v0 OR ^v9) AND
       (NOT ^v0 OR ^v6) AND
       (NOT ^v0 OR ^v7) AND
       (NOT ^v8 OR ^v9) AND
       (NOT ^v8 OR ^v6) AND
       (NOT ^v8 OR ^v7) AND
       (NOT ^v1 OR ^v9) AND
       (NOT ^v1 OR ^v6) AND
       (NOT ^v1 OR ^v7) AND
       (NOT ^v2 OR ^v3) AND
       (NOT ^v4 OR ^v5) AND
       (NOT ^v7 OR ^v8) AND
       (^v8 OR ^v9) AND
       (^v8 OR ^v6) AND
       (^v8 OR ^v7) AND
       (NOT ^v8 OR NOT ^v9))`;


val Eval = Count.apply (EVAL o Term);

Eval `Wang ^BOOL_CASES`;
Eval `Wang ^NOT_BCASES`;
Eval `Wang ^IMP_REFL`;
Eval `Wang ^DISTRIB`;
Eval `Wang ^PEIRCE`;
Eval `Wang ^ANDREWS`;
Eval `Wang ^CLASSIC`;
Eval `Wang ^syn323_1`;
Eval `Wang ^syn029_1`;
Eval `Wang ^syn052_1`;
Eval `Wang ^syn051_1`;
Eval `Wang ^syn044_1`;
Eval `Wang ^syn011_1`;
Eval `Wang ^syn032_1`;
Eval `Wang ^syn030_1`;
Eval `Wang ^syn054_1`;
Eval `Wang ^gra001_1`; (* 45,395,214 inference steps (takes a long time) *)
Eval `Wang ^syn321_1`; (* Takes longer, but not that much: 57,451,380 steps *)


(*---------------------------------------------------------------------------
        Negation normal form (from Paulson's ML book). First a naive
        version, which has a slightly complicated termination proof,
        and then a faster mutually recursive version, which has an
        easy termination proof.
 ---------------------------------------------------------------------------*)

val nnf_defn0 =
 Hol_defn "nnf0"
     `(nnf (VAR x)        = VAR x)
 /\   (nnf (NOT (VAR x))  = NOT(VAR x))
 /\   (nnf (NOT(NOT p))   = nnf p)
 /\   (nnf (NOT(p AND q)) = nnf ((NOT p) OR (NOT q)))
 /\   (nnf (NOT(p OR q))  = nnf ((NOT p) AND (NOT q)))
 /\   (nnf (p AND q)      = (nnf p) AND (nnf q))
 /\   (nnf (p OR q)       = (nnf p) OR (nnf q))`;

(*---------------------------------------------------------------------------
    The size of the largest NOT expression in a proposition.
 ---------------------------------------------------------------------------*)

val prop_size_def = fetch "-" "prop_size_def";

val MAX_def = Define `MAX x y = if x<y then y else x`;

val NOT_SIZE_def =
 Define
    `(NOT_SIZE (VAR x)    = 0)
  /\ (NOT_SIZE (NOT p)    = prop_size (\v.0) p)
  /\ (NOT_SIZE ($AND p q) = MAX (NOT_SIZE p) (NOT_SIZE q))
  /\ (NOT_SIZE ($OR p q)  = MAX (NOT_SIZE p) (NOT_SIZE q))`;


val NOT_SIZE_LESS = Q.prove
(`!p. NOT_SIZE p < prop_size (\v.0) p + 1`,
 Induct
   THEN RW_TAC arith_ss [NOT_SIZE_def, MAX_def, prop_size_def]);

(*---------------------------------------------------------------------------
     Termination of nnf, using NOT_SIZE_LESS
 ---------------------------------------------------------------------------*)

val (nnf0_eqns, nnf0_ind) =
Defn.tprove
 (nnf_defn0,
  WF_REL_TAC nnf_defn0
      `inv_image ($< LEX $<) (\x. (NOT_SIZE x, prop_size (\v.0) x))`
    THEN RW_TAC arith_ss [NOT_SIZE_def, MAX_def,
                          prop_size_def, NOT_SIZE_LESS]);


(*---------------------------------------------------------------------------
      Mutually recursive algorithm. Termination is easy to prove,
      and automatic.
 ---------------------------------------------------------------------------*)

val nnf_mutrec_eqns =
 xDefine "nnf1"
     `(nnfpos (VAR x)   = VAR x)
 /\   (nnfpos (NOT p)   = nnfneg p)
 /\   (nnfpos (p AND q) = (nnfpos p) AND (nnfpos q))
 /\   (nnfpos (p OR q)  = (nnfpos p) OR (nnfpos q))

 /\   (nnfneg (VAR x)   = NOT (VAR x))
 /\   (nnfneg (NOT p)   = nnfpos p)
 /\   (nnfneg (p AND q) = (nnfneg p) OR (nnfneg q))
 /\   (nnfneg (p OR q)  = (nnfneg p) AND (nnfneg q))`;


(*---------------------------------------------------------------------------
    Equivalence of nnf and nnfpos is straightforward.
 ---------------------------------------------------------------------------*)

val nnf_eq_nnfpos = Q.prove
(`!p. nnf p = nnfpos p`,
  recInduct nnf0_ind
    THEN RW_TAC std_ss [nnf0_eqns,nnf_mutrec_eqns]);


(*---------------------------------------------------------------------------
    Evaluation with nnfpos. First tell computeLib about nnf_mutrec_eqns.
 ---------------------------------------------------------------------------*)

val _ = computeLib.add_thms [nnf_mutrec_eqns] compset;

Eval `nnfpos ^syn052_1`;
Eval `nnfpos ^syn051_1`;
Eval `nnfpos ^syn044_1`;
Eval `nnfpos ^syn011_1`;
Eval `nnfpos ^syn032_1`;
Eval `nnfpos ^syn030_1`;
Eval `nnfpos ^syn054_1`;
Eval `nnfpos ^gra001_1`;
Eval `nnfpos ^syn321_1`;


(*---------------------------------------------------------------------------
        Conjunctive normal form (also from Paulson's ML book).
 ---------------------------------------------------------------------------*)

val distrib_def =
 Define
    `(distrib p (q AND r) = distrib p q AND distrib p r)
 /\  (distrib (q AND r) p = distrib q p AND distrib r p)
 /\  (distrib p q         = p OR q)`;


val cnf_def =
 Define
    `(cnf (p AND q) = cnf p AND cnf q)
 /\  (cnf (p OR q)  = distrib (cnf p) (cnf q))
 /\  (cnf p         = p)`;


val Value_def =
 Define
   `(Value P (VAR x)   = P x)
 /\ (Value P (NOT p)   = ~Value P p)
 /\ (Value P (p AND q) = Value P p /\ Value P q)
 /\ (Value P (p OR q)  = Value P p \/ Value P q)`;


val Value_distrib_disj = Q.prove
(`!p q P. Value P (distrib p q) = Value P p \/ Value P q`,
 recInduct (fetch "-" "distrib_ind")
   THEN RW_TAC std_ss [distrib_def, Value_def]
   THEN PROVE_TAC []);


val Value_cnf_stable = Q.prove
(`!p Q. Value Q (cnf p) = Value Q p`,
 Induct
   THEN RW_TAC std_ss [cnf_def, Value_def, Value_distrib_disj]);


val Value_nnf_stable = Q.prove
(`!p Q. Value Q (nnf p) = Value Q p`,
  recInduct nnf0_ind
    THEN RW_TAC std_ss [nnf0_eqns,Value_def]);


(*---------------------------------------------------------------------------
         An SML version of Wang's algorithm.

fun mem x [] = false
  | mem x (h::t) = (x=h) orelse mem x t;

datatype 'a prop = VAR of 'a
                 | NOT of 'a prop
                 | AND of 'a prop * 'a prop
                 | OR  of 'a prop * 'a prop;

fun Prv vl [] (VAR v::r) vr    = Prv vl [] r (v::vr)
  | Prv vl [] (NOT x::r) vr    = Prv vl [x] r vr
  | Prv vl [] (OR(x,y)::r) vr  = Prv vl [] (x::y::r) vr
  | Prv vl [] (AND(x,y)::r) vr = Prv vl [] (x::r) vr
                                      andalso
                                  Prv vl [] (y::r) vr
  | Prv vl (VAR v::l) r vr     = Prv (v::vl) l r vr
  | Prv vl (NOT x::l) r vr     = Prv vl l (x::r) vr
  | Prv vl (AND(x,y)::l) r vr  = Prv vl (x::y::l) r vr
  | Prv vl (OR(x,y)::l) r vr   = Prv vl (x::l) r vr
                                    andalso
                                Prv vl (y::l) r vr

  | Prv vl [] [] vr = List.exists (fn y => mem y vl) vr;

infixr 5 AND;
infixr 4 OR;

fun Wang M = Prv [] [] [M] [];


 *************************  Examples  *****************************

val x = VAR "x"; val y = VAR "y"; val z = VAR "z"; val p = VAR "p";
val q = VAR "q"; val r = VAR "r"; val s = VAR "s";

val v0 = VAR "v0"; val v1 = VAR "v1"; val v2 = VAR "v2"; val v3 = VAR "v3";
val v4 = VAR "v4"; val v5 = VAR "v5"; val v6 = VAR "v6"; val v7 = VAR "v7";
val v8 = VAR "v8"; val v9 = VAR "v9";

fun imp x y = NOT x OR y;
fun iff x y = (imp x y) AND (imp y x);

val BOOL_CASES = time Wang (x OR (NOT x));
val NOT_BCASES = time Wang (x OR (NOT y));
val IMP_REFL   = time Wang (imp x x);
val DISTRIB    = time Wang (iff (x AND (y OR z))
                            ((x AND y) OR (x AND z)));

val PEIRCE     = time Wang (imp (imp (imp p q) p) p);

val ANDREWS    = time Wang
 (imp ((imp p (q AND (r OR s))) AND ((NOT q) OR (NOT r)))
     (imp p s));

val syn323_1 = time Wang
  (NOT((v0 OR v1) AND
       (NOT v0 OR v1) AND
       (NOT v1 OR v0) AND
       (NOT v0 OR NOT v1)));

val syn029_1 =
time Wang
   (NOT((NOT v2 OR NOT v1) AND
        v0 AND
        (NOT v0 OR NOT v1 OR v2) AND
        (NOT v2 OR v1) AND (v1 OR v2)));


val syn052_1 =
time Wang
   (NOT((NOT v1 OR v0) AND
        (NOT v0 OR v1) AND
        (v1 OR v0) AND (NOT v1 OR v1) AND (NOT v0 OR NOT v1)));

val syn051_1 =
time Wang
  (NOT((v1 OR v0) AND
       (v1 OR v2) AND
       (NOT v0 OR NOT v1) AND
       (NOT v2 OR NOT v1) AND
       (NOT v0 OR v1) AND
       (NOT v1 OR v2)));

val syn044_1 =
time Wang
  (NOT((v0 OR v1) AND
       (NOT v0 OR NOT v1) AND
       (NOT v0 OR v1 OR v2) AND
       (NOT v2 OR v1) AND
       (NOT v2 OR v0) AND
       (NOT v1 OR v2)));

val syn011_1 =
time Wang
  (NOT(v6 AND
       (NOT v0 OR NOT v2) AND
       (v0 OR v1 OR v5) AND
       (NOT v2 OR NOT v1) AND
       (NOT v4 OR v2) AND
       (NOT v3 OR v2) AND
       (v3 OR v4 OR v5) AND
       (NOT v5 OR NOT v6)));

val syn032_1 =
time Wang
  (NOT((NOT v5 OR NOT v1) AND
       (NOT v4 OR NOT v0) AND
       (NOT v4 OR v0) AND
       (NOT v5 OR v1) AND
       (NOT v2 OR v4 OR v3) AND
       (v4 OR v2 OR v3) AND
       (NOT v3 OR v4 OR v5)));

val syn030_1 =
time Wang
   (NOT((NOT v4 OR NOT v0 OR NOT v1) AND
        (NOT v3 OR NOT v4 OR v0) AND
        (NOT v1 OR v0) AND
        (v0 OR v1) AND
        (NOT v0 OR v1) AND
        (NOT v1 OR NOT v0 OR v2) AND
        (NOT v2 OR v1) AND
        (NOT v1 OR v3) AND
        (NOT v2 OR NOT v3 OR v4)));

val syn054_1 =
time Wang
  (NOT((NOT v1 OR NOT v7) AND
       (NOT v2 OR NOT v0) AND
       (NOT v3 OR v7 OR v4) AND
       (NOT v6 OR v0 OR v5) AND
       (NOT v7 OR v1) AND
       (NOT v0 OR v2) AND
       (NOT v4 OR v1) AND
       (NOT v5 OR v2) AND
       (NOT v3 OR NOT v4) AND
       (NOT v6 OR NOT v5) AND
       (v6 OR v7)));


val gra001_1 =
time Wang
  (NOT((NOT v1 OR v0) AND
       (NOT v0 OR v1) AND
       (NOT v4 OR NOT v2 OR NOT v0) AND
       (NOT v4 OR v2 OR v0) AND
       (NOT v2 OR v4 OR v0) AND
       (NOT v0 OR v4 OR v2) AND
       (NOT v3 OR NOT v2 OR NOT v1) AND
       (NOT v3 OR v2 OR v1) AND
       (NOT v2 OR v3 OR v1) AND
       (NOT v1 OR v3 OR v2) AND
       (NOT v3 OR NOT v4) AND
       (v3 OR v4)));

val syn321_1 =
time Wang
  (NOT((NOT v0 OR v9) AND
       (NOT v0 OR v6) AND
       (NOT v0 OR v7) AND
       (NOT v8 OR v9) AND
       (NOT v8 OR v6) AND
       (NOT v8 OR v7) AND
       (NOT v1 OR v9) AND
       (NOT v1 OR v6) AND
       (NOT v1 OR v7) AND
       (NOT v2 OR v3) AND
       (NOT v4 OR v5) AND
       (NOT v7 OR v8) AND
       (v8 OR v9) AND
       (v8 OR v6) AND
       (v8 OR v7) AND
       (NOT v8 OR NOT v9))) ;


     End of SML version.
 ---------------------------------------------------------------------------*)