bossLib.std

The simplification set std_ss extends bool_ss with a useful set of rewrite rules for terms involving options, pairs, and sums. It also performs beta and eta reduction. It applies some standard rewrites to evaluate expressions involving only numerals.

The following rewrites from pairTheory are included in std_ss:

   |- !x. (FST x,SND x) = x
   |- !x y. FST (x,y) = x
   |- !x y. SND (x,y) = y
   |- !x y a b. ((x,y) = (a,b)) = (x = a) /\ (y = b)
   |- !f. CURRY (UNCURRY f) = f
   |- !f. UNCURRY (CURRY f) = f
   |- (CURRY f = CURRY g) = (f = g)
   |- (UNCURRY f = UNCURRY g) = (f = g)
   |- !f x y. CURRY f x y = f (x,y)
   |- !f x y. UNCURRY f (x,y) = f x y
   |- !f g x y. (f ## g) (x,y) = (f x,g y)

The following rewrites from sumTheory are included in std_ss:

   |- !x. ISL x ==> (INL (OUTL x) = x)
   |- !x. ISR x ==> (INR (OUTR x) = x)
   |- (!x. ISL (INL x)) /\ !y. ~ISL (INR y)
   |- (!x. ISR (INR x)) /\ !y. ~ISR (INL y)
   |- !x. OUTL (INL x) = x 
   |- !x. OUTR (INR x) = x
   |- !x y. ~(INL x = INR y) 
   |- !x y. ~(INR y = INL x)
   |- (!y x. (INL x = INL y) = (x = y)) /\
      (!y x. (INR x = INR y) = (x = y))
   |- (!f g x. case f g (INL x) = f x) /\
      (!f g y. case f g (INR y) = g y)

The following rewrites from optionTheory are included in std_ss:

   |- (!x y. (SOME x = SOME y) = (x = y))
   |- (!x. ~(NONE = SOME x))
   |- (!x. ~(SOME x = NONE))
   |- (!x. THE (SOME x) = x) 
   |- (!x. IS_SOME (SOME x) = T) 
   |- (IS_SOME NONE = F)
   |- (!x. IS_NONE x = (x = NONE))
   |- (!x. ~IS_SOME x = (x = NONE))
   |- (!x. IS_SOME x ==> (SOME (THE x) = x))
   |- (!x. case NONE SOME x = x)
   |- (!x. case x SOME x = x)
   |- (!x. IS_NONE x ==> (case e f x = e))
   |- (!x. IS_SOME x ==> (case e f x = f (THE x)))
   |- (!x. IS_SOME x ==> (case e SOME x = x))
   |- (!u f. case u f NONE = u)
   |- (!u f x. case u f (SOME x) = f x)
   |- (!f x. OPTION_MAP f (SOME x) = SOME (f x))
   |- (!f. OPTION_MAP f NONE = NONE)
   |- (OPTION_JOIN NONE = NONE)
   |- (!x. OPTION_JOIN (SOME x) = x)
   |- !f x y. (OPTION_MAP f x = SOME y) = ?z. (x = SOME z) /\ (y = f z)
   |- !f x. (OPTION_MAP f x = NONE) = (x = NONE)