module basiclem.

accumulate basiclemSig.
accumulate lemma.

def_lemma symm 
  (Proof\ pi P\ pi A\ pi B\ 
     (Proof P proves eq A B :- P proves eq B A))
  (P\ elam A\ elam B\ extract (eq A B)
     (eq_congr P refl (eq A) A)).

def_lemma symm_store U V :- def_lemma symm U V.

def_lemma trans_eq
  (Proof\ pi C\ pi P1\ pi P2\ pi A\ pi B\ 
       (Proof C P1 P2 proves (eq A B) :-  
             P1 proves (eq A C), P2 proves (eq C B)))
  (C\ P1\ P2\ just_because).

def_lemma imp_simplify 
  (Proof\ pi V\ pi W\ pi V'\ pi B\ pi Q\ pi P\
     (Proof P Q V' proves eq V W imp B :-
        P proves eq V V',
        assume (eq V' W) => Q proves B))
  (P\Q\V'\ just_because).

def_lemma and_imp
  (Proof \ (pi A \ pi B \ pi C \ pi Q1 \ (
        Proof Q1 proves (A and B) imp C :-
            Q1 proves A imp B imp C )))
  (Q1\just_because).

def_lemma or_imp
  (Proof \ (pi A \pi B \ pi C \ pi Q1 \ pi Q2 \  (
      Proof Q1 Q2 proves (A or B) imp C :-
       Q1 proves A imp C,
       Q2 proves B imp C)))
  (Q1\ Q2\ 
   (elam A\ (elam B\ (elam C\ (extract ((A or B) imp C)
    (imp_r (or_l A B (cut Q1 (imp_l A C initial initial) (A imp C)) 
		 (cut Q2 (imp_l B C initial initial) (B imp C))))))))).

def_lemma cut_imp 
  (Proof\ pi Q1\ pi Q2\ pi A\ pi C\ 
     (Proof Q1 Q2 A proves C :- Q1 proves A, Q2 proves A imp C))
  (Q1\Q2\A\ just_because).

def_lemma gt_congr1
  (Proof\ pi P1\ pi P2\ pi A'\ pi A\ pi B\ 
     (Proof P1 P2 A' proves greater A B :-
        P1 proves eq A A', P2 proves greater A' B))
  (P1\ P2\ A'\ just_because).

def_lemma gt_congr2
  (Proof\ pi P1\ pi P2\ pi B'\ pi A\ pi B\ 
     (Proof P1 P2 B' proves greater A B :-
        P1 proves eq B B', P2 proves greater A B'))
  (P1\ P2\ B'\ just_because).

def_lemma cong_exp
  (Proof\ pi P\ pi F\ pi A\ pi B\
      (Proof F P proves eq (F A) (F B) :- P proves eq A B))
  (F\P\ just_because).

def_lemma cong_plus1
  (Proof\ pi P\ pi A\ pi B\ pi A'\
      (Proof P proves eq (plus A B) (plus A' B) :- P proves eq A A'))
  (P\ just_because).

def_lemma cong_plus2
  (Proof\ pi P\ pi A\ pi B\ pi B'\
      (Proof P proves eq (plus A B) (plus A B') :- P proves eq B B'))
  (P\ just_because).

def_lemma cong_minus1
  (Proof\ pi P\ pi A\ pi B\ pi A'\
      (Proof P proves eq (minus A B) (minus A' B) :- P proves eq A A'))
  (P\ just_because).

def_lemma cong_minus2
  (Proof\ pi P\ pi A\ pi B\ pi B'\
      (Proof P proves eq (minus A B) (minus A B') :- P proves eq B B'))
  (P\ just_because).

def_lemma cong_sel1
  (Proof\ pi P\ pi A\ pi B\ pi B'\
      (Proof P proves eq (sel A B) (sel A B') :- P proves eq B B'))
  (P\ just_because).


def_lemma cong_sel2 
  (Proof\ pi P\ pi M\ pi M'\ pi A\
     Proof P proves eq (sel M A) (sel M' A) :- P proves eq M M')
  (P\ just_because).

def_lemma cong_upd2 
  (Proof\ pi P\ pi M\ pi A\ pi A'\ pi V\ 
     Proof P proves eq (upd M A V) (upd M A' V) :- P proves eq A A')
  (P\ just_because).


def_lemma plus_redex 
  (Proof\ pi A\ pi I\ pi J\ pi K\ 
    (Proof proves  eq (plus (plus A (const I)) (const J)) (plus A (const K)) :-
     K is' I + J))
  (just_because).

def_lemma minus_redex 
  (Proof\ pi A\ pi I\ pi J\ pi K\ 
    (Proof proves  eq (minus (plus A (const I)) (const J)) (plus A (const K)) :-
     K is' I - J))
  (just_because).

def_lemma minus_zero
  (Proof\ pi A\ 
      (Proof proves eq (minus A (const 0)) A))
  (just_because).

def_lemma gt_congr_1_2 
  (Proof\ pi P1\ pi P2\ pi P3\ pi A\ pi B\ pi A'\ pi B'\
      (Proof P1 P2 P3 A' B' proves greater A B :-
          P1 proves eq A A', P2 proves eq B B', P3 proves greater A' B'))
  (P1\P2\P3\A'\B'\ just_because).

def_lemma trans_ge_gt 
 (Proof \ pi A\ pi B\ pi C\ pi P1\ pi P2\ (
   Proof P1 P2 B proves greater A C :-
     P1 proves neg (greater B A),
     P2 proves greater B C))
 (P1\ P2\ B\just_because).

def_lemma special_eq_congr
  (Proof\ pi A\ pi B\ pi A'\ pi B'\ pi P1\ pi P2\
     (Proof A B P1 P2 proves (eq A' B') :-
         assume (eq A B), P1 proves eq A A', P2 proves eq B B'))
  (A\B\P1\P2\ (trans_eq A (symm P1) (trans_eq B initial P2))).

def_lemma special_eq_congr1
  (Proof\ pi A\ pi B\ pi B'\ pi P2\
     (Proof B P2 proves (eq A B') :-
         assume (eq A B), P2 proves eq B B'))
  (B\P2\ just_because).

def_lemma special_eq_congr2
  (Proof\ pi A\ pi B\ pi A'\ pi P1\
     (Proof A P1 proves (eq A' B) :-
         assume (eq A B), P1 proves eq A A'))
  (A\P1\ just_because).

def_lemma neg_eq_congr
  (Proof\ pi A\ pi B\ pi A'\ pi B'\ pi P1\ pi P2\
     (Proof A B P1 P2 proves neg (eq A' B') :-
         assume (neg (eq A B)), P1 proves eq A A', P2 proves eq B B'))
  (A\B\P1\P2\ just_because).

def_lemma neg_eq_congr1
  (Proof\ pi A\ pi B\ pi B'\ pi P2\
     (Proof B P2 proves neg (eq A B') :-
         assume (neg (eq A B)), P2 proves eq B B'))
  (B\P2\ just_because).

def_lemma neg_eq_congr2
  (Proof\ pi A\ pi B\ pi A'\ pi P1\
     (Proof A P1 proves neg (eq A' B) :-
         assume (neg (eq A B)), P1 proves eq A A'))
  (A\P1\ just_because).

def_lemma forall_exp_eq_assump
  (Proof\ pi R\ pi A\ pi B\ pi P\
     (Proof P A R proves B :-
        assume (forall Z\ eq Z R imp A Z),
        pi Z\ assume (eq Z R) => assume (A Z) => (P Z proves B)))
  (P\A\R\ just_because).

def_lemma forall_exp_eq_l
  (Proof\ pi R\ pi A\ pi B\ pi P\
     (Proof P proves (forall Z\ eq Z R imp A Z) imp B :-
        pi Z\ assume (eq Z R) => (P Z proves A Z imp B)))
  (P\ just_because).

def_lemma readable_congr 
  (Proof\ pi P1\ pi P2\ pi V\ pi M\ pi X\
      (Proof P1 P2 V proves readable M X :-
         P1 proves readable M V, P2 proves eq X V))
  (P1\ P2\ V\ just_because).

def_lemma cut_and_l1
  (Proof\ pi A\ pi B\ pi P\ 
      (Proof P B proves A :-
             P proves A and B))
  (P\B\ just_because).

def_lemma cut_and_l2
  (Proof\ pi A\ pi B\ pi P\ 
      (Proof P A proves B :-
             P proves A and B))
  (P\A\ just_because).

def_lemma trans_eq_assump
  (Proof\ pi X\ pi Y\ pi Z\
      (Proof Z proves eq X Y :-
          assume (eq Y Z), assume (eq X Z)))
  (Z\ just_because).

def_lemma forall_l2
  (Proof\  pi B\ pi C\ pi Q\ pi T1\ pi T2\
    Proof B T1 T2 Q proves C :-
       assume (forall A1\ forall A2\ B A1 A2),
       assume (B T1 T2) => Q proves C)
  (B\T1\T2\Q\just_because).

def_lemma forall_l2a U V :- def_lemma forall_l2 U V.

def_lemma forall_l4
  (Proof\  pi B\ pi C\ pi Q\ pi T1\ pi T2\ pi T3\ pi T4\
    Proof B T1 T2 T3 T4 Q proves C :-
       assume (forall A1\ forall A2\ forall A3\ forall A4\ B A1 A2 A3 A4),
       assume (B T1 T2 T3 T4) => Q proves C)
  (B\T1\T2\T3\T4\Q\just_because).

def_lemma forall_l4a
  (Proof\  pi B\ pi C\ pi Q\ pi T1\ pi T2\ pi T3\ pi T4\
    Proof B T1 T2 T3 T4 Q proves C :-
       assume (forall A1\ forall A2\ forall A3\ forall A4\ B A1 A2 A3 A4),
       assume (B T1 T2 T3 T4) => Q proves C)
  (B\T1\T2\T3\T4\Q\just_because).

def_lemma forall_l4b
  (Proof\  pi B\ pi C\ pi Q\ pi T1\ pi T2\ pi T3\ pi T4\
    Proof B T1 T2 T3 T4 Q proves C :-
       assume (forall A1\ forall A2\ forall A3\ forall A4\ B A1 A2 A3 A4),
       assume (B T1 T2 T3 T4) => Q proves C)
  (B\T1\T2\T3\T4\Q\just_because).


def_lemma forall_l5 
  (Proof\  pi B\ pi C\ pi Q\ pi T1\ pi T2\ pi T3\ pi T4\ pi T5\
    Proof B T1 T2 T3 T4 T5 Q proves C :-
       assume (forall A1\ forall A2\ forall A3\ forall A4\ forall A5\ B A1 A2 A3 A4 A5),
       assume (B T1 T2 T3 T4 T5) => Q proves C)
  (B\T1\T2\T3\T4\T5\Q\just_because).

def_lemma forall_l6 
  (Proof\  pi B\ pi C\ pi Q\ pi T1\ pi T2\ pi T3\ pi T4\ pi T5\ pi T6\
    Proof B T1 T2 T3 T4 T5 T6 Q proves C :-
       assume (forall A1\ forall A2\ forall A3\ forall A4\ forall A5\ forall A6\ B A1 A2 A3 A4 A5 A6),
       assume (B T1 T2 T3 T4 T5 T6) => Q proves C)
  (B\T1\T2\T3\T4\T5\T6\Q\just_because).

def_lemma cutfold
  (Proof\ pi Name\ pi P\ pi B\ pi Q\ pi D\ pi F\ pi A\
    Proof Name P B Q proves D :- 
         P proves B,
         definition Name F, 
         replace Name F B A,
         assume A => Q proves D)
  (Name\P\B\Q\ just_because).

% hack to work around insufficient polymorphism in Terzo
def_lemma LemmaName Inference Proof :-
  cutfold_lemma DefName LemmaName,
  Inference = 
   (Proof\ pi P\ pi B\ pi Q\ pi D\ pi F\ pi A\
    Proof P B Q proves D :- 
         P proves B,
         definition DefName F, 
         replace DefName F B A,
         assume A => Q proves D),
  Proof = (P\B\Q\ just_because).

def_lemma contradictory_properties  
  (Proof\ pi P\ pi Q\ pi F\ pi X\ pi Y\
    Proof P Q F proves neg (eq X Y) :- P proves F X, Q proves neg (F Y))
  (P\Q\F\ just_because).

def_lemma symm_neg_eq
  (Proof\ pi P\ pi A\ pi B\ 
    Proof P proves neg (eq A B) :- P proves neg (eq B A))
  (P\ just_because).

def_lemma or_r_l
  (Proof\ pi Q1\ pi Q2\ pi A\ pi B\ pi A'\ pi B'\
     Proof A' B' Q1 Q2 proves A or B :- 
       assume (A' or B'),
       assume A' => Q1 proves A, assume B' => Q2 proves B)
  (A'\B'\Q1\Q2\ just_because).