Removed "funpow" for lambda terms, using FUNPOW (APP f) instead

examples/lambda/barendregt/solvableScript.sml

@@ -657,15 +657,16 @@ Proof
  >> qabbrev_tac ‘n = LENGTH vs’
  >> qabbrev_tac ‘m = LENGTH Ns’
  >> Q.PAT_X_ASSUM ‘N = LAMl vs (VAR y @* Ns)’ (ONCE_REWRITE_TAC o wrap)
- >> qabbrev_tac ‘Ms = GENLIST (\i. funpow K m I) n’
+ (* now we use arithmeticTheory.FUNPOW instead of locally defined one *)
+ >> qabbrev_tac ‘Ms = GENLIST (\i. FUNPOW (APP K) m I) n’
  >> Q.EXISTS_TAC ‘Ms’
  (* applying lameq_LAMl_appstar and ssub_appstar *)
  >> MATCH_MP_TAC lameq_TRANS
  >> Q.EXISTS_TAC ‘(FEMPTY |++ ZIP (vs,Ms)) ' (VAR y @* Ns)’
  >> CONJ_TAC
  >- (MATCH_MP_TAC lameq_LAMl_appstar >> art [] \\
      CONJ_TAC >- rw [Abbr ‘Ms’] \\
-     rw [EVERY_EL, Abbr ‘Ms’, closed_def, FV_funpow])
+     rw [EVERY_EL, Abbr ‘Ms’, closed_def, FV_FUNPOW])
  >> REWRITE_TAC [ssub_appstar]
  >> Q.PAT_ASSUM ‘MEM y vs’ ((Q.X_CHOOSE_THEN ‘i’ STRIP_ASSUME_TAC) o
                             (REWRITE_RULE [MEM_EL]))
@@ -680,7 +681,7 @@ Proof
      ‘j <> i’ by rw [] \\
      METIS_TAC [EL_ALL_DISTINCT_EL_EQ])
  >> Rewr'
- >> Know ‘EL i Ms = funpow K m I’
+ >> Know ‘EL i Ms = FUNPOW (APP K) m I’
  >- (‘i < n’ by rw [Abbr ‘n’] \\
      rw [Abbr ‘Ms’, EL_GENLIST])
  >> Rewr'
@@ -689,11 +690,11 @@ Proof
  >> Know ‘LENGTH Ps = m’ >- (rw [Abbr ‘m’, Abbr ‘Ps’])
  >> KILL_TAC
  >> Q.ID_SPEC_TAC ‘Ps’
- >> Induct_on ‘m’ >- ASM_SIMP_TAC (betafy(srw_ss())) [LENGTH_NIL, funpow_def]
- >> rw [funpow_SUC]
+ >> Induct_on ‘m’ >- ASM_SIMP_TAC (betafy(srw_ss())) [LENGTH_NIL, FUNPOW]
+ >> rw [FUNPOW_SUC]
  >> Cases_on ‘Ps’ >> fs []
  >> MATCH_MP_TAC lameq_TRANS
- >> Q.EXISTS_TAC ‘funpow K m I @* t’ >> rw []
+ >> Q.EXISTS_TAC ‘FUNPOW (APP K) m I @* t’ >> rw []
  >> MATCH_MP_TAC lameq_appstar_cong >> rw [lameq_K]
 QED
 

examples/lambda/basics/appFOLDLScript.sml

@@ -6,8 +6,6 @@ open termTheory binderLib;
 
 val _ = new_theory "appFOLDL"
 
-val _ = set_trace "Unicode" 1
-
 val _ = set_fixity "@*" (Infixl 901)
 val _ = Unicode.unicode_version { u = "··", tmnm = "@*"}
 val _ = overload_on ("@*", ``λf (args:term list). FOLDL APP f args``)
@@ -301,38 +299,20 @@ Proof
 QED
 
 (*---------------------------------------------------------------------------*
- *  funpow for lambda terms (cf. arithmeticTheory.FUNPOW)
+ *  funpow for lambda terms (using arithmeticTheory.FUNPOW)
  *---------------------------------------------------------------------------*)
 
-Definition funpow :
-    funpow f n (x :term) =
-        if n = 0 then x else funpow f (n - 1) (f @@ x)
-End
-
-Theorem funpow_def :
-    (!f   x. funpow f       0 x = x) /\
-    (!f n x. funpow f (SUC n) x = funpow f n (f @@ x))
-Proof
-    NTAC 2 (rw [Once funpow])
-QED
-
-Theorem funpow_SUC :
-    !f n x. funpow f (SUC n) x = f @@ (funpow f n x)
-Proof
-    Q.X_GEN_TAC ‘f’
- >> Induct_on ‘n’ >> rw [funpow_def]
- >> fs [funpow_def]
-QED
+Overload funpow = “\f. FUNPOW (APP (f :term))”
 
-Theorem FV_funpow :
-    !f x n. FV (funpow f n x) = if n = 0 then FV x else FV f UNION FV x
+Theorem FV_FUNPOW :
+    !(f :term) x n. FV (FUNPOW (APP f) n x) = if n = 0 then FV x else FV f UNION FV x
 Proof
     rpt STRIP_TAC
  >> Q.SPEC_TAC (‘n’, ‘i’)
- >> Cases_on ‘i’ >- rw [funpow_def]
+ >> Cases_on ‘i’ >- rw [FUNPOW]
  >> simp []
- >> Induct_on ‘n’ >- rw [funpow_def]
- >> fs [funpow_SUC]
+ >> Induct_on ‘n’ >- rw [FUNPOW]
+ >> fs [FUNPOW_SUC]
  >> SET_TAC []
 QED