# HG changeset patch # User wenzelm # Date 1320601337 -3600 # Node ID ccec8b6d5d81559267eaa70af0dd6d309586987e # Parent cc455b2897f8224776b7acd01cdca5cb3eb20963# Parent 208634369af2df99135a80a26111efbb64f15e50 merged diff -r cc455b2897f8 -r ccec8b6d5d81 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Nov 06 14:23:04 2011 +0100 +++ b/src/HOL/IsaMakefile Sun Nov 06 18:42:17 2011 +0100 @@ -1299,11 +1299,12 @@ 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 +$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/ROOT.ML \ + 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 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace diff -r cc455b2897f8 -r ccec8b6d5d81 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Sun Nov 06 14:23:04 2011 +0100 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sun Nov 06 18:42:17 2011 +0100 @@ -880,6 +880,10 @@ prefix = prefix}} | x => x); +fun write_prv path s = + let val path_prv = Path.ext "prv" path; + in if try File.read path_prv = SOME s then () else File.write path_prv s end; + fun close thy = thy |> VCs.map (fn @@ -888,7 +892,7 @@ (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of (proved, []) => (Thm.join_proofs (maps (the o #2 o snd) proved); - File.write (Path.ext "prv" path) + write_prv path (implode (map (fn (s, _) => snd (strip_number s) ^ " -- proved by " ^ Distribution.version ^ "\n") proved)); {pfuns = pfuns, type_map = type_map, env = NONE}) diff -r cc455b2897f8 -r ccec8b6d5d81 src/HOL/Statespace/DistinctTreeProver.thy --- a/src/HOL/Statespace/DistinctTreeProver.thy Sun Nov 06 14:23:04 2011 +0100 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Sun Nov 06 18:42:17 2011 +0100 @@ -51,21 +51,20 @@ 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" +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" +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" +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" +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)" @@ -87,17 +86,17 @@ 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 +assume 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. -*} +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. *} primrec delete :: "'a \ 'a tree \ 'a tree option" @@ -109,14 +108,14 @@ 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 + (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) +lemma delete_Some_set_of: "delete x t = Some t' \ set_of t' \ set_of t" +proof (induct t arbitrary: t') case Tip thus ?case by simp next case (Node l y d r) @@ -164,9 +163,9 @@ qed qed -lemma delete_Some_all_distinct: -"\t'. \delete x t = Some t'; all_distinct t\ \ all_distinct t'" -proof (induct t) +lemma delete_Some_all_distinct: + "delete x t = Some t' \ all_distinct t \ all_distinct t'" +proof (induct t arbitrary: t') case Tip thus ?case by simp next case (Node l y d r) @@ -238,8 +237,8 @@ qed lemma delete_Some_x_set_of: - "\t'. delete x t = Some t' \ x \ set_of t \ x \ set_of t'" -proof (induct t) + "delete x t = Some t' \ x \ set_of t \ x \ set_of t'" +proof (induct t arbitrary: t') case Tip thus ?case by simp next case (Node l y d r) @@ -305,8 +304,8 @@ | 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) + "subtract t\<^isub>1 t\<^isub>2 = Some t \ set_of t \ set_of t\<^isub>2" +proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t) case Tip thus ?case by simp next case (Node l x b r) @@ -350,8 +349,8 @@ 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) + "subtract t\<^isub>1 t\<^isub>2 = Some t \ set_of t\<^isub>1 \ set_of t\<^isub>2" +proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t) case Tip thus ?case by simp next case (Node l x d r) @@ -400,8 +399,8 @@ 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) + "subtract t\<^isub>1 t\<^isub>2 = Some t \ all_distinct t\<^isub>2 \ all_distinct t" +proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t) case Tip thus ?case by simp next case (Node l x d r) @@ -448,8 +447,8 @@ 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) + "subtract t\<^isub>1 t\<^isub>2 = Some t \ set_of t\<^isub>1 \ set_of t = {}" +proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t) case Tip thus ?case by simp next case (Node l x d r) @@ -502,8 +501,8 @@ 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) + "subtract t\<^isub>1 t\<^isub>2 = Some t \ all_distinct t\<^isub>2 \ all_distinct t\<^isub>1" +proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t) case Tip thus ?case by simp next case (Node l x d r) diff -r cc455b2897f8 -r ccec8b6d5d81 src/HOL/Statespace/StateFun.thy --- a/src/HOL/Statespace/StateFun.thy Sun Nov 06 14:23:04 2011 +0100 +++ b/src/HOL/Statespace/StateFun.thy Sun Nov 06 18:42:17 2011 +0100 @@ -58,8 +58,7 @@ 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" +lemma destr_contstr_comp_id: "(\v. destr (constr v) = v) \ destr \ constr = id" by (rule ext) simp @@ -67,16 +66,16 @@ lemma block_conj_cong: "(P \ Q) = (P \ Q)" by simp -lemma conj1_False: "(P\False) \ (P \ Q) \ False" +lemma conj1_False: "P \ False \ (P \ Q) \ False" by simp -lemma conj2_False: "\Q\False\ \ (P \ Q) \ False" +lemma conj2_False: "Q \ False \ (P \ Q) \ False" by simp -lemma conj_True: "\P\True; Q\True\ \ (P \ Q) \ True" +lemma conj_True: "P \ True \ Q \ True \ (P \ Q) \ True" by simp -lemma conj_cong: "\P\P'; Q\Q'\ \ (P \ Q) \ (P' \ Q')" +lemma conj_cong: "P \ P' \ Q \ Q' \ (P \ Q) \ (P' \ Q')" by simp diff -r cc455b2897f8 -r ccec8b6d5d81 src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Sun Nov 06 14:23:04 2011 +0100 +++ b/src/HOL/Statespace/StateSpaceEx.thy Sun Nov 06 18:42:17 2011 +0100 @@ -12,12 +12,9 @@ "_statespace_updates" :: "('a \ 'b) \ updbinds \ ('a \ 'b)" ("_\_\" [900,0] 900) (*>*) -text {* Did you ever dream about records with multiple inheritance. +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... -*} - - +what you are dreaming of. Or at least almost \dots *} text {* Isabelle allows to add new top-level commands to the @@ -169,12 +166,12 @@ proof - thm foo1 txt {* The Lemma @{thm [source] foo1} from the parent state space - is also available here: \begin{center}@{thm foo1}\end{center}.*} + 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}.*} + \begin{center}@{thm bar1}\end{center} *} have "s\C = s\C" by (rule bar1) show ?thesis @@ -198,9 +195,9 @@ by simp -text {* Hmm, I hoped this would work now...*} +(* +text "Hmm, I hoped this would work now..." -(* locale fooX = foo + assumes "s\b = k" *) @@ -231,4 +228,252 @@ elaborate locale infrastructure in place this may be an easy exercise. *} + +subsection {* Benchmarks *} + +text {* Here are some bigger examples for benchmarking. *} + +ML {* + fun make_benchmark n = + writeln (Markup.markup Markup.sendback + ("statespace benchmark" ^ string_of_int n ^ " =\n" ^ + (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n))))); +*} + +text "0.2s" +statespace benchmark100 = A1::nat A2::nat A3::nat A4::nat A5::nat +A6::nat A7::nat A8::nat A9::nat A10::nat A11::nat A12::nat A13::nat +A14::nat A15::nat A16::nat A17::nat A18::nat A19::nat A20::nat +A21::nat A22::nat A23::nat A24::nat A25::nat A26::nat A27::nat +A28::nat A29::nat A30::nat A31::nat A32::nat A33::nat A34::nat +A35::nat A36::nat A37::nat A38::nat A39::nat A40::nat A41::nat +A42::nat A43::nat A44::nat A45::nat A46::nat A47::nat A48::nat +A49::nat A50::nat A51::nat A52::nat A53::nat A54::nat A55::nat +A56::nat A57::nat A58::nat A59::nat A60::nat A61::nat A62::nat +A63::nat A64::nat A65::nat A66::nat A67::nat A68::nat A69::nat +A70::nat A71::nat A72::nat A73::nat A74::nat A75::nat A76::nat +A77::nat A78::nat A79::nat A80::nat A81::nat A82::nat A83::nat +A84::nat A85::nat A86::nat A87::nat A88::nat A89::nat A90::nat +A91::nat A92::nat A93::nat A94::nat A95::nat A96::nat A97::nat +A98::nat A99::nat A100::nat + +text "2.4s" +statespace benchmark500 = A1::nat A2::nat A3::nat A4::nat A5::nat +A6::nat A7::nat A8::nat A9::nat A10::nat A11::nat A12::nat A13::nat +A14::nat A15::nat A16::nat A17::nat A18::nat A19::nat A20::nat +A21::nat A22::nat A23::nat A24::nat A25::nat A26::nat A27::nat +A28::nat A29::nat A30::nat A31::nat A32::nat A33::nat A34::nat +A35::nat A36::nat A37::nat A38::nat A39::nat A40::nat A41::nat +A42::nat A43::nat A44::nat A45::nat A46::nat A47::nat A48::nat +A49::nat A50::nat A51::nat A52::nat A53::nat A54::nat A55::nat +A56::nat A57::nat A58::nat A59::nat A60::nat A61::nat A62::nat +A63::nat A64::nat A65::nat A66::nat A67::nat A68::nat A69::nat +A70::nat A71::nat A72::nat A73::nat A74::nat A75::nat A76::nat +A77::nat A78::nat A79::nat A80::nat A81::nat A82::nat A83::nat +A84::nat A85::nat A86::nat A87::nat A88::nat A89::nat A90::nat +A91::nat A92::nat A93::nat A94::nat A95::nat A96::nat A97::nat +A98::nat A99::nat A100::nat A101::nat A102::nat A103::nat A104::nat +A105::nat A106::nat A107::nat A108::nat A109::nat A110::nat A111::nat +A112::nat A113::nat A114::nat A115::nat A116::nat A117::nat A118::nat +A119::nat A120::nat A121::nat A122::nat A123::nat A124::nat A125::nat +A126::nat A127::nat A128::nat A129::nat A130::nat A131::nat A132::nat +A133::nat A134::nat A135::nat A136::nat A137::nat A138::nat A139::nat +A140::nat A141::nat A142::nat A143::nat A144::nat A145::nat A146::nat +A147::nat A148::nat A149::nat A150::nat A151::nat A152::nat A153::nat +A154::nat A155::nat A156::nat A157::nat A158::nat A159::nat A160::nat +A161::nat A162::nat A163::nat A164::nat A165::nat A166::nat A167::nat +A168::nat A169::nat A170::nat A171::nat A172::nat A173::nat A174::nat +A175::nat A176::nat A177::nat A178::nat A179::nat A180::nat A181::nat +A182::nat A183::nat A184::nat A185::nat A186::nat A187::nat A188::nat +A189::nat A190::nat A191::nat A192::nat A193::nat A194::nat A195::nat +A196::nat A197::nat A198::nat A199::nat A200::nat A201::nat A202::nat +A203::nat A204::nat A205::nat A206::nat A207::nat A208::nat A209::nat +A210::nat A211::nat A212::nat A213::nat A214::nat A215::nat A216::nat +A217::nat A218::nat A219::nat A220::nat A221::nat A222::nat A223::nat +A224::nat A225::nat A226::nat A227::nat A228::nat A229::nat A230::nat +A231::nat A232::nat A233::nat A234::nat A235::nat A236::nat A237::nat +A238::nat A239::nat A240::nat A241::nat A242::nat A243::nat A244::nat +A245::nat A246::nat A247::nat A248::nat A249::nat A250::nat A251::nat +A252::nat A253::nat A254::nat A255::nat A256::nat A257::nat A258::nat +A259::nat A260::nat A261::nat A262::nat A263::nat A264::nat A265::nat +A266::nat A267::nat A268::nat A269::nat A270::nat A271::nat A272::nat +A273::nat A274::nat A275::nat A276::nat A277::nat A278::nat A279::nat +A280::nat A281::nat A282::nat A283::nat A284::nat A285::nat A286::nat +A287::nat A288::nat A289::nat A290::nat A291::nat A292::nat A293::nat +A294::nat A295::nat A296::nat A297::nat A298::nat A299::nat A300::nat +A301::nat A302::nat A303::nat A304::nat A305::nat A306::nat A307::nat +A308::nat A309::nat A310::nat A311::nat A312::nat A313::nat A314::nat +A315::nat A316::nat A317::nat A318::nat A319::nat A320::nat A321::nat +A322::nat A323::nat A324::nat A325::nat A326::nat A327::nat A328::nat +A329::nat A330::nat A331::nat A332::nat A333::nat A334::nat A335::nat +A336::nat A337::nat A338::nat A339::nat A340::nat A341::nat A342::nat +A343::nat A344::nat A345::nat A346::nat A347::nat A348::nat A349::nat +A350::nat A351::nat A352::nat A353::nat A354::nat A355::nat A356::nat +A357::nat A358::nat A359::nat A360::nat A361::nat A362::nat A363::nat +A364::nat A365::nat A366::nat A367::nat A368::nat A369::nat A370::nat +A371::nat A372::nat A373::nat A374::nat A375::nat A376::nat A377::nat +A378::nat A379::nat A380::nat A381::nat A382::nat A383::nat A384::nat +A385::nat A386::nat A387::nat A388::nat A389::nat A390::nat A391::nat +A392::nat A393::nat A394::nat A395::nat A396::nat A397::nat A398::nat +A399::nat A400::nat A401::nat A402::nat A403::nat A404::nat A405::nat +A406::nat A407::nat A408::nat A409::nat A410::nat A411::nat A412::nat +A413::nat A414::nat A415::nat A416::nat A417::nat A418::nat A419::nat +A420::nat A421::nat A422::nat A423::nat A424::nat A425::nat A426::nat +A427::nat A428::nat A429::nat A430::nat A431::nat A432::nat A433::nat +A434::nat A435::nat A436::nat A437::nat A438::nat A439::nat A440::nat +A441::nat A442::nat A443::nat A444::nat A445::nat A446::nat A447::nat +A448::nat A449::nat A450::nat A451::nat A452::nat A453::nat A454::nat +A455::nat A456::nat A457::nat A458::nat A459::nat A460::nat A461::nat +A462::nat A463::nat A464::nat A465::nat A466::nat A467::nat A468::nat +A469::nat A470::nat A471::nat A472::nat A473::nat A474::nat A475::nat +A476::nat A477::nat A478::nat A479::nat A480::nat A481::nat A482::nat +A483::nat A484::nat A485::nat A486::nat A487::nat A488::nat A489::nat +A490::nat A491::nat A492::nat A493::nat A494::nat A495::nat A496::nat +A497::nat A498::nat A499::nat A500::nat + +text "9.0s" +statespace benchmark1000 = A1::nat A2::nat A3::nat A4::nat A5::nat +A6::nat A7::nat A8::nat A9::nat A10::nat A11::nat A12::nat A13::nat +A14::nat A15::nat A16::nat A17::nat A18::nat A19::nat A20::nat +A21::nat A22::nat A23::nat A24::nat A25::nat A26::nat A27::nat +A28::nat A29::nat A30::nat A31::nat A32::nat A33::nat A34::nat +A35::nat A36::nat A37::nat A38::nat A39::nat A40::nat A41::nat +A42::nat A43::nat A44::nat A45::nat A46::nat A47::nat A48::nat +A49::nat A50::nat A51::nat A52::nat A53::nat A54::nat A55::nat +A56::nat A57::nat A58::nat A59::nat A60::nat A61::nat A62::nat +A63::nat A64::nat A65::nat A66::nat A67::nat A68::nat A69::nat +A70::nat A71::nat A72::nat A73::nat A74::nat A75::nat A76::nat +A77::nat A78::nat A79::nat A80::nat A81::nat A82::nat A83::nat +A84::nat A85::nat A86::nat A87::nat A88::nat A89::nat A90::nat +A91::nat A92::nat A93::nat A94::nat A95::nat A96::nat A97::nat +A98::nat A99::nat A100::nat A101::nat A102::nat A103::nat A104::nat +A105::nat A106::nat A107::nat A108::nat A109::nat A110::nat A111::nat +A112::nat A113::nat A114::nat A115::nat A116::nat A117::nat A118::nat +A119::nat A120::nat A121::nat A122::nat A123::nat A124::nat A125::nat +A126::nat A127::nat A128::nat A129::nat A130::nat A131::nat A132::nat +A133::nat A134::nat A135::nat A136::nat A137::nat A138::nat A139::nat +A140::nat A141::nat A142::nat A143::nat A144::nat A145::nat A146::nat +A147::nat A148::nat A149::nat A150::nat A151::nat A152::nat A153::nat +A154::nat A155::nat A156::nat A157::nat A158::nat A159::nat A160::nat +A161::nat A162::nat A163::nat A164::nat A165::nat A166::nat A167::nat +A168::nat A169::nat A170::nat A171::nat A172::nat A173::nat A174::nat +A175::nat A176::nat A177::nat A178::nat A179::nat A180::nat A181::nat +A182::nat A183::nat A184::nat A185::nat A186::nat A187::nat A188::nat +A189::nat A190::nat A191::nat A192::nat A193::nat A194::nat A195::nat +A196::nat A197::nat A198::nat A199::nat A200::nat A201::nat A202::nat +A203::nat A204::nat A205::nat A206::nat A207::nat A208::nat A209::nat +A210::nat A211::nat A212::nat A213::nat A214::nat A215::nat A216::nat +A217::nat A218::nat A219::nat A220::nat A221::nat A222::nat A223::nat +A224::nat A225::nat A226::nat A227::nat A228::nat A229::nat A230::nat +A231::nat A232::nat A233::nat A234::nat A235::nat A236::nat A237::nat +A238::nat A239::nat A240::nat A241::nat A242::nat A243::nat A244::nat +A245::nat A246::nat A247::nat A248::nat A249::nat A250::nat A251::nat +A252::nat A253::nat A254::nat A255::nat A256::nat A257::nat A258::nat +A259::nat A260::nat A261::nat A262::nat A263::nat A264::nat A265::nat +A266::nat A267::nat A268::nat A269::nat A270::nat A271::nat A272::nat +A273::nat A274::nat A275::nat A276::nat A277::nat A278::nat A279::nat +A280::nat A281::nat A282::nat A283::nat A284::nat A285::nat A286::nat +A287::nat A288::nat A289::nat A290::nat A291::nat A292::nat A293::nat +A294::nat A295::nat A296::nat A297::nat A298::nat A299::nat A300::nat +A301::nat A302::nat A303::nat A304::nat A305::nat A306::nat A307::nat +A308::nat A309::nat A310::nat A311::nat A312::nat A313::nat A314::nat +A315::nat A316::nat A317::nat A318::nat A319::nat A320::nat A321::nat +A322::nat A323::nat A324::nat A325::nat A326::nat A327::nat A328::nat +A329::nat A330::nat A331::nat A332::nat A333::nat A334::nat A335::nat +A336::nat A337::nat A338::nat A339::nat A340::nat A341::nat A342::nat +A343::nat A344::nat A345::nat A346::nat A347::nat A348::nat A349::nat +A350::nat A351::nat A352::nat A353::nat A354::nat A355::nat A356::nat +A357::nat A358::nat A359::nat A360::nat A361::nat A362::nat A363::nat +A364::nat A365::nat A366::nat A367::nat A368::nat A369::nat A370::nat +A371::nat A372::nat A373::nat A374::nat A375::nat A376::nat A377::nat +A378::nat A379::nat A380::nat A381::nat A382::nat A383::nat A384::nat +A385::nat A386::nat A387::nat A388::nat A389::nat A390::nat A391::nat +A392::nat A393::nat A394::nat A395::nat A396::nat A397::nat A398::nat +A399::nat A400::nat A401::nat A402::nat A403::nat A404::nat A405::nat +A406::nat A407::nat A408::nat A409::nat A410::nat A411::nat A412::nat +A413::nat A414::nat A415::nat A416::nat A417::nat A418::nat A419::nat +A420::nat A421::nat A422::nat A423::nat A424::nat A425::nat A426::nat +A427::nat A428::nat A429::nat A430::nat A431::nat A432::nat A433::nat +A434::nat A435::nat A436::nat A437::nat A438::nat A439::nat A440::nat +A441::nat A442::nat A443::nat A444::nat A445::nat A446::nat A447::nat +A448::nat A449::nat A450::nat A451::nat A452::nat A453::nat A454::nat +A455::nat A456::nat A457::nat A458::nat A459::nat A460::nat A461::nat +A462::nat A463::nat A464::nat A465::nat A466::nat A467::nat A468::nat +A469::nat A470::nat A471::nat A472::nat A473::nat A474::nat A475::nat +A476::nat A477::nat A478::nat A479::nat A480::nat A481::nat A482::nat +A483::nat A484::nat A485::nat A486::nat A487::nat A488::nat A489::nat +A490::nat A491::nat A492::nat A493::nat A494::nat A495::nat A496::nat +A497::nat A498::nat A499::nat A500::nat A501::nat A502::nat A503::nat +A504::nat A505::nat A506::nat A507::nat A508::nat A509::nat A510::nat +A511::nat A512::nat A513::nat A514::nat A515::nat A516::nat A517::nat +A518::nat A519::nat A520::nat A521::nat A522::nat A523::nat A524::nat +A525::nat A526::nat A527::nat A528::nat A529::nat A530::nat A531::nat +A532::nat A533::nat A534::nat A535::nat A536::nat A537::nat A538::nat +A539::nat A540::nat A541::nat A542::nat A543::nat A544::nat A545::nat +A546::nat A547::nat A548::nat A549::nat A550::nat A551::nat A552::nat +A553::nat A554::nat A555::nat A556::nat A557::nat A558::nat A559::nat +A560::nat A561::nat A562::nat A563::nat A564::nat A565::nat A566::nat +A567::nat A568::nat A569::nat A570::nat A571::nat A572::nat A573::nat +A574::nat A575::nat A576::nat A577::nat A578::nat A579::nat A580::nat +A581::nat A582::nat A583::nat A584::nat A585::nat A586::nat A587::nat +A588::nat A589::nat A590::nat A591::nat A592::nat A593::nat A594::nat +A595::nat A596::nat A597::nat A598::nat A599::nat A600::nat A601::nat +A602::nat A603::nat A604::nat A605::nat A606::nat A607::nat A608::nat +A609::nat A610::nat A611::nat A612::nat A613::nat A614::nat A615::nat +A616::nat A617::nat A618::nat A619::nat A620::nat A621::nat A622::nat +A623::nat A624::nat A625::nat A626::nat A627::nat A628::nat A629::nat +A630::nat A631::nat A632::nat A633::nat A634::nat A635::nat A636::nat +A637::nat A638::nat A639::nat A640::nat A641::nat A642::nat A643::nat +A644::nat A645::nat A646::nat A647::nat A648::nat A649::nat A650::nat +A651::nat A652::nat A653::nat A654::nat A655::nat A656::nat A657::nat +A658::nat A659::nat A660::nat A661::nat A662::nat A663::nat A664::nat +A665::nat A666::nat A667::nat A668::nat A669::nat A670::nat A671::nat +A672::nat A673::nat A674::nat A675::nat A676::nat A677::nat A678::nat +A679::nat A680::nat A681::nat A682::nat A683::nat A684::nat A685::nat +A686::nat A687::nat A688::nat A689::nat A690::nat A691::nat A692::nat +A693::nat A694::nat A695::nat A696::nat A697::nat A698::nat A699::nat +A700::nat A701::nat A702::nat A703::nat A704::nat A705::nat A706::nat +A707::nat A708::nat A709::nat A710::nat A711::nat A712::nat A713::nat +A714::nat A715::nat A716::nat A717::nat A718::nat A719::nat A720::nat +A721::nat A722::nat A723::nat A724::nat A725::nat A726::nat A727::nat +A728::nat A729::nat A730::nat A731::nat A732::nat A733::nat A734::nat +A735::nat A736::nat A737::nat A738::nat A739::nat A740::nat A741::nat +A742::nat A743::nat A744::nat A745::nat A746::nat A747::nat A748::nat +A749::nat A750::nat A751::nat A752::nat A753::nat A754::nat A755::nat +A756::nat A757::nat A758::nat A759::nat A760::nat A761::nat A762::nat +A763::nat A764::nat A765::nat A766::nat A767::nat A768::nat A769::nat +A770::nat A771::nat A772::nat A773::nat A774::nat A775::nat A776::nat +A777::nat A778::nat A779::nat A780::nat A781::nat A782::nat A783::nat +A784::nat A785::nat A786::nat A787::nat A788::nat A789::nat A790::nat +A791::nat A792::nat A793::nat A794::nat A795::nat A796::nat A797::nat +A798::nat A799::nat A800::nat A801::nat A802::nat A803::nat A804::nat +A805::nat A806::nat A807::nat A808::nat A809::nat A810::nat A811::nat +A812::nat A813::nat A814::nat A815::nat A816::nat A817::nat A818::nat +A819::nat A820::nat A821::nat A822::nat A823::nat A824::nat A825::nat +A826::nat A827::nat A828::nat A829::nat A830::nat A831::nat A832::nat +A833::nat A834::nat A835::nat A836::nat A837::nat A838::nat A839::nat +A840::nat A841::nat A842::nat A843::nat A844::nat A845::nat A846::nat +A847::nat A848::nat A849::nat A850::nat A851::nat A852::nat A853::nat +A854::nat A855::nat A856::nat A857::nat A858::nat A859::nat A860::nat +A861::nat A862::nat A863::nat A864::nat A865::nat A866::nat A867::nat +A868::nat A869::nat A870::nat A871::nat A872::nat A873::nat A874::nat +A875::nat A876::nat A877::nat A878::nat A879::nat A880::nat A881::nat +A882::nat A883::nat A884::nat A885::nat A886::nat A887::nat A888::nat +A889::nat A890::nat A891::nat A892::nat A893::nat A894::nat A895::nat +A896::nat A897::nat A898::nat A899::nat A900::nat A901::nat A902::nat +A903::nat A904::nat A905::nat A906::nat A907::nat A908::nat A909::nat +A910::nat A911::nat A912::nat A913::nat A914::nat A915::nat A916::nat +A917::nat A918::nat A919::nat A920::nat A921::nat A922::nat A923::nat +A924::nat A925::nat A926::nat A927::nat A928::nat A929::nat A930::nat +A931::nat A932::nat A933::nat A934::nat A935::nat A936::nat A937::nat +A938::nat A939::nat A940::nat A941::nat A942::nat A943::nat A944::nat +A945::nat A946::nat A947::nat A948::nat A949::nat A950::nat A951::nat +A952::nat A953::nat A954::nat A955::nat A956::nat A957::nat A958::nat +A959::nat A960::nat A961::nat A962::nat A963::nat A964::nat A965::nat +A966::nat A967::nat A968::nat A969::nat A970::nat A971::nat A972::nat +A973::nat A974::nat A975::nat A976::nat A977::nat A978::nat A979::nat +A980::nat A981::nat A982::nat A983::nat A984::nat A985::nat A986::nat +A987::nat A988::nat A989::nat A990::nat A991::nat A992::nat A993::nat +A994::nat A995::nat A996::nat A997::nat A998::nat A999::nat A1000::nat + end diff -r cc455b2897f8 -r ccec8b6d5d81 src/HOL/Statespace/StateSpaceLocale.thy --- a/src/HOL/Statespace/StateSpaceLocale.thy Sun Nov 06 14:23:04 2011 +0100 +++ b/src/HOL/Statespace/StateSpaceLocale.thy Sun Nov 06 18:42:17 2011 +0100 @@ -19,21 +19,20 @@ fixes project :: "'value \ 'a" and inject :: "'a \ 'value" assumes project_inject_cancel [statefun_simp]: "project (inject x) = x" +begin -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 ex_project [statefun_simp]: "\v. project v = x" +proof + show "project (inject x) = x" + by (rule project_inject_cancel) +qed -lemma (in project_inject) - project_inject_comp_id [statefun_simp]: "project \ inject = id" +lemma 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" +lemma project_inject_comp_cancel[statefun_simp]: "f \ project \ inject = f" by (rule ext) (simp add: project_inject_cancel) - +end end \ No newline at end of file diff -r cc455b2897f8 -r ccec8b6d5d81 src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Sun Nov 06 14:23:04 2011 +0100 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Sun Nov 06 18:42:17 2011 +0100 @@ -4,101 +4,92 @@ signature DISTINCT_TREE_PROVER = sig - datatype Direction = Left | Right + datatype direction = Left | Right val mk_tree : ('a -> term) -> typ -> 'a list -> term val dest_tree : term -> term list - val find_tree : term -> term -> Direction list option + val find_tree : term -> term -> direction list option val neq_to_eq_False : thm - val distinctTreeProver : thm -> Direction list -> Direction list -> thm - val neq_x_y : Proof.context -> term -> term -> string -> thm option + val distinctTreeProver : thm -> direction list -> direction list -> thm + val neq_x_y : Proof.context -> term -> term -> string -> thm option val distinctFieldSolver : string list -> solver val distinctTree_tac : string list -> Proof.context -> int -> tactic val distinct_implProver : thm -> cterm -> thm val subtractProver : term -> cterm -> thm -> thm val distinct_simproc : string list -> simproc - + val discharge : thm list -> thm -> thm end; structure DistinctTreeProver : DISTINCT_TREE_PROVER = struct -val all_distinct_left = @{thm DistinctTreeProver.all_distinct_left}; -val all_distinct_right = @{thm DistinctTreeProver.all_distinct_right}; +val neq_to_eq_False = @{thm neq_to_eq_False}; -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}; +datatype direction = Left | Right; -val swap_neq = @{thm DistinctTreeProver.swap_neq}; -val neq_to_eq_False = @{thm DistinctTreeProver.neq_to_eq_False}; - -datatype Direction = Left | Right - -fun treeT T = Type ("DistinctTreeProver.tree",[T]); -fun mk_tree' e T n [] = Const ("DistinctTreeProver.tree.Tip",treeT T) +fun treeT T = Type (@{type_name tree}, [T]); +fun mk_tree' e T n [] = Const (@{const_name 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 + in + Const (@{const_name 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 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]); +fun dest_tree (Const (@{const_name Tip}, _)) = [] + | dest_tree (Const (@{const_name Node}, _) $ l $ e $ _ $ r) = dest_tree l @ e :: dest_tree r + | dest_tree t = raise TERM ("dest_tree", [t]); -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 +fun lin_find_tree e (Const (@{const_name Tip}, _)) = NONE + | lin_find_tree e (Const (@{const_name 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]) + 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 bin_find_tree order e (Const (@{const_name Tip}, _)) = NONE + | bin_find_tree order e (Const (@{const_name 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_Ord.fast_term_ord e t of - NONE => lin_find_tree e t - | x => x); + 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 index_tree (Const (@{const_name Tip}, _)) path tab = tab + | index_tree (Const (@{const_name 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) +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 @@ -106,14 +97,14 @@ *) fun instantiate instTs insts = let - val instTs' = map (fn (T,U) => (dest_TVar (typ_of T),typ_of U)) instTs; + 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; + 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", @@ -141,62 +132,69 @@ in match end; -(* expects that relevant type variables are already contained in +(* 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 = +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; + 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 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 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 Thm.elim_implies prems rule' end; + 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 Thm.elim_implies 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 (l_in_set_root, x_in_set_root, r_in_set_root) = + let + val (Node_l_x_d, r) = + cprop_of @{thm 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_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 +val (x_in_set_left, r_in_set_left) = + let + val (Node_l_x_d, r) = + cprop_of @{thm 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 @{thm 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 (* @@ -210,127 +208,132 @@ 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) + | dist_subtree (p :: ps) thm = + let + val rule = + (case p of Left => @{thm all_distinct_left} | Right => @{thm 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 (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; - + val (_, [l, _, _, r]) = Drule.strip_comb subtree; + fun in_set ps tree = let - val (_,[l,x,_,r]) = Drule.strip_comb tree; + 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; + 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)] @{thm 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)] @{thm 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)] @{thm in_set_right}; + in discharge [in_set_r] in_set_right' end) + end; - 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 + 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] @{thm distinct_left} + | distinct_lr node_in_set Right = discharge [dist_subtree_thm, node_in_set] @{thm 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 (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] @{thm distinct_left_right}) + | Right => + (true, discharge [dist_subtree_thm, y_in_set, x_in_set] @{thm distinct_left_right})) + end)); + in if swap then discharge [neq] @{thm 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] +fun deleteProver dist_thm [] = @{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}; + let + val dist_rule = + (case p of Left => @{thm all_distinct_left} | Right => @{thm all_distinct_right}); + val dist_thm' = discharge [dist_thm] dist_rule; + val del_rule = (case p of Left => @{thm delete_left} | Right => @{thm delete_right}); + val del = deleteProver dist_thm' ps; + in discharge [dist_thm, del] del_rule end; local - val (alpha,v) = + val (alpha, v) = let - val ct = subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 - |> Thm.dest_comb |> #2 + val ct = + @{thm 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 subtractProver (Const (@{const_name 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')]) @{thm subtract_Tip} + end + | subtractProver (Const (@{const_name 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] @{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'] @{thm subtract_Some_all_distinct_res}); + in discharge [del_tree, sub_l, sub_r] @{thm subtract_Node} end; + +end; + 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; + in @{thm 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); + | 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 @@ -340,8 +343,8 @@ 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) + in SOME thm + end handle Option.Option => NONE); fun distinctTree_tac names ctxt = SUBGOAL (fn (goal, i) => (case goal of @@ -352,17 +355,18 @@ | NONE => no_tac) | _ => no_tac)) -fun distinctFieldSolver names = mk_solver "distinctFieldSolver" - (distinctTree_tac names o Simplifier.the_context) +fun distinctFieldSolver names = + mk_solver "distinctFieldSolver" (distinctTree_tac names o Simplifier.the_context); fun distinct_simproc names = Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"] - (fn thy => fn ss => fn (Const (@{const_name HOL.eq},_)$x$y) => - case try Simplifier.the_context 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 - ) + (fn thy => fn ss => fn (Const (@{const_name HOL.eq}, _) $ x $ y) => + (case try Simplifier.the_context ss of + SOME ctxt => + Option.map (fn neq => @{thm neq_to_eq_False} OF [neq]) + (get_fst_success (neq_x_y ctxt x y) names) + | NONE => NONE)); -end +end; + end; \ No newline at end of file diff -r cc455b2897f8 -r ccec8b6d5d81 src/HOL/Statespace/document/root.tex --- a/src/HOL/Statespace/document/root.tex Sun Nov 06 14:23:04 2011 +0100 +++ b/src/HOL/Statespace/document/root.tex Sun Nov 06 18:42:17 2011 +0100 @@ -20,26 +20,34 @@ \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. +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 +\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. +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 diff -r cc455b2897f8 -r ccec8b6d5d81 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Sun Nov 06 14:23:04 2011 +0100 +++ b/src/HOL/Statespace/state_fun.ML Sun Nov 06 18:42:17 2011 +0100 @@ -20,22 +20,23 @@ val setup : theory -> theory end; -structure StateFun: STATE_FUN = +structure StateFun: STATE_FUN = struct -val lookupN = "StateFun.lookup"; -val updateN = "StateFun.update"; +val lookupN = @{const_name StateFun.lookup}; +val updateN = @{const_name StateFun.update}; val sel_name = HOLogic.dest_string; 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)) - + 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}; @@ -43,9 +44,10 @@ val conj_True = @{thm conj_True}; val conj_cong = @{thm conj_cong}; -fun isFalse (Const (@{const_name False},_)) = true +fun isFalse (Const (@{const_name False}, _)) = true | isFalse _ = false; -fun isTrue (Const (@{const_name True},_)) = true + +fun isTrue (Const (@{const_name True}, _)) = true | isTrue _ = false; in @@ -53,36 +55,34 @@ val lazy_conj_simproc = Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"] (fn thy => fn ss => fn t => - (case t of (Const (@{const_name HOL.conj},_)$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 + (case t of (Const (@{const_name HOL.conj},_) $ 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 +val string_eq_simp_tac = simp_tac (HOL_basic_ss addsimps (@{thms list.inject} @ @{thms char.inject} @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms}) addsimprocs [lazy_conj_simproc] - addcongs [@{thm block_conj_cong}]) + addcongs [@{thm block_conj_cong}]); end; -val lookup_ss = (HOL_basic_ss +val lookup_ss = (HOL_basic_ss addsimps (@{thms list.inject} @ @{thms char.inject} @ @{thms list.distinct} @ @{thms char.distinct} @ @{thms simp_thms} @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel}, @@ -94,235 +94,238 @@ val ex_lookup_ss = HOL_ss addsimps @{thms StateFun.ex_id}; -structure StateFunData = Generic_Data +structure Data = Generic_Data ( - type T = simpset * simpset * bool; - (* lookup simpset, ex_lookup simpset, are simprocs installed *) + 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 ((ss1, ex_ss1, b1), (ss2, ex_ss2, b2)) = - (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2 (* FIXME odd merge *)); + (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2); ); val init_state_fun_data = - Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false)); + Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false)); val lookup_simproc = Simplifier.simproc_global @{theory} "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)$_$_$_$_$_)) => + (case t of (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $ + (s as Const (@{const_name 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))); + fun mk_upds (Const (@{const_name 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 (@{const_name K_statefun}, KT) $ v'' => + (case v'' of + (Const (@{const_name StateFun.lookup}, _) $ + (d as (Const (@{const_name 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 (@{const_name StateFun.K_statefun}, KT) $ + Var (("v", cnt), vT), cnt + 1) + | _ => + (Const (@{const_name StateFun.K_statefun}, KT) $ + Var (("v", cnt), vT), cnt + 1)) + | _ => (v, cnt)); + in (Const (@{const_name 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 (@{const_name StateFun.lookup}, lT) $ destr $ n $ fst (mk_upds s)); val ctxt = Simplifier.the_context ss; - val basic_ss = #1 (StateFunData.get (Context.Proof ctxt)); + val basic_ss = #1 (Data.get (Context.Proof ctxt)); val ss' = Simplifier.context (Config.put simp_depth_limit 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 + in + if (op aconv) (Logic.dest_equals (prop_of thm)) + then NONE + else SOME thm end - handle Option => NONE) - + handle Option.Option => NONE) | _ => NONE )); local + val meta_ext = @{thm StateFun.meta_ext}; val ss' = (HOL_ss addsimps (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject} @ @{thms list.distinct} @ @{thms char.distinct}) addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc] addcongs @{thms block_conj_cong}); + in + val update_simproc = Simplifier.simproc_global @{theory} "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); + (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_comp f fT g gT = + let val T = domain_type fT --> range_type gT + in (Const (@{const_name Fun.comp}, gT --> fT --> T) $ g $ f, T) end; - fun mk_comps fs = - foldl1 (fn ((f,fT),(g,gT)) => mk_comp g gT f fT) fs; + fun mk_comps fs = foldl1 (fn ((f, fT), (g, gT)) => mk_comp g gT f fT) 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 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 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; + 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 occurred. - "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; + (* mk_updterm returns + * - (orig-term-skeleton,simplified-term-skeleton, vars, b) + * where boolean b tells if a simplification has occurred. + "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 (@{const_name 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 = Simplifier.the_context ss |> Config.put simp_depth_limit 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, Logic.mk_equals (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 (Thm.transitive eq1 eq2) end - | _ => NONE) - end - | _ => NONE)); -end + val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100; + val ss1 = Simplifier.context ctxt ss'; + val ss2 = Simplifier.context ctxt (#1 (Data.get (Context.Proof ctxt))); + in + (case mk_updterm [] t of + (trm, trm', vars, _, true) => + let + val eq1 = + Goal.prove ctxt [] [] + (list_all (vars, Logic.mk_equals (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 (Thm.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) = Record.get_recT_fields thy T - in member (fn (s,(n,_)) => n=s) (more::flds) sel - end; + let val (flds, more) = Record.get_recT_fields thy T + in member (fn (s, (n, _)) => n = s) (more :: flds) sel end; + in + val ex_lookup_eq_simproc = Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"] (fn thy => fn ss => fn t => - let - val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 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); + let + val ctxt = Simplifier.the_context ss |> Config.put simp_depth_limit 100; + val ex_lookup_ss = #2 (Data.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 (Term.is_dependent x) - then Bound 1 - else raise TERM ("",[x]); - val n' = if not (Term.is_dependent n) - then Bound 2 - else raise TERM ("",[n]); - val sel' = lo $ d $ n' $ s; - in (Const (@{const_name HOL.eq},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end; + 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 (Term.is_dependent x) then Bound 1 else raise TERM ("", [x]); + val n' = if not (Term.is_dependent n) then Bound 2 else raise TERM ("", [n]); + val sel' = lo $ d $ n' $ s; + in (Const (@{const_name HOL.eq}, 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_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 (@{const_name HOL.eq},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 (@{const_name HOL.eq},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 ("",[]); + fun dest_sel_eq + (Const (@{const_name HOL.eq}, Teq) $ + ((lo as (Const (@{const_name StateFun.lookup}, lT))) $ d $ n $ s) $ X) = + (false, Teq, lT, lo, d, n, X, dest_state s) + | dest_sel_eq + (Const (@{const_name HOL.eq}, Teq) $ X $ + ((lo as (Const (@{const_name 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 (@{const_name 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 (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const)); + val thm = Drule.export_without_context (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.Option => NONE); - in - (case t of - (Const (@{const_name 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 (@{const_name Ex},Tex)$Abs(s,T,eq), - HOLogic.true_const)); - val thm = Drule.export_without_context (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 = +fun mkUpper str = (case String.explode str of [] => "" - | c::cs => String.implode (Char.toUpper c::cs )) + | c::cs => String.implode (Char.toUpper c :: cs)); fun mkName (Type (T,args)) = implode (map mkName args) ^ mkUpper (Long_Name.base_name T) | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x) @@ -333,50 +336,53 @@ fun mk_map "List.list" = Syntax.const "List.map" | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n); -fun gen_constr_destr comp prfx thy (Type (T,[])) = +fun gen_constr_destr comp prfx thy (Type (T, [])) = Syntax.const (deco prfx (mkUpper (Long_Name.base_name T))) | gen_constr_destr comp prfx thy (T as Type ("fun",_)) = - let val (argTs,rangeT) = strip_type T; - in comp + let val (argTs, rangeT) = strip_type T; + in + comp (Syntax.const (deco prfx (implode (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 (Long_Name.base_name 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 (implode (map mkName argTs) ^ mkUpper (Long_Name.base_name 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_" + (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 (Long_Name.base_name 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 (implode (map mkName argTs) ^ mkUpper (Long_Name.base_name 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 @{const_name Fun.comp} $ a $ b) ""; +val mk_destr = gen_constr_destr (fn a => fn b => Syntax.const @{const_name Fun.comp} $ b $ a) "the_"; + + val statefun_simp_attr = Thm.declaration_attribute (fn thm => fn ctxt => let - val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt; - val (lookup_ss', ex_lookup_ss') = - (case (concl_of thm) of - (_$((Const (@{const_name 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 Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt + val (lookup_ss, ex_lookup_ss, simprocs_active) = Data.get ctxt; + val (lookup_ss', ex_lookup_ss') = + (case concl_of thm of + (_ $ ((Const (@{const_name 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 Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc, update_simproc]) ctxt; in - ctxt + ctxt |> activate_simprocs - |> (StateFunData.put (lookup_ss',ex_lookup_ss',true)) + |> Data.put (lookup_ss', ex_lookup_ss', true) end); -val setup = +val setup = init_state_fun_data #> Attrib.setup @{binding statefun_simp} (Scan.succeed statefun_simp_attr) - "simplification in statespaces" -end + "simplification in statespaces"; + +end; diff -r cc455b2897f8 -r ccec8b6d5d81 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Sun Nov 06 14:23:04 2011 +0100 +++ b/src/HOL/Statespace/state_space.ML Sun Nov 06 18:42:17 2011 +0100 @@ -3,67 +3,65 @@ *) signature STATE_SPACE = - sig - val KN : string - val distinct_compsN : string - val getN : string - val putN : string - val injectN : string - val namespaceN : string - val projectN : string - val valuetypesN : string +sig + val distinct_compsN : string + val getN : string + val putN : string + val injectN : string + val namespaceN : string + val projectN : string + val valuetypesN : string - val namespace_definition : - bstring -> - typ -> - Expression.expression -> - string list -> string list -> theory -> theory + val namespace_definition : + bstring -> + typ -> + Expression.expression -> + string list -> string list -> theory -> theory - val define_statespace : - string list -> - string -> - (string list * bstring * (string * string) list) list -> - (string * string) list -> theory -> theory - val define_statespace_i : - string option -> - string list -> - string -> - (typ list * bstring * (string * string) list) list -> - (string * typ) list -> theory -> theory + val define_statespace : + string list -> + string -> + (string list * bstring * (string * string) list) list -> + (string * string) list -> theory -> theory + val define_statespace_i : + string option -> + string list -> + string -> + (typ list * bstring * (string * string) list) list -> + (string * typ) list -> theory -> theory - val statespace_decl : - ((string list * bstring) * - ((string list * xstring * (bstring * bstring) list) list * - (bstring * string) list)) parser + val statespace_decl : + ((string list * bstring) * + ((string list * xstring * (bstring * bstring) list) list * + (bstring * string) list)) parser - val neq_x_y : Proof.context -> term -> term -> thm option - val distinctNameSolver : Simplifier.solver - val distinctTree_tac : Proof.context -> int -> tactic - val distinct_simproc : Simplifier.simproc + val neq_x_y : Proof.context -> term -> term -> thm option + val distinctNameSolver : Simplifier.solver + val distinctTree_tac : Proof.context -> int -> tactic + val distinct_simproc : Simplifier.simproc - val get_comp : Context.generic -> string -> (typ * string) Option.option - val get_silent : Context.generic -> bool - val set_silent : bool -> Context.generic -> Context.generic + val get_comp : Context.generic -> string -> (typ * string) Option.option + val get_silent : Context.generic -> bool + val set_silent : bool -> Context.generic -> Context.generic - val gen_lookup_tr : Proof.context -> term -> string -> term - val lookup_swap_tr : Proof.context -> term list -> term - val lookup_tr : Proof.context -> term list -> term - val lookup_tr' : Proof.context -> term list -> term + val gen_lookup_tr : Proof.context -> term -> string -> term + val lookup_swap_tr : Proof.context -> term list -> term + val lookup_tr : Proof.context -> term list -> term + val lookup_tr' : Proof.context -> term list -> term - val gen_update_tr : - bool -> Proof.context -> string -> term -> term -> term - val update_tr : Proof.context -> term list -> term - val update_tr' : Proof.context -> term list -> term - end; + val gen_update_tr : + bool -> Proof.context -> string -> term -> term -> term + val update_tr : Proof.context -> term list -> term + val update_tr' : Proof.context -> term list -> term +end; structure StateSpace : STATE_SPACE = struct -(* Theorems *) +(* Names *) -(* Names *) val distinct_compsN = "distinct_names" val namespaceN = "_namespace" val valuetypesN = "_valuetypes" @@ -72,7 +70,6 @@ val getN = "get" val putN = "put" val project_injectL = "StateSpaceLocale.project_inject"; -val KN = "StateFun.K_statefun" (* Library *) @@ -150,13 +147,13 @@ |> Proof_Context.theory_of fun add_locale name expr elems thy = - thy + thy |> Expression.add_locale I (Binding.name name) (Binding.name name) expr elems |> snd |> Local_Theory.exit; fun add_locale_cmd name expr elems thy = - thy + thy |> Expression.add_locale_cmd I (Binding.name name) Binding.empty expr elems |> snd |> Local_Theory.exit; @@ -213,7 +210,7 @@ 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) + end handle Option.Option => NONE) fun distinctTree_tac ctxt = SUBGOAL (fn (goal, i) => (case goal of @@ -225,24 +222,24 @@ | NONE => no_tac) | _ => no_tac)); -val distinctNameSolver = mk_solver "distinctNameSolver" - (distinctTree_tac o Simplifier.the_context) +val distinctNameSolver = + mk_solver "distinctNameSolver" (distinctTree_tac o Simplifier.the_context); val distinct_simproc = Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"] (fn thy => fn ss => (fn (Const (@{const_name HOL.eq},_)$(x as Free _)$(y as Free _)) => (case try Simplifier.the_context ss of - SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) - (neq_x_y ctxt x y) + SOME ctxt => + Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) + (neq_x_y ctxt x y) | NONE => NONE) - | _ => NONE)) + | _ => NONE)); local val ss = HOL_basic_ss in fun interprete_parent name dist_thm_name parent_expr thy = let - fun solve_tac ctxt = CSUBGOAL (fn (goal, i) => let val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name; @@ -252,8 +249,8 @@ fun tac ctxt = Locale.intro_locales_tac true ctxt [] THEN ALLGOALS (solve_tac ctxt); - in thy - |> prove_interpretation_in tac (name,parent_expr) + in + thy |> prove_interpretation_in tac (name, parent_expr) end; end; @@ -295,17 +292,17 @@ val attr = Attrib.internal type_attr; - val assumes = Element.Assumes [((Binding.name 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 - |> add_locale name ([],vars) [assumes] - |> Proof_Context.theory_of - |> interprete_parent name dist_thm_full_name parent_expr + val assume = + ((Binding.name dist_thm_name, [attr]), + [(HOLogic.Trueprop $ + (Const (@{const_name all_distinct}, Type (@{type_name tree}, [nameT]) --> HOLogic.boolT) $ + DistinctTreeProver.mk_tree (fn n => Free (n, nameT)) nameT + (sort fast_string_ord all_comps)), [])]); + in + thy + |> add_locale name ([], vars) [Element.Assumes [assume]] + |> Proof_Context.theory_of + |> interprete_parent name dist_thm_full_name parent_expr end; fun encode_dot x = if x= #"." then #"_" else x; @@ -329,12 +326,14 @@ 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 lookup_const T nT V = + Const (@{const_name 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)); + Const (@{const_name StateFun.update}, + (V --> T) --> (T --> V) --> nT --> (T --> T) --> (nT --> V) --> (nT --> V)); -fun K_const T = Const ("StateFun.K_statefun",T --> T --> T); +fun K_const T = Const (@{const_name K_statefun}, T --> T --> T); fun add_declaration name decl thy = @@ -349,8 +348,7 @@ 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 {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 = @@ -385,8 +383,8 @@ fun projectT T = valueT --> T; fun injectT T = T --> valueT; val locinsts = map (fn T => (project_injectL, - (("",false),Expression.Positional - [SOME (Free (project_name T,projectT T)), + (("",false),Expression.Positional + [SOME (Free (project_name T,projectT T)), SOME (Free ((inject_name T,injectT T)))]))) Ts; val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn), (Binding.name (inject_name T),NONE,NoSyn)]) Ts; @@ -400,7 +398,7 @@ val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types; - val expr = ([(suffix valuetypesN name, + val expr = ([(suffix valuetypesN name, (("",false),Expression.Positional (map SOME pars)))],[]); in prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of) @@ -450,12 +448,12 @@ (map fst parent_comps) (map fst components) |> Context.theory_map (add_statespace full_name args parents components []) |> add_locale (suffix valuetypesN name) (locinsts,locs) [] - |> Proof_Context.theory_of + |> Proof_Context.theory_of |> fold interprete_parent_valuetypes parents |> add_locale_cmd name ([(suffix namespaceN full_name ,(("",false),Expression.Named [])), (suffix valuetypesN full_name,(("",false),Expression.Named []))],[]) fixestate - |> Proof_Context.theory_of + |> Proof_Context.theory_of |> fold interprete_parent parents |> add_declaration full_name (declare_declinfo components') end; @@ -588,9 +586,9 @@ 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 @@ -605,13 +603,15 @@ 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 "undefined" $ Syntax.free n $ s - else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[])); + (case get_comp (Context.Proof ctxt) n of + SOME (T, _) => + Syntax.const @{const_name StateFun.lookup} $ + Syntax.free (project_name T) $ Syntax.free n $ s + | NONE => + if get_silent (Context.Proof ctxt) + then Syntax.const @{const_name StateFun.lookup} $ + Syntax.const @{const_syntax undefined} $ Syntax.free n $ s + else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined", [])); fun lookup_tr ctxt [s, x] = (case Term_Position.strip_positions x of @@ -620,29 +620,31 @@ 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 +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 "undefined" $ Syntax.const "undefined" $ - Syntax.free n $ (Syntax.const KN $ v) $ s - else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined",[])) + fun pname T = if id then @{const_name Fun.id} else project_name T; + fun iname T = if id then @{const_name Fun.id} else inject_name T; + in + (case get_comp (Context.Proof ctxt) n of + SOME (T, _) => + Syntax.const @{const_name StateFun.update} $ + Syntax.free (pname T) $ Syntax.free (iname T) $ + Syntax.free n $ (Syntax.const @{const_name K_statefun} $ v) $ s + | NONE => + if get_silent (Context.Proof ctxt) then + Syntax.const @{const_name StateFun.update} $ + Syntax.const @{const_syntax undefined} $ Syntax.const @{const_syntax undefined} $ + Syntax.free n $ (Syntax.const @{const_name K_statefun} $ v) $ s + else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined", [])) end; fun update_tr ctxt [s, x, v] = @@ -650,13 +652,15 @@ Free (n, _) => gen_update_tr false ctxt n v s | _ => raise Match); -fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] = - if Long_Name.base_name k = Long_Name.base_name KN then +fun update_tr' ctxt + [_ $ Free (prj, _), _ $ Free (inj, _), n as (_ $ Free (name, _)), (Const (k, _) $ v), s] = + if Long_Name.base_name k = Long_Name.base_name @{const_name K_statefun} 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) + 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; @@ -665,6 +669,8 @@ (*** outer syntax *) +local + val type_insts = Parse.typ >> single || Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.typ --| Parse.$$$ ")") @@ -677,21 +683,23 @@ val rename = Parse.name -- (mapsto |-- Parse.name); val renames = Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.list1 rename --| Parse.$$$ "]")) []; +val parent = + ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames + >> (fn ((insts, name), renames) => (insts,name, renames)); -val parent = ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames - >> (fn ((insts,name),renames) => (insts,name,renames)) - +in val statespace_decl = - Parse.type_args -- Parse.name -- + Parse.type_args -- Parse.name -- (Parse.$$$ "=" |-- - ((Scan.repeat1 comp >> pair []) || - (plus1_unless comp parent -- - Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 comp)) []))) + ((Scan.repeat1 comp >> pair []) || + (plus1_unless comp parent -- + Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 comp)) []))); +val _ = + Outer_Syntax.command "statespace" "define state space" Keyword.thy_decl + (statespace_decl >> (fn ((args, name), (parents, comps)) => + Toplevel.theory (define_statespace args name parents comps))); -val statespace_command = - Outer_Syntax.command "statespace" "define state space" Keyword.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 +end; diff -r cc455b2897f8 -r ccec8b6d5d81 src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Sun Nov 06 14:23:04 2011 +0100 +++ b/src/Pure/Concurrent/task_queue.ML Sun Nov 06 18:42:17 2011 +0100 @@ -104,7 +104,9 @@ val timing_start = (Time.zeroTime, Time.zeroTime, []): timing; -fun new_timing () = Synchronized.var "timing" timing_start; +fun new_timing () = + if ! Multithreading.trace < 2 then NONE + else SOME (Synchronized.var "timing" timing_start); abstype task = Task of {group: group, @@ -118,7 +120,7 @@ Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE}; fun new_task group name pri = - Task {group = group, name = name, id = new_id (), pri = pri, timing = SOME (new_timing ())}; + Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing ()}; fun group_of_task (Task {group, ...}) = group; fun name_of_task (Task {name, ...}) = name;