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