module lemmas.

accumulate lemma.

type symm  lprf -> lprf.
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)).

type trans_eq  exp -> lprf -> lprf -> lprf.
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).

type imp_simplify  lprf -> lprf -> exp -> lprf.
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).

type and_imp  lprf -> lprf.
def_lemma and_imp
 (Proof\ pi A\ pi B\ pi C\ pi Q\
    Proof Q proves (A and B) imp C :- Q proves A imp B imp C)
 (Q\ just_because).

type or_imp  lprf -> lprf -> lprf.
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\ just_because).

type cut_imp  lprf -> lprf -> form -> lprf.
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).

type gt_congr1  lprf -> lprf -> exp -> lprf.
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).

type gt_congr2  lprf -> lprf -> exp -> lprf.
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).

type cong_exp  (exp -> exp) -> lprf -> lprf.
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).

type cong_plus1  lprf -> lprf.
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).

type cong_plus2  lprf -> lprf.
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).

type cong_minus1  lprf -> lprf.
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).

type cong_minus2  lprf -> lprf.
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).

type cong_sel1  lprf -> lprf.
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).

type plus_redex  lprf.
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).

type minus_redex  lprf.
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).

type minus_zero  lprf.
def_lemma minus_zero
 (Proof\ pi A\ Proof proves eq (minus A (const 0)) A)
 (elam A\ extract (eq (minus A (const 0)) A)
    (trans_eq (minus (plus A (const 0)) (const 0))
      (cong_minus1 (symm plus_zero))
      (trans_eq (plus A (minus (const 0) (const 0))) (symm minus_assoc2)
        (trans_eq (plus A (const 0)) (cong_plus2 eval_minus) plus_zero)))).

type gt_congr_1_2  lprf -> lprf -> lprf -> exp -> exp -> lprf.
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).

type trans_ge_gt  lprf -> lprf -> exp -> lprf.
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).

type special_eq_congr                  exp -> exp -> lprf -> lprf -> lprf.
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\ just_because).

type special_eq_congr1   exp -> lprf -> lprf.
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).

type special_eq_congr2   exp -> lprf -> lprf.
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).

type neg_eq_congr                  exp -> exp -> lprf -> lprf -> lprf.
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).

type neg_eq_congr1   exp -> lprf -> lprf.
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).

type neg_eq_congr2   exp -> lprf -> lprf.
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).

type lesseq_congr                  exp -> exp -> lprf -> lprf -> lprf.
def_lemma lesseq_congr
  (Proof\ pi A\ pi B\ pi A'\ pi B'\ pi P1\ pi P2\
     (Proof A B P1 P2 proves neg (greater A' B') :-
         assume (neg (greater A B)), P1 proves eq A A', P2 proves eq B B'))
  (A\B\P1\P2\ just_because).

type lesseq_congr1   exp -> lprf -> lprf.
def_lemma lesseq_congr1
  (Proof\ pi A\ pi B\ pi B'\ pi P2\
     (Proof B P2 proves neg (greater A B') :-
         assume (neg (greater A B)), P2 proves eq B B'))
  (B\P2\ just_because).

type lesseq_congr2   exp -> lprf -> lprf.
def_lemma lesseq_congr2
  (Proof\ pi A\ pi B\ pi A'\ pi P1\
     (Proof A P1 proves neg (greater A' B) :-
         assume (neg (greater A B)), P1 proves eq A A'))
  (A\P1\ just_because).

