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