src/HOL/Metis_Examples/Binary_Tree.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45705 a25ff4283352
child 49962 a8cc904a6820
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42103
diff changeset
     1
(*  Title:      HOL/Metis_Examples/Binary_Tree.thy
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42103
diff changeset
     2
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
36487
50fd056cc3ce insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents: 36484
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     4
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42103
diff changeset
     5
Metis example featuring binary trees.
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     6
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     7
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42103
diff changeset
     8
header {* Metis Example Featuring Binary Trees *}
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     9
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42103
diff changeset
    10
theory Binary_Tree
27104
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 26312
diff changeset
    11
imports Main
791607529f6d rep_datatype command now takes list of constructors as input arguments
haftmann
parents: 26312
diff changeset
    12
begin
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    13
42103
6066a35f6678 Metis examples use the new Skolemizer to test it
blanchet
parents: 41144
diff changeset
    14
declare [[metis_new_skolemizer]]
6066a35f6678 Metis examples use the new Skolemizer to test it
blanchet
parents: 41144
diff changeset
    15
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    16
datatype 'a bt =
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    17
    Lf
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    18
  | Br 'a  "'a bt"  "'a bt"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    19
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    20
primrec n_nodes :: "'a bt => nat" where
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    21
  "n_nodes Lf = 0"
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    22
| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    23
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    24
primrec n_leaves :: "'a bt => nat" where
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    25
  "n_leaves Lf = Suc 0"
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    26
| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    27
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    28
primrec depth :: "'a bt => nat" where
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    29
  "depth Lf = 0"
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    30
| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    31
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    32
primrec reflect :: "'a bt => 'a bt" where
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    33
  "reflect Lf = Lf"
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    34
| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    35
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    36
primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    37
  "bt_map f Lf = Lf"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    38
| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    39
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    40
primrec preorder :: "'a bt => 'a list" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    41
  "preorder Lf = []"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    42
| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    43
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    44
primrec inorder :: "'a bt => 'a list" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    45
  "inorder Lf = []"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    46
| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    47
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    48
primrec postorder :: "'a bt => 'a list" where
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    49
  "postorder Lf = []"
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    50
| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    51
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    52
primrec append :: "'a bt => 'a bt => 'a bt" where
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    53
  "append Lf t = t"
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
    54
| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    55
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    56
text {* \medskip BT simplification *}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    57
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    58
lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    59
proof (induct t)
36487
50fd056cc3ce insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents: 36484
diff changeset
    60
  case Lf thus ?case
50fd056cc3ce insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents: 36484
diff changeset
    61
  proof -
50fd056cc3ce insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents: 36484
diff changeset
    62
    let "?p\<^isub>1 x\<^isub>1" = "x\<^isub>1 \<noteq> n_leaves (reflect (Lf::'a bt))"
50fd056cc3ce insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents: 36484
diff changeset
    63
    have "\<not> ?p\<^isub>1 (Suc 0)" by (metis reflect.simps(1) n_leaves.simps(1))
50fd056cc3ce insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents: 36484
diff changeset
    64
    hence "\<not> ?p\<^isub>1 (n_leaves (Lf::'a bt))" by (metis n_leaves.simps(1))
50fd056cc3ce insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents: 36484
diff changeset
    65
    thus "n_leaves (reflect (Lf::'a bt)) = n_leaves (Lf::'a bt)" by metis
50fd056cc3ce insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents: 36484
diff changeset
    66
  qed
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    67
next
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    68
  case (Br a t1 t2) thus ?case
36487
50fd056cc3ce insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents: 36484
diff changeset
    69
    by (metis n_leaves.simps(2) nat_add_commute reflect.simps(2))
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    70
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    71
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    72
lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    73
proof (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    74
  case Lf thus ?case by (metis reflect.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    75
next
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    76
  case (Br a t1 t2) thus ?case
36844
5f9385ecc1a7 Removed usage of normalizating locales.
hoelzl
parents: 36725
diff changeset
    77
    by (metis add_commute n_nodes.simps(2) reflect.simps(2))
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    78
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    79
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    80
lemma depth_reflect: "depth (reflect t) = depth t"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    81
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    82
 apply (metis depth.simps(1) reflect.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    83
by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2))
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    84
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    85
text {*
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    86
The famous relationship between the numbers of leaves and nodes.
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    87
*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    88
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    89
lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    90
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    91
 apply (metis n_leaves.simps(1) n_nodes.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    92
by auto
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    93
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    94
lemma reflect_reflect_ident: "reflect (reflect t) = t"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    95
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    96
 apply (metis reflect.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    97
proof -
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    98
  fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
    99
  assume A1: "reflect (reflect t1) = t1"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   100
  assume A2: "reflect (reflect t2) = t2"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   101
  have "\<And>V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   102
    using A1 by (metis reflect.simps(2))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   103
  hence "\<And>V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   104
    by (metis reflect.simps(2))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   105
  hence "\<And>U. reflect (reflect (Br U t1 t2)) = Br U t1 t2"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   106
    using A2 by metis
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   107
  thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   108
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   109
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   110
lemma bt_map_ident: "bt_map (%x. x) = (%y. y)"
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42103
diff changeset
   111
apply (rule ext)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   112
apply (induct_tac y)
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   113
 apply (metis bt_map.simps(1))
36571
16ec4fe058cb minor improvements
blanchet
parents: 36487
diff changeset
   114
by (metis bt_map.simps(2))
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   115
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   116
lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   117
apply (induct t)
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   118
 apply (metis append.simps(1) bt_map.simps(1))
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   119
by (metis append.simps(2) bt_map.simps(2))
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   120
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   121
lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   122
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   123
 apply (metis bt_map.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   124
by (metis bt_map.simps(2) o_eq_dest_lhs)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   125
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   126
lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   127
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   128
 apply (metis bt_map.simps(1) reflect.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   129
by (metis bt_map.simps(2) reflect.simps(2))
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   130
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   131
lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   132
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   133
 apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   134
by simp
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   135
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   136
lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   137
proof (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   138
  case Lf thus ?case
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   139
  proof -
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   140
    have "map f [] = []" by (metis map.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   141
    hence "map f [] = inorder Lf" by (metis inorder.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   142
    hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   143
    thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   144
  qed
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   145
next
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   146
  case (Br a t1 t2) thus ?case by simp
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   147
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   148
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   149
lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   150
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   151
 apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   152
by simp
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   153
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   154
lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   155
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   156
 apply (metis bt_map.simps(1) depth.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   157
by simp
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   158
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   159
lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   160
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   161
 apply (metis bt_map.simps(1) n_leaves.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   162
proof -
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   163
  fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   164
  assume A1: "n_leaves (bt_map f t1) = n_leaves t1"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   165
  assume A2: "n_leaves (bt_map f t2) = n_leaves t2"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   166
  have "\<And>V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   167
    using A1 by (metis n_leaves.simps(2))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   168
  hence "\<And>V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   169
    by (metis bt_map.simps(2))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   170
  hence F1: "\<And>U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   171
    using A2 by metis
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   172
  have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   173
    by (metis n_leaves.simps(2))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   174
  thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)"
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   175
    using F1 by metis
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   176
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   177
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   178
lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   179
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   180
 apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   181
              reflect.simps(1))
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   182
apply simp
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   183
done
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   184
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   185
lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   186
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   187
 apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   188
by simp
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   189
(* Slow:
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   190
by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   191
          reflect.simps(2) rev.simps(2) rev_append)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   192
*)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   193
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   194
lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   195
apply (induct t)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   196
 apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   197
              reflect.simps(1))
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   198
by (metis preorder_reflect reflect_reflect_ident rev_swap)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   199
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   200
text {*
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   201
Analogues of the standard properties of the append function for lists.
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   202
*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   203
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   204
lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   205
apply (induct t1)
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   206
 apply (metis append.simps(1))
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   207
by (metis append.simps(2))
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   208
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   209
lemma append_Lf2 [simp]: "append t Lf = t"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   210
apply (induct t)
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   211
 apply (metis append.simps(1))
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   212
by (metis append.simps(2))
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   213
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   214
declare max_add_distrib_left [simp]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   215
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   216
lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   217
apply (induct t1)
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   218
 apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1))
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   219
by simp
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   220
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   221
lemma n_leaves_append [simp]:
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   222
     "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   223
apply (induct t1)
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   224
 apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
45502
6246bef495ff avoid theorem references like 'semiring_norm(111)'
huffman
parents: 43197
diff changeset
   225
              Suc_eq_plus1)
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   226
by (simp add: left_distrib)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   227
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   228
lemma (*bt_map_append:*)
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   229
     "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
36484
134ac130a8ed redid the proofs with the latest Sledgehammer;
blanchet
parents: 33027
diff changeset
   230
apply (induct t1)
39246
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   231
 apply (metis append.simps(1) bt_map.simps(1))
9e58f0499f57 modernized primrec
haftmann
parents: 38991
diff changeset
   232
by (metis bt_map_append)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   233
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   234
end