wip

Author: MirceaS

12-proof-system-p.mm1

@@ -167,6 +167,9 @@ theorem appCtxRVar {box: SVar} (phi1 phi2: Pattern):
 theorem appCtxLRVar {box: SVar} (phi1 phi2 phi3: Pattern):
   $ Norm (app[ phi1 / box ] (app (app phi3 (sVar box)) phi2)) (app (app phi3 phi1) phi2) $ =
   '(norm_trans appCtxL_disjoint @ norm_app appCtxRVar norm_refl);
+theorem appCtxRLRVar {box: SVar} (phi1 phi2 phi3 phi4: Pattern):
+  $ Norm (app[ phi1 / box ] (app phi4 (app (app phi3 (sVar box)) phi2))) (app phi4 (app (app phi3 phi1) phi2)) $ =
+  '(norm_trans appCtxR_disjoint @ norm_app norm_refl appCtxLRVar);
 
 theorem app_framing_l (h: $phi1 -> phi2$): $(app phi1 psi) -> (app phi2 psi)$ =
   '(norm (norm_imp appCtxLVar appCtxLVar) (! framing box _ _ _ h));
@@ -1119,3 +1122,11 @@ 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 @ ibii absurdum @ norm (norm_imp_l defNorm) propag_bot)
       (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 pointwise_decomposition {box: SVar} {x: EVar} (ctx: Pattern box) (phi psi: Pattern)
+  (hyp: $ (x in phi) -> (app[ eVar x / box ] ctx C= psi) $):
+  $ app[ phi / box ] ctx C= psi $ =
+  '(imp_to_subset @ rsyl (anl appCtx_pointwise) @
+    exists_generalization_disjoint @
+    impcom @
+    rsyl hyp subset_to_imp);

nominal/core.mm1

@@ -22,11 +22,14 @@ def is_atom {a: EVar} (alpha: Pattern): Pattern a = $ is_of_sort (eVar a) alpha
 
 term swap_sym: Symbol;
 def swap {a b: EVar} (phi: Pattern a b): Pattern a b = $ (sym swap_sym) @@ eVar a @@ eVar b @@ phi $;
+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} (phi: Pattern a): Pattern a = $ (sym freshness_sym) @@ eVar a @@ phi $;
-def fresh_in_all {a: EVar} (phi: Pattern a) {.x: EVar}: Pattern a = $ forall x (freshness a (eVar x /\ phi)) $;
+def freshness {a: EVar}: Pattern a = $ (sym freshness_sym) @@ eVar a $;
+
+def EV_pattern {.a .b: EVar} (alpha phi: Pattern): Pattern =
+$ s_forall alpha a (s_forall alpha b ((swap a b phi) == phi)) $;
 
 axiom function_swap:
   $ is_atom_sort alpha $ >
