src/HOL/Statespace/DistinctTreeProver.thy
author wenzelm
Sun Nov 06 16:29:22 2011 +0100 (2011-11-06)
changeset 45358 4849133d7a78
parent 45355 c0704e988526
child 48891 c0eafbd55de3
permissions -rw-r--r--
tuned document;
tuned proofs;
wenzelm@29269
     1
(*  Title:      HOL/Statespace/DistinctTreeProver.thy
schirmer@25171
     2
    Author:     Norbert Schirmer, TU Muenchen
schirmer@25171
     3
*)
schirmer@25171
     4
schirmer@25171
     5
header {* Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}*}
schirmer@25171
     6
schirmer@25171
     7
theory DistinctTreeProver 
schirmer@25171
     8
imports Main
wenzelm@25174
     9
uses ("distinct_tree_prover.ML")
schirmer@25171
    10
begin
schirmer@25171
    11
schirmer@25171
    12
text {* A state space manages a set of (abstract) names and assumes
schirmer@25171
    13
that the names are distinct. The names are stored as parameters of a
schirmer@25171
    14
locale and distinctness as an assumption. The most common request is
schirmer@25171
    15
to proof distinctness of two given names. We maintain the names in a
schirmer@25171
    16
balanced binary tree and formulate a predicate that all nodes in the
schirmer@25171
    17
tree have distinct names. This setup leads to logarithmic certificates.
schirmer@25171
    18
*}
schirmer@25171
    19
schirmer@25171
    20
subsection {* The Binary Tree *}
schirmer@25171
    21
schirmer@25171
    22
datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
schirmer@25171
    23
schirmer@25171
    24
schirmer@25171
    25
text {* The boolean flag in the node marks the content of the node as
schirmer@25171
    26
deleted, without having to build a new tree. We prefer the boolean
schirmer@25171
    27
flag to an option type, so that the ML-layer can still use the node
schirmer@25171
    28
content to facilitate binary search in the tree. The ML code keeps the
schirmer@25171
    29
nodes sorted using the term order. We do not have to push ordering to
schirmer@25171
    30
the HOL level. *}
schirmer@25171
    31
schirmer@25171
    32
subsection {* Distinctness of Nodes *}
schirmer@25171
    33
schirmer@25171
    34
wenzelm@38838
    35
primrec set_of :: "'a tree \<Rightarrow> 'a set"
wenzelm@38838
    36
where
wenzelm@38838
    37
  "set_of Tip = {}"
wenzelm@38838
    38
| "set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"
schirmer@25171
    39
wenzelm@38838
    40
primrec all_distinct :: "'a tree \<Rightarrow> bool"
wenzelm@38838
    41
where
wenzelm@38838
    42
  "all_distinct Tip = True"
wenzelm@38838
    43
| "all_distinct (Node l x d r) =
wenzelm@38838
    44
    ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> 
wenzelm@38838
    45
      set_of l \<inter> set_of r = {} \<and>
wenzelm@38838
    46
      all_distinct l \<and> all_distinct r)"
schirmer@25171
    47
schirmer@25171
    48
text {* Given a binary tree @{term "t"} for which 
schirmer@25171
    49
@{const all_distinct} holds, given two different nodes contained in the tree,
schirmer@25171
    50
we want to write a ML function that generates a logarithmic
schirmer@25171
    51
certificate that the content of the nodes is distinct. We use the
schirmer@25171
    52
following lemmas to achieve this.  *} 
schirmer@25171
    53
wenzelm@45355
    54
lemma all_distinct_left: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct l"
schirmer@25171
    55
  by simp
schirmer@25171
    56
schirmer@25171
    57
lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r"
schirmer@25171
    58
  by simp
schirmer@25171
    59
wenzelm@45358
    60
lemma distinct_left: "all_distinct (Node l x False r) \<Longrightarrow> y \<in> set_of l \<Longrightarrow> x \<noteq> y"
schirmer@25171
    61
  by auto
schirmer@25171
    62
wenzelm@45358
    63
lemma distinct_right: "all_distinct (Node l x False r) \<Longrightarrow> y \<in> set_of r \<Longrightarrow> x \<noteq> y"
schirmer@25171
    64
  by auto
schirmer@25171
    65
wenzelm@45358
    66
lemma distinct_left_right:
wenzelm@45358
    67
    "all_distinct (Node l z b r) \<Longrightarrow> x \<in> set_of l \<Longrightarrow> y \<in> set_of r \<Longrightarrow> x \<noteq> y"
schirmer@25171
    68
  by auto
schirmer@25171
    69
schirmer@25171
    70
lemma in_set_root: "x \<in> set_of (Node l x False r)"
schirmer@25171
    71
  by simp
schirmer@25171
    72
schirmer@25171
    73
lemma in_set_left: "y \<in> set_of l \<Longrightarrow>  y \<in> set_of (Node l x False r)"
schirmer@25171
    74
  by simp
schirmer@25171
    75
schirmer@25171
    76
lemma in_set_right: "y \<in> set_of r \<Longrightarrow>  y \<in> set_of (Node l x False r)"
schirmer@25171
    77
  by simp
schirmer@25171
    78
