type_rws
bossLib.type_rws : hol_type -> thm list
List rewrites for a concrete type.
An application type_rws ty, where ty is a declared datatype, returns
a list of rewrite rules corresponding to the type. The list typically
contains theorems about the distinctness and injectivity of
constructors, the definition of the case constant introduced at the time
the type was defined, and any extra rewrites coming from the use of
records.
Failure
If ty is not a declared datatype.
Example
> type_rws ``:'a list``;
val it =
[⊢ (∀v f. list_CASE [] v f = v) ∧
∀a0 a1 v f. list_CASE (a0::a1) v f = f a0 a1, ⊢ ∀a1 a0. [] ≠ a0::a1,
⊢ ∀a1 a0. a0::a1 ≠ [],
⊢ ∀a0 a1 a0' a1'. a0::a1 = a0'::a1' ⇔ a0 = a0' ∧ a1 = a1',
⊢ (∀f. list_size f [] = 0) ∧
∀f a0 a1. list_size f (a0::a1) = 1 + (f a0 + list_size f a1)]: thm list
> Hol_datatype `point = <| x:num ; y:num |>`;
val it = (): unit
> type_rws ``:point``;
val it =
[⊢ ∀p g f.
p with <|y updated_by f; x updated_by g|> =
p with <|x updated_by g; y updated_by f|>,
⊢ (∀g f. y_fupd f ∘ x_fupd g = x_fupd g ∘ y_fupd f) ∧
∀h g f. y_fupd f ∘ x_fupd g ∘ h = x_fupd g ∘ y_fupd f ∘ h,
⊢ (∀n n0. (point n n0).x = n) ∧ ∀n n0. (point n n0).y = n0,
⊢ (∀p f. (p with y updated_by f).x = p.x) ∧
(∀p f. (p with x updated_by f).y = p.y) ∧
(∀p f. (p with x updated_by f).x = f p.x) ∧
∀p f. (p with y updated_by f).y = f p.y,
⊢ ∀p n0 n. p with <|x := n0; y := n|> = <|x := n0; y := n|>,
⊢ ∀n01 n1 n02 n2.
<|x := n01; y := n1|> = <|x := n02; y := n2|> ⇔ n01 = n02 ∧ n1 = n2,
⊢ (∀p g f.
p with <|x updated_by f; x updated_by g|> =
p with x updated_by f ∘ g) ∧
∀p g f.
p with <|y updated_by f; y updated_by g|> = p with y updated_by f ∘ g,
⊢ ((∀g f. x_fupd f ∘ x_fupd g = x_fupd (f ∘ g)) ∧
∀h g f. x_fupd f ∘ x_fupd g ∘ h = x_fupd (f ∘ g) ∘ h) ∧
(∀g f. y_fupd f ∘ y_fupd g = y_fupd (f ∘ g)) ∧
∀h g f. y_fupd f ∘ y_fupd g ∘ h = y_fupd (f ∘ g) ∘ h,
⊢ ∀a0 a1 f. point_CASE (point a0 a1) f = f a0 a1,
⊢ ∀a0 a1 a0' a1'. point a0 a1 = point a0' a1' ⇔ a0 = a0' ∧ a1 = a1',
⊢ ∀a0 a1. point_size (point a0 a1) = 1 + (a0 + a1)]: thm list
Comments
RW_TAC and SRW_TAC automatically include these rewrites.