proved the first chunk of subst_induction

Author: MirceaS

02-ml-normalization.mm1

@@ -183,19 +183,29 @@ theorem forall_framing {x: EVar} (phi1 phi2: Pattern x)
   $ (forall x phi1) -> forall x phi2 $ =
   '(con3 @ exists_framing @ con3 h);
 
-theorem or_exists_disjoint {x: EVar} (phi1: Pattern) (phi2: Pattern x):
+theorem disjoint_forall: $ phi -> forall x phi $ = '(con2 @ exists_generalization_disjoint id);
+
+theorem or_exists_fresh {x: EVar} (phi1 phi2: Pattern x) (freshness_phi1: $ _eFresh x phi1 $):
   $ (phi1 \/ exists x phi2) <-> exists x (phi1 \/ phi2) $ =
   '(ibii
     (eori
       (syl exists_intro_same_var orl)
       (exists_generalization eFresh_exists_same_var @ syl exists_intro_same_var orr))
-    (exists_generalization (eFresh_or eFresh_disjoint eFresh_exists_same_var) @ eori orl @ orrd exists_intro_same_var));
+    (exists_generalization (eFresh_or freshness_phi1 eFresh_exists_same_var) @ eori orl @ orrd exists_intro_same_var));
 
-theorem imp_exists_disjoint {x: EVar} (phi1: Pattern) (phi2: Pattern x):
+theorem or_exists_disjoint {x: EVar} (phi1: Pattern) (phi2: Pattern x):
+  $ (phi1 \/ exists x phi2) <-> exists x (phi1 \/ phi2) $ =
+  '(or_exists_fresh eFresh_disjoint);
+
+theorem imp_exists_fresh {x: EVar} (phi1 phi2: Pattern x) (freshness_phi1: $ _eFresh x phi1 $):
   $ (phi1 -> exists x phi2) <-> exists x (phi1 -> phi2) $ =
   '(ibii
-    (rsyl (imim1 dne) @ rsyl (anl or_exists_disjoint) @ exists_framing @ imim1 notnot1)
-    (rsyl (exists_framing @ imim1 dne) @ rsyl (anr or_exists_disjoint) @ imim1 notnot1));
+    (rsyl (imim1 dne) @ rsyl (anl @ or_exists_fresh @ eFresh_not freshness_phi1) @ exists_framing @ imim1 notnot1)
+    (rsyl (exists_framing @ imim1 dne) @ rsyl (anr @ or_exists_fresh @ eFresh_not freshness_phi1) @ imim1 notnot1));
+
+theorem imp_exists_disjoint {x: EVar} (phi1: Pattern) (phi2: Pattern x):
+  $ (phi1 -> exists x phi2) <-> exists x (phi1 -> phi2) $ =
+  '(imp_exists_fresh eFresh_disjoint);
 
 theorem and_exists {x: EVar} (phi1 phi2: Pattern x):
   $ (exists x (phi1 /\ phi2)) -> ((exists x phi1) /\ (exists x phi2)) $ =
@@ -212,14 +222,23 @@ theorem or_exists_bi {x: EVar} (phi1 phi2: Pattern x):
   $ (exists x (phi1 \/ phi2)) <-> ((exists x phi1) \/ (exists x phi2)) $ =
   '(ibii or_exists_forwards or_exists_reverse);
 
-theorem and_exists_disjoint_forwards {x: EVar} (phi1: Pattern) (phi2: Pattern x):
+theorem and_exists_fresh_forwards {x: EVar} (phi1 phi2: Pattern x) (freshness_phi1: $ _eFresh x phi1 $):
   $ (exists x (phi1 /\ phi2)) -> (phi1 /\ exists x phi2) $ =
   '(iand
-    (rsyl (exists_framing anl) (exists_generalization_disjoint id))
+    (rsyl (exists_framing anl) (exists_generalization freshness_phi1 id))
     (exists_framing anr));