schirmer@25171
    79
lemma swap_neq: "x \<noteq> y \<Longrightarrow> y \<noteq> x"
schirmer@25171
    80
  by blast
schirmer@25171
    81
schirmer@25171
    82
lemma neq_to_eq_False: "x\<noteq>y \<Longrightarrow> (x=y)\<equiv>False"
schirmer@25171
    83
  by simp
schirmer@25171
    84
schirmer@25171
    85
subsection {* Containment of Trees *}
schirmer@25171
    86
schirmer@25171
    87
text {* When deriving a state space from other ones, we create a new
schirmer@25171
    88
name tree which contains all the names of the parent state spaces and
wenzelm@45358
    89
assume the predicate @{const all_distinct}. We then prove that the new
wenzelm@45358
    90
locale interprets all parent locales. Hence we have to show that the
wenzelm@45358
    91
new distinctness assumption on all names implies the distinctness
schirmer@25171
    92
assumptions of the parent locales. This proof is implemented in ML. We
schirmer@25171
    93
do this efficiently by defining a kind of containment check of trees
wenzelm@45358
    94
by ``subtraction''.  We subtract the parent tree from the new tree. If
wenzelm@45358
    95
this succeeds we know that @{const all_distinct} of the new tree
wenzelm@45358
    96
implies @{const all_distinct} of the parent tree.  The resulting
wenzelm@45358
    97
certificate is of the order @{term "n * log(m)"} where @{term "n"} is
wenzelm@45358
    98
the size of the (smaller) parent tree and @{term "m"} the size of the
wenzelm@45358
    99
(bigger) new tree.  *}
schirmer@25171
   100
schirmer@25171
   101
wenzelm@38838
   102
primrec delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
wenzelm@38838
   103
where
wenzelm@38838
   104
  "delete x Tip = None"
wenzelm@38838
   105
| "delete x (Node l y d r) = (case delete x l of
wenzelm@38838
   106
                                Some l' \<Rightarrow>
wenzelm@38838
   107
                                 (case delete x r of 
wenzelm@38838
   108
                                    Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')
wenzelm@38838
   109
                                  | None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))
wenzelm@38838
   110
                               | None \<Rightarrow>
wenzelm@45358
   111
                                  (case delete x r of 
wenzelm@38838
   112
                                     Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')
wenzelm@38838
   113
                                   | None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)
wenzelm@38838
   114
                                             else None))"
schirmer@25171
   115
schirmer@25171
   116
wenzelm@45358
   117
lemma delete_Some_set_of: "delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t"
wenzelm@45358
   118