@@ -39,33 +42,20 @@ axiom function_abstraction:
 axiom pred_freshness:
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
-  $ ,(is_rel '(sym freshness_sym) '[alpha tau]) $;
+  $ ,(is_multi_function '(sym freshness_sym) '[alpha] 'tau) $;
+
 
--- Axioms of Nominal Logic
-axiom EV_app (alpha tau: Pattern) {a b: EVar} (phi rho: Pattern a b):
+
+axiom EV_pred (alpha tau: Pattern):
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
-  $ is_atom a alpha $ >
-  $ is_atom b alpha $ >
-  $ is_of_sort phi tau $ >
-  $ is_of_sort rho tau $ >
-  $ (swap a b (app phi rho)) == (app (swap a b phi) (swap a b rho)) $;
-axiom EV_sym (alpha: Pattern) {a b: EVar} (s: Symbol):
-  $ is_atom_sort alpha $ >
-  $ is_atom a alpha $ >
-  $ is_atom b alpha $ >
-  $ (swap a b (sym s)) == sym s $;
-axiom EV_pred (alpha: Pattern) {a b: EVar}:
-  $ is_atom_sort alpha $ >
-  $ is_atom a alpha $ >
-  $ is_atom b alpha $ >
-  $ (swap a b (dom pred)) == dom pred $;
+  $ EV_pattern alpha (dom tau) $;
 axiom S1 (alpha tau: Pattern) {a: EVar} (phi: Pattern a):
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
   $ is_atom a alpha $ >
   $ is_of_sort phi tau $ >
-  $ (swap a a phi) == phi $;
+  $ (moot_swap a phi) == phi $;
 axiom S2 (alpha tau: Pattern) {a b: EVar} (phi: Pattern a b):
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
@@ -84,24 +74,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 $ >
-  $ (freshness a phi) /\ (freshness b phi) -> ((swap a b phi) == phi) $;
+  $ (phi C= freshness a) /\ (phi C= freshness b) -> ((swap a b phi) == phi) $;
 axiom F2 (alpha: Pattern) {a b: EVar}:
   $ is_atom_sort alpha $ >
   $ is_atom a alpha $ >
   $ is_atom b alpha $ >
-  $ (freshness a (eVar b)) <-> (eVar a != eVar b) $;
+  $ (b in freshness a) <-> (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 $ >
   $ alpha1 != alpha2 $ >
-  $ freshness a (eVar b) $;
+  $ b in freshness a $;
 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_in_all a phi) $;
+  $ s_exists alpha a (phi C= freshness a) $;
 axiom A1 (alpha tau: Pattern) {a b: EVar} (phi rho: Pattern a b):
   $ is_atom_sort alpha $ >
   $ is_nominal_sort tau $ >
@@ -111,7 +101,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)) \/
-    ((freshness a rho) /\ ((swap a b phi) == rho)) $;
+    ((rho C= freshness a) /\ ((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

@@ -2,10 +2,12 @@ import "core.mm1";
 
 term Var_sym: Symbol;
 def Var: Pattern = $ sym Var_sym $;
+def Vars: Pattern = $ dom Var $;
 axiom Var_atom: $ is_atom_sort Var $;
 
 term Exp_sym: Symbol;
 def Exp: Pattern = $ sym Exp_sym $;
+def Exps: Pattern = $ dom Exp $;
 axiom Exp_sort: $ is_nominal_sort Exp $;
 
 term lc_var_sym: Symbol;
@@ -19,15 +21,79 @@ axiom function_lc_app: $ ,(is_function '(sym lc_var_app) '[Exp Exp] 'Exp) $;
 term lc_lam_sym: Symbol;
 def lc_lam (phi: Pattern): Pattern = $ (sym lc_lam_sym) @@ phi $;
 axiom function_lc_lam: $ ,(is_function '(sym lc_lam_sym) '[(sort_abstraction Var Exp)] 'Exp) $;
+axiom EV_lc_lam (phi: Pattern) {a b: EVar}:
+  $ s_forall Var a (s_forall Var b ((swap a b (lc_lam phi)) == lc_lam (swap a b phi))) $;
 
 axiom no_junk {X: SVar}:
-  $ (dom Exp) == mu X ( (lc_var (dom Var))
-                     \/ (lc_app (sVar X) (sVar X))
-                     \/ (lc_lam (abstraction (dom Var) (sVar X)))) $;
+  $ Exps == mu X ( (lc_var Vars)
+                \/ (lc_app (sVar X) (sVar X))
+                \/ (lc_lam (abstraction Vars (sVar X)))) $;
 
 --- no_confusion
 
 
+theorem exp_pred_ev_unquantified {x y: EVar} (exp_pred: Pattern)
+  (exp_pred_ev: $ EV_pattern Var exp_pred $):
+  $ (is_of_sort (eVar x) Var) /\ (is_of_sort (eVar y) Var) -> ((swap x y exp_pred) == exp_pred) $ =
+  '(curry @ syl var_subst_same_var @ var_subst_same_var exp_pred_ev);
+
+theorem lc_lemma_1 {x: EVar} (exp_pred exp_suff_fresh: Pattern)
+  (exp_suff_fresh_sorting: $ is_of_sort exp_suff_fresh Var $)
+  (exp_suff_fresh_nonempty: $ |^ exp_suff_fresh ^| $)
+  (h_abs: $ (lc_lam (abstraction exp_suff_fresh exp_pred)) C= exp_pred $):
+  $ s_exists Var x ((lc_lam (abstraction (eVar x) exp_pred)) C= exp_pred) $ =
+  (named '(exists_framing (rsyl (anl eVar_in_subset) @ iand
+    (com12 subset_trans exp_suff_fresh_sorting)
+    (rsyl (syl
+        ,(subset_imp_subset_framing_subst 'appCtxRVar)
+        ,(subset_imp_subset_framing_subst 'appCtxLRVar)
+      ) @ com12 subset_trans h_abs))
+    @ anl lemma_ceil_exists_membership exp_suff_fresh_nonempty));
+
+theorem lc_lemma_2 {x y: EVar} (exp_pred: Pattern)
+  (ev_unquant: $ (is_of_sort (eVar x) Var) /\ (is_of_sort (eVar y) Var) -> ((swap x y exp_pred) == exp_pred) $):
+  $ (((is_of_sort (eVar x) Var) /\ (is_of_sort (eVar y) Var)) /\ ((lc_lam (abstraction (eVar y) exp_pred)) C= exp_pred)) -> ((lc_lam (abstraction (eVar x) exp_pred)) C= exp_pred) $ =
+  '();
+
+theorem lc_lemma_3 {y: EVar} (exp_pred: Pattern)
+  (exp_suff_fresh_sorting: $ is_of_sort exp_suff_fresh Var $)
+  (exp_suff_fresh_nonempty: $ |^ exp_suff_fresh ^| $)
+  (exp_pred_ev: $ EV_pattern Var exp_pred $)
+  (h_abs: $ (lc_lam (abstraction exp_suff_fresh exp_pred)) C= exp_pred $):
+  $ is_of_sort (eVar y) Var -> ((lc_lam (abstraction (eVar y) exp_pred)) C= exp_pred) $ =
+  (named '(
+    rsyl (ian2 @ lc_lemma_1 exp_suff_fresh_sorting exp_suff_fresh_nonempty h_abs) @
+    rsyl and_exists_disjoint_reverse @
+    exists_generalization_disjoint @
+    rsyl (anr anass) @
+    lc_lemma_2 @ exp_pred_ev_unquantified exp_pred_ev));
+ 
+
+theorem freshness_irrelevance (exp_pred exp_suff_fresh: Pattern)
+  (exp_suff_fresh_sorting: $ is_of_sort exp_suff_fresh Var $)
+  (exp_suff_fresh_nonempty: $ |^ exp_suff_fresh ^| $)
+  (exp_pred_ev: $ EV_pattern Var exp_pred $)
+  (h_abs: $ (lc_lam (abstraction exp_suff_fresh exp_pred)) C= exp_pred $):
+  $ (lc_lam (abstraction Vars exp_pred)) C= exp_pred $ = (named
+  '(norm (norm_subset appCtxRLRVar norm_refl) @
+    pointwise_decomposition @
+    norm (norm_sym @ norm_imp_r @ norm_subset appCtxRLRVar norm_refl) @
+    rsyl (anl eVar_in_subset) @
+    lc_lemma_3 exp_suff_fresh_sorting exp_suff_fresh_nonempty exp_pred_ev h_abs));
+
+
+
+
+theorem prototype_induction_principle (exp_pred exp_suff_fresh: Pattern)
+  (exp_suff_fresh_sorting: $ is_of_sort exp_suff_fresh Var $)
+  (exp_suff_fresh_nonempty: $ |^ exp_suff_fresh ^| $)
+  (exp_pred_sorting: $ is_of_sort exp_pred Exp $)
+  (exp_pred_ev: $ EV_pattern Var exp_pred $)
+  (h_var: $ (lc_var Vars) C= exp_pred $)
+  (h_app: $ (lc_app exp_pred exp_pred) C= exp_pred $)
+  (h_abs: $ (lc_lam (abstraction exp_suff_fresh exp_pred)) C= exp_pred $):
+  $ Exps == exp_pred $ = '();
+
 
 
 do {
@@ -160,6 +226,7 @@ theorem induction_lemma_abs (pred freshness_arg: Pattern)
   -- @ rsyl (anim2 @ anim1 @ curry @ syl (rsyl (exists_framing imancom) (anr imp_exists_disjoint)) @ anr imp_exists_disjoint @ exists_framing imancom @ exists_framing (iand id @ curry (com23 @ syl var_subst_same_var @ var_subst_same_var h_abs)) (F4 Var_atom Exp_sort freshness_arg_Exp))
   -- @ rsyl (anim2 @ anim1 @ exists_framing @ anim1 anl)
   -- @ syl (curry @ syl anr ,(func_subst_explicit_helper 'z $(eVar z C= dom Exp) /\ (eVar z /\ (pred @@ eVar z @@ freshness_arg))$))
+  
   _);
 
 theorem induction_principle (pred freshness_arg: Pattern)

nominal/lemmas.mm1

@@ -0,0 +1 @@
+import "core.mm1";