src/HOL/Statespace/DistinctTreeProver.thy
changeset 25171 4a9c25bffc9b
child 25174 d70d6dbc3a60
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Wed Oct 24 18:36:09 2007 +0200
     1.3 @@ -0,0 +1,726 @@
     1.4 +(*  Title:      DistinctTreeProver.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Norbert Schirmer, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}*}
    1.10 +
    1.11 +theory DistinctTreeProver 
    1.12 +imports Main
    1.13 +uses (distinct_tree_prover)
    1.14 +begin
    1.15 +
    1.16 +text {* A state space manages a set of (abstract) names and assumes
    1.17 +that the names are distinct. The names are stored as parameters of a
    1.18 +locale and distinctness as an assumption. The most common request is
    1.19 +to proof distinctness of two given names. We maintain the names in a
    1.20 +balanced binary tree and formulate a predicate that all nodes in the
    1.21 +tree have distinct names. This setup leads to logarithmic certificates.
    1.22 +*}
    1.23 +
    1.24 +subsection {* The Binary Tree *}
    1.25 +
    1.26 +datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
    1.27 +
    1.28 +
    1.29 +text {* The boolean flag in the node marks the content of the node as
    1.30 +deleted, without having to build a new tree. We prefer the boolean
    1.31 +flag to an option type, so that the ML-layer can still use the node
    1.32 +content to facilitate binary search in the tree. The ML code keeps the
    1.33 +nodes sorted using the term order. We do not have to push ordering to
    1.34 +the HOL level. *}
    1.35 +
    1.36 +subsection {* Distinctness of Nodes *}
    1.37 +
    1.38 +
    1.39 +consts set_of:: "'a tree \<Rightarrow> 'a set"
    1.40 +primrec 
    1.41 +"set_of Tip = {}"
    1.42 +"set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"
    1.43 +
    1.44 +consts all_distinct:: "'a tree \<Rightarrow> bool"
    1.45 +primrec
    1.46 +"all_distinct Tip = True"
    1.47 +"all_distinct (Node l x d r) = ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> 
    1.48 +                               set_of l \<inter> set_of r = {} \<and>
    1.49 +                               all_distinct l \<and> all_distinct r)"
    1.50 +
    1.51 +text {* Given a binary tree @{term "t"} for which 
    1.52 +@{const all_distinct} holds, given two different nodes contained in the tree,
    1.53 +we want to write a ML function that generates a logarithmic
    1.54 +certificate that the content of the nodes is distinct. We use the
    1.55 +following lemmas to achieve this.  *} 
    1.56 +
    1.57 +lemma all_distinct_left:
    1.58 +"all_distinct (Node l x b r) \<Longrightarrow> all_distinct l"
    1.59 +  by simp
    1.60 +
    1.61 +lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r"
    1.62 +  by simp
    1.63 +
    1.64 +lemma distinct_left: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of l \<rbrakk> \<Longrightarrow> x\<noteq>y"
    1.65 +  by auto
    1.66 +
    1.67 +lemma distinct_right: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of r \<rbrakk> \<Longrightarrow> x\<noteq>y"
    1.68 +  by auto
    1.69 +
    1.70 +lemma distinct_left_right: "\<lbrakk>all_distinct (Node l z b r); x \<in> set_of l; y \<in> set_of r\<rbrakk>
    1.71 +  \<Longrightarrow> x\<noteq>y"
    1.72 +  by auto
    1.73 +
    1.74 +lemma in_set_root: "x \<in> set_of (Node l x False r)"
    1.75 +  by simp
    1.76 +
    1.77 +lemma in_set_left: "y \<in> set_of l \<Longrightarrow>  y \<in> set_of (Node l x False r)"
    1.78 +  by simp
    1.79 +
    1.80 +lemma in_set_right: "y \<in> set_of r \<Longrightarrow>  y \<in> set_of (Node l x False r)"
    1.81 +  by simp
    1.82 +
    1.83 +lemma swap_neq: "x \<noteq> y \<Longrightarrow> y \<noteq> x"
    1.84 +  by blast
    1.85 +
    1.86 +lemma neq_to_eq_False: "x\<noteq>y \<Longrightarrow> (x=y)\<equiv>False"
    1.87 +  by simp
    1.88 +
    1.89 +subsection {* Containment of Trees *}
    1.90 +
    1.91 +text {* When deriving a state space from other ones, we create a new
    1.92 +name tree which contains all the names of the parent state spaces and
    1.93 +assumme the predicate @{const all_distinct}. We then prove that the new locale
    1.94 +interprets all parent locales. Hence we have to show that the new
    1.95 +distinctness assumption on all names implies the distinctness
    1.96 +assumptions of the parent locales. This proof is implemented in ML. We
    1.97 +do this efficiently by defining a kind of containment check of trees
    1.98 +by 'subtraction'.  We subtract the parent tree from the new tree. If this
    1.99 +succeeds we know that @{const all_distinct} of the new tree implies
   1.100 +@{const all_distinct} of the parent tree.  The resulting certificate is
   1.101 +of the order @{term "n * log(m)"} where @{term "n"} is the size of the
   1.102 +(smaller) parent tree and @{term "m"} the size of the (bigger) new tree.
   1.103 +*}
   1.104 +
   1.105 +
   1.106 +consts "delete" :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
   1.107 +primrec
   1.108 +"delete x Tip = None"
   1.109 +"delete x (Node l y d r) = (case delete x l of
   1.110 +                              Some l' \<Rightarrow>
   1.111 +                               (case delete x r of 
   1.112 +                                  Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')
   1.113 +                                | None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))
   1.114 +                             | None \<Rightarrow>
   1.115 +                                (case (delete x r) of 
   1.116 +                                   Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')
   1.117 +                                 | None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)
   1.118 +                                           else None))"
   1.119 +
   1.120 +
   1.121 +lemma delete_Some_set_of: "\<And>t'. delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t"
   1.122 +proof (induct t)
   1.123 +  case Tip thus ?case by simp
   1.124 +next
   1.125 +  case (Node l y d r)
   1.126 +  have del: "delete x (Node l y d r) = Some t'".
   1.127 +  show ?case
   1.128 +  proof (cases "delete x l")
   1.129 +    case (Some l')
   1.130 +    note x_l_Some = this
   1.131 +    with Node.hyps
   1.132 +    have l'_l: "set_of l' \<subseteq> set_of l"
   1.133 +      by simp
   1.134 +    show ?thesis
   1.135 +    proof (cases "delete x r")
   1.136 +      case (Some r')
   1.137 +      with Node.hyps
   1.138 +      have "set_of r' \<subseteq> set_of r"
   1.139 +	by simp
   1.140 +      with l'_l Some x_l_Some del
   1.141 +      show ?thesis
   1.142 +	by (auto split: split_if_asm)
   1.143 +    next
   1.144 +      case None
   1.145 +      with l'_l Some x_l_Some del
   1.146 +      show ?thesis
   1.147 +	by (fastsimp split: split_if_asm)
   1.148 +    qed
   1.149 +  next
   1.150 +    case None
   1.151 +    note x_l_None = this
   1.152 +    show ?thesis
   1.153 +    proof (cases "delete x r")
   1.154 +      case (Some r')
   1.155 +      with Node.hyps
   1.156 +      have "set_of r' \<subseteq> set_of r"
   1.157 +	by simp
   1.158 +      with Some x_l_None del
   1.159 +      show ?thesis
   1.160 +	by (fastsimp split: split_if_asm)
   1.161 +    next
   1.162 +      case None
   1.163 +      with x_l_None del
   1.164 +      show ?thesis
   1.165 +	by (fastsimp split: split_if_asm)
   1.166 +    qed
   1.167 +  qed
   1.168 +qed
   1.169 +
   1.170 +lemma delete_Some_all_distinct: 
   1.171 +"\<And>t'. \<lbrakk>delete x t = Some t'; all_distinct t\<rbrakk> \<Longrightarrow> all_distinct t'"
   1.172 +proof (induct t)
   1.173 +  case Tip thus ?case by simp
   1.174 +next
   1.175 +  case (Node l y d r)
   1.176 +  have del: "delete x (Node l y d r) = Some t'".
   1.177 +  have "all_distinct (Node l y d r)".
   1.178 +  then obtain
   1.179 +    dist_l: "all_distinct l" and
   1.180 +    dist_r: "all_distinct r" and
   1.181 +    d: "d \<or> (y \<notin> set_of l \<and> y \<notin> set_of r)" and
   1.182 +    dist_l_r: "set_of l \<inter> set_of r = {}"
   1.183 +    by auto
   1.184 +  show ?case
   1.185 +  proof (cases "delete x l")
   1.186 +    case (Some l')
   1.187 +    note x_l_Some = this
   1.188 +    from Node.hyps (1) [OF Some dist_l]
   1.189 +    have dist_l': "all_distinct l'"
   1.190 +      by simp
   1.191 +    from delete_Some_set_of [OF x_l_Some]
   1.192 +    have l'_l: "set_of l' \<subseteq> set_of l".
   1.193 +    show ?thesis
   1.194 +    proof (cases "delete x r")
   1.195 +      case (Some r')
   1.196 +      from Node.hyps (2) [OF Some dist_r]
   1.197 +      have dist_r': "all_distinct r'"
   1.198 +	by simp
   1.199 +      from delete_Some_set_of [OF Some]
   1.200 +      have "set_of r' \<subseteq> set_of r".
   1.201 +      
   1.202 +      with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r
   1.203 +      show ?thesis
   1.204 +	by fastsimp
   1.205 +    next
   1.206 +      case None
   1.207 +      with l'_l dist_l'  x_l_Some del d dist_l_r dist_r
   1.208 +      show ?thesis
   1.209 +	by fastsimp
   1.210 +    qed
   1.211 +  next
   1.212 +    case None
   1.213 +    note x_l_None = this
   1.214 +    show ?thesis
   1.215 +    proof (cases "delete x r")
   1.216 +      case (Some r')
   1.217 +      with Node.hyps (2) [OF Some dist_r]
   1.218 +      have dist_r': "all_distinct r'"
   1.219 +	by simp
   1.220 +      from delete_Some_set_of [OF Some]
   1.221 +      have "set_of r' \<subseteq> set_of r".
   1.222 +      with Some dist_r' x_l_None del dist_l d dist_l_r
   1.223 +      show ?thesis
   1.224 +	by fastsimp
   1.225 +    next
   1.226 +      case None
   1.227 +      with x_l_None del dist_l dist_r d dist_l_r
   1.228 +      show ?thesis
   1.229 +	by (fastsimp split: split_if_asm)
   1.230 +    qed
   1.231 +  qed
   1.232 +qed
   1.233 +
   1.234 +lemma delete_None_set_of_conv: "delete x t = None = (x \<notin> set_of t)"
   1.235 +proof (induct t)
   1.236 +  case Tip thus ?case by simp
   1.237 +next
   1.238 +  case (Node l y d r)
   1.239 +  thus ?case
   1.240 +    by (auto split: option.splits)
   1.241 +qed
   1.242 +
   1.243 +lemma delete_Some_x_set_of:
   1.244 +  "\<And>t'. delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> set_of t'"
   1.245 +proof (induct t)
   1.246 +  case Tip thus ?case by simp
   1.247 +next
   1.248 +  case (Node l y d r)
   1.249 +  have del: "delete x (Node l y d r) = Some t'".
   1.250 +  show ?case
   1.251 +  proof (cases "delete x l")
   1.252 +    case (Some l')
   1.253 +    note x_l_Some = this
   1.254 +    from Node.hyps (1) [OF Some]
   1.255 +    obtain x_l: "x \<in> set_of l" "x \<notin> set_of l'"
   1.256 +      by simp
   1.257 +    show ?thesis
   1.258 +    proof (cases "delete x r")
   1.259 +      case (Some r')
   1.260 +      from Node.hyps (2) [OF Some]
   1.261 +      obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"
   1.262 +	by simp
   1.263 +      from x_r x_l Some x_l_Some del 
   1.264 +      show ?thesis
   1.265 +	by (clarsimp split: split_if_asm)
   1.266 +    next
   1.267 +      case None
   1.268 +      then have "x \<notin> set_of r"
   1.269 +	by (simp add: delete_None_set_of_conv)
   1.270 +      with x_l None x_l_Some del
   1.271 +      show ?thesis
   1.272 +	by (clarsimp split: split_if_asm)
   1.273 +    qed
   1.274 +  next
   1.275 +    case None
   1.276 +    note x_l_None = this
   1.277 +    then have x_notin_l: "x \<notin> set_of l"
   1.278 +      by (simp add: delete_None_set_of_conv)
   1.279 +    show ?thesis
   1.280 +    proof (cases "delete x r")
   1.281 +      case (Some r')
   1.282 +      from Node.hyps (2) [OF Some]
   1.283 +      obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"
   1.284 +	by simp
   1.285 +      from x_r x_notin_l Some x_l_None del 
   1.286 +      show ?thesis
   1.287 +	by (clarsimp split: split_if_asm)
   1.288 +    next
   1.289 +      case None
   1.290 +      then have "x \<notin> set_of r"
   1.291 +	by (simp add: delete_None_set_of_conv)
   1.292 +      with None x_l_None x_notin_l del
   1.293 +      show ?thesis
   1.294 +	by (clarsimp split: split_if_asm)
   1.295 +    qed
   1.296 +  qed
   1.297 +qed
   1.298 +
   1.299 +
   1.300 +consts "subtract" :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
   1.301 +primrec
   1.302 +"subtract Tip t = Some t"
   1.303 +"subtract (Node l x b r) t = 
   1.304 +   (case delete x t of
   1.305 +      Some t' \<Rightarrow> (case subtract l t' of 
   1.306 +                   Some t'' \<Rightarrow> subtract r t''
   1.307 +                  | None \<Rightarrow> None)
   1.308 +    | None \<Rightarrow> None)"
   1.309 +
   1.310 +lemma subtract_Some_set_of_res: 
   1.311 +  "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t \<subseteq> set_of t\<^isub>2"
   1.312 +proof (induct t\<^isub>1)
   1.313 +  case Tip thus ?case by simp
   1.314 +next
   1.315 +  case (Node l x b r)
   1.316 +  have sub: "subtract (Node l x b r) t\<^isub>2 = Some t".
   1.317 +  show ?case
   1.318 +  proof (cases "delete x t\<^isub>2")
   1.319 +    case (Some t\<^isub>2')
   1.320 +    note del_x_Some = this
   1.321 +    from delete_Some_set_of [OF Some] 
   1.322 +    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
   1.323 +    show ?thesis
   1.324 +    proof (cases "subtract l t\<^isub>2'")
   1.325 +      case (Some t\<^isub>2'')
   1.326 +      note sub_l_Some = this
   1.327 +      from Node.hyps (1) [OF Some] 
   1.328 +      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
   1.329 +      show ?thesis
   1.330 +      proof (cases "subtract r t\<^isub>2''")
   1.331 +	case (Some t\<^isub>2''')
   1.332 +	from Node.hyps (2) [OF Some ] 
   1.333 +	have "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''" .
   1.334 +	with Some sub_l_Some del_x_Some sub t2''_t2' t2'_t2
   1.335 +	show ?thesis
   1.336 +	  by simp
   1.337 +      next
   1.338 +	case None
   1.339 +	with del_x_Some sub_l_Some sub
   1.340 +	show ?thesis
   1.341 +	  by simp
   1.342 +      qed
   1.343 +    next
   1.344 +      case None
   1.345 +      with del_x_Some sub 
   1.346 +      show ?thesis
   1.347 +	by simp
   1.348 +    qed
   1.349 +  next
   1.350 +    case None
   1.351 +    with sub show ?thesis by simp
   1.352 +  qed
   1.353 +qed
   1.354 +
   1.355 +lemma subtract_Some_set_of: 
   1.356 +  "\<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"
   1.357 +proof (induct t\<^isub>1)
   1.358 +  case Tip thus ?case by simp
   1.359 +next
   1.360 +  case (Node l x d r)
   1.361 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
   1.362 +  show ?case
   1.363 +  proof (cases "delete x t\<^isub>2")
   1.364 +    case (Some t\<^isub>2')
   1.365 +    note del_x_Some = this
   1.366 +    from delete_Some_set_of [OF Some] 
   1.367 +    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
   1.368 +    from delete_None_set_of_conv [of x t\<^isub>2] Some
   1.369 +    have x_t2: "x \<in> set_of t\<^isub>2"
   1.370 +      by simp
   1.371 +    show ?thesis
   1.372 +    proof (cases "subtract l t\<^isub>2'")
   1.373 +      case (Some t\<^isub>2'')
   1.374 +      note sub_l_Some = this
   1.375 +      from Node.hyps (1) [OF Some] 
   1.376 +      have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" .
   1.377 +      from subtract_Some_set_of_res [OF Some]
   1.378 +      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
   1.379 +      show ?thesis
   1.380 +      proof (cases "subtract r t\<^isub>2''")
   1.381 +	case (Some t\<^isub>2''')
   1.382 +	from Node.hyps (2) [OF Some ] 
   1.383 +	have r_t\<^isub>2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
   1.384 +	from Some sub_l_Some del_x_Some sub r_t\<^isub>2'' l_t2' t2'_t2 t2''_t2' x_t2
   1.385 +	show ?thesis
   1.386 +	  by auto
   1.387 +      next
   1.388 +	case None
   1.389 +	with del_x_Some sub_l_Some sub
   1.390 +	show ?thesis
   1.391 +	  by simp
   1.392 +      qed
   1.393 +    next
   1.394 +      case None
   1.395 +      with del_x_Some sub 
   1.396 +      show ?thesis
   1.397 +	by simp
   1.398 +    qed
   1.399 +  next
   1.400 +    case None
   1.401 +    with sub show ?thesis by simp
   1.402 +  qed
   1.403 +qed
   1.404 +
   1.405 +lemma subtract_Some_all_distinct_res: 
   1.406 +  "\<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"
   1.407 +proof (induct t\<^isub>1)
   1.408 +  case Tip thus ?case by simp
   1.409 +next
   1.410 +  case (Node l x d r)
   1.411 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
   1.412 +  have dist_t2: "all_distinct t\<^isub>2".
   1.413 +  show ?case
   1.414 +  proof (cases "delete x t\<^isub>2")
   1.415 +    case (Some t\<^isub>2')
   1.416 +    note del_x_Some = this
   1.417 +    from delete_Some_all_distinct [OF Some dist_t2] 
   1.418 +    have dist_t2': "all_distinct t\<^isub>2'" .
   1.419 +    show ?thesis
   1.420 +    proof (cases "subtract l t\<^isub>2'")
   1.421 +      case (Some t\<^isub>2'')
   1.422 +      note sub_l_Some = this
   1.423 +      from Node.hyps (1) [OF Some dist_t2'] 
   1.424 +      have dist_t2'': "all_distinct t\<^isub>2''" .
   1.425 +      show ?thesis
   1.426 +      proof (cases "subtract r t\<^isub>2''")
   1.427 +	case (Some t\<^isub>2''')
   1.428 +	from Node.hyps (2) [OF Some dist_t2''] 
   1.429 +	have dist_t2''': "all_distinct t\<^isub>2'''" .
   1.430 +	from Some sub_l_Some del_x_Some sub 
   1.431 +             dist_t2'''
   1.432 +	show ?thesis
   1.433 +	  by simp
   1.434 +      next
   1.435 +	case None
   1.436 +	with del_x_Some sub_l_Some sub
   1.437 +	show ?thesis
   1.438 +	  by simp
   1.439 +      qed
   1.440 +    next
   1.441 +      case None
   1.442 +      with del_x_Some sub 
   1.443 +      show ?thesis
   1.444 +	by simp
   1.445 +    qed
   1.446 +  next
   1.447 +    case None
   1.448 +    with sub show ?thesis by simp
   1.449 +  qed
   1.450 +qed
   1.451 +
   1.452 +
   1.453 +lemma subtract_Some_dist_res: 
   1.454 +  "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<inter> set_of t = {}"
   1.455 +proof (induct t\<^isub>1)
   1.456 +  case Tip thus ?case by simp
   1.457 +next
   1.458 +  case (Node l x d r)
   1.459 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
   1.460 +  show ?case
   1.461 +  proof (cases "delete x t\<^isub>2")
   1.462 +    case (Some t\<^isub>2')
   1.463 +    note del_x_Some = this
   1.464 +    from delete_Some_x_set_of [OF Some]
   1.465 +    obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'"
   1.466 +      by simp
   1.467 +    from delete_Some_set_of [OF Some]
   1.468 +    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
   1.469 +    show ?thesis
   1.470 +    proof (cases "subtract l t\<^isub>2'")
   1.471 +      case (Some t\<^isub>2'')
   1.472 +      note sub_l_Some = this
   1.473 +      from Node.hyps (1) [OF Some ] 
   1.474 +      have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}".
   1.475 +      from subtract_Some_set_of_res [OF Some]
   1.476 +      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
   1.477 +      show ?thesis
   1.478 +      proof (cases "subtract r t\<^isub>2''")
   1.479 +	case (Some t\<^isub>2''')
   1.480 +	from Node.hyps (2) [OF Some] 
   1.481 +	have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}" .
   1.482 +	from subtract_Some_set_of_res [OF Some]
   1.483 +	have t2'''_t2'': "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''".
   1.484 +	
   1.485 +	from Some sub_l_Some del_x_Some sub t2'''_t2'' dist_l_t2'' dist_r_t2'''
   1.486 +             t2''_t2' t2'_t2 x_not_t2'
   1.487 +	show ?thesis
   1.488 +	  by auto
   1.489 +      next
   1.490 +	case None
   1.491 +	with del_x_Some sub_l_Some sub
   1.492 +	show ?thesis
   1.493 +	  by simp
   1.494 +      qed
   1.495 +    next
   1.496 +      case None
   1.497 +      with del_x_Some sub 
   1.498 +      show ?thesis
   1.499 +	by simp
   1.500 +    qed
   1.501 +  next
   1.502 +    case None
   1.503 +    with sub show ?thesis by simp
   1.504 +  qed
   1.505 +qed
   1.506 +	
   1.507 +lemma subtract_Some_all_distinct:
   1.508 +  "\<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"
   1.509 +proof (induct t\<^isub>1)
   1.510 +  case Tip thus ?case by simp
   1.511 +next
   1.512 +  case (Node l x d r)
   1.513 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
   1.514 +  have dist_t2: "all_distinct t\<^isub>2".
   1.515 +  show ?case
   1.516 +  proof (cases "delete x t\<^isub>2")
   1.517 +    case (Some t\<^isub>2')
   1.518 +    note del_x_Some = this
   1.519 +    from delete_Some_all_distinct [OF Some dist_t2 ] 
   1.520 +    have dist_t2': "all_distinct t\<^isub>2'" .
   1.521 +    from delete_Some_set_of [OF Some]
   1.522 +    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
   1.523 +    from delete_Some_x_set_of [OF Some]
   1.524 +    obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'"
   1.525 +      by simp
   1.526 +
   1.527 +    show ?thesis
   1.528 +    proof (cases "subtract l t\<^isub>2'")
   1.529 +      case (Some t\<^isub>2'')
   1.530 +      note sub_l_Some = this
   1.531 +      from Node.hyps (1) [OF Some dist_t2' ] 
   1.532 +      have dist_l: "all_distinct l" .
   1.533 +      from subtract_Some_all_distinct_res [OF Some dist_t2'] 
   1.534 +      have dist_t2'': "all_distinct t\<^isub>2''" .
   1.535 +      from subtract_Some_set_of [OF Some]
   1.536 +      have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" .
   1.537 +      from subtract_Some_set_of_res [OF Some]
   1.538 +      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
   1.539 +      from subtract_Some_dist_res [OF Some]
   1.540 +      have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}".
   1.541 +      show ?thesis
   1.542 +      proof (cases "subtract r t\<^isub>2''")
   1.543 +	case (Some t\<^isub>2''')
   1.544 +	from Node.hyps (2) [OF Some dist_t2''] 
   1.545 +	have dist_r: "all_distinct r" .
   1.546 +	from subtract_Some_set_of [OF Some]
   1.547 +	have r_t2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
   1.548 +	from subtract_Some_dist_res [OF Some]
   1.549 +	have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}".
   1.550 +
   1.551 +	from dist_l dist_r Some sub_l_Some del_x_Some r_t2'' l_t2' x_t2 x_not_t2' 
   1.552 +	     t2''_t2' dist_l_t2'' dist_r_t2'''
   1.553 +	show ?thesis
   1.554 +	  by auto
   1.555 +      next
   1.556 +	case None
   1.557 +	with del_x_Some sub_l_Some sub
   1.558 +	show ?thesis
   1.559 +	  by simp
   1.560 +      qed
   1.561 +    next
   1.562 +      case None
   1.563 +      with del_x_Some sub 
   1.564 +      show ?thesis
   1.565 +	by simp
   1.566 +    qed
   1.567 +  next
   1.568 +    case None
   1.569 +    with sub show ?thesis by simp
   1.570 +  qed
   1.571 +qed
   1.572 +
   1.573 +
   1.574 +lemma delete_left:
   1.575 +  assumes dist: "all_distinct (Node l y d r)" 
   1.576 +  assumes del_l: "delete x l = Some l'"
   1.577 +  shows "delete x (Node l y d r) = Some (Node l' y d r)"
   1.578 +proof -
   1.579 +  from delete_Some_x_set_of [OF del_l]
   1.580 +  obtain "x \<in> set_of l"
   1.581 +    by simp
   1.582 +  moreover with dist 
   1.583 +  have "delete x r = None"
   1.584 +    by (cases "delete x r") (auto dest:delete_Some_x_set_of)
   1.585 +
   1.586 +  ultimately 
   1.587 +  show ?thesis
   1.588 +    using del_l dist
   1.589 +    by (auto split: option.splits)
   1.590 +qed
   1.591 +
   1.592 +lemma delete_right:
   1.593 +  assumes dist: "all_distinct (Node l y d r)" 
   1.594 +  assumes del_r: "delete x r = Some r'"
   1.595 +  shows "delete x (Node l y d r) = Some (Node l y d r')"
   1.596 +proof -
   1.597 +  from delete_Some_x_set_of [OF del_r]
   1.598 +  obtain "x \<in> set_of r"
   1.599 +    by simp
   1.600 +  moreover with dist 
   1.601 +  have "delete x l = None"
   1.602 +    by (cases "delete x l") (auto dest:delete_Some_x_set_of)
   1.603 +
   1.604 +  ultimately 
   1.605 +  show ?thesis
   1.606 +    using del_r dist
   1.607 +    by (auto split: option.splits)
   1.608 +qed
   1.609 +
   1.610 +lemma delete_root: 
   1.611 +  assumes dist: "all_distinct (Node l x False r)" 
   1.612 +  shows "delete x (Node l x False r) = Some (Node l x True r)"
   1.613 +proof -
   1.614 +  from dist have "delete x r = None"
   1.615 +    by (cases "delete x r") (auto dest:delete_Some_x_set_of)
   1.616 +  moreover
   1.617 +  from dist have "delete x l = None"
   1.618 +    by (cases "delete x l") (auto dest:delete_Some_x_set_of)
   1.619 +  ultimately show ?thesis
   1.620 +    using dist
   1.621 +       by (auto split: option.splits)
   1.622 +qed               
   1.623 +
   1.624 +lemma subtract_Node:
   1.625 + assumes del: "delete x t = Some t'"                                
   1.626 + assumes sub_l: "subtract l t' = Some t''"
   1.627 + assumes sub_r: "subtract r t'' = Some t'''"
   1.628 + shows "subtract (Node l x False r) t = Some t'''"
   1.629 +using del sub_l sub_r
   1.630 +by simp
   1.631 +
   1.632 +lemma subtract_Tip: "subtract Tip t = Some t"
   1.633 +  by simp
   1.634 + 
   1.635 +text {* Now we have all the theorems in place that are needed for the
   1.636 +certificate generating ML functions. *}
   1.637 +
   1.638 +use distinct_tree_prover
   1.639 +
   1.640 +(* Uncomment for profiling or debugging *)
   1.641 +(*
   1.642 +ML {*
   1.643 +(*
   1.644 +val nums = (0 upto 10000);
   1.645 +val nums' = (200 upto 3000);
   1.646 +*)
   1.647 +val nums = (0 upto 10000);
   1.648 +val nums' = (0 upto 3000);
   1.649 +val const_decls = map (fn i => Syntax.no_syn 
   1.650 +                                 ("const" ^ string_of_int i,Type ("nat",[]))) nums
   1.651 +
   1.652 +val consts = sort Term.fast_term_ord 
   1.653 +              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
   1.654 +val consts' = sort Term.fast_term_ord 
   1.655 +              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
   1.656 +
   1.657 +val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts
   1.658 +
   1.659 +
   1.660 +val t' = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts'
   1.661 +
   1.662 +
   1.663 +val dist = 
   1.664 +     HOLogic.Trueprop$
   1.665 +       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t)
   1.666 +
   1.667 +val dist' = 
   1.668 +     HOLogic.Trueprop$
   1.669 +       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t')
   1.670 +
   1.671 +val da = ref refl;
   1.672 +
   1.673 +*}
   1.674 +
   1.675 +setup {*
   1.676 +Theory.add_consts_i const_decls
   1.677 +#> (fn thy  => let val ([thm],thy') = PureThy.add_axioms_i [(("dist_axiom",dist),[])] thy
   1.678 +               in (da := thm; thy') end)
   1.679 +*}
   1.680 +
   1.681 +
   1.682 +ML {* 
   1.683 + val ct' = cterm_of (the_context ()) t';
   1.684 +*}
   1.685 +
   1.686 +ML {*
   1.687 + timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);())) 
   1.688 +*}
   1.689 +
   1.690 +(* 590 s *)
   1.691 +
   1.692 +ML {*
   1.693 +
   1.694 +
   1.695 +val p1 = 
   1.696 + the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const1",Type ("nat",[]))) t)
   1.697 +val p2 =
   1.698 + the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const10000",Type ("nat",[]))) t)
   1.699 +*}
   1.700 +
   1.701 +
   1.702 +ML {* timeit (fn () => DistinctTreeProver.distinctTreeProver (!da )
   1.703 +       p1
   1.704 +       p2)*}
   1.705 +
   1.706 +
   1.707 +ML {* timeit (fn () => (DistinctTreeProver.deleteProver (!da) p1;())) *}
   1.708 +
   1.709 +
   1.710 +
   1.711 +
   1.712 +ML {*
   1.713 +val cdist' = cterm_of (the_context ()) dist';
   1.714 +DistinctTreeProver.distinct_implProver (!da) cdist';
   1.715 +*}
   1.716 +
   1.717 +*)
   1.718 +
   1.719 +
   1.720 +
   1.721 +
   1.722 +
   1.723 +
   1.724 +
   1.725 +
   1.726 +
   1.727 +
   1.728 +end
   1.729 +