proved first chunk of subst induction

Author: MirceaS

12-proof-system-p.mm1

@@ -262,6 +262,10 @@ theorem imp_forall_fresh {x: EVar} (phi1 phi2: Pattern x) (freshness_phi1: $ _eF
   $ (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 $):
@@ -1047,6 +1051,9 @@ do {
   (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
   ))
@@ -1235,8 +1242,10 @@ theorem subset_mem_disjoint_lemma {x: EVar} (phi: Pattern) (psi: Pattern x)
   $ (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);
 
-theorem in_exists_lemma {x: EVar} (phi: Pattern x): $ (x in exists x (eVar x /\ phi)) -> x in phi $ = '();
+do {
+  (def (forall_imp_climb n) (iterate n (fn (pf) '(syl (anl imp_forall) @ imim2 ,pf)) 'id))
 
-theorem in_exists_to_forall_domain {x: EVar} (pred: Pattern x) (phi: Pattern):
-  $ (phi C= exists x (eVar x /\ pred)) -> forall x (x in phi -> x in pred)$ =
-  '(rsyl (subset_mem_disjoint_lemma eFresh_exists_same_var) @ forall_framing @ imim2 in_exists_lemma);
+  (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

@@ -93,7 +93,7 @@ axiom F2 (alpha: Pattern) {a b: EVar}:
   $ is_atom_sort alpha $ >
   $ (is_atom a alpha) ->
     (is_atom b alpha) ->
-    ((b in freshness a) <-> (eVar a != eVar b)) $;
+    (((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 $ >
@@ -115,7 +115,7 @@ axiom A1 (alpha tau: Pattern) {a b: EVar} (phi rho: Pattern a b):
     (is_of_sort rho tau) ->
     (((abstraction (eVar a) phi) == (abstraction (eVar b) rho)) <->
     ((eVar a == eVar b) /\ (phi == rho)) \/
-    ((rho C= freshness a) /\ ((swap a 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 $ >

nominal/lambda.mm1

@@ -172,53 +172,81 @@ theorem induction_principle (exp_pred exp_suff_fresh: Pattern)
 
 
 term subst_sym: Symbol;
-def subst {a: EVar} (phi1 phi2: Pattern a): Pattern a = $ (sym subst_sym) @@ (eVar a) @@ phi1 @@ phi2 $;
+def subst (a phi1 phi2: Pattern): Pattern = $ (sym subst_sym) @@ a @@ phi1 @@ phi2 $;
 
 axiom function_subst: $ ,(is_function '(sym subst_sym) '[Var Exp Exp] 'Exp) $;
 axiom subst_same_var {a: EVar} (plug: Pattern a):
   $ (is_var (eVar a)) ->
     (is_exp plug) ->
-    ((subst a (lc_var (eVar a)) plug) == plug) $;
+    ((subst (eVar a) (lc_var (eVar a)) plug) == plug) $;
 axiom subst_diff_var {a b: EVar} (plug: Pattern a b):
   $ (is_var (eVar a)) ->
     (is_var (eVar b)) ->
     ((eVar a) != (eVar b)) -> 
     (is_exp plug) ->
-    ((subst b (lc_var (eVar a)) plug) == (lc_var (eVar a))) $;
-axiom subst_app {a: EVar} (plug phi1 phi2: Pattern a):
-  $ (is_var (eVar a)) ->
-    (is_exp plug) ->
-    (is_exp phi1) ->
+    ((subst (eVar b) (lc_var (eVar a)) plug) == (lc_var (eVar a))) $;
+axiom subst_app {a: EVar} (phi1 phi2 plug: Pattern a):
+  $ (is_exp phi1) ->
     (is_exp phi2) ->
-    ((subst a (lc_app phi1 phi2) plug) == (lc_app (subst a phi1 plug) (subst a phi2 plug))) $;
+    (is_var (eVar a)) ->
+    (is_exp plug) ->
+    ((subst (eVar a) (lc_app phi1 phi2) plug) == (lc_app (subst (eVar a) phi1 plug) (subst (eVar a) phi2 plug))) $;
 axiom subst_lam {a b: EVar} (plug phi: Pattern a b):
   $ (is_var (eVar a)) ->
     (is_var (eVar b)) ->
     (is_exp plug) ->
     (is_exp phi) ->
     (fresh_for (eVar a) plug) ->
-    ((subst b (lc_lam_a a phi) plug) == (lc_lam_a a (subst b phi plug))) $;
+    ((subst (eVar b) (lc_lam_a a phi) plug) == (lc_lam_a a (subst (eVar b) phi plug))) $;
 
-def subst_induction_pred (a b phi plug1 plug2: Pattern) = $ (subst b (subst a phi plug1) plug2) == (subst a (subst b phi plug2) (subst b plug1 plug2)) $;
-def satisfying_exps {.x: EVar} (a b plug1 plug2: Pattern) = $ exists x ((eVar x) /\ subst_induction_pred a b (eVar x) plug1 plug2) $;
+def subst_induction_pred (a b phi plug1 plug2: Pattern): Pattern = $ (subst b (subst a phi plug1) plug2) == (subst a (subst b phi plug2) (subst b plug1 plug2)) $;
+def satisfying_exps {.x: EVar} (a b plug1 plug2: Pattern): Pattern = $ s_exists Exp x ((eVar x) /\ subst_induction_pred a b (eVar x) plug1 plug2) $;
 
-theorem subst_induction_app_lemma {x y: EVar} (a b phi1 plug1 plug2: Pattern)
+theorem subst_induction_app_lemma {x y: EVar} (a b plug1 plug2: Pattern)
   (a_var: $ is_sorted_func Var a $)
   (b_var: $ is_sorted_func Var b $)
   (plug1_exp: $ is_exp plug1 $)
   (plug2_exp: $ is_exp plug2 $)
   (a_fresh: $ fresh_for a phi3 $):
-  $ (subst_induction_pred a b x plug1 plug2 /\ subst_induction_pred a b y plug1 plug2) -> subst_induction_pred a b (lc_app x y) plug1 plug2 $ =
+  $ (is_exp (eVar x) /\ subst_induction_pred a b (eVar x) plug1 plug2) /\ (is_exp (eVar y) /\ subst_induction_pred a b (eVar y) plug1 plug2) -> subst_induction_pred a b (lc_app (eVar x) (eVar y)) plug1 plug2 $ =
   '();
 
-theorem subst_induction_app (a b phi1 plug1 plug2: Pattern)
+theorem subst_induction_app (a b plug1 plug2: Pattern)
   (a_var: $ is_sorted_func Var a $)
   (b_var: $ is_sorted_func Var b $)
   (plug1_exp: $ is_exp plug1 $)
   (plug2_exp: $ is_exp plug2 $)
   (a_fresh: $ fresh_for a phi3 $):
   $ (lc_app (satisfying_exps a b plug1 plug2) (satisfying_exps a b plug1 plug2)) C= (satisfying_exps a b plug1 plug2) $ =
-  '();
+  (named '(imp_to_subset @
+    rsyl (anl ,(ex_appCtx_subst 'appCtxLRVar)) @
+    exists_generalization_disjoint @
+    rsyl (anl ,(ex_appCtx_subst 'appCtxRVar)) @
+    exists_generalization_disjoint @
+    rsyl ,(appCtx_floor_commute_b_subst 'appCtxLRVar) @
+    rsyl (anim1 @ iand id id) @
+    rsyl (anl anass) @
+    rsyl (anim2 @
+      rsyl (anim2 ,(appCtx_floor_commute_subst 'appCtxLRVar)) @
+      rsyl (anim2 ancom) @
+      rsyl (anr anass) @
+      rsyl (anim2 @
+        rsyl ,(appCtx_floor_commute_b_subst 'appCtxRVar) @
+        rsyl (anim1 @ iand id id) @
+        rsyl (anl anass) @
+        anim2 @
+        rsyl (anim2 ,(appCtx_floor_commute_subst 'appCtxRVar)) @
+        rsyl (anim2 ancom) @
+        anr anass
+        ) @
+      rsyl (anl anlass) @
+      anim2 @
+      anr anass) @
+    rsyl (anr anass) @
+    rsyl (anim2 @ anim1 @ subst_induction_app_lemma a_var b_var plug1_exp plug2_exp a_fresh) @
+    rsyl (anim2 @ ancom) @
+    rsyl (anim1 @ curry @ mp ,(inst_foralls 2) function_lc_app) @
+    curry ,(func_subst_alt_thm_sorted 'x $(eVar x) /\ ((app (app _ (app (app _ (eVar x)) _)) _) == (app (app _ (app (app _ (eVar x)) _)) _))$)));
 
 
 theorem subst_induction (a b phi1 plug1 plug2: Pattern)
@@ -229,7 +257,7 @@ theorem subst_induction (a b phi1 plug1 plug2: Pattern)
   (plug2_exp: $ is_exp plug2 $)
   (a_fresh: $ fresh_for a phi3 $):
   $ (subst b (subst a phi1 plug1) plug2) == (subst a (subst b phi1 plug2) (subst b plug1 plug2)) $ =
-  '(induction_principle);
+  '();