wip

Author: MirceaS

nominal/lambda.mm1

@@ -199,22 +199,14 @@ axiom subst_lam {a b: EVar} (plug phi: Pattern a b):
     (fresh_for (eVar a) plug) ->
     ((subst (eVar b) (lc_lam_a a phi) plug) == (lc_lam_a a (subst (eVar b) phi plug))) $;
 
--- phi[a / plug1][b / plug2] == phi[b / plug2][a / plug1[b / plug2]]
-
--- (app x y)[a / plug1][b / plug2] == (app x y)[b / plug2][a / plug1[b / plug2]]
--- (app (x[a / plug1]) (y[a / plug1]))[b / plug2] == (app (x[b / plug2]) (y[b / plug2]))[a / plug1[b / plug2]]
--- app (x[a / plug1][b / plug2]) (y[a / plug1][b / plug2]) == app (x[b / plug2][a / plug1[b / plug2]]) (y[b / plug2][a / plug1[b / 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 plug1 plug2: Pattern)
-  (diff_atoms: $ a != b $)
+theorem subst_induction_app_lemma
   (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 $):
+  (plug2_exp: $ is_exp 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 $ =
   '(rsyl (anl an4) @ rsyl (anim2 @
     syl (curry eq_trans) @
@@ -228,7 +220,23 @@ theorem subst_induction_app_lemma {x y: EVar} (a b plug1 plug2: Pattern)
     (mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting a_var)) plug1_exp)
     (mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting a_var)) plug1_exp)
     )) @
-  _);
+  rsyl (anim2 @ curry eq_trans) @
+  rsyl (anim1 @ iand id id) @
+  rsyl (anl anass) @
+  rsyl (anim2 @ anim1 @ syl ,(eq_imp_eq_framing_subst 'appCtxLRVar) @ curry @ subst_app a_var plug1_exp) @
+  rsyl (anim2 @ curry eq_trans) @
+  rsyl (anim1 @ iand id id) @
+  rsyl (anl anass) @
+  rsyl (anim2 @ anim1 @ syl eq_sym @ syl (curry @ subst_app a_var (mp (mp (mp ,(function_sorting 3 'function_subst) (domain_func_sorting b_var)) plug1_exp) plug2_exp)) (anim
+    (mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting b_var)) plug2_exp)
+    (mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting b_var)) plug2_exp)
+    )) @
+  rsyl (anim2 @ impcom eq_trans) @
+  rsyl (anim1 @ iand id id) @
+  rsyl (anl anass) @
+  rsyl (anim2 @ anim1 @ syl eq_sym @ syl ,(eq_imp_eq_framing_subst 'appCtxLRVar) @ curry @ subst_app b_var plug2_exp) @
+  rsyl (anim2 @ impcom eq_trans) @
+  anr);
 
 theorem subst_induction_app (a b plug1 plug2: Pattern)
   (lemma: $ (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 $):
@@ -263,16 +271,26 @@ theorem subst_induction_app (a b plug1 plug2: Pattern)
     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_lemma (a b phi plug1 plug2: Pattern)
+  (diff_atoms: $ a != b $)
+  (a_var: $ is_sorted_func Var a $)
+  (b_var: $ is_sorted_func Var b $)
+  (phi_exp: $ is_exp phi $)
+  (plug1_exp: $ is_exp plug1 $)
+  (plug2_exp: $ is_exp plug2 $)
+  (a_fresh: $ fresh_for a plug2 $):
+  $ Exps == (satisfying_exps a b plug1 plug2) $ =
+  '(induction_principle _ _ _ _ _ (subst_induction_app @ subst_induction_app_lemma a_var b_var plug1_exp plug2_exp) _);
 
-theorem subst_induction (a b phi1 plug1 plug2: Pattern)
+theorem subst_induction (a b phi plug1 plug2: Pattern)
   (diff_atoms: $ a != b $)
   (a_var: $ is_sorted_func Var a $)
   (b_var: $ is_sorted_func Var b $)
-  (phi1_exp: $ is_exp phi1 $)
+  (phi_exp: $ is_exp phi $)
   (plug1_exp: $ is_exp plug1 $)
   (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)) $ =
+  (a_fresh: $ fresh_for a plug2 $):
+  $ (subst b (subst a phi plug1) plug2) == (subst a (subst b phi plug2) (subst b plug1 plug2)) $ =
   '();