Structure quoteTheory
signature quoteTheory =
sig
type thm = Thm.thm
(* Definitions *)
val index_TY_DEF : thm
val index_case_def : thm
val index_lt_def : thm
val index_size_def : thm
val varmap_TY_DEF : thm
val varmap_case_def : thm
val varmap_size_def : thm
(* Theorems *)
val compare_index_equal : thm
val compare_list_index : thm
val datatype_index : thm
val datatype_varmap : thm
val index_11 : thm
val index_Axiom : thm
val index_case_cong : thm
val index_case_eq : thm
val index_compare_def : thm
val index_compare_ind : thm
val index_distinct : thm
val index_induction : thm
val index_nchotomy : thm
val varmap_11 : thm
val varmap_Axiom : thm
val varmap_case_cong : thm
val varmap_case_eq : thm
val varmap_distinct : thm
val varmap_find_def : thm
val varmap_find_ind : thm
val varmap_induction : thm
val varmap_nchotomy : thm
val quote_grammars : type_grammar.grammar * term_grammar.grammar
(*
[ternaryComparisons] Parent theory of "quote"
[index_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0.
∀ $var$('index').
(∀a0.
(∃a. a0 =
(λa.
ind_type$CONSTR 0 ARB
(ind_type$FCONS a (λn. ind_type$BOTTOM)))
a ∧ $var$('index') a) ∨
(∃a. a0 =
(λa.
ind_type$CONSTR (SUC 0) ARB
(ind_type$FCONS a (λn. ind_type$BOTTOM)))
a ∧ $var$('index') a) ∨
a0 =
ind_type$CONSTR (SUC (SUC 0)) ARB
(λn. ind_type$BOTTOM) ⇒
$var$('index') a0) ⇒
$var$('index') a0) rep
[index_case_def] Definition
⊢ (∀a f f1 v. index_CASE (Left_idx a) f f1 v = f a) ∧
(∀a f f1 v. index_CASE (Right_idx a) f f1 v = f1 a) ∧
∀f f1 v. index_CASE End_idx f f1 v = v
[index_lt_def] Definition
⊢ ∀i1 i2. index_lt i1 i2 ⇔ index_compare i1 i2 = LESS
[index_size_def] Definition
⊢ (∀a. index_size (Left_idx a) = 1 + index_size a) ∧
(∀a. index_size (Right_idx a) = 1 + index_size a) ∧
index_size End_idx = 0
[varmap_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
∀ $var$('varmap').
(∀a0'.
a0' = ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM) ∨
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR (SUC 0) a0
(ind_type$FCONS a1
(ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
a0 a1 a2 ∧ $var$('varmap') a1 ∧
$var$('varmap') a2) ⇒
$var$('varmap') a0') ⇒
$var$('varmap') a0') rep
[varmap_case_def] Definition
⊢ (∀v f. varmap_CASE Empty_vm v f = v) ∧
∀a0 a1 a2 v f. varmap_CASE (Node_vm a0 a1 a2) v f = f a0 a1 a2
[varmap_size_def] Definition
⊢ (∀f. varmap_size f Empty_vm = 0) ∧
∀f a0 a1 a2.
varmap_size f (Node_vm a0 a1 a2) =
1 + (f a0 + (varmap_size f a1 + varmap_size f a2))
[compare_index_equal] Theorem
⊢ ∀i1 i2. index_compare i1 i2 = EQUAL ⇔ i1 = i2
[compare_list_index] Theorem
⊢ ∀l1 l2. list_compare index_compare l1 l2 = EQUAL ⇔ l1 = l2
[datatype_index] Theorem
⊢ DATATYPE (index Left_idx Right_idx End_idx)
[datatype_varmap] Theorem
⊢ DATATYPE (varmap Empty_vm Node_vm)
[index_11] Theorem
⊢ (∀a a'. Left_idx a = Left_idx a' ⇔ a = a') ∧
∀a a'. Right_idx a = Right_idx a' ⇔ a = a'
[index_Axiom] Theorem
⊢ ∀f0 f1 f2. ∃fn.
(∀a. fn (Left_idx a) = f0 a (fn a)) ∧
(∀a. fn (Right_idx a) = f1 a (fn a)) ∧ fn End_idx = f2
[index_case_cong] Theorem
⊢ ∀M M' f f1 v.
M = M' ∧ (∀a. M' = Left_idx a ⇒ f a = f' a) ∧
(∀a. M' = Right_idx a ⇒ f1 a = f1' a) ∧ (M' = End_idx ⇒ v = v') ⇒
index_CASE M f f1 v = index_CASE M' f' f1' v'
[index_case_eq] Theorem
⊢ index_CASE x f f1 v = v' ⇔
(∃i. x = Left_idx i ∧ f i = v') ∨
(∃i. x = Right_idx i ∧ f1 i = v') ∨ x = End_idx ∧ v = v'
[index_compare_def] Theorem
⊢ index_compare End_idx End_idx = EQUAL ∧
(∀v10. index_compare End_idx (Left_idx v10) = LESS) ∧
(∀v11. index_compare End_idx (Right_idx v11) = LESS) ∧
(∀v2. index_compare (Left_idx v2) End_idx = GREATER) ∧
(∀v3. index_compare (Right_idx v3) End_idx = GREATER) ∧
(∀n' m'.
index_compare (Left_idx n') (Left_idx m') = index_compare n' m') ∧
(∀n' m'. index_compare (Left_idx n') (Right_idx m') = LESS) ∧
(∀n' m'.
index_compare (Right_idx n') (Right_idx m') =
index_compare n' m') ∧
∀n' m'. index_compare (Right_idx n') (Left_idx m') = GREATER
[index_compare_ind] Theorem
⊢ ∀P. P End_idx End_idx ∧ (∀v10. P End_idx (Left_idx v10)) ∧
(∀v11. P End_idx (Right_idx v11)) ∧
(∀v2. P (Left_idx v2) End_idx) ∧
(∀v3. P (Right_idx v3) End_idx) ∧
(∀n' m'. P n' m' ⇒ P (Left_idx n') (Left_idx m')) ∧
(∀n' m'. P (Left_idx n') (Right_idx m')) ∧
(∀n' m'. P n' m' ⇒ P (Right_idx n') (Right_idx m')) ∧
(∀n' m'. P (Right_idx n') (Left_idx m')) ⇒
∀v v1. P v v1
[index_distinct] Theorem
⊢ (∀a' a. Left_idx a ≠ Right_idx a') ∧ (∀a. Left_idx a ≠ End_idx) ∧
∀a. Right_idx a ≠ End_idx
[index_induction] Theorem
⊢ ∀P. (∀i. P i ⇒ P (Left_idx i)) ∧ (∀i. P i ⇒ P (Right_idx i)) ∧
P End_idx ⇒
∀i. P i
[index_nchotomy] Theorem
⊢ ∀ii. (∃i. ii = Left_idx i) ∨ (∃i. ii = Right_idx i) ∨ ii = End_idx
[varmap_11] Theorem
⊢ ∀a0 a1 a2 a0' a1' a2'.
Node_vm a0 a1 a2 = Node_vm a0' a1' a2' ⇔
a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
[varmap_Axiom] Theorem
⊢ ∀f0 f1. ∃fn.
fn Empty_vm = f0 ∧
∀a0 a1 a2. fn (Node_vm a0 a1 a2) = f1 a0 a1 a2 (fn a1) (fn a2)
[varmap_case_cong] Theorem
⊢ ∀M M' v f.
M = M' ∧ (M' = Empty_vm ⇒ v = v') ∧
(∀a0 a1 a2. M' = Node_vm a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
varmap_CASE M v f = varmap_CASE M' v' f'
[varmap_case_eq] Theorem
⊢ varmap_CASE x v f = v' ⇔
x = Empty_vm ∧ v = v' ∨
∃a v'' v0. x = Node_vm a v'' v0 ∧ f a v'' v0 = v'
[varmap_distinct] Theorem
⊢ ∀a2 a1 a0. Empty_vm ≠ Node_vm a0 a1 a2
[varmap_find_def] Theorem
⊢ (∀x v2 v1. varmap_find End_idx (Node_vm x v1 v2) = x) ∧
(∀x v2 v1 i1.
varmap_find (Right_idx i1) (Node_vm x v1 v2) = varmap_find i1 v2) ∧
(∀x v2 v1 i1.
varmap_find (Left_idx i1) (Node_vm x v1 v2) = varmap_find i1 v1) ∧
∀i. varmap_find i Empty_vm = @x. T
[varmap_find_ind] Theorem
⊢ ∀P. (∀x v1 v2. P End_idx (Node_vm x v1 v2)) ∧
(∀i1 x v1 v2. P i1 v2 ⇒ P (Right_idx i1) (Node_vm x v1 v2)) ∧
(∀i1 x v1 v2. P i1 v1 ⇒ P (Left_idx i1) (Node_vm x v1 v2)) ∧
(∀i. P i Empty_vm) ⇒
∀v v1. P v v1
[varmap_induction] Theorem
⊢ ∀P. P Empty_vm ∧ (∀v v0. P v ∧ P v0 ⇒ ∀a. P (Node_vm a v v0)) ⇒
∀v. P v
[varmap_nchotomy] Theorem
⊢ ∀vv. vv = Empty_vm ∨ ∃a v v0. vv = Node_vm a v v0
*)
end
HOL 4, Kananaskis-14