Stage work on hreduce_permutator_shared

examples/lambda/barendregt/head_reductionScript.sml

@@ -2029,6 +2029,7 @@ Proof
  >> DISCH_TAC
  >> REWRITE_TAC [GSYM LAMl_SNOC]
  >> qabbrev_tac ‘Z' = SNOC z Z’
+ >> ‘MEM z Z'’ by rw [Abbr ‘Z'’]
  >> ‘LENGTH Z' = SUC (LENGTH Z)’ by rw [Abbr ‘Z'’]
  >> ‘ALL_DISTINCT Z'’ by rw [Abbr ‘Z'’, ALL_DISTINCT_SNOC]
  (* applying LAMl_ALPHA_ssub, ‘Y = SNOC y xs’ will be there *)
@@ -2042,35 +2043,31 @@ Proof
  >> REWRITE_TAC [GSYM fromPairs_def]
  >> qabbrev_tac ‘fm = fromPairs Z' (MAP VAR Y)’
  >> ‘FDOM fm = set Z'’ by rw [FDOM_fromPairs, Abbr ‘fm’]
- >> cheat
-(*
  >> qabbrev_tac ‘y = LAST Y’
  >> ‘!t. LAMl Y t = LAMl (SNOC y (FRONT Y)) t’
        by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_LAST_FRONT]) >> POP_ORW
  >> REWRITE_TAC [LAMl_SNOC]
  >> Know ‘fm ' M = VAR y @* MAP VAR (FRONT Y)’
  >- (simp [Abbr ‘M’, ssub_appstar] \\
      Know ‘fm ' z = VAR y’
-     >- (rw [Abbr ‘fm’, Abbr ‘z’, LAST_EL] \\
-         Know ‘fromPairs Z (MAP VAR Y) ' (EL (PRE (n + 1)) Z) =
-               EL (PRE (n + 1)) (MAP VAR Y)’
+     >- (‘z = EL n Z'’ by simp [Abbr ‘Z'’, EL_APPEND2] >> POP_ORW \\
+         simp [Abbr ‘fm’, LAST_EL] \\
+         Know ‘fromPairs Z' (MAP VAR Y) ' (EL n Z') = EL n (MAP VAR Y)’
          >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\
          rw [EL_MAP, Abbr ‘y’, LAST_EL]) >> Rewr' \\
-     Suff ‘MAP ($' fm) (MAP VAR (FRONT Z)) = MAP VAR (FRONT Y)’ >- rw [] \\
-     rw [LIST_EQ_REWRITE, LENGTH_FRONT] \\
-    ‘PRE (n + 1) = n’ by rw [] >> POP_ASSUM (fs o wrap) \\
-     rename1 ‘i < n’ \\
+     Suff ‘MAP ($' fm) (MAP VAR Z) = MAP VAR (FRONT Y)’ >- rw [] \\
+     simp [LIST_EQ_REWRITE, LENGTH_FRONT] \\
+     Q.X_GEN_TAC ‘i’ >> DISCH_TAC \\
      simp [EL_MAP, LENGTH_FRONT] \\
-     Know ‘MEM (EL i (FRONT Z)) Z’
-     >- (rw [MEM_EL] \\
-         Q.EXISTS_TAC ‘i’ >> rw [] \\
-         MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) \\
+     Know ‘MEM (EL i Z) Z'’
+     >- (rw [MEM_EL, Abbr ‘Z'’] \\
+         DISJ2_TAC >> Q.EXISTS_TAC ‘i’ >> rw []) \\
      rw [Abbr ‘fm’] \\
-     Know ‘EL i (FRONT Z) = EL i Z’
-     >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) >> Rewr' \\
+     Know ‘EL i Z = EL i Z'’
+     >- (simp [Abbr ‘Z'’, EL_APPEND1]) >> Rewr' \\
      Know ‘EL i (FRONT Y) = EL i Y’
      >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) >> Rewr' \\
-     Know ‘fromPairs Z (MAP VAR Y) ' (EL i Z) = EL i (MAP VAR Y)’
+     Know ‘fromPairs Z' (MAP VAR Y) ' (EL i Z') = EL i (MAP VAR Y)’
      >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\
      rw [EL_MAP])
  >> Rewr'
@@ -2090,6 +2087,7 @@ Proof
  >> POP_ORW
  >> REWRITE_TAC [LAMl_APPEND]
  >> qabbrev_tac ‘t1 = LAMl vs2 t’
+ >> cheat (*
  (* applying hreduce_LAMl_appstar *)
  >> Know ‘LAMl vs1 t1 @* Ns -h->* (FEMPTY |++ ZIP (vs1,Ns)) ' t1’
  >- (MATCH_MP_TAC (REWRITE_RULE [fromPairs_def] hreduce_LAMl_appstar) \\