+theorem and_exists_disjoint_forwards {x: EVar} (phi1: Pattern) (phi2: Pattern x):
+  $ (exists x (phi1 /\ phi2)) -> (phi1 /\ exists x phi2) $ =
+  '(and_exists_fresh_forwards eFresh_disjoint);
+theorem and_exists_fresh_reverse {x: EVar} (phi1 phi2: Pattern x) (freshness_phi1: $ _eFresh x phi1 $):
+  $ (phi1 /\ exists x phi2) -> (exists x (phi1 /\ phi2)) $ =
+  '(impcom @ syl (anr @ imp_exists_fresh freshness_phi1) (exists_framing ian2));
 theorem and_exists_disjoint_reverse {x: EVar} (phi1: Pattern) (phi2: Pattern x):
   $ (phi1 /\ exists x phi2) -> (exists x (phi1 /\ phi2)) $ =
-  '(impcom @ syl (anr imp_exists_disjoint) (exists_framing ian2));
+  '(and_exists_fresh_reverse eFresh_disjoint);
+theorem and_exists_fresh {x: EVar} (phi1 phi2: Pattern x) (freshness_phi1: $ _eFresh x phi1 $):
+  $ (exists x (phi1 /\ phi2)) <-> (phi1 /\ exists x phi2) $ =
+  '(ibii (and_exists_fresh_forwards freshness_phi1) (and_exists_fresh_reverse freshness_phi1));
 theorem and_exists_disjoint {x: EVar} (phi1: Pattern) (phi2: Pattern x):
   $ (exists x (phi1 /\ phi2)) <-> (phi1 /\ exists x phi2) $ =
   '(ibii and_exists_disjoint_forwards and_exists_disjoint_reverse);

12-proof-system-p.mm1

@@ -21,6 +21,11 @@ theorem eFresh_mem {x y: EVar} (phi: Pattern x y)
 theorem eFresh_ctximp_same_var {box: SVar} (ctx phi: Pattern box):
   $ _eFresh x (ctximp_app box ctx phi) $ =
   '(eFresh_exists_same_var);
+theorem eFresh_subset {x: EVar} (phi psi: Pattern x)
+  (h1: $ _eFresh x phi $)
+  (h2: $ _eFresh x psi $):
+  $ _eFresh x (phi C= psi) $ =
+  '(eFresh_not @ eFresh_ceil @ eFresh_not @ eFresh_imp h1 h2);
 
 theorem sFresh_ceil {X: SVar} (phi: Pattern X)
   (h: $ _sFresh X phi $):
@@ -114,6 +119,12 @@ theorem prop_43_exists {box: SVar} {x: EVar} (ctx: Pattern box) (phi: Pattern bo
   $ (exists x (app[ phi / box ] ctx)) -> app[ exists x phi / box ] ctx $ =
   '(exists_generalization (eFresh_appCtx eFresh_disjoint eFresh_exists_same_var) (framing exists_intro_same_var));
 
+theorem prop_43_exists_fresh {box: SVar} {x: EVar} (ctx phi: Pattern box x)
+  (ctx_fresh: $ _eFresh x ctx $):
+  $ (exists x (app[ phi / box ] ctx)) -> app[ exists x phi / box ] ctx $ =
+  '(exists_generalization (eFresh_appCtx ctx_fresh eFresh_exists_same_var) (framing exists_intro_same_var));
+
+
 theorem exists_appCtx {x: EVar} {box: SVar} (ctx: Pattern box) (phi: Pattern x):
   $ (app[ exists x phi / box ] ctx) <-> exists x (app[ phi / box ] ctx) $ =
   '(ibii propag_exists_disjoint prop_43_exists);
@@ -246,6 +257,16 @@ theorem var_subst {x y: EVar} (phi: Pattern x y):
 theorem var_subst_same_var {x: EVar} (phi: Pattern x):
   $ (forall x phi) -> phi $ = '(con1 exists_intro_same_var);
 
+
+theorem imp_forall_fresh {x: EVar} (phi1 phi2: Pattern x) (freshness_phi1: $ _eFresh x phi1 $):
+  $ (phi1 -> forall x phi2) <-> forall x (phi1 -> phi2) $ =
+  '(con2b @ bitr (cong_of_equiv_exists @ con3b @ imeq2i notnot) @ and_exists_fresh freshness_phi1);
+
+theorem imp_forall {x: EVar} (phi1: Pattern) (phi2: Pattern x):
+  $ (phi1 -> forall x phi2) <-> forall x (phi1 -> phi2) $ =
+  '(imp_forall_fresh eFresh_disjoint);
+
+
 theorem lemma_46 (phi: Pattern) {box: SVar} (ctx: Pattern box)
   (p : $ phi $):
   $ ~ (app[ (~ phi) / box ] ctx) $ = '(syl propag_bot @ framing @ notnot1 p);
@@ -555,7 +576,7 @@ theorem lemma_14 {box: SVar} (ctx psi phi1 phi2: Pattern box)
     (imim2 @ norm (norm_imp_l @ norm_trans appCtxNested_disjoint @ norm_ctxApp_pt norm_refl defNorm) (! lemma_56 box2))
   );
 
