src/HOL/Statespace/DistinctTreeProver.thy
author wenzelm
Tue Sep 29 16:24:36 2009 +0200 (2009-09-29)
changeset 32740 9dd0a2f83429
parent 32010 cb1a1c94b4cd
child 32960 69916a850301
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
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
schirmer@25171
    35
consts set_of:: "'a tree \<Rightarrow> 'a set"
schirmer@25171
    36
primrec 
schirmer@25171
    37
"set_of Tip = {}"
schirmer@25171
    38
"set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"
schirmer@25171
    39
schirmer@25171
    40
consts all_distinct:: "'a tree \<Rightarrow> bool"
schirmer@25171
    41
primrec
schirmer@25171
    42
"all_distinct Tip = True"
schirmer@25171
    43
"all_distinct (Node l x d r) = ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> 
schirmer@25171
    44
                               set_of l \<inter> set_of r = {} \<and>
schirmer@25171
    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
schirmer@25171
    53
lemma all_distinct_left:
schirmer@25171
    54
"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
schirmer@25171
    60
lemma distinct_left: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of l \<rbrakk> \<Longrightarrow> x\<noteq>y"
schirmer@25171
    61
  by auto
schirmer@25171
    62
schirmer@25171
    63
lemma distinct_right: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of r \<rbrakk> \<Longrightarrow> x\<noteq>y"
schirmer@25171
    64
  by auto
schirmer@25171
    65
schirmer@25171
    66
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
    67
  \<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
schirmer@25171
    89
assumme the predicate @{const all_distinct}. We then prove that the new locale
schirmer@25171
    90
interprets all parent locales. Hence we have to show that the new
schirmer@25171
    91
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
schirmer@25171
    94
by 'subtraction'.  We subtract the parent tree from the new tree. If this
schirmer@25171
    95
succeeds we know that @{const all_distinct} of the new tree implies
schirmer@25171
    96
@{const all_distinct} of the parent tree.  The resulting certificate is
schirmer@25171
    97
of the order @{term "n * log(m)"} where @{term "n"} is the size of the
schirmer@25171
    98
(smaller) parent tree and @{term "m"} the size of the (bigger) new tree.
schirmer@25171
    99
*}
schirmer@25171
   100
schirmer@25171
   101
schirmer@25171
   102
consts "delete" :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
schirmer@25171
   103
primrec
schirmer@25171
   104
"delete x Tip = None"
schirmer@25171
   105
"delete x (Node l y d r) = (case delete x l of
schirmer@25171
   106
                              Some l' \<Rightarrow>
schirmer@25171
   107
                               (case delete x r of 
schirmer@25171
   108
                                  Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')
schirmer@25171
   109
                                | None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))
schirmer@25171
   110
                             | None \<Rightarrow>
schirmer@25171
   111
                                (case (delete x r) of 
schirmer@25171
   112
                                   Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')
schirmer@25171
   113
                                 | None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)
schirmer@25171
   114
                                           else None))"
schirmer@25171
   115
schirmer@25171
   116
schirmer@25171
   117
lemma delete_Some_set_of: "\<And>t'. delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t"
schirmer@25171
   118
