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