--- 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
--- 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})
--- 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) \<Longrightarrow> all_distinct l"
+lemma all_distinct_left: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct l"
by simp
lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r"
by simp
-lemma distinct_left: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of l \<rbrakk> \<Longrightarrow> x\<noteq>y"
+lemma distinct_left: "all_distinct (Node l x False r) \<Longrightarrow> y \<in> set_of l \<Longrightarrow> x \<noteq> y"
by auto
-lemma distinct_right: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of r \<rbrakk> \<Longrightarrow> x\<noteq>y"
+lemma distinct_right: "all_distinct (Node l x False r) \<Longrightarrow> y \<in> set_of r \<Longrightarrow> x \<noteq> y"
by auto
-lemma distinct_left_right: "\<lbrakk>all_distinct (Node l z b r); x \<in> set_of l; y \<in> set_of r\<rbrakk>
- \<Longrightarrow> x\<noteq>y"
+lemma distinct_left_right:
+ "all_distinct (Node l z b r) \<Longrightarrow> x \<in> set_of l \<Longrightarrow> y \<in> set_of r \<Longrightarrow> x \<noteq> y"
by auto
lemma in_set_root: "x \<in> 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 \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
@@ -109,14 +108,14 @@
Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')
| None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))
| None \<Rightarrow>
- (case (delete x r) of
+ (case delete x r of
Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')
| None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)
else None))"
-lemma delete_Some_set_of: "\<And>t'. delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t"
-proof (induct t)
+lemma delete_Some_set_of: "delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> 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:
-"\<And>t'. \<lbrakk>delete x t = Some t'; all_distinct t\<rbrakk> \<Longrightarrow> all_distinct t'"
-proof (induct t)
+lemma delete_Some_all_distinct:
+ "delete x t = Some t' \<Longrightarrow> all_distinct t \<Longrightarrow> 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:
- "\<And>t'. delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> set_of t'"
-proof (induct t)
+ "delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> 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 \<Rightarrow> None)"
lemma subtract_Some_set_of_res:
- "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t \<subseteq> set_of t\<^isub>2"
-proof (induct t\<^isub>1)
+ "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t \<subseteq> 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:
- "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<subseteq> set_of t\<^isub>2"
-proof (induct t\<^isub>1)
+ "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<subseteq> 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:
- "\<And>t\<^isub>2 t. \<lbrakk>subtract t\<^isub>1 t\<^isub>2 = Some t; all_distinct t\<^isub>2\<rbrakk> \<Longrightarrow> all_distinct t"
-proof (induct t\<^isub>1)
+ "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> all_distinct t\<^isub>2 \<Longrightarrow> 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:
- "\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<inter> set_of t = {}"
-proof (induct t\<^isub>1)
+ "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<inter> 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:
- "\<And>t\<^isub>2 t. \<lbrakk>subtract t\<^isub>1 t\<^isub>2 = Some t; all_distinct t\<^isub>2\<rbrakk> \<Longrightarrow> all_distinct t\<^isub>1"
-proof (induct t\<^isub>1)
+ "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> all_distinct t\<^isub>2 \<Longrightarrow> 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)
--- 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:
-"(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id"
+lemma destr_contstr_comp_id: "(\<And>v. destr (constr v) = v) \<Longrightarrow> destr \<circ> constr = id"
by (rule ext) simp
@@ -67,16 +66,16 @@
lemma block_conj_cong: "(P \<and> Q) = (P \<and> Q)"
by simp
-lemma conj1_False: "(P\<equiv>False) \<Longrightarrow> (P \<and> Q) \<equiv> False"
+lemma conj1_False: "P \<equiv> False \<Longrightarrow> (P \<and> Q) \<equiv> False"
by simp
-lemma conj2_False: "\<lbrakk>Q\<equiv>False\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> False"
+lemma conj2_False: "Q \<equiv> False \<Longrightarrow> (P \<and> Q) \<equiv> False"
by simp
-lemma conj_True: "\<lbrakk>P\<equiv>True; Q\<equiv>True\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> True"
+lemma conj_True: "P \<equiv> True \<Longrightarrow> Q \<equiv> True \<Longrightarrow> (P \<and> Q) \<equiv> True"
by simp
-lemma conj_cong: "\<lbrakk>P\<equiv>P'; Q\<equiv>Q'\<rbrakk> \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> Q')"
+lemma conj_cong: "P \<equiv> P' \<Longrightarrow> Q \<equiv> Q' \<Longrightarrow> (P \<and> Q) \<equiv> (P' \<and> Q')"
by simp
--- 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 \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [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>\<cdot>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<B:=True>\<cdot>C = s\<cdot>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<a:=i>\<cdot>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
--- 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 \<Rightarrow> 'a"
and inject :: "'a \<Rightarrow> 'value"
assumes project_inject_cancel [statefun_simp]: "project (inject x) = x"
+begin
-lemma (in project_inject)
- ex_project [statefun_simp]: "\<exists>v. project v = x"
- apply (rule_tac x= "inject x" in exI)
- apply (simp add: project_inject_cancel)
- done
+lemma ex_project [statefun_simp]: "\<exists>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 \<circ> inject = id"
+lemma project_inject_comp_id [statefun_simp]: "project \<circ> inject = id"
by (rule ext) (simp add: project_inject_cancel)
-lemma (in project_inject)
- project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
+lemma project_inject_comp_cancel[statefun_simp]: "f \<circ> project \<circ> inject = f"
by (rule ext) (simp add: project_inject_cancel)
-
+end
end
\ No newline at end of file
--- 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
--- 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
--- 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;
--- 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;
--- 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;