proof (induct 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"
schirmer@25171
   135
	by simp
schirmer@25171
   136
      with l'_l Some x_l_Some del
schirmer@25171
   137
      show ?thesis
schirmer@25171
   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
schirmer@25171
   143
	by (fastsimp 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"
schirmer@25171
   153
	by simp
schirmer@25171
   154
      with Some x_l_None del
schirmer@25171
   155
      show ?thesis
schirmer@25171
   156
	by (fastsimp 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
schirmer@25171
   161
	by (fastsimp split: split_if_asm)
schirmer@25171
   162
    qed
schirmer@25171
   163
  qed
schirmer@25171
   164
qed
schirmer@25171
   165
schirmer@25171
   166
lemma delete_Some_all_distinct: 
schirmer@25171
   167
"\<And>t'. \<lbrakk>delete x t = Some t'; all_distinct t\<rbrakk> \<Longrightarrow> all_distinct t'"
schirmer@25171
   168
proof (induct 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'"
schirmer@25171
   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
schirmer@25171
   200
	by fastsimp
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
schirmer@25171
   205
	by fastsimp
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'"
schirmer@25171
   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
schirmer@25171
   220
	by fastsimp
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
schirmer@25171
   225
	by (fastsimp 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:
schirmer@25171
   240
  "\<And>t'. delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> set_of t'"
schirmer@25171
   241
proof (induct 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'"
schirmer@25171
   258
	by simp
schirmer@25171
   259
      from x_r x_l Some x_l_Some del 
schirmer@25171
   260
      show ?thesis
schirmer@25171
   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"
schirmer@25171
   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
schirmer@25171
   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'"
schirmer@25171
   280
	by simp
schirmer@25171
   281
      from x_r x_notin_l Some x_l_None del 
schirmer@25171
   282
      show ?thesis
schirmer@25171
   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"
schirmer@25171
   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
schirmer@25171
   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
schirmer@25171
   296
consts "subtract" :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
schirmer@25171
   297
primrec
schirmer@25171
   298
"subtract Tip t = Some t"
schirmer@25171
   299
"subtract (Node l x b r) t = 
schirmer@25171
   300
   (case delete x t of
schirmer@25171
   301
      Some t' \<Rightarrow> (case subtract l t' of 
schirmer@25171
   302
                   Some t'' \<Rightarrow> subtract r t''
schirmer@25171
   303
                  | None \<Rightarrow> None)
schirmer@25171
   304
    | None \<Rightarrow> None)"
schirmer@25171
   305
schirmer@25171
   306
lemma subtract_Some_set_of_res: 
schirmer@25171
   307
  "\<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
   308
proof (induct t\<^isub>1)
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''")
schirmer@25171
   327
	case (Some t\<^isub>2''')
schirmer@25171
   328
	from Node.hyps (2) [OF Some ] 
schirmer@25171
   329
	have "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''" .
schirmer@25171
   330
	with Some sub_l_Some del_x_Some sub t2''_t2' t2'_t2
schirmer@25171
   331
	show ?thesis
schirmer@25171
   332
	  by simp
schirmer@25171
   333
      next
schirmer@25171
   334
	case None
schirmer@25171
   335
	with del_x_Some sub_l_Some sub
schirmer@25171
   336
	show ?thesis
schirmer@25171
   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
schirmer@25171
   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: 
schirmer@25171
   352
  "\<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
   353
proof (induct t\<^isub>1)
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''")
schirmer@25171
   377
	case (Some t\<^isub>2''')
schirmer@25171
   378
	from Node.hyps (2) [OF Some ] 
schirmer@25171
   379
	have r_t\<^isub>2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
schirmer@25171
   380
	from Some sub_l_Some del_x_Some sub r_t\<^isub>2'' l_t2' t2'_t2 t2''_t2' x_t2
schirmer@25171
   381
	show ?thesis
schirmer@25171
   382
	  by auto
schirmer@25171
   383
      next
schirmer@25171
   384
	case None
schirmer@25171
   385
	with del_x_Some sub_l_Some sub
schirmer@25171
   386
	show ?thesis
schirmer@25171
   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
schirmer@25171
   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: 
schirmer@25171
   402
  "\<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
   403
proof (induct t\<^isub>1)
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''")
schirmer@25171
   423
	case (Some t\<^isub>2''')
schirmer@25171
   424
	from Node.hyps (2) [OF Some dist_t2''] 
schirmer@25171
   425
	have dist_t2''': "all_distinct t\<^isub>2'''" .
schirmer@25171
   426
	from Some sub_l_Some del_x_Some sub 
schirmer@25171
   427
             dist_t2'''
schirmer@25171
   428
	show ?thesis
schirmer@25171
   429
	  by simp
schirmer@25171
   430
      next
schirmer@25171
   431
	case None
schirmer@25171
   432
	with del_x_Some sub_l_Some sub
schirmer@25171
   433
	show ?thesis
schirmer@25171
   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
schirmer@25171
   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: 
schirmer@25171
   450
  "\<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
   451
proof (induct t\<^isub>1)
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''")
schirmer@25171
   475
	case (Some t\<^isub>2''')
schirmer@25171
   476
	from Node.hyps (2) [OF Some] 
schirmer@25171
   477
	have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}" .
schirmer@25171
   478
	from subtract_Some_set_of_res [OF Some]
schirmer@25171
   479
	have t2'''_t2'': "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''".
schirmer@25171
   480
	
schirmer@25171
   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'
schirmer@25171
   483
	show ?thesis
schirmer@25171
   484
	  by auto
schirmer@25171
   485
      next
schirmer@25171
   486
	case None
schirmer@25171
   487
	with del_x_Some sub_l_Some sub
schirmer@25171
   488
	show ?thesis
schirmer@25171
   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
schirmer@25171
   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
schirmer@25171
   502
	
schirmer@25171
   503
lemma subtract_Some_all_distinct:
schirmer@25171
   504
  "\<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
   505
proof (induct t\<^isub>1)
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''")
schirmer@25171
   539
	case (Some t\<^isub>2''')
schirmer@25171
   540
	from Node.hyps (2) [OF Some dist_t2''] 
schirmer@25171
   541
	have dist_r: "all_distinct r" .
schirmer@25171
   542
	from subtract_Some_set_of [OF Some]
schirmer@25171
   543
	have r_t2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
schirmer@25171
   544
	from subtract_Some_dist_res [OF Some]
schirmer@25171
   545
	have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}".
schirmer@25171
   546
schirmer@25171
   547
	from dist_l dist_r Some sub_l_Some del_x_Some r_t2'' l_t2' x_t2 x_not_t2' 
schirmer@25171
   548
	     t2''_t2' dist_l_t2'' dist_r_t2'''
schirmer@25171
   549
	show ?thesis
schirmer@25171
   550
	  by auto
schirmer@25171
   551
      next
schirmer@25171
   552
	case None
schirmer@25171
   553
	with del_x_Some sub_l_Some sub
schirmer@25171
   554
	show ?thesis
schirmer@25171
   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
schirmer@25171
   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);
schirmer@25171
   645
val const_decls = map (fn i => Syntax.no_syn 
schirmer@25171
   646
                                 ("const" ^ string_of_int i,Type ("nat",[]))) nums
schirmer@25171
   647
wenzelm@29269
   648
val consts = sort TermOrd.fast_term_ord 
schirmer@25171
   649
              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
wenzelm@29269
   650
val consts' = sort TermOrd.fast_term_ord 
schirmer@25171
   651
              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
schirmer@25171
   652
schirmer@25171
   653
val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts
schirmer@25171
   654
schirmer@25171
   655
schirmer@25171
   656
val t' = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts'
schirmer@25171
   657
schirmer@25171
   658
schirmer@25171
   659
val dist = 
schirmer@25171
   660
     HOLogic.Trueprop$
schirmer@25171
   661
       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t)
