wip

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 $):
@@ -246,6 +251,12 @@ 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 lemma_46 (phi: Pattern) {box: SVar} (ctx: Pattern box)
   (p : $ phi $):
   $ ~ (app[ (~ phi) / box ] ctx) $ = '(syl propag_bot @ framing @ notnot1 p);
@@ -555,7 +566,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 @
@@ -1208,4 +1219,19 @@ 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);
+
+theorem in_exists_lemma {x: EVar} (phi: Pattern x): $ (x in exists x (eVar x /\ phi)) -> x in phi $ = '();
+
+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);
+
+theorem eq_pred_pointwise {box1 box2: SVar} {x: EVar} (phi: Pattern x box1 box2) (ctx1 ctx2: Pattern x box1 box2):
+  $ (phi C= exists x (eVar x /\ ((app[ eVar x / box1 ] ctx1) == (app[ eVar x / box2 ] ctx2)))) ->
+    ((app[ phi / box1 ] ctx1) == (app[ phi / box2 ] ctx2)) $ = '();

nominal/lambda.mm1

@@ -201,12 +201,56 @@ axiom subst_lam {a b: EVar} (plug phi: Pattern a b):
 
 
 
-theorem subst_induction {a b: EVar} (phi1 phi2 phi3: Pattern):
+theorem subst_induction {a b: EVar} (phi1 plug1 plug2: Pattern):
   $ (is_var (eVar a)) ->
     (is_var (eVar b)) ->
     (is_exp phi1) ->
-    (is_exp phi2) ->
-    (is_exp phi3) ->
+    (is_exp plug1) ->
+    (is_exp plug2) ->
     (fresh_for a phi3) ->
-    ((subst b (subst a phi1 phi2) phi3) == (subst a (subst b phi1 phi3) (subst b phi2 phi3))) $ =
+    ((subst b (subst a phi1 plug1) plug2) == (subst a (subst b phi1 plug2) (subst b plug1 plug2))) $ =
     '();
+
+
+
+term reduce_sym: Symbol;
+def reduce (phi: Pattern): Pattern = $ (sym reduce_sym) @@ phi $;
+
+-- axiom reduce_subst {a: EVar} (phi1 phi2: Pattern a):
+--   $ 
+--     (reduce (lc_app (lc_lam_a a phi1) phi2)) == () $;
+
+
+
+
+-- term red_sym: Symbol;
+-- def red (phi: Pattern) : Pattern = $ (sym red_sym) @@ phi $;
+
+-- axiom red_app (phi rho: Pattern)
+--   (phi_sorting: $ is_of_sort phi Exp $)
+--   (rho_sorting: $ is_of_sort rho Exp $):
+--   $ (red (app phi rho)) == (app (red phi) rho) \/ (app phi (red rho)) \/ (s_exists )$;
+
+
+-- def double (phi: Pattern) = exists x (a(a(x)) /\ a(x) in phi)
+
+
+
+
+--- term Type_sym: Symbol;
+--- def Type: Pattern = $ sym Type_sym $;
+--- def Types: Pattern = $ dom Type $;
+--- 
+--- term fn_type_sym: Symbol;
+--- def fn_type (phi rho: Pattern): Pattern = $ (sym fn_type_sym) @@ phi @@ rho $;
+--- axiom function_fn_type: $ ,(is_function '(sym fn_type_symfn_type_sym) '[Type] 'Type) $;
+--- 
+--- 
+--- def is_typing_context (phi: Pattern): Pattern = $ ,(is_function '(phi) '[Var] 'Type) $;
+--- 
+--- def wf (c t: Pattern) {a u t1 t2: EVar} {X: SVar}: Pattern =
+--- $ mu X (
+---      (s_exists Var a ((lc_var a) /\ t == (c @@ a)))
+---   \/ (s_exists Type u (lc_app () ()))
+---   \/ ()
+---   ) $;