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