# HG changeset patch # User schirmer # Date 1193243769 -7200 # Node ID 4a9c25bffc9b4b7a413309449c7378cf85767264 # Parent bd06fd396fd0f357af69aad5dfa5044d71a7586c added Statespace library diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Oct 24 18:32:53 2007 +0200 +++ b/src/HOL/IsaMakefile Wed Oct 24 18:36:09 2007 +0200 @@ -37,6 +37,7 @@ HOL-NumberTheory \ HOL-Prolog \ HOL-SET-Protocol \ + HOL-Statespace \ HOL-Subst \ TLA-Buffer \ TLA-Inc \ @@ -845,6 +846,17 @@ Word/Examples/WordExamples.thy @cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples +## HOL-Statespace + +HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz + +$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy \ + Statespace/StateFun.thy Statespace/StateSpaceLocale.thy \ + Statespace/StateSpaceSyntax.thy StateSpace/StateSpaceEx.thy \ + Statespace/distinct_tree_prover.ML Statespace/state_space.ML \ + Statespace/state_fun.ML \ + Statespace/document/root.tex + @$(ISATOOL) usedir -g true $(OUT)/HOL Statespace ## clean diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/Statespace/DistinctTreeProver.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Wed Oct 24 18:36:09 2007 +0200 @@ -0,0 +1,726 @@ +(* Title: DistinctTreeProver.thy + ID: $Id$ + Author: Norbert Schirmer, TU Muenchen +*) + +header {* Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}*} + +theory DistinctTreeProver +imports Main +uses (distinct_tree_prover) +begin + +text {* A state space manages a set of (abstract) names and assumes +that the names are distinct. The names are stored as parameters of a +locale and distinctness as an assumption. The most common request is +to proof distinctness of two given names. We maintain the names in a +balanced binary tree and formulate a predicate that all nodes in the +tree have distinct names. This setup leads to logarithmic certificates. +*} + +subsection {* The Binary Tree *} + +datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip + + +text {* The boolean flag in the node marks the content of the node as +deleted, without having to build a new tree. We prefer the boolean +flag to an option type, so that the ML-layer can still use the node +content to facilitate binary search in the tree. The ML code keeps the +nodes sorted using the term order. We do not have to push ordering to +the HOL level. *} + +subsection {* Distinctness of Nodes *} + + +consts set_of:: "'a tree \ 'a set" +primrec +"set_of Tip = {}" +"set_of (Node l x d r) = (if d then {} else {x}) \ set_of l \ set_of r" + +consts all_distinct:: "'a tree \ bool" +primrec +"all_distinct Tip = True" +"all_distinct (Node l x d r) = ((d \ (x \ set_of l \ x \ set_of r)) \ + set_of l \ set_of r = {} \ + all_distinct l \ all_distinct r)" + +text {* Given a binary tree @{term "t"} for which +@{const all_distinct} holds, given two different nodes contained in the tree, +we want to write a ML function that generates a logarithmic +certificate that the content of the nodes is distinct. We use the +following lemmas to achieve this. *} + +lemma all_distinct_left: +"all_distinct (Node l x b r) \ all_distinct l" + by simp + +lemma all_distinct_right: "all_distinct (Node l x b r) \ all_distinct r" + by simp + +lemma distinct_left: "\all_distinct (Node l x False r); y \ set_of l \ \ x\y" + by auto + +lemma distinct_right: "\all_distinct (Node l x False r); y \ set_of r \ \ x\y" + by auto + +lemma distinct_left_right: "\all_distinct (Node l z b r); x \ set_of l; y \ set_of r\ + \ x\y" + by auto + +lemma in_set_root: "x \ set_of (Node l x False r)" + by simp + +lemma in_set_left: "y \ set_of l \ y \ set_of (Node l x False r)" + by simp + +lemma in_set_right: "y \ set_of r \ y \ set_of (Node l x False r)" + by simp + +lemma swap_neq: "x \ y \ y \ x" + by blast + +lemma neq_to_eq_False: "x\y \ (x=y)\False" + by simp + +subsection {* Containment of Trees *} + +text {* When deriving a state space from other ones, we create a new +name tree which contains all the names of the parent state spaces and +assumme the predicate @{const all_distinct}. We then prove that the new locale +interprets all parent locales. Hence we have to show that the new +distinctness assumption on all names implies the distinctness +assumptions of the parent locales. This proof is implemented in ML. We +do this efficiently by defining a kind of containment check of trees +by 'subtraction'. We subtract the parent tree from the new tree. If this +succeeds we know that @{const all_distinct} of the new tree implies +@{const all_distinct} of the parent tree. The resulting certificate is +of the order @{term "n * log(m)"} where @{term "n"} is the size of the +(smaller) parent tree and @{term "m"} the size of the (bigger) new tree. +*} + + +consts "delete" :: "'a \ 'a tree \ 'a tree option" +primrec +"delete x Tip = None" +"delete x (Node l y d r) = (case delete x l of + Some l' \ + (case delete x r of + Some r' \ Some (Node l' y (d \ (x=y)) r') + | None \ Some (Node l' y (d \ (x=y)) r)) + | None \ + (case (delete x r) of + Some r' \ Some (Node l y (d \ (x=y)) r') + | None \ if x=y \ \d then Some (Node l y True r) + else None))" + + +lemma delete_Some_set_of: "\t'. delete x t = Some t' \ set_of t' \ set_of t" +proof (induct t) + case Tip thus ?case by simp +next + case (Node l y d r) + have del: "delete x (Node l y d r) = Some t'". + show ?case + proof (cases "delete x l") + case (Some l') + note x_l_Some = this + with Node.hyps + have l'_l: "set_of l' \ set_of l" + by simp + show ?thesis + proof (cases "delete x r") + case (Some r') + with Node.hyps + have "set_of r' \ set_of r" + by simp + with l'_l Some x_l_Some del + show ?thesis + by (auto split: split_if_asm) + next + case None + with l'_l Some x_l_Some del + show ?thesis + by (fastsimp split: split_if_asm) + qed + next + case None + note x_l_None = this + show ?thesis + proof (cases "delete x r") + case (Some r') + with Node.hyps + have "set_of r' \ set_of r" + by simp + with Some x_l_None del + show ?thesis + by (fastsimp split: split_if_asm) + next + case None + with x_l_None del + show ?thesis + by (fastsimp split: split_if_asm) + qed + qed +qed + +lemma delete_Some_all_distinct: +"\t'. \delete x t = Some t'; all_distinct t\ \ all_distinct t'" +proof (induct t) + case Tip thus ?case by simp +next + case (Node l y d r) + have del: "delete x (Node l y d r) = Some t'". + have "all_distinct (Node l y d r)". + then obtain + dist_l: "all_distinct l" and + dist_r: "all_distinct r" and + d: "d \ (y \ set_of l \ y \ set_of r)" and + dist_l_r: "set_of l \ set_of r = {}" + by auto + show ?case + proof (cases "delete x l") + case (Some l') + note x_l_Some = this + from Node.hyps (1) [OF Some dist_l] + have dist_l': "all_distinct l'" + by simp + from delete_Some_set_of [OF x_l_Some] + have l'_l: "set_of l' \ set_of l". + show ?thesis + proof (cases "delete x r") + case (Some r') + from Node.hyps (2) [OF Some dist_r] + have dist_r': "all_distinct r'" + by simp + from delete_Some_set_of [OF Some] + have "set_of r' \ set_of r". + + with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r + show ?thesis + by fastsimp + next + case None + with l'_l dist_l' x_l_Some del d dist_l_r dist_r + show ?thesis + by fastsimp + qed + next + case None + note x_l_None = this + show ?thesis + proof (cases "delete x r") + case (Some r') + with Node.hyps (2) [OF Some dist_r] + have dist_r': "all_distinct r'" + by simp + from delete_Some_set_of [OF Some] + have "set_of r' \ set_of r". + with Some dist_r' x_l_None del dist_l d dist_l_r + show ?thesis + by fastsimp + next + case None + with x_l_None del dist_l dist_r d dist_l_r + show ?thesis + by (fastsimp split: split_if_asm) + qed + qed +qed + +lemma delete_None_set_of_conv: "delete x t = None = (x \ set_of t)" +proof (induct t) + case Tip thus ?case by simp +next + case (Node l y d r) + thus ?case + by (auto split: option.splits) +qed + +lemma delete_Some_x_set_of: + "\t'. delete x t = Some t' \ x \ set_of t \ x \ set_of t'" +proof (induct t) + case Tip thus ?case by simp +next + case (Node l y d r) + have del: "delete x (Node l y d r) = Some t'". + show ?case + proof (cases "delete x l") + case (Some l') + note x_l_Some = this + from Node.hyps (1) [OF Some] + obtain x_l: "x \ set_of l" "x \ set_of l'" + by simp + show ?thesis + proof (cases "delete x r") + case (Some r') + from Node.hyps (2) [OF Some] + obtain x_r: "x \ set_of r" "x \ set_of r'" + by simp + from x_r x_l Some x_l_Some del + show ?thesis + by (clarsimp split: split_if_asm) + next + case None + then have "x \ set_of r" + by (simp add: delete_None_set_of_conv) + with x_l None x_l_Some del + show ?thesis + by (clarsimp split: split_if_asm) + qed + next + case None + note x_l_None = this + then have x_notin_l: "x \ set_of l" + by (simp add: delete_None_set_of_conv) + show ?thesis + proof (cases "delete x r") + case (Some r') + from Node.hyps (2) [OF Some] + obtain x_r: "x \ set_of r" "x \ set_of r'" + by simp + from x_r x_notin_l Some x_l_None del + show ?thesis + by (clarsimp split: split_if_asm) + next + case None + then have "x \ set_of r" + by (simp add: delete_None_set_of_conv) + with None x_l_None x_notin_l del + show ?thesis + by (clarsimp split: split_if_asm) + qed + qed +qed + + +consts "subtract" :: "'a tree \ 'a tree \ 'a tree option" +primrec +"subtract Tip t = Some t" +"subtract (Node l x b r) t = + (case delete x t of + Some t' \ (case subtract l t' of + Some t'' \ subtract r t'' + | None \ None) + | None \ None)" + +lemma subtract_Some_set_of_res: + "\t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \ set_of t \ set_of t\<^isub>2" +proof (induct t\<^isub>1) + case Tip thus ?case by simp +next + case (Node l x b r) + have sub: "subtract (Node l x b r) t\<^isub>2 = Some t". + show ?case + proof (cases "delete x t\<^isub>2") + case (Some t\<^isub>2') + note del_x_Some = this + from delete_Some_set_of [OF Some] + have t2'_t2: "set_of t\<^isub>2' \ set_of t\<^isub>2" . + show ?thesis + proof (cases "subtract l t\<^isub>2'") + case (Some t\<^isub>2'') + note sub_l_Some = this + from Node.hyps (1) [OF Some] + have t2''_t2': "set_of t\<^isub>2'' \ set_of t\<^isub>2'" . + show ?thesis + proof (cases "subtract r t\<^isub>2''") + case (Some t\<^isub>2''') + from Node.hyps (2) [OF Some ] + have "set_of t\<^isub>2''' \ set_of t\<^isub>2''" . + with Some sub_l_Some del_x_Some sub t2''_t2' t2'_t2 + show ?thesis + by simp + next + case None + with del_x_Some sub_l_Some sub + show ?thesis + by simp + qed + next + case None + with del_x_Some sub + show ?thesis + by simp + qed + next + case None + with sub show ?thesis by simp + qed +qed + +lemma subtract_Some_set_of: + "\t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \ set_of t\<^isub>1 \ set_of t\<^isub>2" +proof (induct t\<^isub>1) + case Tip thus ?case by simp +next + case (Node l x d r) + have sub: "subtract (Node l x d r) t\<^isub>2 = Some t". + show ?case + proof (cases "delete x t\<^isub>2") + case (Some t\<^isub>2') + note del_x_Some = this + from delete_Some_set_of [OF Some] + have t2'_t2: "set_of t\<^isub>2' \ set_of t\<^isub>2" . + from delete_None_set_of_conv [of x t\<^isub>2] Some + have x_t2: "x \ set_of t\<^isub>2" + by simp + show ?thesis + proof (cases "subtract l t\<^isub>2'") + case (Some t\<^isub>2'') + note sub_l_Some = this + from Node.hyps (1) [OF Some] + have l_t2': "set_of l \ set_of t\<^isub>2'" . + from subtract_Some_set_of_res [OF Some] + have t2''_t2': "set_of t\<^isub>2'' \ set_of t\<^isub>2'" . + show ?thesis + proof (cases "subtract r t\<^isub>2''") + case (Some t\<^isub>2''') + from Node.hyps (2) [OF Some ] + have r_t\<^isub>2'': "set_of r \ set_of t\<^isub>2''" . + from Some sub_l_Some del_x_Some sub r_t\<^isub>2'' l_t2' t2'_t2 t2''_t2' x_t2 + show ?thesis + by auto + next + case None + with del_x_Some sub_l_Some sub + show ?thesis + by simp + qed + next + case None + with del_x_Some sub + show ?thesis + by simp + qed + next + case None + with sub show ?thesis by simp + qed +qed + +lemma subtract_Some_all_distinct_res: + "\t\<^isub>2 t. \subtract t\<^isub>1 t\<^isub>2 = Some t; all_distinct t\<^isub>2\ \ all_distinct t" +proof (induct t\<^isub>1) + case Tip thus ?case by simp +next + case (Node l x d r) + have sub: "subtract (Node l x d r) t\<^isub>2 = Some t". + have dist_t2: "all_distinct t\<^isub>2". + show ?case + proof (cases "delete x t\<^isub>2") + case (Some t\<^isub>2') + note del_x_Some = this + from delete_Some_all_distinct [OF Some dist_t2] + have dist_t2': "all_distinct t\<^isub>2'" . + show ?thesis + proof (cases "subtract l t\<^isub>2'") + case (Some t\<^isub>2'') + note sub_l_Some = this + from Node.hyps (1) [OF Some dist_t2'] + have dist_t2'': "all_distinct t\<^isub>2''" . + show ?thesis + proof (cases "subtract r t\<^isub>2''") + case (Some t\<^isub>2''') + from Node.hyps (2) [OF Some dist_t2''] + have dist_t2''': "all_distinct t\<^isub>2'''" . + from Some sub_l_Some del_x_Some sub + dist_t2''' + show ?thesis + by simp + next + case None + with del_x_Some sub_l_Some sub + show ?thesis + by simp + qed + next + case None + with del_x_Some sub + show ?thesis + by simp + qed + next + case None + with sub show ?thesis by simp + qed +qed + + +lemma subtract_Some_dist_res: + "\t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \ set_of t\<^isub>1 \ set_of t = {}" +proof (induct t\<^isub>1) + case Tip thus ?case by simp +next + case (Node l x d r) + have sub: "subtract (Node l x d r) t\<^isub>2 = Some t". + show ?case + proof (cases "delete x t\<^isub>2") + case (Some t\<^isub>2') + note del_x_Some = this + from delete_Some_x_set_of [OF Some] + obtain x_t2: "x \ set_of t\<^isub>2" and x_not_t2': "x \ set_of t\<^isub>2'" + by simp + from delete_Some_set_of [OF Some] + have t2'_t2: "set_of t\<^isub>2' \ set_of t\<^isub>2" . + show ?thesis + proof (cases "subtract l t\<^isub>2'") + case (Some t\<^isub>2'') + note sub_l_Some = this + from Node.hyps (1) [OF Some ] + have dist_l_t2'': "set_of l \ set_of t\<^isub>2'' = {}". + from subtract_Some_set_of_res [OF Some] + have t2''_t2': "set_of t\<^isub>2'' \ set_of t\<^isub>2'" . + show ?thesis + proof (cases "subtract r t\<^isub>2''") + case (Some t\<^isub>2''') + from Node.hyps (2) [OF Some] + have dist_r_t2''': "set_of r \ set_of t\<^isub>2''' = {}" . + from subtract_Some_set_of_res [OF Some] + have t2'''_t2'': "set_of t\<^isub>2''' \ set_of t\<^isub>2''". + + from Some sub_l_Some del_x_Some sub t2'''_t2'' dist_l_t2'' dist_r_t2''' + t2''_t2' t2'_t2 x_not_t2' + show ?thesis + by auto + next + case None + with del_x_Some sub_l_Some sub + show ?thesis + by simp + qed + next + case None + with del_x_Some sub + show ?thesis + by simp + qed + next + case None + with sub show ?thesis by simp + qed +qed + +lemma subtract_Some_all_distinct: + "\t\<^isub>2 t. \subtract t\<^isub>1 t\<^isub>2 = Some t; all_distinct t\<^isub>2\ \ all_distinct t\<^isub>1" +proof (induct t\<^isub>1) + case Tip thus ?case by simp +next + case (Node l x d r) + have sub: "subtract (Node l x d r) t\<^isub>2 = Some t". + have dist_t2: "all_distinct t\<^isub>2". + show ?case + proof (cases "delete x t\<^isub>2") + case (Some t\<^isub>2') + note del_x_Some = this + from delete_Some_all_distinct [OF Some dist_t2 ] + have dist_t2': "all_distinct t\<^isub>2'" . + from delete_Some_set_of [OF Some] + have t2'_t2: "set_of t\<^isub>2' \ set_of t\<^isub>2" . + from delete_Some_x_set_of [OF Some] + obtain x_t2: "x \ set_of t\<^isub>2" and x_not_t2': "x \ set_of t\<^isub>2'" + by simp + + show ?thesis + proof (cases "subtract l t\<^isub>2'") + case (Some t\<^isub>2'') + note sub_l_Some = this + from Node.hyps (1) [OF Some dist_t2' ] + have dist_l: "all_distinct l" . + from subtract_Some_all_distinct_res [OF Some dist_t2'] + have dist_t2'': "all_distinct t\<^isub>2''" . + from subtract_Some_set_of [OF Some] + have l_t2': "set_of l \ set_of t\<^isub>2'" . + from subtract_Some_set_of_res [OF Some] + have t2''_t2': "set_of t\<^isub>2'' \ set_of t\<^isub>2'" . + from subtract_Some_dist_res [OF Some] + have dist_l_t2'': "set_of l \ set_of t\<^isub>2'' = {}". + show ?thesis + proof (cases "subtract r t\<^isub>2''") + case (Some t\<^isub>2''') + from Node.hyps (2) [OF Some dist_t2''] + have dist_r: "all_distinct r" . + from subtract_Some_set_of [OF Some] + have r_t2'': "set_of r \ set_of t\<^isub>2''" . + from subtract_Some_dist_res [OF Some] + have dist_r_t2''': "set_of r \ set_of t\<^isub>2''' = {}". + + from dist_l dist_r Some sub_l_Some del_x_Some r_t2'' l_t2' x_t2 x_not_t2' + t2''_t2' dist_l_t2'' dist_r_t2''' + show ?thesis + by auto + next + case None + with del_x_Some sub_l_Some sub + show ?thesis + by simp + qed + next + case None + with del_x_Some sub + show ?thesis + by simp + qed + next + case None + with sub show ?thesis by simp + qed +qed + + +lemma delete_left: + assumes dist: "all_distinct (Node l y d r)" + assumes del_l: "delete x l = Some l'" + shows "delete x (Node l y d r) = Some (Node l' y d r)" +proof - + from delete_Some_x_set_of [OF del_l] + obtain "x \ set_of l" + by simp + moreover with dist + have "delete x r = None" + by (cases "delete x r") (auto dest:delete_Some_x_set_of) + + ultimately + show ?thesis + using del_l dist + by (auto split: option.splits) +qed + +lemma delete_right: + assumes dist: "all_distinct (Node l y d r)" + assumes del_r: "delete x r = Some r'" + shows "delete x (Node l y d r) = Some (Node l y d r')" +proof - + from delete_Some_x_set_of [OF del_r] + obtain "x \ set_of r" + by simp + moreover with dist + have "delete x l = None" + by (cases "delete x l") (auto dest:delete_Some_x_set_of) + + ultimately + show ?thesis + using del_r dist + by (auto split: option.splits) +qed + +lemma delete_root: + assumes dist: "all_distinct (Node l x False r)" + shows "delete x (Node l x False r) = Some (Node l x True r)" +proof - + from dist have "delete x r = None" + by (cases "delete x r") (auto dest:delete_Some_x_set_of) + moreover + from dist have "delete x l = None" + by (cases "delete x l") (auto dest:delete_Some_x_set_of) + ultimately show ?thesis + using dist + by (auto split: option.splits) +qed + +lemma subtract_Node: + assumes del: "delete x t = Some t'" + assumes sub_l: "subtract l t' = Some t''" + assumes sub_r: "subtract r t'' = Some t'''" + shows "subtract (Node l x False r) t = Some t'''" +using del sub_l sub_r +by simp + +lemma subtract_Tip: "subtract Tip t = Some t" + by simp + +text {* Now we have all the theorems in place that are needed for the +certificate generating ML functions. *} + +use distinct_tree_prover + +(* Uncomment for profiling or debugging *) +(* +ML {* +(* +val nums = (0 upto 10000); +val nums' = (200 upto 3000); +*) +val nums = (0 upto 10000); +val nums' = (0 upto 3000); +val const_decls = map (fn i => Syntax.no_syn + ("const" ^ string_of_int i,Type ("nat",[]))) nums + +val consts = sort Term.fast_term_ord + (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums) +val consts' = sort Term.fast_term_ord + (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums') + +val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts + + +val t' = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts' + + +val dist = + HOLogic.Trueprop$ + (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t) + +val dist' = + HOLogic.Trueprop$ + (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t') + +val da = ref refl; + +*} + +setup {* +Theory.add_consts_i const_decls +#> (fn thy => let val ([thm],thy') = PureThy.add_axioms_i [(("dist_axiom",dist),[])] thy + in (da := thm; thy') end) +*} + + +ML {* + val ct' = cterm_of (the_context ()) t'; +*} + +ML {* + timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);())) +*} + +(* 590 s *) + +ML {* + + +val p1 = + the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const1",Type ("nat",[]))) t) +val p2 = + the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const10000",Type ("nat",[]))) t) +*} + + +ML {* timeit (fn () => DistinctTreeProver.distinctTreeProver (!da ) + p1 + p2)*} + + +ML {* timeit (fn () => (DistinctTreeProver.deleteProver (!da) p1;())) *} + + + + +ML {* +val cdist' = cterm_of (the_context ()) dist'; +DistinctTreeProver.distinct_implProver (!da) cdist'; +*} + +*) + + + + + + + + + + +end + diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/Statespace/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Statespace/ROOT.ML Wed Oct 24 18:36:09 2007 +0200 @@ -0,0 +1,1 @@ +use_thy "StateSpaceEx"; \ No newline at end of file diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/Statespace/StateFun.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Statespace/StateFun.thy Wed Oct 24 18:36:09 2007 +0200 @@ -0,0 +1,115 @@ +(* Title: StateFun.thy + ID: $Id$ + Author: Norbert Schirmer, TU Muenchen +*) + +header {* State Space Representation as Function \label{sec:StateFun}*} + +theory StateFun imports DistinctTreeProver +(*uses "state_space.ML" (state_fun)*) +begin + + +text {* The state space is represented as a function from names to +values. We neither fix the type of names nor the type of values. We +define lookup and update functions and provide simprocs that simplify +expressions containing these, similar to HOL-records. + +The lookup and update function get constructor/destructor functions as +parameters. These are used to embed various HOL-types into the +abstract value type. Conceptually the abstract value type is a sum of +all types that we attempt to store in the state space. + +The update is actually generalized to a map function. The map supplies +better compositionality, especially if you think of nested state +spaces. *} + +constdefs K_statefun:: "'a \ 'b \ 'a" "K_statefun c x \ c" + +lemma K_statefun_apply [simp]: "K_statefun c x = c" + by (simp add: K_statefun_def) + +lemma K_statefun_comp [simp]: "(K_statefun c \ f) = K_statefun c" + by (rule ext) (simp add: K_statefun_apply comp_def) + +lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x" + by (rule refl) + +constdefs lookup:: "('v \ 'a) \ 'n \ ('n \ 'v) \ 'a" +"lookup destr n s \ destr (s n)" + +constdefs update:: + "('v \ 'a1) \ ('a2 \ 'v) \ 'n \ ('a1 \ 'a2) \ ('n \ 'v) \ ('n \ 'v)" +"update destr constr n f s \ s(n := constr (f (destr (s n))))" + +lemma lookup_update_same: + "(\v. destr (constr v) = v) \ lookup destr n (update destr constr n f s) = + f (destr (s n))" + by (simp add: lookup_def update_def) + +lemma lookup_update_id_same: + "lookup destr n (update destr' id n (K_statefun (lookup id n s')) s) = + lookup destr n s'" + by (simp add: lookup_def update_def) + +lemma lookup_update_other: + "n\m \ lookup destr n (update destr' constr m f s) = lookup destr n s" + by (simp add: lookup_def update_def) + + +lemma id_id_cancel: "id (id x) = x" + by (simp add: id_def) + +lemma destr_contstr_comp_id: +"(\v. destr (constr v) = v) \ destr \ constr = id" + by (rule ext) simp + + + +lemma block_conj_cong: "(P \ Q) = (P \ Q)" + by simp + +lemma conj1_False: "(P\False) \ (P \ Q) \ False" + by simp + +lemma conj2_False: "\Q\False\ \ (P \ Q) \ False" + by simp + +lemma conj_True: "\P\True; Q\True\ \ (P \ Q) \ True" + by simp + +lemma conj_cong: "\P\P'; Q\Q'\ \ (P \ Q) \ (P' \ Q')" + by simp + + +lemma update_apply: "(update destr constr n f s x) = + (if x=n then constr (f (destr (s n))) else s x)" + by (simp add: update_def) + +lemma ex_id: "\x. id x = y" + by (simp add: id_def) + +lemma swap_ex_eq: + "\s. f s = x \ True \ + \s. x = f s \ True" + apply (rule eq_reflection) + apply auto + done + +lemmas meta_ext = eq_reflection [OF ext] + +(* This lemma only works if the store is welltyped: + "\x. s ''n'' = (c x)" + or in general when c (d x) = x, + (for example: c=id and d=id) + *) +lemma "update d c n (K_statespace (lookup d n s)) s = s" + apply (simp add: update_def lookup_def) + apply (rule ext) + apply simp + oops + +(*use "state_fun" +setup StateFun.setup +*) +end \ No newline at end of file diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/Statespace/StateSpaceEx.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Statespace/StateSpaceEx.thy Wed Oct 24 18:36:09 2007 +0200 @@ -0,0 +1,221 @@ +(* Title: StateSpaceEx.thy + ID: $Id$ + Author: Norbert Schirmer, TU Muenchen +*) + +header {* Examples \label{sec:Examples} *} +theory StateSpaceEx +imports StateSpaceLocale StateSpaceSyntax + +begin +(* FIXME: Use proper keywords file *) +(*<*) +syntax + "_statespace_updates" :: "('a \ 'b) \ updbinds \ ('a \ 'b)" ("_\_\" [900,0] 900) +(*>*) + +text {* Did you ever dream about records with multiple inheritance. +Then you should definitely have a look at statespaces. They may be +what you are dreaming of. Or at least almost... +*} + + + + +text {* Isabelle allows to add new top-level commands to the +system. Building on the locale infrastructure, we provide a command +\isacommand{statespace} like this:*} + +statespace vars = + n::nat + b::bool + +text {* \noindent This resembles a \isacommand{record} definition, +but introduces sophisticated locale +infrastructure instead of HOL type schemes. The resulting context +postulates two distinct names @{term "n"} and @{term "b"} and +projection~/ injection functions that convert from abstract values to +@{typ "nat"} and @{text "bool"}. The logical content of the locale is: *} + +locale vars' = + fixes n::'name and b::'name + assumes "distinct [n, b]" + + fixes project_nat::"'value \ nat" and inject_nat::"nat \ 'value" + assumes "\n. project_nat (inject_nat n) = n" + + fixes project_bool::"'value \ bool" and inject_bool::"bool \ 'value" + assumes "\b. project_bool (inject_bool b) = b" + +text {* \noindent The HOL predicate @{const "distinct"} describes +distinctness of all names in the context. Locale @{text "vars'"} +defines the raw logical content that is defined in the state space +locale. We also maintain non-logical context information to support +the user: + +\begin{itemize} + +\item Syntax for state lookup and updates that automatically inserts +the corresponding projection and injection functions. + +\item Setup for the proof tools that exploit the distinctness +information and the cancellation of projections and injections in +deductions and simplifications. + +\end{itemize} + +This extra-logical information is added to the locale in form of +declarations, which associate the name of a variable to the +corresponding projection and injection functions to handle the syntax +transformations, and a link from the variable name to the +corresponding distinctness theorem. As state spaces are merged or +extended there are multiple distinctness theorems in the context. Our +declarations take care that the link always points to the strongest +distinctness assumption. With these declarations in place, a lookup +can be written as @{text "s\n"}, which is translated to @{text +"project_nat (s n)"}, and an update as @{text "s\n := 2\"}, which is +translated to @{text "s(n := inject_nat 2)"}. We can now establish the +following lemma: *} + +lemma (in vars) foo: "s\b = s\b" by simp + +text {* \noindent Here the simplifier was able to refer to +distinctness of @{term "b"} and @{term "n"} to solve the equation. +The resulting lemma is also recorded in locale @{text "vars"} for +later use and is automatically propagated to all its interpretations. +Here is another example: *} + +statespace 'a varsX = vars [n=N, b=B] + vars + x::'a + +text {* \noindent The state space @{text "varsX"} imports two copies +of the state space @{text "vars"}, where one has the variables renamed +to upper-case letters, and adds another variable @{term "x"} of type +@{typ "'a"}. This type is fixed inside the state space but may get +instantiated later on, analogous to type parameters of an ML-functor. +The distinctness assumption is now @{text "distinct [N, B, n, b, x]"}, +from this we can derive both @{term "distinct [N,B]"} and @{term +"distinct [n,b]"}, the distinction assumptions for the two versions of +locale @{text "vars"} above. Moreover we have all necessary +projection and injection assumptions available. These assumptions +together allow us to establish state space @{term "varsX"} as an +interpretation of both instances of locale @{term "vars"}. Hence we +inherit both variants of theorem @{text "foo"}: @{text "s\N := 2\\B = +s\B"} as well as @{text "s\n := 2\\b = s\b"}. These are immediate +consequences of the locale interpretation action. + +The declarations for syntax and the distinctness theorems also observe +the morphisms generated by the locale package due to the renaming +@{term "n = N"}: *} + +lemma (in varsX) foo: "s\N := 2\\x = s\x" by simp + +text {* To assure scalability towards many distinct names, the +distinctness predicate is refined to operate on balanced trees. Thus +we get logarithmic certificates for the distinctness of two names by +the distinctness of the paths in the tree. Asked for the distinctness +of two names, our tool produces the paths of the variables in the tree +(this is implemented in SML, outside the logic) and returns a +certificate corresponding to the different paths. Merging state +spaces requires to prove that the combined distinctness assumption +implies the distinctness assumptions of the components. Such a proof +is of the order $m \cdot \log n$, where $n$ and $m$ are the number of +nodes in the larger and smaller tree, respectively.*} + +text {* We continue with more examples. *} + +statespace 'a foo = + f::"nat\nat" + a::int + b::nat + c::'a + + + +lemma (in foo) foo1: + shows "s\a := i\\a = i" + by simp + +lemma (in foo) foo2: + shows "(s\a:=i\)\a = i" + by simp + +lemma (in foo) foo3: + shows "(s\a:=i\)\b = s\b" + by simp + +lemma (in foo) foo4: + shows "(s\a:=i,b:=j,c:=k,a:=x\) = (s\b:=j,c:=k,a:=x\)" + by simp + +statespace bar = + b::bool + c::string + +lemma (in bar) bar1: + shows "(s\b:=True\)\c = s\c" + by simp + +text {* You can define a derived state space by inheriting existing state spaces, renaming +of components if you like, and by declaring new components. +*} + +statespace ('a,'b) loo = 'a foo + bar [b=B,c=C] + + X::'b + +lemma (in loo) loo1: + shows "s\a:=i\\B = s\B" +proof - + thm foo1 + txt {* The Lemma @{thm [source] foo1} from the parent state space + is also available here: \begin{center}@{thm foo1}\end{center}.*} + have "s\a = i" + by (rule foo1) + thm bar1 + txt {* Note the renaming of the parameters in Lemma @{thm [source] bar1}: + \begin{center}@{thm bar1}\end{center}.*} + have "s\C = s\C" + by (rule bar1) + show ?thesis + by simp +qed + + +statespace 'a dup = 'a foo [f=F, a=A] + 'a foo + + x::int + +lemma (in dup) + shows "s\x = s\x" + by simp + +lemma (in dup) + shows "s\a = s\a" + by simp + +lemma (in dup) + shows "s\x = s\x" + by simp + + +text {* There are known problems with syntax-declarations. They currently +only work, when the context is already built. Hopefully this will be +implemented correctly in future Isabelle versions. *} + +lemma + includes foo + shows True + term "s\a = i" + by simp + +(* +lemma + includes foo + shows "s\a = i" +*) + +text {* It would be nice to have nested state spaces. This is +logically no problem. From the locale-implementation side this may be +something like an 'includes' into a locale. When there is a more +elaborate locale infrastructure in place this may be an easy exercise. +*} + +end diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/Statespace/StateSpaceLocale.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Statespace/StateSpaceLocale.thy Wed Oct 24 18:36:09 2007 +0200 @@ -0,0 +1,40 @@ +(* Title: StateSpaceLocale.thy + ID: $Id$ + Author: Norbert Schirmer, TU Muenchen +*) + +header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*} + +theory StateSpaceLocale imports StateFun +uses "state_space.ML" "state_fun" +begin + +setup StateFun.setup + +text {* For every type that is to be stored in a state space, an +instance of this locale is imported in order convert the abstract and +concrete values.*} + + +locale project_inject = + fixes project :: "'value \ 'a" + and "inject":: "'a \ 'value" + assumes project_inject_cancel [statefun_simp]: "project (inject x) = x" + +lemma (in project_inject) + ex_project [statefun_simp]: "\v. project v = x" + apply (rule_tac x= "inject x" in exI) + apply (simp add: project_inject_cancel) + done + +lemma (in project_inject) + project_inject_comp_id [statefun_simp]: "project \ inject = id" + by (rule ext) (simp add: project_inject_cancel) + +lemma (in project_inject) + project_inject_comp_cancel[statefun_simp]: "f \ project \ inject = f" + by (rule ext) (simp add: project_inject_cancel) + + + +end \ No newline at end of file diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/Statespace/StateSpaceSyntax.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Statespace/StateSpaceSyntax.thy Wed Oct 24 18:36:09 2007 +0200 @@ -0,0 +1,42 @@ +(* Title: StateSpaceSyntax.thy + ID: $Id$ + Author: Norbert Schirmer, TU Muenchen +*) + +header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*} +theory StateSpaceSyntax +imports StateSpaceLocale + +begin + +text {* The state space syntax is kept in an extra theory so that you +can choose if you want to use it or not. *} + +syntax + "_statespace_lookup" :: "('a \ 'b) \ 'a \ 'c" ("_\_" [60,60] 60) + "_statespace_update" :: "('a \ 'b) \ 'a \ 'c \ ('a \ 'b)" + "_statespace_updates" :: "('a \ 'b) \ updbinds \ ('a \ 'b)" ("_<_>" [900,0] 900) + +translations + "_statespace_updates f (_updbinds b bs)" == + "_statespace_updates (_statespace_updates f b) bs" + "s" == "_statespace_update s x y" + + +parse_translation (advanced) +{* +[("_statespace_lookup",StateSpace.lookup_tr), + ("_get",StateSpace.lookup_tr), + ("_statespace_update",StateSpace.update_tr)] +*} + + +print_translation (advanced) +{* +[("lookup",StateSpace.lookup_tr'), + ("StateFun.lookup",StateSpace.lookup_tr'), + ("update",StateSpace.update_tr'), + ("StateFun.update",StateSpace.update_tr')] +*} + +end \ No newline at end of file diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/Statespace/distinct_tree_prover.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Wed Oct 24 18:36:09 2007 +0200 @@ -0,0 +1,349 @@ +(* Title: distinct_tree_prover.thy + ID: $Id$ + Author: Norbert Schirmer, TU Muenchen +*) + +structure DistinctTreeProver = +struct +val all_distinct_left = thm "DistinctTreeProver.all_distinct_left"; +val all_distinct_right = thm "DistinctTreeProver.all_distinct_right"; + +val distinct_left = thm "DistinctTreeProver.distinct_left"; +val distinct_right = thm "DistinctTreeProver.distinct_right"; +val distinct_left_right = thm "DistinctTreeProver.distinct_left_right"; +val in_set_root = thm "DistinctTreeProver.in_set_root"; +val in_set_left = thm "DistinctTreeProver.in_set_left"; +val in_set_right = thm "DistinctTreeProver.in_set_right"; + +val swap_neq = thm "DistinctTreeProver.swap_neq"; +val neq_to_eq_False = thm "DistinctTreeProver.neq_to_eq_False" + +fun treeT T = Type ("DistinctTreeProver.tree",[T]); +fun mk_tree' e T n [] = Const ("DistinctTreeProver.tree.Tip",treeT T) + | mk_tree' e T n xs = + let + val m = (n - 1) div 2; + val (xsl,x::xsr) = chop m xs; + val l = mk_tree' e T m xsl; + val r = mk_tree' e T (n-(m+1)) xsr; + in Const ("DistinctTreeProver.tree.Node", + treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $ + l$ e x $ HOLogic.false_const $ r + end + +fun mk_tree e T xs = mk_tree' e T (length xs) xs; + +fun dest_tree (Const ("DistinctTreeProver.tree.Tip",_)) = [] + | dest_tree (Const ("DistinctTreeProver.tree.Node",_)$l$e$_$r) = dest_tree l @ e :: dest_tree r + | dest_tree t = raise TERM ("DistinctTreeProver.dest_tree",[t]); + +datatype Direction = Left | Right + +fun lin_find_tree e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE + | lin_find_tree e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) = + if e aconv x + then SOME [] + else (case lin_find_tree e l of + SOME path => SOME (Left::path) + | NONE => (case lin_find_tree e r of + SOME path => SOME (Right::path) + | NONE => NONE)) + | lin_find_tree e t = raise TERM ("find_tree: input not a tree",[t]) + +fun bin_find_tree order e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE + | bin_find_tree order e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) = + (case order (e,x) of + EQUAL => SOME [] + | LESS => Option.map (cons Left) (bin_find_tree order e l) + | GREATER => Option.map (cons Right) (bin_find_tree order e r)) + | bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t]) + +fun find_tree e t = + (case bin_find_tree Term.fast_term_ord e t of + NONE => lin_find_tree e t + | x => x); + + +fun index_tree (Const ("DistinctTreeProver.tree.Tip",_)) path tab = tab + | index_tree (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) path tab = + tab + |> Termtab.update_new (x,path) + |> index_tree l (path@[Left]) + |> index_tree r (path@[Right]) + | index_tree t _ _ = raise TERM ("index_tree: input not a tree",[t]) + +fun split_common_prefix xs [] = ([],xs,[]) + | split_common_prefix [] ys = ([],[],ys) + | split_common_prefix (xs as (x::xs')) (ys as (y::ys')) = + if x=y + then let val (ps,xs'',ys'') = split_common_prefix xs' ys' in (x::ps,xs'',ys'') end + else ([],xs,ys) + + +(* Wrapper around Thm.instantiate. The type instiations of instTs are applied to + * the right hand sides of insts + *) +fun instantiate instTs insts = + let + val instTs' = map (fn (T,U) => (dest_TVar (typ_of T),typ_of U)) instTs; + fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T'); + fun mapT_and_recertify ct = + let + val thy = theory_of_cterm ct; + in (cterm_of thy (Term.map_types (Term.map_type_tvar substT) (term_of ct))) end; + val insts' = map (apfst mapT_and_recertify) insts; + in Thm.instantiate (instTs,insts') end; + +fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^ + quote (Term.string_of_vname ixn) ^ " has two distinct sorts", + [TVar (ixn, S), TVar (ixn, S')], []); + +fun lookup (tye, (ixn, S)) = + (case AList.lookup (op =) tye ixn of + NONE => NONE + | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S'); + +val naive_typ_match = + let + fun match (TVar (v, S), T) subs = + (case lookup (subs, (v, S)) of + NONE => ((v, (S, T))::subs) + | SOME _ => subs) + | match (Type (a, Ts), Type (b, Us)) subs = + if a <> b then raise Type.TYPE_MATCH + else matches (Ts, Us) subs + | match (TFree x, TFree y) subs = + if x = y then subs else raise Type.TYPE_MATCH + | match _ _ = raise Type.TYPE_MATCH + and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs) + | matches _ subs = subs; + in match end; + + +(* expects that relevant type variables are already contained in + * term variables. First instantiation of variables is returned without further + * checking. + *) +fun naive_cterm_first_order_match (t,ct) env = + let + val thy = (theory_of_cterm ct); + fun mtch (env as (tyinsts,insts)) = fn + (Var(ixn,T),ct) => + (case AList.lookup (op =) insts ixn of + NONE => (naive_typ_match (T,typ_of (ctyp_of_term ct)) tyinsts, + (ixn, ct)::insts) + | SOME _ => env) + | (f$t,ct) => let val (cf,ct') = Thm.dest_comb ct; + in mtch (mtch env (f,cf)) (t,ct') end + | _ => env + in mtch env (t,ct) end; + + +fun mp prem rule = implies_elim rule prem; + +fun discharge prems rule = + let + val thy = theory_of_thm (hd prems); + val (tyinsts,insts) = + fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([],[]); + + val tyinsts' = map (fn (v,(S,U)) => (ctyp_of thy (TVar (v,S)),ctyp_of thy U)) + tyinsts; + val insts' = map (fn (idxn,ct) => (cterm_of thy (Var (idxn,typ_of (ctyp_of_term ct))),ct)) + insts; + val rule' = Thm.instantiate (tyinsts',insts') rule; + in fold mp prems rule' end; + +local + +val (l_in_set_root,x_in_set_root,r_in_set_root) = + let val (Node_l_x_d,r) = (cprop_of in_set_root) + |> Thm.dest_comb |> #2 + |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb; + val (Node_l,x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb; + val l = Node_l |> Thm.dest_comb |> #2; + in (l,x,r) end +val (x_in_set_left,r_in_set_left) = + let val (Node_l_x_d,r) = (cprop_of in_set_left) + |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 + |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb; + val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2; + in (x,r) end + +val (x_in_set_right,l_in_set_right) = + let val (Node_l,x) = (cprop_of in_set_right) + |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 + |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 + |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1 + |> Thm.dest_comb + val l = Node_l |> Thm.dest_comb |> #2; + in (x,l) end + +in +(* +1. First get paths x_path y_path of x and y in the tree. +2. For the common prefix descend into the tree according to the path + and lemmas all_distinct_left/right +3. If one restpath is empty use distinct_left/right, + otherwise all_distinct_left_right +*) + +fun distinctTreeProver dist_thm x_path y_path = + let + fun dist_subtree [] thm = thm + | dist_subtree (p::ps) thm = + let + val rule = (case p of Left => all_distinct_left | Right => all_distinct_right) + in dist_subtree ps (discharge [thm] rule) end; + + val (ps,x_rest,y_rest) = split_common_prefix x_path y_path; + val dist_subtree_thm = dist_subtree ps dist_thm; + val subtree = cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; + val (_,[l,_,_,r]) = Drule.strip_comb subtree; + + fun in_set ps tree = + let + val (_,[l,x,_,r]) = Drule.strip_comb tree; + val xT = ctyp_of_term x; + in (case ps of + [] => instantiate + [(ctyp_of_term x_in_set_root,xT)] + [(l_in_set_root,l),(x_in_set_root,x),(r_in_set_root,r)] in_set_root + | (Left::ps') => + let + val in_set_l = in_set ps' l; + val in_set_left' = instantiate [(ctyp_of_term x_in_set_left,xT)] + [(x_in_set_left,x),(r_in_set_left,r)] in_set_left; + in discharge [in_set_l] in_set_left' end + | (Right::ps') => + let + val in_set_r = in_set ps' r; + val in_set_right' = instantiate [(ctyp_of_term x_in_set_right,xT)] + [(x_in_set_right,x),(l_in_set_right,l)] in_set_right; + in discharge [in_set_r] in_set_right' end) + end + + fun in_set' [] = raise TERM ("distinctTreeProver",[]) + | in_set' (Left::ps) = in_set ps l + | in_set' (Right::ps) = in_set ps r; + + fun distinct_lr node_in_set Left = discharge [dist_subtree_thm,node_in_set] distinct_left + | distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right + + val (swap,neq) = + (case x_rest of + [] => let + val y_in_set = in_set' y_rest; + in (false,distinct_lr y_in_set (hd y_rest)) end + | (xr::xrs) => + (case y_rest of + [] => let + val x_in_set = in_set' x_rest; + in (true,distinct_lr x_in_set (hd x_rest)) end + | (yr::yrs) => + let + val x_in_set = in_set' x_rest; + val y_in_set = in_set' y_rest; + in (case xr of + Left => (false, + discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right) + |Right => (true, + discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right)) + end + )) + in if swap then discharge [neq] swap_neq else neq + end + + +val delete_root = thm "DistinctTreeProver.delete_root"; +val delete_left = thm "DistinctTreeProver.delete_left"; +val delete_right = thm "DistinctTreeProver.delete_right"; + +fun deleteProver dist_thm [] = delete_root OF [dist_thm] + | deleteProver dist_thm (p::ps) = + let + val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right); + val dist_thm' = discharge [dist_thm] dist_rule + val del_rule = (case p of Left => delete_left | Right => delete_right) + val del = deleteProver dist_thm' ps; + in discharge [dist_thm, del] del_rule end; + +val subtract_Tip = thm "DistinctTreeProver.subtract_Tip"; +val subtract_Node = thm "DistinctTreeProver.subtract_Node"; +val delete_Some_all_distinct = thm "DistinctTreeProver.delete_Some_all_distinct"; +val subtract_Some_all_distinct_res = thm "DistinctTreeProver.subtract_Some_all_distinct_res"; + +local + val (alpha,v) = + let + val ct = subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 + |> Thm.dest_comb |> #2 + val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp; + in (alpha, #1 (dest_Var (term_of ct))) end; +in +fun subtractProver (Const ("DistinctTreeProver.tree.Tip",T)) ct dist_thm = + let + val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; + val thy = theory_of_cterm ct; + val [alphaI] = #2 (dest_Type T); + in Thm.instantiate ([(alpha,ctyp_of thy alphaI)], + [(cterm_of thy (Var (v,treeT alphaI)),ct')]) subtract_Tip + end + | subtractProver (Const ("DistinctTreeProver.tree.Node",nT)$l$x$d$r) ct dist_thm = + let + val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; + val (_,[cl,_,_,cr]) = Drule.strip_comb ct; + val ps = the (find_tree x (term_of ct')); + val del_tree = deleteProver dist_thm ps; + val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct; + val sub_l = subtractProver (term_of cl) cl (dist_thm'); + val sub_r = subtractProver (term_of cr) cr + (discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res); + in discharge [del_tree, sub_l, sub_r] subtract_Node end +end + +val subtract_Some_all_distinct = thm "DistinctTreeProver.subtract_Some_all_distinct"; +fun distinct_implProver dist_thm ct = + let + val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; + val sub = subtractProver (term_of ctree) ctree dist_thm; + in subtract_Some_all_distinct OF [sub, dist_thm] end; + +fun get_fst_success f [] = NONE + | get_fst_success f (x::xs) = (case f x of NONE => get_fst_success f xs + | SOME v => SOME v); + +fun neq_x_y ctxt x y name = + (let + val dist_thm = the (try (ProofContext.get_thm ctxt) (PureThy.Name name)); + val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; + val tree = term_of ctree; + val x_path = the (find_tree x tree); + val y_path = the (find_tree y tree); + val thm = distinctTreeProver dist_thm x_path y_path; + in SOME thm + end handle Option => NONE) + +fun distinctTree_tac names ctxt + (Const ("Trueprop",_) $ (Const ("Not", _) $ (Const ("op =", _) $ x $ y)), i) = + (case get_fst_success (neq_x_y ctxt x y) names of + SOME neq => rtac neq i + | NONE => no_tac) + | distinctTree_tac _ _ _ = no_tac; + +fun distinctFieldSolver names = mk_solver' "distinctFieldSolver" + (fn ss => case #context (#1 (rep_ss ss)) of + SOME ctxt => SUBGOAL (distinctTree_tac names ctxt) + | NONE => fn i => no_tac) + +fun distinct_simproc names = + Simplifier.simproc HOL.thy "DistinctTreeProver.distinct_simproc" ["x = y"] + (fn thy => fn ss => fn (Const ("op =",_)$x$y) => + case #context (#1 (rep_ss ss)) of + SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) + (get_fst_success (neq_x_y ctxt x y) names) + | NONE => NONE + ) + +end +end; \ No newline at end of file diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/Statespace/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Statespace/document/root.tex Wed Oct 24 18:36:09 2007 +0200 @@ -0,0 +1,83 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage[greek,english]{babel} + %option greek for \ + %option english (default language) for \, \ + +%\usepackage[latin1]{inputenc} + %for \, \, \, \, + %\, \, \ + +%\usepackage[only,bigsqcap]{stmaryrd} + %for \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + + +\begin{document} + +\title{State Spaces: The Locale Way} +\author{Norbert Schirmer} +\maketitle + +\tableofcontents + +%\parindent 0pt\parskip 0.5ex + +\section{Introduction} + +These theories introduce a new command called \isacommand{statespace}. +It's usage is similar to \isacommand{record}s. However, the command does not introduce a new type but an +abstract specification based on the locale infrastructure. This leads +to extra flexibility in composing state space components, in particular +multiple inheritance and renaming of components. + +The state space infrastructure basically manages the following things: +\begin{itemize} +\item distinctness of field names +\item projections~/ injections from~/ to an abstract \emph{value} type +\item syntax translations for lookup and update, hiding the projections and injections +\item simplification procedure for lookups~/ updates, similar to records +\end{itemize} + + +\paragraph{Overview} +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 +state spaces. The state is represented as a function from (abstract) names to (abstract) values as +introduced in Section \ref{sec:StateFun}. The basic setup for state spaces is in Section +\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. + + +% generated text of all theories +\input{session} + +% optional bibliography +%\bibliographystyle{abbrv} +%\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/Statespace/state_fun.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Statespace/state_fun.ML Wed Oct 24 18:36:09 2007 +0200 @@ -0,0 +1,397 @@ +(* Title: state_fun.ML + ID: $Id$ + Author: Norbert Schirmer, TU Muenchen +*) + + +structure StateFun = +struct + +val lookupN = "StateFun.lookup"; +val updateN = "StateFun.update"; + + +fun dest_nib c = + let val h = List.last (String.explode c) + in if #"0" <= h andalso h <= #"9" then Char.ord h - Char.ord #"0" + else if #"A" <= h andalso h <= #"F" then Char.ord h - Char.ord #"A" + 10 + else raise Match + end; + +fun dest_chr (Const ("List.char.Char",_)$Const (c1,_)$(Const (c2,_))) = + let val c = Char.chr (dest_nib c1 * 16 + dest_nib c2) + in if Char.isPrint c then c else raise Match end + | dest_chr _ = raise Match; + +fun dest_string (Const ("List.list.Nil",_)) = [] + | dest_string (Const ("List.list.Cons",_)$c$cs) = dest_chr c::dest_string cs + | dest_string _ = raise TERM ("dest_string",[]); + +fun sel_name n = String.implode (dest_string n); + +fun mk_name i t = + (case try sel_name t of + SOME name => name + | NONE => (case t of + Free (x,_) => x + |Const (x,_) => x + |_ => "x"^string_of_int i)) + +local +val conj1_False = thm "conj1_False"; +val conj2_False = thm "conj2_False"; +val conj_True = thm "conj_True"; +val conj_cong = thm "conj_cong"; +fun isFalse (Const ("False",_)) = true + | isFalse _ = false; +fun isTrue (Const ("True",_)) = true + | isTrue _ = false; + +in +val lazy_conj_simproc = + Simplifier.simproc HOL.thy "lazy_conj_simp" ["P & Q"] + (fn thy => fn ss => fn t => + (case t of (Const ("op &",_)$P$Q) => + let + val P_P' = Simplifier.rewrite ss (cterm_of thy P); + val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 + in if isFalse P' + then SOME (conj1_False OF [P_P']) + else + let + val Q_Q' = Simplifier.rewrite ss (cterm_of thy Q); + val Q' = Q_Q' |> prop_of |> Logic.dest_equals |> #2 + in if isFalse Q' + then SOME (conj2_False OF [Q_Q']) + else if isTrue P' andalso isTrue Q' + then SOME (conj_True OF [P_P', Q_Q']) + else if P aconv P' andalso Q aconv Q' then NONE + else SOME (conj_cong OF [P_P', Q_Q']) + end + end + + | _ => NONE)); + +val string_eq_simp_tac = + simp_tac (HOL_basic_ss + addsimps (thms "list.inject"@thms "char.inject"@simp_thms) + addsimprocs [distinct_simproc,lazy_conj_simproc] + addcongs [thm "block_conj_cong"]) +end; + + + +local +val rules = + [thm "StateFun.lookup_update_id_same", + thm "StateFun.id_id_cancel", + thm "StateFun.lookup_update_same",thm "StateFun.lookup_update_other" + ] +in +val lookup_ss = (HOL_basic_ss + addsimps (thms "list.inject"@thms "char.inject"@simp_thms@rules) + addsimprocs [distinct_simproc,lazy_conj_simproc] + addcongs [thm "block_conj_cong"] + addSolver StateSpace.distinctNameSolver) +end; + +val ex_lookup_ss = HOL_ss addsimps [thm "StateFun.ex_id"]; + +structure StateFunArgs = +struct + type T = (simpset * simpset * bool); + (* lookup simpset, ex_lookup simpset, are simprocs installed *) + val empty = (empty_ss, empty_ss, false); + val extend = I; + fun merge pp ((ss1,ex_ss1,b1),(ss2,ex_ss2,b2)) = + (merge_ss (ss1,ss2) + ,merge_ss (ex_ss1,ex_ss2) + ,b1 orelse b2); +end; + + +structure StateFunData = GenericDataFun(StateFunArgs); + +val init_state_fun_data = + Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false)); + +val lookup_simproc = + Simplifier.simproc (the_context ()) "lookup_simp" ["lookup d n (update d' c m v s)"] + (fn thy => fn ss => fn t => + (case t of (Const ("StateFun.lookup",lT)$destr$n$ + (s as Const ("StateFun.update",uT)$_$_$_$_$_)) => + (let + val (_::_::_::_::sT::_) = binder_types uT; + val mi = maxidx_of_term t; + fun mk_upds (Const ("StateFun.update",uT)$d'$c$m$v$s) = + let + val (_::_::_::fT::_::_) = binder_types uT; + val vT = domain_type fT; + val (s',cnt) = mk_upds s; + val (v',cnt') = + (case v of + Const ("StateFun.K_statefun",KT)$v'' + => (case v'' of + (Const ("StateFun.lookup",_)$(d as (Const ("Fun.id",_)))$n'$_) + => if d aconv c andalso n aconv m andalso m aconv n' + then (v,cnt) (* Keep value so that + lookup_update_id_same can fire *) + else (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT), + cnt+1) + | _ => (Const ("StateFun.K_statefun",KT)$Var (("v",cnt),vT), + cnt+1)) + | _ => (v,cnt)); + in (Const ("StateFun.update",uT)$d'$c$m$v'$s',cnt') + end + | mk_upds s = (Var (("s",mi+1),sT),mi+2); + + val ct = cterm_of thy + (Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s))); + val ctxt = the (#context (#1 (rep_ss ss))); + val basic_ss = #1 (StateFunData.get (Context.Proof ctxt)); + val ss' = Simplifier.context + (Config.map MetaSimplifier.simp_depth_limit (K 100) ctxt) basic_ss; + val thm = Simplifier.rewrite ss' ct; + in if (op aconv) (Logic.dest_equals (prop_of thm)) + then NONE + else SOME thm + end + handle Option => NONE) + + | _ => NONE )); + + +fun foldl1 f (x::xs) = foldl f x xs; + +local +val update_apply = thm "StateFun.update_apply"; +val meta_ext = thm "StateFun.meta_ext"; +val o_apply = thm "Fun.o_apply"; +val ss' = (HOL_ss addsimps (update_apply::o_apply::thms "list.inject"@thms "char.inject") + addsimprocs [distinct_simproc,lazy_conj_simproc,StateSpace.distinct_simproc] + addcongs [thm "block_conj_cong"]); +in +val update_simproc = + Simplifier.simproc (the_context ()) "update_simp" ["update d c n v s"] + (fn thy => fn ss => fn t => + (case t of ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s) => + let + + val (_::_::_::_::sT::_) = binder_types uT; + (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*) + fun init_seed s = (Bound 0,Bound 0, [("s",sT)],[], false); + + fun mk_comp f fT g gT = + let val T = (domain_type fT --> range_type gT) + in (Const ("Fun.comp",gT --> fT --> T)$g$f,T) end + + fun mk_comps fs = + foldl1 (fn ((f,fT),(g,gT)) => mk_comp f fT g gT) fs; + + fun append n c cT f fT d dT comps = + (case AList.lookup (op aconv) comps n of + SOME gTs => AList.update (op aconv) + (n,[(c,cT),(f,fT),(d,dT)]@gTs) comps + | NONE => AList.update (op aconv) (n,[(c,cT),(f,fT),(d,dT)]) comps) + + fun split_list (x::xs) = let val (xs',y) = split_last xs in (x,xs',y) end + | split_list _ = error "StateFun.split_list"; + + fun merge_upds n comps = + let val ((c,cT),fs,(d,dT)) = split_list (the (AList.lookup (op aconv) comps n)) + in ((c,cT),fst (mk_comps fs),(d,dT)) end; + + (* mk_updterm returns + * - (orig-term-skeleton,simplified-term-skeleton, vars, b) + * where boolean b tells if a simplification has occured. + "orig-term-skeleton = simplified-term-skeleton" is + * the desired simplification rule. + * The algorithm first walks down the updates to the seed-state while + * memorising the updates in the already-table. While walking up the + * updates again, the optimised term is constructed. + *) + fun mk_updterm already + (t as ((upd as Const ("StateFun.update", uT)) $ d $ c $ n $ v $ s)) = + let + fun rest already = mk_updterm already; + val (dT::cT::nT::vT::sT::_) = binder_types uT; + (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => + ('n => 'v) => ('n => 'v)"*) + in if member (op aconv) already n + then (case rest already s of + (trm,trm',vars,comps,_) => + let + val i = length vars; + val kv = (mk_name i n,vT); + val kb = Bound i; + val comps' = append n c cT kb vT d dT comps; + in (upd$d$c$n$kb$trm, trm', kv::vars,comps',true) end) + else + (case rest (n::already) s of + (trm,trm',vars,comps,b) => + let + val i = length vars; + val kv = (mk_name i n,vT); + val kb = Bound i; + val comps' = append n c cT kb vT d dT comps; + val ((c',c'T),f',(d',d'T)) = merge_upds n comps'; + val vT' = range_type d'T --> domain_type c'T; + val upd' = Const ("StateFun.update",d'T --> c'T --> nT --> vT' --> sT --> sT); + in (upd$d$c$n$kb$trm, upd'$d'$c'$n$f'$trm', kv::vars,comps',b) + end) + end + | mk_updterm _ t = init_seed t; + + val ctxt = the (#context (#1 (rep_ss ss))) |> + Config.map MetaSimplifier.simp_depth_limit (K 100); + val ss1 = Simplifier.context ctxt ss'; + val ss2 = Simplifier.context ctxt + (#1 (StateFunData.get (Context.Proof ctxt))); + in (case mk_updterm [] t of + (trm,trm',vars,_,true) + => let + val eq1 = Goal.prove ctxt [] [] + (list_all (vars,equals sT$trm$trm')) + (fn _ => rtac meta_ext 1 THEN + simp_tac ss1 1); + val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1)); + in SOME (transitive eq1 eq2) end + | _ => NONE) + end + | _ => NONE)); +end + + + + +local +val swap_ex_eq = thm "StateFun.swap_ex_eq"; +fun is_selector thy T sel = + let + val (flds,more) = RecordPackage.get_recT_fields thy T + in member (fn (s,(n,_)) => n=s) (more::flds) sel + end; +in +val ex_lookup_eq_simproc = + Simplifier.simproc HOL.thy "ex_lookup_eq_simproc" ["Ex t"] + (fn thy => fn ss => fn t => + let + val ctxt = Simplifier.the_context ss |> + Config.map MetaSimplifier.simp_depth_limit (K 100) + val ex_lookup_ss = #2 (StateFunData.get (Context.Proof ctxt)); + val ss' = (Simplifier.context ctxt ex_lookup_ss); + fun prove prop = + Goal.prove_global thy [] [] prop + (fn _ => record_split_simp_tac [] (K ~1) 1 THEN + simp_tac ss' 1); + + fun mkeq (swap,Teq,lT,lo,d,n,x,s) i = + let val (_::nT::_) = binder_types lT; + (* ('v => 'a) => 'n => ('n => 'v) => 'a *) + val x' = if not (loose_bvar1 (x,0)) + then Bound 1 + else raise TERM ("",[x]); + val n' = if not (loose_bvar1 (n,0)) + then Bound 2 + else raise TERM ("",[n]); + val sel' = lo $ d $ n' $ s; + in (Const ("op =",Teq)$sel'$x',hd (binder_types Teq),nT,swap) end; + + fun dest_state (s as Bound 0) = s + | dest_state (s as (Const (sel,sT)$Bound 0)) = + if is_selector thy (domain_type sT) sel + then s + else raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]) + | dest_state s = + raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]); + + fun dest_sel_eq (Const ("op =",Teq)$ + ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) = + (false,Teq,lT,lo,d,n,X,dest_state s) + | dest_sel_eq (Const ("op =",Teq)$X$ + ((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) = + (true,Teq,lT,lo,d,n,X,dest_state s) + | dest_sel_eq _ = raise TERM ("",[]); + + in + (case t of + (Const ("Ex",Tex)$Abs(s,T,t)) => + (let val (eq,eT,nT,swap) = mkeq (dest_sel_eq t) 0; + val prop = list_all ([("n",nT),("x",eT)], + Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq), + HOLogic.true_const)); + val thm = standard (prove prop); + val thm' = if swap then swap_ex_eq OF [thm] else thm + in SOME thm' end + handle TERM _ => NONE) + | _ => NONE) + end handle Option => NONE) +end; + +val val_sfx = "V"; +val val_prfx = "StateFun." +fun deco base_prfx s = val_prfx ^ (base_prfx ^ suffix val_sfx s); + +fun mkUpper str = + (case String.explode str of + [] => "" + | c::cs => String.implode (Char.toUpper c::cs )) + +fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base T) + | mkName (TFree (x,_)) = mkUpper (NameSpace.base x) + | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base x); + +fun is_datatype thy n = is_some (Symtab.lookup (DatatypePackage.get_datatypes thy) n); + +fun mk_map ("List.list") = Syntax.const "List.map" + | mk_map n = Syntax.const ("StateFun." ^ "map_" ^ NameSpace.base n); + +fun gen_constr_destr comp prfx thy (Type (T,[])) = + Syntax.const (deco prfx (mkUpper (NameSpace.base T))) + | gen_constr_destr comp prfx thy (T as Type ("fun",_)) = + let val (argTs,rangeT) = strip_type T; + in comp + (Syntax.const (deco prfx (concat (map mkName argTs) ^ "Fun"))) + (fold (fn x => fn y => x$y) + (replicate (length argTs) (Syntax.const "StateFun.map_fun")) + (gen_constr_destr comp prfx thy rangeT)) + end + | gen_constr_destr comp prfx thy (T' as Type (T,argTs)) = + if is_datatype thy T + then (* datatype args are recursively embedded into val *) + (case argTs of + [argT] => comp + ((Syntax.const (deco prfx (mkUpper (NameSpace.base T))))) + ((mk_map T $ gen_constr_destr comp prfx thy argT)) + | _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[]))) + else (* type args are not recursively embedded into val *) + Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base T))) + | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[])); + +val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) "" +val mk_destr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ b $ a) "the_" + + +fun statefun_simp_attr src (ctxt,thm) = + let + val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt; + val (lookup_ss', ex_lookup_ss') = + (case (concl_of thm) of + (_$((Const ("Ex",_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm]) + | _ => (lookup_ss addsimps [thm], ex_lookup_ss)) + fun activate_simprocs ctxt = + if simprocs_active then ctxt + else StateSpace.change_simpset + (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt + + + val ctxt' = ctxt + |> activate_simprocs + |> (StateFunData.put (lookup_ss',ex_lookup_ss',true)) + in (ctxt', thm) end; + +val setup = + init_state_fun_data + #> Attrib.add_attributes + [("statefun_simp",statefun_simp_attr,"simplification in statespaces")] +end diff -r bd06fd396fd0 -r 4a9c25bffc9b src/HOL/Statespace/state_space.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Statespace/state_space.ML Wed Oct 24 18:36:09 2007 +0200 @@ -0,0 +1,660 @@ +(* Title: state_space.ML + ID: $Id$ + Author: Norbert Schirmer, TU Muenchen +*) + +structure StateSpace = +struct + +(* Theorems *) + +(* Names *) +val distinct_compsN = "distinct_names" +val namespaceN = "_namespace" +val valuetypesN = "_valuetypes" +val projectN = "project" +val injectN = "inject" +val getN = "get" +val putN = "put" +val project_injectL = "StateSpaceLocale.project_inject"; +val KN = "StateFun.K_statefun" + + +(* messages *) + +val quiet_mode = ref false; +fun message s = if ! quiet_mode then () else writeln s; + +(* Library *) + +fun fold1 f xs = fold f (tl xs) (hd xs) +fun fold1' f [] x = x + | fold1' f xs _ = fold1 f xs + +fun sublist_idx eq xs ys = + let + fun sublist n xs ys = + if is_prefix eq xs ys then SOME n + else (case ys of [] => NONE + | (y::ys') => sublist (n+1) xs ys') + in sublist 0 xs ys end; + +fun is_sublist eq xs ys = is_some (sublist_idx eq xs ys); + +fun sorted_subset eq [] ys = true + | sorted_subset eq (x::xs) [] = false + | sorted_subset eq (x::xs) (y::ys) = if eq (x,y) then sorted_subset eq xs ys + else sorted_subset eq (x::xs) ys; + + + +type namespace_info = + {declinfo: (typ*string) Termtab.table, (* type, name of statespace *) + distinctthm: thm Symtab.table, + silent: bool + }; + +structure NameSpaceArgs = +struct + type T = namespace_info; + val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false}; + val extend = I; + fun merge pp ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1}, + {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) = + {declinfo = Termtab.merge (K true) (declinfo1, declinfo2), + distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2), + silent = silent1 andalso silent2} +end; + +structure NameSpaceData = GenericDataFun(NameSpaceArgs); + +fun make_namespace_data declinfo distinctthm silent = + {declinfo=declinfo,distinctthm=distinctthm,silent=silent}; + + +fun delete_declinfo n ctxt = + let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt; + in NameSpaceData.put + (make_namespace_data (Termtab.delete_safe n declinfo) distinctthm silent) ctxt + end; + + +fun update_declinfo (n,v) ctxt = + let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt; + in NameSpaceData.put + (make_namespace_data (Termtab.update (n,v) declinfo) distinctthm silent) ctxt + end; + +fun set_silent silent ctxt = + let val {declinfo,distinctthm,...} = NameSpaceData.get ctxt; + in NameSpaceData.put + (make_namespace_data declinfo distinctthm silent) ctxt + end; + +val get_silent = #silent o NameSpaceData.get; + +fun prove_interpretation_in ctxt_tac (name, expr) thy = + thy + |> Locale.interpretation_in_locale I (name, expr) + |> Proof.global_terminal_proof + (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE) + |> ProofContext.theory_of + +type statespace_info = + {args: (string * sort) list, (* type arguments *) + parents: (typ list * string * string option list) list, + (* type instantiation, state-space name, component renamings *) + components: (string * typ) list, + types: typ list (* range types of state space *) + }; + +structure StateSpaceArgs = +struct + val name = "HOL/StateSpace"; + type T = statespace_info Symtab.table; + val empty = Symtab.empty; + val extend = I; + + fun merge pp (nt1,nt2) = Symtab.merge (K true) (nt1, nt2); +end; + +structure StateSpaceData = GenericDataFun(StateSpaceArgs); + +fun add_statespace name args parents components types ctxt = + StateSpaceData.put + (Symtab.update_new (name, {args=args,parents=parents, + components=components,types=types}) (StateSpaceData.get ctxt)) + ctxt; + +fun get_statespace ctxt name = + Symtab.lookup (StateSpaceData.get ctxt) name; + + +fun lookupI eq xs n = + (case AList.lookup eq xs n of + SOME v => v + | NONE => n); + +fun mk_free ctxt name = + if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name + then + let val n' = lookupI (op =) (Variable.fixes_of ctxt) name + in SOME (Free (n',ProofContext.infer_type ctxt n')) end + else NONE + + +fun get_dist_thm ctxt name = Symtab.lookup (#distinctthm (NameSpaceData.get ctxt)) name; +fun get_comp ctxt name = + Option.mapPartial + (Termtab.lookup (#declinfo (NameSpaceData.get ctxt))) + (mk_free (Context.proof_of ctxt) name); + + +(*** Tactics ***) + +fun neq_x_y ctxt x y = + (let + val dist_thm = the (get_dist_thm (Context.Proof ctxt) (#1 (dest_Free x))); + val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; + val tree = term_of ctree; + val x_path = the (DistinctTreeProver.find_tree x tree); + val y_path = the (DistinctTreeProver.find_tree y tree); + val thm = DistinctTreeProver.distinctTreeProver dist_thm x_path y_path; + in SOME thm + end handle Option => NONE) + +fun distinctTree_tac ctxt + (Const ("Trueprop",_) $ + (Const ("Not", _) $ (Const ("op =", _) $ (x as Free _)$ (y as Free _))), i) = + (case (neq_x_y ctxt x y) of + SOME neq => rtac neq i + | NONE => no_tac) + | distinctTree_tac _ _ = no_tac; + +val distinctNameSolver = mk_solver' "distinctNameSolver" + (fn ss => case #context (#1 (rep_ss ss)) of + SOME ctxt => SUBGOAL (distinctTree_tac ctxt) + | NONE => fn i => no_tac) + +val distinct_simproc = + Simplifier.simproc HOL.thy "StateSpace.distinct_simproc" ["x = y"] + (fn thy => fn ss => (fn (Const ("op =",_)$(x as Free _)$(y as Free _)) => + (case #context (#1 (rep_ss ss)) of + SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) + (neq_x_y ctxt x y) + | NONE => NONE) + | _ => NONE)) + +fun change_simpset f = + Context.mapping + (fn thy => (change_simpset_of thy f; thy)) + (fn ctxt => Simplifier.put_local_simpset (f (Simplifier.get_local_simpset ctxt)) ctxt); + +fun read_typ thy s = + Sign.read_typ thy s; + +local + val ss = HOL_basic_ss +in +fun interprete_parent name dist_thm_name parent_expr thy = + let + + fun solve_tac ctxt (_,i) st = + let + val distinct_thm = ProofContext.get_thm ctxt (Name dist_thm_name); + val goal = List.nth (cprems_of st,i-1); + val rule = DistinctTreeProver.distinct_implProver distinct_thm goal; + in EVERY [rtac rule i] st + end + + fun tac ctxt = EVERY [Locale.intro_locales_tac true ctxt [], + ALLGOALS (SUBGOAL (solve_tac ctxt))] + + in thy + |> prove_interpretation_in tac (name,parent_expr) + end; + +end; + +fun namespace_definition name nameT parent_expr parent_comps new_comps thy = + let + val all_comps = parent_comps @ new_comps; + val vars = Locale.Merge + (map (fn n => Locale.Rename (Locale.Locale (Locale.intern thy "var") + ,[SOME (n,NONE)])) all_comps); + + val full_name = Sign.full_name thy name; + val dist_thm_name = distinct_compsN; + val dist_thm_full_name = + let val prefix = fold1' (fn name => fn prfx => prfx ^ "_" ^ name) all_comps ""; + in if prefix = "" then dist_thm_name else prefix ^ "." ^ dist_thm_name end; + + fun comps_of_thm thm = prop_of thm + |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free); + + fun type_attr phi (ctxt,thm) = + (case ctxt of Context.Theory _ => (ctxt,thm) + | _ => + let + val {declinfo,distinctthm=tt,silent} = (NameSpaceData.get ctxt); + val all_names = comps_of_thm thm; + fun upd name tt = + (case (Symtab.lookup tt name) of + SOME dthm => if sorted_subset (op =) (comps_of_thm dthm) all_names + then Symtab.update (name,thm) tt else tt + | NONE => Symtab.update (name,thm) tt) + + val tt' = tt |> fold upd all_names; + val activate_simproc = + Output.no_warnings + (change_simpset (fn ss => ss addsimprocs [distinct_simproc])); + val ctxt' = + ctxt + |> NameSpaceData.put {declinfo=declinfo,distinctthm=tt',silent=silent} + |> activate_simproc + in (ctxt',thm) + end) + + val attr = Attrib.internal type_attr; + + val assumes = Element.Assumes [((dist_thm_name,[attr]), + [(HOLogic.Trueprop $ + (Const ("DistinctTreeProver.all_distinct", + Type ("DistinctTreeProver.tree",[nameT]) --> HOLogic.boolT) $ + DistinctTreeProver.mk_tree (fn n => Free (n,nameT)) nameT + (sort fast_string_ord all_comps)), + ([]))])]; + + in thy + |> Locale.add_locale_i (SOME "") name vars [assumes] + ||> ProofContext.theory_of + ||> interprete_parent name dist_thm_full_name parent_expr + |> #2 + end; + +structure Typetab = TableFun(type key=typ val ord = Term.typ_ord); + +fun encode_dot x = if x= #"." then #"_" else x; + +fun encode_type (TFree (s, _)) = s + | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i + | encode_type (Type (n,Ts)) = + let + val Ts' = fold1' (fn x => fn y => x ^ "_" ^ y) (map encode_type Ts) ""; + val n' = String.map encode_dot n; + in if Ts'="" then n' else Ts' ^ "_" ^ n' end; + +fun project_name T = projectN ^"_"^encode_type T; +fun inject_name T = injectN ^"_"^encode_type T; + +fun project_free T pT V = Free (project_name T, V --> pT); +fun inject_free T pT V = Free (inject_name T, pT --> V); + +fun get_name n = getN ^ "_" ^ n; +fun put_name n = putN ^ "_" ^ n; +fun get_const n T nT V = Free (get_name n, (nT --> V) --> T); +fun put_const n T nT V = Free (put_name n, T --> (nT --> V) --> (nT --> V)); + +fun lookup_const T nT V = Const ("StateFun.lookup",(V --> T) --> nT --> (nT --> V) --> T); +fun update_const T nT V = + Const ("StateFun.update", + (V --> T) --> (T --> V) --> nT --> (T --> T) --> (nT --> V) --> (nT --> V)); + +fun K_const T = Const ("StateFun.K_statefun",T --> T --> T); + +val no_syn = #3 (Syntax.no_syn ((),())); + + +fun add_declaration name decl thy = + thy + |> TheoryTarget.init name + |> (fn lthy => LocalTheory.declaration (decl lthy) lthy) + |> LocalTheory.exit + |> ProofContext.theory_of; + +fun parent_components thy (Ts, pname, renaming) = + let + val ctxt = Context.Theory thy; + fun rename [] xs = xs + | rename (NONE::rs) (x::xs) = x::rename rs xs + | rename (SOME r::rs) ((x,T)::xs) = (r,T)::rename rs xs; + val {args,parents,components,...} = + the (Symtab.lookup (StateSpaceData.get ctxt) pname); + val inst = map fst args ~~ Ts; + val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); + val parent_comps = + List.concat (map (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents); + val all_comps = rename renaming (parent_comps @ map (apsnd subst) components); + in all_comps end; + +fun take_upto i xs = List.take(xs,i) handle Subscript => xs; + +fun statespace_definition state_type args name parents parent_comps components thy = + let + val full_name = Sign.full_name thy name; + val all_comps = parent_comps @ components; + + val components' = map (fn (n,T) => (n,(T,full_name))) components; + val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps; + fun parent_expr (_,n,rs) = Locale.Rename + (Locale.Locale (suffix namespaceN n), + map (Option.map (fn s => (s,NONE))) rs); + val parents_expr = Locale.Merge (fold (fn p => fn es => parent_expr p::es) parents []); + + fun distinct_types Ts = + let val tab = fold (fn T => fn tab => Typetab.update (T,()) tab) Ts Typetab.empty; + in map fst (Typetab.dest tab) end; + + val Ts = distinct_types (map snd all_comps); + val arg_names = map fst args; + val valueN = Name.variant arg_names "'value"; + val nameN = Name.variant (valueN::arg_names) "'name"; + val valueT = TFree (valueN, Sign.defaultS thy); + val nameT = TFree (nameN, Sign.defaultS thy); + val stateT = nameT --> valueT; + fun projectT T = valueT --> T; + fun injectT T = T --> valueT; + + val locs = map (fn T => Locale.Rename (Locale.Locale project_injectL, + [SOME (project_name T,NONE), + SOME (inject_name T ,NONE)])) Ts; + val constrains = List.concat + (map (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts); + + fun interprete_parent_valuetypes (Ts, pname, _) = + let + val {args,types,...} = + the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname); + val inst = map fst args ~~ Ts; + val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); + val pars = List.concat (map ((fn T => [project_name T,inject_name T]) o subst) types); + val expr = Locale.Rename (Locale.Locale (suffix valuetypesN name), + map (fn n => SOME (n,NONE)) pars); + in prove_interpretation_in (K all_tac) + (suffix valuetypesN name, expr) end; + + fun interprete_parent (_, pname, rs) = + let + val expr = Locale.Rename (Locale.Locale pname, map (Option.map (fn n => (n,NONE))) rs) + in prove_interpretation_in + (fn ctxt => Locale.intro_locales_tac false ctxt []) + (full_name, expr) end; + + fun declare_declinfo updates lthy phi ctxt = + let + fun upd_prf ctxt = + let + fun upd (n,v) = + let + val nT = ProofContext.infer_type (LocalTheory.target_of lthy) n + in Context.proof_map + (update_declinfo (Morphism.term phi (Free (n,nT)),v)) + end; + in ctxt |> fold upd updates end; + + in Context.mapping I upd_prf ctxt end; + + fun string_of_typ T = + setmp show_sorts true + (setmp print_mode [] (Syntax.string_of_typ (ProofContext.init thy))) T; + val fixestate = (case state_type of + NONE => [] + | SOME s => + let + val fx = Element.Fixes [(s,SOME (string_of_typ stateT),NoSyn)]; + val cs = Element.Constrains + (map (fn (n,T) => (n,string_of_typ T)) + ((map (fn (n,_) => (n,nameT)) all_comps) @ + constrains)) + in [fx,cs] end + ) + + + in thy + |> namespace_definition + (suffix namespaceN name) nameT parents_expr + (map fst parent_comps) (map fst components) + |> Context.theory_map (add_statespace full_name args parents components []) + |> Locale.add_locale_i (SOME "") (suffix valuetypesN name) (Locale.Merge locs) + [Element.Constrains constrains] + |> ProofContext.theory_of o #2 + |> fold interprete_parent_valuetypes parents + |> Locale.add_locale (SOME "") name + (Locale.Merge [Locale.Locale (suffix namespaceN full_name) + ,Locale.Locale (suffix valuetypesN full_name)]) fixestate + |> ProofContext.theory_of o #2 + |> fold interprete_parent parents + |> add_declaration (SOME full_name) (declare_declinfo components') + end; + + +(* prepare arguments *) + +fun read_raw_parent sg s = + (case Sign.read_typ_abbrev sg s handle TYPE (msg, _, _) => error msg of + Type (name, Ts) => (Ts, name) + | _ => error ("Bad parent statespace specification: " ^ quote s)); + +fun read_typ sg s env = + let + fun def_sort (x, ~1) = AList.lookup (op =) env x + | def_sort _ = NONE; + val T = Type.no_tvars (Sign.read_def_typ (sg, def_sort) s) handle TYPE (msg, _, _) => error msg; + in (T, Term.add_typ_tfrees (T, env)) end; + +fun cert_typ sg raw_T env = + let val T = Type.no_tvars (Sign.certify_typ sg raw_T) handle TYPE (msg, _, _) => error msg + in (T, Term.add_typ_tfrees (T, env)) end; + + + + +fun gen_define_statespace prep_typ state_space args name parents comps thy = + let (* - args distinct + - only args may occur in comps and parent-instantiations + - number of insts must match parent args + - no duplicate renamings + - renaming should occur in namespace + *) + val _ = message ("Defining statespace " ^ quote name ^ " ..."); + + fun add_parent (Ts,pname,rs) env = + let + val full_pname = Sign.full_name thy pname; + val {args,components,...} = + (case get_statespace (Context.Theory thy) full_pname of + SOME r => r + | NONE => error ("Undefined statespace " ^ quote pname)); + + + val (Ts',env') = fold_map (prep_typ thy) Ts env + handle ERROR msg => cat_error msg + ("The error(s) above occured in parent statespace specification " + ^ quote pname); + val err_insts = if length args <> length Ts' then + ["number of type instantiation(s) does not match arguments of parent statespace " + ^ quote pname] + else []; + + val rnames = map fst rs + val err_dup_renamings = (case duplicates (op =) rnames of + [] => [] + | dups => ["Duplicate renaming(s) for " ^ commas dups]) + + val cnames = map fst components; + val err_rename_unknowns = (case (filter (fn n => not (n mem cnames))) rnames of + [] => [] + | rs => ["Unknown components " ^ commas rs]); + + + val rs' = map (AList.lookup (op =) rs o fst) components; + val errs =err_insts @ err_dup_renamings @ err_rename_unknowns + in if null errs then ((Ts',full_pname,rs'),env') + else error (cat_lines (errs @ ["in parent statespace " ^ quote pname])) + end; + + val (parents',env) = fold_map add_parent parents []; + + val err_dup_args = + (case duplicates (op =) args of + [] => [] + | dups => ["Duplicate type argument(s) " ^ commas dups]); + + + val err_dup_components = + (case duplicates (op =) (map fst comps) of + [] => [] + | dups => ["Duplicate state-space components " ^ commas dups]); + + fun prep_comp (n,T) env = + let val (T', env') = prep_typ thy T env handle ERROR msg => + cat_error msg ("The error(s) above occured in component " ^ quote n) + in ((n,T'), env') end; + + val (comps',env') = fold_map prep_comp comps env; + + val err_extra_frees = + (case subtract (op =) args (map fst env') of + [] => [] + | extras => ["Extra free type variable(s) " ^ commas extras]); + + val defaultS = Sign.defaultS thy; + val args' = map (fn x => (x, AList.lookup (op =) env x |> the_default defaultS)) args; + + + fun fst_eq ((x:string,_),(y,_)) = x = y; + fun snd_eq ((_,t:typ),(_,u)) = t = u; + + val raw_parent_comps = (List.concat (map (parent_components thy) parents')); + fun check_type (n,T) = + (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of + [] => [] + | [_] => [] + | rs => ["Different types for component " ^ n ^": " ^ commas + (map (Pretty.string_of o Display.pretty_ctyp o ctyp_of thy o snd) rs)]) + + val err_dup_types = List.concat (map check_type (duplicates fst_eq raw_parent_comps)) + + val parent_comps = distinct (fst_eq) raw_parent_comps; + val all_comps = parent_comps @ comps'; + val err_comp_in_parent = (case duplicates (op =) (map fst all_comps) of + [] => [] + | xs => ["Components already defined in parents: " ^ commas xs]); + val errs = err_dup_args @ err_dup_components @ err_extra_frees @ + err_dup_types @ err_comp_in_parent; + + in if null errs + then thy |> statespace_definition state_space args' name parents' parent_comps comps' + else error (cat_lines errs) + end + handle ERROR msg => cat_error msg ("Failed to define statespace " ^ quote name); + + +val define_statespace = gen_define_statespace read_typ NONE; +val define_statespace_i = gen_define_statespace cert_typ; + + +(*** parse/print - translations ***) + + +local +fun map_get_comp f ctxt (Free (name,_)) = + (case (get_comp ctxt name) of + SOME (T,_) => f T T dummyT + | NONE => (Syntax.free "arbitrary"(*; error "context not ready"*))) + | map_get_comp _ _ _ = Syntax.free "arbitrary"; + +val get_comp_projection = map_get_comp project_free; +val get_comp_injection = map_get_comp inject_free; + +fun name_of (Free (n,_)) = n; +in + +fun gen_lookup_tr ctxt s n = + (case get_comp (Context.Proof ctxt) n of + SOME (T,_) => + Syntax.const "StateFun.lookup"$Syntax.free (project_name T)$Syntax.free n$s + | NONE => + if get_silent (Context.Proof ctxt) + then Syntax.const "StateFun.lookup"$Syntax.const "arbitrary"$Syntax.free n$s + else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[])); + +fun lookup_tr ctxt [s,Free (n,_)] = gen_lookup_tr ctxt s n; +fun lookup_swap_tr ctxt [Free (n,_),s] = gen_lookup_tr ctxt s n; + +fun lookup_tr' ctxt [_$Free (prj,_),n as (_$Free (name,_)),s] = + ( case get_comp (Context.Proof ctxt) name of + SOME (T,_) => if prj=project_name T then + Syntax.const "_statespace_lookup" $ s $ n + else raise Match + | NONE => raise Match) + | lookup_tr' _ ts = raise Match; + +fun gen_update_tr id ctxt n v s = + let + fun pname T = if id then "Fun.id" else project_name T + fun iname T = if id then "Fun.id" else inject_name T + in + (case get_comp (Context.Proof ctxt) n of + SOME (T,_) => Syntax.const "StateFun.update"$ + Syntax.free (pname T)$Syntax.free (iname T)$ + Syntax.free n$(Syntax.const KN $ v)$s + | NONE => + if get_silent (Context.Proof ctxt) + then Syntax.const "StateFun.update"$ + Syntax.const "arbitrary"$Syntax.const "arbitrary"$ + Syntax.free n$(Syntax.const KN $ v)$s + else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined",[])) + end; + +fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s; + +fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] = + if NameSpace.base k = NameSpace.base KN then + (case get_comp (Context.Proof ctxt) name of + SOME (T,_) => if inj=inject_name T andalso prj=project_name T then + Syntax.const "_statespace_update" $ s $ n $ v + else raise Match + | NONE => raise Match) + else raise Match + | update_tr' _ _ = raise Match; + +end; + + +(*** outer syntax *) + +local structure P = OuterParse and K = OuterKeyword in + +val type_insts = + P.typ >> single || + P.$$$ "(" |-- P.!!! (P.list1 P.typ --| P.$$$ ")") + +val comp = P.name -- (P.$$$ "::" |-- P.!!! P.typ); +fun plus1_unless test scan = + scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::; + +val mapsto = P.$$$ "="; +val rename = P.name -- (mapsto |-- P.name); +val renames = Scan.optional (P.$$$ "[" |-- P.!!! (P.list1 rename --| P.$$$ "]")) []; + + +val parent = ((type_insts -- P.xname) || (P.xname >> pair [])) -- renames + >> (fn ((insts,name),renames) => (insts,name,renames)) + + +val statespace_decl = + P.type_args -- P.name -- + (P.$$$ "=" |-- + ((Scan.repeat1 comp >> pair []) || + (plus1_unless comp parent -- + Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 comp)) []))) + +val statespace_command = + OuterSyntax.command "statespace" "define state space" K.thy_decl + (statespace_decl >> (fn ((args,name),(parents,comps)) => + Toplevel.theory (define_statespace args name parents comps))) + +end; + +end; \ No newline at end of file