finished EV proof

Author: MirceaS

01-propositional.mm1

@@ -760,3 +760,6 @@ theorem absurd_an_r: $aa /\ ~aa <-> bot$ = '(ibii (curry mpcom) absurdum);
 
 theorem imp_or_split: $ (aa -> bb \/ c) -> (aa -> bb) \/ (aa -> c) $ =
   '(rsyl (anr impexp) @ orim (imim2 dne) prop_1);
+
+theorem iand4 (h1: $ aa -> bb $) (h2: $ aa -> c $) (h3: $ aa -> d $) (h4: $ aa -> e $): $ aa -> bb /\ c /\ d /\ e $ =
+  '(iand (iand (iand h1 h2) h3) h4);

12-proof-system-p.mm1

@@ -1040,16 +1040,16 @@ theorem alpha_exists_disjoint {x y: EVar} (phi: Pattern x):
   $ (exists x phi) <-> exists y (e[ eVar y / x ] phi) $ =
   '(alpha_exists eFresh_disjoint);
 
-theorem subset_imp_subset_framing {box: SVar} (ctx phi psi: Pattern box):
+theorem imp_subset_framing {box: SVar} (ctx phi psi: Pattern box):
   $ (phi C= psi) -> ((app[ phi / box ] ctx) C= (app[ psi / box ] ctx)) $ =
   '(rsyl (anr floor_idem) @ framing_floor @ lemma_14 subset_to_imp);
-theorem eq_imp_eq_framing {box: SVar} (ctx phi psi: Pattern box):
+theorem imp_eq_framing {box: SVar} (ctx phi psi: Pattern box):
   $ (phi == psi) -> ((app[ phi / box ] ctx) == (app[ psi / box ] ctx)) $ =
-  '(rsyl (iand eq_imp_subset @ rsyl eq_sym eq_imp_subset) @ rsyl (anim subset_imp_subset_framing subset_imp_subset_framing) @ curry subset_to_eq);
+  '(rsyl (iand eq_imp_subset @ rsyl eq_sym eq_imp_subset) @ rsyl (anim imp_subset_framing imp_subset_framing) @ curry subset_to_eq);
 
 do {
-  (def (subset_imp_subset_framing_subst subst) '(norm (norm_imp_r @ norm_subset ,subst ,subst) (!! subset_imp_subset_framing box)))
-  (def (eq_imp_eq_framing_subst subst) '(norm (norm_imp_r @ norm_eq ,subst ,subst) eq_imp_eq_framing))
+  (def (imp_subset_framing_subst subst) '(norm (norm_imp_r @ norm_subset ,subst ,subst) (!! imp_subset_framing box)))
+  (def (imp_eq_framing_subst subst) '(norm (norm_imp_r @ norm_eq ,subst ,subst) imp_eq_framing))
 };
 
 do {
@@ -1257,7 +1257,7 @@ theorem ceil_idempotency_for_pred (phi: Pattern): $ ((phi == bot) \/ (phi == top
       (mp ,(func_subst_imp_to_var 'x $eVar x == |^ eVar x ^| $) @ lemma_46_floor @ bicom @ taut_equiv_top @ framing_def imp_top definedness))
     (mp ,(func_subst_imp_to_var 'x $(eVar x == bot) \/ (eVar x == top)$) ceil_is_pred)));
 
-theorem framing_imp {box: SVar} (ctx: Pattern box) (phi psi: Pattern):
+theorem subset_framing_imp {box: SVar} (ctx: Pattern box) (phi psi: Pattern):
   $ (phi C= psi) -> ((app[ phi / box ] ctx) C= (app[ psi / box ] ctx)) $ =
   '(rsyl subset_imp_or_subset_r @
     rsyl (com12 subset_to_eq @ subset_imp_subset_or_r subset_refl) @
@@ -1267,8 +1267,13 @@ theorem framing_imp {box: SVar} (ctx: Pattern box) (phi psi: Pattern):
     imp_to_subset @
     framing orl);
 
+theorem eq_framing_imp {box: SVar} (ctx: Pattern box) (phi psi: Pattern):
+  $ (phi == psi) -> ((app[ phi / box ] ctx) == (app[ psi / box ] ctx)) $ =
+  '(syl (curry subset_to_eq) @ iand (rsyl eq_imp_subset subset_framing_imp) @ rsyl eq_sym @ rsyl eq_imp_subset subset_framing_imp);
+
 do {
-  (def (framing_imp_subst subst) '(norm (norm_imp_r @ norm_subset ,subst ,subst) framing_imp))
+  (def (subset_framing_imp_subst subst) '(norm (norm_imp_r @ norm_subset ,subst ,subst) subset_framing_imp))
+  (def (eq_framing_imp_subst subst) '(norm (norm_imp_r @ norm_eq ,subst ,subst) eq_framing_imp))
 };
 
 theorem under_domain_forall {x: EVar} (phi_a phi_b phi_c phi_d: Pattern x)

nominal/core.mm1

@@ -55,7 +55,12 @@ axiom EV_abstraction {a b: EVar} (alpha tau: Pattern) (phi psi: Pattern a b):
     (is_of_sort psi tau) ->
     ((swap (eVar a) (eVar b) (abstraction phi psi)) == abstraction (swap (eVar a) (eVar b) phi) (swap (eVar a) (eVar b) psi)))) $;
 -- add EV axiom for swap
--- add EV axiom for freshness
+axiom EV_supp {a b: EVar}  (tau: Pattern) (phi: Pattern a b):
+  $ is_atom_sort alpha $ >
+  $ is_nominal_sort tau $ >
+  $ s_forall alpha a (s_forall alpha b (
+    (is_of_sort phi tau) ->
+    ((swap (eVar a) (eVar b) (supp phi)) == supp (swap (eVar a) (eVar b) phi)))) $;
 
 axiom EV_pred (alpha tau: Pattern):
   $ is_atom_sort alpha $ >