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