add statement for subst induction and use support instead of freshness

Author: MirceaS

nominal/core.mm1

@@ -25,8 +25,9 @@ def swap {a b: EVar} (phi: Pattern a b): Pattern a b = $ (sym swap_sym) @@ eVar
 def moot_swap {a: EVar} (phi: Pattern a): Pattern a = $ (sym swap_sym) @@ eVar a @@ eVar a @@ phi $;
 term abstraction_sym: Symbol;
 def abstraction (phi rho: Pattern): Pattern = $ (sym abstraction_sym) @@ phi @@ rho $;
-term freshness_sym: Symbol;
-def freshness {a: EVar}: Pattern a = $ (sym freshness_sym) @@ eVar a $;
+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 EV_pattern {.a .b: EVar} (alpha phi: Pattern): Pattern =
 $ s_forall alpha a (s_forall alpha b ((swap a b phi) == phi)) $;
@@ -39,10 +40,10 @@ axiom function_abstraction:
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
   $ ,(is_function '(sym abstraction_sym) '[alpha tau] '(sort_abstraction alpha tau)) $;
-axiom pred_freshness:
+axiom multifunction_supp:
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
-  $ ,(is_multi_function '(sym freshness_sym) '[alpha] 'tau) $;
+  $ ,(is_multi_function '(sym supp_sym) '[tau] 'alpha) $;
 
 axiom EV_abstraction {a b: EVar} (alpha tau: Pattern) (phi psi: Pattern a b):
   $ is_atom_sort alpha $ >
@@ -87,18 +88,18 @@ 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) ->
-    ((phi C= freshness a) /\ (phi C= freshness b) -> ((swap a b phi) == phi)) $;
+    ((fresh_for a phi) /\ (fresh_for b phi) -> ((swap a b phi) == phi)) $;
 axiom F23 (alpha1 alpha2: Pattern) {a b: EVar}:
   $ is_atom_sort alpha1 $ >
   $ is_atom_sort alpha2 $ >
   $ (is_atom a alpha1) ->
     (is_atom b alpha2) ->
-    (b in freshness a) $;
+    (fresh_for 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 (phi C= freshness a)) $;
+    (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 $ >
@@ -114,7 +115,7 @@ 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)) <->
-    ((rho C= freshness a) /\ ((swap a b phi) == rho))) $;
+    ((fresh_for 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,28 +172,41 @@ theorem induction_principle (exp_pred exp_suff_fresh: Pattern)
 
 
 term subst_sym: Symbol;
-def subst (phi1 phi2 phi3: Pattern): Pattern = $ (sym subst_sym) @@ phi1 @@ phi2 @@ phi3 $;
+def subst {a: EVar} (phi1 phi2: Pattern a): Pattern a = $ (sym subst_sym) @@ (eVar a) @@ phi1 @@ phi2 $;
 
-axiom function_subst: $ ,(is_function '(sym subst_sym) '[Exp Var Exp] 'Exp) $;
+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 (lc_var (eVar a)) (eVar a) plug) == plug) $;
+    ((subst 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)) ->
     (is_exp plug) ->
-    ((subst (lc_var (eVar a)) (eVar b) plug) == (lc_var (eVar a))) $;
+    ((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) ->
     (is_exp phi2) ->
-    ((subst (lc_app phi1 phi2) (eVar a) plug) == (lc_app (subst phi1 (eVar a) plug) (subst phi2 (eVar a) plug))) $;
+    ((subst a (lc_app phi1 phi2) plug) == (lc_app (subst a phi1 plug) (subst 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) ->
-    (plug C= freshness a) ->
-    ((subst (lc_lam_a a phi) (eVar b) plug) == (lc_lam_a a (subst phi (eVar b) plug))) $;
+    (fresh_for a plug) ->
+    ((subst b (lc_lam_a a phi) plug) == (lc_lam_a a (subst b phi plug))) $;
+
+
+
+
+theorem subst_induction {a b: EVar} (phi1 phi2 phi3: Pattern):
+  $ (is_var (eVar a)) ->
+    (is_var (eVar b)) ->
+    (is_exp phi1) ->
+    (is_exp phi2) ->
+    (is_exp phi3) ->
+    (fresh_for a phi3) ->
+    ((subst b (subst a phi1 phi2) phi3) == (subst a (subst b phi1 phi3) (subst b phi2 phi3))) $ =
+    '();