-theorem appCtx_pointwise {box: SVar} (ctx: Pattern box) (phi: Pattern):
+theorem appCtx_pointwise {box: SVar} {x: EVar} (ctx: Pattern box) (phi: Pattern):
   $ app[ phi / box ] ctx <-> exists x ((app[ eVar x / box ] ctx) /\ x in phi) $ =
   '(bitr (cong_of_equiv_appCtx (bicom lemma_62)) @
     bitr exists_appCtx @
@@ -1027,6 +1048,12 @@ do {
   (def (func_subst x phi1 phi1_pf func_phi2) '(
     exists_generalization_disjoint (mp (com12 @ syl anl ,(func_subst_explicit_helper x phi1)) ,phi1_pf) ,func_phi2
   ))
+  (def (func_subst_alt x phi1 func_phi2) '(
+    anr imp_exists_disjoint (mp (exists_framing @ syl anr ,(func_subst_explicit_helper x phi1)) ,func_phi2)
+  ))
+  (def (func_subst_alt_thm_sorted x phi1) '(
+    syl (rsyl (exists_framing imancom) (anr imp_exists_disjoint)) @ exists_framing @ anim2 @ syl anr ,(func_subst_explicit_helper x phi1)
+  ))
   (def (func_subst_thm func_phi2 x phi1) '(
     exists_generalization_disjoint (mp (com12 @ syl anl ,(func_subst_explicit_helper x (nth 4 @ get-decl phi1))) ,phi1) ,func_phi2
   ))
