src/FOLP/simpdata.ML
changeset 3836 f1a1817659e6
parent 2603 4988dda71c0b
child 5304 c133f16febc7
equal deleted inserted replaced
3835:9a5a4e123859 3836:f1a1817659e6
    39  ["(True <-> P) <-> P",         "(P <-> True) <-> P",
    39  ["(True <-> P) <-> P",         "(P <-> True) <-> P",
    40   "(P <-> P) <-> True",
    40   "(P <-> P) <-> True",
    41   "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
    41   "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
    42 
    42 
    43 val quant_rews = map int_prove_fun
    43 val quant_rews = map int_prove_fun
    44  ["(ALL x.P) <-> P",    "(EX x.P) <-> P"];
    44  ["(ALL x. P) <-> P",    "(EX x. P) <-> P"];
    45 
    45 
    46 (*These are NOT supplied by default!*)
    46 (*These are NOT supplied by default!*)
    47 val distrib_rews  = map int_prove_fun
    47 val distrib_rews  = map int_prove_fun
    48  ["~(P|Q) <-> ~P & ~Q",
    48  ["~(P|Q) <-> ~P & ~Q",
    49   "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
    49   "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
    50   "(P | Q --> R) <-> (P --> R) & (Q --> R)",
    50   "(P | Q --> R) <-> (P --> R) & (Q --> R)",
    51   "~(EX x.NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
    51   "~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
    52   "((EX x.NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
    52   "((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
    53   "(EX x.NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
    53   "(EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
    54   "NORM(Q) & (EX x.NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
    54   "NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
    55 
    55 
    56 val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)";
    56 val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)";
    57 
    57 
    58 fun make_iff_T th = th RS P_Imp_P_iff_T;
    58 fun make_iff_T th = th RS P_Imp_P_iff_T;
    59 
    59