diff options
Diffstat (limited to '')
-rw-r--r-- | backends/hol4/divDefLibTestTheory.sig | 434 |
1 files changed, 434 insertions, 0 deletions
diff --git a/backends/hol4/divDefLibTestTheory.sig b/backends/hol4/divDefLibTestTheory.sig new file mode 100644 index 00000000..8da736ab --- /dev/null +++ b/backends/hol4/divDefLibTestTheory.sig @@ -0,0 +1,434 @@ +signature divDefLibTestTheory = +sig + type thm = Thm.thm + + (* Definitions *) + val btree_TY_DEF : thm + val btree_case_def : thm + val btree_size_def : thm + val list_t_TY_DEF : thm + val list_t_case_def : thm + val list_t_size_def : thm + val node_TY_DEF : thm + val node_case_def : thm + val tree_TY_DEF : thm + val tree_case_def : thm + val tree_size_def : thm + + (* Theorems *) + val btree_11 : thm + val btree_Axiom : thm + val btree_case_cong : thm + val btree_case_eq : thm + val btree_distinct : thm + val btree_height_def : thm + val btree_induction : thm + val btree_nchotomy : thm + val datatype_btree : thm + val datatype_list_t : thm + val datatype_tree : thm + val even_def : thm + val list_t_11 : thm + val list_t_Axiom : thm + val list_t_case_cong : thm + val list_t_case_eq : thm + val list_t_distinct : thm + val list_t_induction : thm + val list_t_nchotomy : thm + val node_11 : thm + val node_Axiom : thm + val node_case_cong : thm + val node_case_eq : thm + val node_induction : thm + val node_nchotomy : thm + val nth_def : thm + val odd_def : thm + val tree_11 : thm + val tree_Axiom : thm + val tree_case_cong : thm + val tree_case_eq : thm + val tree_distinct : thm + val tree_height_def : thm + val tree_induction : thm + val tree_nchotomy : thm + val tree_nodes_height_def : thm + val tree_size_eq : thm + + val divDefLibTest_grammars : type_grammar.grammar * term_grammar.grammar +(* + [divDef] Parent theory of "divDefLibTest" + + [btree_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0'. + ∀ $var$('btree'). + (∀a0'. + (∃a. a0' = + (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM)) + a) ∨ + (∃a0 a1. + a0' = + (λa0 a1. + ind_type$CONSTR (SUC 0) ARB + (ind_type$FCONS a0 + (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))) + a0 a1 ∧ $var$('btree') a0 ∧ $var$('btree') a1) ⇒ + $var$('btree') a0') ⇒ + $var$('btree') a0') rep + + [btree_case_def] Definition + + ⊢ (∀a f f1. btree_CASE (BLeaf a) f f1 = f a) ∧ + ∀a0 a1 f f1. btree_CASE (BNode a0 a1) f f1 = f1 a0 a1 + + [btree_size_def] Definition + + ⊢ (∀f a. btree_size f (BLeaf a) = 1 + f a) ∧ + ∀f a0 a1. + btree_size f (BNode a0 a1) = + 1 + (btree_size f a0 + btree_size f a1) + + [list_t_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0'. + ∀ $var$('list_t'). + (∀a0'. + (∃a0 a1. + a0' = + (λa0 a1. + ind_type$CONSTR 0 a0 + (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) + a0 a1 ∧ $var$('list_t') a1) ∨ + a0' = + ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒ + $var$('list_t') a0') ⇒ + $var$('list_t') a0') rep + + [list_t_case_def] Definition + + ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧ + ∀f v. list_t_CASE ListNil f v = v + + [list_t_size_def] Definition + + ⊢ (∀f a0 a1. + list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧ + ∀f. list_t_size f ListNil = 0 + + [node_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa1'. + ∀ $var$('tree') $var$('node') + $var$('@temp @ind_typedivDefLibTest8list'). + (∀a0'. + (∃a. a0' = + (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM)) + a) ∨ + (∃a. a0' = + (λa. + ind_type$CONSTR (SUC 0) ARB + (ind_type$FCONS a (λn. ind_type$BOTTOM))) + a ∧ $var$('node') a) ⇒ + $var$('tree') a0') ∧ + (∀a1'. + (∃a. a1' = + (λa. + ind_type$CONSTR (SUC (SUC 0)) ARB + (ind_type$FCONS a (λn. ind_type$BOTTOM))) + a ∧ + $var$('@temp @ind_typedivDefLibTest8list') a) ⇒ + $var$('node') a1') ∧ + (∀a2. + a2 = + ind_type$CONSTR (SUC (SUC (SUC 0))) ARB + (λn. ind_type$BOTTOM) ∨ + (∃a0 a1. + a2 = + (λa0 a1. + ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) ARB + (ind_type$FCONS a0 + (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))) + a0 a1 ∧ $var$('tree') a0 ∧ + $var$('@temp @ind_typedivDefLibTest8list') a1) ⇒ + $var$('@temp @ind_typedivDefLibTest8list') a2) ⇒ + $var$('node') a1') rep + + [node_case_def] Definition + + ⊢ ∀a f. node_CASE (Node a) f = f a + + [tree_TY_DEF] Definition + + ⊢ ∃rep. + TYPE_DEFINITION + (λa0'. + ∀ $var$('tree') $var$('node') + $var$('@temp @ind_typedivDefLibTest8list'). + (∀a0'. + (∃a. a0' = + (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM)) + a) ∨ + (∃a. a0' = + (λa. + ind_type$CONSTR (SUC 0) ARB + (ind_type$FCONS a (λn. ind_type$BOTTOM))) + a ∧ $var$('node') a) ⇒ + $var$('tree') a0') ∧ + (∀a1'. + (∃a. a1' = + (λa. + ind_type$CONSTR (SUC (SUC 0)) ARB + (ind_type$FCONS a (λn. ind_type$BOTTOM))) + a ∧ + $var$('@temp @ind_typedivDefLibTest8list') a) ⇒ + $var$('node') a1') ∧ + (∀a2. + a2 = + ind_type$CONSTR (SUC (SUC (SUC 0))) ARB + (λn. ind_type$BOTTOM) ∨ + (∃a0 a1. + a2 = + (λa0 a1. + ind_type$CONSTR (SUC (SUC (SUC (SUC 0)))) ARB + (ind_type$FCONS a0 + (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))) + a0 a1 ∧ $var$('tree') a0 ∧ + $var$('@temp @ind_typedivDefLibTest8list') a1) ⇒ + $var$('@temp @ind_typedivDefLibTest8list') a2) ⇒ + $var$('tree') a0') rep + + [tree_case_def] Definition + + ⊢ (∀a f f1. tree_CASE (TLeaf a) f f1 = f a) ∧ + ∀a f f1. tree_CASE (TNode a) f f1 = f1 a + + [tree_size_def] Definition + + ⊢ (∀f a. tree_size f (TLeaf a) = 1 + f a) ∧ + (∀f a. tree_size f (TNode a) = 1 + node_size f a) ∧ + (∀f a. node_size f (Node a) = 1 + tree1_size f a) ∧ + (∀f. tree1_size f [] = 0) ∧ + ∀f a0 a1. + tree1_size f (a0::a1) = 1 + (tree_size f a0 + tree1_size f a1) + + [btree_11] Theorem + + ⊢ (∀a a'. BLeaf a = BLeaf a' ⇔ a = a') ∧ + ∀a0 a1 a0' a1'. BNode a0 a1 = BNode a0' a1' ⇔ a0 = a0' ∧ a1 = a1' + + [btree_Axiom] Theorem + + ⊢ ∀f0 f1. ∃fn. + (∀a. fn (BLeaf a) = f0 a) ∧ + ∀a0 a1. fn (BNode a0 a1) = f1 a0 a1 (fn a0) (fn a1) + + [btree_case_cong] Theorem + + ⊢ ∀M M' f f1. + M = M' ∧ (∀a. M' = BLeaf a ⇒ f a = f' a) ∧ + (∀a0 a1. M' = BNode a0 a1 ⇒ f1 a0 a1 = f1' a0 a1) ⇒ + btree_CASE M f f1 = btree_CASE M' f' f1' + + [btree_case_eq] Theorem + + ⊢ btree_CASE x f f1 = v ⇔ + (∃a. x = BLeaf a ∧ f a = v) ∨ ∃b b0. x = BNode b b0 ∧ f1 b b0 = v + + [btree_distinct] Theorem + + ⊢ ∀a1 a0 a. BLeaf a ≠ BNode a0 a1 + + [btree_height_def] Theorem + + ⊢ ∀tree. + btree_height tree = + case tree of + BLeaf v => Return 1 + | BNode l r => + do + hl <- btree_height l; + hr <- btree_height r; + Return (hl + hr) + od + + [btree_induction] Theorem + + ⊢ ∀P. (∀a. P (BLeaf a)) ∧ (∀b b0. P b ∧ P b0 ⇒ P (BNode b b0)) ⇒ + ∀b. P b + + [btree_nchotomy] Theorem + + ⊢ ∀bb. (∃a. bb = BLeaf a) ∨ ∃b b0. bb = BNode b b0 + + [datatype_btree] Theorem + + ⊢ DATATYPE (btree BLeaf BNode) + + [datatype_list_t] Theorem + + ⊢ DATATYPE (list_t ListCons ListNil) + + [datatype_tree] Theorem + + ⊢ DATATYPE (tree TLeaf TNode ∧ node Node) + + [even_def] Theorem + + ⊢ ∀i. even i = if i = 0 then Return T else odd (i − 1) + + [list_t_11] Theorem + + ⊢ ∀a0 a1 a0' a1'. + ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1' + + [list_t_Axiom] Theorem + + ⊢ ∀f0 f1. ∃fn. + (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧ + fn ListNil = f1 + + [list_t_case_cong] Theorem + + ⊢ ∀M M' f v. + M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧ + (M' = ListNil ⇒ v = v') ⇒ + list_t_CASE M f v = list_t_CASE M' f' v' + + [list_t_case_eq] Theorem + + ⊢ list_t_CASE x f v = v' ⇔ + (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v' + + [list_t_distinct] Theorem + + ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil + + [list_t_induction] Theorem + + ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l + + [list_t_nchotomy] Theorem + + ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil + + [node_11] Theorem + + ⊢ ∀a a'. Node a = Node a' ⇔ a = a' + + [node_Axiom] Theorem + + ⊢ ∀f0 f1 f2 f3 f4. ∃fn0 fn1 fn2. + (∀a. fn0 (TLeaf a) = f0 a) ∧ (∀a. fn0 (TNode a) = f1 a (fn1 a)) ∧ + (∀a. fn1 (Node a) = f2 a (fn2 a)) ∧ fn2 [] = f3 ∧ + ∀a0 a1. fn2 (a0::a1) = f4 a0 a1 (fn0 a0) (fn2 a1) + + [node_case_cong] Theorem + + ⊢ ∀M M' f. + M = M' ∧ (∀a. M' = Node a ⇒ f a = f' a) ⇒ + node_CASE M f = node_CASE M' f' + + [node_case_eq] Theorem + + ⊢ node_CASE x f = v ⇔ ∃l. x = Node l ∧ f l = v + + [node_induction] Theorem + + ⊢ ∀P0 P1 P2. + (∀a. P0 (TLeaf a)) ∧ (∀n. P1 n ⇒ P0 (TNode n)) ∧ + (∀l. P2 l ⇒ P1 (Node l)) ∧ P2 [] ∧ + (∀t l. P0 t ∧ P2 l ⇒ P2 (t::l)) ⇒ + (∀t. P0 t) ∧ (∀n. P1 n) ∧ ∀l. P2 l + + [node_nchotomy] Theorem + + ⊢ ∀nn. ∃l. nn = Node l + + [nth_def] Theorem + + ⊢ ∀ls i. + nth ls i = + case ls of + ListCons x tl => + if u32_to_int i = 0 then Return x + else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od + | ListNil => Fail Failure + + [odd_def] Theorem + + ⊢ ∀i. odd i = if i = 0 then Return F else even (i − 1) + + [tree_11] Theorem + + ⊢ (∀a a'. TLeaf a = TLeaf a' ⇔ a = a') ∧ + ∀a a'. TNode a = TNode a' ⇔ a = a' + + [tree_Axiom] Theorem + + ⊢ ∀f0 f1 f2 f3 f4. ∃fn0 fn1 fn2. + (∀a. fn0 (TLeaf a) = f0 a) ∧ (∀a. fn0 (TNode a) = f1 a (fn1 a)) ∧ + (∀a. fn1 (Node a) = f2 a (fn2 a)) ∧ fn2 [] = f3 ∧ + ∀a0 a1. fn2 (a0::a1) = f4 a0 a1 (fn0 a0) (fn2 a1) + + [tree_case_cong] Theorem + + ⊢ ∀M M' f f1. + M = M' ∧ (∀a. M' = TLeaf a ⇒ f a = f' a) ∧ + (∀a. M' = TNode a ⇒ f1 a = f1' a) ⇒ + tree_CASE M f f1 = tree_CASE M' f' f1' + + [tree_case_eq] Theorem + + ⊢ tree_CASE x f f1 = v ⇔ + (∃a. x = TLeaf a ∧ f a = v) ∨ ∃n. x = TNode n ∧ f1 n = v + + [tree_distinct] Theorem + + ⊢ ∀a' a. TLeaf a ≠ TNode a' + + [tree_height_def] Theorem + + ⊢ ∀tree. + tree_height tree = + case tree of + TLeaf v => Return 1 + | TNode (Node ls) => tree_nodes_height ls + + [tree_induction] Theorem + + ⊢ ∀P0 P1 P2. + (∀a. P0 (TLeaf a)) ∧ (∀n. P1 n ⇒ P0 (TNode n)) ∧ + (∀l. P2 l ⇒ P1 (Node l)) ∧ P2 [] ∧ + (∀t l. P0 t ∧ P2 l ⇒ P2 (t::l)) ⇒ + (∀t. P0 t) ∧ (∀n. P1 n) ∧ ∀l. P2 l + + [tree_nchotomy] Theorem + + ⊢ ∀tt. (∃a. tt = TLeaf a) ∨ ∃n. tt = TNode n + + [tree_nodes_height_def] Theorem + + ⊢ ∀ls. + tree_nodes_height ls = + case ls of + [] => Return 0 + | t::tl => + do + h1 <- tree_height t; + h2 <- tree_nodes_height tl; + Return (h1 + h2) + od + + [tree_size_eq] Theorem + + ⊢ tree1_size f = list_size (tree_size f) + + +*) +end |