type  forall_exp_eq_assump  (exp -> lprf) -> (exp -> form) -> exp -> lprf.
def_lemma forall_exp_eq_assump
  (Proof\ pi R\ pi A\ pi B\ pi P\
     (Proof P A R proves B :-
        assume (forall_exp 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).

type forall_exp_eq_l  (exp -> lprf) -> lprf.
def_lemma forall_exp_eq_l
  (Proof\ pi R\ pi A\ pi B\ pi P\
     (Proof P proves (forall_exp 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).

type readable_congr  lprf -> lprf -> exp -> lprf.
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).

type neg_allocated_lemma  lprf -> lprf.
def_lemma neg_allocated_lemma
  (Proof\ pi P\ pi V\
       (Proof P proves neg (allocated V) :-
           P proves neg (greater allocptr V)))
  (P\ elam V\ just_because).

type dt_sel_relate_lemma  lprf -> lprf. 
def_lemma dt_sel_relate_lemma
  (Proof\ pi X\ pi Q1'\
     (Proof Q1' proves neg (greater allocptr X) :-
         Q1' proves neg (allocated X)))
  (Q1'\ just_because).

type add_under_forall  (exp -> lprf) -> (exp -> form) -> lprf.
def_lemma add_under_forall
  (Proof\ pi A\ pi B\ pi Q\ pi B'\
     (Proof Q B' proves (forall_exp Z\ A Z imp B Z) :-
        assume (forall_exp Z\ A Z imp B' Z),
        pi Z\ (assume (A Z) => assume (B' Z) => Q Z proves B Z)))
  (Q\B'\ just_because).

type add_under_forall_gen  lprf -> (exp -> lprf) -> exp -> (exp -> form) -> lprf.
def_lemma add_under_forall_gen
  (Proof\ pi B\ pi Q\ pi B'\ pi R\ pi R'\ pi P\
     (Proof P Q R' B' proves (forall_exp Z\ eq Z R imp B Z) :-
        assume (forall_exp Z\ eq Z R' imp B' Z),
        P proves eq R' R,
        pi Z\ (assume (eq Z R) => assume (B' Z) => Q Z proves B Z)))
  (P\Q\R'\B'\ just_because).

type add_under_forall2  lprf -> (exp -> form) -> exp -> lprf.
def_lemma add_under_forall2
  (Proof\ pi R\ pi B\ pi C\ pi Q\ (
    Proof Q C R  proves B :-
        assume (forall_exp r\ ((eq r R) imp (C r))),
        (assume (C R) => Q proves B)))
  (Q\C\R\ just_because).

type add_under_forall3  lprf -> exp -> (exp -> form) -> exp -> lprf.
def_lemma add_under_forall3
  (Proof\ pi X\ pi R\ pi C\ pi B\ pi Q\ (
      Proof Q R C X proves B :-
         assume (eq X R), assume (forall_exp r\ (eq r R imp C r)), 
         (assume (C X) => Q proves B)))
  (Q\R\C\X\ just_because).

type merge_formulas_and1  lprf.
def_lemma merge_formulas_and1
  (Proof\ pi A\ pi B\ pi C\ 
     (Proof proves (A and B) :-
          assume (A and (B and C))))
  (just_because).

type merge_formulas_and2  lprf -> form -> lprf.
def_lemma merge_formulas_and2
  (Proof\ pi A\ pi B\ pi C\ pi A'\ pi P\
     (Proof P A proves (A' and C) :-
          assume (A and (B and C)),
          assume A => P proves A'))
  (P\A\ just_because).

type merge_formulas_lemma1  lprf -> lprf.
def_lemma merge_formulas_lemma1
  (Proof\ pi P\ pi A\ pi B\ pi A'\ pi C\
      (Proof P proves (A and B) and (A' and C) :-
          assume (A and (B and C)),
          assume A => P proves A'))
  (P\ just_because).

type cut_and_l1   lprf -> form -> lprf.
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).

type cut_and_l2   lprf -> form -> lprf.
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).

type merge_formulas_lemma2   (exp -> lprf) -> (exp -> form) -> lprf.
def_lemma merge_formulas_lemma2
  (Proof\ pi P\ pi C\ pi A\ pi R\ pi B\
      (Proof P C proves (forall_exp r\ ((eq r R) imp (A r))) 
                        and (forall_exp r\ ((eq r R) imp (B r))) :-
          assume (forall_exp r\ ((eq r R) imp (C r))),
          pi r\ assume (C r) => assume (eq r R) => P r proves A r and B r))
  (P\C\ just_because).

type merge_formulas_lemma3   (exp -> lprf) -> (exp -> form) -> lprf.
def_lemma merge_formulas_lemma3
  (Proof\ pi P\ pi C\ pi A\ pi R\ pi B\
      (Proof P C proves (forall_exp r\ ((eq r R) imp (A r))) and B :-
          assume (forall_exp r\ ((eq r R) imp (C r))),
          pi r\ assume (C r) => assume (eq r R) => P r proves A r and B))
  (P\C\ just_because).

type merge_formulas_lemma4        (exp -> lprf) -> (exp -> form) -> lprf.
def_lemma merge_formulas_lemma4
  (Proof\ pi P\ pi C\ pi A\ pi R\ pi B\
      (Proof P C proves A and (forall_exp r\ ((eq r R) imp (B r))) :-
          assume (forall_exp r\ ((eq r R) imp (C r))),
          pi r\ assume (C r) => assume (eq r R) => P r proves A and B r))
  (P\C\ just_because).

type trans_eq_assump exp -> lprf.
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).

type trans_eq_assump2 exp -> lprf.
def_lemma trans_eq_assump2
 (Proof\ pi X\ pi Y\ pi Z\
    Proof Z proves eq X Y :- assume (eq Z Y) , assume (eq X Z))
 (Z\ just_because).

type safe_instr_trans_pre  lprf -> lprf -> form -> lprf.
def_lemma safe_instr_trans_pre
  (Proof\ pi Q1\ pi Q2\ pi Targets\ pi I\ pi Pre\ pi Instr\ pi Post\ pi Pre'\ 
     (Proof Q1 Q2 Pre' proves safe_instr Targets I Pre Instr Post :- 
         Q1 proves Pre imp Pre',
         Q2 proves safe_instr Targets I Pre' Instr Post, !))
  (Q1\Q2\Pre'\ just_because).

type safe_instr_alloc1  lprf -> lprf.
def_lemma safe_instr_alloc1
  (Proof\ pi X\ pi A\ pi Inv\ pi P5\
      (Proof P5 proves (eq (plus allocptr X) (plus A X)) and Inv :- 
          P5 proves eq allocptr A and Inv, !))
  (P5\ just_because).

type safe_instr_alloc2  lprf -> lprf -> lprf -> lprf -> lprf -> exp -> exp -> form -> form -> form -> lprf.
def_lemma safe_instr_alloc2
  (Proof\ pi P5\ pi P2\ pi P1\ pi Q1\ pi Q\ pi A\ pi X\ pi Inv\
     pi Pre1'\ pi Pre1\ pi Targets\ pi I\ pi Pre2\ pi Instr\ pi Post\
     (Proof P5 P2 P1 Q1 Q A X Inv Pre1' Pre1 proves
      safe_instr Targets I Pre2 Instr Post :-
        (assume Pre2 => (P5 proves eq allocptr A and Inv)),
        (assume (eq allocptr (plus A X)) => assume Inv => P2 proves Pre1'),
        (assume (eq allocptr (plus A X)) => assume Pre1' => P1 proves Pre1),
        subst (plus allocptr X) allocptr (eq allocptr (plus A X) and Inv) 
              (eq (plus allocptr X) (plus A X) and Inv),
        assume Inv => Q1 proves greater X (const 0),
        Q proves safe_instr Targets I Pre1 Instr Post ))
  (P5\P2\P1\Q1\Q\A\X\Inv\Pre1'\Pre1\ just_because).

type and_3_2  lprf.
def_lemma and_3_2
   (Proof\ pi A\ pi B\ pi C\
      (Proof proves A and B :- assume (A and (C and B))))
   (just_because).

type loadstore  lprf -> lprf -> lprf -> form -> form -> lprf.
def_lemma loadstore
  (Proof\ pi P1\ pi P2\ pi Pre2\ pi Targets\ pi I\ pi Pre'\ pi Instr\ pi Post\
          pi SafeP\ pi ReadWrite\ pi Pre1\ pi Comment\ 
     (Proof SafeP P1 P2 Pre1 ReadWrite proves 
                  safe_instr Targets I Pre' Instr Post :-
         SafeP proves (safe_instr Targets I
				  (comment Comment ReadWrite and Pre1)
				  Instr Post),
         assume Pre' => P2 proves Pre1,
         assume Pre' => P1 proves comment Comment ReadWrite))
  (SafeP\P1\P2\Pre1\ReadWrite\ just_because).

type branch_lemma  form -> (form -> form) -> lprf.
def_lemma branch_lemma
   (Proof\ pi A\ pi C\ pi Eq\ pi Com\ 
      (Proof Eq Com proves A and C :-
	 assume (A and (Com (Eq imp C))), 
  	 assume Eq,
         pi X\ (assume (Com X) => assume' X)))
   (Eq\ Com\ just_because).

type branch_lemma2  lprf -> lprf -> form -> lprf -> form -> lprf.
def_lemma branch_lemma2
  (Proof\ pi Pre'\ pi S'\ pi Eq\ pi VCtaken\ pi Post\
          pi Q1\ pi P1\ pi P2\ pi VC1\ pi VC2\
     (Proof Q1 P1 VC1 P2 VC2 proves 
      Pre' imp (comment S' (Eq imp VCtaken) and (neg Eq imp Post)) :-
            assume Pre' => Q1 proves VC1 and VC2,
            assume Eq => assume VC1 => P1 proves VCtaken,
            assume (neg Eq) => assume VC2 => P2 proves Post))
  (Q1\ P1\ VC1\ P2\ VC2\ just_because).

type unconditional_branch  lprf.
def_lemma unconditional_branch
  (Proof\ pi Targets\ pi I\ pi Pre'\ pi N\ pi Post\ pi J\
     (Proof proves safe_instr Targets I Pre' (beq (const 0) N) Post :-
              J is' I + N, nth Targets J Pre'))
  (just_because).