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