proof (induct t arbitrary: t')
schirmer@25171
   119
  case Tip thus ?case by simp
schirmer@25171
   120
next
schirmer@25171
   121
  case (Node l y d r)
wenzelm@25364
   122
  have del: "delete x (Node l y d r) = Some t'" by fact
schirmer@25171
   123
  show ?case
schirmer@25171
   124
  proof (cases "delete x l")
schirmer@25171
   125
    case (Some l')
schirmer@25171
   126
    note x_l_Some = this
schirmer@25171
   127
    with Node.hyps
schirmer@25171
   128
    have l'_l: "set_of l' \<subseteq> set_of l"
schirmer@25171
   129
      by simp
schirmer@25171
   130
    show ?thesis
schirmer@25171
   131
    proof (cases "delete x r")
schirmer@25171
   132
      case (Some r')
schirmer@25171
   133
      with Node.hyps
schirmer@25171
   134
      have "set_of r' \<subseteq> set_of r"
wenzelm@32960
   135
        by simp
schirmer@25171
   136
      with l'_l Some x_l_Some del
schirmer@25171
   137
      show ?thesis
wenzelm@32960
   138
        by (auto split: split_if_asm)
schirmer@25171
   139
    next
schirmer@25171
   140
      case None
schirmer@25171
   141
      with l'_l Some x_l_Some del
schirmer@25171
   142
      show ?thesis
nipkow@44890
   143
        by (fastforce split: split_if_asm)
schirmer@25171
   144
    qed
schirmer@25171
   145
  next
schirmer@25171
   146
    case None
schirmer@25171
   147
    note x_l_None = this
schirmer@25171
   148
    show ?thesis
schirmer@25171
   149
    proof (cases "delete x r")
schirmer@25171
   150
      case (Some r')
schirmer@25171
   151
      with Node.hyps
schirmer@25171
   152
      have "set_of r' \<subseteq> set_of r"
wenzelm@32960
   153
        by simp
schirmer@25171
   154
      with Some x_l_None del
schirmer@25171
   155
      show ?thesis
nipkow@44890
   156
        by (fastforce split: split_if_asm)
schirmer@25171
   157
    next
schirmer@25171
   158
      case None
schirmer@25171
   159
      with x_l_None del
schirmer@25171
   160
      show ?thesis
nipkow@44890
   161
        by (fastforce split: split_if_asm)
schirmer@25171
   162
    qed
schirmer@25171
   163
  qed
schirmer@25171
   164
qed
schirmer@25171
   165
wenzelm@45355
   166
lemma delete_Some_all_distinct:
wenzelm@45358
   167
  "delete x t = Some t' \<Longrightarrow> all_distinct t \<Longrightarrow> all_distinct t'"
wenzelm@45358
   168
proof (induct t arbitrary: t')
schirmer@25171
   169
  case Tip thus ?case by simp
schirmer@25171
   170
next
schirmer@25171
   171
  case (Node l y d r)
wenzelm@25364
   172
  have del: "delete x (Node l y d r) = Some t'" by fact
wenzelm@25364
   173
  have "all_distinct (Node l y d r)" by fact
schirmer@25171
   174
  then obtain
schirmer@25171
   175
    dist_l: "all_distinct l" and
schirmer@25171
   176
    dist_r: "all_distinct r" and
schirmer@25171
   177
    d: "d \<or> (y \<notin> set_of l \<and> y \<notin> set_of r)" and
schirmer@25171
   178
    dist_l_r: "set_of l \<inter> set_of r = {}"
schirmer@25171
   179
    by auto
schirmer@25171
   180
  show ?case
schirmer@25171
   181
  proof (cases "delete x l")
schirmer@25171
   182
    case (Some l')
schirmer@25171
   183
    note x_l_Some = this
schirmer@25171
   184
    from Node.hyps (1) [OF Some dist_l]
schirmer@25171
   185
    have dist_l': "all_distinct l'"
schirmer@25171
   186
      by simp
schirmer@25171
   187
    from delete_Some_set_of [OF x_l_Some]
schirmer@25171
   188
    have l'_l: "set_of l' \<subseteq> set_of l".
schirmer@25171
   189
    show ?thesis
schirmer@25171
   190
    proof (cases "delete x r")
schirmer@25171
   191
      case (Some r')
schirmer@25171
   192
      from Node.hyps (2) [OF Some dist_r]
schirmer@25171
   193
      have dist_r': "all_distinct r'"
wenzelm@32960
   194
        by simp
schirmer@25171
   195
      from delete_Some_set_of [OF Some]
schirmer@25171
   196
      have "set_of r' \<subseteq> set_of r".
schirmer@25171
   197
      
schirmer@25171
   198
      with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r
schirmer@25171
   199
      show ?thesis
nipkow@44890
   200
        by fastforce
schirmer@25171
   201
    next
schirmer@25171
   202
      case None
schirmer@25171
   203
      with l'_l dist_l'  x_l_Some del d dist_l_r dist_r
schirmer@25171
   204
      show ?thesis
nipkow@44890
   205
        by fastforce
schirmer@25171
   206
    qed
schirmer@25171
   207
  next
schirmer@25171
   208
    case None
schirmer@25171
   209
    note x_l_None = this
schirmer@25171
   210
    show ?thesis
schirmer@25171
   211
    proof (cases "delete x r")
schirmer@25171
   212
      case (Some r')
schirmer@25171
   213
      with Node.hyps (2) [OF Some dist_r]
schirmer@25171
   214
      have dist_r': "all_distinct r'"
wenzelm@32960
   215
        by simp
schirmer@25171
   216
      from delete_Some_set_of [OF Some]
schirmer@25171
   217
      have "set_of r' \<subseteq> set_of r".
schirmer@25171
   218
      with Some dist_r' x_l_None del dist_l d dist_l_r
schirmer@25171
   219
      show ?thesis
nipkow@44890
   220
        by fastforce
schirmer@25171
   221
    next
schirmer@25171
   222
      case None
schirmer@25171
   223
      with x_l_None del dist_l dist_r d dist_l_r
schirmer@25171
   224
      show ?thesis
nipkow@44890
   225
        by (fastforce split: split_if_asm)
schirmer@25171
   226
    qed
schirmer@25171
   227
  qed
schirmer@25171
   228
qed
schirmer@25171
   229
schirmer@25171
   230
lemma delete_None_set_of_conv: "delete x t = None = (x \<notin> set_of t)"
schirmer@25171
   231
proof (induct t)
schirmer@25171
   232
  case Tip thus ?case by simp
schirmer@25171
   233
next
schirmer@25171
   234
  case (Node l y d r)
schirmer@25171
   235
  thus ?case
schirmer@25171
   236
    by (auto split: option.splits)
schirmer@25171
   237
qed
schirmer@25171
   238
schirmer@25171
   239
lemma delete_Some_x_set_of:
wenzelm@45358
   240
  "delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> set_of t'"
wenzelm@45358
   241
proof (induct t arbitrary: t')
schirmer@25171
   242
  case Tip thus ?case by simp
schirmer@25171
   243
next
schirmer@25171
   244
  case (Node l y d r)
wenzelm@25364
   245
  have del: "delete x (Node l y d r) = Some t'" by fact
schirmer@25171
   246
  show ?case
schirmer@25171
   247
  proof (cases "delete x l")
schirmer@25171
   248
    case (Some l')
schirmer@25171
   249
    note x_l_Some = this
schirmer@25171
   250
    from Node.hyps (1) [OF Some]
schirmer@25171
   251
    obtain x_l: "x \<in> set_of l" "x \<notin> set_of l'"
schirmer@25171
   252
      by simp
schirmer@25171
   253
    show ?thesis
schirmer@25171
   254
    proof (cases "delete x r")
schirmer@25171
   255
      case (Some r')
schirmer@25171
   256
      from Node.hyps (2) [OF Some]
schirmer@25171
   257
      obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"
wenzelm@32960
   258
        by simp
schirmer@25171
   259
      from x_r x_l Some x_l_Some del 
schirmer@25171
   260
      show ?thesis
wenzelm@32960
   261
        by (clarsimp split: split_if_asm)
schirmer@25171
   262
    next
schirmer@25171
   263
      case None
schirmer@25171
   264
      then have "x \<notin> set_of r"
wenzelm@32960
   265
        by (simp add: delete_None_set_of_conv)
schirmer@25171
   266
      with x_l None x_l_Some del
schirmer@25171
   267
      show ?thesis
wenzelm@32960
   268
        by (clarsimp split: split_if_asm)
schirmer@25171
   269
    qed
schirmer@25171
   270
  next
schirmer@25171
   271
    case None
schirmer@25171
   272
    note x_l_None = this
schirmer@25171
   273
    then have x_notin_l: "x \<notin> set_of l"
schirmer@25171
   274
      by (simp add: delete_None_set_of_conv)
schirmer@25171
   275
    show ?thesis
schirmer@25171
   276
    proof (cases "delete x r")
schirmer@25171
   277
      case (Some r')
schirmer@25171
   278
      from Node.hyps (2) [OF Some]
schirmer@25171
   279
      obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"
wenzelm@32960
   280
        by simp
schirmer@25171
   281
      from x_r x_notin_l Some x_l_None del 
schirmer@25171
   282
      show ?thesis
wenzelm@32960
   283
        by (clarsimp split: split_if_asm)
schirmer@25171
   284
    next
schirmer@25171
   285
      case None
schirmer@25171
   286
      then have "x \<notin> set_of r"
wenzelm@32960
   287
        by (simp add: delete_None_set_of_conv)
schirmer@25171
   288
      with None x_l_None x_notin_l del
schirmer@25171
   289
      show ?thesis
wenzelm@32960
   290
        by (clarsimp split: split_if_asm)
schirmer@25171
   291
    qed
schirmer@25171
   292
  qed
schirmer@25171
   293
qed
schirmer@25171
   294
schirmer@25171
   295
wenzelm@38838
   296
primrec subtract :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
wenzelm@38838
   297
where
wenzelm@38838
   298
  "subtract Tip t = Some t"
wenzelm@38838
   299
| "subtract (Node l x b r) t =
wenzelm@38838
   300
     (case delete x t of
wenzelm@38838
   301
        Some t' \<Rightarrow> (case subtract l t' of 
wenzelm@38838
   302
                     Some t'' \<Rightarrow> subtract r t''
wenzelm@38838
   303
                    | None \<Rightarrow> None)
wenzelm@38838
   304
       | None \<Rightarrow> None)"
schirmer@25171
   305
schirmer@25171
   306
lemma subtract_Some_set_of_res: 
wenzelm@45358
   307
  "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t \<subseteq> set_of t\<^isub>2"
wenzelm@45358
   308
proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)
schirmer@25171
   309
  case Tip thus ?case by simp
schirmer@25171
   310
next
schirmer@25171
   311
  case (Node l x b r)
wenzelm@25364
   312
  have sub: "subtract (Node l x b r) t\<^isub>2 = Some t" by fact
schirmer@25171
   313
  show ?case
schirmer@25171
   314
  proof (cases "delete x t\<^isub>2")
schirmer@25171
   315
    case (Some t\<^isub>2')
schirmer@25171
   316
    note del_x_Some = this
schirmer@25171
   317
    from delete_Some_set_of [OF Some] 
schirmer@25171
   318
    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
schirmer@25171
   319
    show ?thesis
schirmer@25171
   320
    proof (cases "subtract l t\<^isub>2'")
schirmer@25171
   321
      case (Some t\<^isub>2'')
schirmer@25171
   322
      note sub_l_Some = this
schirmer@25171
   323
      from Node.hyps (1) [OF Some] 
schirmer@25171
   324
      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
schirmer@25171
   325
      show ?thesis
schirmer@25171
   326
      proof (cases "subtract r t\<^isub>2''")
wenzelm@32960
   327
        case (Some t\<^isub>2''')
wenzelm@32960
   328
        from Node.hyps (2) [OF Some ] 
wenzelm@32960
   329
        have "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''" .
wenzelm@32960
   330
        with Some sub_l_Some del_x_Some sub t2''_t2' t2'_t2
wenzelm@32960
   331
        show ?thesis
wenzelm@32960
   332
          by simp
schirmer@25171
   333
      next
wenzelm@32960
   334
        case None
wenzelm@32960
   335
        with del_x_Some sub_l_Some sub
wenzelm@32960
   336
        show ?thesis
wenzelm@32960
   337
          by simp
schirmer@25171
   338
      qed
schirmer@25171
   339
    next
schirmer@25171
   340
      case None
schirmer@25171
   341
      with del_x_Some sub 
schirmer@25171
   342
      show ?thesis
wenzelm@32960
   343
        by simp
schirmer@25171
   344
    qed
schirmer@25171
   345
  next
schirmer@25171
   346
    case None
schirmer@25171
   347
    with sub show ?thesis by simp
schirmer@25171
   348
  qed
schirmer@25171
   349
qed
schirmer@25171
   350
schirmer@25171
   351
lemma subtract_Some_set_of: 
wenzelm@45358
   352
  "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<subseteq> set_of t\<^isub>2"
wenzelm@45358
   353
proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)
schirmer@25171
   354
  case Tip thus ?case by simp
schirmer@25171
   355
next
schirmer@25171
   356
  case (Node l x d r)
wenzelm@25364
   357
  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
schirmer@25171
   358
  show ?case
schirmer@25171
   359
  proof (cases "delete x t\<^isub>2")
schirmer@25171
   360
    case (Some t\<^isub>2')
schirmer@25171
   361
    note del_x_Some = this
schirmer@25171
   362
    from delete_Some_set_of [OF Some] 
schirmer@25171
   363
    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
schirmer@25171
   364
    from delete_None_set_of_conv [of x t\<^isub>2] Some
schirmer@25171
   365
    have x_t2: "x \<in> set_of t\<^isub>2"
schirmer@25171
   366
      by simp
schirmer@25171
   367
    show ?thesis
schirmer@25171
   368
    proof (cases "subtract l t\<^isub>2'")
schirmer@25171
   369
      case (Some t\<^isub>2'')
schirmer@25171
   370
      note sub_l_Some = this
schirmer@25171
   371
      from Node.hyps (1) [OF Some] 
schirmer@25171
   372
      have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" .
schirmer@25171
   373
      from subtract_Some_set_of_res [OF Some]
schirmer@25171
   374
      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
schirmer@25171
   375
      show ?thesis
schirmer@25171
   376
      proof (cases "subtract r t\<^isub>2''")
wenzelm@32960
   377
        case (Some t\<^isub>2''')
wenzelm@32960
   378
        from Node.hyps (2) [OF Some ] 
wenzelm@32960
   379
        have r_t\<^isub>2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
wenzelm@32960
   380
        from Some sub_l_Some del_x_Some sub r_t\<^isub>2'' l_t2' t2'_t2 t2''_t2' x_t2
wenzelm@32960
   381
        show ?thesis
wenzelm@32960
   382
          by auto
schirmer@25171
   383
      next
wenzelm@32960
   384
        case None
wenzelm@32960
   385
        with del_x_Some sub_l_Some sub
wenzelm@32960
   386
        show ?thesis
wenzelm@32960
   387
          by simp
schirmer@25171
   388
      qed
schirmer@25171
   389
    next
schirmer@25171
   390
      case None
schirmer@25171
   391
      with del_x_Some sub 
schirmer@25171
   392
      show ?thesis
wenzelm@32960
   393
        by simp
schirmer@25171
   394
    qed
schirmer@25171
   395
  next
schirmer@25171
   396
    case None
schirmer@25171
   397
    with sub show ?thesis by simp
schirmer@25171
   398
  qed
schirmer@25171
   399
qed
schirmer@25171
   400
schirmer@25171
   401
lemma subtract_Some_all_distinct_res: 
wenzelm@45358
   402
  "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> all_distinct t\<^isub>2 \<Longrightarrow> all_distinct t"
wenzelm@45358
   403
proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)
schirmer@25171
   404
  case Tip thus ?case by simp
schirmer@25171
   405
next
schirmer@25171
   406
  case (Node l x d r)
wenzelm@25364
   407
  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
wenzelm@25364
   408
  have dist_t2: "all_distinct t\<^isub>2" by fact
schirmer@25171
   409
  show ?case
schirmer@25171
   410
  proof (cases "delete x t\<^isub>2")
schirmer@25171
   411
    case (Some t\<^isub>2')
schirmer@25171
   412
    note del_x_Some = this
schirmer@25171
   413
    from delete_Some_all_distinct [OF Some dist_t2] 
schirmer@25171
   414
    have dist_t2': "all_distinct t\<^isub>2'" .
schirmer@25171
   415
    show ?thesis
schirmer@25171
   416
    proof (cases "subtract l t\<^isub>2'")
schirmer@25171
   417
      case (Some t\<^isub>2'')
schirmer@25171
   418
      note sub_l_Some = this
schirmer@25171
   419
      from Node.hyps (1) [OF Some dist_t2'] 
schirmer@25171
   420
      have dist_t2'': "all_distinct t\<^isub>2''" .
schirmer@25171
   421
      show ?thesis
schirmer@25171
   422
      proof (cases "subtract r t\<^isub>2''")
wenzelm@32960
   423
        case (Some t\<^isub>2''')
wenzelm@32960
   424
        from Node.hyps (2) [OF Some dist_t2''] 
wenzelm@32960
   425
        have dist_t2''': "all_distinct t\<^isub>2'''" .
wenzelm@32960
   426
        from Some sub_l_Some del_x_Some sub 
schirmer@25171
   427
             dist_t2'''
wenzelm@32960
   428
        show ?thesis
wenzelm@32960
   429
          by simp
schirmer@25171
   430
      next
wenzelm@32960
   431
        case None
wenzelm@32960
   432
        with del_x_Some sub_l_Some sub
wenzelm@32960
   433
        show ?thesis
wenzelm@32960
   434
          by simp
schirmer@25171
   435
      qed
schirmer@25171
   436
    next
schirmer@25171
   437
      case None
schirmer@25171
   438
      with del_x_Some sub 
schirmer@25171
   439
      show ?thesis
wenzelm@32960
   440
        by simp
schirmer@25171
   441
    qed
schirmer@25171
   442
  next
schirmer@25171
   443
    case None
schirmer@25171
   444
    with sub show ?thesis by simp
schirmer@25171
   445
  qed
schirmer@25171
   446
qed
schirmer@25171
   447
schirmer@25171
   448
schirmer@25171
   449
lemma subtract_Some_dist_res: 
wenzelm@45358
   450
  "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<inter> set_of t = {}"
wenzelm@45358
   451
proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)
schirmer@25171
   452
  case Tip thus ?case by simp
schirmer@25171
   453
next
schirmer@25171
   454
  case (Node l x d r)
wenzelm@29291
   455
  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
schirmer@25171
   456
  show ?case
schirmer@25171
   457
  proof (cases "delete x t\<^isub>2")
schirmer@25171
   458
    case (Some t\<^isub>2')
schirmer@25171
   459
    note del_x_Some = this
schirmer@25171
   460
    from delete_Some_x_set_of [OF Some]
schirmer@25171
   461
    obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'"
schirmer@25171
   462
      by simp
schirmer@25171
   463
    from delete_Some_set_of [OF Some]
schirmer@25171
   464
    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
schirmer@25171
   465
    show ?thesis
schirmer@25171
   466
    proof (cases "subtract l t\<^isub>2'")
schirmer@25171
   467
      case (Some t\<^isub>2'')
schirmer@25171
   468
      note sub_l_Some = this
schirmer@25171
   469
      from Node.hyps (1) [OF Some ] 
schirmer@25171
   470
      have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}".
schirmer@25171
   471
      from subtract_Some_set_of_res [OF Some]
schirmer@25171
   472
      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
schirmer@25171
   473
      show ?thesis
schirmer@25171
   474
      proof (cases "subtract r t\<^isub>2''")
wenzelm@32960
   475
        case (Some t\<^isub>2''')
wenzelm@32960
   476
        from Node.hyps (2) [OF Some] 
wenzelm@32960
   477
        have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}" .
wenzelm@32960
   478
        from subtract_Some_set_of_res [OF Some]
wenzelm@32960
   479
        have t2'''_t2'': "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''".
wenzelm@32960
   480
        
wenzelm@32960
   481
        from Some sub_l_Some del_x_Some sub t2'''_t2'' dist_l_t2'' dist_r_t2'''
schirmer@25171
   482
             t2''_t2' t2'_t2 x_not_t2'
wenzelm@32960
   483
        show ?thesis
wenzelm@32960
   484
          by auto
schirmer@25171
   485
      next
wenzelm@32960
   486
        case None
wenzelm@32960
   487
        with del_x_Some sub_l_Some sub
wenzelm@32960
   488
        show ?thesis
wenzelm@32960
   489
          by simp
schirmer@25171
   490
      qed
schirmer@25171
   491
    next
schirmer@25171
   492
      case None
schirmer@25171
   493
      with del_x_Some sub 
schirmer@25171
   494
      show ?thesis
wenzelm@32960
   495
        by simp
schirmer@25171
   496
    qed
schirmer@25171
   497
  next
schirmer@25171
   498
    case None
schirmer@25171
   499
    with sub show ?thesis by simp
schirmer@25171
   500
  qed
schirmer@25171
   501
qed
wenzelm@32960
   502
        
schirmer@25171
   503
lemma subtract_Some_all_distinct:
wenzelm@45358
   504
  "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> all_distinct t\<^isub>2 \<Longrightarrow> all_distinct t\<^isub>1"
wenzelm@45358
   505
proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)
schirmer@25171
   506
  case Tip thus ?case by simp
schirmer@25171
   507
next
schirmer@25171
   508
  case (Node l x d r)
wenzelm@25364
   509
  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
wenzelm@25364
   510
  have dist_t2: "all_distinct t\<^isub>2" by fact
schirmer@25171
   511
  show ?case
schirmer@25171
   512
  proof (cases "delete x t\<^isub>2")
schirmer@25171
   513
    case (Some t\<^isub>2')
schirmer@25171
   514
    note del_x_Some = this
schirmer@25171
   515
    from delete_Some_all_distinct [OF Some dist_t2 ] 
schirmer@25171
   516
    have dist_t2': "all_distinct t\<^isub>2'" .
schirmer@25171
   517
    from delete_Some_set_of [OF Some]
schirmer@25171
   518
    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
schirmer@25171
   519
    from delete_Some_x_set_of [OF Some]
schirmer@25171
   520
    obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'"
schirmer@25171
   521
      by simp
schirmer@25171
   522
schirmer@25171
   523
    show ?thesis
schirmer@25171
   524
    proof (cases "subtract l t\<^isub>2'")
schirmer@25171
   525
      case (Some t\<^isub>2'')
schirmer@25171
   526
      note sub_l_Some = this
schirmer@25171
   527
      from Node.hyps (1) [OF Some dist_t2' ] 
schirmer@25171
   528
      have dist_l: "all_distinct l" .
schirmer@25171
   529
      from subtract_Some_all_distinct_res [OF Some dist_t2'] 
schirmer@25171
   530
      have dist_t2'': "all_distinct t\<^isub>2''" .
schirmer@25171
   531
      from subtract_Some_set_of [OF Some]
schirmer@25171
   532
      have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" .
schirmer@25171
   533
      from subtract_Some_set_of_res [OF Some]
schirmer@25171
   534
      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
schirmer@25171
   535
      from subtract_Some_dist_res [OF Some]
schirmer@25171
   536
      have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}".
schirmer@25171
   537
      show ?thesis
schirmer@25171
   538
      proof (cases "subtract r t\<^isub>2''")
wenzelm@32960
   539
        case (Some t\<^isub>2''')
wenzelm@32960
   540
        from Node.hyps (2) [OF Some dist_t2''] 
wenzelm@32960
   541
        have dist_r: "all_distinct r" .
wenzelm@32960
   542
        from subtract_Some_set_of [OF Some]
wenzelm@32960
   543
        have r_t2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
wenzelm@32960
   544
        from subtract_Some_dist_res [OF Some]
wenzelm@32960
   545
        have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}".
schirmer@25171
   546
wenzelm@32960
   547
        from dist_l dist_r Some sub_l_Some del_x_Some r_t2'' l_t2' x_t2 x_not_t2' 
wenzelm@32960
   548
             t2''_t2' dist_l_t2'' dist_r_t2'''
wenzelm@32960
   549
        show ?thesis
wenzelm@32960
   550
          by auto
schirmer@25171
   551
      next
wenzelm@32960
   552
        case None
wenzelm@32960
   553
        with del_x_Some sub_l_Some sub
wenzelm@32960
   554
        show ?thesis
wenzelm@32960
   555
          by simp
schirmer@25171
   556
      qed
schirmer@25171
   557
    next
schirmer@25171
   558
      case None
schirmer@25171
   559
      with del_x_Some sub 
schirmer@25171
   560
      show ?thesis
wenzelm@32960
   561
        by simp
schirmer@25171
   562
    qed
schirmer@25171
   563
  next
schirmer@25171
   564
    case None
schirmer@25171
   565
    with sub show ?thesis by simp
schirmer@25171
   566
  qed
schirmer@25171
   567
qed
schirmer@25171
   568
schirmer@25171
   569
schirmer@25171
   570
lemma delete_left:
schirmer@25171
   571
  assumes dist: "all_distinct (Node l y d r)" 
schirmer@25171
   572
  assumes del_l: "delete x l = Some l'"
schirmer@25171
   573
  shows "delete x (Node l y d r) = Some (Node l' y d r)"
schirmer@25171
   574
proof -
schirmer@25171
   575
  from delete_Some_x_set_of [OF del_l]
schirmer@25171
   576
  obtain "x \<in> set_of l"
schirmer@25171
   577
    by simp
schirmer@25171
   578
  moreover with dist 
schirmer@25171
   579
  have "delete x r = None"
schirmer@25171
   580
    by (cases "delete x r") (auto dest:delete_Some_x_set_of)
schirmer@25171
   581
schirmer@25171
   582
  ultimately 
schirmer@25171
   583
  show ?thesis
schirmer@25171
   584
    using del_l dist
schirmer@25171
   585
    by (auto split: option.splits)
schirmer@25171
   586
qed
schirmer@25171
   587
schirmer@25171
   588
lemma delete_right:
schirmer@25171
   589
  assumes dist: "all_distinct (Node l y d r)" 
schirmer@25171
   590
  assumes del_r: "delete x r = Some r'"
schirmer@25171
   591
  shows "delete x (Node l y d r) = Some (Node l y d r')"
schirmer@25171
   592
proof -
schirmer@25171
   593
  from delete_Some_x_set_of [OF del_r]
schirmer@25171
   594
  obtain "x \<in> set_of r"
schirmer@25171
   595
    by simp
schirmer@25171
   596
  moreover with dist 
schirmer@25171
   597
  have "delete x l = None"
schirmer@25171
   598
    by (cases "delete x l") (auto dest:delete_Some_x_set_of)
schirmer@25171
   599
schirmer@25171
   600
  ultimately 
schirmer@25171
   601
  show ?thesis
schirmer@25171
   602
    using del_r dist
schirmer@25171
   603
    by (auto split: option.splits)
schirmer@25171
   604
qed
schirmer@25171
   605
schirmer@25171
   606
lemma delete_root: 
schirmer@25171
   607
  assumes dist: "all_distinct (Node l x False r)" 
schirmer@25171
   608
  shows "delete x (Node l x False r) = Some (Node l x True r)"
schirmer@25171
   609
proof -
schirmer@25171
   610
  from dist have "delete x r = None"
schirmer@25171
   611
    by (cases "delete x r") (auto dest:delete_Some_x_set_of)
schirmer@25171
   612
  moreover
schirmer@25171
   613
  from dist have "delete x l = None"
schirmer@25171
   614
    by (cases "delete x l") (auto dest:delete_Some_x_set_of)
schirmer@25171
   615
  ultimately show ?thesis
schirmer@25171
   616
    using dist
schirmer@25171
   617
       by (auto split: option.splits)
schirmer@25171
   618
qed               
schirmer@25171
   619
schirmer@25171
   620
lemma subtract_Node:
schirmer@25171
   621
 assumes del: "delete x t = Some t'"                                
schirmer@25171
   622
 assumes sub_l: "subtract l t' = Some t''"
schirmer@25171
   623
 assumes sub_r: "subtract r t'' = Some t'''"
schirmer@25171
   624
 shows "subtract (Node l x False r) t = Some t'''"
schirmer@25171
   625
using del sub_l sub_r
schirmer@25171
   626
by simp
schirmer@25171
   627
schirmer@25171
   628
lemma subtract_Tip: "subtract Tip t = Some t"
schirmer@25171
   629
  by simp
schirmer@25171
   630
 
schirmer@25171
   631
text {* Now we have all the theorems in place that are needed for the
schirmer@25171
   632
certificate generating ML functions. *}
schirmer@25171
   633
wenzelm@25174
   634
use "distinct_tree_prover.ML"
schirmer@25171
   635
schirmer@25171
   636
(* Uncomment for profiling or debugging *)
schirmer@25171
   637
(*
schirmer@25171
   638
ML {*
schirmer@25171
   639
(*
schirmer@25171
   640
val nums = (0 upto 10000);
schirmer@25171
   641
val nums' = (200 upto 3000);
schirmer@25171
   642
*)
schirmer@25171
   643
val nums = (0 upto 10000);
schirmer@25171
   644
val nums' = (0 upto 3000);
wenzelm@42287
   645
val const_decls = map (fn i => ("const" ^ string_of_int i, Type ("nat", []), NoSyn)) nums
schirmer@25171
   646
wenzelm@35408
   647
val consts = sort Term_Ord.fast_term_ord 
schirmer@25171
   648
              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
wenzelm@35408
   649
val consts' = sort Term_Ord.fast_term_ord 
schirmer@25171
   650
              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
schirmer@25171
   651
schirmer@25171
   652
val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts
schirmer@25171
   653
schirmer@25171
   654
schirmer@25171
   655
val t' = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts'
schirmer@25171
   656
schirmer@25171
   657
schirmer@25171
   658
val dist = 
schirmer@25171
   659
     HOLogic.Trueprop$
schirmer@25171
   660
       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t)
schirmer@25171
   661
schirmer@25171
   662
val dist' = 
schirmer@25171
   663
     HOLogic.Trueprop$
schirmer@25171
   664
       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t')
schirmer@25171
   665
wenzelm@32740
   666
val da = Unsynchronized.ref refl;
schirmer@25171
   667
schirmer@25171
   668
*}
schirmer@25171
   669
schirmer@25171
   670
setup {*
schirmer@25171
   671
Theory.add_consts_i const_decls
wenzelm@39557
   672
#> (fn thy  => let val ([thm],thy') = Global_Theory.add_axioms [(("dist_axiom",dist),[])] thy
schirmer@25171
   673
               in (da := thm; thy') end)
schirmer@25171
   674
*}
schirmer@25171
   675
schirmer@25171
   676
schirmer@25171
   677
ML {* 
wenzelm@32010
   678
 val ct' = cterm_of @{theory} t';
schirmer@25171
   679
*}
schirmer@25171
   680
schirmer@25171
   681
ML {*
schirmer@25171
   682
 timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);())) 
schirmer@25171
   683
*}
schirmer@25171
   684
schirmer@25171
   685
(* 590 s *)
schirmer@25171
   686
schirmer@25171
   687
ML {*
schirmer@25171
   688
schirmer@25171
   689
schirmer@25171
   690
val p1 = 
schirmer@25171
   691
 the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const1",Type ("nat",[]))) t)
schirmer@25171
   692
val p2 =
schirmer@25171
   693
 the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const10000",Type ("nat",[]))) t)
schirmer@25171
   694
*}
schirmer@25171
   695
schirmer@25171
   696
schirmer@25171
   697
ML {* timeit (fn () => DistinctTreeProver.distinctTreeProver (!da )
schirmer@25171
   698
       p1
schirmer@25171
   699
       p2)*}
schirmer@25171
   700
schirmer@25171
   701
schirmer@25171
   702
ML {* timeit (fn () => (DistinctTreeProver.deleteProver (!da) p1;())) *}
schirmer@25171
   703
schirmer@25171
   704
schirmer@25171
   705
schirmer@25171
   706
schirmer@25171
   707
ML {*
wenzelm@32010
   708
val cdist' = cterm_of @{theory} dist';
schirmer@25171
   709
DistinctTreeProver.distinct_implProver (!da) cdist';
schirmer@25171
   710
*}
schirmer@25171
   711
schirmer@25171
   712
*)
schirmer@25171
   713
schirmer@25171
   714
end