propositional/proof_theory/derived.elf

	derived.elf revision c6506aa7090643badb5a6dca5df0ca6617558f5e
%read "prop.elf".
%read "../syntax/derived.elf".

%sig FalsityPFExt = {
  %include FalsityPF  %open.
  falseE' : ded false -> ded A = [p] falseE p A.
}.

%sig NEGPFExt = {
  %include NEGPF      %open.
  notE'   : ded A -> ded not A -> ded B = [p][q] notE q p B.
  nn : o -> o = [x] not not x.
  notnotI : ded A -> ded nn A = [p] notI ([q][_] notE' p q).
  int_notnotE : ded nn not A -> ded not A
    = [p] notI [q][_] notE' (notnotI q) p.
}.

%sig IMPPFExt = {
  %include IMPPF      %open.
  imp2I  : (ded A -> ded B -> ded C) -> ded A imp (B imp C) = [f] impI [p] impI [q] f p q.
  imp2E  : ded A imp (B imp C)  -> ded A -> ded B -> ded C  =  [p][q][r] impE (impE p q) r.
}.

%sig CONJPFExt = {
  %include CONJPF     %open.
  and3I  : ded A -> ded B -> ded C -> ded A and B and C
         = [p][q][r] andI (andI p q) r.
  and3El : ded A and B and C -> ded A = [p] andEl (andEl p).
  and3Em : ded A and B and C -> ded B = [p] andEr (andEl p).
  and3Er : ded A and B and C -> ded C = andEr.
  and_comm : ded A and B -> ded B and A = [p] andI (andEr p) (andEl p).
  and_assl : ded (A and B) and C -> ded A and (B and C) = [p] andI (and3El p) (andI (and3Em p) (and3Er p)).
  and_assr : ded A and (B and C) -> ded (A and B) and C = [p] and3I (andEl p) (andEl (andEr p)) (andEr (andEr p)).
  and_idem : ded A -> ded A and A = [p] andI p p.
}.

%sig DISJPFExt = {
  %include DISJPF     %open.
  or3Il : ded A -> ded A or B or C = [p] orIl (orIl p).
  or3Im : ded B -> ded A or B or C = [p] orIl (orIr p).
  or3Ir : ded C -> ded A or B or C = orIr.
  or3E  : ded A or B or C -> (ded A -> ded D) -> (ded B -> ded D) -> (ded C -> ded D) -> ded D
        = [p][f][g][h] orE p ([q] orE q f g) h.
  or_comm : ded A or B -> ded B or A = [p] orE p orIr orIl.
  or_assl : ded (A or B) or C -> ded A or (B or C) = [p] or3E p orIl ([r] orIr (orIl r)) ([r] orIr (orIr r)).
  or_assr : ded A or (B or C) -> ded (A or B) or C = [p] orE p or3Il ([q] orE q or3Im or3Ir).
  or_idem : ded A or A -> ded A = [p] orE p ([q]q) ([q]q).

}.

%sig EquivPF = {
  %include Equiv    %open.
  %include CONJPF   %open.
  %include IMPPF   %open.
  equivI      : (ded A -> ded B) -> (ded B -> ded A) -> ded A equiv B = [f][g] andI (impI f) (impI g).
  equivEl     : ded A equiv B -> ded A -> ded B = [p] [a] impE (andEl p) a.
  equivEr     : ded A equiv B -> ded B -> ded A = [p] [b] impE (andEr p) b.
  equiv_refl  : ded A equiv A = equivI ([a] a) ([a] a).
  equiv_sym   : ded A equiv B -> ded B equiv A
            = [p] equivI ([b] equivEr p b) ([a] equivEl p a).
  equiv_trans : ded A equiv B -> ded B equiv C -> ded A equiv C
            = [p][q] equivI ([a] equivEl q (equivEl p a)) ([c] equivEr p (equivEr q c)).
}.

%sig PLPFExt = {
   %include CPLPF        %open.
   %include FalsityPFExt %open.
   %include NEGPFExt     %open.
   %include IMPPFExt     %open.
   %include CONJPFExt    %open.
   %include DISJPFExt    %open.
   %include EquivPF      %open.
   nnotE   : ded not (not A) -> ded A = [p] orE tnd ([q:ded A] q) ([q: ded not A] notE' q p).
   indir   : (ded not A -> {B} ded B) -> ded A = [f] nnotE (notI ([p: ded not A] f p)).
   norEl   : ded not (A or B) -> ded not A = [p] notI [q] notE p (orIl q).
   norEr   : ded not (A or B) -> ded not B = [p] notI [q] notE p (orIr q).
   nimpEl  : ded not (A imp B) -> ded A = [p] indir [q] notE p (impI ([r] notE' r q)).
   nimpEr  : ded not (A imp B) -> ded not B = [p] notI [q] notE p (impI [r] q).
}.