Structure ordinalNotationTheory
signature ordinalNotationTheory =
sig
type thm = Thm.thm
(* Definitions *)
val cf1_def : thm
val cf2_def : thm
val coeff_def : thm
val expt_def : thm
val finp_def : thm
val is_ord_def : thm
val oless_def : thm
val ord_less_def : thm
val osyntax_TY_DEF : thm
val osyntax_case_def : thm
val osyntax_size_def : thm
val padd_def : thm
val rank_def : thm
val restn_def : thm
val tail_def : thm
(* Theorems *)
val WF_ord_less : thm
val datatype_osyntax : thm
val decompose_plus : thm
val e0_INDUCTION : thm
val e0_RECURSION : thm
val is_ord_cases : thm
val is_ord_coeff_pos : thm
val is_ord_downclosed : thm
val is_ord_equations : thm
val is_ord_expt_closed : thm
val is_ord_ind : thm
val is_ord_rules : thm
val is_ord_strong_ind : thm
val is_ord_strongind : thm
val is_ord_tail_closed : thm
val lemma : thm
val main_lemma : thm
val oless_End_End : thm
val oless_antirefl : thm
val oless_antisym : thm
val oless_cases : thm
val oless_equations : thm
val oless_expt : thm
val oless_imp_rank_leq : thm
val oless_ind : thm
val oless_rules : thm
val oless_strong_ind : thm
val oless_strongind : thm
val oless_tail : thm
val ord_add_def : thm
val ord_add_ind : thm
val ord_mult_def : thm
val ord_mult_ind : thm
val ord_sub_def : thm
val ord_sub_ind : thm
val osyntax_11 : thm
val osyntax_Axiom : thm
val osyntax_case_cong : thm
val osyntax_case_eq : thm
val osyntax_distinct : thm
val osyntax_induction : thm
val osyntax_nchotomy : thm
val padd_compute : thm
val pmult_def : thm
val pmult_ind : thm
val rank_0_End : thm
val rank_expt : thm
val rank_finp : thm
val rank_less_imp_oless : thm
val rank_positive : thm
val rank_positive_exists : thm
val rank_positive_expt : thm
val restn_compute : thm
val ordinalNotation_grammars : type_grammar.grammar * term_grammar.grammar
(*
[indexedLists] Parent theory of "ordinalNotation"
[patternMatches] Parent theory of "ordinalNotation"
[cf1_def] Definition
⊢ (∀v0 b. cf1 (End v0) b = 0) ∧
∀e1 c1 k1 b.
cf1 (Plus e1 c1 k1) b =
if ord_less (expt b) e1 then 1 + cf1 k1 b else 0
[cf2_def] Definition
⊢ ∀a b n. cf2 a b n = n + cf1 (restn a n) b
[coeff_def] Definition
⊢ (∀x. coeff (End x) = x) ∧ ∀e k t. coeff (Plus e k t) = k
[expt_def] Definition
⊢ (∀v0. expt (End v0) = End 0) ∧ ∀e k t. expt (Plus e k t) = e
[finp_def] Definition
⊢ (∀v0. finp (End v0) ⇔ T) ∧ ∀v1 v2 v3. finp (Plus v1 v2 v3) ⇔ F
[is_ord_def] Definition
⊢ is_ord =
(λa0.
∀is_ord'.
(∀a0.
(∃k. a0 = End k) ∨
(∃e k t.
(a0 = Plus e k t) ∧ is_ord' e ∧ e ≠ End 0 ∧ 0 < k ∧
is_ord' t ∧ oless (expt t) e) ⇒
is_ord' a0) ⇒
is_ord' a0)
[oless_def] Definition
⊢ oless =
(λa0 a1.
∀oless'.
(∀a0 a1.
(∃k1 k2. (a0 = End k1) ∧ (a1 = End k2) ∧ k1 < k2) ∨
(∃k1 e2 k2 t2. (a0 = End k1) ∧ (a1 = Plus e2 k2 t2)) ∨
(∃e1 k1 t1 e2 k2 t2.
(a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧
oless' e1 e2) ∨
(∃e1 k1 t1 e2 k2 t2.
(a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧
(e1 = e2) ∧ k1 < k2) ∨
(∃e1 k1 t1 e2 k2 t2.
(a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧
(e1 = e2) ∧ (k1 = k2) ∧ oless' t1 t2) ⇒
oless' a0 a1) ⇒
oless' a0 a1)
[ord_less_def] Definition
⊢ ∀x y. ord_less x y ⇔ is_ord x ∧ is_ord y ∧ oless x y
[osyntax_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
∀ $var$('osyntax').
(∀a0'.
(∃a. a0' =
(λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
a) ∨
(∃a0 a1 a2.
(a0' =
(λa0 a1 a2.
ind_type$CONSTR (SUC 0) a1
(ind_type$FCONS a0
(ind_type$FCONS a2
(λn. ind_type$BOTTOM)))) a0 a1 a2) ∧
$var$('osyntax') a0 ∧ $var$('osyntax') a2) ⇒
$var$('osyntax') a0') ⇒
$var$('osyntax') a0') rep
[osyntax_case_def] Definition
⊢ (∀a f f1. osyntax_CASE (End a) f f1 = f a) ∧
∀a0 a1 a2 f f1. osyntax_CASE (Plus a0 a1 a2) f f1 = f1 a0 a1 a2
[osyntax_size_def] Definition
⊢ (∀a. osyntax_size (End a) = 1 + a) ∧
∀a0 a1 a2.
osyntax_size (Plus a0 a1 a2) =
1 + (osyntax_size a0 + (a1 + osyntax_size a2))
[padd_def] Definition
⊢ (∀a b. padd a b 0 = ord_add a b) ∧
∀a b n.
padd a b (SUC n) = Plus (expt a) (coeff a) (padd (tail a) b n)
[rank_def] Definition
⊢ (∀v0. rank (End v0) = 0) ∧ ∀e k t. rank (Plus e k t) = 1 + rank e
[restn_def] Definition
⊢ (∀a. restn a 0 = a) ∧ ∀a n. restn a (SUC n) = restn (tail a) n
[tail_def] Definition
⊢ ∀e k t. tail (Plus e k t) = t
[WF_ord_less] Theorem
⊢ WF ord_less
[datatype_osyntax] Theorem
⊢ DATATYPE (osyntax End Plus)
[decompose_plus] Theorem
⊢ ∀e k t.
is_ord (Plus e k t) ⇒
is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧ oless (expt t) e
[e0_INDUCTION] Theorem
⊢ ∀P f. (∀x. (∀y. ord_less (f y) (f x) ⇒ P y) ⇒ P x) ⇒ ∀x. P x
[e0_RECURSION] Theorem
⊢ ∀f. ∃!g. ∀x. g x = M (RESTRICT g (λx y. ord_less (f x) (f y)) x) x
[is_ord_cases] Theorem
⊢ ∀a0.
is_ord a0 ⇔
(∃k. a0 = End k) ∨
∃e k t.
(a0 = Plus e k t) ∧ is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧
oless (expt t) e
[is_ord_coeff_pos] Theorem
⊢ ∀x. ¬finp x ∧ is_ord x ⇒ 0 < coeff x
[is_ord_downclosed] Theorem
⊢ is_ord (Plus w k t) ⇒ is_ord w ∧ is_ord t
[is_ord_equations] Theorem
⊢ (is_ord (End k) ⇔ T) ∧
(is_ord (Plus e k t) ⇔
is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧ oless (expt t) e)
[is_ord_expt_closed] Theorem
⊢ ∀x. is_ord x ⇒ is_ord (expt x)
[is_ord_ind] Theorem
⊢ ∀is_ord'.
(∀k. is_ord' (End k)) ∧
(∀e k t.
is_ord' e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord' t ∧ oless (expt t) e ⇒
is_ord' (Plus e k t)) ⇒
∀a0. is_ord a0 ⇒ is_ord' a0
[is_ord_rules] Theorem
⊢ (∀k. is_ord (End k)) ∧
∀e k t.
is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧ oless (expt t) e ⇒
is_ord (Plus e k t)
[is_ord_strong_ind] Theorem
⊢ ∀is_ord'.
(∀k. is_ord' (End k)) ∧
(∀e k t.
is_ord e ∧ is_ord' e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧
is_ord' t ∧ oless (expt t) e ⇒
is_ord' (Plus e k t)) ⇒
∀a0. is_ord a0 ⇒ is_ord' a0
[is_ord_strongind] Theorem
⊢ ∀is_ord'.
(∀k. is_ord' (End k)) ∧
(∀e k t.
is_ord e ∧ is_ord' e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧
is_ord' t ∧ oless (expt t) e ⇒
is_ord' (Plus e k t)) ⇒
∀a0. is_ord a0 ⇒ is_ord' a0
[is_ord_tail_closed] Theorem
⊢ ∀x. ¬finp x ∧ is_ord x ⇒ is_ord (tail x)
[lemma] Theorem
⊢ ∀n P.
(∃x. is_ord x ∧ P x ∧ rank x ≤ n) ⇒
∃m. is_ord m ∧ P m ∧ rank m ≤ n ∧
∀y. is_ord y ∧ rank y ≤ n ∧ oless y m ⇒ ¬P y
[main_lemma] Theorem
⊢ ∀P. (∃x. P x ∧ is_ord x) ⇒
∃x. P x ∧ is_ord x ∧ ∀y. is_ord y ∧ oless y x ⇒ ¬P y
[oless_End_End] Theorem
⊢ ∀k1 k2. oless (End k1) (End k2) ⇒ k1 < k2
[oless_antirefl] Theorem
⊢ ∀x. is_ord x ⇒ ¬oless x x
[oless_antisym] Theorem
⊢ ∀x y. is_ord x ∧ is_ord y ∧ oless x y ⇒ ¬oless y x
[oless_cases] Theorem
⊢ ∀a0 a1.
oless a0 a1 ⇔
(∃k1 k2. (a0 = End k1) ∧ (a1 = End k2) ∧ k1 < k2) ∨
(∃k1 e2 k2 t2. (a0 = End k1) ∧ (a1 = Plus e2 k2 t2)) ∨
(∃e1 k1 t1 e2 k2 t2.
(a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ oless e1 e2) ∨
(∃e1 k1 t1 e2 k2 t2.
(a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ (e1 = e2) ∧
k1 < k2) ∨
∃e1 k1 t1 e2 k2 t2.
(a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ (e1 = e2) ∧
(k1 = k2) ∧ oless t1 t2
[oless_equations] Theorem
⊢ (oless (End m) (End n) ⇔ m < n) ∧
(oless (End m) (Plus e k t) ⇔ T) ∧
(oless (Plus e k t) (End m) ⇔ F) ∧
(oless (Plus e1 k1 t1) (Plus e2 k2 t2) ⇔
if oless e1 e2 then T
else if (e1 = e2) ∧ k1 < k2 then T
else if (e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 then T
else F)
[oless_expt] Theorem
⊢ ∀e k t. is_ord (Plus e k t) ⇒ oless e (Plus e k t)
[oless_imp_rank_leq] Theorem
⊢ ∀x y. is_ord x ∧ is_ord y ∧ oless x y ⇒ rank x ≤ rank y
[oless_ind] Theorem
⊢ ∀oless'.
(∀k1 k2. k1 < k2 ⇒ oless' (End k1) (End k2)) ∧
(∀k1 e2 k2 t2. oless' (End k1) (Plus e2 k2 t2)) ∧
(∀e1 k1 t1 e2 k2 t2.
oless' e1 e2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
(∀e1 k1 t1 e2 k2 t2.
(e1 = e2) ∧ k1 < k2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
(∀e1 k1 t1 e2 k2 t2.
(e1 = e2) ∧ (k1 = k2) ∧ oless' t1 t2 ⇒
oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
∀a0 a1. oless a0 a1 ⇒ oless' a0 a1
[oless_rules] Theorem
⊢ (∀k1 k2. k1 < k2 ⇒ oless (End k1) (End k2)) ∧
(∀k1 e2 k2 t2. oless (End k1) (Plus e2 k2 t2)) ∧
(∀e1 k1 t1 e2 k2 t2.
oless e1 e2 ⇒ oless (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
(∀e1 k1 t1 e2 k2 t2.
(e1 = e2) ∧ k1 < k2 ⇒ oless (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
∀e1 k1 t1 e2 k2 t2.
(e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 ⇒
oless (Plus e1 k1 t1) (Plus e2 k2 t2)
[oless_strong_ind] Theorem
⊢ ∀oless'.
(∀k1 k2. k1 < k2 ⇒ oless' (End k1) (End k2)) ∧
(∀k1 e2 k2 t2. oless' (End k1) (Plus e2 k2 t2)) ∧
(∀e1 k1 t1 e2 k2 t2.
oless e1 e2 ∧ oless' e1 e2 ⇒
oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
(∀e1 k1 t1 e2 k2 t2.
(e1 = e2) ∧ k1 < k2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
(∀e1 k1 t1 e2 k2 t2.
(e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 ∧ oless' t1 t2 ⇒
oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
∀a0 a1. oless a0 a1 ⇒ oless' a0 a1
[oless_strongind] Theorem
⊢ ∀oless'.
(∀k1 k2. k1 < k2 ⇒ oless' (End k1) (End k2)) ∧
(∀k1 e2 k2 t2. oless' (End k1) (Plus e2 k2 t2)) ∧
(∀e1 k1 t1 e2 k2 t2.
oless e1 e2 ∧ oless' e1 e2 ⇒
oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
(∀e1 k1 t1 e2 k2 t2.
(e1 = e2) ∧ k1 < k2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
(∀e1 k1 t1 e2 k2 t2.
(e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 ∧ oless' t1 t2 ⇒
oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
∀a0 a1. oless a0 a1 ⇒ oless' a0 a1
[oless_tail] Theorem
⊢ ∀x. is_ord x ∧ ¬finp x ⇒ oless (tail x) x
[ord_add_def] Theorem
⊢ (∀n m. ord_add (End m) (End n) = End (m + n)) ∧
(∀t p m k. ord_add (End m) (Plus p k t) = Plus p k t) ∧
(∀t m k e.
ord_add (Plus e k t) (End m) = Plus e k (ord_add t (End m))) ∧
∀t2 t1 k2 k1 e2 e1.
ord_add (Plus e1 k1 t1) (Plus e2 k2 t2) =
if oless e1 e2 then Plus e2 k2 t2
else if e1 = e2 then Plus e2 (k1 + k2) t2
else Plus e1 k1 (ord_add t1 (Plus e2 k2 t2))
[ord_add_ind] Theorem
⊢ ∀P. (∀m n. P (End m) (End n)) ∧
(∀m p k t. P (End m) (Plus p k t)) ∧
(∀e k t m. P t (End m) ⇒ P (Plus e k t) (End m)) ∧
(∀e1 k1 t1 e2 k2 t2.
(¬oless e1 e2 ∧ e1 ≠ e2 ⇒ P t1 (Plus e2 k2 t2)) ⇒
P (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
∀v v1. P v v1
[ord_mult_def] Theorem
⊢ ∀y x.
ord_mult x y =
if (x = End 0) ∨ (y = End 0) then End 0
else
case (x,y) of
(End m,End n) => End (m * n)
| (End m,Plus e k t) =>
Plus (ord_add (End 0) e) k (ord_mult (End m) t)
| (Plus e' k' t',End n') => Plus e' (k' * n') t'
| (Plus e' k' t',Plus e2 k2 t2) =>
Plus (ord_add e' e2) k2 (ord_mult (Plus e' k' t') t2)
[ord_mult_ind] Theorem
⊢ ∀P. (∀x y.
(∀v v1 m e k t.
¬((x = End 0) ∨ (y = End 0)) ∧ ((x,y) = (v,v1)) ∧
(v = End m) ∧ (v1 = Plus e k t) ⇒
P (End m) t) ∧
(∀v v1 e' k' t' e2 k2 t2.
¬((x = End 0) ∨ (y = End 0)) ∧ ((x,y) = (v,v1)) ∧
(v = Plus e' k' t') ∧ (v1 = Plus e2 k2 t2) ⇒
P (Plus e' k' t') t2) ⇒
P x y) ⇒
∀v v1. P v v1
[ord_sub_def] Theorem
⊢ (∀n m. ord_sub (End m) (End n) = End (m − n)) ∧
(∀t p m k. ord_sub (End m) (Plus p k t) = End 0) ∧
(∀t m k e. ord_sub (Plus e k t) (End m) = Plus e k t) ∧
∀t2 t1 k2 k1 e2 e1.
ord_sub (Plus e1 k1 t1) (Plus e2 k2 t2) =
if oless e1 e2 then End 0
else if e1 = e2 then
if k1 < k2 then End 0
else if k1 > k2 then Plus e1 (k1 − k2) t1
else ord_sub t1 t2
else Plus e1 k1 t1
[ord_sub_ind] Theorem
⊢ ∀P. (∀m n. P (End m) (End n)) ∧
(∀m p k t. P (End m) (Plus p k t)) ∧
(∀e k t m. P (Plus e k t) (End m)) ∧
(∀e1 k1 t1 e2 k2 t2.
(¬oless e1 e2 ∧ (e1 = e2) ∧ ¬(k1 < k2) ∧ ¬(k1 > k2) ⇒
P t1 t2) ⇒
P (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
∀v v1. P v v1
[osyntax_11] Theorem
⊢ (∀a a'. (End a = End a') ⇔ (a = a')) ∧
∀a0 a1 a2 a0' a1' a2'.
(Plus a0 a1 a2 = Plus a0' a1' a2') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')
[osyntax_Axiom] Theorem
⊢ ∀f0 f1. ∃fn.
(∀a. fn (End a) = f0 a) ∧
∀a0 a1 a2. fn (Plus a0 a1 a2) = f1 a1 a0 a2 (fn a0) (fn a2)
[osyntax_case_cong] Theorem
⊢ ∀M M' f f1.
(M = M') ∧ (∀a. (M' = End a) ⇒ (f a = f' a)) ∧
(∀a0 a1 a2. (M' = Plus a0 a1 a2) ⇒ (f1 a0 a1 a2 = f1' a0 a1 a2)) ⇒
(osyntax_CASE M f f1 = osyntax_CASE M' f' f1')
[osyntax_case_eq] Theorem
⊢ (osyntax_CASE x f f1 = v) ⇔
(∃n. (x = End n) ∧ (f n = v)) ∨
∃o' n o0. (x = Plus o' n o0) ∧ (f1 o' n o0 = v)
[osyntax_distinct] Theorem
⊢ ∀a2 a1 a0 a. End a ≠ Plus a0 a1 a2
[osyntax_induction] Theorem
⊢ ∀P. (∀n. P (End n)) ∧ (∀ $o o0. P $o ∧ P o0 ⇒ ∀n. P (Plus $o n o0)) ⇒
∀ $o. P $o
[osyntax_nchotomy] Theorem
⊢ ∀oo. (∃n. oo = End n) ∨ ∃ $o n o0. oo = Plus $o n o0
[padd_compute] Theorem
⊢ (∀a b. padd a b 0 = ord_add a b) ∧
(∀a b n.
padd a b (NUMERAL (BIT1 n)) =
Plus (expt a) (coeff a) (padd (tail a) b (NUMERAL (BIT1 n) − 1))) ∧
∀a b n.
padd a b (NUMERAL (BIT2 n)) =
Plus (expt a) (coeff a) (padd (tail a) b (NUMERAL (BIT1 n)))
[pmult_def] Theorem
⊢ ∀n b a.
pmult a b n =
if (a = End 0) ∨ (b = End 0) then End 0
else
case (a,b) of
(End i,End j) => End (i * j)
| (Plus e1 c1 k1,End j) => Plus e1 (c1 * j) k1
| (v,Plus e2 c2 k2) =>
(let
m = cf2 (expt a) e2 n
in
Plus (padd (expt a) e2 m) c2 (pmult a k2 m))
[pmult_ind] Theorem
⊢ ∀P. (∀a b n.
(∀v v1 e2 c2 k2 m.
¬((a = End 0) ∨ (b = End 0)) ∧ ((a,b) = (v,v1)) ∧
(v1 = Plus e2 c2 k2) ∧ (m = cf2 (expt a) e2 n) ⇒
P a k2 m) ⇒
P a b n) ⇒
∀v v1 v2. P v v1 v2
[rank_0_End] Theorem
⊢ ∀x. (rank x = 0) ⇔ ∃n. x = End n
[rank_expt] Theorem
⊢ ∀x n. is_ord x ∧ (rank x = SUC n) ⇒ (rank (expt x) = n)
[rank_finp] Theorem
⊢ ∀x. (rank x = 0) ⇔ finp x
[rank_less_imp_oless] Theorem
⊢ ∀x y. is_ord x ∧ is_ord y ∧ rank x < rank y ⇒ oless x y
[rank_positive] Theorem
⊢ ∀x. 0 < rank x ⇔ (x = Plus (expt x) (coeff x) (tail x))
[rank_positive_exists] Theorem
⊢ ∀x. 0 < rank x ⇔ ∃e c t. x = Plus e c t
[rank_positive_expt] Theorem
⊢ ∀x n. (rank x = SUC n) ⇒ (rank (expt x) = n)
[restn_compute] Theorem
⊢ (∀a. restn a 0 = a) ∧
(∀a n.
restn a (NUMERAL (BIT1 n)) =
restn (tail a) (NUMERAL (BIT1 n) − 1)) ∧
∀a n.
restn a (NUMERAL (BIT2 n)) = restn (tail a) (NUMERAL (BIT1 n))
*)
end
HOL 4, Kananaskis-14