--- a/NEWS Mon Jan 09 18:32:56 2012 +0100
+++ b/NEWS Mon Jan 09 18:33:55 2012 +0100
@@ -41,8 +41,8 @@
* Redundant attribute 'code_inline' has been discontinued. Use
'code_unfold' instead. INCOMPATIBILITY.
-* Dropped attribute 'code_unfold_post' in favor of the its dual 'code_abbrev',
-which yields a common pattern in definitions like
+* Dropped attribute 'code_unfold_post' in favor of the its dual
+'code_abbrev', which yields a common pattern in definitions like
definition [code_abbrev]: "f = t"
@@ -60,10 +60,68 @@
*** HOL ***
+* Type 'a set is now a proper type constructor (just as before
+Isabelle2008). Definitions mem_def and Collect_def have disappeared.
+Non-trivial INCOMPATIBILITY. For developments keeping predicates and
+sets separate, it is often sufficient to rephrase sets S accidentally
+used as predicates by "%x. x : S" and predicates P accidentally used
+as sets by "{x. P x}". Corresponding proofs in a first step should be
+pruned from any tinkering with former theorems mem_def and
+Collect_def. For developments which deliberately mixed predicates and
+sets, a planning step is necessary to determine what should become a
+predicate and what a set. It can be helpful to carry out that step in
+Isabelle2011-1 before jumping right into the current release.
+
+* Consolidated various theorem names relating to Finite_Set.fold
+combinator:
+
+ inf_INFI_fold_inf ~> inf_INF_fold_inf
+ sup_SUPR_fold_sup ~> sup_SUP_fold_sup
+ INFI_fold_inf ~> INF_fold_inf
+ SUPR_fold_sup ~> SUP_fold_sup
+ union_set ~> union_set_fold
+ minus_set ~> minus_set_fold
+
+INCOMPATIBILITY.
+
+* Consolidated theorem names concerning fold combinators:
+
+ INFI_set_fold ~> INF_set_fold
+ SUPR_set_fold ~> SUP_set_fold
+ INF_code ~> INF_set_foldr
+ SUP_code ~> SUP_set_foldr
+ foldr.simps ~> foldr_Nil foldr_Cons (in point-free formulation)
+ foldl.simps ~> foldl_Nil foldl_Cons
+ foldr_fold_rev ~> foldr_def
+ foldl_fold ~> foldl_def
+
+INCOMPATIBILITY.
+
+* Dropped rarely useful theorems concerning fold combinators:
+foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,
+rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,
+concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
+foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,
+listsum_conv_fold, listsum_foldl, sort_foldl_insort. INCOMPATIBILITY.
+Prefer "List.fold" with canonical argument order, or boil down
+"List.foldr" and "List.foldl" to "List.fold" by unfolding "foldr_def"
+and "foldl_def". For the common phrases "%xs. List.foldr plus xs 0"
+and "List.foldl plus 0", prefer "List.listsum".
+
+* Concrete syntax for case expressions includes constraints for source
+positions, and thus produces Prover IDE markup for its bindings.
+INCOMPATIBILITY for old-style syntax translations that augment the
+pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
+one_case.
+
+* Discontinued configuration option "syntax_positions": atomic terms
+in parse trees are always annotated by position constraints.
+
* Finite_Set.fold now qualified. INCOMPATIBILITY.
-* Renamed some facts on canonical fold on lists, in order to avoid problems
-with interpretation involving corresponding facts on foldl with the same base names:
+* Renamed some facts on canonical fold on lists, in order to avoid
+problems with interpretation involving corresponding facts on foldl
+with the same base names:
fold_set_remdups ~> fold_set_fold_remdups
fold_set ~> fold_set_fold
@@ -71,21 +129,17 @@
INCOMPATIBILITY.
-* 'set' is now a proper type constructor. Definitions mem_def and Collect_def
-have disappeared. INCOMPATIBILITY, rephrase sets S used as predicates by
-`%x. x : S` and predicates P used as sets by `{x. P x}`. For typical proofs,
-it is often sufficent to prune any tinkering with former theorems mem_def
-and Collect_def.
-
-* Theory HOL/Library/AList has been renamed to AList_Impl. INCOMPATIBILITY.
+* Theory HOL/Library/AList has been renamed to
+ AList_Impl. INCOMPATIBILITY.
* 'datatype' specifications allow explicit sort constraints.
-* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, use
-theory HOL/Library/Nat_Bijection instead.
-
-* Session HOL-Word: Discontinued many redundant theorems specific to type
-'a word. INCOMPATIBILITY, use the corresponding generic theorems instead.
+* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
+use theory HOL/Library/Nat_Bijection instead.
+
+* Session HOL-Word: Discontinued many redundant theorems specific to
+type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
+instead.
word_sub_alt ~> word_sub_wi
word_add_alt ~> word_add_def
--- a/doc-src/IsarImplementation/Thy/Isar.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy Mon Jan 09 18:33:55 2012 +0100
@@ -269,8 +269,8 @@
Example: @{method "induct"}, which is also a ``raw'' method since it
operates on the internal representation of simultaneous claims as
- Pure conjunction (\secref{{sec:logic-aux}}), instead of separate
- subgoals (\secref{sec::tactical-goals}).
+ Pure conjunction (\secref{sec:logic-aux}), instead of separate
+ subgoals (\secref{sec:tactical-goals}).
\item \emph{Structured method} with strong emphasis on facts outside
the goal state.
--- a/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Jan 09 18:32:56 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Jan 09 18:33:55 2012 +0100
@@ -379,8 +379,8 @@
Example: \hyperlink{method.induct}{\mbox{\isa{induct}}}, which is also a ``raw'' method since it
operates on the internal representation of simultaneous claims as
- Pure conjunction (\secref{{sec:logic-aux}}), instead of separate
- subgoals (\secref{sec::tactical-goals}).
+ Pure conjunction (\secref{sec:logic-aux}), instead of separate
+ subgoals (\secref{sec:tactical-goals}).
\item \emph{Structured method} with strong emphasis on facts outside
the goal state.
--- a/doc-src/Main/Docs/Main_Doc.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/doc-src/Main/Docs/Main_Doc.thy Mon Jan 09 18:33:55 2012 +0100
@@ -495,8 +495,9 @@
@{const List.drop} & @{typeof List.drop}\\
@{const List.dropWhile} & @{typeof List.dropWhile}\\
@{const List.filter} & @{typeof List.filter}\\
+@{const List.fold} & @{typeof List.fold}\\
+@{const List.foldr} & @{typeof List.foldr}\\
@{const List.foldl} & @{typeof List.foldl}\\
-@{const List.foldr} & @{typeof List.foldr}\\
@{const List.hd} & @{typeof List.hd}\\
@{const List.last} & @{typeof List.last}\\
@{const List.length} & @{typeof List.length}\\
--- a/doc-src/Main/Docs/document/Main_Doc.tex Mon Jan 09 18:32:56 2012 +0100
+++ b/doc-src/Main/Docs/document/Main_Doc.tex Mon Jan 09 18:33:55 2012 +0100
@@ -502,8 +502,9 @@
\isa{drop} & \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
\isa{dropWhile} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
\isa{filter} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}\\
+\isa{fold} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\
+\isa{foldr} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\
\isa{foldl} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
-\isa{foldr} & \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b}\\
\isa{hd} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
\isa{last} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
\isa{length} & \isa{{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat}\\
--- a/src/HOL/Algebra/Divisibility.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Mon Jan 09 18:33:55 2012 +0100
@@ -1283,9 +1283,10 @@
assumes anunit: "a \<notin> Units G"
and fs: "factors G as a"
shows "length as > 0"
-apply (insert fs, elim factorsE)
-apply (metis Units_one_closed assms(1) foldr.simps(1) length_greater_0_conv)
-done
+proof -
+ from anunit Units_one_closed have "a \<noteq> \<one>" by auto
+ with fs show ?thesis by (auto elim: factorsE)
+qed
lemma (in monoid) unit_wfactors [simp]:
assumes aunit: "a \<in> Units G"
@@ -3307,182 +3308,192 @@
lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:
"\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>
wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
-apply (induct as)
-apply (metis Units_one_closed essentially_equal_def foldr.simps(1) is_monoid_cancel listassoc_refl monoid_cancel.assoc_unit_r perm_refl unit_wfactors_empty wfactorsE)
-apply clarsimp
-proof -
- fix a as ah as'
- assume ih[rule_format]:
- "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and>
- wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
- and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"
- and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"
- and afs: "wfactors G (ah # as) a"
- and afs': "wfactors G as' a"
- hence ahdvda: "ah divides a"
+proof (induct as)
+ case Nil show ?case apply auto
+ proof -
+ fix a as'
+ assume a: "a \<in> carrier G"
+ assume "wfactors G [] a"
+ then obtain "\<one> \<sim> a" by (auto elim: wfactorsE)
+ with a have "a \<in> Units G" by (auto intro: assoc_unit_r)
+ moreover assume "wfactors G as' a"
+ moreover assume "set as' \<subseteq> carrier G"
+ ultimately have "as' = []" by (rule unit_wfactors_empty)
+ then show "essentially_equal G [] as'" by simp
+ qed
+next
+ case (Cons ah as) then show ?case apply clarsimp
+ proof -
+ fix a as'
+ assume ih [rule_format]:
+ "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>
+ wfactors G as' a \<longrightarrow> essentially_equal G as as'"
+ and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"
+ and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"
+ and afs: "wfactors G (ah # as) a"
+ and afs': "wfactors G as' a"
+ hence ahdvda: "ah divides a"
by (intro wfactors_dividesI[of "ah#as" "a"], simp+)
- hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE)
- from this obtain a'
+ hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE)
+ from this obtain a'
where a'carr: "a' \<in> carrier G"
and a: "a = ah \<otimes> a'"
by auto
- have a'fs: "wfactors G as a'"
- apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
- apply (simp add: a, insert ascarr a'carr)
- apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)
- done
-
- from afs have ahirr: "irreducible G ah" by (elim wfactorsE, simp)
- with ascarr have ahprime: "prime G ah" by (intro irreducible_prime ahcarr)
-
- note carr [simp] = acarr ahcarr ascarr as'carr a'carr
-
- note ahdvda
- also from afs'
- have "a divides (foldr (op \<otimes>) as' \<one>)"
- by (elim wfactorsE associatedE, simp)
- finally have "ah divides (foldr (op \<otimes>) as' \<one>)" by simp
-
- with ahprime
+ have a'fs: "wfactors G as a'"
+ apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
+ apply (simp add: a, insert ascarr a'carr)
+ apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)
+ done
+ from afs have ahirr: "irreducible G ah" by (elim wfactorsE, simp)
+ with ascarr have ahprime: "prime G ah" by (intro irreducible_prime ahcarr)
+
+ note carr [simp] = acarr ahcarr ascarr as'carr a'carr
+
+ note ahdvda
+ also from afs'
+ have "a divides (foldr (op \<otimes>) as' \<one>)"
+ by (elim wfactorsE associatedE, simp)
+ finally have "ah divides (foldr (op \<otimes>) as' \<one>)" by simp
+
+ with ahprime
have "\<exists>i<length as'. ah divides as'!i"
by (intro multlist_prime_pos, simp+)
- from this obtain i
+ from this obtain i
where len: "i<length as'" and ahdvd: "ah divides as'!i"
by auto
- from afs' carr have irrasi: "irreducible G (as'!i)"
+ from afs' carr have irrasi: "irreducible G (as'!i)"
by (fast intro: nth_mem[OF len] elim: wfactorsE)
- from len carr
+ from len carr
have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force)
- note carr = carr asicarr
-
- from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE)
- from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto
-
- with carr irrasi[simplified asi]
+ note carr = carr asicarr
+
+ from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE)
+ from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto
+
+ with carr irrasi[simplified asi]
have asiah: "as'!i \<sim> ah" apply -
- apply (elim irreducible_prodE[of "ah" "x"], assumption+)
- apply (rule associatedI2[of x], assumption+)
- apply (rule irreducibleE[OF ahirr], simp)
- done
-
- note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
- note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
- note carr = carr partscarr
-
- have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
- apply (intro wfactors_prod_exists)
- using setparts afs' by (fast elim: wfactorsE, simp)
- from this obtain aa_1
- where aa1carr: "aa_1 \<in> carrier G"
- and aa1fs: "wfactors G (take i as') aa_1"
- by auto
-
- have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
- apply (intro wfactors_prod_exists)
- using setparts afs' by (fast elim: wfactorsE, simp)
- from this obtain aa_2
- where aa2carr: "aa_2 \<in> carrier G"
- and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
- by auto
-
- note carr = carr aa1carr[simp] aa2carr[simp]
-
- from aa1fs aa2fs
+ apply (elim irreducible_prodE[of "ah" "x"], assumption+)
+ apply (rule associatedI2[of x], assumption+)
+ apply (rule irreducibleE[OF ahirr], simp)
+ done
+
+ note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
+ note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
+ note carr = carr partscarr
+
+ have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
+ apply (intro wfactors_prod_exists)
+ using setparts afs' by (fast elim: wfactorsE, simp)
+ from this obtain aa_1
+ where aa1carr: "aa_1 \<in> carrier G"
+ and aa1fs: "wfactors G (take i as') aa_1"
+ by auto
+
+ have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
+ apply (intro wfactors_prod_exists)
+ using setparts afs' by (fast elim: wfactorsE, simp)
+ from this obtain aa_2
+ where aa2carr: "aa_2 \<in> carrier G"
+ and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
+ by auto
+
+ note carr = carr aa1carr[simp] aa2carr[simp]
+
+ from aa1fs aa2fs
have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
by (intro wfactors_mult, simp+)
- hence v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
+ hence v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
apply (intro wfactors_mult_single)
using setparts afs'
by (fast intro: nth_mem[OF len] elim: wfactorsE, simp+)
- from aa2carr carr aa1fs aa2fs
+ from aa2carr carr aa1fs aa2fs
have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
- apply (intro wfactors_mult_single)
- apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len])
- apply (fast intro: nth_mem[OF len])
- apply fast
- apply fast
- apply assumption
- done
- with len carr aa1carr aa2carr aa1fs
+ apply (intro wfactors_mult_single)
+ apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len])
+ apply (fast intro: nth_mem[OF len])
+ apply fast
+ apply fast
+ apply assumption
+ done
+ with len carr aa1carr aa2carr aa1fs
have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
- apply (intro wfactors_mult)
- apply fast
- apply (simp, (fast intro: nth_mem[OF len])?)+
- done
-
- from len
+ apply (intro wfactors_mult)
+ apply fast
+ apply (simp, (fast intro: nth_mem[OF len])?)+
+ done
+
+ from len
have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
by (simp add: drop_Suc_conv_tl)
- with carr
+ with carr
have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
by simp
- with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
+ with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
- apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'" "as'"])
- apply fast+
- apply (simp, fast)
- done
- then
- have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
- apply (simp add: m_assoc[symmetric])
- apply (simp add: m_comm)
- done
- from carr asiah
- have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
+ apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'" "as'"])
+ apply fast+
+ apply (simp, fast)
+ done
+ then
+ have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
+ apply (simp add: m_assoc[symmetric])
+ apply (simp add: m_comm)
+ done
+ from carr asiah
+ have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
apply (intro mult_cong_l)
apply (fast intro: associated_sym, simp+)
- done
- also note t1
- finally
+ done
+ also note t1
+ finally
have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
- with carr aa1carr aa2carr a'carr nth_mem[OF len]
+ with carr aa1carr aa2carr a'carr nth_mem[OF len]
have a': "aa_1 \<otimes> aa_2 \<sim> a'"
by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])
- note v1
- also note a'
- finally have "wfactors G (take i as' @ drop (Suc i) as') a'" by simp
-
- from a'fs this carr
+ note v1
+ also note a'
+ finally have "wfactors G (take i as' @ drop (Suc i) as') a'" by simp
+
+ from a'fs this carr
have "essentially_equal G as (take i as' @ drop (Suc i) as')"
by (intro ih[of a']) simp
- hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
- apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI)
- done
-
- from carr
- have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
- (as' ! i # take i as' @ drop (Suc i) as')"
- proof (intro essentially_equalI)
- show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
+ hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
+ apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI)
+ done
+
+ from carr
+ have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
+ (as' ! i # take i as' @ drop (Suc i) as')"
+ proof (intro essentially_equalI)
+ show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
by simp
- next show "ah # take i as' @ drop (Suc i) as' [\<sim>]
- as' ! i # take i as' @ drop (Suc i) as'"
- apply (simp add: list_all2_append)
- apply (simp add: asiah[symmetric] ahcarr asicarr)
+ next
+ show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
+ apply (simp add: list_all2_append)
+ apply (simp add: asiah[symmetric] ahcarr asicarr)
+ done
+ qed
+
+ note ee1
+ also note ee2
+ also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
+ (take i as' @ as' ! i # drop (Suc i) as')"
+ apply (intro essentially_equalI)
+ apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
+ take i as' @ as' ! i # drop (Suc i) as'")
+ apply simp
+ apply (rule perm_append_Cons)
+ apply simp
done
+ finally
+ have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" by simp
+ then show "essentially_equal G (ah # as) as'" by (subst as', assumption)
qed
-
- note ee1
- also note ee2
- also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
- (take i as' @ as' ! i # drop (Suc i) as')"
- apply (intro essentially_equalI)
- apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
- take i as' @ as' ! i # drop (Suc i) as'")
-apply simp
- apply (rule perm_append_Cons)
- apply simp
- done
- finally
- have "essentially_equal G (ah # as)
- (take i as' @ as' ! i # drop (Suc i) as')" by simp
-
- thus "essentially_equal G (ah # as) as'" by (subst as', assumption)
qed
lemma (in primeness_condition_monoid) wfactors_unique:
--- a/src/HOL/Complete_Lattices.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy Mon Jan 09 18:33:55 2012 +0100
@@ -542,10 +542,10 @@
begin
definition
- [simp]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
+ [simp, code]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
definition
- [simp]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
+ [simp, code]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
instance proof
qed (auto intro: bool_induct)
@@ -579,14 +579,14 @@
definition
"\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
-lemma Inf_apply:
+lemma Inf_apply [code]:
"(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
by (simp add: Inf_fun_def)
definition
"\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
-lemma Sup_apply:
+lemma Sup_apply [code]:
"(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
by (simp add: Sup_fun_def)
--- a/src/HOL/Decision_Procs/MIR.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Mon Jan 09 18:33:55 2012 +0100
@@ -3324,7 +3324,7 @@
in map (\<lambda> ((p,n,t),(q,m,s)). (And p q, n+m, Add t s)) [(a,b). a\<leftarrow>acs,b\<leftarrow>bcs])"
| "rsplit0 (Sub a b) = rsplit0 (Add a (Neg b))"
| "rsplit0 (Neg a) = map (\<lambda> (p,n,s). (p,-n,Neg s)) (rsplit0 a)"
-| "rsplit0 (Floor a) = foldl (op @) [] (map
+| "rsplit0 (Floor a) = concat (map
(\<lambda> (p,n,s). if n=0 then [(p,0,Floor s)]
else (map (\<lambda> j. (fp p n s j, 0, Add (Floor s) (C j))) (if n > 0 then [0 .. n] else [n .. 0])))
(rsplit0 a))"
@@ -3377,7 +3377,7 @@
by (auto simp add: split_def)
qed
have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
- by (auto simp add: foldl_conv_concat)
+ by auto
also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
also have "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
@@ -3534,7 +3534,7 @@
by (auto simp add: split_def)
qed
- have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by (auto simp add: foldl_conv_concat)
+ have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by auto
also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
also have "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
--- a/src/HOL/Finite_Set.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Finite_Set.thy Mon Jan 09 18:33:55 2012 +0100
@@ -718,7 +718,7 @@
qed auto
lemma comp_fun_idem_remove:
- "comp_fun_idem (\<lambda>x A. A - {x})"
+ "comp_fun_idem Set.remove"
proof
qed auto
@@ -742,10 +742,11 @@
lemma minus_fold_remove:
assumes "finite A"
- shows "B - A = fold (\<lambda>x A. A - {x}) B A"
+ shows "B - A = fold Set.remove B A"
proof -
- interpret comp_fun_idem "\<lambda>x A. A - {x}" by (fact comp_fun_idem_remove)
- from `finite A` show ?thesis by (induct A arbitrary: B) auto
+ interpret comp_fun_idem Set.remove by (fact comp_fun_idem_remove)
+ from `finite A` have "fold Set.remove B A = B - A" by (induct A arbitrary: B) auto
+ then show ?thesis ..
qed
context complete_lattice
@@ -779,7 +780,7 @@
shows "Sup A = fold sup bot A"
using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
-lemma inf_INFI_fold_inf:
+lemma inf_INF_fold_inf:
assumes "finite A"
shows "inf B (INFI A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold")
proof (rule sym)
@@ -790,7 +791,7 @@
(simp_all add: INF_def inf_left_commute)
qed
-lemma sup_SUPR_fold_sup:
+lemma sup_SUP_fold_sup:
assumes "finite A"
shows "sup B (SUPR A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold")
proof (rule sym)
@@ -801,15 +802,15 @@
(simp_all add: SUP_def sup_left_commute)
qed
-lemma INFI_fold_inf:
+lemma INF_fold_inf:
assumes "finite A"
shows "INFI A f = fold (inf \<circ> f) top A"
- using assms inf_INFI_fold_inf [of A top] by simp
+ using assms inf_INF_fold_inf [of A top] by simp
-lemma SUPR_fold_sup:
+lemma SUP_fold_sup:
assumes "finite A"
shows "SUPR A f = fold (sup \<circ> f) bot A"
- using assms sup_SUPR_fold_sup [of A bot] by simp
+ using assms sup_SUP_fold_sup [of A bot] by simp
end
@@ -2066,10 +2067,10 @@
assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
shows "finite (UNIV :: 'b set)"
proof -
- from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
- by(rule finite_imageI)
- moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
- by(rule UNIV_eq_I) auto
+ from fin have "\<And>arbitrary. finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
+ by (rule finite_imageI)
+ moreover have "\<And>arbitrary. UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
+ by (rule UNIV_eq_I) auto
ultimately show "finite (UNIV :: 'b set)" by simp
qed
--- a/src/HOL/HOL.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/HOL.thy Mon Jan 09 18:33:55 2012 +0100
@@ -104,34 +104,31 @@
notation (xsymbols)
iff (infixr "\<longleftrightarrow>" 25)
-nonterminal letbinds and letbind
-nonterminal case_pat and case_syn and cases_syn
+syntax
+ "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10)
+translations
+ "THE x. P" == "CONST The (%x. P)"
+print_translation {*
+ [(@{const_syntax The}, fn [Abs abs] =>
+ let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
+ in Syntax.const @{syntax_const "_The"} $ x $ t end)]
+*} -- {* To avoid eta-contraction of body *}
+nonterminal letbinds and letbind
syntax
- "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10)
-
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10)
"" :: "letbind => letbinds" ("_")
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" [0, 10] 10)
- "_case_syntax" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
- "_case1" :: "[case_pat, 'b] => case_syn" ("(2_ =>/ _)" 10)
- "" :: "case_syn => cases_syn" ("_")
- "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
- "_strip_positions" :: "'a => case_pat" ("_")
-
+nonterminal case_syn and cases_syn
+syntax
+ "_case_syntax" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
+ "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10)
+ "" :: "case_syn => cases_syn" ("_")
+ "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
syntax (xsymbols)
- "_case1" :: "[case_pat, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10)
-
-translations
- "THE x. P" == "CONST The (%x. P)"
-
-print_translation {*
- [(@{const_syntax The}, fn [Abs abs] =>
- let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
- in Syntax.const @{syntax_const "_The"} $ x $ t end)]
-*} -- {* To avoid eta-contraction of body *}
+ "_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10)
notation (xsymbols)
All (binder "\<forall>" 10) and
@@ -2011,37 +2008,6 @@
fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
end;
-val case_split = @{thm case_split};
-val cong = @{thm cong};
-val de_Morgan_conj = @{thm de_Morgan_conj};
-val de_Morgan_disj = @{thm de_Morgan_disj};
-val disj_assoc = @{thm disj_assoc};
-val disj_comms = @{thms disj_comms};
-val disj_cong = @{thm disj_cong};
-val eq_ac = @{thms eq_ac};
-val eq_cong2 = @{thm eq_cong2}
-val Eq_FalseI = @{thm Eq_FalseI};
-val Eq_TrueI = @{thm Eq_TrueI};
-val Ex1_def = @{thm Ex1_def};
-val ex_disj_distrib = @{thm ex_disj_distrib};
-val ex_simps = @{thms ex_simps};
-val if_cancel = @{thm if_cancel};
-val if_eq_cancel = @{thm if_eq_cancel};
-val if_False = @{thm if_False};
-val iff_conv_conj_imp = @{thm iff_conv_conj_imp};
-val iff = @{thm iff};
-val if_splits = @{thms if_splits};
-val if_True = @{thm if_True};
-val if_weak_cong = @{thm if_weak_cong};
-val imp_all = @{thm imp_all};
-val imp_cong = @{thm imp_cong};
-val imp_conjL = @{thm imp_conjL};
-val imp_conjR = @{thm imp_conjR};
-val imp_conv_disj = @{thm imp_conv_disj};
-val split_if = @{thm split_if};
-val the1_equality = @{thm the1_equality};
-val theI = @{thm theI};
-val theI' = @{thm theI'};
val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps});
*}
--- a/src/HOL/HOLCF/One.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/HOLCF/One.thy Mon Jan 09 18:33:55 2012 +0100
@@ -58,6 +58,7 @@
translations
"case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x"
+ "case x of XCONST ONE :: 'a \<Rightarrow> t" => "CONST one_case\<cdot>t\<cdot>x"
"\<Lambda> (XCONST ONE). t" == "CONST one_case\<cdot>t"
lemma one_case1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
--- a/src/HOL/HOLCF/Ssum.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/HOLCF/Ssum.thy Mon Jan 09 18:33:55 2012 +0100
@@ -168,6 +168,7 @@
translations
"case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
+ "case s of (XCONST sinl :: 'a)\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" => "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
translations
"\<Lambda>(XCONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Mon Jan 09 18:33:55 2012 +0100
@@ -452,27 +452,35 @@
val cabs = app "_cabs"
val capp = app @{const_syntax Rep_cfun}
val capps = Library.foldl capp
- fun con1 authentic n (con,args) =
+ fun con1 authentic n (con, args) =
Library.foldl capp (c_ast authentic con, argvars n args)
- fun case1 authentic (n, c) =
- app "_case1" (Ast.strip_positions (con1 authentic n c), expvar n)
+ fun con1_constraint authentic n (con, args) =
+ Library.foldl capp
+ (Ast.Appl
+ [Ast.Constant @{syntax_const "_constrain"}, c_ast authentic con,
+ Ast.Variable ("'a" ^ string_of_int n)],
+ argvars n args)
+ fun case1 constraint authentic (n, c) =
+ app @{syntax_const "_case1"}
+ ((if constraint then con1_constraint else con1) authentic n c, expvar n)
fun arg1 (n, (_, args)) = List.foldr cabs (expvar n) (argvars n args)
fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
val case_constant = Ast.Constant (syntax (case_const dummyT))
- fun case_trans authentic =
- (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
+ fun case_trans constraint authentic =
(app "_case_syntax"
(Ast.Variable "x",
- foldr1 (app "_case2") (map_index (case1 authentic) spec)),
+ foldr1 (app @{syntax_const "_case2"}) (map_index (case1 constraint authentic) spec)),
capp (capps (case_constant, map_index arg1 spec), Ast.Variable "x"))
fun one_abscon_trans authentic (n, c) =
- (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
- (cabs (con1 authentic n c, expvar n),
- capps (case_constant, map_index (when1 n) spec))
+ (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
+ (cabs (con1 authentic n c, expvar n),
+ capps (case_constant, map_index (when1 n) spec))
fun abscon_trans authentic =
map_index (one_abscon_trans authentic) spec
val trans_rules : Ast.ast Syntax.trrule list =
- case_trans false :: case_trans true ::
+ Syntax.Parse_Print_Rule (case_trans false true) ::
+ Syntax.Parse_Rule (case_trans false false) ::
+ Syntax.Parse_Rule (case_trans true false) ::
abscon_trans false @ abscon_trans true
in
val thy = Sign.add_trrules trans_rules thy
--- a/src/HOL/HOLCF/Tools/cont_proc.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML Mon Jan 09 18:33:55 2012 +0100
@@ -121,7 +121,7 @@
local
fun solve_cont thy _ t =
let
- val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI
+ val tr = instantiate' [] [SOME (cterm_of thy t)] @{thm Eq_TrueI}
in Option.map fst (Seq.pull (cont_tac 1 tr)) end
in
fun cont_proc thy =
--- a/src/HOL/HOLCF/Up.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/HOLCF/Up.thy Mon Jan 09 18:33:55 2012 +0100
@@ -181,6 +181,7 @@
translations
"case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
+ "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
"\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
text {* continuous versions of lemmas for @{typ "('a)u"} *}
--- a/src/HOL/IMP/ACom.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/IMP/ACom.thy Mon Jan 09 18:33:55 2012 +0100
@@ -84,6 +84,14 @@
lemma strip_anno[simp]: "strip (anno a c) = c"
by(induct c) simp_all
+lemma strip_eq_SKIP:
+ "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})"
+by (cases c) simp_all
+
+lemma strip_eq_Assign:
+ "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})"
+by (cases c) simp_all
+
lemma strip_eq_Semi:
"strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
by (cases c) simp_all
--- a/src/HOL/IMP/Abs_Int0.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Mon Jan 09 18:33:55 2012 +0100
@@ -124,11 +124,268 @@
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
by(auto simp add: le_st_def lookup_def update_def)
-lemma step'_mono: "S \<sqsubseteq> S' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c"
-apply(induction c arbitrary: S S')
-apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split)
+lemma mono_step': "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'"
+apply(induction c c' arbitrary: S S' rule: le_acom.induct)
+apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj
+ split: option.split)
done
end
+
+subsubsection "Ascending Chain Condition"
+
+hide_const acc
+
+abbreviation "strict r == r \<inter> -(r^-1)"
+abbreviation "acc r == wf((strict r)^-1)"
+
+lemma strict_inv_image: "strict(inv_image r f) = inv_image (strict r) f"
+by(auto simp: inv_image_def)
+
+lemma acc_inv_image:
+ "acc r \<Longrightarrow> acc (inv_image r f)"
+by (metis converse_inv_image strict_inv_image wf_inv_image)
+
+text{* ACC for option type: *}
+
+lemma acc_option: assumes "acc {(x,y::'a::preord). x \<sqsubseteq> y}"
+shows "acc {(x,y::'a option). x \<sqsubseteq> y}"
+proof(auto simp: wf_eq_minimal)
+ fix xo :: "'a option" and Qo assume "xo : Qo"
+ let ?Q = "{x. Some x \<in> Qo}"
+ show "\<exists>yo\<in>Qo. \<forall>zo. yo \<sqsubseteq> zo \<and> ~ zo \<sqsubseteq> yo \<longrightarrow> zo \<notin> Qo" (is "\<exists>zo\<in>Qo. ?P zo")
+ proof cases
+ assume "?Q = {}"
+ hence "?P None" by auto
+ moreover have "None \<in> Qo" using `?Q = {}` `xo : Qo`
+ by auto (metis not_Some_eq)
+ ultimately show ?thesis by blast
+ next
+ assume "?Q \<noteq> {}"
+ with assms show ?thesis
+ apply(auto simp: wf_eq_minimal)
+ apply(erule_tac x="?Q" in allE)
+ apply auto
+ apply(rule_tac x = "Some z" in bexI)
+ by auto
+ qed
+qed
+
+text{* ACC for abstract states, via measure functions. *}
+
+(*FIXME mv*)
+lemma setsum_strict_mono1:
+fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
+assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
+shows "setsum f A < setsum g A"
+proof-
+ from assms(3) obtain a where a: "a:A" "f a < g a" by blast
+ have "setsum f A = setsum f ((A-{a}) \<union> {a})"
+ by(simp add:insert_absorb[OF `a:A`])
+ also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
+ using `finite A` by(subst setsum_Un_disjoint) auto
+ also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
+ by(rule setsum_mono)(simp add: assms(2))
+ also have "setsum f {a} < setsum g {a}" using a by simp
+ also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
+ using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
+ also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
+ finally show ?thesis by (metis add_right_mono add_strict_left_mono)
+qed
+
+lemma measure_st: assumes "(strict{(x,y::'a::SL_top). x \<sqsubseteq> y})^-1 <= measure m"
+and "\<forall>x y::'a. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m x = m y"
+shows "(strict{(S,S'::'a st). S \<sqsubseteq> S'})^-1 \<subseteq>
+ measure(%fd. \<Sum>x| x\<in>set(dom fd) \<and> ~ \<top> \<sqsubseteq> fun fd x. m(fun fd x)+1)"
+proof-
+ { fix S S' :: "'a st" assume "S \<sqsubseteq> S'" "~ S' \<sqsubseteq> S"
+ let ?X = "set(dom S)" let ?Y = "set(dom S')"
+ let ?f = "fun S" let ?g = "fun S'"
+ let ?X' = "{x:?X. ~ \<top> \<sqsubseteq> ?f x}" let ?Y' = "{y:?Y. ~ \<top> \<sqsubseteq> ?g y}"
+ from `S \<sqsubseteq> S'` have "ALL y:?Y'\<inter>?X. ?f y \<sqsubseteq> ?g y"
+ by(auto simp: le_st_def lookup_def)
+ hence 1: "ALL y:?Y'\<inter>?X. m(?g y)+1 \<le> m(?f y)+1"
+ using assms(1,2) by(fastforce)
+ from `~ S' \<sqsubseteq> S` obtain u where u: "u : ?X" "~ lookup S' u \<sqsubseteq> ?f u"
+ by(auto simp: le_st_def)
+ hence "u : ?X'" by simp (metis preord_class.le_trans top)
+ have "?Y'-?X = {}" using `S \<sqsubseteq> S'` by(fastforce simp: le_st_def lookup_def)
+ have "?Y'\<inter>?X <= ?X'" apply auto
+ apply (metis `S \<sqsubseteq> S'` le_st_def lookup_def preord_class.le_trans)
+ done
+ have "(\<Sum>y\<in>?Y'. m(?g y)+1) = (\<Sum>y\<in>(?Y'-?X) \<union> (?Y'\<inter>?X). m(?g y)+1)"
+ by (metis Un_Diff_Int)
+ also have "\<dots> = (\<Sum>y\<in>?Y'\<inter>?X. m(?g y)+1)"
+ using `?Y'-?X = {}` by (metis Un_empty_left)
+ also have "\<dots> < (\<Sum>x\<in>?X'. m(?f x)+1)"
+ proof cases
+ assume "u \<in> ?Y'"
+ hence "m(?g u) < m(?f u)" using assms(1) `S \<sqsubseteq> S'` u
+ by (fastforce simp: le_st_def lookup_def)
+ have "(\<Sum>y\<in>?Y'\<inter>?X. m(?g y)+1) < (\<Sum>y\<in>?Y'\<inter>?X. m(?f y)+1)"
+ using `u:?X` `u:?Y'` `m(?g u) < m(?f u)`
+ by(fastforce intro!: setsum_strict_mono1[OF _ 1])
+ also have "\<dots> \<le> (\<Sum>y\<in>?X'. m(?f y)+1)"
+ by(simp add: setsum_mono3[OF _ `?Y'\<inter>?X <= ?X'`])
+ finally show ?thesis .
+ next
+ assume "u \<notin> ?Y'"
+ with `?Y'\<inter>?X <= ?X'` have "?Y'\<inter>?X - {u} <= ?X' - {u}" by blast
+ have "(\<Sum>y\<in>?Y'\<inter>?X. m(?g y)+1) = (\<Sum>y\<in>?Y'\<inter>?X - {u}. m(?g y)+1)"
+ proof-
+ have "?Y'\<inter>?X = ?Y'\<inter>?X - {u}" using `u \<notin> ?Y'` by auto
+ thus ?thesis by metis
+ qed
+ also have "\<dots> < (\<Sum>y\<in>?Y'\<inter>?X-{u}. m(?g y)+1) + (\<Sum>y\<in>{u}. m(?f y)+1)" by simp
+ also have "(\<Sum>y\<in>?Y'\<inter>?X-{u}. m(?g y)+1) \<le> (\<Sum>y\<in>?Y'\<inter>?X-{u}. m(?f y)+1)"
+ using 1 by(blast intro: setsum_mono)
+ also have "\<dots> \<le> (\<Sum>y\<in>?X'-{u}. m(?f y)+1)"
+ by(simp add: setsum_mono3[OF _ `?Y'\<inter>?X-{u} <= ?X'-{u}`])
+ also have "\<dots> + (\<Sum>y\<in>{u}. m(?f y)+1)= (\<Sum>y\<in>(?X'-{u}) \<union> {u}. m(?f y)+1)"
+ using `u:?X'` by(subst setsum_Un_disjoint[symmetric]) auto
+ also have "\<dots> = (\<Sum>x\<in>?X'. m(?f x)+1)"
+ using `u : ?X'` by(simp add:insert_absorb)
+ finally show ?thesis by (blast intro: add_right_mono)
+ qed
+ finally have "(\<Sum>y\<in>?Y'. m(?g y)+1) < (\<Sum>x\<in>?X'. m(?f x)+1)" .
+ } thus ?thesis by(auto simp add: measure_def inv_image_def)
+qed
+
+text{* ACC for acom. First the ordering on acom is related to an ordering on
+lists of annotations. *}
+
+(* FIXME mv and add [simp] *)
+lemma listrel_Cons_iff:
+ "(x#xs, y#ys) : listrel r \<longleftrightarrow> (x,y) \<in> r \<and> (xs,ys) \<in> listrel r"
+by (blast intro:listrel.Cons)
+
+lemma listrel_app: "(xs1,ys1) : listrel r \<Longrightarrow> (xs2,ys2) : listrel r
+ \<Longrightarrow> (xs1@xs2, ys1@ys2) : listrel r"
+by(auto simp add: listrel_iff_zip)
+
+lemma listrel_app_same_size: "size xs1 = size ys1 \<Longrightarrow> size xs2 = size ys2 \<Longrightarrow>
+ (xs1@xs2, ys1@ys2) : listrel r \<longleftrightarrow>
+ (xs1,ys1) : listrel r \<and> (xs2,ys2) : listrel r"
+by(auto simp add: listrel_iff_zip)
+
+lemma listrel_converse: "listrel(r^-1) = (listrel r)^-1"
+proof-
+ { fix xs ys
+ have "(xs,ys) : listrel(r^-1) \<longleftrightarrow> (ys,xs) : listrel r"
+ apply(induct xs arbitrary: ys)
+ apply (fastforce simp: listrel.Nil)
+ apply (fastforce simp: listrel_Cons_iff)
+ done
+ } thus ?thesis by auto
+qed
+
+(* It would be nice to get rid of refl & trans and build them into the proof *)
+lemma acc_listrel: fixes r :: "('a*'a)set" assumes "refl r" and "trans r"
+and "acc r" shows "acc (listrel r - {([],[])})"
+proof-
+ have refl: "!!x. (x,x) : r" using `refl r` unfolding refl_on_def by blast
+ have trans: "!!x y z. (x,y) : r \<Longrightarrow> (y,z) : r \<Longrightarrow> (x,z) : r"
+ using `trans r` unfolding trans_def by blast
+ from assms(3) obtain mx :: "'a set \<Rightarrow> 'a" where
+ mx: "!!S x. x:S \<Longrightarrow> mx S : S \<and> (\<forall>y. (mx S,y) : strict r \<longrightarrow> y \<notin> S)"
+ by(simp add: wf_eq_minimal) metis
+ let ?R = "listrel r - {([], [])}"
+ { fix Q and xs :: "'a list"
+ have "xs \<in> Q \<Longrightarrow> \<exists>ys. ys\<in>Q \<and> (\<forall>zs. (ys, zs) \<in> strict ?R \<longrightarrow> zs \<notin> Q)"
+ (is "_ \<Longrightarrow> \<exists>ys. ?P Q ys")
+ proof(induction xs arbitrary: Q rule: length_induct)
+ case (1 xs)
+ { have "!!ys Q. size ys < size xs \<Longrightarrow> ys : Q \<Longrightarrow> EX ms. ?P Q ms"
+ using "1.IH" by blast
+ } note IH = this
+ show ?case
+ proof(cases xs)
+ case Nil with `xs : Q` have "?P Q []" by auto
+ thus ?thesis by blast
+ next
+ case (Cons x ys)
+ let ?Q1 = "{a. \<exists>bs. size bs = size ys \<and> a#bs : Q}"
+ have "x : ?Q1" using `xs : Q` Cons by auto
+ from mx[OF this] obtain m1 where
+ 1: "m1 \<in> ?Q1 \<and> (\<forall>y. (m1,y) \<in> strict r \<longrightarrow> y \<notin> ?Q1)" by blast
+ then obtain ms1 where "size ms1 = size ys" "m1#ms1 : Q" by blast+
+ hence "size ms1 < size xs" using Cons by auto
+ let ?Q2 = "{bs. \<exists>m1'. (m1',m1):r \<and> (m1,m1'):r \<and> m1'#bs : Q \<and> size bs = size ms1}"
+ have "ms1 : ?Q2" using `m1#ms1 : Q` by(blast intro: refl)
+ from IH[OF `size ms1 < size xs` this]
+ obtain ms where 2: "?P ?Q2 ms" by auto
+ then obtain m1' where m1': "(m1',m1) : r \<and> (m1,m1') : r \<and> m1'#ms : Q"
+ by blast
+ hence "\<forall>ab. (m1'#ms,ab) : strict ?R \<longrightarrow> ab \<notin> Q" using 1 2
+ apply (auto simp: listrel_Cons_iff)
+ apply (metis `length ms1 = length ys` listrel_eq_len trans)
+ by (metis `length ms1 = length ys` listrel_eq_len trans)
+ with m1' show ?thesis by blast
+ qed
+ qed
+ }
+ thus ?thesis unfolding wf_eq_minimal by (metis converse_iff)
+qed
+
+
+fun annos :: "'a acom \<Rightarrow> 'a list" where
+"annos (SKIP {a}) = [a]" |
+"annos (x::=e {a}) = [a]" |
+"annos (c1;c2) = annos c1 @ annos c2" |
+"annos (IF b THEN c1 ELSE c2 {a}) = a # annos c1 @ annos c2" |
+"annos ({i} WHILE b DO c {a}) = i # a # annos c"
+
+lemma size_annos_same: "strip c1 = strip c2 \<Longrightarrow> size(annos c1) = size(annos c2)"
+apply(induct c2 arbitrary: c1)
+apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Semi strip_eq_If strip_eq_While)
+done
+
+lemma le_iff_le_annos: "c1 \<sqsubseteq> c2 \<longleftrightarrow>
+ (annos c1, annos c2) : listrel{(x,y). x \<sqsubseteq> y} \<and> strip c1 = strip c2"
+apply(induct c1 c2 rule: le_acom.induct)
+apply (auto simp: listrel.Nil listrel_Cons_iff listrel_app size_annos_same)
+apply (metis listrel_app_same_size size_annos_same)+
+done
+
+lemma le_acom_subset_same_annos:
+ "(strict{(c,c'::'a::preord acom). c \<sqsubseteq> c'})^-1 \<subseteq>
+ (strict(inv_image (listrel{(a,a'::'a). a \<sqsubseteq> a'} - {([],[])}) annos))^-1"
+by(auto simp: le_iff_le_annos)
+
+lemma acc_acom: "acc {(a,a'::'a::preord). a \<sqsubseteq> a'} \<Longrightarrow>
+ acc {(c,c'::'a acom). c \<sqsubseteq> c'}"
+apply(rule wf_subset[OF _ le_acom_subset_same_annos])
+apply(rule acc_inv_image[OF acc_listrel])
+apply(auto simp: refl_on_def trans_def intro: le_trans)
+done
+
+text{* Termination of the fixed-point finders, assuming monotone functions: *}
+
+lemma pfp_termination:
+fixes x0 :: "'a::preord"
+assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "acc {(x::'a,y). x \<sqsubseteq> y}"
+and "x0 \<sqsubseteq> f x0" shows "EX x. pfp f x0 = Some x"
+proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. x \<sqsubseteq> f x"])
+ show "wf {(x, s). (s \<sqsubseteq> f s \<and> \<not> f s \<sqsubseteq> s) \<and> x = f s}"
+ by(rule wf_subset[OF assms(2)]) auto
+next
+ show "x0 \<sqsubseteq> f x0" by(rule assms)
+next
+ fix x assume "x \<sqsubseteq> f x" thus "f x \<sqsubseteq> f(f x)" by(rule mono)
+qed
+
+lemma lpfpc_termination:
+ fixes f :: "(('a::SL_top)option acom \<Rightarrow> 'a option acom)"
+ assumes "acc {(x::'a,y). x \<sqsubseteq> y}" and "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+ and "\<And>c. strip(f c) = strip c"
+ shows "\<exists>c'. lpfp\<^isub>c f c = Some c'"
+unfolding lpfp\<^isub>c_def
+apply(rule pfp_termination)
+ apply(erule assms(2))
+ apply(rule acc_acom[OF acc_option[OF assms(1)]])
+apply(simp add: bot_acom assms(3))
+done
+
+
end
--- a/src/HOL/IMP/Abs_Int0_const.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy Mon Jan 09 18:33:55 2012 +0100
@@ -6,29 +6,29 @@
subsection "Constant Propagation"
-datatype cval = Const val | Any
+datatype const = Const val | Any
-fun \<gamma>_cval where
-"\<gamma>_cval (Const n) = {n}" |
-"\<gamma>_cval (Any) = UNIV"
+fun \<gamma>_const where
+"\<gamma>_const (Const n) = {n}" |
+"\<gamma>_const (Any) = UNIV"
-fun plus_cval where
-"plus_cval (Const m) (Const n) = Const(m+n)" |
-"plus_cval _ _ = Any"
+fun plus_const where
+"plus_const (Const m) (Const n) = Const(m+n)" |
+"plus_const _ _ = Any"
-lemma plus_cval_cases: "plus_cval a1 a2 =
+lemma plus_const_cases: "plus_const a1 a2 =
(case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
-by(auto split: prod.split cval.split)
+by(auto split: prod.split const.split)
-instantiation cval :: SL_top
+instantiation const :: SL_top
begin
-fun le_cval where
+fun le_const where
"_ \<sqsubseteq> Any = True" |
"Const n \<sqsubseteq> Const m = (n=m)" |
"Any \<sqsubseteq> Const _ = False"
-fun join_cval where
+fun join_const where
"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
"_ \<squnion> _ = Any"
@@ -46,29 +46,29 @@
next
case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
next
- case goal6 thus ?case by(simp add: Top_cval_def)
+ case goal6 thus ?case by(simp add: Top_const_def)
qed
end
interpretation Val_abs
-where \<gamma> = \<gamma>_cval and num' = Const and plus' = plus_cval
+where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
defines aval'_const is aval'
proof
case goal1 thus ?case
by(cases a, cases b, simp, simp, cases b, simp, simp)
next
- case goal2 show ?case by(simp add: Top_cval_def)
+ case goal2 show ?case by(simp add: Top_const_def)
next
case goal3 show ?case by simp
next
case goal4 thus ?case
- by(auto simp: plus_cval_cases split: cval.split)
+ by(auto simp: plus_const_cases split: const.split)
qed
interpretation Abs_Int
-where \<gamma> = \<gamma>_cval and num' = Const and plus' = plus_cval
+where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
defines AI_const is AI
and step_const is step'
proof qed
@@ -77,12 +77,30 @@
text{* Monotonicity: *}
interpretation Abs_Int_mono
-where \<gamma> = \<gamma>_cval and num' = Const and plus' = plus_cval
+where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
proof
case goal1 thus ?case
- by(auto simp: plus_cval_cases split: cval.split)
+ by(auto simp: plus_const_cases split: const.split)
qed
+text{* Termination: *}
+
+lemma measure_const:
+ "(strict{(x::const,y). x \<sqsubseteq> y})^-1 \<subseteq>
+ measure(%x. case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)"
+by(auto split: const.splits)
+
+lemma measure_const_eq:
+ "\<forall> x y::const. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> (%x. case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0) x = (%x. case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0) y"
+by(auto split: const.splits)
+
+lemma acc_const_st: "Abs_Int0.acc{(x::const st,y). x \<sqsubseteq> y}"
+by(rule wf_subset[OF wf_measure measure_st[OF measure_const measure_const_eq]])
+
+lemma "EX c'. AI_const c = Some c'"
+by(metis AI_def lpfpc_termination[OF acc_const_st, where f = "step_const \<top>",
+ OF mono_step'[OF le_refl] strip_step'])
+
subsubsection "Tests"
--- a/src/HOL/IMP/Abs_Int0_fun.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy Mon Jan 09 18:33:55 2012 +0100
@@ -372,6 +372,9 @@
subsubsection "Monotonicity"
+lemma mono_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
+by(induction c c' rule: le_acom.induct) (auto)
+
locale Abs_Int_Fun_mono = Abs_Int_Fun +
assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
begin
@@ -382,9 +385,10 @@
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
by(simp add: le_fun_def)
-lemma step'_mono: "S \<sqsubseteq> S' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c"
-apply(induction c arbitrary: S S')
-apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split)
+lemma mono_step': "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'"
+apply(induction c c' arbitrary: S S' rule: le_acom.induct)
+apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj
+ split: option.split)
done
end
--- a/src/HOL/IMP/Abs_Int1.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Mon Jan 09 18:33:55 2012 +0100
@@ -260,18 +260,14 @@
apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv)
done
-
-lemma post_le_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
-by (induction c c' rule: le_acom.induct) simp_all
-
-lemma mono_step'_aux: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'"
+lemma mono_step': "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'"
apply(induction c c' arbitrary: S S' rule: le_acom.induct)
-apply (auto simp: post_le_post Let_def mono_bfilter mono_update mono_aval' le_join_disj
+apply (auto simp: mono_post mono_bfilter mono_update mono_aval' Let_def le_join_disj
split: option.split)
done
-lemma mono_step': "mono (step' S)"
-by(simp add: mono_def mono_step'_aux[OF le_refl])
+lemma mono_step'2: "mono (step' S)"
+by(simp add: mono_def mono_step'[OF le_refl])
end
--- a/src/HOL/IMP/Abs_Int2.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy Mon Jan 09 18:33:55 2012 +0100
@@ -190,7 +190,7 @@
lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'"
proof(simp add: CS_def AI_WN_def)
assume 1: "pfp_WN (step' \<top>) c = Some c'"
- from pfp_WN_pfp[OF allI[OF strip_step'] mono_step' 1]
+ from pfp_WN_pfp[OF allI[OF strip_step'] mono_step'2 1]
have 2: "step' \<top> c' \<sqsubseteq> c'" .
have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1])
have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> c')"
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Mon Jan 09 18:33:55 2012 +0100
@@ -5,7 +5,7 @@
header {* An efficient checker for proofs from a SAT solver *}
theory SatChecker
-imports "~~/src/HOL/Library/RBT_Impl" Sorted_List Imperative_HOL
+imports "~~/src/HOL/Library/RBT_Impl" Sorted_List "../Imperative_HOL"
begin
section{* General settings and functions for our representation of clauses *}
@@ -264,7 +264,7 @@
case (3 l v va r)
thus ?case
unfolding resolve2.simps
- by (fastforce dest!: res_mem simp add: merge_Nil)
+ by (fastforce dest!: res_mem)
qed
lemma res_thm'_Inv:
@@ -707,9 +707,10 @@
code_type ProofStep
(SML "MinisatProofStep.ProofStep")
-code_const ProofDone and Root and Conflict and Delete and Xstep
- (SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))")
+code_const ProofDone and Root and Conflict and Delete and Xstep
+ (SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))")
export_code checker tchecker lchecker in SML
end
+
--- a/src/HOL/Import/HOL/rich_list.imp Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Import/HOL/rich_list.imp Mon Jan 09 18:33:55 2012 +0100
@@ -100,7 +100,6 @@
"REVERSE_SNOC" > "HOL4Base.rich_list.REVERSE_SNOC"
"REVERSE_REVERSE" > "List.rev_rev_ident"
"REVERSE_FOLDR" > "HOL4Base.rich_list.REVERSE_FOLDR"
- "REVERSE_FOLDL" > "List.rev_foldl_cons"
"REVERSE_FLAT" > "HOL4Base.rich_list.REVERSE_FLAT"
"REVERSE_EQ_NIL" > "List.rev_is_Nil_conv"
"REVERSE_APPEND" > "List.rev_append"
@@ -238,7 +237,6 @@
"FLAT_SNOC" > "HOL4Base.rich_list.FLAT_SNOC"
"FLAT_REVERSE" > "HOL4Base.rich_list.FLAT_REVERSE"
"FLAT_FOLDR" > "HOL4Base.rich_list.FLAT_FOLDR"
- "FLAT_FOLDL" > "List.concat_conv_foldl"
"FLAT_FLAT" > "HOL4Base.rich_list.FLAT_FLAT"
"FLAT_APPEND" > "List.concat_append"
"FLAT" > "HOL4Compat.FLAT"
--- a/src/HOL/IsaMakefile Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/IsaMakefile Mon Jan 09 18:33:55 2012 +0100
@@ -286,8 +286,6 @@
List.thy \
Main.thy \
Map.thy \
- More_List.thy \
- More_Set.thy \
Nat_Numeral.thy \
Nat_Transfer.thy \
New_DSequence.thy \
--- a/src/HOL/Library/AList_Impl.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Library/AList_Impl.thy Mon Jan 09 18:33:55 2012 +0100
@@ -76,10 +76,10 @@
lemma image_update [simp]:
"x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
- by (simp add: update_conv' image_map_upd)
+ by (simp add: update_conv')
definition updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list" where
- "updates ks vs = More_List.fold (prod_case update) (zip ks vs)"
+ "updates ks vs = fold (prod_case update) (zip ks vs)"
lemma updates_simps [simp]:
"updates [] vs ps = ps"
@@ -94,10 +94,10 @@
lemma updates_conv': "map_of (updates ks vs al) = (map_of al)(ks[\<mapsto>]vs)"
proof -
- have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
- More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
+ have "map_of \<circ> fold (prod_case update) (zip ks vs) =
+ fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
by (rule fold_commute) (auto simp add: fun_eq_iff update_conv')
- then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_fold split_def)
+ then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_def split_def)
qed
lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
@@ -107,12 +107,12 @@
assumes "distinct (map fst al)"
shows "distinct (map fst (updates ks vs al))"
proof -
- have "distinct (More_List.fold
+ have "distinct (fold
(\<lambda>(k, v) al. if k \<in> set al then al else al @ [k])
(zip ks vs) (map fst al))"
by (rule fold_invariant [of "zip ks vs" "\<lambda>_. True"]) (auto intro: assms)
- moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
- More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
+ moreover have "map fst \<circ> fold (prod_case update) (zip ks vs) =
+ fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
by (rule fold_commute) (simp add: update_keys split_def prod_case_beta comp_def)
ultimately show ?thesis by (simp add: updates_def fun_eq_iff)
qed
@@ -339,8 +339,8 @@
lemma clearjunk_updates:
"clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
proof -
- have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
- More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
+ have "clearjunk \<circ> fold (prod_case update) (zip ks vs) =
+ fold (prod_case update) (zip ks vs) \<circ> clearjunk"
by (rule fold_commute) (simp add: clearjunk_update prod_case_beta o_def)
then show ?thesis by (simp add: updates_def fun_eq_iff)
qed
@@ -427,7 +427,7 @@
lemma merge_updates:
"merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
- by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
+ by (simp add: merge_def updates_def foldr_def zip_rev zip_map_fst_snd)
lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
by (induct ys arbitrary: xs) (auto simp add: dom_update)
@@ -444,11 +444,11 @@
lemma merge_conv':
"map_of (merge xs ys) = map_of xs ++ map_of ys"
proof -
- have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
- More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
+ have "map_of \<circ> fold (prod_case update) (rev ys) =
+ fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff)
then show ?thesis
- by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev fun_eq_iff)
+ by (simp add: merge_def map_add_map_of_foldr foldr_def fun_eq_iff)
qed
corollary merge_conv:
--- a/src/HOL/Library/Cset.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Library/Cset.thy Mon Jan 09 18:33:55 2012 +0100
@@ -276,7 +276,7 @@
fix xs :: "'a list"
show "member (Cset.set xs) = member (fold insert xs Cset.empty)"
by (simp add: fold_commute_apply [symmetric, where ?h = Set and ?g = Set.insert]
- fun_eq_iff Cset.set_def union_set [symmetric])
+ fun_eq_iff Cset.set_def union_set_fold [symmetric])
qed
lemma single_code [code]:
@@ -296,7 +296,7 @@
"inf A (Cset.coset xs) = foldr Cset.remove xs A"
proof -
show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
- by (simp add: inter project_def Cset.set_def member_def)
+ by (simp add: project_def Cset.set_def member_def) auto
have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of)"
by (simp add: fun_eq_iff Set.remove_def)
have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs =
@@ -306,7 +306,7 @@
set_of (fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs A)"
by (simp add: fun_eq_iff)
then have "inf A (Cset.coset xs) = fold Cset.remove xs A"
- by (simp add: Diff_eq [symmetric] minus_set *)
+ by (simp add: Diff_eq [symmetric] minus_set_fold *)
moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
by (auto simp add: Set.remove_def *)
ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A"
@@ -326,7 +326,7 @@
set_of (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs A)"
by (simp add: fun_eq_iff)
then have "sup (Cset.set xs) A = fold Cset.insert xs A"
- by (simp add: union_set *)
+ by (simp add: union_set_fold *)
moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
by (auto simp add: *)
ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
@@ -370,7 +370,7 @@
lemma bind_set:
"Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
- by (simp add: Cset.bind_def SUPR_set_fold)
+ by (simp add: Cset.bind_def SUP_set_fold)
hide_fact (open) bind_set
lemma pred_of_cset_set:
--- a/src/HOL/Library/Dlist.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Library/Dlist.thy Mon Jan 09 18:33:55 2012 +0100
@@ -74,7 +74,7 @@
"length dxs = List.length (list_of_dlist dxs)"
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
- "fold f dxs = More_List.fold f (list_of_dlist dxs)"
+ "fold f dxs = List.fold f (list_of_dlist dxs)"
definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
"foldr f dxs = List.foldr f (list_of_dlist dxs)"
--- a/src/HOL/Library/Formal_Power_Series.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Jan 09 18:33:55 2012 +0100
@@ -1279,64 +1279,21 @@
subsubsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary
finite product of FPS, also the relvant instance of powers of a FPS*}
-definition "natpermute n k = {l:: nat list. length l = k \<and> foldl op + 0 l = n}"
+definition "natpermute n k = {l :: nat list. length l = k \<and> listsum l = n}"
lemma natlist_trivial_1: "natpermute n 1 = {[n]}"
apply (auto simp add: natpermute_def)
apply (case_tac x, auto)
done
-lemma foldl_add_start0:
- "foldl op + x xs = x + foldl op + (0::nat) xs"
- apply (induct xs arbitrary: x)
- apply simp
- unfolding foldl.simps
- apply atomize
- apply (subgoal_tac "\<forall>x\<Colon>nat. foldl op + x xs = x + foldl op + (0\<Colon>nat) xs")
- apply (erule_tac x="x + a" in allE)
- apply (erule_tac x="a" in allE)
- apply simp
- apply assumption
- done
-
-lemma foldl_add_append: "foldl op + (x::nat) (xs@ys) = foldl op + x xs + foldl op + 0 ys"
- apply (induct ys arbitrary: x xs)
- apply auto
- apply (subst (2) foldl_add_start0)
- apply simp
- apply (subst (2) foldl_add_start0)
- by simp
-
-lemma foldl_add_setsum: "foldl op + (x::nat) xs = x + setsum (nth xs) {0..<length xs}"
-proof(induct xs arbitrary: x)
- case Nil thus ?case by simp
-next
- case (Cons a as x)
- have eq: "setsum (op ! (a#as)) {1..<length (a#as)} = setsum (op ! as) {0..<length as}"
- apply (rule setsum_reindex_cong [where f=Suc])
- by (simp_all add: inj_on_def)
- have f: "finite {0}" "finite {1 ..< length (a#as)}" by simp_all
- have d: "{0} \<inter> {1..<length (a#as)} = {}" by simp
- have seq: "{0} \<union> {1..<length(a#as)} = {0 ..<length (a#as)}" by auto
- have "foldl op + x (a#as) = x + foldl op + a as "
- apply (subst foldl_add_start0) by simp
- also have "\<dots> = x + a + setsum (op ! as) {0..<length as}" unfolding Cons.hyps by simp
- also have "\<dots> = x + setsum (op ! (a#as)) {0..<length (a#as)}"
- unfolding eq[symmetric]
- unfolding setsum_Un_disjoint[OF f d, unfolded seq]
- by simp
- finally show ?case .
-qed
-
-
lemma append_natpermute_less_eq:
- assumes h: "xs@ys \<in> natpermute n k" shows "foldl op + 0 xs \<le> n" and "foldl op + 0 ys \<le> n"
+ assumes h: "xs@ys \<in> natpermute n k" shows "listsum xs \<le> n" and "listsum ys \<le> n"
proof-
- {from h have "foldl op + 0 (xs@ ys) = n" by (simp add: natpermute_def)
- hence "foldl op + 0 xs + foldl op + 0 ys = n" unfolding foldl_add_append .}
+ {from h have "listsum (xs @ ys) = n" by (simp add: natpermute_def)
+ hence "listsum xs + listsum ys = n" by simp}
note th = this
- {from th show "foldl op + 0 xs \<le> n" by simp}
- {from th show "foldl op + 0 ys \<le> n" by simp}
+ {from th show "listsum xs \<le> n" by simp}
+ {from th show "listsum ys \<le> n" by simp}
qed
lemma natpermute_split:
@@ -1345,12 +1302,10 @@
proof-
{fix l assume l: "l \<in> ?R"
from l obtain m xs ys where h: "m \<in> {0..n}" and xs: "xs \<in> natpermute m h" and ys: "ys \<in> natpermute (n - m) (k - h)" and leq: "l = xs@ys" by blast
- from xs have xs': "foldl op + 0 xs = m" by (simp add: natpermute_def)
- from ys have ys': "foldl op + 0 ys = n - m" by (simp add: natpermute_def)
+ from xs have xs': "listsum xs = m" by (simp add: natpermute_def)
+ from ys have ys': "listsum ys = n - m" by (simp add: natpermute_def)
have "l \<in> ?L" using leq xs ys h
- apply simp
- apply (clarsimp simp add: natpermute_def simp del: foldl_append)
- apply (simp add: foldl_add_append[unfolded foldl_append])
+ apply (clarsimp simp add: natpermute_def)
unfolding xs' ys'
using mn xs ys
unfolding natpermute_def by simp}
@@ -1358,19 +1313,21 @@
{fix l assume l: "l \<in> natpermute n k"
let ?xs = "take h l"
let ?ys = "drop h l"
- let ?m = "foldl op + 0 ?xs"
- from l have ls: "foldl op + 0 (?xs @ ?ys) = n" by (simp add: natpermute_def)
+ let ?m = "listsum ?xs"
+ from l have ls: "listsum (?xs @ ?ys) = n" by (simp add: natpermute_def)
have xs: "?xs \<in> natpermute ?m h" using l mn by (simp add: natpermute_def)
- have ys: "?ys \<in> natpermute (n - ?m) (k - h)" using l mn ls[unfolded foldl_add_append]
- by (simp add: natpermute_def)
- from ls have m: "?m \<in> {0..n}" unfolding foldl_add_append by simp
+ have l_take_drop: "listsum l = listsum (take h l @ drop h l)" by simp
+ then have ys: "?ys \<in> natpermute (n - ?m) (k - h)" using l mn ls
+ by (auto simp add: natpermute_def simp del: append_take_drop_id)
+ from ls have m: "?m \<in> {0..n}" by (simp add: l_take_drop del: append_take_drop_id)
from xs ys ls have "l \<in> ?R"
apply auto
apply (rule bexI[where x = "?m"])
apply (rule exI[where x = "?xs"])
apply (rule exI[where x = "?ys"])
- using ls l unfolding foldl_add_append
- by (auto simp add: natpermute_def)}
+ using ls l
+ apply (auto simp add: natpermute_def l_take_drop simp del: append_take_drop_id)
+ by simp}
ultimately show ?thesis by blast
qed
@@ -1408,7 +1365,7 @@
have f: "finite({0..k} - {i})" "finite {i}" by auto
have d: "({0..k} - {i}) \<inter> {i} = {}" using i by auto
from H have "n = setsum (nth xs) {0..k}" apply (simp add: natpermute_def)
- unfolding foldl_add_setsum by (auto simp add: atLeastLessThanSuc_atLeastAtMost)
+ by (auto simp add: atLeastLessThanSuc_atLeastAtMost listsum_setsum_nth)
also have "\<dots> = n + setsum (nth xs) ({0..k} - {i})"
unfolding setsum_Un_disjoint[OF f d, unfolded eqs] using i by simp
finally have zxs: "\<forall> j\<in> {0..k} - {i}. xs!j = 0" by auto
@@ -1430,8 +1387,8 @@
have nxs: "n \<in> set ?xs"
apply (rule set_update_memI) using i by simp
have xsl: "length ?xs = k+1" by (simp only: length_replicate length_list_update)
- have "foldl op + 0 ?xs = setsum (nth ?xs) {0..<k+1}"
- unfolding foldl_add_setsum add_0 length_replicate length_list_update ..
+ have "listsum ?xs = setsum (nth ?xs) {0..<k+1}"
+ unfolding listsum_setsum_nth xsl ..
also have "\<dots> = setsum (\<lambda>j. if j = i then n else 0) {0..< k+1}"
apply (rule setsum_cong2) by (simp del: replicate.simps)
also have "\<dots> = n" using i by (simp add: setsum_delta)
@@ -1579,9 +1536,9 @@
have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1..<Suc k}" by simp_all
have d: "{0 ..< i} \<inter> ({i} \<union> {i+1 ..< Suc k}) = {}" "{i} \<inter> {i+1..< Suc k} = {}" by auto
have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})" using i by auto
- from xs have "Suc n = foldl op + 0 xs" by (simp add: natpermute_def)
- also have "\<dots> = setsum (nth xs) {0..<Suc k}" unfolding foldl_add_setsum using xs
- by (simp add: natpermute_def)
+ from xs have "Suc n = listsum xs" by (simp add: natpermute_def)
+ also have "\<dots> = setsum (nth xs) {0..<Suc k}" using xs
+ by (simp add: natpermute_def listsum_setsum_nth)
also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}"
unfolding eqs setsum_Un_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
unfolding setsum_Un_disjoint[OF fths(2) fths(3) d(2)]
@@ -1824,9 +1781,9 @@
have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1..<Suc k}" by simp_all
have d: "{0 ..< i} \<inter> ({i} \<union> {i+1 ..< Suc k}) = {}" "{i} \<inter> {i+1..< Suc k} = {}" by auto
have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})" using i by auto
- from xs have "n = foldl op + 0 xs" by (simp add: natpermute_def)
- also have "\<dots> = setsum (nth xs) {0..<Suc k}" unfolding foldl_add_setsum using xs
- by (simp add: natpermute_def)
+ from xs have "n = listsum xs" by (simp add: natpermute_def)
+ also have "\<dots> = setsum (nth xs) {0..<Suc k}" using xs
+ by (simp add: natpermute_def listsum_setsum_nth)
also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}"
unfolding eqs setsum_Un_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
unfolding setsum_Un_disjoint[OF fths(2) fths(3) d(2)]
--- a/src/HOL/Library/List_Cset.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Library/List_Cset.thy Mon Jan 09 18:33:55 2012 +0100
@@ -72,7 +72,7 @@
lemma filter_set [code]:
"Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)"
- by (simp add: Cset.set_def project_set)
+ by (simp add: Cset.set_def)
lemma forall_set [code]:
"Cset.forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
--- a/src/HOL/Library/Monad_Syntax.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy Mon Jan 09 18:33:55 2012 +0100
@@ -74,7 +74,7 @@
#> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
#> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
#> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
- #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name More_List.bind}
+ #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name List.bind}
*}
end
--- a/src/HOL/Library/RBT.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Library/RBT.thy Mon Jan 09 18:33:55 2012 +0100
@@ -146,7 +146,7 @@
by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
lemma fold_fold:
- "fold f t = More_List.fold (prod_case f) (entries t)"
+ "fold f t = List.fold (prod_case f) (entries t)"
by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
lemma is_empty_empty [simp]:
--- a/src/HOL/Library/RBT_Impl.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Library/RBT_Impl.thy Mon Jan 09 18:33:55 2012 +0100
@@ -1049,7 +1049,7 @@
subsection {* Folding over entries *}
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
- "fold f t = More_List.fold (prod_case f) (entries t)"
+ "fold f t = List.fold (prod_case f) (entries t)"
lemma fold_simps [simp, code]:
"fold f Empty = id"
@@ -1071,12 +1071,12 @@
proof -
obtain ys where "ys = rev xs" by simp
have "\<And>t. is_rbt t \<Longrightarrow>
- lookup (More_List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
+ lookup (List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta)
from this Empty_is_rbt have
- "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
+ "lookup (List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
by (simp add: `ys = rev xs`)
- then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev)
+ then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_def)
qed
hide_const (open) R B Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
--- a/src/HOL/List.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/List.thy Mon Jan 09 18:33:55 2012 +0100
@@ -49,6 +49,10 @@
"set [] = {}"
| "set (x # xs) = insert x (set xs)"
+definition
+ coset :: "'a list \<Rightarrow> 'a set" where
+ [simp]: "coset xs = - set xs"
+
primrec
map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
"map f [] = []"
@@ -81,15 +85,18 @@
syntax (HTML output)
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
-primrec
+primrec -- {* canonical argument order *}
+ fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
+ "fold f [] = id"
+ | "fold f (x # xs) = fold f xs \<circ> f x"
+
+definition
+ foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
+ [code_abbrev]: "foldr f xs = fold f (rev xs)"
+
+definition
foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
- foldl_Nil: "foldl f a [] = a"
- | foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
-
-primrec
- foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
- "foldr f [] a = a"
- | "foldr f (x # xs) a = f x (foldr f xs a)"
+ "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
primrec
concat:: "'a list list \<Rightarrow> 'a list" where
@@ -236,8 +243,9 @@
@{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
@{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
@{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
-@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
-@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
+@{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\
+@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by (simp add: foldr_def)}\\
+@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by (simp add: foldl_def)}\\
@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
@@ -261,7 +269,7 @@
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def eval_nat_numeral)}\\
@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
-@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}
+@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)}
\end{tabular}}
\caption{Characteristic examples}
\label{fig:Characteristic}
@@ -298,11 +306,11 @@
by simp_all
primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
-"insort_key f x [] = [x]" |
-"insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
+ "insort_key f x [] = [x]" |
+ "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
-"sort_key f xs = foldr (insort_key f) xs []"
+ "sort_key f xs = foldr (insort_key f) xs []"
definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
"insort_insert_key f x xs = (if f x \<in> f ` set xs then xs else insort_key f x xs)"
@@ -341,90 +349,91 @@
mangled). In such cases it can be advisable to introduce separate
definitions for the list comprehensions in question. *}
-nonterminal lc_gen and lc_qual and lc_quals
+nonterminal lc_qual and lc_quals
syntax
-"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __")
-"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
-"_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
-(*"_lc_let" :: "letbinds => lc_qual" ("let _")*)
-"_lc_end" :: "lc_quals" ("]")
-"_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
-"_lc_abs" :: "'a => 'b list => 'b list"
-"_strip_positions" :: "'a \<Rightarrow> lc_gen" ("_")
+ "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __")
+ "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
+ "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
+ (*"_lc_let" :: "letbinds => lc_qual" ("let _")*)
+ "_lc_end" :: "lc_quals" ("]")
+ "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
+ "_lc_abs" :: "'a => 'b list => 'b list"
(* These are easier than ML code but cannot express the optimized
translation of [e. p<-xs]
translations
-"[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
-"_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
- => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
-"[e. P]" => "if P then [e] else []"
-"_listcompr e (_lc_test P) (_lc_quals Q Qs)"
- => "if P then (_listcompr e Q Qs) else []"
-"_listcompr e (_lc_let b) (_lc_quals Q Qs)"
- => "_Let b (_listcompr e Q Qs)"
+ "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
+ "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
+ => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
+ "[e. P]" => "if P then [e] else []"
+ "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
+ => "if P then (_listcompr e Q Qs) else []"
+ "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
+ => "_Let b (_listcompr e Q Qs)"
*)
syntax (xsymbols)
-"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
+ "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
syntax (HTML output)
-"_lc_gen" :: "lc_gen \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
+ "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
parse_translation (advanced) {*
-let
- val NilC = Syntax.const @{const_syntax Nil};
- val ConsC = Syntax.const @{const_syntax Cons};
- val mapC = Syntax.const @{const_syntax map};
- val concatC = Syntax.const @{const_syntax concat};
- val IfC = Syntax.const @{const_syntax If};
-
- fun singl x = ConsC $ x $ NilC;
-
- fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
- let
- (* FIXME proper name context!? *)
- val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
- val e = if opti then singl e else e;
- val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
- val case2 =
- Syntax.const @{syntax_const "_case1"} $
- Syntax.const @{const_syntax dummy_pattern} $ NilC;
- val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
- val ft = Datatype_Case.case_tr false ctxt [x, cs];
- in lambda x ft end;
-
- fun abs_tr ctxt (p as Free (s, T)) e opti =
- let
- val thy = Proof_Context.theory_of ctxt;
- val s' = Proof_Context.intern_const ctxt s;
- in
- if Sign.declared_const thy s'
- then (pat_tr ctxt p e opti, false)
- else (lambda p e, true)
- end
- | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
-
- fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
- let
- val res =
- (case qs of
- Const (@{syntax_const "_lc_end"}, _) => singl e
- | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
- in IfC $ b $ res $ NilC end
- | lc_tr ctxt
- [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
- Const(@{syntax_const "_lc_end"}, _)] =
- (case abs_tr ctxt p e true of
- (f, true) => mapC $ f $ es
- | (f, false) => concatC $ (mapC $ f $ es))
- | lc_tr ctxt
- [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
- Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
- let val e' = lc_tr ctxt [e, q, qs];
- in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
-
-in [(@{syntax_const "_listcompr"}, lc_tr)] end
+ let
+ val NilC = Syntax.const @{const_syntax Nil};
+ val ConsC = Syntax.const @{const_syntax Cons};
+ val mapC = Syntax.const @{const_syntax map};
+ val concatC = Syntax.const @{const_syntax concat};
+ val IfC = Syntax.const @{const_syntax If};
+
+ fun single x = ConsC $ x $ NilC;
+
+ fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
+ let
+ (* FIXME proper name context!? *)
+ val x =
+ Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
+ val e = if opti then single e else e;
+ val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
+ val case2 =
+ Syntax.const @{syntax_const "_case1"} $
+ Syntax.const @{const_syntax dummy_pattern} $ NilC;
+ val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
+ in Syntax_Trans.abs_tr [x, Datatype_Case.case_tr false ctxt [x, cs]] end;
+
+ fun abs_tr ctxt p e opti =
+ (case Term_Position.strip_positions p of
+ Free (s, T) =>
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val s' = Proof_Context.intern_const ctxt s;
+ in
+ if Sign.declared_const thy s'
+ then (pat_tr ctxt p e opti, false)
+ else (Syntax_Trans.abs_tr [p, e], true)
+ end
+ | _ => (pat_tr ctxt p e opti, false));
+
+ fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
+ let
+ val res =
+ (case qs of
+ Const (@{syntax_const "_lc_end"}, _) => single e
+ | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
+ in IfC $ b $ res $ NilC end
+ | lc_tr ctxt
+ [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
+ Const(@{syntax_const "_lc_end"}, _)] =
+ (case abs_tr ctxt p e true of
+ (f, true) => mapC $ f $ es
+ | (f, false) => concatC $ (mapC $ f $ es))
+ | lc_tr ctxt
+ [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
+ Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
+ let val e' = lc_tr ctxt [e, q, qs];
+ in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
+
+ in [(@{syntax_const "_listcompr"}, lc_tr)] end
*}
ML {*
@@ -470,6 +479,9 @@
simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
+code_datatype set coset
+
+hide_const (open) coset
subsubsection {* @{const Nil} and @{const Cons} *}
@@ -2368,159 +2380,81 @@
by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
-subsubsection {* @{text foldl} and @{text foldr} *}
-
-lemma foldl_append [simp]:
- "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
-by (induct xs arbitrary: a) auto
-
-lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
-by (induct xs) auto
-
-lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
-by(induct xs) simp_all
-
-text{* For efficient code generation: avoid intermediate list. *}
-lemma foldl_map[code_unfold]:
- "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
-by(induct xs arbitrary:a) simp_all
-
-lemma foldl_apply:
- assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x"
- shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
- by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_iff)
-
-lemma foldl_cong [fundef_cong]:
- "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]
- ==> foldl f a l = foldl g b k"
-by (induct k arbitrary: a b l) simp_all
-
-lemma foldr_cong [fundef_cong]:
- "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |]
- ==> foldr f l a = foldr g k b"
-by (induct k arbitrary: a b l) simp_all
-
-lemma foldl_fun_comm:
- assumes "\<And>x y s. f (f s x) y = f (f s y) x"
- shows "f (foldl f s xs) x = foldl f (f s x) xs"
- by (induct xs arbitrary: s)
- (simp_all add: assms)
-
-lemma (in semigroup_add) foldl_assoc:
-shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
-by (induct zs arbitrary: y) (simp_all add:add_assoc)
-
-lemma (in monoid_add) foldl_absorb0:
-shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
-by (induct zs) (simp_all add:foldl_assoc)
-
-lemma foldl_rev:
- assumes "\<And>x y s. f (f s x) y = f (f s y) x"
- shows "foldl f s (rev xs) = foldl f s xs"
-proof (induct xs arbitrary: s)
- case Nil then show ?case by simp
-next
- case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)
-qed
-
-lemma rev_foldl_cons [code]:
- "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
-proof (induct xs)
- case Nil then show ?case by simp
-next
- case Cons
- {
- fix x xs ys
- have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
- = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
- by (induct xs arbitrary: ys) auto
- }
- note aux = this
- show ?case by (induct xs) (auto simp add: Cons aux)
+subsubsection {* @{const fold} with canonical argument order *}
+
+lemma fold_remove1_split:
+ assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
+ and x: "x \<in> set xs"
+ shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
+ using assms by (induct xs) (auto simp add: o_assoc [symmetric])
+
+lemma fold_cong [fundef_cong]:
+ "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
+ \<Longrightarrow> fold f xs a = fold g ys b"
+ by (induct ys arbitrary: a b xs) simp_all
+
+lemma fold_id:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
+ shows "fold f xs = id"
+ using assms by (induct xs) simp_all
+
+lemma fold_commute:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
+ shows "h \<circ> fold g xs = fold f xs \<circ> h"
+ using assms by (induct xs) (simp_all add: fun_eq_iff)
+
+lemma fold_commute_apply:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
+ shows "h (fold g xs s) = fold f xs (h s)"
+proof -
+ from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
+ then show ?thesis by (simp add: fun_eq_iff)
qed
-
-text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
-
-lemma foldr_foldl:
- "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
- by (induct xs) auto
-
-lemma foldl_foldr:
- "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
- by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
-
-
-text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
-
-lemma (in monoid_add) foldl_foldr1_lemma:
- "foldl op + a xs = a + foldr op + xs 0"
- by (induct xs arbitrary: a) (auto simp: add_assoc)
-
-corollary (in monoid_add) foldl_foldr1:
- "foldl op + 0 xs = foldr op + xs 0"
- by (simp add: foldl_foldr1_lemma)
-
-lemma (in ab_semigroup_add) foldr_conv_foldl:
- "foldr op + xs a = foldl op + a xs"
- by (induct xs) (simp_all add: foldl_assoc add.commute)
-
-text {*
-Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
-difficult to use because it requires an additional transitivity step.
-*}
-
-lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
-by (induct ns arbitrary: n) auto
-
-lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
-by (force intro: start_le_sum simp add: in_set_conv_decomp)
-
-lemma sum_eq_0_conv [iff]:
- "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
-by (induct ns arbitrary: m) auto
-
-lemma foldr_invariant:
- "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f x y) \<rbrakk> \<Longrightarrow> Q (foldr f xs x)"
- by (induct xs, simp_all)
-
-lemma foldl_invariant:
- "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f y x) \<rbrakk> \<Longrightarrow> Q (foldl f x xs)"
- by (induct xs arbitrary: x, simp_all)
-
-lemma foldl_weak_invariant:
- assumes "P s"
- and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)"
- shows "P (foldl f s xs)"
+lemma fold_invariant:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
+ and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
+ shows "P (fold f xs s)"
using assms by (induct xs arbitrary: s) simp_all
-text {* @{const foldl} and @{const concat} *}
-
-lemma foldl_conv_concat:
- "foldl (op @) xs xss = xs @ concat xss"
-proof (induct xss arbitrary: xs)
- case Nil show ?case by simp
-next
- interpret monoid_add "op @" "[]" proof qed simp_all
- case Cons then show ?case by (simp add: foldl_absorb0)
-qed
-
-lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
- by (simp add: foldl_conv_concat)
-
-text {* @{const Finite_Set.fold} and @{const foldl} *}
-
-lemma (in comp_fun_commute) fold_set_remdups:
- "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
+lemma fold_append [simp]:
+ "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
+ by (induct xs) simp_all
+
+lemma fold_map [code_unfold]:
+ "fold g (map f xs) = fold (g o f) xs"
+ by (induct xs) simp_all
+
+lemma fold_rev:
+ assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
+ shows "fold f (rev xs) = fold f xs"
+using assms by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
+
+lemma fold_Cons_rev:
+ "fold Cons xs = append (rev xs)"
+ by (induct xs) simp_all
+
+lemma rev_conv_fold [code]:
+ "rev xs = fold Cons xs []"
+ by (simp add: fold_Cons_rev)
+
+lemma fold_append_concat_rev:
+ "fold append xss = append (concat (rev xss))"
+ by (induct xss) simp_all
+
+text {* @{const Finite_Set.fold} and @{const fold} *}
+
+lemma (in comp_fun_commute) fold_set_fold_remdups:
+ "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
-lemma (in comp_fun_idem) fold_set:
- "Finite_Set.fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
+lemma (in comp_fun_idem) fold_set_fold:
+ "Finite_Set.fold f y (set xs) = fold f xs y"
by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
-lemma (in ab_semigroup_idem_mult) fold1_set:
+lemma (in ab_semigroup_idem_mult) fold1_set_fold:
assumes "xs \<noteq> []"
- shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"
+ shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
proof -
interpret comp_fun_idem times by (fact comp_fun_idem)
from assms obtain y ys where xs: "xs = y # ys"
@@ -2532,10 +2466,235 @@
case False
then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
by (simp only: finite_set fold1_eq_fold_idem)
- with xs show ?thesis by (simp add: fold_set mult_commute)
+ with xs show ?thesis by (simp add: fold_set_fold mult_commute)
qed
qed
+lemma union_set_fold:
+ "set xs \<union> A = fold Set.insert xs A"
+proof -
+ interpret comp_fun_idem Set.insert
+ by (fact comp_fun_idem_insert)
+ show ?thesis by (simp add: union_fold_insert fold_set_fold)
+qed
+
+lemma minus_set_fold:
+ "A - set xs = fold Set.remove xs A"
+proof -
+ interpret comp_fun_idem Set.remove
+ by (fact comp_fun_idem_remove)
+ show ?thesis
+ by (simp add: minus_fold_remove [of _ A] fold_set_fold)
+qed
+
+lemma (in lattice) Inf_fin_set_fold:
+ "Inf_fin (set (x # xs)) = fold inf xs x"
+proof -
+ interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact ab_semigroup_idem_mult_inf)
+ show ?thesis
+ by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
+qed
+
+lemma (in lattice) Sup_fin_set_fold:
+ "Sup_fin (set (x # xs)) = fold sup xs x"
+proof -
+ interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact ab_semigroup_idem_mult_sup)
+ show ?thesis
+ by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
+qed
+
+lemma (in linorder) Min_fin_set_fold:
+ "Min (set (x # xs)) = fold min xs x"
+proof -
+ interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact ab_semigroup_idem_mult_min)
+ show ?thesis
+ by (simp add: Min_def fold1_set_fold del: set.simps)
+qed
+
+lemma (in linorder) Max_fin_set_fold:
+ "Max (set (x # xs)) = fold max xs x"
+proof -
+ interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact ab_semigroup_idem_mult_max)
+ show ?thesis
+ by (simp add: Max_def fold1_set_fold del: set.simps)
+qed
+
+lemma (in complete_lattice) Inf_set_fold:
+ "Inf (set xs) = fold inf xs top"
+proof -
+ interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact comp_fun_idem_inf)
+ show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute)
+qed
+
+lemma (in complete_lattice) Sup_set_fold:
+ "Sup (set xs) = fold sup xs bot"
+proof -
+ interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact comp_fun_idem_sup)
+ show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute)
+qed
+
+lemma (in complete_lattice) INF_set_fold:
+ "INFI (set xs) f = fold (inf \<circ> f) xs top"
+ unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
+
+lemma (in complete_lattice) SUP_set_fold:
+ "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
+ unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
+
+
+subsubsection {* Fold variants: @{const foldr} and @{const foldl} *}
+
+text {* Correspondence *}
+
+lemma foldr_foldl: -- {* The ``Third Duality Theorem'' in Bird \& Wadler: *}
+ "foldr f xs a = foldl (\<lambda>x y. f y x) a (rev xs)"
+ by (simp add: foldr_def foldl_def)
+
+lemma foldl_foldr:
+ "foldl f a xs = foldr (\<lambda>x y. f y x) (rev xs) a"
+ by (simp add: foldr_def foldl_def)
+
+lemma foldr_fold:
+ assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
+ shows "foldr f xs = fold f xs"
+ using assms unfolding foldr_def by (rule fold_rev)
+
+lemma
+ foldr_Nil [code, simp]: "foldr f [] = id"
+ and foldr_Cons [code, simp]: "foldr f (x # xs) = f x \<circ> foldr f xs"
+ by (simp_all add: foldr_def)
+
+lemma
+ foldl_Nil [simp]: "foldl f a [] = a"
+ and foldl_Cons [simp]: "foldl f a (x # xs) = foldl f (f a x) xs"
+ by (simp_all add: foldl_def)
+
+lemma foldr_cong [fundef_cong]:
+ "a = b \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f x a = g x a) \<Longrightarrow> foldr f l a = foldr g k b"
+ by (auto simp add: foldr_def intro!: fold_cong)
+
+lemma foldl_cong [fundef_cong]:
+ "a = b \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f a x = g a x) \<Longrightarrow> foldl f a l = foldl g b k"
+ by (auto simp add: foldl_def intro!: fold_cong)
+
+lemma foldr_append [simp]:
+ "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
+ by (simp add: foldr_def)
+
+lemma foldl_append [simp]:
+ "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
+ by (simp add: foldl_def)
+
+lemma foldr_map [code_unfold]:
+ "foldr g (map f xs) a = foldr (g o f) xs a"
+ by (simp add: foldr_def fold_map rev_map)
+
+lemma foldl_map [code_unfold]:
+ "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs"
+ by (simp add: foldl_def fold_map comp_def)
+
+text {* Executing operations in terms of @{const foldr} -- tail-recursive! *}
+
+lemma concat_conv_foldr [code]:
+ "concat xss = foldr append xss []"
+ by (simp add: fold_append_concat_rev foldr_def)
+
+lemma minus_set_foldr [code]:
+ "A - set xs = foldr Set.remove xs A"
+proof -
+ have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
+ by (auto simp add: remove_def)
+ then show ?thesis by (simp add: minus_set_fold foldr_fold)
+qed
+
+lemma subtract_coset_filter [code]:
+ "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
+ by auto
+
+lemma union_set_foldr [code]:
+ "set xs \<union> A = foldr Set.insert xs A"
+proof -
+ have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
+ by auto
+ then show ?thesis by (simp add: union_set_fold foldr_fold)
+qed
+
+lemma union_coset_foldr [code]:
+ "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
+ by auto
+
+lemma inter_set_filer [code]:
+ "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
+ by auto
+
+lemma inter_coset_foldr [code]:
+ "A \<inter> List.coset xs = foldr Set.remove xs A"
+ by (simp add: Diff_eq [symmetric] minus_set_foldr)
+
+lemma (in lattice) Inf_fin_set_foldr [code]:
+ "Inf_fin (set (x # xs)) = foldr inf xs x"
+ by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
+
+lemma (in lattice) Sup_fin_set_foldr [code]:
+ "Sup_fin (set (x # xs)) = foldr sup xs x"
+ by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
+
+lemma (in linorder) Min_fin_set_foldr [code]:
+ "Min (set (x # xs)) = foldr min xs x"
+ by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
+
+lemma (in linorder) Max_fin_set_foldr [code]:
+ "Max (set (x # xs)) = foldr max xs x"
+ by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
+
+lemma (in complete_lattice) Inf_set_foldr:
+ "Inf (set xs) = foldr inf xs top"
+ by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
+
+lemma (in complete_lattice) Sup_set_foldr:
+ "Sup (set xs) = foldr sup xs bot"
+ by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
+
+declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code]
+declare Inf_set_foldr [where 'a = "'a Predicate.pred", code] Sup_set_foldr [where 'a = "'a Predicate.pred", code]
+
+lemma (in complete_lattice) INF_set_foldr [code]:
+ "INFI (set xs) f = foldr (inf \<circ> f) xs top"
+ by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric])
+
+lemma (in complete_lattice) SUP_set_foldr [code]:
+ "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
+ by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric])
+
+(* FIXME: better implement conversion by bisection *)
+
+lemma pred_of_set_fold_sup:
+ assumes "finite A"
+ shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs")
+proof (rule sym)
+ interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
+ by (fact comp_fun_idem_sup)
+ from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI)
+qed
+
+lemma pred_of_set_set_fold_sup:
+ "pred_of_set (set xs) = fold sup (map Predicate.single xs) bot"
+proof -
+ interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
+ by (fact comp_fun_idem_sup)
+ show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric])
+qed
+
+lemma pred_of_set_set_foldr_sup [code]:
+ "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
+ by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
+
subsubsection {* @{text upt} *}
@@ -2940,16 +3099,11 @@
"distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
-
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
-lemma (in monoid_add) listsum_foldl [code]:
- "listsum = foldl (op +) 0"
- by (simp add: listsum_def foldl_foldr1 fun_eq_iff)
-
lemma (in monoid_add) listsum_simps [simp]:
"listsum [] = 0"
- "listsum (x#xs) = x + listsum xs"
+ "listsum (x # xs) = x + listsum xs"
by (simp_all add: listsum_def)
lemma (in monoid_add) listsum_append [simp]:
@@ -2958,7 +3112,60 @@
lemma (in comm_monoid_add) listsum_rev [simp]:
"listsum (rev xs) = listsum xs"
- by (simp add: listsum_def [of "rev xs"]) (simp add: listsum_foldl foldr_foldl add.commute)
+ by (simp add: listsum_def foldr_def fold_rev fun_eq_iff add_ac)
+
+lemma (in monoid_add) fold_plus_listsum_rev:
+ "fold plus xs = plus (listsum (rev xs))"
+proof
+ fix x
+ have "fold plus xs x = fold plus xs (x + 0)" by simp
+ also have "\<dots> = fold plus (x # xs) 0" by simp
+ also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_def)
+ also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def)
+ also have "\<dots> = listsum (rev xs) + listsum [x]" by simp
+ finally show "fold plus xs x = listsum (rev xs) + x" by simp
+qed
+
+lemma (in semigroup_add) foldl_assoc:
+ "foldl plus (x + y) zs = x + foldl plus y zs"
+ by (simp add: foldl_def fold_commute_apply [symmetric] fun_eq_iff add_assoc)
+
+lemma (in ab_semigroup_add) foldr_conv_foldl:
+ "foldr plus xs a = foldl plus a xs"
+ by (simp add: foldl_def foldr_fold fun_eq_iff add_ac)
+
+text {*
+ Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
+ difficult to use because it requires an additional transitivity step.
+*}
+
+lemma start_le_sum:
+ fixes m n :: nat
+ shows "m \<le> n \<Longrightarrow> m \<le> foldl plus n ns"
+ by (simp add: foldl_def add_commute fold_plus_listsum_rev)
+
+lemma elem_le_sum:
+ fixes m n :: nat
+ shows "n \<in> set ns \<Longrightarrow> n \<le> foldl plus 0 ns"
+ by (force intro: start_le_sum simp add: in_set_conv_decomp)
+
+lemma sum_eq_0_conv [iff]:
+ fixes m :: nat
+ shows "foldl plus m ns = 0 \<longleftrightarrow> m = 0 \<and> (\<forall>n \<in> set ns. n = 0)"
+ by (induct ns arbitrary: m) auto
+
+text{* Some syntactic sugar for summing a function over a list: *}
+
+syntax
+ "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
+syntax (xsymbols)
+ "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+syntax (HTML output)
+ "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+
+translations -- {* Beware of argument permutation! *}
+ "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
+ "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
lemma (in comm_monoid_add) listsum_map_remove1:
"x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
@@ -2983,7 +3190,7 @@
lemma listsum_eq_0_nat_iff_nat [simp]:
"listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
- by (simp add: listsum_foldl)
+ by (simp add: listsum_def foldr_conv_foldl)
lemma elem_le_listsum_nat:
"k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
@@ -3000,19 +3207,6 @@
apply arith
done
-text{* Some syntactic sugar for summing a function over a list: *}
-
-syntax
- "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
-syntax (xsymbols)
- "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
-syntax (HTML output)
- "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
-
-translations -- {* Beware of argument permutation! *}
- "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
- "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
-
lemma (in monoid_add) listsum_triv:
"(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
by (induct xs) (simp_all add: left_distrib)
@@ -3819,9 +4013,26 @@
"sort_key f (x#xs) = insort_key f x (sort_key f xs)"
by (simp_all add: sort_key_def)
-lemma sort_foldl_insort:
- "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs"
- by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm)
+lemma (in linorder) sort_key_conv_fold:
+ assumes "inj_on f (set xs)"
+ shows "sort_key f xs = fold (insort_key f) xs []"
+proof -
+ have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
+ proof (rule fold_rev, rule ext)
+ fix zs
+ fix x y
+ assume "x \<in> set xs" "y \<in> set xs"
+ with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
+ have **: "x = y \<longleftrightarrow> y = x" by auto
+ show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
+ by (induct zs) (auto intro: * simp add: **)
+ qed
+ then show ?thesis by (simp add: sort_key_def foldr_def)
+qed
+
+lemma (in linorder) sort_conv_fold:
+ "sort xs = fold insort xs []"
+ by (rule sort_key_conv_fold) simp
lemma length_sort[simp]: "length (sort_key f xs) = length xs"
by (induct xs, auto)
@@ -4312,7 +4523,7 @@
"sorted_list_of_set (set xs) = sort (remdups xs)"
proof -
interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
- show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
+ show ?thesis by (simp add: sorted_list_of_set_def sort_conv_fold fold_set_fold_remdups)
qed
lemma sorted_list_of_set_remove:
@@ -4973,6 +5184,19 @@
by (induct xs) force+
+subsection {* Monad operation *}
+
+definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
+ "bind xs f = concat (map f xs)"
+
+hide_const (open) bind
+
+lemma bind_simps [simp]:
+ "List.bind [] f = []"
+ "List.bind (x # xs) f = f x @ List.bind xs f"
+ by (simp_all add: bind_def)
+
+
subsection {* Transfer *}
definition
@@ -5033,11 +5257,6 @@
"x \<in> set xs \<longleftrightarrow> member xs x"
by (simp add: member_def)
-declare INF_def [code_unfold]
-declare SUP_def [code_unfold]
-
-declare set_map [symmetric, code_unfold]
-
definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
@@ -5348,4 +5567,100 @@
code_const list_ex
(Haskell "any")
+
+subsubsection {* Implementation of sets by lists *}
+
+text {* Basic operations *}
+
+lemma is_empty_set [code]:
+ "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
+ by (simp add: Set.is_empty_def null_def)
+
+lemma empty_set [code]:
+ "{} = set []"
+ by simp
+
+lemma UNIV_coset [code]:
+ "UNIV = List.coset []"
+ by simp
+
+lemma compl_set [code]:
+ "- set xs = List.coset xs"
+ by simp
+
+lemma compl_coset [code]:
+ "- List.coset xs = set xs"
+ by simp
+
+lemma [code]:
+ "x \<in> set xs \<longleftrightarrow> List.member xs x"
+ "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x"
+ by (simp_all add: member_def)
+
+lemma insert_code [code]:
+ "insert x (set xs) = set (List.insert x xs)"
+ "insert x (List.coset xs) = List.coset (removeAll x xs)"
+ by simp_all
+
+lemma remove_code [code]:
+ "Set.remove x (set xs) = set (removeAll x xs)"
+ "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
+ by (simp_all add: remove_def Compl_insert)
+
+lemma project_set [code]:
+ "Set.project P (set xs) = set (filter P xs)"
+ by auto
+
+lemma image_set [code]:
+ "image f (set xs) = set (map f xs)"
+ by simp
+
+lemma Ball_set [code]:
+ "Ball (set xs) P \<longleftrightarrow> list_all P xs"
+ by (simp add: list_all_iff)
+
+lemma Bex_set [code]:
+ "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
+ by (simp add: list_ex_iff)
+
+lemma card_set [code]:
+ "card (set xs) = length (remdups xs)"
+proof -
+ have "card (set (remdups xs)) = length (remdups xs)"
+ by (rule distinct_card) simp
+ then show ?thesis by simp
+qed
+
+lemma the_elem_set [code]:
+ "the_elem (set [x]) = x"
+ by simp
+
+lemma Pow_set [code]:
+ "Pow (set []) = {{}}"
+ "Pow (set (x # xs)) = (let A = Pow (set xs) in A \<union> insert x ` A)"
+ by (simp_all add: Pow_insert Let_def)
+
+
+text {* Operations on relations *}
+
+lemma product_code [code]:
+ "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
+ by (auto simp add: Product_Type.product_def)
+
+lemma Id_on_set [code]:
+ "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
+ by (auto simp add: Id_on_def)
+
+lemma trancl_set_ntrancl [code]:
+ "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
+ by (simp add: finite_trancl_ntranl)
+
+lemma set_rel_comp [code]:
+ "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
+ by (auto simp add: Bex_def)
+
+lemma wf_set [code]:
+ "wf (set xs) = acyclic (set xs)"
+ by (simp add: wf_iff_acyclic_if_finite)
+
end
--- a/src/HOL/Main.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Main.thy Mon Jan 09 18:33:55 2012 +0100
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Plain Predicate_Compile Nitpick More_Set
+imports Plain Predicate_Compile Nitpick
begin
text {*
--- a/src/HOL/More_List.thy Mon Jan 09 18:32:56 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,283 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Operations on lists beyond the standard List theory *}
-
-theory More_List
-imports List
-begin
-
-text {* Fold combinator with canonical argument order *}
-
-primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
- "fold f [] = id"
- | "fold f (x # xs) = fold f xs \<circ> f x"
-
-lemma foldl_fold:
- "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
- by (induct xs arbitrary: s) simp_all
-
-lemma foldr_fold_rev:
- "foldr f xs = fold f (rev xs)"
- by (simp add: foldr_foldl foldl_fold fun_eq_iff)
-
-lemma fold_rev_conv [code_unfold]:
- "fold f (rev xs) = foldr f xs"
- by (simp add: foldr_fold_rev)
-
-lemma fold_cong [fundef_cong]:
- "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
- \<Longrightarrow> fold f xs a = fold g ys b"
- by (induct ys arbitrary: a b xs) simp_all
-
-lemma fold_id:
- assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
- shows "fold f xs = id"
- using assms by (induct xs) simp_all
-
-lemma fold_commute:
- assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
- shows "h \<circ> fold g xs = fold f xs \<circ> h"
- using assms by (induct xs) (simp_all add: fun_eq_iff)
-
-lemma fold_commute_apply:
- assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
- shows "h (fold g xs s) = fold f xs (h s)"
-proof -
- from assms have "h \<circ> fold g xs = fold f xs \<circ> h" by (rule fold_commute)
- then show ?thesis by (simp add: fun_eq_iff)
-qed
-
-lemma fold_invariant:
- assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
- and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
- shows "P (fold f xs s)"
- using assms by (induct xs arbitrary: s) simp_all
-
-lemma fold_weak_invariant:
- assumes "P s"
- and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
- shows "P (fold f xs s)"
- using assms by (induct xs arbitrary: s) simp_all
-
-lemma fold_append [simp]:
- "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
- by (induct xs) simp_all
-
-lemma fold_map [code_unfold]:
- "fold g (map f xs) = fold (g o f) xs"
- by (induct xs) simp_all
-
-lemma fold_remove1_split:
- assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
- and x: "x \<in> set xs"
- shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
- using assms by (induct xs) (auto simp add: o_assoc [symmetric])
-
-lemma fold_rev:
- assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
- shows "fold f (rev xs) = fold f xs"
-using assms by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
-
-lemma foldr_fold:
- assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
- shows "foldr f xs = fold f xs"
- using assms unfolding foldr_fold_rev by (rule fold_rev)
-
-lemma fold_Cons_rev:
- "fold Cons xs = append (rev xs)"
- by (induct xs) simp_all
-
-lemma rev_conv_fold [code]:
- "rev xs = fold Cons xs []"
- by (simp add: fold_Cons_rev)
-
-lemma fold_append_concat_rev:
- "fold append xss = append (concat (rev xss))"
- by (induct xss) simp_all
-
-lemma concat_conv_foldr [code]:
- "concat xss = foldr append xss []"
- by (simp add: fold_append_concat_rev foldr_fold_rev)
-
-lemma fold_plus_listsum_rev:
- "fold plus xs = plus (listsum (rev xs))"
- by (induct xs) (simp_all add: add.assoc)
-
-lemma (in monoid_add) listsum_conv_fold [code]:
- "listsum xs = fold (\<lambda>x y. y + x) xs 0"
- by (auto simp add: listsum_foldl foldl_fold fun_eq_iff)
-
-lemma (in linorder) sort_key_conv_fold:
- assumes "inj_on f (set xs)"
- shows "sort_key f xs = fold (insort_key f) xs []"
-proof -
- have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
- proof (rule fold_rev, rule ext)
- fix zs
- fix x y
- assume "x \<in> set xs" "y \<in> set xs"
- with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
- have **: "x = y \<longleftrightarrow> y = x" by auto
- show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
- by (induct zs) (auto intro: * simp add: **)
- qed
- then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
-qed
-
-lemma (in linorder) sort_conv_fold:
- "sort xs = fold insort xs []"
- by (rule sort_key_conv_fold) simp
-
-
-text {* @{const Finite_Set.fold} and @{const fold} *}
-
-lemma (in comp_fun_commute) fold_set_fold_remdups:
- "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
- by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
-
-lemma (in comp_fun_idem) fold_set_fold:
- "Finite_Set.fold f y (set xs) = fold f xs y"
- by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
-
-lemma (in ab_semigroup_idem_mult) fold1_set_fold:
- assumes "xs \<noteq> []"
- shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
-proof -
- interpret comp_fun_idem times by (fact comp_fun_idem)
- from assms obtain y ys where xs: "xs = y # ys"
- by (cases xs) auto
- show ?thesis
- proof (cases "set ys = {}")
- case True with xs show ?thesis by simp
- next
- case False
- then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
- by (simp only: finite_set fold1_eq_fold_idem)
- with xs show ?thesis by (simp add: fold_set_fold mult_commute)
- qed
-qed
-
-lemma (in lattice) Inf_fin_set_fold:
- "Inf_fin (set (x # xs)) = fold inf xs x"
-proof -
- interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact ab_semigroup_idem_mult_inf)
- show ?thesis
- by (simp add: Inf_fin_def fold1_set_fold del: set.simps)
-qed
-
-lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
- "Inf_fin (set (x # xs)) = foldr inf xs x"
- by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
-
-lemma (in lattice) Sup_fin_set_fold:
- "Sup_fin (set (x # xs)) = fold sup xs x"
-proof -
- interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact ab_semigroup_idem_mult_sup)
- show ?thesis
- by (simp add: Sup_fin_def fold1_set_fold del: set.simps)
-qed
-
-lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
- "Sup_fin (set (x # xs)) = foldr sup xs x"
- by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
-
-lemma (in linorder) Min_fin_set_fold:
- "Min (set (x # xs)) = fold min xs x"
-proof -
- interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact ab_semigroup_idem_mult_min)
- show ?thesis
- by (simp add: Min_def fold1_set_fold del: set.simps)
-qed
-
-lemma (in linorder) Min_fin_set_foldr [code_unfold]:
- "Min (set (x # xs)) = foldr min xs x"
- by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
-
-lemma (in linorder) Max_fin_set_fold:
- "Max (set (x # xs)) = fold max xs x"
-proof -
- interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact ab_semigroup_idem_mult_max)
- show ?thesis
- by (simp add: Max_def fold1_set_fold del: set.simps)
-qed
-
-lemma (in linorder) Max_fin_set_foldr [code_unfold]:
- "Max (set (x # xs)) = foldr max xs x"
- by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
-
-lemma (in complete_lattice) Inf_set_fold:
- "Inf (set xs) = fold inf xs top"
-proof -
- interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact comp_fun_idem_inf)
- show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute)
-qed
-
-lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
- "Inf (set xs) = foldr inf xs top"
- by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
-
-lemma (in complete_lattice) Sup_set_fold:
- "Sup (set xs) = fold sup xs bot"
-proof -
- interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
- by (fact comp_fun_idem_sup)
- show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute)
-qed
-
-lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
- "Sup (set xs) = foldr sup xs bot"
- by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
-
-lemma (in complete_lattice) INFI_set_fold:
- "INFI (set xs) f = fold (inf \<circ> f) xs top"
- unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
-
-lemma (in complete_lattice) SUPR_set_fold:
- "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
- unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
-
-
-text {* @{text nth_map} *}
-
-definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "nth_map n f xs = (if n < length xs then
- take n xs @ [f (xs ! n)] @ drop (Suc n) xs
- else xs)"
-
-lemma nth_map_id:
- "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
- by (simp add: nth_map_def)
-
-lemma nth_map_unfold:
- "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
- by (simp add: nth_map_def)
-
-lemma nth_map_Nil [simp]:
- "nth_map n f [] = []"
- by (simp add: nth_map_def)
-
-lemma nth_map_zero [simp]:
- "nth_map 0 f (x # xs) = f x # xs"
- by (simp add: nth_map_def)
-
-lemma nth_map_Suc [simp]:
- "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
- by (simp add: nth_map_def)
-
-
-text {* monad operation *}
-
-definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
- "bind xs f = concat (map f xs)"
-
-lemma bind_simps [simp]:
- "bind [] f = []"
- "bind (x # xs) f = f x @ bind xs f"
- by (simp_all add: bind_def)
-
-end
--- a/src/HOL/More_Set.thy Mon Jan 09 18:32:56 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,299 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Relating (finite) sets and lists *}
-
-theory More_Set
-imports More_List
-begin
-
-lemma comp_fun_idem_remove:
- "comp_fun_idem Set.remove"
-proof -
- have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
- show ?thesis by (simp only: comp_fun_idem_remove rem)
-qed
-
-lemma minus_fold_remove:
- assumes "finite A"
- shows "B - A = Finite_Set.fold Set.remove B A"
-proof -
- have rem: "Set.remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
- show ?thesis by (simp only: rem assms minus_fold_remove)
-qed
-
-lemma bounded_Collect_code: (* FIXME delete candidate *)
- "{x \<in> A. P x} = Set.project P A"
- by (simp add: project_def)
-
-
-subsection {* Basic set operations *}
-
-lemma is_empty_set:
- "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
- by (simp add: Set.is_empty_def null_def)
-
-lemma empty_set:
- "{} = set []"
- by simp
-
-lemma insert_set_compl:
- "insert x (- set xs) = - set (removeAll x xs)"
- by auto
-
-lemma remove_set_compl:
- "Set.remove x (- set xs) = - set (List.insert x xs)"
- by (auto simp add: remove_def List.insert_def)
-
-lemma image_set:
- "image f (set xs) = set (map f xs)"
- by simp
-
-lemma project_set:
- "Set.project P (set xs) = set (filter P xs)"
- by (auto simp add: project_def)
-
-
-subsection {* Functorial set operations *}
-
-lemma union_set:
- "set xs \<union> A = fold Set.insert xs A"
-proof -
- interpret comp_fun_idem Set.insert
- by (fact comp_fun_idem_insert)
- show ?thesis by (simp add: union_fold_insert fold_set_fold)
-qed
-
-lemma union_set_foldr:
- "set xs \<union> A = foldr Set.insert xs A"
-proof -
- have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
- by auto
- then show ?thesis by (simp add: union_set foldr_fold)
-qed
-
-lemma minus_set:
- "A - set xs = fold Set.remove xs A"
-proof -
- interpret comp_fun_idem Set.remove
- by (fact comp_fun_idem_remove)
- show ?thesis
- by (simp add: minus_fold_remove [of _ A] fold_set_fold)
-qed
-
-lemma minus_set_foldr:
- "A - set xs = foldr Set.remove xs A"
-proof -
- have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y"
- by (auto simp add: remove_def)
- then show ?thesis by (simp add: minus_set foldr_fold)
-qed
-
-
-subsection {* Derived set operations *}
-
-lemma member:
- "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
- by simp
-
-lemma subset_eq:
- "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
- by (fact subset_eq)
-
-lemma subset:
- "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
- by (fact less_le_not_le)
-
-lemma set_eq:
- "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
- by (fact eq_iff)
-
-lemma inter:
- "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
- by (auto simp add: project_def)
-
-
-subsection {* Theorems on relations *}
-
-lemma product_code:
- "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
- by (auto simp add: Product_Type.product_def)
-
-lemma Id_on_set:
- "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
- by (auto simp add: Id_on_def)
-
-lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
- by (simp add: finite_trancl_ntranl)
-
-lemma set_rel_comp:
- "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
- by (auto simp add: Bex_def)
-
-lemma wf_set:
- "wf (set xs) = acyclic (set xs)"
- by (simp add: wf_iff_acyclic_if_finite)
-
-
-subsection {* Code generator setup *}
-
-definition coset :: "'a list \<Rightarrow> 'a set" where
- [simp]: "coset xs = - set xs"
-
-code_datatype set coset
-
-
-subsection {* Basic operations *}
-
-lemma [code]:
- "x \<in> set xs \<longleftrightarrow> List.member xs x"
- "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x"
- by (simp_all add: member_def)
-
-lemma [code_unfold]:
- "A = {} \<longleftrightarrow> Set.is_empty A"
- by (simp add: Set.is_empty_def)
-
-declare empty_set [code]
-
-declare is_empty_set [code]
-
-lemma UNIV_coset [code]:
- "UNIV = coset []"
- by simp
-
-lemma insert_code [code]:
- "insert x (set xs) = set (List.insert x xs)"
- "insert x (coset xs) = coset (removeAll x xs)"
- by simp_all
-
-lemma remove_code [code]:
- "Set.remove x (set xs) = set (removeAll x xs)"
- "Set.remove x (coset xs) = coset (List.insert x xs)"
- by (simp_all add: remove_def Compl_insert)
-
-declare image_set [code]
-
-declare project_set [code]
-
-lemma Ball_set [code]:
- "Ball (set xs) P \<longleftrightarrow> list_all P xs"
- by (simp add: list_all_iff)
-
-lemma Bex_set [code]:
- "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
- by (simp add: list_ex_iff)
-
-lemma card_set [code]:
- "card (set xs) = length (remdups xs)"
-proof -
- have "card (set (remdups xs)) = length (remdups xs)"
- by (rule distinct_card) simp
- then show ?thesis by simp
-qed
-
-
-subsection {* Derived operations *}
-
-declare subset_eq [code]
-
-declare subset [code]
-
-
-subsection {* Functorial operations *}
-
-lemma inter_code [code]:
- "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
- "A \<inter> coset xs = foldr Set.remove xs A"
- by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
-
-lemma subtract_code [code]:
- "A - set xs = foldr Set.remove xs A"
- "A - coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
- by (auto simp add: minus_set_foldr)
-
-lemma union_code [code]:
- "set xs \<union> A = foldr insert xs A"
- "coset xs \<union> A = coset (List.filter (\<lambda>x. x \<notin> A) xs)"
- by (auto simp add: union_set_foldr)
-
-definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
- [simp, code_abbrev]: "Inf = Complete_Lattices.Inf"
-
-hide_const (open) Inf
-
-definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
- [simp, code_abbrev]: "Sup = Complete_Lattices.Sup"
-
-hide_const (open) Sup
-
-lemma Inf_code [code]:
- "More_Set.Inf (set xs) = foldr inf xs top"
- "More_Set.Inf (coset []) = bot"
- by (simp_all add: Inf_set_foldr)
-
-lemma Sup_sup [code]:
- "More_Set.Sup (set xs) = foldr sup xs bot"
- "More_Set.Sup (coset []) = top"
- by (simp_all add: Sup_set_foldr)
-
-lemma INF_code [code]:
- "INFI (set xs) f = foldr (inf \<circ> f) xs top"
- by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map)
-
-lemma SUP_sup [code]:
- "SUPR (set xs) f = foldr (sup \<circ> f) xs bot"
- by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map)
-
-(* FIXME: better implement conversion by bisection *)
-
-lemma pred_of_set_fold_sup:
- assumes "finite A"
- shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs")
-proof (rule sym)
- interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
- by (fact comp_fun_idem_sup)
- from `finite A` show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI)
-qed
-
-lemma pred_of_set_set_fold_sup:
- "pred_of_set (set xs) = fold sup (map Predicate.single xs) bot"
-proof -
- interpret comp_fun_idem "sup :: 'a Predicate.pred \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a Predicate.pred"
- by (fact comp_fun_idem_sup)
- show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric])
-qed
-
-lemma pred_of_set_set_foldr_sup [code]:
- "pred_of_set (set xs) = foldr sup (map Predicate.single xs) bot"
- by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
-
-hide_const (open) coset
-
-
-subsection {* Operations on relations *}
-
-text {* Initially contributed by Tjark Weber. *}
-
-declare Domain_fst [code]
-
-declare Range_snd [code]
-
-declare trans_join [code]
-
-declare irrefl_distinct [code]
-
-declare trancl_set_ntrancl [code]
-
-declare acyclic_irrefl [code]
-
-declare product_code [code]
-
-declare Id_on_set [code]
-
-declare set_rel_comp [code]
-
-declare wf_set [code]
-
-end
-
--- a/src/HOL/Nominal/Examples/Standardization.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Nominal/Examples/Standardization.thy Mon Jan 09 18:33:55 2012 +0100
@@ -212,8 +212,8 @@
apply (erule allE, erule impE)
prefer 2
apply (erule allE, erule impE, rule refl, erule spec)
- apply simp
- apply (metis add_strict_increasing le_add1 length_pos_if_in_set listsum_foldl listsum_map_remove1 nat_add_commute)
+ apply simp
+ apply (clarsimp simp add: foldr_conv_foldl [symmetric] foldr_def fold_plus_listsum_rev listsum_map_remove1)
apply clarify
apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)")
prefer 2
--- a/src/HOL/Nominal/nominal_datatype.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Jan 09 18:33:55 2012 +0100
@@ -982,7 +982,7 @@
else foldr1 (HOLogic.mk_binop @{const_abbrev union}) (map supp args2)))))
(fn _ =>
simp_tac (HOL_basic_ss addsimps (supp_def ::
- Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
+ Un_assoc :: @{thm de_Morgan_conj} :: Collect_disj_eq :: finite_Un ::
Collect_False_empty :: finite_emptyI :: @{thms simp_thms} @
abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
in
@@ -1968,7 +1968,7 @@
end) context 1])) idxss) (ndescr ~~ rec_elims))
end));
- val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
+ val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
(* define primrec combinators *)
@@ -2011,7 +2011,7 @@
(augment_sort thy12 fs_cp_sort concl')
(fn {prems, ...} => EVERY
[rewrite_goals_tac reccomb_defs,
- rtac the1_equality 1,
+ rtac @{thm the1_equality} 1,
solve rec_unique_thms prems 1,
resolve_tac rec_intrs 1,
REPEAT (solve (prems @ rec_total_thms) prems 1)])
--- a/src/HOL/Product_Type.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Product_Type.thy Mon Jan 09 18:33:55 2012 +0100
@@ -893,11 +893,6 @@
hide_const (open) Times
-definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
- [code_abbrev]: "product A B = Sigma A (\<lambda>_. B)"
-
-hide_const (open) product
-
syntax
"_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
translations
@@ -1044,12 +1039,21 @@
lemma image_split_eq_Sigma:
"(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
-proof (safe intro!: imageI vimageI)
+proof (safe intro!: imageI)
fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A"
using * eq[symmetric] by auto
qed simp_all
+definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
+ [code_abbrev]: "product A B = A \<times> B"
+
+hide_const (open) product
+
+lemma member_product:
+ "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B"
+ by (simp add: product_def)
+
text {* The following @{const map_pair} lemmas are due to Joachim Breitner: *}
lemma map_pair_inj_on:
--- a/src/HOL/Prolog/prolog.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Prolog/prolog.ML Mon Jan 09 18:33:55 2012 +0100
@@ -63,9 +63,9 @@
|> Simplifier.set_mksimps (mksimps mksimps_pairs))
addsimps [
@{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
- imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
- imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
- imp_all]; (* "((!x. D) :- G) = (!x. D :- G)" *)
+ @{thm imp_conjL} RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
+ @{thm imp_conjR}, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
+ @{thm imp_all}]; (* "((!x. D) :- G) = (!x. D :- G)" *)
(*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
--- a/src/HOL/Quotient_Examples/FSet.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy Mon Jan 09 18:33:55 2012 +0100
@@ -247,7 +247,7 @@
and "x \<in> set xs"
shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
proof -
- from assms have "More_List.fold f (remdups xs) = More_List.fold f (remove1 x (remdups xs)) \<circ> f x"
+ from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \<circ> f x"
by (auto intro!: fold_remove1_split elim: rsp_foldE)
then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll)
qed
--- a/src/HOL/Quotient_Examples/Lift_RBT.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Mon Jan 09 18:33:55 2012 +0100
@@ -186,7 +186,7 @@
by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
lemma fold_fold:
- "fold f t = More_List.fold (prod_case f) (entries t)"
+ "fold f t = List.fold (prod_case f) (entries t)"
by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
lemma is_empty_empty [simp]:
--- a/src/HOL/Quotient_Examples/List_Quotient_Cset.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Quotient_Examples/List_Quotient_Cset.thy Mon Jan 09 18:33:55 2012 +0100
@@ -77,7 +77,7 @@
apply descending
apply (simp add: Set.remove_def)
apply descending
-by (simp add: remove_set_compl)
+by (auto simp add: set_eq_iff)
lemma insert_set [code]:
"Quotient_Cset.insert x (Quotient_Cset.set xs) = Quotient_Cset.set (List.insert x xs)"
@@ -92,7 +92,7 @@
lemma filter_set [code]:
"Quotient_Cset.filter P (Quotient_Cset.set xs) = Quotient_Cset.set (List.filter P xs)"
-by descending (simp add: project_set)
+by descending (simp add: set_eq_iff)
lemma forall_set [code]:
"Quotient_Cset.forall (Quotient_Cset.set xs) P \<longleftrightarrow> list_all P xs"
--- a/src/HOL/Relation.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Relation.thy Mon Jan 09 18:33:55 2012 +0100
@@ -275,7 +275,7 @@
subsection {* Transitivity *}
-lemma trans_join:
+lemma trans_join [code]:
"trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
by (auto simp add: trans_def)
@@ -300,7 +300,7 @@
subsection {* Irreflexivity *}
-lemma irrefl_distinct:
+lemma irrefl_distinct [code]:
"irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
by (auto simp add: irrefl_def)
@@ -395,7 +395,7 @@
"a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
by (iprover dest!: iffD1 [OF Domain_iff])
-lemma Domain_fst:
+lemma Domain_fst [code]:
"Domain r = fst ` r"
by (auto simp add: image_def Bex_def)
@@ -453,7 +453,7 @@
lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
-lemma Range_snd:
+lemma Range_snd [code]:
"Range r = snd ` r"
by (auto simp add: image_def Bex_def)
--- a/src/HOL/Set.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Set.thy Mon Jan 09 18:33:55 2012 +0100
@@ -256,7 +256,6 @@
print_translation {*
let
- val Type (set_type, _) = @{typ "'a set"}; (* FIXME 'a => bool (!?!) *)
val All_binder = Mixfix.binder_name @{const_syntax All};
val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
val impl = @{const_syntax HOL.implies};
@@ -275,14 +274,12 @@
then Syntax.const c $ Syntax_Trans.mark_bound v' $ n $ P else raise Match;
fun tr' q = (q,
- fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (T, _)),
+ fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (@{type_name set}, _)),
Const (c, _) $
(Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', _)) $ n) $ P] =>
- if T = set_type then
- (case AList.lookup (op =) trans (q, c, d) of
- NONE => raise Match
- | SOME l => mk v v' l n P)
- else raise Match
+ (case AList.lookup (op =) trans (q, c, d) of
+ NONE => raise Match
+ | SOME l => mk v v' l n P)
| _ => raise Match);
in
[tr' All_binder, tr' Ex_binder]
@@ -508,7 +505,7 @@
-- {* Classical elimination rule. *}
by (auto simp add: less_eq_set_def le_fun_def)
-lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
+lemma subset_eq [code, no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
by blast
@@ -525,6 +522,10 @@
lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
by (rule subsetD)
+lemma subset_not_subset_eq [code]:
+ "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
+ by (fact less_le_not_le)
+
lemma eq_mem_trans: "a=b ==> b \<in> A ==> a \<in> A"
by simp
@@ -833,7 +834,7 @@
thus ?R using `a\<noteq>b` by auto
qed
next
- assume ?R thus ?L by(auto split: if_splits)
+ assume ?R thus ?L by (auto split: if_splits)
qed
subsubsection {* Singletons, using insert *}
@@ -1796,7 +1797,7 @@
by (auto simp add: bind_def)
lemma empty_bind [simp]:
- "Set.bind {} B = {}"
+ "Set.bind {} f = {}"
by (simp add: bind_def)
lemma nonempty_bind_const:
@@ -1810,20 +1811,28 @@
subsubsection {* Operations for execution *}
definition is_empty :: "'a set \<Rightarrow> bool" where
- "is_empty A \<longleftrightarrow> A = {}"
+ [code_abbrev]: "is_empty A \<longleftrightarrow> A = {}"
hide_const (open) is_empty
definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "remove x A = A - {x}"
+ [code_abbrev]: "remove x A = A - {x}"
hide_const (open) remove
+lemma member_remove [simp]:
+ "x \<in> Set.remove y A \<longleftrightarrow> x \<in> A \<and> x \<noteq> y"
+ by (simp add: remove_def)
+
definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
[code_abbrev]: "project P A = {a \<in> A. P a}"
hide_const (open) project
+lemma member_project [simp]:
+ "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
+ by (simp add: project_def)
+
instantiation set :: (equal) equal
begin
@@ -1835,6 +1844,7 @@
end
+
text {* Misc *}
hide_const (open) member not_member
--- a/src/HOL/Tools/Datatype/datatype_case.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Mon Jan 09 18:33:55 2012 +0100
@@ -3,6 +3,16 @@
Author: Stefan Berghofer, TU Muenchen
Datatype package: nested case expressions on datatypes.
+
+TODO:
+ * Avoid fragile operations on syntax trees (with type constraints
+ getting in the way). Instead work with auxiliary "destructor"
+ constants in translations and introduce the actual case
+ combinators in a separate term check phase (similar to term
+ abbreviations).
+
+ * Avoid hard-wiring with datatype package. Instead provide generic
+ generic declarations of case splits based on an internal data slot.
*)
signature DATATYPE_CASE =
@@ -49,33 +59,41 @@
fun add_row_used ((prfx, pats), (tm, tag)) =
fold Term.add_free_names (tm :: pats @ map Free prfx);
-(*try to preserve names given by user*)
-fun default_names names ts =
- map (fn ("", Free (name', _)) => name' | (name, _) => name) (names ~~ ts);
+fun default_name name (t, cs) =
+ let
+ val name' = if name = "" then (case t of Free (name', _) => name' | _ => name) else name;
+ val cs' = if is_Free t then cs else filter_out Term_Position.is_position cs;
+ in (name, cs') end;
fun strip_constraints (Const (@{syntax_const "_constrain"}, _) $ t $ tT) =
strip_constraints t ||> cons tT
| strip_constraints t = (t, []);
-fun mk_fun_constrain tT t =
- Syntax.const @{syntax_const "_constrain"} $ t $
- (Syntax.const @{type_syntax fun} $ tT $ Syntax.const @{type_syntax dummy});
+fun constrain tT t = Syntax.const @{syntax_const "_constrain"} $ t $ tT;
+fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
(*Produce an instance of a constructor, plus fresh variables for its arguments.*)
fun fresh_constr ty_match ty_inst colty used c =
let
- val (_, Ty) = dest_Const c;
- val Ts = binder_types Ty;
+ val (_, T) = dest_Const c;
+ val Ts = binder_types T;
val names =
Name.variant_list used (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
- val ty = body_type Ty;
+ val ty = body_type T;
val ty_theta = ty_match ty colty
handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
val c' = ty_inst ty_theta c;
val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts);
in (c', gvars) end;
+fun strip_comb_positions tm =
+ let
+ fun result t ts = (Term_Position.strip_positions t, ts);
+ fun strip (t as Const (@{syntax_const "_constrain"}, _) $ _ $ _) ts = result t ts
+ | strip (f $ t) ts = strip f (t :: ts)
+ | strip t ts = result t ts;
+ in strip tm [] end;
(*Go through a list of rows and pick out the ones beginning with a
pattern with constructor = name.*)
@@ -83,15 +101,19 @@
let val k = length (binder_types T) in
fold (fn (row as ((prfx, p :: ps), rhs as (_, i))) =>
fn ((in_group, not_in_group), (names, cnstrts)) =>
- (case strip_comb p of
+ (case strip_comb_positions p of
(Const (name', _), args) =>
if name = name' then
if length args = k then
- let val (args', cnstrts') = split_list (map strip_constraints args) in
+ let
+ val constraints' = map strip_constraints args;
+ val (args', cnstrts') = split_list constraints';
+ val (names', cnstrts'') = split_list (map2 default_name names constraints');
+ in
((((prfx, args' @ ps), rhs) :: in_group, not_in_group),
- (default_names names args', map2 append cnstrts cnstrts'))
+ (names', map2 append cnstrts cnstrts''))
end
- else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ name, i)
+ else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ quote name, i)
else ((in_group, row :: not_in_group), (names, cnstrts))
| _ => raise CASE_ERROR ("Not a constructor pattern", i)))
rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
@@ -124,7 +146,7 @@
[((prfx, gvars @ map Free (xs ~~ Ts)),
(Const (@{const_syntax undefined}, res_ty), ~1))]
end
- else in_group
+ else in_group;
in
{constructor = c',
new_formals = gvars,
@@ -144,14 +166,14 @@
let
val get_info = Datatype_Data.info_of_constr_permissive (Proof_Context.theory_of ctxt);
- fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand_var_row", ~1)
+ fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1)
| expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
if is_Free p then
let
val used' = add_row_used row used;
fun expnd c =
let val capp = list_comb (fresh_constr ty_match ty_inst ty used' c)
- in ((prfx, capp :: ps), (subst_free [(p, capp)] rhs, tag)) end
+ in ((prfx, capp :: ps), (subst_free [(p, capp)] rhs, tag)) end;
in map expnd constructors end
else [row];
@@ -162,7 +184,8 @@
| mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row]
| mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
- (case Option.map (apfst head_of) (find_first (not o is_Free o fst) col0) of
+ (case Option.map (apfst (fst o strip_comb_positions))
+ (find_first (not o is_Free o fst) col0) of
NONE =>
let
val rows' = map (fn ((v, _), row) => row ||>
@@ -170,7 +193,7 @@
in mk us rows' end
| SOME (Const (cname, cT), i) =>
(case Option.map ty_info (get_info (cname, cT)) of
- NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
+ NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ quote cname, i)
| SOME {case_name, constructors} =>
let
val pty = body_type cT;
@@ -186,7 +209,7 @@
map2 (fn {new_formals, names, constraints, ...} =>
fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
Abs (if s = "" then name else s, T, abstract_over (x, t))
- |> fold mk_fun_constrain cnstrts) (new_formals ~~ names ~~ constraints))
+ |> fold constrain_Abs cnstrts) (new_formals ~~ names ~~ constraints))
subproblems dtrees;
val types = map type_of (case_functions @ [u]);
val case_const = Const (case_name, types ---> range_ty);
@@ -210,7 +233,7 @@
case_error (quote s ^ " occurs repeatedly in the pattern " ^
quote (Syntax.string_of_term ctxt pat))
else x :: xs)
- | _ => I) pat [];
+ | _ => I) (Term_Position.strip_positions pat) [];
fun gen_make_case ty_match ty_inst type_of ctxt config used x clauses =
let
@@ -293,8 +316,8 @@
in
make_case_untyped ctxt
(if err then Error else Warning) []
- (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
- (flat cnstrts) t) cases
+ (fold constrain (filter_out Term_Position.is_position (flat cnstrts)) t)
+ cases
end
| case_tr _ _ _ = case_error "case_tr";
@@ -432,7 +455,8 @@
| Const (s, _) => Syntax.const (Lexicon.mark_const s)
| t => t) pat $
map_aterms
- (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
+ (fn x as Free (s, T) =>
+ if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
| t => t) rhs
end;
in
--- a/src/HOL/Transitive_Closure.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Transitive_Closure.thy Mon Jan 09 18:33:55 2012 +0100
@@ -1047,7 +1047,7 @@
abbreviation acyclicP :: "('a => 'a => bool) => bool" where
"acyclicP r \<equiv> acyclic {(x, y). r x y}"
-lemma acyclic_irrefl:
+lemma acyclic_irrefl [code]:
"acyclic r \<longleftrightarrow> irrefl (r^+)"
by (simp add: acyclic_def irrefl_def)
--- a/src/HOL/Word/Tools/smt_word.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Word/Tools/smt_word.ML Mon Jan 09 18:33:55 2012 +0100
@@ -68,7 +68,7 @@
fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
fun add_word_fun f (t, n) =
- let val c as (m, _) = Term.dest_Const t
+ let val (m, _) = Term.dest_Const t
in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
fun hd2 xs = hd (tl xs)
--- a/src/HOL/Word/Word.thy Mon Jan 09 18:32:56 2012 +0100
+++ b/src/HOL/Word/Word.thy Mon Jan 09 18:33:55 2012 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/Word/Word.thy
- Author: Jeremy Dawson and Gerwin Klein, NICTA
+ Author: Jeremy Dawson and Gerwin Klein, NICTA
*)
header {* A type of finite bit strings *}
@@ -116,7 +116,8 @@
"word_int_case f w = f (uint w)"
translations
- "case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x"
+ "case x of XCONST of_int y => b" == "CONST word_int_case (%y. b) x"
+ "case x of (XCONST of_int :: 'a) y => b" => "CONST word_int_case (%y. b) x"
subsection {* Type-definition locale instantiations *}
@@ -1049,8 +1050,7 @@
unfolding word_less_def word_le_def by (simp add: less_le)
lemma signed_linorder: "class.linorder word_sle word_sless"
-proof
-qed (unfold word_sle_def word_sless_def, auto)
+ by default (unfold word_sle_def word_sless_def, auto)
interpretation signed: linorder "word_sle" "word_sless"
by (rule signed_linorder)
@@ -2505,7 +2505,7 @@
apply clarsimp
apply clarsimp
apply (drule word_gt_0 [THEN iffD1])
- apply (safe intro!: word_eqI bin_nth_lem ext)
+ apply (safe intro!: word_eqI bin_nth_lem)
apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
done
@@ -4111,26 +4111,21 @@
subsection {* Maximum machine word *}
lemma word_int_cases:
- "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len0 word) = word_of_int n; 0 \<le> n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
- \<Longrightarrow> P"
+ obtains n where "(x ::'a::len0 word) = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
lemma word_nat_cases [cases type: word]:
- "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len word) = of_nat n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
- \<Longrightarrow> P"
+ obtains n where "(x ::'a::len word) = of_nat n" and "n < 2^len_of TYPE('a)"
by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
-lemma max_word_eq:
- "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
+lemma max_word_eq: "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p)
-lemma max_word_max [simp,intro!]:
- "n \<le> max_word"
+lemma max_word_max [simp,intro!]: "n \<le> max_word"
by (cases n rule: word_int_cases)
(simp add: max_word_def word_le_def int_word_uint int_mod_eq')
-lemma word_of_int_2p_len:
- "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
+lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
by (subst word_uint.Abs_norm [symmetric])
(simp add: word_of_int_hom_syms)
@@ -4546,7 +4541,6 @@
use "~~/src/HOL/Word/Tools/smt_word.ML"
-
setup {* SMT_Word.setup *}
end
--- a/src/Pure/Isar/attrib.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/Isar/attrib.ML Mon Jan 09 18:33:55 2012 +0100
@@ -498,7 +498,6 @@
val _ = Context.>> (Context.map_theory
(register_config Ast.trace_raw #>
register_config Ast.stats_raw #>
- register_config Syntax.positions_raw #>
register_config Printer.show_brackets_raw #>
register_config Printer.show_sorts_raw #>
register_config Printer.show_types_raw #>
--- a/src/Pure/Isar/keyword.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/Isar/keyword.ML Mon Jan 09 18:33:55 2012 +0100
@@ -151,17 +151,17 @@
val keyword_statusN = "keyword_status";
-fun status_message s =
+fun status_message m s =
Position.setmp_thread_data Position.none
- (if print_mode_active keyword_statusN then Output.status else writeln) s;
+ (if print_mode_active keyword_statusN then Output.raw_message m else writeln) s;
fun keyword_status name =
- status_message (Markup.markup (Isabelle_Markup.keyword_decl name)
- ("Outer syntax keyword: " ^ quote name));
+ status_message (Isabelle_Markup.keyword_decl name)
+ ("Outer syntax keyword: " ^ quote name);
fun command_status (name, kind) =
- status_message (Markup.markup (Isabelle_Markup.command_decl name (kind_of kind))
- ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
+ status_message (Isabelle_Markup.command_decl name (kind_of kind))
+ ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")");
fun status () =
let val (keywords, commands) = CRITICAL (fn () =>
--- a/src/Pure/Isar/keyword.scala Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/Isar/keyword.scala Mon Jan 09 18:33:55 2012 +0100
@@ -54,26 +54,5 @@
Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
val improper = Set(THY_SCRIPT, PRF_SCRIPT)
-
-
- /* protocol messages */
-
- object Keyword_Decl {
- def unapply(msg: XML.Tree): Option[String] =
- msg match {
- case XML.Elem(Markup(Isabelle_Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) =>
- Some(name)
- case _ => None
- }
- }
-
- object Command_Decl {
- def unapply(msg: XML.Tree): Option[(String, String)] =
- msg match {
- case XML.Elem(Markup(Isabelle_Markup.COMMAND_DECL,
- List((Markup.NAME, name), (Markup.KIND, kind))), _) => Some((name, kind))
- case _ => None
- }
- }
}
--- a/src/Pure/PIDE/command.scala Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/PIDE/command.scala Mon Jan 09 18:33:55 2012 +0100
@@ -23,27 +23,20 @@
val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
val markup: Markup_Tree = Markup_Tree.empty)
{
- /* content */
-
- def add_status(st: Markup): State = copy(status = st :: status)
- def add_markup(m: Text.Markup): State = copy(markup = markup + m)
- def add_result(serial: Long, result: XML.Tree): State =
- copy(results = results + (serial -> result))
+ /* accumulate content */
- def root_info: Text.Markup =
- Text.Info(command.range,
- XML.Elem(Markup(Isabelle_Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
- def root_markup: Markup_Tree = markup + root_info
+ private def add_status(st: Markup): State = copy(status = st :: status)
+ private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
-
- /* message dispatch */
-
- def accumulate(message: XML.Elem): Command.State =
+ def + (message: XML.Elem): Command.State =
message match {
case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) =>
(this /: msgs)((state, msg) =>
msg match {
- case XML.Elem(markup, Nil) => state.add_status(markup)
+ case elem @ XML.Elem(markup, Nil) =>
+ val info: Text.Markup = Text.Info(command.range, elem)
+ state.add_status(markup).add_markup(info)
+
case _ => System.err.println("Ignored status message: " + msg); state
})
@@ -64,13 +57,13 @@
atts match {
case Isabelle_Markup.Serial(i) =>
val result = XML.Elem(Markup(name, Position.purge(atts)), body)
- val st0 = add_result(i, result)
+ val st0 = copy(results = results + (i -> result))
val st1 =
if (Protocol.is_tracing(message)) st0
else
(st0 /: Protocol.message_positions(command, message))(
(st, range) => st.add_markup(Text.Info(range, result)))
- val st2 = (st1 /: Protocol.message_reports(message))(_ accumulate _)
+ val st2 = (st1 /: Protocol.message_reports(message))(_ + _)
st2
case _ => System.err.println("Ignored message without serial number: " + message); this
}
--- a/src/Pure/PIDE/document.scala Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/PIDE/document.scala Mon Jan 09 18:33:55 2012 +0100
@@ -325,12 +325,12 @@
def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
execs.get(id) match {
case Some(st) =>
- val new_st = st.accumulate(message)
+ val new_st = st + message
(new_st, copy(execs = execs + (id -> new_st)))
case None =>
commands.get(id) match {
case Some(st) =>
- val new_st = st.accumulate(message)
+ val new_st = st + message
(new_st, copy(commands = commands + (id -> new_st)))
case None => fail
}
--- a/src/Pure/PIDE/isabelle_markup.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML Mon Jan 09 18:33:55 2012 +0100
@@ -66,8 +66,6 @@
val ML_antiquotationN: string
val doc_antiquotationN: string
val doc_antiquotation_optionN: string
- val keyword_declN: string val keyword_decl: string -> Markup.T
- val command_declN: string val command_decl: string -> string -> Markup.T
val keywordN: string val keyword: Markup.T
val operatorN: string val operator: Markup.T
val commandN: string val command: Markup.T
@@ -81,7 +79,6 @@
val command_spanN: string val command_span: string -> Markup.T
val ignored_spanN: string val ignored_span: Markup.T
val malformed_spanN: string val malformed_span: Markup.T
- val loaded_theoryN: string val loaded_theory: string -> Markup.T
val elapsedN: string
val cpuN: string
val gcN: string
@@ -100,11 +97,14 @@
val serialN: string
val legacyN: string val legacy: Markup.T
val promptN: string val prompt: Markup.T
- val readyN: string val ready: Markup.T
val reportN: string val report: Markup.T
val no_reportN: string val no_report: Markup.T
val badN: string val bad: Markup.T
val functionN: string
+ val ready: Properties.T
+ val loaded_theory: string -> Properties.T
+ val keyword_decl: string -> Properties.T
+ val command_decl: string -> string -> Properties.T
val assign_execs: Properties.T
val removed_versions: Properties.T
val invoke_scala: string -> string -> Properties.T
@@ -235,13 +235,6 @@
(* outer syntax *)
-val (keyword_declN, keyword_decl) = markup_string "keyword_decl" Markup.nameN;
-
-val command_declN = "command_decl";
-
-fun command_decl name kind : Markup.T =
- (command_declN, [(Markup.nameN, name), (Markup.kindN, kind)]);
-
val (keywordN, keyword) = markup_elem "keyword";
val (operatorN, operator) = markup_elem "operator";
val (commandN, command) = markup_elem "command";
@@ -260,11 +253,6 @@
val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
-(* theory loader *)
-
-val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" Markup.nameN;
-
-
(* timing *)
val timingN = "timing";
@@ -307,7 +295,6 @@
val (legacyN, legacy) = markup_elem "legacy";
val (promptN, prompt) = markup_elem "prompt";
-val (readyN, ready) = markup_elem "ready";
val (reportN, report) = markup_elem "report";
val (no_reportN, no_report) = markup_elem "no_report";
@@ -319,6 +306,14 @@
val functionN = "function"
+val ready = [(functionN, "ready")];
+
+fun loaded_theory name = [(functionN, "loaded_theory"), (Markup.nameN, name)];
+
+fun keyword_decl name = [(functionN, "keyword_decl"), (Markup.nameN, name)];
+fun command_decl name kind =
+ [(functionN, "command_decl"), (Markup.nameN, name), (Markup.kindN, kind)];
+
val assign_execs = [(functionN, "assign_execs")];
val removed_versions = [(functionN, "removed_versions")];
--- a/src/Pure/PIDE/isabelle_markup.scala Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala Mon Jan 09 18:33:55 2012 +0100
@@ -142,9 +142,6 @@
/* outer syntax */
- val KEYWORD_DECL = "keyword_decl"
- val COMMAND_DECL = "command_decl"
-
val KEYWORD = "keyword"
val OPERATOR = "operator"
val COMMAND = "command"
@@ -160,11 +157,6 @@
val MALFORMED_SPAN = "malformed_span"
- /* theory loader */
-
- val LOADED_THEORY = "loaded_theory"
-
-
/* timing */
val TIMING = "timing"
@@ -249,33 +241,57 @@
val BAD = "bad"
- val READY = "ready"
-
/* raw message functions */
val FUNCTION = "function"
val Function = new Properties.String(FUNCTION)
+ val Ready: Properties.T = List((FUNCTION, "ready"))
+
+ object Loaded_Theory
+ {
+ def unapply(props: Properties.T): Option[String] =
+ props match {
+ case List((FUNCTION, "loaded_theory"), (Markup.NAME, name)) => Some(name)
+ case _ => None
+ }
+ }
+
+ object Keyword_Decl
+ {
+ def unapply(props: Properties.T): Option[String] =
+ props match {
+ case List((FUNCTION, "keyword_decl"), (Markup.NAME, name)) => Some(name)
+ case _ => None
+ }
+ }
+ object Command_Decl
+ {
+ def unapply(props: Properties.T): Option[(String, String)] =
+ props match {
+ case List((FUNCTION, "command_decl"), (Markup.NAME, name), (Markup.KIND, kind)) =>
+ Some((name, kind))
+ case _ => None
+ }
+ }
+
val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
- val INVOKE_SCALA = "invoke_scala"
object Invoke_Scala
{
def unapply(props: Properties.T): Option[(String, String)] =
props match {
- case List((FUNCTION, INVOKE_SCALA), (Markup.NAME, name), (ID, id)) => Some((name, id))
+ case List((FUNCTION, "invoke_scala"), (Markup.NAME, name), (ID, id)) => Some((name, id))
case _ => None
}
}
-
- val CANCEL_SCALA = "cancel_scala"
object Cancel_Scala
{
def unapply(props: Properties.T): Option[String] =
props match {
- case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
+ case List((FUNCTION, "cancel_scala"), (ID, id)) => Some(id)
case _ => None
}
}
--- a/src/Pure/PIDE/protocol.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML Mon Jan 09 18:33:55 2012 +0100
@@ -8,16 +8,16 @@
struct
val _ =
- Isabelle_Process.add_command "Document.define_command"
+ Isabelle_Process.protocol_command "Document.define_command"
(fn [id, name, text] =>
Document.change_state (Document.define_command (Document.parse_id id) name text));
val _ =
- Isabelle_Process.add_command "Document.cancel_execution"
+ Isabelle_Process.protocol_command "Document.cancel_execution"
(fn [] => ignore (Document.cancel_execution (Document.state ())));
val _ =
- Isabelle_Process.add_command "Document.update_perspective"
+ Isabelle_Process.protocol_command "Document.update_perspective"
(fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
let
val old_id = Document.parse_id old_id_string;
@@ -33,7 +33,7 @@
end));
val _ =
- Isabelle_Process.add_command "Document.update"
+ Isabelle_Process.protocol_command "Document.update"
(fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
let
val old_id = Document.parse_id old_id_string;
@@ -66,7 +66,7 @@
in state2 end));
val _ =
- Isabelle_Process.add_command "Document.remove_versions"
+ Isabelle_Process.protocol_command "Document.remove_versions"
(fn [versions_yxml] => Document.change_state (fn state =>
let
val versions =
@@ -77,7 +77,7 @@
in state1 end));
val _ =
- Isabelle_Process.add_command "Document.invoke_scala"
+ Isabelle_Process.protocol_command "Document.invoke_scala"
(fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
end;
--- a/src/Pure/PIDE/protocol.scala Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Jan 09 18:33:55 2012 +0100
@@ -101,13 +101,6 @@
/* specific messages */
- def is_ready(msg: XML.Tree): Boolean =
- msg match {
- case XML.Elem(Markup(Isabelle_Markup.STATUS, _),
- List(XML.Elem(Markup(Isabelle_Markup.READY, _), _))) => true
- case _ => false
- }
-
def is_tracing(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
--- a/src/Pure/Syntax/syntax.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/Syntax/syntax.ML Mon Jan 09 18:33:55 2012 +0100
@@ -10,8 +10,6 @@
type operations
val install_operations: operations -> unit
val root: string Config.T
- val positions_raw: Config.raw
- val positions: bool Config.T
val ambiguity_enabled: bool Config.T
val ambiguity_level_raw: Config.raw
val ambiguity_level: int Config.T
@@ -159,9 +157,6 @@
val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
-val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
-val positions = Config.bool positions_raw;
-
val ambiguity_enabled =
Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
--- a/src/Pure/Syntax/syntax_phases.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Jan 09 18:33:55 2012 +0100
@@ -128,7 +128,7 @@
(* parsetree_to_ast *)
-fun parsetree_to_ast ctxt constrain_pos trf parsetree =
+fun parsetree_to_ast ctxt raw trf parsetree =
let
val reports = Unsynchronized.ref ([]: Position.report list);
fun report pos = Position.store_reports reports [pos];
@@ -154,10 +154,10 @@
val _ = report pos (markup_type ctxt) c;
in [Ast.Constant (Lexicon.mark_type c)] end
| asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
- if constrain_pos then
+ if raw then [ast_of pt]
+ else
[Ast.Appl [Ast.Constant "_constrain", ast_of pt,
Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
- else [ast_of pt]
| asts_of (Parser.Node (a, pts)) =
let
val _ = pts |> List.app
@@ -300,10 +300,9 @@
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))))
else ();
-
- val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
- val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos ast_tr;
- in map parsetree_to_ast pts end;
+ in
+ map (parsetree_to_ast ctxt raw ast_tr) pts
+ end;
fun parse_raw ctxt root input =
let
--- a/src/Pure/System/isabelle_process.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML Mon Jan 09 18:33:55 2012 +0100
@@ -18,8 +18,7 @@
signature ISABELLE_PROCESS =
sig
val is_active: unit -> bool
- val add_command: string -> (string list -> unit) -> unit
- val command: string -> string list -> unit
+ val protocol_command: string -> (string list -> unit) -> unit
val crashes: exn list Synchronized.var
val init_fifos: string -> string -> unit
val init_socket: string -> unit
@@ -38,7 +37,7 @@
val _ = Markup.add_mode isabelle_processN YXML.output_markup;
-(* commands *)
+(* protocol commands *)
local
@@ -47,16 +46,18 @@
in
-fun add_command name cmd =
+fun protocol_command name cmd =
Synchronized.change commands (fn cmds =>
(if not (Symtab.defined cmds name) then ()
else warning ("Redefining Isabelle process command " ^ quote name);
Symtab.update (name, cmd) cmds));
-fun command name args =
+fun run_command name args =
(case Symtab.lookup (Synchronized.value commands) name of
NONE => error ("Undefined Isabelle process command " ^ quote name)
- | SOME cmd => cmd args);
+ | SOME cmd =>
+ (Runtime.debugging cmd args handle exn =>
+ error ("Isabelle process protocol failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn)));
end;
@@ -145,11 +146,6 @@
NONE => raise Runtime.TERMINATE
| SOME line => map (read_chunk channel) (space_explode "," line));
-fun run_command name args =
- Runtime.debugging (command name) args
- handle exn =>
- error ("Isabelle process command failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn);
-
in
fun loop channel =
@@ -189,7 +185,7 @@
val _ = Keyword.status ();
val _ = Thy_Info.status ();
- val _ = Output.status (Markup.markup Isabelle_Markup.ready "process ready");
+ val _ = Output.raw_message Isabelle_Markup.ready "";
in loop channel end));
fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
--- a/src/Pure/System/isabelle_process.scala Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala Mon Jan 09 18:33:55 2012 +0100
@@ -58,8 +58,7 @@
def is_status = kind == Isabelle_Markup.STATUS
def is_report = kind == Isabelle_Markup.REPORT
def is_raw = kind == Isabelle_Markup.RAW
- def is_ready = Protocol.is_ready(message)
- def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
+ def is_syslog = is_init || is_exit || is_system || is_stderr
override def toString: String =
{
--- a/src/Pure/System/session.scala Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/System/session.scala Mon Jan 09 18:33:55 2012 +0100
@@ -56,7 +56,7 @@
val phase_changed = new Event_Bus[Session.Phase]
val syslog_messages = new Event_Bus[Isabelle_Process.Result]
val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
- val raw_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck
+ val protocol_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck
@@ -355,6 +355,7 @@
}
result.properties match {
+
case Position.Id(state_id) if !result.is_raw =>
try {
val st = global_state.change_yield(_.accumulate(state_id, result.message))
@@ -363,6 +364,7 @@
catch {
case _: Document.State.Fail => bad_result(result)
}
+
case Isabelle_Markup.Assign_Execs if result.is_raw =>
XML.content(result.body).mkString match {
case Protocol.Assign(id, assign) =>
@@ -376,6 +378,7 @@
if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
prune_next = System.currentTimeMillis() + prune_delay.ms
}
+
case Isabelle_Markup.Removed_Versions if result.is_raw =>
XML.content(result.body).mkString match {
case Protocol.Removed(removed) =>
@@ -383,35 +386,39 @@
catch { case _: Document.State.Fail => bad_result(result) }
case _ => bad_result(result)
}
+
case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw =>
Future.fork {
val arg = XML.content(result.body).mkString
val (tag, res) = Invoke_Scala.method(name, arg)
prover.get.invoke_scala(id, tag, res)
}
- case Isabelle_Markup.Cancel_Scala(id) =>
- System.err.println("cancel_scala " + id) // FIXME cancel JVM task
+
+ case Isabelle_Markup.Cancel_Scala(id) if result.is_raw =>
+ System.err.println("cancel_scala " + id) // FIXME actually cancel JVM task
+
+ case Isabelle_Markup.Ready if result.is_raw =>
+ // FIXME move to ML side (!?)
+ syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
+ syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
+ phase = Session.Ready
+
+ case Isabelle_Markup.Loaded_Theory(name) if result.is_raw =>
+ thy_load.register_thy(name)
+
+ case Isabelle_Markup.Command_Decl(name, kind) if result.is_raw =>
+ syntax += (name, kind)
+
+ case Isabelle_Markup.Keyword_Decl(name) if result.is_raw =>
+ syntax += name
+
case _ =>
if (result.is_syslog) {
reverse_syslog ::= result.message
- if (result.is_ready) {
- // FIXME move to ML side (!?)
- syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
- syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
- phase = Session.Ready
- }
- else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
+ if (result.is_exit && phase == Session.Startup) phase = Session.Failed
else if (result.is_exit) phase = Session.Inactive
}
else if (result.is_stdout) { }
- else if (result.is_status) {
- result.body match {
- case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
- case List(Keyword.Keyword_Decl(name)) => syntax += name
- case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
- case _ => bad_result(result)
- }
- }
else bad_result(result)
}
}
@@ -467,13 +474,13 @@
case Messages(msgs) =>
msgs foreach {
case input: Isabelle_Process.Input =>
- raw_messages.event(input)
+ protocol_messages.event(input)
case result: Isabelle_Process.Result =>
handle_result(result)
if (result.is_syslog) syslog_messages.event(result)
if (result.is_stdout || result.is_stderr) raw_output_messages.event(result)
- raw_messages.event(result)
+ protocol_messages.event(result)
}
case change: Change_Node
--- a/src/Pure/Thy/thy_info.ML Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/Thy/thy_info.ML Mon Jan 09 18:33:55 2012 +0100
@@ -89,7 +89,7 @@
fun get_names () = Graph.topological_order (get_thys ());
fun status () =
- List.app (Output.status o Markup.markup_only o Isabelle_Markup.loaded_theory) (get_names ());
+ List.app (fn name => Output.raw_message (Isabelle_Markup.loaded_theory name) "") (get_names ());
(* access thy *)
--- a/src/Pure/Thy/thy_info.scala Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Pure/Thy/thy_info.scala Mon Jan 09 18:33:55 2012 +0100
@@ -7,21 +7,6 @@
package isabelle
-object Thy_Info
-{
- /* protocol messages */
-
- object Loaded_Theory {
- def unapply(msg: XML.Tree): Option[String] =
- msg match {
- case XML.Elem(Markup(Isabelle_Markup.LOADED_THEORY, List((Markup.NAME, name))), _) =>
- Some(name)
- case _ => None
- }
- }
-}
-
-
class Thy_Info(thy_load: Thy_Load)
{
/* messages */
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Jan 09 18:33:55 2012 +0100
@@ -152,7 +152,7 @@
val root = data.root
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
- snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Markup) =>
+ snapshot.command_state(command).markup.swing_tree(root)((info: Text.Markup) =>
{
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')
--- a/src/Tools/jEdit/src/protocol_dockable.scala Mon Jan 09 18:32:56 2012 +0100
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Mon Jan 09 18:33:55 2012 +0100
@@ -39,6 +39,6 @@
}
}
- override def init() { Isabelle.session.raw_messages += main_actor }
- override def exit() { Isabelle.session.raw_messages -= main_actor }
+ override def init() { Isabelle.session.protocol_messages += main_actor }
+ override def exit() { Isabelle.session.protocol_messages -= main_actor }
}