schirmer@25171
   662
schirmer@25171
   663
val dist' = 
schirmer@25171
   664
     HOLogic.Trueprop$
schirmer@25171
   665
       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t')
schirmer@25171
   666
wenzelm@32740
   667
val da = Unsynchronized.ref refl;
schirmer@25171
   668
schirmer@25171
   669
*}
schirmer@25171
   670
schirmer@25171
   671
setup {*
schirmer@25171
   672
Theory.add_consts_i const_decls
haftmann@27691
   673
#> (fn thy  => let val ([thm],thy') = PureThy.add_axioms [(("dist_axiom",dist),[])] thy
schirmer@25171
   674
               in (da := thm; thy') end)
schirmer@25171
   675
*}
schirmer@25171
   676
schirmer@25171
   677
schirmer@25171
   678
ML {* 
wenzelm@32010
   679
 val ct' = cterm_of @{theory} t';
schirmer@25171
   680
*}
schirmer@25171
   681
schirmer@25171
   682
ML {*
schirmer@25171
   683
 timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);())) 
schirmer@25171
   684
*}
schirmer@25171
   685
schirmer@25171
   686
(* 590 s *)
schirmer@25171
   687
schirmer@25171
   688
ML {*
schirmer@25171
   689
schirmer@25171
   690
schirmer@25171
   691
val p1 = 
schirmer@25171
   692
 the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const1",Type ("nat",[]))) t)
schirmer@25171
   693
val p2 =
schirmer@25171
   694
 the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const10000",Type ("nat",[]))) t)
schirmer@25171
   695
*}
schirmer@25171
   696
schirmer@25171
   697
schirmer@25171
   698
ML {* timeit (fn () => DistinctTreeProver.distinctTreeProver (!da )
schirmer@25171
   699
       p1
schirmer@25171
   700
       p2)*}
schirmer@25171
   701
schirmer@25171
   702
schirmer@25171
   703
ML {* timeit (fn () => (DistinctTreeProver.deleteProver (!da) p1;())) *}
schirmer@25171
   704
schirmer@25171
   705
schirmer@25171
   706
schirmer@25171
   707
schirmer@25171
   708
ML {*
wenzelm@32010
   709
val cdist' = cterm_of @{theory} dist';
schirmer@25171
   710
DistinctTreeProver.distinct_implProver (!da) cdist';
schirmer@25171
   711
*}
schirmer@25171
   712
schirmer@25171
   713
*)
schirmer@25171
   714
schirmer@25171
   715
end