@@ -1101,6 +1128,12 @@ theorem propag_mem_test_12 {x y z: EVar}:
   (propag_mem 'x $~(app (sym defSym) (bot -> eVar y))$);
 
 
+
+theorem eq_equiv_to_eq_eq
+  (eq_equiv: $ (phi1 == phi2) -> (psi1 <-> psi2) $):
+  $ (phi1 == phi2) -> (psi1 == psi2) $ =
+  '(syl (framing_floor eq_equiv) @ anr floor_idem);
+
 theorem lemma_14_subset {box: SVar} (ctx psi phi1 phi2: Pattern box)
   (h: $ |_ psi _| -> (phi1 C= phi2) $):
   $ |_ psi _| -> ((app[ phi1 / box ] ctx) C= app[ phi2 / box ] ctx) $ =
@@ -1208,4 +1241,17 @@ theorem pointwise_decomposition_imp {box: SVar} {x: EVar} (ctx: Pattern box) (ph
 
 do {
   (def (pointwise_decomposition_imp_subst subst) '(norm (norm_imp (norm_forall @ norm_imp_r @ norm_subset ,subst norm_refl) @ norm_subset ,subst norm_refl) pointwise_decomposition_imp))
-};
+};
+
+theorem subset_mem_disjoint_lemma {x: EVar} (phi: Pattern) (psi: Pattern x)
+  (freshness_psi: $ _eFresh x psi $):
+  $ (phi C= psi) -> forall x ((x in phi) -> x in psi) $ =
+  '(anr (imp_forall_fresh @ eFresh_subset eFresh_disjoint freshness_psi) @ univ_gene @ com12 @ rsyl eVar_in_subset_forward @ rsyl subset_trans @ imim2 eVar_in_subset_reverse);
+
+do {
+  (def (forall_imp_climb n) (iterate n (fn (pf) '(syl (anl imp_forall) @ imim2 ,pf)) 'id))
+
+  (def (inst_foralls n) (if {n = 0} 'id
+    '(rsyl (rsyl ,(inst_foralls {n - 1}) ,(forall_imp_climb {n - 1})) var_subst_same_var)
+  ))
+};

nominal/core.mm1

@@ -27,7 +27,7 @@ term abstraction_sym: Symbol;
 def abstraction (phi rho: Pattern): Pattern = $ (sym abstraction_sym) @@ phi @@ rho $;
 term supp_sym: Symbol;
 def supp (phi: Pattern): Pattern = $ (sym supp_sym) @@ phi $;
-def fresh_for {a: EVar} (phi: Pattern a): Pattern a = $ ~ (a in supp phi) $;
+def fresh_for (phi psi: Pattern): Pattern = $ ~ (phi C= supp psi) $;
 
 def EV_pattern {.a .b: EVar} (alpha phi: Pattern): Pattern =
 $ s_forall alpha a (s_forall alpha b ((swap a b phi) == phi)) $;
@@ -88,25 +88,24 @@ axiom F1 (alpha tau: Pattern) {a b: EVar} (phi: Pattern a b):
   $ (is_atom a alpha) ->
     (is_atom b alpha) ->
     (is_of_sort phi tau) ->
-    ((fresh_for a phi) /\ (fresh_for b phi) -> ((swap a b phi) == phi)) $;
-axiom F23 (alpha1 alpha2: Pattern) {a b: EVar}:
+    ((fresh_for (eVar a) phi) /\ (fresh_for (eVar b) phi) -> ((swap a b phi) == phi)) $;
+axiom F2 (alpha: Pattern) {a b: EVar}:
+  $ is_atom_sort alpha $ >
+  $ (is_atom a alpha) ->
+    (is_atom b alpha) ->
+    (((eVar a) != (eVar b)) <-> (fresh_for (eVar a) (eVar b))) $;
+axiom F3 (alpha1 alpha2: Pattern) {a b: EVar}:
   $ is_atom_sort alpha1 $ >
   $ is_atom_sort alpha2 $ >
   $ (is_atom a alpha1) ->
     (is_atom b alpha2) ->
-    (fresh_for a (eVar b)) $;
+    (alpha1 != alpha2) ->
+    ((eVar a) != (eVar b)) $;
 axiom F4 (alpha tau phi: Pattern) {a: EVar}:
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
   $ (is_of_sort phi tau) ->
-    (s_exists alpha a (fresh_for a phi)) $;
-axiom A1_same (alpha tau: Pattern) {a: EVar} (phi rho: Pattern a):
-  $ is_atom_sort alpha $ >
-  $ is_nominal_sort tau $ >
-  $ (is_atom a alpha) ->
-    (is_of_sort phi tau) ->
-    (is_of_sort rho tau) ->
-    (((abstraction (eVar a) phi) == (abstraction (eVar a) rho)) <-> (phi == rho)) $;
+    (s_exists alpha a (fresh_for (eVar a) phi)) $;
 axiom A1 (alpha tau: Pattern) {a b: EVar} (phi rho: Pattern a b):
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
@@ -115,7 +114,8 @@ axiom A1 (alpha tau: Pattern) {a b: EVar} (phi rho: Pattern a b):
     (is_of_sort phi tau) ->
     (is_of_sort rho tau) ->
     (((abstraction (eVar a) phi) == (abstraction (eVar b) rho)) <->
-    ((fresh_for a rho) /\ ((swap a b phi) == rho))) $;
+    ((eVar a == eVar b) /\ (phi == rho)) \/
+    ((fresh_for (eVar a) rho) /\ ((swap a b phi) == rho))) $;
 axiom A2 (alpha tau: Pattern) {x a y: EVar}:
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >