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