added Statespace library
authorschirmer
Wed Oct 24 18:36:09 2007 +0200 (2007-10-24)
changeset 251714a9c25bffc9b
parent 25170 bd06fd396fd0
child 25172 ad25033f9ca4
added Statespace library
src/HOL/IsaMakefile
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Statespace/ROOT.ML
src/HOL/Statespace/StateFun.thy
src/HOL/Statespace/StateSpaceEx.thy
src/HOL/Statespace/StateSpaceLocale.thy
src/HOL/Statespace/StateSpaceSyntax.thy
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/document/root.tex
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Oct 24 18:32:53 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Oct 24 18:36:09 2007 +0200
     1.3 @@ -37,6 +37,7 @@
     1.4    HOL-NumberTheory \
     1.5    HOL-Prolog \
     1.6    HOL-SET-Protocol \
     1.7 +  HOL-Statespace \
     1.8    HOL-Subst \
     1.9        TLA-Buffer \
    1.10        TLA-Inc \
    1.11 @@ -845,6 +846,17 @@
    1.12    Word/Examples/WordExamples.thy
    1.13  	@cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples
    1.14  
    1.15 +## HOL-Statespace
    1.16 +
    1.17 +HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz
    1.18 +
    1.19 +$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy \
    1.20 +  Statespace/StateFun.thy Statespace/StateSpaceLocale.thy \
    1.21 +  Statespace/StateSpaceSyntax.thy StateSpace/StateSpaceEx.thy \
    1.22 +  Statespace/distinct_tree_prover.ML Statespace/state_space.ML \
    1.23 +  Statespace/state_fun.ML \
    1.24 +  Statespace/document/root.tex
    1.25 +	@$(ISATOOL) usedir -g true $(OUT)/HOL Statespace
    1.26  
    1.27  ## clean
    1.28  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Wed Oct 24 18:36:09 2007 +0200
     2.3 @@ -0,0 +1,726 @@
     2.4 +(*  Title:      DistinctTreeProver.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Norbert Schirmer, TU Muenchen
     2.7 +*)
     2.8 +
     2.9 +header {* Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}*}
    2.10 +
    2.11 +theory DistinctTreeProver 
    2.12 +imports Main
    2.13 +uses (distinct_tree_prover)
    2.14 +begin
    2.15 +
    2.16 +text {* A state space manages a set of (abstract) names and assumes
    2.17 +that the names are distinct. The names are stored as parameters of a
    2.18 +locale and distinctness as an assumption. The most common request is
    2.19 +to proof distinctness of two given names. We maintain the names in a
    2.20 +balanced binary tree and formulate a predicate that all nodes in the
    2.21 +tree have distinct names. This setup leads to logarithmic certificates.
    2.22 +*}
    2.23 +
    2.24 +subsection {* The Binary Tree *}
    2.25 +
    2.26 +datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
    2.27 +
    2.28 +
    2.29 +text {* The boolean flag in the node marks the content of the node as
    2.30 +deleted, without having to build a new tree. We prefer the boolean
    2.31 +flag to an option type, so that the ML-layer can still use the node
    2.32 +content to facilitate binary search in the tree. The ML code keeps the
    2.33 +nodes sorted using the term order. We do not have to push ordering to
    2.34 +the HOL level. *}
    2.35 +
    2.36 +subsection {* Distinctness of Nodes *}
    2.37 +
    2.38 +
    2.39 +consts set_of:: "'a tree \<Rightarrow> 'a set"
    2.40 +primrec 
    2.41 +"set_of Tip = {}"
    2.42 +"set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"
    2.43 +
    2.44 +consts all_distinct:: "'a tree \<Rightarrow> bool"
    2.45 +primrec
    2.46 +"all_distinct Tip = True"
    2.47 +"all_distinct (Node l x d r) = ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> 
    2.48 +                               set_of l \<inter> set_of r = {} \<and>
    2.49 +                               all_distinct l \<and> all_distinct r)"
    2.50 +
    2.51 +text {* Given a binary tree @{term "t"} for which 
    2.52 +@{const all_distinct} holds, given two different nodes contained in the tree,
    2.53 +we want to write a ML function that generates a logarithmic
    2.54 +certificate that the content of the nodes is distinct. We use the
    2.55 +following lemmas to achieve this.  *} 
    2.56 +
    2.57 +lemma all_distinct_left:
    2.58 +"all_distinct (Node l x b r) \<Longrightarrow> all_distinct l"
    2.59 +  by simp
    2.60 +
    2.61 +lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r"
    2.62 +  by simp
    2.63 +
    2.64 +lemma distinct_left: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of l \<rbrakk> \<Longrightarrow> x\<noteq>y"
    2.65 +  by auto
    2.66 +
    2.67 +lemma distinct_right: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of r \<rbrakk> \<Longrightarrow> x\<noteq>y"
    2.68 +  by auto
    2.69 +
    2.70 +lemma distinct_left_right: "\<lbrakk>all_distinct (Node l z b r); x \<in> set_of l; y \<in> set_of r\<rbrakk>
    2.71 +  \<Longrightarrow> x\<noteq>y"
    2.72 +  by auto
    2.73 +
    2.74 +lemma in_set_root: "x \<in> set_of (Node l x False r)"
    2.75 +  by simp
    2.76 +
    2.77 +lemma in_set_left: "y \<in> set_of l \<Longrightarrow>  y \<in> set_of (Node l x False r)"
    2.78 +  by simp
    2.79 +
    2.80 +lemma in_set_right: "y \<in> set_of r \<Longrightarrow>  y \<in> set_of (Node l x False r)"
    2.81 +  by simp
    2.82 +
    2.83 +lemma swap_neq: "x \<noteq> y \<Longrightarrow> y \<noteq> x"
    2.84 +  by blast
    2.85 +
    2.86 +lemma neq_to_eq_False: "x\<noteq>y \<Longrightarrow> (x=y)\<equiv>False"
    2.87 +  by simp
    2.88 +
    2.89 +subsection {* Containment of Trees *}
    2.90 +
    2.91 +text {* When deriving a state space from other ones, we create a new
    2.92 +name tree which contains all the names of the parent state spaces and
    2.93 +assumme the predicate @{const all_distinct}. We then prove that the new locale
    2.94 +interprets all parent locales. Hence we have to show that the new
    2.95 +distinctness assumption on all names implies the distinctness
    2.96 +assumptions of the parent locales. This proof is implemented in ML. We
    2.97 +do this efficiently by defining a kind of containment check of trees
    2.98 +by 'subtraction'.  We subtract the parent tree from the new tree. If this
    2.99 +succeeds we know that @{const all_distinct} of the new tree implies
   2.100 +@{const all_distinct} of the parent tree.  The resulting certificate is
   2.101 +of the order @{term "n * log(m)"} where @{term "n"} is the size of the
   2.102 +(smaller) parent tree and @{term "m"} the size of the (bigger) new tree.
   2.103 +*}
   2.104 +
   2.105 +
   2.106 +consts "delete" :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
   2.107 +primrec
   2.108 +"delete x Tip = None"
   2.109 +"delete x (Node l y d r) = (case delete x l of
   2.110 +                              Some l' \<Rightarrow>
   2.111 +                               (case delete x r of 
   2.112 +                                  Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')
   2.113 +                                | None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))
   2.114 +                             | None \<Rightarrow>
   2.115 +                                (case (delete x r) of 
   2.116 +                                   Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')
   2.117 +                                 | None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)
   2.118 +                                           else None))"
   2.119 +
   2.120 +
   2.121 +lemma delete_Some_set_of: "\<And>t'. delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t"
   2.122 +proof (induct t)
   2.123 +  case Tip thus ?case by simp
   2.124 +next
   2.125 +  case (Node l y d r)
   2.126 +  have del: "delete x (Node l y d r) = Some t'".
   2.127 +  show ?case
   2.128 +  proof (cases "delete x l")
   2.129 +    case (Some l')
   2.130 +    note x_l_Some = this
   2.131 +    with Node.hyps
   2.132 +    have l'_l: "set_of l' \<subseteq> set_of l"
   2.133 +      by simp
   2.134 +    show ?thesis
   2.135 +    proof (cases "delete x r")
   2.136 +      case (Some r')
   2.137 +      with Node.hyps
   2.138 +      have "set_of r' \<subseteq> set_of r"
   2.139 +	by simp
   2.140 +      with l'_l Some x_l_Some del
   2.141 +      show ?thesis
   2.142 +	by (auto split: split_if_asm)
   2.143 +    next
   2.144 +      case None
   2.145 +      with l'_l Some x_l_Some del
   2.146 +      show ?thesis
   2.147 +	by (fastsimp split: split_if_asm)
   2.148 +    qed
   2.149 +  next
   2.150 +    case None
   2.151 +    note x_l_None = this
   2.152 +    show ?thesis
   2.153 +    proof (cases "delete x r")
   2.154 +      case (Some r')
   2.155 +      with Node.hyps
   2.156 +      have "set_of r' \<subseteq> set_of r"
   2.157 +	by simp
   2.158 +      with Some x_l_None del
   2.159 +      show ?thesis
   2.160 +	by (fastsimp split: split_if_asm)
   2.161 +    next
   2.162 +      case None
   2.163 +      with x_l_None del
   2.164 +      show ?thesis
   2.165 +	by (fastsimp split: split_if_asm)
   2.166 +    qed
   2.167 +  qed
   2.168 +qed
   2.169 +
   2.170 +lemma delete_Some_all_distinct: 
   2.171 +"\<And>t'. \<lbrakk>delete x t = Some t'; all_distinct t\<rbrakk> \<Longrightarrow> all_distinct t'"
   2.172 +proof (induct t)
   2.173 +  case Tip thus ?case by simp
   2.174 +next
   2.175 +  case (Node l y d r)
   2.176 +  have del: "delete x (Node l y d r) = Some t'".
   2.177 +  have "all_distinct (Node l y d r)".
   2.178 +  then obtain
   2.179 +    dist_l: "all_distinct l" and
   2.180 +    dist_r: "all_distinct r" and
   2.181 +    d: "d \<or> (y \<notin> set_of l \<and> y \<notin> set_of r)" and
   2.182 +    dist_l_r: "set_of l \<inter> set_of r = {}"
   2.183 +    by auto
   2.184 +  show ?case
   2.185 +  proof (cases "delete x l")
   2.186 +    case (Some l')
   2.187 +    note x_l_Some = this
   2.188 +    from Node.hyps (1) [OF Some dist_l]
   2.189 +    have dist_l': "all_distinct l'"
   2.190 +      by simp
   2.191 +    from delete_Some_set_of [OF x_l_Some]
   2.192 +    have l'_l: "set_of l' \<subseteq> set_of l".
   2.193 +    show ?thesis
   2.194 +    proof (cases "delete x r")
   2.195 +      case (Some r')
   2.196 +      from Node.hyps (2) [OF Some dist_r]
   2.197 +      have dist_r': "all_distinct r'"
   2.198 +	by simp
   2.199 +      from delete_Some_set_of [OF Some]
   2.200 +      have "set_of r' \<subseteq> set_of r".
   2.201 +      
   2.202 +      with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r
   2.203 +      show ?thesis
   2.204 +	by fastsimp
   2.205 +    next
   2.206 +      case None
   2.207 +      with l'_l dist_l'  x_l_Some del d dist_l_r dist_r
   2.208 +      show ?thesis
   2.209 +	by fastsimp
   2.210 +    qed
   2.211 +  next
   2.212 +    case None
   2.213 +    note x_l_None = this
   2.214 +    show ?thesis
   2.215 +    proof (cases "delete x r")
   2.216 +      case (Some r')
   2.217 +      with Node.hyps (2) [OF Some dist_r]
   2.218 +      have dist_r': "all_distinct r'"
   2.219 +	by simp
   2.220 +      from delete_Some_set_of [OF Some]
   2.221 +      have "set_of r' \<subseteq> set_of r".
   2.222 +      with Some dist_r' x_l_None del dist_l d dist_l_r
   2.223 +      show ?thesis
   2.224 +	by fastsimp
   2.225 +    next
   2.226 +      case None
   2.227 +      with x_l_None del dist_l dist_r d dist_l_r
   2.228 +      show ?thesis
   2.229 +	by (fastsimp split: split_if_asm)
   2.230 +    qed
   2.231 +  qed
   2.232 +qed
   2.233 +
   2.234 +lemma delete_None_set_of_conv: "delete x t = None = (x \<notin> set_of t)"
   2.235 +proof (induct t)
   2.236 +  case Tip thus ?case by simp
   2.237 +next
   2.238 +  case (Node l y d r)
   2.239 +  thus ?case
   2.240 +    by (auto split: option.splits)
   2.241 +qed
   2.242 +
   2.243 +lemma delete_Some_x_set_of:
   2.244 +  "\<And>t'. delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> set_of t'"
   2.245 +proof (induct t)
   2.246 +  case Tip thus ?case by simp
   2.247 +next
   2.248 +  case (Node l y d r)
   2.249 +  have del: "delete x (Node l y d r) = Some t'".
   2.250 +  show ?case
   2.251 +  proof (cases "delete x l")
   2.252 +    case (Some l')
   2.253 +    note x_l_Some = this
   2.254 +    from Node.hyps (1) [OF Some]
   2.255 +    obtain x_l: "x \<in> set_of l" "x \<notin> set_of l'"
   2.256 +      by simp
   2.257 +    show ?thesis
   2.258 +    proof (cases "delete x r")
   2.259 +      case (Some r')
   2.260 +      from Node.hyps (2) [OF Some]
   2.261 +      obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"
   2.262 +	by simp
   2.263 +      from x_r x_l Some x_l_Some del 
   2.264 +      show ?thesis
   2.265 +	by (clarsimp split: split_if_asm)
   2.266 +    next
   2.267 +      case None
   2.268 +      then have "x \<notin> set_of r"
   2.269 +	by (simp add: delete_None_set_of_conv)
   2.270 +      with x_l None x_l_Some del
   2.271 +      show ?thesis
   2.272 +	by (clarsimp split: split_if_asm)
   2.273 +    qed
   2.274 +  next
   2.275 +    case None
   2.276 +    note x_l_None = this
   2.277 +    then have x_notin_l: "x \<notin> set_of l"
   2.278 +      by (simp add: delete_None_set_of_conv)
   2.279 +    show ?thesis
   2.280 +    proof (cases "delete x r")
   2.281 +      case (Some r')
   2.282 +      from Node.hyps (2) [OF Some]
   2.283 +      obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"
   2.284 +	by simp
   2.285 +      from x_r x_notin_l Some x_l_None del 
   2.286 +      show ?thesis
   2.287 +	by (clarsimp split: split_if_asm)
   2.288 +    next
   2.289 +      case None
   2.290 +      then have "x \<notin> set_of r"
   2.291 +	by (simp add: delete_None_set_of_conv)
   2.292 +      with None x_l_None x_notin_l del
   2.293 +      show ?thesis
   2.294 +	by (clarsimp split: split_if_asm)
   2.295 +    qed
   2.296 +  qed
   2.297 +qed
   2.298 +
   2.299 +
   2.300 +consts "subtract" :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
   2.301 +primrec
   2.302 +"subtract Tip t = Some t"
   2.303 +"subtract (Node l x b r) t = 
   2.304 +   (case delete x t of
   2.305 +      Some t' \<Rightarrow> (case subtract l t' of 
   2.306 +                   Some t'' \<Rightarrow> subtract r t''
   2.307 +                  | None \<Rightarrow> None)
   2.308 +    | None \<Rightarrow> None)"
   2.309 +
   2.310 +lemma subtract_Some_set_of_res: 
   2.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"
   2.312 +proof (induct t\<^isub>1)
   2.313 +  case Tip thus ?case by simp
   2.314 +next
   2.315 +  case (Node l x b r)
   2.316 +  have sub: "subtract (Node l x b r) t\<^isub>2 = Some t".
   2.317 +  show ?case
   2.318 +  proof (cases "delete x t\<^isub>2")
   2.319 +    case (Some t\<^isub>2')
   2.320 +    note del_x_Some = this
   2.321 +    from delete_Some_set_of [OF Some] 
   2.322 +    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
   2.323 +    show ?thesis
   2.324 +    proof (cases "subtract l t\<^isub>2'")
   2.325 +      case (Some t\<^isub>2'')
   2.326 +      note sub_l_Some = this
   2.327 +      from Node.hyps (1) [OF Some] 
   2.328 +      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
   2.329 +      show ?thesis
   2.330 +      proof (cases "subtract r t\<^isub>2''")
   2.331 +	case (Some t\<^isub>2''')
   2.332 +	from Node.hyps (2) [OF Some ] 
   2.333 +	have "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''" .
   2.334 +	with Some sub_l_Some del_x_Some sub t2''_t2' t2'_t2
   2.335 +	show ?thesis
   2.336 +	  by simp
   2.337 +      next
   2.338 +	case None
   2.339 +	with del_x_Some sub_l_Some sub
   2.340 +	show ?thesis
   2.341 +	  by simp
   2.342 +      qed
   2.343 +    next
   2.344 +      case None
   2.345 +      with del_x_Some sub 
   2.346 +      show ?thesis
   2.347 +	by simp
   2.348 +    qed
   2.349 +  next
   2.350 +    case None
   2.351 +    with sub show ?thesis by simp
   2.352 +  qed
   2.353 +qed
   2.354 +
   2.355 +lemma subtract_Some_set_of: 
   2.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"
   2.357 +proof (induct t\<^isub>1)
   2.358 +  case Tip thus ?case by simp
   2.359 +next
   2.360 +  case (Node l x d r)
   2.361 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
   2.362 +  show ?case
   2.363 +  proof (cases "delete x t\<^isub>2")
   2.364 +    case (Some t\<^isub>2')
   2.365 +    note del_x_Some = this
   2.366 +    from delete_Some_set_of [OF Some] 
   2.367 +    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
   2.368 +    from delete_None_set_of_conv [of x t\<^isub>2] Some
   2.369 +    have x_t2: "x \<in> set_of t\<^isub>2"
   2.370 +      by simp
   2.371 +    show ?thesis
   2.372 +    proof (cases "subtract l t\<^isub>2'")
   2.373 +      case (Some t\<^isub>2'')
   2.374 +      note sub_l_Some = this
   2.375 +      from Node.hyps (1) [OF Some] 
   2.376 +      have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" .
   2.377 +      from subtract_Some_set_of_res [OF Some]
   2.378 +      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
   2.379 +      show ?thesis
   2.380 +      proof (cases "subtract r t\<^isub>2''")
   2.381 +	case (Some t\<^isub>2''')
   2.382 +	from Node.hyps (2) [OF Some ] 
   2.383 +	have r_t\<^isub>2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
   2.384 +	from Some sub_l_Some del_x_Some sub r_t\<^isub>2'' l_t2' t2'_t2 t2''_t2' x_t2
   2.385 +	show ?thesis
   2.386 +	  by auto
   2.387 +      next
   2.388 +	case None
   2.389 +	with del_x_Some sub_l_Some sub
   2.390 +	show ?thesis
   2.391 +	  by simp
   2.392 +      qed
   2.393 +    next
   2.394 +      case None
   2.395 +      with del_x_Some sub 
   2.396 +      show ?thesis
   2.397 +	by simp
   2.398 +    qed
   2.399 +  next
   2.400 +    case None
   2.401 +    with sub show ?thesis by simp
   2.402 +  qed
   2.403 +qed
   2.404 +
   2.405 +lemma subtract_Some_all_distinct_res: 
   2.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"
   2.407 +proof (induct t\<^isub>1)
   2.408 +  case Tip thus ?case by simp
   2.409 +next
   2.410 +  case (Node l x d r)
   2.411 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
   2.412 +  have dist_t2: "all_distinct t\<^isub>2".
   2.413 +  show ?case
   2.414 +  proof (cases "delete x t\<^isub>2")
   2.415 +    case (Some t\<^isub>2')
   2.416 +    note del_x_Some = this
   2.417 +    from delete_Some_all_distinct [OF Some dist_t2] 
   2.418 +    have dist_t2': "all_distinct t\<^isub>2'" .
   2.419 +    show ?thesis
   2.420 +    proof (cases "subtract l t\<^isub>2'")
   2.421 +      case (Some t\<^isub>2'')
   2.422 +      note sub_l_Some = this
   2.423 +      from Node.hyps (1) [OF Some dist_t2'] 
   2.424 +      have dist_t2'': "all_distinct t\<^isub>2''" .
   2.425 +      show ?thesis
   2.426 +      proof (cases "subtract r t\<^isub>2''")
   2.427 +	case (Some t\<^isub>2''')
   2.428 +	from Node.hyps (2) [OF Some dist_t2''] 
   2.429 +	have dist_t2''': "all_distinct t\<^isub>2'''" .
   2.430 +	from Some sub_l_Some del_x_Some sub 
   2.431 +             dist_t2'''
   2.432 +	show ?thesis
   2.433 +	  by simp
   2.434 +      next
   2.435 +	case None
   2.436 +	with del_x_Some sub_l_Some sub
   2.437 +	show ?thesis
   2.438 +	  by simp
   2.439 +      qed
   2.440 +    next
   2.441 +      case None
   2.442 +      with del_x_Some sub 
   2.443 +      show ?thesis
   2.444 +	by simp
   2.445 +    qed
   2.446 +  next
   2.447 +    case None
   2.448 +    with sub show ?thesis by simp
   2.449 +  qed
   2.450 +qed
   2.451 +
   2.452 +
   2.453 +lemma subtract_Some_dist_res: 
   2.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 = {}"
   2.455 +proof (induct t\<^isub>1)
   2.456 +  case Tip thus ?case by simp
   2.457 +next
   2.458 +  case (Node l x d r)
   2.459 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
   2.460 +  show ?case
   2.461 +  proof (cases "delete x t\<^isub>2")
   2.462 +    case (Some t\<^isub>2')
   2.463 +    note del_x_Some = this
   2.464 +    from delete_Some_x_set_of [OF Some]
   2.465 +    obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'"
   2.466 +      by simp
   2.467 +    from delete_Some_set_of [OF Some]
   2.468 +    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
   2.469 +    show ?thesis
   2.470 +    proof (cases "subtract l t\<^isub>2'")
   2.471 +      case (Some t\<^isub>2'')
   2.472 +      note sub_l_Some = this
   2.473 +      from Node.hyps (1) [OF Some ] 
   2.474 +      have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}".
   2.475 +      from subtract_Some_set_of_res [OF Some]
   2.476 +      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
   2.477 +      show ?thesis
   2.478 +      proof (cases "subtract r t\<^isub>2''")
   2.479 +	case (Some t\<^isub>2''')
   2.480 +	from Node.hyps (2) [OF Some] 
   2.481 +	have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}" .
   2.482 +	from subtract_Some_set_of_res [OF Some]
   2.483 +	have t2'''_t2'': "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''".
   2.484 +	
   2.485 +	from Some sub_l_Some del_x_Some sub t2'''_t2'' dist_l_t2'' dist_r_t2'''
   2.486 +             t2''_t2' t2'_t2 x_not_t2'
   2.487 +	show ?thesis
   2.488 +	  by auto
   2.489 +      next
   2.490 +	case None
   2.491 +	with del_x_Some sub_l_Some sub
   2.492 +	show ?thesis
   2.493 +	  by simp
   2.494 +      qed
   2.495 +    next
   2.496 +      case None
   2.497 +      with del_x_Some sub 
   2.498 +      show ?thesis
   2.499 +	by simp
   2.500 +    qed
   2.501 +  next
   2.502 +    case None
   2.503 +    with sub show ?thesis by simp
   2.504 +  qed
   2.505 +qed
   2.506 +	
   2.507 +lemma subtract_Some_all_distinct:
   2.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"
   2.509 +proof (induct t\<^isub>1)
   2.510 +  case Tip thus ?case by simp
   2.511 +next
   2.512 +  case (Node l x d r)
   2.513 +  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
   2.514 +  have dist_t2: "all_distinct t\<^isub>2".
   2.515 +  show ?case
   2.516 +  proof (cases "delete x t\<^isub>2")
   2.517 +    case (Some t\<^isub>2')
   2.518 +    note del_x_Some = this
   2.519 +    from delete_Some_all_distinct [OF Some dist_t2 ] 
   2.520 +    have dist_t2': "all_distinct t\<^isub>2'" .
   2.521 +    from delete_Some_set_of [OF Some]
   2.522 +    have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .
   2.523 +    from delete_Some_x_set_of [OF Some]
   2.524 +    obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'"
   2.525 +      by simp
   2.526 +
   2.527 +    show ?thesis
   2.528 +    proof (cases "subtract l t\<^isub>2'")
   2.529 +      case (Some t\<^isub>2'')
   2.530 +      note sub_l_Some = this
   2.531 +      from Node.hyps (1) [OF Some dist_t2' ] 
   2.532 +      have dist_l: "all_distinct l" .
   2.533 +      from subtract_Some_all_distinct_res [OF Some dist_t2'] 
   2.534 +      have dist_t2'': "all_distinct t\<^isub>2''" .
   2.535 +      from subtract_Some_set_of [OF Some]
   2.536 +      have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" .
   2.537 +      from subtract_Some_set_of_res [OF Some]
   2.538 +      have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .
   2.539 +      from subtract_Some_dist_res [OF Some]
   2.540 +      have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}".
   2.541 +      show ?thesis
   2.542 +      proof (cases "subtract r t\<^isub>2''")
   2.543 +	case (Some t\<^isub>2''')
   2.544 +	from Node.hyps (2) [OF Some dist_t2''] 
   2.545 +	have dist_r: "all_distinct r" .
   2.546 +	from subtract_Some_set_of [OF Some]
   2.547 +	have r_t2'': "set_of r \<subseteq> set_of t\<^isub>2''" .
   2.548 +	from subtract_Some_dist_res [OF Some]
   2.549 +	have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}".
   2.550 +
   2.551 +	from dist_l dist_r Some sub_l_Some del_x_Some r_t2'' l_t2' x_t2 x_not_t2' 
   2.552 +	     t2''_t2' dist_l_t2'' dist_r_t2'''
   2.553 +	show ?thesis
   2.554 +	  by auto
   2.555 +      next
   2.556 +	case None
   2.557 +	with del_x_Some sub_l_Some sub
   2.558 +	show ?thesis
   2.559 +	  by simp
   2.560 +      qed
   2.561 +    next
   2.562 +      case None
   2.563 +      with del_x_Some sub 
   2.564 +      show ?thesis
   2.565 +	by simp
   2.566 +    qed
   2.567 +  next
   2.568 +    case None
   2.569 +    with sub show ?thesis by simp
   2.570 +  qed
   2.571 +qed
   2.572 +
   2.573 +
   2.574 +lemma delete_left:
   2.575 +  assumes dist: "all_distinct (Node l y d r)" 
   2.576 +  assumes del_l: "delete x l = Some l'"
   2.577 +  shows "delete x (Node l y d r) = Some (Node l' y d r)"
   2.578 +proof -
   2.579 +  from delete_Some_x_set_of [OF del_l]
   2.580 +  obtain "x \<in> set_of l"
   2.581 +    by simp
   2.582 +  moreover with dist 
   2.583 +  have "delete x r = None"
   2.584 +    by (cases "delete x r") (auto dest:delete_Some_x_set_of)
   2.585 +
   2.586 +  ultimately 
   2.587 +  show ?thesis
   2.588 +    using del_l dist
   2.589 +    by (auto split: option.splits)
   2.590 +qed
   2.591 +
   2.592 +lemma delete_right:
   2.593 +  assumes dist: "all_distinct (Node l y d r)" 
   2.594 +  assumes del_r: "delete x r = Some r'"
   2.595 +  shows "delete x (Node l y d r) = Some (Node l y d r')"
   2.596 +proof -
   2.597 +  from delete_Some_x_set_of [OF del_r]
   2.598 +  obtain "x \<in> set_of r"
   2.599 +    by simp
   2.600 +  moreover with dist 
   2.601 +  have "delete x l = None"
   2.602 +    by (cases "delete x l") (auto dest:delete_Some_x_set_of)
   2.603 +
   2.604 +  ultimately 
   2.605 +  show ?thesis
   2.606 +    using del_r dist
   2.607 +    by (auto split: option.splits)
   2.608 +qed
   2.609 +
   2.610 +lemma delete_root: 
   2.611 +  assumes dist: "all_distinct (Node l x False r)" 
   2.612 +  shows "delete x (Node l x False r) = Some (Node l x True r)"
   2.613 +proof -
   2.614 +  from dist have "delete x r = None"
   2.615 +    by (cases "delete x r") (auto dest:delete_Some_x_set_of)
   2.616 +  moreover
   2.617 +  from dist have "delete x l = None"
   2.618 +    by (cases "delete x l") (auto dest:delete_Some_x_set_of)
   2.619 +  ultimately show ?thesis
   2.620 +    using dist
   2.621 +       by (auto split: option.splits)
   2.622 +qed               
   2.623 +
   2.624 +lemma subtract_Node:
   2.625 + assumes del: "delete x t = Some t'"                                
   2.626 + assumes sub_l: "subtract l t' = Some t''"
   2.627 + assumes sub_r: "subtract r t'' = Some t'''"
   2.628 + shows "subtract (Node l x False r) t = Some t'''"
   2.629 +using del sub_l sub_r
   2.630 +by simp
   2.631 +
   2.632 +lemma subtract_Tip: "subtract Tip t = Some t"
   2.633 +  by simp
   2.634 + 
   2.635 +text {* Now we have all the theorems in place that are needed for the
   2.636 +certificate generating ML functions. *}
   2.637 +
   2.638 +use distinct_tree_prover
   2.639 +
   2.640 +(* Uncomment for profiling or debugging *)
   2.641 +(*
   2.642 +ML {*
   2.643 +(*
   2.644 +val nums = (0 upto 10000);
   2.645 +val nums' = (200 upto 3000);
   2.646 +*)
   2.647 +val nums = (0 upto 10000);
   2.648 +val nums' = (0 upto 3000);
   2.649 +val const_decls = map (fn i => Syntax.no_syn 
   2.650 +                                 ("const" ^ string_of_int i,Type ("nat",[]))) nums
   2.651 +
   2.652 +val consts = sort Term.fast_term_ord 
   2.653 +              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
   2.654 +val consts' = sort Term.fast_term_ord 
   2.655 +              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
   2.656 +
   2.657 +val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts
   2.658 +
   2.659 +
   2.660 +val t' = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts'
   2.661 +
   2.662 +
   2.663 +val dist = 
   2.664 +     HOLogic.Trueprop$
   2.665 +       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t)
   2.666 +
   2.667 +val dist' = 
   2.668 +     HOLogic.Trueprop$
   2.669 +       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t')
   2.670 +
   2.671 +val da = ref refl;
   2.672 +
   2.673 +*}
   2.674 +
   2.675 +setup {*
   2.676 +Theory.add_consts_i const_decls
   2.677 +#> (fn thy  => let val ([thm],thy') = PureThy.add_axioms_i [(("dist_axiom",dist),[])] thy
   2.678 +               in (da := thm; thy') end)
   2.679 +*}
   2.680 +
   2.681 +
   2.682 +ML {* 
   2.683 + val ct' = cterm_of (the_context ()) t';
   2.684 +*}
   2.685 +
   2.686 +ML {*
   2.687 + timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);())) 
   2.688 +*}
   2.689 +
   2.690 +(* 590 s *)
   2.691 +
   2.692 +ML {*
   2.693 +
   2.694 +
   2.695 +val p1 = 
   2.696 + the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const1",Type ("nat",[]))) t)
   2.697 +val p2 =
   2.698 + the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const10000",Type ("nat",[]))) t)
   2.699 +*}
   2.700 +
   2.701 +
   2.702 +ML {* timeit (fn () => DistinctTreeProver.distinctTreeProver (!da )
   2.703 +       p1
   2.704 +       p2)*}
   2.705 +
   2.706 +
   2.707 +ML {* timeit (fn () => (DistinctTreeProver.deleteProver (!da) p1;())) *}
   2.708 +
   2.709 +
   2.710 +
   2.711 +
   2.712 +ML {*
   2.713 +val cdist' = cterm_of (the_context ()) dist';
   2.714 +DistinctTreeProver.distinct_implProver (!da) cdist';
   2.715 +*}
   2.716 +
   2.717 +*)
   2.718 +
   2.719 +
   2.720 +
   2.721 +
   2.722 +
   2.723 +
   2.724 +
   2.725 +
   2.726 +
   2.727 +
   2.728 +end
   2.729 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Statespace/ROOT.ML	Wed Oct 24 18:36:09 2007 +0200
     3.3 @@ -0,0 +1,1 @@
     3.4 +use_thy "StateSpaceEx";
     3.5 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Statespace/StateFun.thy	Wed Oct 24 18:36:09 2007 +0200
     4.3 @@ -0,0 +1,115 @@
     4.4 +(*  Title:      StateFun.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Norbert Schirmer, TU Muenchen
     4.7 +*)
     4.8 +
     4.9 +header {* State Space Representation as Function \label{sec:StateFun}*}
    4.10 +
    4.11 +theory StateFun imports DistinctTreeProver 
    4.12 +(*uses "state_space.ML" (state_fun)*)
    4.13 +begin
    4.14 +
    4.15 +
    4.16 +text {* The state space is represented as a function from names to
    4.17 +values. We neither fix the type of names nor the type of values. We
    4.18 +define lookup and update functions and provide simprocs that simplify
    4.19 +expressions containing these, similar to HOL-records.
    4.20 +
    4.21 +The lookup and update function get constructor/destructor functions as
    4.22 +parameters. These are used to embed various HOL-types into the
    4.23 +abstract value type. Conceptually the abstract value type is a sum of
    4.24 +all types that we attempt to store in the state space.
    4.25 +
    4.26 +The update is actually generalized to a map function. The map supplies
    4.27 +better compositionality, especially if you think of nested state
    4.28 +spaces.  *} 
    4.29 +
    4.30 +constdefs K_statefun:: "'a \<Rightarrow> 'b \<Rightarrow> 'a" "K_statefun c x \<equiv> c"
    4.31 +
    4.32 +lemma K_statefun_apply [simp]: "K_statefun c x = c"
    4.33 +  by (simp add: K_statefun_def)
    4.34 +
    4.35 +lemma K_statefun_comp [simp]: "(K_statefun c \<circ> f) = K_statefun c"
    4.36 +  by (rule ext) (simp add: K_statefun_apply comp_def)
    4.37 +
    4.38 +lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
    4.39 +  by (rule refl)
    4.40 +
    4.41 +constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
    4.42 +"lookup destr n s \<equiv> destr (s n)"
    4.43 +
    4.44 +constdefs update:: 
    4.45 +  "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
    4.46 +"update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
    4.47 +
    4.48 +lemma lookup_update_same:
    4.49 +  "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) = 
    4.50 +         f (destr (s n))"  
    4.51 +  by (simp add: lookup_def update_def)
    4.52 +
    4.53 +lemma lookup_update_id_same:
    4.54 +  "lookup destr n (update destr' id n (K_statefun (lookup id n s')) s) =                  
    4.55 +     lookup destr n s'"  
    4.56 +  by (simp add: lookup_def update_def)
    4.57 +
    4.58 +lemma lookup_update_other:
    4.59 +  "n\<noteq>m \<Longrightarrow> lookup destr n (update destr' constr m f s) = lookup destr n s"  
    4.60 +  by (simp add: lookup_def update_def)
    4.61 +
    4.62 +
    4.63 +lemma id_id_cancel: "id (id x) = x" 
    4.64 +  by (simp add: id_def)
    4.65 +  
    4.66 +lemma destr_contstr_comp_id:
    4.67 +"(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id"
    4.68 +  by (rule ext) simp
    4.69 +
    4.70 +
    4.71 +
    4.72 +lemma block_conj_cong: "(P \<and> Q) = (P \<and> Q)"
    4.73 +  by simp
    4.74 +
    4.75 +lemma conj1_False: "(P\<equiv>False) \<Longrightarrow> (P \<and> Q) \<equiv> False"
    4.76 +  by simp
    4.77 +
    4.78 +lemma conj2_False: "\<lbrakk>Q\<equiv>False\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> False"
    4.79 +  by simp
    4.80 +
    4.81 +lemma conj_True: "\<lbrakk>P\<equiv>True; Q\<equiv>True\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> True"
    4.82 +  by simp
    4.83 +
    4.84 +lemma conj_cong: "\<lbrakk>P\<equiv>P'; Q\<equiv>Q'\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> Q')"
    4.85 +  by simp
    4.86 +
    4.87 +
    4.88 +lemma update_apply: "(update destr constr n f s x) = 
    4.89 +     (if x=n then constr (f (destr (s n))) else s x)"
    4.90 +  by (simp add: update_def)
    4.91 +
    4.92 +lemma ex_id: "\<exists>x. id x = y"
    4.93 +  by (simp add: id_def)
    4.94 +
    4.95 +lemma swap_ex_eq: 
    4.96 +  "\<exists>s. f s = x \<equiv> True \<Longrightarrow>
    4.97 +   \<exists>s. x = f s \<equiv> True"
    4.98 +  apply (rule eq_reflection)
    4.99 +  apply auto
   4.100 +  done
   4.101 +
   4.102 +lemmas meta_ext = eq_reflection [OF ext]
   4.103 +
   4.104 +(* This lemma only works if the store is welltyped:
   4.105 +    "\<exists>x.  s ''n'' = (c x)" 
   4.106 +   or in general when c (d x) = x,
   4.107 +     (for example: c=id and d=id)
   4.108 + *)
   4.109 +lemma "update d c n (K_statespace (lookup d n s)) s = s"
   4.110 +  apply (simp add: update_def lookup_def)
   4.111 +  apply (rule ext)
   4.112 +  apply simp
   4.113 +  oops
   4.114 +
   4.115 +(*use "state_fun"
   4.116 +setup StateFun.setup
   4.117 +*)
   4.118 +end
   4.119 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Wed Oct 24 18:36:09 2007 +0200
     5.3 @@ -0,0 +1,221 @@
     5.4 +(*  Title:      StateSpaceEx.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Norbert Schirmer, TU Muenchen
     5.7 +*)
     5.8 +
     5.9 +header {* Examples \label{sec:Examples} *}
    5.10 +theory StateSpaceEx
    5.11 +imports StateSpaceLocale StateSpaceSyntax
    5.12 +
    5.13 +begin
    5.14 +(* FIXME: Use proper keywords file *)
    5.15 +(*<*)
    5.16 +syntax
    5.17 + "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [900,0] 900)
    5.18 +(*>*)
    5.19 +
    5.20 +text {* Did you ever dream about records with multiple inheritance.
    5.21 +Then you should definitely have a look at statespaces. They may be
    5.22 +what you are dreaming of. Or at least almost...
    5.23 +*}
    5.24 +
    5.25 +
    5.26 +
    5.27 +
    5.28 +text {* Isabelle allows to add new top-level commands to the
    5.29 +system. Building on the locale infrastructure, we provide a command
    5.30 +\isacommand{statespace} like this:*}
    5.31 +
    5.32 +statespace vars =
    5.33 +  n::nat
    5.34 +  b::bool
    5.35 +
    5.36 +text {* \noindent This resembles a \isacommand{record} definition, 
    5.37 +but introduces sophisticated locale
    5.38 +infrastructure instead of HOL type schemes.  The resulting context
    5.39 +postulates two distinct names @{term "n"} and @{term "b"} and
    5.40 +projection~/ injection functions that convert from abstract values to
    5.41 +@{typ "nat"} and @{text "bool"}. The logical content of the locale is: *}
    5.42 +
    5.43 +locale vars' =
    5.44 +  fixes n::'name and b::'name
    5.45 +  assumes "distinct [n, b]" 
    5.46 +
    5.47 +  fixes project_nat::"'value \<Rightarrow> nat" and inject_nat::"nat \<Rightarrow> 'value"
    5.48 +  assumes "\<And>n. project_nat (inject_nat n) = n" 
    5.49 +
    5.50 +  fixes project_bool::"'value \<Rightarrow> bool" and inject_bool::"bool \<Rightarrow> 'value"
    5.51 +  assumes "\<And>b. project_bool (inject_bool b) = b"
    5.52 + 
    5.53 +text {* \noindent The HOL predicate @{const "distinct"} describes
    5.54 +distinctness of all names in the context.  Locale @{text "vars'"}
    5.55 +defines the raw logical content that is defined in the state space
    5.56 +locale. We also maintain non-logical context information to support
    5.57 +the user:
    5.58 +
    5.59 +\begin{itemize}
    5.60 +
    5.61 +\item Syntax for state lookup and updates that automatically inserts
    5.62 +the corresponding projection and injection functions.
    5.63 +
    5.64 +\item Setup for the proof tools that exploit the distinctness
    5.65 +information and the cancellation of projections and injections in
    5.66 +deductions and simplifications.
    5.67 +
    5.68 +\end{itemize}
    5.69 +
    5.70 +This extra-logical information is added to the locale in form of
    5.71 +declarations, which associate the name of a variable to the
    5.72 +corresponding projection and injection functions to handle the syntax
    5.73 +transformations, and a link from the variable name to the
    5.74 +corresponding distinctness theorem. As state spaces are merged or
    5.75 +extended there are multiple distinctness theorems in the context. Our
    5.76 +declarations take care that the link always points to the strongest
    5.77 +distinctness assumption.  With these declarations in place, a lookup
    5.78 +can be written as @{text "s\<cdot>n"}, which is translated to @{text
    5.79 +"project_nat (s n)"}, and an update as @{text "s\<langle>n := 2\<rangle>"}, which is
    5.80 +translated to @{text "s(n := inject_nat 2)"}. We can now establish the
    5.81 +following lemma: *}
    5.82 +
    5.83 +lemma (in vars) foo: "s<n := 2>\<cdot>b = s\<cdot>b" by simp
    5.84 +
    5.85 +text {* \noindent Here the simplifier was able to refer to
    5.86 +distinctness of @{term "b"} and @{term "n"} to solve the equation.
    5.87 +The resulting lemma is also recorded in locale @{text "vars"} for
    5.88 +later use and is automatically propagated to all its interpretations.
    5.89 +Here is another example: *}
    5.90 +
    5.91 +statespace 'a varsX = vars [n=N, b=B] + vars + x::'a
    5.92 +
    5.93 +text {* \noindent The state space @{text "varsX"} imports two copies
    5.94 +of the state space @{text "vars"}, where one has the variables renamed
    5.95 +to upper-case letters, and adds another variable @{term "x"} of type
    5.96 +@{typ "'a"}. This type is fixed inside the state space but may get
    5.97 +instantiated later on, analogous to type parameters of an ML-functor.
    5.98 +The distinctness assumption is now @{text "distinct [N, B, n, b, x]"},
    5.99 +from this we can derive both @{term "distinct [N,B]"} and @{term
   5.100 +"distinct [n,b]"}, the distinction assumptions for the two versions of
   5.101 +locale @{text "vars"} above.  Moreover we have all necessary
   5.102 +projection and injection assumptions available. These assumptions
   5.103 +together allow us to establish state space @{term "varsX"} as an
   5.104 +interpretation of both instances of locale @{term "vars"}. Hence we
   5.105 +inherit both variants of theorem @{text "foo"}: @{text "s\<langle>N := 2\<rangle>\<cdot>B =
   5.106 +s\<cdot>B"} as well as @{text "s\<langle>n := 2\<rangle>\<cdot>b = s\<cdot>b"}. These are immediate
   5.107 +consequences of the locale interpretation action.
   5.108 +
   5.109 +The declarations for syntax and the distinctness theorems also observe
   5.110 +the morphisms generated by the locale package due to the renaming
   5.111 +@{term "n = N"}: *}
   5.112 +
   5.113 +lemma (in varsX) foo: "s\<langle>N := 2\<rangle>\<cdot>x = s\<cdot>x" by simp
   5.114 +
   5.115 +text {* To assure scalability towards many distinct names, the
   5.116 +distinctness predicate is refined to operate on balanced trees. Thus
   5.117 +we get logarithmic certificates for the distinctness of two names by
   5.118 +the distinctness of the paths in the tree. Asked for the distinctness
   5.119 +of two names, our tool produces the paths of the variables in the tree
   5.120 +(this is implemented in SML, outside the logic) and returns a
   5.121 +certificate corresponding to the different paths.  Merging state
   5.122 +spaces requires to prove that the combined distinctness assumption
   5.123 +implies the distinctness assumptions of the components.  Such a proof
   5.124 +is of the order $m \cdot \log n$, where $n$ and $m$ are the number of
   5.125 +nodes in the larger and smaller tree, respectively.*}
   5.126 +
   5.127 +text {* We continue with more examples. *}
   5.128 +
   5.129 +statespace 'a foo = 
   5.130 +  f::"nat\<Rightarrow>nat"
   5.131 +  a::int
   5.132 +  b::nat
   5.133 +  c::'a
   5.134 +
   5.135 +
   5.136 +
   5.137 +lemma (in foo) foo1: 
   5.138 +  shows "s\<langle>a := i\<rangle>\<cdot>a = i"
   5.139 +  by simp
   5.140 +
   5.141 +lemma (in foo) foo2: 
   5.142 +  shows "(s\<langle>a:=i\<rangle>)\<cdot>a = i"
   5.143 +  by simp
   5.144 +
   5.145 +lemma (in foo) foo3: 
   5.146 +  shows "(s\<langle>a:=i\<rangle>)\<cdot>b = s\<cdot>b"
   5.147 +  by simp
   5.148 +
   5.149 +lemma (in foo) foo4: 
   5.150 +  shows "(s\<langle>a:=i,b:=j,c:=k,a:=x\<rangle>) = (s\<langle>b:=j,c:=k,a:=x\<rangle>)"
   5.151 +  by simp
   5.152 +
   5.153 +statespace bar =
   5.154 +  b::bool
   5.155 +  c::string
   5.156 +
   5.157 +lemma (in bar) bar1: 
   5.158 +  shows "(s\<langle>b:=True\<rangle>)\<cdot>c = s\<cdot>c"
   5.159 +  by simp
   5.160 +
   5.161 +text {* You can define a derived state space by inheriting existing state spaces, renaming
   5.162 +of components if you like, and by declaring new components.
   5.163 +*}
   5.164 +
   5.165 +statespace ('a,'b) loo = 'a foo + bar [b=B,c=C] +
   5.166 +  X::'b
   5.167 +
   5.168 +lemma (in loo) loo1: 
   5.169 +  shows "s\<langle>a:=i\<rangle>\<cdot>B = s\<cdot>B"
   5.170 +proof -
   5.171 +  thm foo1
   5.172 +  txt {* The Lemma @{thm [source] foo1} from the parent state space 
   5.173 +         is also available here: \begin{center}@{thm foo1}\end{center}.*}
   5.174 +  have "s<a:=i>\<cdot>a = i"
   5.175 +    by (rule foo1)
   5.176 +  thm bar1
   5.177 +  txt {* Note the renaming of the parameters in Lemma @{thm [source] bar1}: 
   5.178 +         \begin{center}@{thm bar1}\end{center}.*}
   5.179 +  have "s<B:=True>\<cdot>C = s\<cdot>C"
   5.180 +    by (rule bar1)
   5.181 +  show ?thesis
   5.182 +    by simp
   5.183 +qed
   5.184 +
   5.185 +
   5.186 +statespace 'a dup = 'a foo [f=F, a=A] + 'a foo +
   5.187 +  x::int
   5.188 +
   5.189 +lemma (in dup)
   5.190 + shows "s<a := i>\<cdot>x = s\<cdot>x"
   5.191 +  by simp
   5.192 +
   5.193 +lemma (in dup)
   5.194 + shows "s<A := i>\<cdot>a = s\<cdot>a"
   5.195 +  by simp
   5.196 +
   5.197 +lemma (in dup)
   5.198 + shows "s<A := i>\<cdot>x = s\<cdot>x"
   5.199 +  by simp
   5.200 +
   5.201 +
   5.202 +text {* There are known problems with syntax-declarations. They currently
   5.203 +only work, when the context is already built. Hopefully this will be 
   5.204 +implemented correctly in future Isabelle versions. *}
   5.205 +
   5.206 +lemma 
   5.207 + includes foo
   5.208 + shows True
   5.209 +  term "s<a := i>\<cdot>a = i"
   5.210 +  by simp
   5.211 +
   5.212 +(*
   5.213 +lemma 
   5.214 +  includes foo
   5.215 +  shows "s<a := i>\<cdot>a = i"
   5.216 +*)
   5.217 +
   5.218 +text {* It would be nice to have nested state spaces. This is
   5.219 +logically no problem. From the locale-implementation side this may be
   5.220 +something like an 'includes' into a locale. When there is a more
   5.221 +elaborate locale infrastructure in place this may be an easy exercise.
   5.222 +*} 
   5.223 +
   5.224 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Statespace/StateSpaceLocale.thy	Wed Oct 24 18:36:09 2007 +0200
     6.3 @@ -0,0 +1,40 @@
     6.4 +(*  Title:      StateSpaceLocale.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Norbert Schirmer, TU Muenchen
     6.7 +*)
     6.8 +
     6.9 +header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}
    6.10 +
    6.11 +theory StateSpaceLocale imports StateFun 
    6.12 +uses "state_space.ML" "state_fun"
    6.13 +begin
    6.14 +
    6.15 +setup StateFun.setup
    6.16 +
    6.17 +text {* For every type that is to be stored in a state space, an
    6.18 +instance of this locale is imported in order convert the abstract and
    6.19 +concrete values.*}
    6.20 +
    6.21 +
    6.22 +locale project_inject =
    6.23 + fixes project :: "'value \<Rightarrow> 'a"
    6.24 + and   "inject":: "'a \<Rightarrow> 'value"
    6.25 + assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
    6.26 +
    6.27 +lemma (in project_inject)
    6.28 + ex_project [statefun_simp]: "\<exists>v. project v = x"
    6.29 +  apply (rule_tac x= "inject x" in exI)
    6.30 +  apply (simp add: project_inject_cancel)
    6.31 +  done
    6.32 +
    6.33 +lemma (in project_inject)
    6.34 + project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
    6.35 +  by (rule ext) (simp add: project_inject_cancel)
    6.36 +
    6.37 +lemma (in project_inject)
    6.38 + project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
    6.39 +  by (rule ext) (simp add: project_inject_cancel)
    6.40 +
    6.41 +
    6.42 +
    6.43 +end
    6.44 \ No newline at end of file
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Wed Oct 24 18:36:09 2007 +0200
     7.3 @@ -0,0 +1,42 @@
     7.4 +(*  Title:      StateSpaceSyntax.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Norbert Schirmer, TU Muenchen
     7.7 +*)
     7.8 +
     7.9 +header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
    7.10 +theory StateSpaceSyntax
    7.11 +imports StateSpaceLocale
    7.12 +
    7.13 +begin
    7.14 +
    7.15 +text {* The state space syntax is kept in an extra theory so that you
    7.16 +can choose if you want to use it or not.  *}
    7.17 +
    7.18 +syntax 
    7.19 + "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" ("_\<cdot>_" [60,60] 60)
    7.20 + "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
    7.21 + "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900,0] 900)
    7.22 +
    7.23 +translations
    7.24 +  "_statespace_updates f (_updbinds b bs)"  == 
    7.25 +     "_statespace_updates (_statespace_updates f b) bs"
    7.26 +  "s<x:=y>"                     == "_statespace_update s x y"
    7.27 +
    7.28 +
    7.29 +parse_translation (advanced)
    7.30 +{*
    7.31 +[("_statespace_lookup",StateSpace.lookup_tr),
    7.32 + ("_get",StateSpace.lookup_tr),
    7.33 + ("_statespace_update",StateSpace.update_tr)] 
    7.34 +*}
    7.35 +
    7.36 +
    7.37 +print_translation (advanced)
    7.38 +{*
    7.39 +[("lookup",StateSpace.lookup_tr'),
    7.40 + ("StateFun.lookup",StateSpace.lookup_tr'),
    7.41 + ("update",StateSpace.update_tr'),
    7.42 + ("StateFun.update",StateSpace.update_tr')] 
    7.43 +*}
    7.44 +
    7.45 +end
    7.46 \ No newline at end of file
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Oct 24 18:36:09 2007 +0200
     8.3 @@ -0,0 +1,349 @@
     8.4 +(*  Title:      distinct_tree_prover.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     Norbert Schirmer, TU Muenchen
     8.7 +*)
     8.8 +
     8.9 +structure DistinctTreeProver =
    8.10 +struct
    8.11 +val all_distinct_left = thm "DistinctTreeProver.all_distinct_left";
    8.12 +val all_distinct_right = thm "DistinctTreeProver.all_distinct_right";
    8.13 +
    8.14 +val distinct_left = thm "DistinctTreeProver.distinct_left";
    8.15 +val distinct_right = thm "DistinctTreeProver.distinct_right";
    8.16 +val distinct_left_right = thm "DistinctTreeProver.distinct_left_right";
    8.17 +val in_set_root = thm "DistinctTreeProver.in_set_root";
    8.18 +val in_set_left = thm "DistinctTreeProver.in_set_left";
    8.19 +val in_set_right = thm "DistinctTreeProver.in_set_right";
    8.20 +
    8.21 +val swap_neq = thm "DistinctTreeProver.swap_neq";
    8.22 +val neq_to_eq_False = thm "DistinctTreeProver.neq_to_eq_False"
    8.23 +
    8.24 +fun treeT T = Type ("DistinctTreeProver.tree",[T]);
    8.25 +fun mk_tree' e T n []     = Const ("DistinctTreeProver.tree.Tip",treeT T)
    8.26 +  | mk_tree' e T n xs =
    8.27 +     let
    8.28 +       val m = (n - 1) div 2;
    8.29 +       val (xsl,x::xsr) = chop m xs;
    8.30 +       val l = mk_tree' e T m xsl;
    8.31 +       val r = mk_tree' e T (n-(m+1)) xsr;
    8.32 +     in Const ("DistinctTreeProver.tree.Node",
    8.33 +                treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $ 
    8.34 +          l$ e x $ HOLogic.false_const $ r 
    8.35 +     end
    8.36 +
    8.37 +fun mk_tree e T xs = mk_tree' e T (length xs) xs;         
    8.38 +
    8.39 +fun dest_tree (Const ("DistinctTreeProver.tree.Tip",_)) = []
    8.40 +  | dest_tree (Const ("DistinctTreeProver.tree.Node",_)$l$e$_$r) = dest_tree l @ e :: dest_tree r
    8.41 +  | dest_tree t = raise TERM ("DistinctTreeProver.dest_tree",[t]);
    8.42 +
    8.43 +datatype Direction = Left | Right 
    8.44 +
    8.45 +fun lin_find_tree e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
    8.46 +  | lin_find_tree e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
    8.47 +      if e aconv x 
    8.48 +      then SOME []
    8.49 +      else (case lin_find_tree e l of
    8.50 +              SOME path => SOME (Left::path)
    8.51 +            | NONE => (case lin_find_tree e r of
    8.52 +                        SOME path => SOME (Right::path)
    8.53 +                       | NONE => NONE))
    8.54 +  | lin_find_tree e t = raise TERM ("find_tree: input not a tree",[t])
    8.55 +
    8.56 +fun bin_find_tree order e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
    8.57 +  | bin_find_tree order e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
    8.58 +      (case order (e,x) of
    8.59 +         EQUAL => SOME []
    8.60 +       | LESS => Option.map (cons Left) (bin_find_tree order e l)
    8.61 +       | GREATER => Option.map (cons Right) (bin_find_tree order e r))
    8.62 +  | bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t])
    8.63 +
    8.64 +fun find_tree e t =
    8.65 +  (case bin_find_tree Term.fast_term_ord e t of
    8.66 +     NONE => lin_find_tree e t
    8.67 +   | x => x);
    8.68 +
    8.69 + 
    8.70 +fun index_tree (Const ("DistinctTreeProver.tree.Tip",_)) path tab = tab
    8.71 +  | index_tree (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) path tab =
    8.72 +      tab 
    8.73 +      |> Termtab.update_new (x,path) 
    8.74 +      |> index_tree l (path@[Left])
    8.75 +      |> index_tree r (path@[Right])
    8.76 +  | index_tree t _ _ = raise TERM ("index_tree: input not a tree",[t])
    8.77 +
    8.78 +fun split_common_prefix xs [] = ([],xs,[])
    8.79 +  | split_common_prefix [] ys = ([],[],ys)
    8.80 +  | split_common_prefix (xs as (x::xs')) (ys as (y::ys')) =
    8.81 +     if x=y 
    8.82 +     then let val (ps,xs'',ys'') = split_common_prefix xs' ys' in (x::ps,xs'',ys'') end
    8.83 +     else ([],xs,ys)
    8.84 +
    8.85 +
    8.86 +(* Wrapper around Thm.instantiate. The type instiations of instTs are applied to
    8.87 + * the right hand sides of insts
    8.88 + *)
    8.89 +fun instantiate instTs insts =
    8.90 +  let
    8.91 +    val instTs' = map (fn (T,U) => (dest_TVar (typ_of T),typ_of U)) instTs;
    8.92 +    fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T');
    8.93 +    fun mapT_and_recertify ct =
    8.94 +      let
    8.95 +        val thy = theory_of_cterm ct;
    8.96 +      in (cterm_of thy (Term.map_types (Term.map_type_tvar substT) (term_of ct))) end;
    8.97 +    val insts' = map (apfst mapT_and_recertify) insts;
    8.98 +  in Thm.instantiate (instTs,insts') end;
    8.99 +
   8.100 +fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
   8.101 +  quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
   8.102 +  [TVar (ixn, S), TVar (ixn, S')], []);
   8.103 +
   8.104 +fun lookup (tye, (ixn, S)) =
   8.105 +  (case AList.lookup (op =) tye ixn of
   8.106 +    NONE => NONE
   8.107 +  | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
   8.108 +
   8.109 +val naive_typ_match =
   8.110 +  let
   8.111 +    fun match (TVar (v, S), T) subs =
   8.112 +          (case lookup (subs, (v, S)) of
   8.113 +            NONE => ((v, (S, T))::subs)
   8.114 +          | SOME _ => subs)
   8.115 +      | match (Type (a, Ts), Type (b, Us)) subs =
   8.116 +          if a <> b then raise Type.TYPE_MATCH
   8.117 +          else matches (Ts, Us) subs
   8.118 +      | match (TFree x, TFree y) subs =
   8.119 +          if x = y then subs else raise Type.TYPE_MATCH
   8.120 +      | match _ _ = raise Type.TYPE_MATCH
   8.121 +    and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs)
   8.122 +      | matches _ subs = subs;
   8.123 +  in match end;
   8.124 +
   8.125 +
   8.126 +(* expects that relevant type variables are already contained in 
   8.127 + * term variables. First instantiation of variables is returned without further
   8.128 + * checking.
   8.129 + *)
   8.130 +fun naive_cterm_first_order_match (t,ct) env =
   8.131 +  let
   8.132 +    val thy = (theory_of_cterm ct);
   8.133 +    fun mtch (env as (tyinsts,insts)) = fn
   8.134 +         (Var(ixn,T),ct) =>
   8.135 +           (case AList.lookup (op =) insts ixn of
   8.136 +             NONE => (naive_typ_match (T,typ_of (ctyp_of_term ct)) tyinsts,
   8.137 +                      (ixn, ct)::insts)
   8.138 +            | SOME _ => env)
   8.139 +        | (f$t,ct) => let val (cf,ct') = Thm.dest_comb ct;
   8.140 +                      in mtch (mtch env (f,cf)) (t,ct') end
   8.141 +        | _ => env
   8.142 +  in mtch env (t,ct) end;
   8.143 +
   8.144 +
   8.145 +fun mp prem rule = implies_elim rule prem;
   8.146 +
   8.147 +fun discharge prems rule =
   8.148 +  let
   8.149 +     val thy = theory_of_thm (hd prems);
   8.150 +     val (tyinsts,insts) =  
   8.151 +           fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([],[]);
   8.152 +
   8.153 +     val tyinsts' = map (fn (v,(S,U)) => (ctyp_of thy (TVar (v,S)),ctyp_of thy U)) 
   8.154 +                     tyinsts;
   8.155 +     val insts' = map (fn (idxn,ct) => (cterm_of thy (Var (idxn,typ_of (ctyp_of_term ct))),ct))  
   8.156 +                     insts;
   8.157 +     val rule' = Thm.instantiate (tyinsts',insts') rule;
   8.158 +   in fold mp prems rule' end;
   8.159 +
   8.160 +local
   8.161 +
   8.162 +val (l_in_set_root,x_in_set_root,r_in_set_root) =
   8.163 +  let val (Node_l_x_d,r) = (cprop_of in_set_root) 
   8.164 +                         |> Thm.dest_comb |> #2 
   8.165 +                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   8.166 +      val (Node_l,x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
   8.167 +      val l = Node_l |> Thm.dest_comb |> #2;
   8.168 +  in (l,x,r) end
   8.169 +val (x_in_set_left,r_in_set_left) = 
   8.170 +  let val (Node_l_x_d,r) = (cprop_of in_set_left) 
   8.171 +                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   8.172 +                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
   8.173 +      val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
   8.174 +  in (x,r) end
   8.175 +
   8.176 +val (x_in_set_right,l_in_set_right) = 
   8.177 +  let val (Node_l,x) = (cprop_of in_set_right) 
   8.178 +                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
   8.179 +                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
   8.180 +                         |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1 
   8.181 +                         |> Thm.dest_comb
   8.182 +      val l = Node_l |> Thm.dest_comb |> #2;
   8.183 +  in (x,l) end
   8.184 +
   8.185 +in
   8.186 +(*
   8.187 +1. First get paths x_path y_path of x and y in the tree.
   8.188 +2. For the common prefix descend into the tree according to the path
   8.189 +   and lemmas all_distinct_left/right
   8.190 +3. If one restpath is empty use distinct_left/right,
   8.191 +   otherwise all_distinct_left_right
   8.192 +*)
   8.193 +
   8.194 +fun distinctTreeProver dist_thm x_path y_path =
   8.195 +  let
   8.196 +    fun dist_subtree [] thm = thm
   8.197 +      | dist_subtree (p::ps) thm =
   8.198 +         let 
   8.199 +           val rule = (case p of Left => all_distinct_left | Right => all_distinct_right)
   8.200 +         in dist_subtree ps (discharge [thm] rule) end;
   8.201 +
   8.202 +    val (ps,x_rest,y_rest) = split_common_prefix x_path y_path;
   8.203 +    val dist_subtree_thm = dist_subtree ps dist_thm;
   8.204 +    val subtree = cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   8.205 +    val (_,[l,_,_,r]) = Drule.strip_comb subtree;
   8.206 +    
   8.207 +    fun in_set ps tree =
   8.208 +      let
   8.209 +        val (_,[l,x,_,r]) = Drule.strip_comb tree;
   8.210 +        val xT = ctyp_of_term x;
   8.211 +      in (case ps of
   8.212 +            [] => instantiate 
   8.213 +                    [(ctyp_of_term x_in_set_root,xT)]
   8.214 +                    [(l_in_set_root,l),(x_in_set_root,x),(r_in_set_root,r)] in_set_root
   8.215 +          | (Left::ps') => 
   8.216 +               let
   8.217 +                  val in_set_l = in_set ps' l;
   8.218 +                  val in_set_left' = instantiate [(ctyp_of_term x_in_set_left,xT)]
   8.219 +                                      [(x_in_set_left,x),(r_in_set_left,r)] in_set_left;
   8.220 +               in discharge [in_set_l] in_set_left' end
   8.221 +          | (Right::ps') => 
   8.222 +               let
   8.223 +                  val in_set_r = in_set ps' r;
   8.224 +                  val in_set_right' = instantiate [(ctyp_of_term x_in_set_right,xT)] 
   8.225 +                                      [(x_in_set_right,x),(l_in_set_right,l)] in_set_right;
   8.226 +               in discharge [in_set_r] in_set_right' end)
   8.227 +      end 
   8.228 +       
   8.229 +  fun in_set' [] = raise TERM ("distinctTreeProver",[])
   8.230 +    | in_set' (Left::ps) = in_set ps l
   8.231 +    | in_set' (Right::ps) = in_set ps r;
   8.232 +
   8.233 +  fun distinct_lr node_in_set Left  = discharge [dist_subtree_thm,node_in_set] distinct_left 
   8.234 +    | distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right 
   8.235 +
   8.236 +  val (swap,neq) = 
   8.237 +       (case x_rest of
   8.238 +         [] => let 
   8.239 +                 val y_in_set = in_set' y_rest;
   8.240 +               in (false,distinct_lr y_in_set (hd y_rest)) end
   8.241 +       | (xr::xrs) => 
   8.242 +           (case y_rest of
   8.243 +             [] => let 
   8.244 +                     val x_in_set = in_set' x_rest;
   8.245 +               in (true,distinct_lr x_in_set (hd x_rest)) end
   8.246 +           | (yr::yrs) =>
   8.247 +               let
   8.248 +                 val x_in_set = in_set' x_rest;
   8.249 +                 val y_in_set = in_set' y_rest;
   8.250 +               in (case xr of
   8.251 +                    Left => (false,
   8.252 +                             discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right)
   8.253 +                   |Right => (true,
   8.254 +                             discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right))
   8.255 +               end
   8.256 +        ))
   8.257 +  in if swap then discharge [neq] swap_neq else neq
   8.258 +  end  
   8.259 +
   8.260 +
   8.261 +val delete_root = thm "DistinctTreeProver.delete_root";
   8.262 +val delete_left = thm "DistinctTreeProver.delete_left";
   8.263 +val delete_right = thm "DistinctTreeProver.delete_right";
   8.264 +
   8.265 +fun deleteProver dist_thm [] = delete_root OF [dist_thm]
   8.266 +  | deleteProver dist_thm (p::ps) =
   8.267 +     let
   8.268 +       val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right);
   8.269 +       val dist_thm' = discharge [dist_thm] dist_rule 
   8.270 +       val del_rule = (case p of Left => delete_left | Right => delete_right)
   8.271 +       val del = deleteProver dist_thm' ps;
   8.272 +     in discharge [dist_thm, del] del_rule end;
   8.273 +
   8.274 +val subtract_Tip = thm "DistinctTreeProver.subtract_Tip";
   8.275 +val subtract_Node = thm "DistinctTreeProver.subtract_Node";
   8.276 +val delete_Some_all_distinct = thm "DistinctTreeProver.delete_Some_all_distinct";
   8.277 +val subtract_Some_all_distinct_res = thm "DistinctTreeProver.subtract_Some_all_distinct_res";
   8.278 +
   8.279 +local
   8.280 +  val (alpha,v) = 
   8.281 +    let
   8.282 +      val ct = subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
   8.283 +               |> Thm.dest_comb |> #2
   8.284 +      val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp;
   8.285 +    in (alpha, #1 (dest_Var (term_of ct))) end;
   8.286 +in
   8.287 +fun subtractProver (Const ("DistinctTreeProver.tree.Tip",T)) ct dist_thm =
   8.288 +    let 
   8.289 +      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   8.290 +      val thy = theory_of_cterm ct;
   8.291 +      val [alphaI] = #2 (dest_Type T);
   8.292 +    in Thm.instantiate ([(alpha,ctyp_of thy alphaI)],
   8.293 +                        [(cterm_of thy (Var (v,treeT alphaI)),ct')]) subtract_Tip
   8.294 +    end
   8.295 +  | subtractProver (Const ("DistinctTreeProver.tree.Node",nT)$l$x$d$r) ct dist_thm =
   8.296 +    let
   8.297 +      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   8.298 +      val (_,[cl,_,_,cr]) = Drule.strip_comb ct;
   8.299 +      val ps = the (find_tree x (term_of ct'));
   8.300 +      val del_tree = deleteProver dist_thm ps;
   8.301 +      val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct; 
   8.302 +      val sub_l = subtractProver (term_of cl) cl (dist_thm');
   8.303 +      val sub_r = subtractProver (term_of cr) cr 
   8.304 +                    (discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res);
   8.305 +    in discharge [del_tree, sub_l, sub_r] subtract_Node end
   8.306 +end
   8.307 +
   8.308 +val subtract_Some_all_distinct = thm "DistinctTreeProver.subtract_Some_all_distinct";
   8.309 +fun distinct_implProver dist_thm ct =
   8.310 +  let
   8.311 +    val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   8.312 +    val sub = subtractProver (term_of ctree) ctree dist_thm;
   8.313 +  in subtract_Some_all_distinct OF [sub, dist_thm] end;
   8.314 +
   8.315 +fun get_fst_success f [] = NONE
   8.316 +  | get_fst_success f (x::xs) = (case f x of NONE => get_fst_success f xs 
   8.317 +                                 | SOME v => SOME v);
   8.318 +
   8.319 +fun neq_x_y ctxt x y name =
   8.320 +  (let
   8.321 +    val dist_thm = the (try (ProofContext.get_thm ctxt) (PureThy.Name name)); 
   8.322 +    val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
   8.323 +    val tree = term_of ctree;
   8.324 +    val x_path = the (find_tree x tree);
   8.325 +    val y_path = the (find_tree y tree);
   8.326 +    val thm = distinctTreeProver dist_thm x_path y_path;
   8.327 +  in SOME thm  
   8.328 +  end handle Option => NONE)
   8.329 +
   8.330 +fun distinctTree_tac names ctxt 
   8.331 +      (Const ("Trueprop",_) $ (Const ("Not", _) $ (Const ("op =", _) $ x $ y)), i) =
   8.332 +  (case get_fst_success (neq_x_y ctxt x y) names of
   8.333 +     SOME neq => rtac neq i
   8.334 +   | NONE => no_tac)
   8.335 +  | distinctTree_tac _ _ _ = no_tac;
   8.336 +
   8.337 +fun distinctFieldSolver names = mk_solver' "distinctFieldSolver"
   8.338 +     (fn ss => case #context (#1 (rep_ss ss)) of
   8.339 +                 SOME ctxt => SUBGOAL (distinctTree_tac names ctxt)
   8.340 +                | NONE => fn i => no_tac)
   8.341 +
   8.342 +fun distinct_simproc names =
   8.343 +  Simplifier.simproc HOL.thy "DistinctTreeProver.distinct_simproc" ["x = y"]
   8.344 +    (fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
   8.345 +        case #context (#1 (rep_ss ss)) of
   8.346 +        SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
   8.347 +                      (get_fst_success (neq_x_y ctxt x y) names)
   8.348 +       | NONE => NONE
   8.349 +    )
   8.350 +
   8.351 +end
   8.352 +end;
   8.353 \ No newline at end of file
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Statespace/document/root.tex	Wed Oct 24 18:36:09 2007 +0200
     9.3 @@ -0,0 +1,83 @@
     9.4 +\documentclass[11pt,a4paper]{article}
     9.5 +\usepackage{isabelle,isabellesym}
     9.6 +
     9.7 +% further packages required for unusual symbols (see also
     9.8 +% isabellesym.sty), use only when needed
     9.9 +
    9.10 +%\usepackage{amssymb}
    9.11 +  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
    9.12 +  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
    9.13 +  %\<triangleq>, \<yen>, \<lozenge>
    9.14 +
    9.15 +%\usepackage[greek,english]{babel}
    9.16 +  %option greek for \<euro>
    9.17 +  %option english (default language) for \<guillemotleft>, \<guillemotright>
    9.18 +
    9.19 +%\usepackage[latin1]{inputenc}
    9.20 +  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
    9.21 +  %\<threesuperior>, \<threequarters>, \<degree>
    9.22 +
    9.23 +%\usepackage[only,bigsqcap]{stmaryrd}
    9.24 +  %for \<Sqinter>
    9.25 +
    9.26 +%\usepackage{eufrak}
    9.27 +  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
    9.28 +
    9.29 +%\usepackage{textcomp}
    9.30 +  %for \<cent>, \<currency>
    9.31 +
    9.32 +% this should be the last package used
    9.33 +\usepackage{pdfsetup}
    9.34 +
    9.35 +% urls in roman style, theory text in math-similar italics
    9.36 +\urlstyle{rm}
    9.37 +\isabellestyle{it}
    9.38 +
    9.39 +
    9.40 +\begin{document}
    9.41 +
    9.42 +\title{State Spaces: The Locale Way}
    9.43 +\author{Norbert Schirmer}
    9.44 +\maketitle
    9.45 +
    9.46 +\tableofcontents
    9.47 +
    9.48 +%\parindent 0pt\parskip 0.5ex
    9.49 +
    9.50 +\section{Introduction}
    9.51 +
    9.52 +These theories introduce a new command called \isacommand{statespace}. 
    9.53 +It's usage is similar to \isacommand{record}s. However, the command does not introduce a new type but an
    9.54 +abstract specification based on the locale infrastructure. This leads
    9.55 +to extra flexibility in composing state space components, in particular
    9.56 +multiple inheritance and renaming of components.
    9.57 +
    9.58 +The state space infrastructure basically manages the following things:
    9.59 +\begin{itemize}
    9.60 +\item distinctness of field names
    9.61 +\item projections~/ injections from~/ to an abstract \emph{value} type
    9.62 +\item syntax translations for lookup and update, hiding the projections and injections
    9.63 +\item simplification procedure for lookups~/ updates, similar to records
    9.64 +\end{itemize}
    9.65 +
    9.66 +
    9.67 +\paragraph{Overview}
    9.68 +In Section \ref{sec:DistinctTreeProver} we define distinctness of the nodes in a binary tree and provide the basic prover tools to support efficient distinctness reasoning for field names managed by 
    9.69 +state spaces. The state is represented as a function from (abstract) names to (abstract) values as
    9.70 +introduced in Section \ref{sec:StateFun}. The basic setup for state spaces is in Section 
    9.71 +\ref{sec:StateSpaceLocale}. Some syntax for lookup and updates is added in Section \ref{sec:StateSpaceSyntax}. Finally Section \ref{sec:Examples} explains the usage of state spaces by examples.
    9.72 +
    9.73 +
    9.74 +% generated text of all theories
    9.75 +\input{session}
    9.76 +
    9.77 +% optional bibliography
    9.78 +%\bibliographystyle{abbrv}
    9.79 +%\bibliography{root}
    9.80 +
    9.81 +\end{document}
    9.82 +
    9.83 +%%% Local Variables:
    9.84 +%%% mode: latex
    9.85 +%%% TeX-master: t
    9.86 +%%% End:
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Statespace/state_fun.ML	Wed Oct 24 18:36:09 2007 +0200
    10.3 @@ -0,0 +1,397 @@
    10.4 +(*  Title:      state_fun.ML
    10.5 +    ID:         $Id$
    10.6 +    Author:     Norbert Schirmer, TU Muenchen
    10.7 +*)
    10.8 +
    10.9 +
   10.10 +structure StateFun =
   10.11 +struct
   10.12 +
   10.13 +val lookupN = "StateFun.lookup";
   10.14 +val updateN = "StateFun.update";
   10.15 +
   10.16 +
   10.17 +fun dest_nib c =
   10.18 +     let val h = List.last (String.explode c) 
   10.19 +     in if #"0" <= h andalso h <= #"9" then Char.ord h - Char.ord #"0"
   10.20 +        else if #"A" <= h andalso h <= #"F" then Char.ord h - Char.ord #"A" + 10
   10.21 +        else raise Match
   10.22 +     end;
   10.23 +
   10.24 +fun dest_chr (Const ("List.char.Char",_)$Const (c1,_)$(Const (c2,_))) = 
   10.25 +    let val c = Char.chr (dest_nib c1 * 16 + dest_nib c2)
   10.26 +    in if Char.isPrint c then c else raise Match end
   10.27 +  | dest_chr _ = raise Match;
   10.28 +
   10.29 +fun dest_string (Const ("List.list.Nil",_)) = []
   10.30 +  | dest_string (Const ("List.list.Cons",_)$c$cs) = dest_chr c::dest_string cs
   10.31 +  | dest_string _ = raise TERM ("dest_string",[]);
   10.32 +
   10.33 +fun sel_name n = String.implode (dest_string n);
   10.34 +
   10.35 +fun mk_name i t =
   10.36 +  (case try sel_name t of
   10.37 +     SOME name => name
   10.38 +   | NONE => (case t of 
   10.39 +               Free (x,_) => x
   10.40 +              |Const (x,_) => x
   10.41 +              |_ => "x"^string_of_int i))
   10.42 +               
   10.43 +local
   10.44 +val conj1_False = thm "conj1_False";
   10.45 +val conj2_False = thm "conj2_False";
   10.46 +val conj_True = thm "conj_True";
   10.47 +val conj_cong = thm "conj_cong";
   10.48 +fun isFalse (Const ("False",_)) = true
   10.49 +  | isFalse _ = false;
   10.50 +fun isTrue (Const ("True",_)) = true
   10.51 +  | isTrue _ = false;
   10.52 +
   10.53 +in
   10.54 +val lazy_conj_simproc =
   10.55 +  Simplifier.simproc HOL.thy "lazy_conj_simp" ["P & Q"]
   10.56 +    (fn thy => fn ss => fn t =>
   10.57 +      (case t of (Const ("op &",_)$P$Q) => 
   10.58 +         let
   10.59 +            val P_P' = Simplifier.rewrite ss (cterm_of thy P);
   10.60 +            val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 
   10.61 +         in if isFalse P'
   10.62 +            then SOME (conj1_False OF [P_P'])
   10.63 +            else 
   10.64 +              let
   10.65 +                val Q_Q' = Simplifier.rewrite ss (cterm_of thy Q);
   10.66 +                val Q' = Q_Q' |> prop_of |> Logic.dest_equals |> #2 
   10.67 +              in if isFalse Q'
   10.68 +                 then SOME (conj2_False OF [Q_Q'])
   10.69 +                 else if isTrue P' andalso isTrue Q'
   10.70 +                      then SOME (conj_True OF [P_P', Q_Q'])
   10.71 +                      else if P aconv P' andalso Q aconv Q' then NONE
   10.72 +                           else SOME (conj_cong OF [P_P', Q_Q'])
   10.73 +              end 
   10.74 +         end
   10.75 +        
   10.76 +      | _ => NONE));
   10.77 +
   10.78 +val string_eq_simp_tac =
   10.79 +     simp_tac (HOL_basic_ss 
   10.80 +                 addsimps (thms "list.inject"@thms "char.inject"@simp_thms)
   10.81 +                 addsimprocs [distinct_simproc,lazy_conj_simproc]
   10.82 +                 addcongs [thm "block_conj_cong"])
   10.83 +end;
   10.84 +
   10.85 +
   10.86 +
   10.87 +local
   10.88 +val rules = 
   10.89 + [thm "StateFun.lookup_update_id_same",
   10.90 +  thm "StateFun.id_id_cancel",
   10.91 +  thm "StateFun.lookup_update_same",thm "StateFun.lookup_update_other"
   10.92 +  ]
   10.93 +in
   10.94 +val lookup_ss = (HOL_basic_ss 
   10.95 +                 addsimps (thms "list.inject"@thms "char.inject"@simp_thms@rules)
   10.96 +                 addsimprocs [distinct_simproc,lazy_conj_simproc]
   10.97 +                 addcongs [thm "block_conj_cong"]
   10.98 +                 addSolver StateSpace.distinctNameSolver) 
   10.99 +end;
  10.100 +
  10.101 +val ex_lookup_ss = HOL_ss addsimps [thm "StateFun.ex_id"];
  10.102 +
  10.103 +structure StateFunArgs =
  10.104 +struct
  10.105 +  type T = (simpset * simpset * bool); 
  10.106 +           (* lookup simpset, ex_lookup simpset, are simprocs installed *)
  10.107 +  val empty = (empty_ss, empty_ss, false);
  10.108 +  val extend = I;
  10.109 +  fun merge pp ((ss1,ex_ss1,b1),(ss2,ex_ss2,b2)) = 
  10.110 +               (merge_ss (ss1,ss2)
  10.111 +               ,merge_ss (ex_ss1,ex_ss2)
  10.112 +               ,b1 orelse b2);
  10.113 +end;
  10.114 +
  10.115 +
  10.116 +structure StateFunData = GenericDataFun(StateFunArgs);
  10.117 +
  10.118 +val init_state_fun_data =
  10.119 +  Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
  10.120 +
  10.121 +val lookup_simproc =
  10.122 +  Simplifier.simproc (the_context ()) "lookup_simp" ["lookup d n (update d' c m v s)"]
  10.123 +    (fn thy => fn ss => fn t =>
  10.124 +      (case t of (Const ("StateFun.lookup",lT)$destr$n$
  10.125 +                   (s as Const ("StateFun.update",uT)$_$_$_$_$_)) =>
  10.126 +        (let
  10.127 +          val (_::_::_::_::sT::_) = binder_types uT;
  10.128 +          val mi = maxidx_of_term t;
  10.129 +          fun mk_upds (Const ("StateFun.update",uT)$d'$c$m$v$s) =
  10.130 +               let
  10.131 +                 val (_::_::_::fT::_::_) = binder_types uT;
  10.132 +                 val vT = domain_type fT;
  10.133 +                 val (s',cnt) = mk_upds s;
  10.134 +                 val (v',cnt') = 
  10.135 +                      (case v of
  10.136 +                        Const ("StateFun.K_statefun",KT)$v''
  10.137 +                         => (case v'' of 
  10.138 +                             (Const ("StateFun.lookup",_)$(d as (Const ("Fun.id",_)))$n'$_)
  10.139 +                              => if d aconv c andalso n aconv m andalso m aconv n' 
  10.140 +                                 then (v,cnt) (* Keep value so that 
  10.141 +                                                 lookup_update_id_same can fire *)
  10.142 +                                 else (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT),
  10.143 +                                       cnt+1)
  10.144 +                              | _ => (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT),
  10.145 +                                       cnt+1))
  10.146 +                       | _ => (v,cnt));
  10.147 +               in (Const ("StateFun.update",uT)$d'$c$m$v'$s',cnt')
  10.148 +               end
  10.149 +            | mk_upds s = (Var (("s",mi+1),sT),mi+2);
  10.150 +          
  10.151 +          val ct = cterm_of thy 
  10.152 +                    (Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s)));
  10.153 +          val ctxt = the (#context (#1 (rep_ss ss)));
  10.154 +          val basic_ss = #1 (StateFunData.get (Context.Proof ctxt));
  10.155 +          val ss' = Simplifier.context 
  10.156 +                     (Config.map MetaSimplifier.simp_depth_limit (K 100) ctxt) basic_ss;
  10.157 +          val thm = Simplifier.rewrite ss' ct;
  10.158 +        in if (op aconv) (Logic.dest_equals (prop_of thm))
  10.159 +           then NONE
  10.160 +           else SOME thm
  10.161 +        end
  10.162 +        handle Option => NONE)
  10.163 +         
  10.164 +      | _ => NONE ));
  10.165 +
  10.166 +
  10.167 +fun foldl1 f (x::xs) = foldl f x xs;
  10.168 +
  10.169 +local
  10.170 +val update_apply = thm "StateFun.update_apply";
  10.171 +val meta_ext = thm "StateFun.meta_ext";
  10.172 +val o_apply = thm "Fun.o_apply";
  10.173 +val ss' = (HOL_ss addsimps (update_apply::o_apply::thms "list.inject"@thms "char.inject")
  10.174 +                 addsimprocs [distinct_simproc,lazy_conj_simproc,StateSpace.distinct_simproc]
  10.175 +                 addcongs [thm "block_conj_cong"]);
  10.176 +in
  10.177 +val update_simproc =
  10.178 +  Simplifier.simproc (the_context ()) "update_simp" ["update d c n v s"]
  10.179 +    (fn thy => fn ss => fn t =>
  10.180 +      (case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) =>
  10.181 +         let 
  10.182 +            
  10.183 +             val (_::_::_::_::sT::_) = binder_types uT;
  10.184 +                (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
  10.185 +             fun init_seed s = (Bound 0,Bound 0, [("s",sT)],[], false);
  10.186 +
  10.187 +             fun mk_comp f fT g gT =
  10.188 +               let val T = (domain_type fT --> range_type gT) 
  10.189 +               in (Const ("Fun.comp",gT --> fT --> T)$g$f,T) end
  10.190 +
  10.191 +             fun mk_comps fs = 
  10.192 +                   foldl1 (fn ((f,fT),(g,gT)) => mk_comp f fT g gT) fs;
  10.193 +
  10.194 +             fun append n c cT f fT d dT comps =
  10.195 +               (case AList.lookup (op aconv) comps n of
  10.196 +                  SOME gTs => AList.update (op aconv) 
  10.197 +                                    (n,[(c,cT),(f,fT),(d,dT)]@gTs) comps
  10.198 +                | NONE => AList.update (op aconv) (n,[(c,cT),(f,fT),(d,dT)]) comps)
  10.199 +
  10.200 +             fun split_list (x::xs) = let val (xs',y) = split_last xs in (x,xs',y) end
  10.201 +               | split_list _ = error "StateFun.split_list";
  10.202 +
  10.203 +             fun merge_upds n comps =
  10.204 +               let val ((c,cT),fs,(d,dT)) = split_list (the (AList.lookup (op aconv) comps n))
  10.205 +               in ((c,cT),fst (mk_comps fs),(d,dT)) end;
  10.206 +
  10.207 +             (* mk_updterm returns 
  10.208 +              *  - (orig-term-skeleton,simplified-term-skeleton, vars, b)
  10.209 +              *     where boolean b tells if a simplification has occured.
  10.210 +                    "orig-term-skeleton = simplified-term-skeleton" is
  10.211 +              *     the desired simplification rule.
  10.212 +              * The algorithm first walks down the updates to the seed-state while
  10.213 +              * memorising the updates in the already-table. While walking up the
  10.214 +              * updates again, the optimised term is constructed.
  10.215 +              *)
  10.216 +             fun mk_updterm already
  10.217 +                 (t as ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s)) =
  10.218 +                      let
  10.219 +                         fun rest already = mk_updterm already;
  10.220 +                         val (dT::cT::nT::vT::sT::_) = binder_types uT;
  10.221 +                          (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => 
  10.222 +                                ('n => 'v) => ('n => 'v)"*)
  10.223 +                      in if member (op aconv) already n
  10.224 +                         then (case rest already s of
  10.225 +                                 (trm,trm',vars,comps,_) =>
  10.226 +                                   let
  10.227 +                                     val i = length vars;
  10.228 +                                     val kv = (mk_name i n,vT);
  10.229 +                                     val kb = Bound i;
  10.230 +                                     val comps' = append n c cT kb vT d dT comps;
  10.231 +                                   in (upd$d$c$n$kb$trm, trm', kv::vars,comps',true) end)
  10.232 +                         else
  10.233 +                          (case rest (n::already) s of
  10.234 +                             (trm,trm',vars,comps,b) =>
  10.235 +                                let
  10.236 +                                   val i = length vars;
  10.237 +                                   val kv = (mk_name i n,vT);
  10.238 +                                   val kb = Bound i;
  10.239 +                                   val comps' = append n c cT kb vT d dT comps;
  10.240 +                                   val ((c',c'T),f',(d',d'T)) = merge_upds n comps';
  10.241 +                                   val vT' = range_type d'T --> domain_type c'T;
  10.242 +                                   val upd' = Const ("StateFun.update",d'T --> c'T --> nT --> vT' --> sT --> sT);
  10.243 +                                in (upd$d$c$n$kb$trm, upd'$d'$c'$n$f'$trm', kv::vars,comps',b) 
  10.244 +                                end)
  10.245 +                      end
  10.246 +               | mk_updterm _ t = init_seed t;
  10.247 +
  10.248 +	     val ctxt = the (#context (#1 (rep_ss ss))) |>
  10.249 +                        Config.map MetaSimplifier.simp_depth_limit (K 100);
  10.250 +             val ss1 = Simplifier.context ctxt ss';
  10.251 +             val ss2 = Simplifier.context ctxt 
  10.252 +                         (#1 (StateFunData.get (Context.Proof ctxt)));
  10.253 +         in (case mk_updterm [] t of
  10.254 +               (trm,trm',vars,_,true)
  10.255 +                => let
  10.256 +                     val eq1 = Goal.prove ctxt [] [] 
  10.257 +                                      (list_all (vars,equals sT$trm$trm'))
  10.258 +                                      (fn _ => rtac meta_ext 1 THEN 
  10.259 +                                               simp_tac ss1 1);
  10.260 +                     val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
  10.261 +                   in SOME (transitive eq1 eq2) end
  10.262 +             | _ => NONE)
  10.263 +         end
  10.264 +       | _ => NONE));
  10.265 +end
  10.266 +
  10.267 +
  10.268 +
  10.269 +
  10.270 +local
  10.271 +val swap_ex_eq = thm "StateFun.swap_ex_eq";
  10.272 +fun is_selector thy T sel =
  10.273 +     let 
  10.274 +       val (flds,more) = RecordPackage.get_recT_fields thy T 
  10.275 +     in member (fn (s,(n,_)) => n=s) (more::flds) sel
  10.276 +     end;
  10.277 +in
  10.278 +val ex_lookup_eq_simproc =
  10.279 +  Simplifier.simproc HOL.thy "ex_lookup_eq_simproc" ["Ex t"]
  10.280 +    (fn thy => fn ss => fn t =>
  10.281 +       let
  10.282 +         val ctxt = Simplifier.the_context ss |>
  10.283 +                    Config.map MetaSimplifier.simp_depth_limit (K 100)
  10.284 +         val ex_lookup_ss = #2 (StateFunData.get (Context.Proof ctxt));
  10.285 +         val ss' = (Simplifier.context ctxt ex_lookup_ss);
  10.286 +         fun prove prop =
  10.287 +           Goal.prove_global thy [] [] prop 
  10.288 +             (fn _ => record_split_simp_tac [] (K ~1) 1 THEN
  10.289 +                      simp_tac ss' 1);
  10.290 +
  10.291 +         fun mkeq (swap,Teq,lT,lo,d,n,x,s) i =
  10.292 +               let val (_::nT::_) = binder_types lT;
  10.293 +                         (*  ('v => 'a) => 'n => ('n => 'v) => 'a *)
  10.294 +                   val x' = if not (loose_bvar1 (x,0))
  10.295 +			    then Bound 1
  10.296 +                            else raise TERM ("",[x]);
  10.297 +                   val n' = if not (loose_bvar1 (n,0))
  10.298 +			    then Bound 2
  10.299 +                            else raise TERM ("",[n]);
  10.300 +                   val sel' = lo $ d $ n' $ s;
  10.301 +                  in (Const ("op =",Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
  10.302 +
  10.303 +         fun dest_state (s as Bound 0) = s
  10.304 +           | dest_state (s as (Const (sel,sT)$Bound 0)) =
  10.305 +               if is_selector thy (domain_type sT) sel
  10.306 +               then s
  10.307 +               else raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s])
  10.308 +           | dest_state s = 
  10.309 +                    raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
  10.310 +  
  10.311 +         fun dest_sel_eq (Const ("op =",Teq)$
  10.312 +                           ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
  10.313 +                           (false,Teq,lT,lo,d,n,X,dest_state s)
  10.314 +           | dest_sel_eq (Const ("op =",Teq)$X$
  10.315 +                            ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
  10.316 +                           (true,Teq,lT,lo,d,n,X,dest_state s)
  10.317 +           | dest_sel_eq _ = raise TERM ("",[]);
  10.318 +
  10.319 +       in
  10.320 +         (case t of
  10.321 +           (Const ("Ex",Tex)$Abs(s,T,t)) =>
  10.322 +             (let val (eq,eT,nT,swap) = mkeq (dest_sel_eq t) 0;
  10.323 +                  val prop = list_all ([("n",nT),("x",eT)],
  10.324 +                              Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq),
  10.325 +                                               HOLogic.true_const));
  10.326 +                  val thm = standard (prove prop);
  10.327 +                  val thm' = if swap then swap_ex_eq OF [thm] else thm
  10.328 +             in SOME thm' end
  10.329 +             handle TERM _ => NONE)
  10.330 +          | _ => NONE)
  10.331 +        end handle Option => NONE) 
  10.332 +end;
  10.333 +
  10.334 +val val_sfx = "V";
  10.335 +val val_prfx = "StateFun."
  10.336 +fun deco base_prfx s = val_prfx ^ (base_prfx ^ suffix val_sfx s);
  10.337 +
  10.338 +fun mkUpper str = 
  10.339 +  (case String.explode str of
  10.340 +    [] => ""
  10.341 +   | c::cs => String.implode (Char.toUpper c::cs ))
  10.342 +
  10.343 +fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base T)
  10.344 +  | mkName (TFree (x,_)) = mkUpper (NameSpace.base x)
  10.345 +  | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base x);
  10.346 +
  10.347 +fun is_datatype thy n = is_some (Symtab.lookup (DatatypePackage.get_datatypes thy) n);
  10.348 +
  10.349 +fun mk_map ("List.list") = Syntax.const "List.map"
  10.350 +  | mk_map n = Syntax.const ("StateFun." ^  "map_" ^ NameSpace.base n);
  10.351 +
  10.352 +fun gen_constr_destr comp prfx thy (Type (T,[])) = 
  10.353 +      Syntax.const (deco prfx (mkUpper (NameSpace.base T)))
  10.354 +  | gen_constr_destr comp prfx thy (T as Type ("fun",_)) =
  10.355 +     let val (argTs,rangeT) = strip_type T;
  10.356 +     in comp 
  10.357 +          (Syntax.const (deco prfx (concat (map mkName argTs) ^ "Fun")))
  10.358 +          (fold (fn x => fn y => x$y)
  10.359 +               (replicate (length argTs) (Syntax.const "StateFun.map_fun"))
  10.360 +               (gen_constr_destr comp prfx thy rangeT))
  10.361 +     end
  10.362 +  | gen_constr_destr comp prfx thy (T' as Type (T,argTs)) = 
  10.363 +     if is_datatype thy T
  10.364 +     then (* datatype args are recursively embedded into val *)
  10.365 +         (case argTs of
  10.366 +           [argT] => comp 
  10.367 +                     ((Syntax.const (deco prfx (mkUpper (NameSpace.base T)))))
  10.368 +                     ((mk_map T $ gen_constr_destr comp prfx thy argT))
  10.369 +          | _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[])))
  10.370 +     else (* type args are not recursively embedded into val *)
  10.371 +           Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base T)))
  10.372 +  | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[]));
  10.373 +                   
  10.374 +val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) ""
  10.375 +val mk_destr =  gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ b $ a) "the_"
  10.376 +
  10.377 +  
  10.378 +fun statefun_simp_attr src (ctxt,thm) = 
  10.379 +  let
  10.380 +     val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
  10.381 +     val (lookup_ss', ex_lookup_ss') = 
  10.382 +	   (case (concl_of thm) of
  10.383 +            (_$((Const ("Ex",_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
  10.384 +            | _ => (lookup_ss addsimps [thm], ex_lookup_ss))
  10.385 +     fun activate_simprocs ctxt =
  10.386 +          if simprocs_active then ctxt
  10.387 +          else StateSpace.change_simpset 
  10.388 +                (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt
  10.389 +               
  10.390 +
  10.391 +     val ctxt' = ctxt 
  10.392 +         |> activate_simprocs
  10.393 +         |> (StateFunData.put (lookup_ss',ex_lookup_ss',true))
  10.394 +  in (ctxt', thm) end;
  10.395 +
  10.396 +val setup = 
  10.397 +    init_state_fun_data 
  10.398 +    #> Attrib.add_attributes 
  10.399 +	  [("statefun_simp",statefun_simp_attr,"simplification in statespaces")]     
  10.400 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Oct 24 18:36:09 2007 +0200
    11.3 @@ -0,0 +1,660 @@
    11.4 +(*  Title:      state_space.ML
    11.5 +    ID:         $Id$
    11.6 +    Author:     Norbert Schirmer, TU Muenchen
    11.7 +*)
    11.8 +
    11.9 +structure StateSpace =
   11.10 +struct
   11.11 +
   11.12 +(* Theorems *)
   11.13 +
   11.14 +(* Names *)
   11.15 +val distinct_compsN = "distinct_names"
   11.16 +val namespaceN = "_namespace"
   11.17 +val valuetypesN = "_valuetypes"
   11.18 +val projectN = "project"
   11.19 +val injectN = "inject"
   11.20 +val getN = "get"
   11.21 +val putN = "put"
   11.22 +val project_injectL = "StateSpaceLocale.project_inject";
   11.23 +val KN = "StateFun.K_statefun"
   11.24 +
   11.25 +
   11.26 +(* messages *)
   11.27 +
   11.28 +val quiet_mode = ref false;
   11.29 +fun message s = if ! quiet_mode then () else writeln s;
   11.30 +
   11.31 +(* Library *)
   11.32 +
   11.33 +fun fold1 f xs = fold f (tl xs) (hd xs)
   11.34 +fun fold1' f [] x = x
   11.35 +  | fold1' f xs _ = fold1 f xs
   11.36 + 
   11.37 +fun sublist_idx eq xs ys = 
   11.38 +  let
   11.39 +    fun sublist n xs ys = 
   11.40 +         if is_prefix eq xs ys then SOME n
   11.41 +         else (case ys of [] => NONE
   11.42 +               | (y::ys') => sublist (n+1) xs ys')
   11.43 +  in sublist 0 xs ys end;
   11.44 +
   11.45 +fun is_sublist eq xs ys = is_some (sublist_idx eq xs ys);
   11.46 +
   11.47 +fun sorted_subset eq [] ys = true
   11.48 +  | sorted_subset eq (x::xs) [] = false
   11.49 +  | sorted_subset eq (x::xs) (y::ys) = if eq (x,y) then sorted_subset eq xs ys
   11.50 +                                       else sorted_subset eq (x::xs) ys;
   11.51 +
   11.52 +
   11.53 +
   11.54 +type namespace_info =
   11.55 + {declinfo: (typ*string) Termtab.table, (* type, name of statespace *)
   11.56 +  distinctthm: thm Symtab.table,
   11.57 +  silent: bool
   11.58 + };
   11.59 + 
   11.60 +structure NameSpaceArgs =
   11.61 +struct
   11.62 +  type T = namespace_info; 
   11.63 +  val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false};
   11.64 +  val extend = I;
   11.65 +  fun merge pp ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
   11.66 +                {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) =
   11.67 +                {declinfo = Termtab.merge (K true) (declinfo1, declinfo2),
   11.68 +                 distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2),
   11.69 +                 silent = silent1 andalso silent2}
   11.70 +end;
   11.71 +
   11.72 +structure NameSpaceData = GenericDataFun(NameSpaceArgs);
   11.73 +
   11.74 +fun make_namespace_data declinfo distinctthm silent =
   11.75 +     {declinfo=declinfo,distinctthm=distinctthm,silent=silent};
   11.76 +
   11.77 +
   11.78 +fun delete_declinfo n ctxt =
   11.79 +  let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
   11.80 +  in NameSpaceData.put 
   11.81 +       (make_namespace_data (Termtab.delete_safe n declinfo) distinctthm silent) ctxt
   11.82 +  end;
   11.83 +
   11.84 +
   11.85 +fun update_declinfo (n,v) ctxt =
   11.86 +  let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
   11.87 +  in NameSpaceData.put 
   11.88 +      (make_namespace_data (Termtab.update (n,v) declinfo) distinctthm silent) ctxt
   11.89 +  end;
   11.90 +
   11.91 +fun set_silent silent ctxt =
   11.92 +  let val {declinfo,distinctthm,...} = NameSpaceData.get ctxt;
   11.93 +  in NameSpaceData.put 
   11.94 +      (make_namespace_data declinfo distinctthm silent) ctxt
   11.95 +  end;
   11.96 +
   11.97 +val get_silent = #silent o NameSpaceData.get;
   11.98 + 
   11.99 +fun prove_interpretation_in ctxt_tac (name, expr) thy =
  11.100 +   thy
  11.101 +   |> Locale.interpretation_in_locale I (name, expr)
  11.102 +   |> Proof.global_terminal_proof 
  11.103 +         (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE)
  11.104 +   |> ProofContext.theory_of
  11.105 +
  11.106 +type statespace_info =
  11.107 + {args: (string * sort) list, (* type arguments *)
  11.108 +  parents: (typ list * string * string option list) list,
  11.109 +             (* type instantiation, state-space name, component renamings *)
  11.110 +  components: (string * typ) list,
  11.111 +  types: typ list (* range types of state space *)
  11.112 + };
  11.113 +
  11.114 +structure StateSpaceArgs =
  11.115 +struct
  11.116 +  val name = "HOL/StateSpace";
  11.117 +  type T = statespace_info Symtab.table;
  11.118 +  val empty = Symtab.empty;
  11.119 +  val extend = I;
  11.120 +
  11.121 +  fun merge pp (nt1,nt2) = Symtab.merge (K true) (nt1, nt2);
  11.122 +end;
  11.123 +
  11.124 +structure StateSpaceData = GenericDataFun(StateSpaceArgs);
  11.125 +
  11.126 +fun add_statespace name args parents components types ctxt =
  11.127 +     StateSpaceData.put 
  11.128 +      (Symtab.update_new (name, {args=args,parents=parents,
  11.129 +                                components=components,types=types}) (StateSpaceData.get ctxt))
  11.130 +      ctxt; 
  11.131 +
  11.132 +fun get_statespace ctxt name =
  11.133 +      Symtab.lookup (StateSpaceData.get ctxt) name;
  11.134 +
  11.135 +
  11.136 +fun lookupI eq xs n = 
  11.137 +  (case AList.lookup eq xs n of
  11.138 +     SOME v => v
  11.139 +   | NONE => n);
  11.140 + 
  11.141 +fun mk_free ctxt name =
  11.142 +  if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name 
  11.143 +  then
  11.144 +    let val n' = lookupI (op =) (Variable.fixes_of ctxt) name
  11.145 +    in SOME (Free (n',ProofContext.infer_type ctxt n')) end
  11.146 +  else NONE
  11.147 +  
  11.148 +     
  11.149 +fun get_dist_thm ctxt name = Symtab.lookup (#distinctthm (NameSpaceData.get ctxt)) name;
  11.150 +fun get_comp ctxt name = 
  11.151 +     Option.mapPartial 
  11.152 +       (Termtab.lookup (#declinfo (NameSpaceData.get ctxt))) 
  11.153 +       (mk_free (Context.proof_of ctxt) name);
  11.154 +
  11.155 +
  11.156 +(*** Tactics ***)
  11.157 +
  11.158 +fun neq_x_y ctxt x y =
  11.159 +  (let
  11.160 +    val dist_thm = the (get_dist_thm (Context.Proof ctxt) (#1 (dest_Free x))); 
  11.161 +    val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
  11.162 +    val tree = term_of ctree;
  11.163 +    val x_path = the (DistinctTreeProver.find_tree x tree);
  11.164 +    val y_path = the (DistinctTreeProver.find_tree y tree);
  11.165 +    val thm = DistinctTreeProver.distinctTreeProver dist_thm x_path y_path;
  11.166 +  in SOME thm  
  11.167 +  end handle Option => NONE)
  11.168 +
  11.169 +fun distinctTree_tac ctxt 
  11.170 +      (Const ("Trueprop",_) $ 
  11.171 +        (Const ("Not", _) $ (Const ("op =", _) $ (x as Free _)$ (y as Free _))), i) =
  11.172 +  (case (neq_x_y ctxt x y) of
  11.173 +     SOME neq => rtac neq i
  11.174 +   | NONE => no_tac)
  11.175 +  | distinctTree_tac _ _ = no_tac;
  11.176 +
  11.177 +val distinctNameSolver = mk_solver' "distinctNameSolver"
  11.178 +     (fn ss => case #context (#1 (rep_ss ss)) of
  11.179 +                 SOME ctxt => SUBGOAL (distinctTree_tac ctxt)
  11.180 +                | NONE => fn i => no_tac)
  11.181 +
  11.182 +val distinct_simproc =
  11.183 +  Simplifier.simproc HOL.thy "StateSpace.distinct_simproc" ["x = y"]
  11.184 +    (fn thy => fn ss => (fn (Const ("op =",_)$(x as Free _)$(y as Free _)) =>
  11.185 +        (case #context (#1 (rep_ss ss)) of
  11.186 +          SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) 
  11.187 +                       (neq_x_y ctxt x y) 
  11.188 +        | NONE => NONE)
  11.189 +      | _ => NONE))
  11.190 +
  11.191 +fun change_simpset f = 
  11.192 +     Context.mapping 
  11.193 +       (fn thy  => (change_simpset_of thy f; thy))
  11.194 +       (fn ctxt => Simplifier.put_local_simpset (f (Simplifier.get_local_simpset ctxt)) ctxt);
  11.195 +
  11.196 +fun read_typ thy s =
  11.197 +  Sign.read_typ thy s;
  11.198 +
  11.199 +local
  11.200 +  val ss = HOL_basic_ss 
  11.201 +in    
  11.202 +fun interprete_parent name dist_thm_name parent_expr thy = 
  11.203 +  let
  11.204 +
  11.205 +    fun solve_tac ctxt (_,i) st =
  11.206 +      let
  11.207 +        val distinct_thm = ProofContext.get_thm ctxt (Name dist_thm_name);
  11.208 +        val goal = List.nth (cprems_of st,i-1);
  11.209 +        val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
  11.210 +      in EVERY [rtac rule i] st
  11.211 +      end
  11.212 +        
  11.213 +    fun tac ctxt = EVERY [Locale.intro_locales_tac true ctxt [],
  11.214 +                          ALLGOALS (SUBGOAL (solve_tac ctxt))] 
  11.215 +        
  11.216 +  in thy 
  11.217 +     |> prove_interpretation_in tac (name,parent_expr)
  11.218 +  end;        
  11.219 +
  11.220 +end;
  11.221 +
  11.222 +fun namespace_definition name nameT parent_expr parent_comps new_comps thy = 
  11.223 +  let
  11.224 +    val all_comps = parent_comps @ new_comps;
  11.225 +    val vars = Locale.Merge 
  11.226 +                (map (fn n => Locale.Rename (Locale.Locale (Locale.intern thy "var")
  11.227 +                                            ,[SOME (n,NONE)])) all_comps);
  11.228 +
  11.229 +    val full_name = Sign.full_name thy name;
  11.230 +    val dist_thm_name = distinct_compsN;
  11.231 +    val dist_thm_full_name =
  11.232 +        let val prefix = fold1' (fn name => fn prfx => prfx ^ "_" ^ name) all_comps "";
  11.233 +        in if prefix = "" then dist_thm_name else prefix ^ "." ^ dist_thm_name end;
  11.234 +
  11.235 +    fun comps_of_thm thm = prop_of thm 
  11.236 +             |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free);
  11.237 + 
  11.238 +    fun type_attr phi (ctxt,thm) =
  11.239 +      (case ctxt of Context.Theory _ => (ctxt,thm)
  11.240 +       | _ =>
  11.241 +        let 
  11.242 +          val {declinfo,distinctthm=tt,silent} = (NameSpaceData.get ctxt);
  11.243 +	  val all_names = comps_of_thm thm;
  11.244 +          fun upd name tt =
  11.245 +               (case (Symtab.lookup tt name) of
  11.246 +                 SOME dthm => if sorted_subset (op =) (comps_of_thm dthm) all_names
  11.247 +                              then Symtab.update (name,thm) tt else tt
  11.248 +                | NONE => Symtab.update (name,thm) tt)
  11.249 +
  11.250 +          val tt' = tt |> fold upd all_names;
  11.251 +          val activate_simproc =
  11.252 +              Output.no_warnings 
  11.253 +               (change_simpset (fn ss => ss addsimprocs [distinct_simproc]));
  11.254 +          val ctxt' =
  11.255 +              ctxt 
  11.256 +              |> NameSpaceData.put {declinfo=declinfo,distinctthm=tt',silent=silent}
  11.257 +              |> activate_simproc
  11.258 +        in (ctxt',thm) 
  11.259 +        end)
  11.260 +        
  11.261 +    val attr = Attrib.internal type_attr;
  11.262 +
  11.263 +    val assumes = Element.Assumes [((dist_thm_name,[attr]), 
  11.264 +                    [(HOLogic.Trueprop $
  11.265 +                      (Const ("DistinctTreeProver.all_distinct",
  11.266 +                                 Type ("DistinctTreeProver.tree",[nameT]) --> HOLogic.boolT) $
  11.267 +                      DistinctTreeProver.mk_tree (fn n => Free (n,nameT)) nameT 
  11.268 +                                (sort fast_string_ord all_comps)),
  11.269 +                      ([]))])];
  11.270 +
  11.271 +  in thy 
  11.272 +     |> Locale.add_locale_i (SOME "") name vars [assumes]
  11.273 +     ||> ProofContext.theory_of 
  11.274 +     ||> interprete_parent name dist_thm_full_name parent_expr
  11.275 +     |> #2
  11.276 +  end;
  11.277 +
  11.278 +structure Typetab = TableFun(type key=typ val ord = Term.typ_ord);
  11.279 +
  11.280 +fun encode_dot x = if x= #"." then #"_" else x;
  11.281 +
  11.282 +fun encode_type (TFree (s, _)) = s
  11.283 +  | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i
  11.284 +  | encode_type (Type (n,Ts)) = 
  11.285 +      let
  11.286 +        val Ts' = fold1' (fn x => fn y => x ^ "_" ^ y) (map encode_type Ts) "";
  11.287 +        val n' = String.map encode_dot n;
  11.288 +      in if Ts'="" then n' else Ts' ^ "_" ^ n' end;
  11.289 +
  11.290 +fun project_name T = projectN ^"_"^encode_type T;
  11.291 +fun inject_name T = injectN ^"_"^encode_type T;
  11.292 +
  11.293 +fun project_free T pT V = Free (project_name T, V --> pT);
  11.294 +fun inject_free T pT V = Free (inject_name T, pT --> V);
  11.295 +
  11.296 +fun get_name n = getN ^ "_" ^ n;
  11.297 +fun put_name n = putN ^ "_" ^ n;
  11.298 +fun get_const n T nT V = Free (get_name n, (nT --> V) --> T);
  11.299 +fun put_const n T nT V = Free (put_name n, T --> (nT --> V) --> (nT --> V));
  11.300 +
  11.301 +fun lookup_const T nT V = Const ("StateFun.lookup",(V --> T) --> nT --> (nT --> V) --> T);
  11.302 +fun update_const T nT V = 
  11.303 + Const ("StateFun.update",
  11.304 +          (V --> T) --> (T --> V) --> nT --> (T --> T) --> (nT --> V) --> (nT --> V));
  11.305 +
  11.306 +fun K_const T = Const ("StateFun.K_statefun",T --> T --> T);
  11.307 +
  11.308 +val no_syn = #3 (Syntax.no_syn ((),()));
  11.309 +
  11.310 +
  11.311 +fun add_declaration name decl thy =
  11.312 +  thy
  11.313 +  |> TheoryTarget.init name
  11.314 +  |> (fn lthy => LocalTheory.declaration (decl lthy) lthy)
  11.315 +  |> LocalTheory.exit 
  11.316 +  |> ProofContext.theory_of;
  11.317 +
  11.318 +fun parent_components thy (Ts, pname, renaming) =
  11.319 +  let
  11.320 +    val ctxt = Context.Theory thy;
  11.321 +    fun rename [] xs = xs
  11.322 +      | rename (NONE::rs)  (x::xs) = x::rename rs xs
  11.323 +      | rename (SOME r::rs) ((x,T)::xs) = (r,T)::rename rs xs;
  11.324 +    val {args,parents,components,...} = 
  11.325 +	      the (Symtab.lookup (StateSpaceData.get ctxt) pname);
  11.326 +    val inst = map fst args ~~ Ts;
  11.327 +    val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
  11.328 +    val parent_comps = 
  11.329 +     List.concat (map (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents);
  11.330 +    val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
  11.331 +  in all_comps end;
  11.332 +
  11.333 +fun take_upto i xs = List.take(xs,i) handle Subscript => xs;
  11.334 +
  11.335 +fun statespace_definition state_type args name parents parent_comps components thy =
  11.336 +  let 
  11.337 +    val full_name = Sign.full_name thy name;
  11.338 +    val all_comps = parent_comps @ components;
  11.339 +
  11.340 +    val components' = map (fn (n,T) => (n,(T,full_name))) components;
  11.341 +    val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps; 
  11.342 +    fun parent_expr (_,n,rs) = Locale.Rename 
  11.343 +                                (Locale.Locale (suffix namespaceN n),
  11.344 +                                 map (Option.map (fn s => (s,NONE))) rs);
  11.345 +    val parents_expr = Locale.Merge (fold (fn p => fn es => parent_expr p::es) parents []);
  11.346 +
  11.347 +    fun distinct_types Ts =
  11.348 +      let val tab = fold (fn T => fn tab => Typetab.update (T,()) tab) Ts Typetab.empty;
  11.349 +      in map fst (Typetab.dest tab) end;
  11.350 +
  11.351 +    val Ts = distinct_types (map snd all_comps);
  11.352 +    val arg_names = map fst args;
  11.353 +    val valueN = Name.variant arg_names "'value";
  11.354 +    val nameN = Name.variant (valueN::arg_names) "'name";
  11.355 +    val valueT = TFree (valueN, Sign.defaultS thy);
  11.356 +    val nameT = TFree (nameN, Sign.defaultS thy);
  11.357 +    val stateT = nameT --> valueT;
  11.358 +    fun projectT T = valueT --> T;
  11.359 +    fun injectT T = T --> valueT; 
  11.360 +
  11.361 +    val locs = map (fn T => Locale.Rename (Locale.Locale project_injectL,
  11.362 +                             [SOME (project_name T,NONE),
  11.363 +                              SOME (inject_name T ,NONE)])) Ts;
  11.364 +    val constrains = List.concat 
  11.365 +         (map (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts);
  11.366 +
  11.367 +    fun interprete_parent_valuetypes (Ts, pname, _) = 
  11.368 +      let
  11.369 +        val {args,types,...} = 
  11.370 +             the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname);
  11.371 +        val inst = map fst args ~~ Ts;
  11.372 +        val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
  11.373 +        val pars = List.concat (map ((fn T => [project_name T,inject_name T]) o subst) types);
  11.374 +        val expr = Locale.Rename (Locale.Locale (suffix valuetypesN name),
  11.375 +                                  map (fn n => SOME (n,NONE)) pars);
  11.376 +      in prove_interpretation_in (K all_tac) 
  11.377 +           (suffix valuetypesN name, expr) end;
  11.378 +
  11.379 +    fun interprete_parent (_, pname, rs) =
  11.380 +      let
  11.381 +        val expr = Locale.Rename (Locale.Locale pname, map (Option.map (fn n => (n,NONE))) rs)
  11.382 +      in prove_interpretation_in 
  11.383 +           (fn ctxt => Locale.intro_locales_tac false ctxt []) 
  11.384 +           (full_name, expr) end;
  11.385 +
  11.386 +    fun declare_declinfo updates lthy phi ctxt =
  11.387 +      let
  11.388 +        fun upd_prf ctxt = 
  11.389 +          let
  11.390 +            fun upd (n,v) =
  11.391 +              let
  11.392 +                val nT = ProofContext.infer_type (LocalTheory.target_of lthy) n
  11.393 +              in Context.proof_map 
  11.394 +                  (update_declinfo (Morphism.term phi (Free (n,nT)),v))  
  11.395 +              end;
  11.396 +          in ctxt |> fold upd updates end;
  11.397 +
  11.398 +      in Context.mapping I upd_prf ctxt end;
  11.399 +
  11.400 +   fun string_of_typ T = 
  11.401 +      setmp show_sorts true 
  11.402 +       (setmp print_mode [] (Syntax.string_of_typ (ProofContext.init thy))) T;
  11.403 +   val fixestate = (case state_type of
  11.404 +         NONE => []
  11.405 +       | SOME s => 
  11.406 +          let 
  11.407 +	    val fx = Element.Fixes [(s,SOME (string_of_typ stateT),NoSyn)];
  11.408 +            val cs = Element.Constrains 
  11.409 +                       (map (fn (n,T) =>  (n,string_of_typ T))
  11.410 +                         ((map (fn (n,_) => (n,nameT)) all_comps) @
  11.411 +                          constrains))
  11.412 +          in [fx,cs] end
  11.413 +       )
  11.414 +
  11.415 +   
  11.416 +  in thy 
  11.417 +     |> namespace_definition 
  11.418 +           (suffix namespaceN name) nameT parents_expr 
  11.419 +           (map fst parent_comps) (map fst components)
  11.420 +     |> Context.theory_map (add_statespace full_name args parents components [])
  11.421 +     |> Locale.add_locale_i (SOME "") (suffix valuetypesN name) (Locale.Merge locs) 
  11.422 +            [Element.Constrains constrains]
  11.423 +     |> ProofContext.theory_of o #2
  11.424 +     |> fold interprete_parent_valuetypes parents 
  11.425 +     |> Locale.add_locale (SOME "") name 
  11.426 +              (Locale.Merge [Locale.Locale (suffix namespaceN full_name)
  11.427 +                            ,Locale.Locale (suffix valuetypesN full_name)]) fixestate
  11.428 +     |> ProofContext.theory_of o #2
  11.429 +     |> fold interprete_parent parents
  11.430 +     |> add_declaration (SOME full_name) (declare_declinfo components')
  11.431 +  end;
  11.432 +
  11.433 +
  11.434 +(* prepare arguments *)
  11.435 +
  11.436 +fun read_raw_parent sg s =
  11.437 +  (case Sign.read_typ_abbrev sg s handle TYPE (msg, _, _) => error msg of
  11.438 +    Type (name, Ts) => (Ts, name)
  11.439 +  | _ => error ("Bad parent statespace specification: " ^ quote s));
  11.440 +
  11.441 +fun read_typ sg s env  =
  11.442 +  let
  11.443 +    fun def_sort (x, ~1) = AList.lookup (op =) env x
  11.444 +      | def_sort _ = NONE;
  11.445 +    val T = Type.no_tvars (Sign.read_def_typ (sg, def_sort) s) handle TYPE (msg, _, _) => error msg;
  11.446 +  in (T, Term.add_typ_tfrees (T, env)) end;
  11.447 +
  11.448 +fun cert_typ sg raw_T env =
  11.449 +  let val T = Type.no_tvars (Sign.certify_typ sg raw_T) handle TYPE (msg, _, _) => error msg
  11.450 +  in (T, Term.add_typ_tfrees (T, env)) end;
  11.451 +
  11.452 +
  11.453 +
  11.454 +
  11.455 +fun gen_define_statespace prep_typ state_space args name parents comps thy =
  11.456 +  let (* - args distinct
  11.457 +         - only args may occur in comps and parent-instantiations
  11.458 +         - number of insts must match parent args 
  11.459 +         - no duplicate renamings
  11.460 +         - renaming should occur in namespace
  11.461 +      *)
  11.462 +    val _ = message ("Defining statespace " ^ quote name ^ " ...");
  11.463 +
  11.464 +    fun add_parent (Ts,pname,rs) env =
  11.465 +      let
  11.466 +        val full_pname = Sign.full_name thy pname;
  11.467 +        val {args,components,...} = 
  11.468 +              (case get_statespace (Context.Theory thy) full_pname of
  11.469 +                SOME r => r
  11.470 +               | NONE => error ("Undefined statespace " ^ quote pname));
  11.471 +
  11.472 +
  11.473 +        val (Ts',env') = fold_map (prep_typ thy) Ts env
  11.474 +            handle ERROR msg => cat_error msg 
  11.475 +                    ("The error(s) above occured in parent statespace specification " 
  11.476 +                    ^ quote pname);
  11.477 +        val err_insts = if length args <> length Ts' then
  11.478 +            ["number of type instantiation(s) does not match arguments of parent statespace "
  11.479 +              ^ quote pname]
  11.480 +            else [];
  11.481 +        
  11.482 +        val rnames = map fst rs
  11.483 +        val err_dup_renamings = (case duplicates (op =) rnames of
  11.484 +             [] => []
  11.485 +            | dups => ["Duplicate renaming(s) for " ^ commas dups])
  11.486 +
  11.487 +        val cnames = map fst components;
  11.488 +        val err_rename_unknowns = (case (filter (fn n => not (n mem cnames))) rnames of
  11.489 +              [] => []
  11.490 +             | rs => ["Unknown components " ^ commas rs]);
  11.491 +              
  11.492 +
  11.493 +        val rs' = map (AList.lookup (op =) rs o fst) components;
  11.494 +        val errs =err_insts @ err_dup_renamings @ err_rename_unknowns
  11.495 +      in if null errs then ((Ts',full_pname,rs'),env')
  11.496 +         else error (cat_lines (errs @ ["in parent statespace " ^ quote pname]))
  11.497 +      end;
  11.498 + 
  11.499 +    val (parents',env) = fold_map add_parent parents [];
  11.500 +
  11.501 +    val err_dup_args =
  11.502 +         (case duplicates (op =) args of
  11.503 +            [] => []
  11.504 +          | dups => ["Duplicate type argument(s) " ^ commas dups]);
  11.505 +    
  11.506 +
  11.507 +    val err_dup_components = 
  11.508 +         (case duplicates (op =) (map fst comps) of
  11.509 +           [] => []
  11.510 +          | dups => ["Duplicate state-space components " ^ commas dups]);
  11.511 +
  11.512 +    fun prep_comp (n,T) env =
  11.513 +      let val (T', env') = prep_typ thy T env handle ERROR msg =>
  11.514 +       cat_error msg ("The error(s) above occured in component " ^ quote n)
  11.515 +      in ((n,T'), env') end;
  11.516 +
  11.517 +    val (comps',env') = fold_map prep_comp comps env;
  11.518 +
  11.519 +    val err_extra_frees =
  11.520 +      (case subtract (op =) args (map fst env') of
  11.521 +        [] => []
  11.522 +      | extras => ["Extra free type variable(s) " ^ commas extras]);
  11.523 +
  11.524 +    val defaultS = Sign.defaultS thy;
  11.525 +    val args' = map (fn x => (x, AList.lookup (op =) env x |> the_default defaultS)) args;
  11.526 +
  11.527 +
  11.528 +    fun fst_eq ((x:string,_),(y,_)) = x = y;
  11.529 +    fun snd_eq ((_,t:typ),(_,u)) = t = u;              
  11.530 +
  11.531 +    val raw_parent_comps = (List.concat (map (parent_components thy) parents'));
  11.532 +    fun check_type (n,T) = 
  11.533 +          (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
  11.534 +             []  => []
  11.535 +           | [_] => []
  11.536 +           | rs  => ["Different types for component " ^ n ^": " ^ commas 
  11.537 +                       (map (Pretty.string_of o Display.pretty_ctyp o ctyp_of thy o snd) rs)])
  11.538 +                           
  11.539 +    val err_dup_types = List.concat (map check_type (duplicates fst_eq raw_parent_comps))
  11.540 +
  11.541 +    val parent_comps = distinct (fst_eq) raw_parent_comps;
  11.542 +    val all_comps = parent_comps @ comps';
  11.543 +    val err_comp_in_parent = (case duplicates (op =) (map fst all_comps) of
  11.544 +               [] => []
  11.545 +             | xs => ["Components already defined in parents: " ^ commas xs]);
  11.546 +    val errs = err_dup_args @ err_dup_components @ err_extra_frees @
  11.547 +               err_dup_types @ err_comp_in_parent;
  11.548 +
  11.549 +  in if null errs 
  11.550 +     then thy |> statespace_definition state_space args' name parents' parent_comps comps'
  11.551 +     else error (cat_lines errs) 
  11.552 +  end
  11.553 +  handle ERROR msg => cat_error msg ("Failed to define statespace " ^ quote name);
  11.554 + 
  11.555 +
  11.556 +val define_statespace = gen_define_statespace read_typ NONE;
  11.557 +val define_statespace_i = gen_define_statespace cert_typ;
  11.558 + 
  11.559 +
  11.560 +(*** parse/print - translations ***)
  11.561 +
  11.562 +
  11.563 +local
  11.564 +fun map_get_comp f ctxt (Free (name,_)) = 
  11.565 +      (case (get_comp ctxt name) of 
  11.566 +        SOME (T,_) => f T T dummyT 
  11.567 +      | NONE => (Syntax.free "arbitrary"(*; error "context not ready"*)))
  11.568 +  | map_get_comp _ _ _ = Syntax.free "arbitrary";
  11.569 +
  11.570 +val get_comp_projection = map_get_comp project_free;
  11.571 +val get_comp_injection  = map_get_comp inject_free;
  11.572 +
  11.573 +fun name_of (Free (n,_)) = n;
  11.574 +in
  11.575 +
  11.576 +fun gen_lookup_tr ctxt s n = 
  11.577 +      (case get_comp (Context.Proof ctxt) n of
  11.578 +        SOME (T,_) => 
  11.579 +           Syntax.const "StateFun.lookup"$Syntax.free (project_name T)$Syntax.free n$s
  11.580 +       | NONE => 
  11.581 +           if get_silent (Context.Proof ctxt)
  11.582 +	   then Syntax.const "StateFun.lookup"$Syntax.const "arbitrary"$Syntax.free n$s
  11.583 +           else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[]));
  11.584 +
  11.585 +fun lookup_tr ctxt [s,Free (n,_)] = gen_lookup_tr ctxt s n;
  11.586 +fun lookup_swap_tr ctxt [Free (n,_),s] = gen_lookup_tr ctxt s n;
  11.587 +
  11.588 +fun lookup_tr' ctxt [_$Free (prj,_),n as (_$Free (name,_)),s] =
  11.589 +     ( case get_comp (Context.Proof ctxt) name of
  11.590 +         SOME (T,_) =>  if prj=project_name T then
  11.591 +                           Syntax.const "_statespace_lookup" $ s $ n  
  11.592 +                        else raise Match
  11.593 +      | NONE => raise Match)
  11.594 +  | lookup_tr' _ ts = raise Match;
  11.595 +
  11.596 +fun gen_update_tr id ctxt n v s = 
  11.597 +  let
  11.598 +    fun pname T = if id then "Fun.id" else project_name T
  11.599 +    fun iname T = if id then "Fun.id" else inject_name T
  11.600 +   in
  11.601 +     (case get_comp (Context.Proof ctxt) n of
  11.602 +       SOME (T,_) => Syntax.const "StateFun.update"$
  11.603 +                   Syntax.free (pname T)$Syntax.free (iname T)$
  11.604 +                   Syntax.free n$(Syntax.const KN $ v)$s
  11.605 +      | NONE => 
  11.606 +         if get_silent (Context.Proof ctxt) 
  11.607 +         then Syntax.const "StateFun.update"$
  11.608 +                   Syntax.const "arbitrary"$Syntax.const "arbitrary"$
  11.609 +                   Syntax.free n$(Syntax.const KN $ v)$s
  11.610 +         else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined",[]))
  11.611 +   end;
  11.612 +
  11.613 +fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s;
  11.614 +
  11.615 +fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] =
  11.616 +     if NameSpace.base k = NameSpace.base KN then
  11.617 +        (case get_comp (Context.Proof ctxt) name of
  11.618 +          SOME (T,_) => if inj=inject_name T andalso prj=project_name T then
  11.619 +                           Syntax.const "_statespace_update" $ s $ n $ v  
  11.620 +                        else raise Match
  11.621 +         | NONE => raise Match)
  11.622 +     else raise Match
  11.623 +  | update_tr' _ _ = raise Match;
  11.624 +
  11.625 +end;
  11.626 +
  11.627 +
  11.628 +(*** outer syntax *)
  11.629 +
  11.630 +local structure P = OuterParse and K = OuterKeyword in
  11.631 +
  11.632 +val type_insts =
  11.633 +  P.typ >> single ||
  11.634 +  P.$$$ "(" |-- P.!!! (P.list1 P.typ --| P.$$$ ")") 
  11.635 +
  11.636 +val comp = P.name -- (P.$$$ "::" |-- P.!!! P.typ);
  11.637 +fun plus1_unless test scan =
  11.638 +  scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::;
  11.639 +
  11.640 +val mapsto = P.$$$ "=";
  11.641 +val rename = P.name -- (mapsto |-- P.name);
  11.642 +val renames =  Scan.optional (P.$$$ "[" |-- P.!!! (P.list1 rename --| P.$$$ "]")) [];
  11.643 +
  11.644 +
  11.645 +val parent = ((type_insts -- P.xname) || (P.xname >> pair [])) -- renames
  11.646 +             >> (fn ((insts,name),renames) => (insts,name,renames))
  11.647 +
  11.648 +
  11.649 +val statespace_decl =
  11.650 +   P.type_args -- P.name --
  11.651 +    (P.$$$ "=" |-- 
  11.652 +     ((Scan.repeat1 comp >> pair []) ||
  11.653 +      (plus1_unless comp parent --
  11.654 +        Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 comp)) [])))
  11.655 +
  11.656 +val statespace_command =
  11.657 +  OuterSyntax.command "statespace" "define state space" K.thy_decl
  11.658 +  (statespace_decl >> (fn ((args,name),(parents,comps)) => 
  11.659 +                           Toplevel.theory (define_statespace args name parents comps)))
  11.660 +
  11.661 +end;
  11.662 +
  11.663 +end;
  11.664 \ No newline at end of file