Attic/MyTree.thy
author Chengsong
Wed, 23 Aug 2023 03:02:31 +0100
changeset 668 3831621d7b14
parent 95 a33d3040bf7e
permissions -rw-r--r--
added technical Overview section, almost done introduction
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset
     1
theory MyTree
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset
     2
imports Main
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset
     3
begin
29
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
     4
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
     5
datatype 
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
     6
  'a tree = Tip | 
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
     7
  Node " 'a tree" 'a " 'a tree"
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
     8
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
     9
fun mirror :: " 'a tree \<Rightarrow> 'a tree" where
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    10
  "mirror Tip = Tip" |
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    11
  "mirror (Node l a r) = Node (mirror r) a (mirror l)"
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    12
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    13
lemma "mirror(mirror t) = t"
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    14
  apply(induction t)
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    15
  apply(auto)
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    16
  done
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    17
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    18
datatype 'a option = None | Some 'a
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    19
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    20
fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    21
  "lookup [] x = None" |
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    22
  "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    23
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    24
definition sq :: "nat \<Rightarrow> nat" where
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    25
  "sq n = n * n"
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    26
 
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    27
abbreviation sq' :: "nat \<Rightarrow> nat" where
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    28
  "sq' n \<equiv> n * n"
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    29
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    30
fun div2 :: "nat \<Rightarrow> nat" where
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    31
  "div2 0 = 0" |
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    32
  "div2 (Suc 0) = 0" |
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    33
  "div2 (Suc(Suc n)) = Suc(div2 n)"
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    34
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    35
lemma "div2(n) = n div 2"
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    36
apply(induction n rule: div2.induct)
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    37
apply(auto)
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    38
done
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    39
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    40
value "div2 8"
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    41
2345ba5b4264 Proof Automation
fahadausaf <fahad.ausaf@icloud.com>
parents: 28
diff changeset
    42