summaryrefslogtreecommitdiff
path: root/backends/hol4/ilistTheory.sig
blob: f155a3288560b017a116289efbb9e8de326eb3a8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
signature ilistTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val index_def : thm
    val len_def : thm
    val update_def : thm
  
  (*  Theorems  *)
    val append_len_eq : thm
    val index_eq : thm
    val index_eq_EL : thm
    val len_append : thm
    val len_eq_LENGTH : thm
    val len_pos : thm
    val update_eq : thm
  
  val ilist_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [primitivesArith] Parent theory of "ilist"
   
   [string] Parent theory of "ilist"
   
   [index_def]  Definition
      
      ⊢ ∀i x ls.
          index i (x::ls) =
          if i = 0 then x else if 0 < i then index (i − 1) ls else ARB
   
   [len_def]  Definition
      
      ⊢ len [] = 0 ∧ ∀x ls. len (x::ls) = 1 + len ls
   
   [update_def]  Definition
      
      ⊢ (∀i y. update [] i y = []) ∧
        ∀x ls i y.
          update (x::ls) i y =
          if i = 0 then y::ls
          else if 0 < i then x::update ls (i − 1) y
          else x::ls
   
   [append_len_eq]  Theorem
      
      ⊢ (∀l1 l2 l1' l2'.
           len l1 = len l1' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')) ∧
        ∀l1 l2 l1' l2'.
          len l2 = len l2' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')
   
   [index_eq]  Theorem
      
      ⊢ (∀x ls. index 0 (x::ls) = x) ∧
        ∀i x ls.
          index i (x::ls) =
          if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then index (i − 1) ls
          else if i = 0 then x
          else ARB
   
   [index_eq_EL]  Theorem
      
      ⊢ ∀i ls. 0 ≤ i ⇒ i < len ls ⇒ index i ls = EL (Num i) ls
   
   [len_append]  Theorem
      
      ⊢ ∀l1 l2. len (l1 ⧺ l2) = len l1 + len l2
   
   [len_eq_LENGTH]  Theorem
      
      ⊢ ∀ls. len ls = &LENGTH ls
   
   [len_pos]  Theorem
      
      ⊢ ∀ls. 0 ≤ len ls
   
   [update_eq]  Theorem
      
      ⊢ (∀i y. update [] i y = []) ∧
        (∀x ls y. update (x::ls) 0 y = y::ls) ∧
        ∀x ls i y.
          update (x::ls) i y =
          if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then x::update ls (i − 1) y
          else if i < 0 then x::ls
          else y::ls
   
   
*)
end