Re: [isabelle-dev] [isabelle] Code_Abstract_Nat raises exception for a variable with name g
Hi Andreas, see now http://isabelle.in.tum.de/repos/isabelle/rev/91f9e4148460. Despite the ambitious commit message, for economic reasons I did not attempt to modernize the whole preprocessor but restricted myself to low-level tinkering with maxidx. Cheers, Florian On 18.06.2014 23:19, Florian Haftmann wrote: Hi Andreas, thanks for reporting this. The attached patch attempts to get this correct. Due to the current breakdowns I have not yet been able to test or push it. Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JinjaThreads CYCLES-Exception at export-code
See now http://isabelle.in.tum.de/repos/isabelle/rev/47c8475e7864. Interesting to see how bad dynamic typing actually is… Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Code preprocessor tracing
Hi Andreas, with http://isabelle.in.tum.de/repos/isabelle/rev/020cea57eaa4 I have provided very basic means to trace the code preprocessor. Alas, I only dimly remember what your real requirements are, so feel free to comment on it. Anyway, it is a starting point. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Product on lists
The attached patches provide product on lists, where as much of the
development is shared with sums on lists (similar to products and sums
on sets).
I am reluctant to push such a massive extension so short before a
release without having it exposed to critical eyes. For my part I do
not see much pressure to pursue it by now.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
# HG changeset patch
# Parent d8a8a6b10f617f99e8041a2e2377a4f11015f1ac
separated listsum material
diff -r d8a8a6b10f61 src/HOL/Groups_List.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +
+++ b/src/HOL/Groups_List.thy Sat Jun 28 21:30:01 2014 +0200
@@ -0,0 +1,212 @@
+
+(* Author: Tobias Nipkow, TU Muenchen *)
+
+header {* Summation over lists *}
+
+theory Groups_List
+imports List
+begin
+
+definition (in monoid_add) listsum :: 'a list \Rightarrow 'a where
+listsum xs = foldr plus xs 0
+
+subsubsection {* List summation: @{const listsum} and @{text\Sum}*}
+
+lemma (in monoid_add) listsum_simps [simp]:
+ listsum [] = 0
+ listsum (x # xs) = x + listsum xs
+ by (simp_all add: listsum_def)
+
+lemma (in monoid_add) listsum_append [simp]:
+ listsum (xs @ ys) = listsum xs + listsum ys
+ by (induct xs) (simp_all add: add.assoc)
+
+lemma (in comm_monoid_add) listsum_rev [simp]:
+ listsum (rev xs) = listsum xs
+ by (simp add: listsum_def foldr_fold 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_conv_fold)
+ 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
+
+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)
+ \Sumx\leftarrowxs. 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))
+ by (induct xs) (auto simp add: ac_simps)
+
+lemma (in monoid_add) size_list_conv_listsum:
+ size_list f xs = listsum (map f xs) + size xs
+ by (induct xs) auto
+
+lemma (in monoid_add) length_concat:
+ length (concat xss) = listsum (map length xss)
+ by (induct xss) simp_all
+
+lemma (in monoid_add) length_product_lists:
+ length (product_lists xss) = foldr op * (map length xss) 1
+proof (induct xss)
+ case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat
o_def)
+qed simp
+
+lemma (in monoid_add) listsum_map_filter:
+ assumes \Andx. x \in set xs \Longrightarrow \not P x
\Longrightarrow f x = 0
+ shows listsum (map f (filter P xs)) = listsum (map f xs)
+ using assms by (induct xs) auto
+
+lemma (in comm_monoid_add) distinct_listsum_conv_Setsum:
+ distinct xs \Longrightarrow listsum xs = Setsum (set xs)
+ by (induct xs) simp_all
+
+lemma listsum_eq_0_nat_iff_nat [simp]:
+ listsum ns = (0::nat) \longleftrightarrow (\foralln \in set ns. n =
0)
+ by (induct ns) simp_all
+
+lemma member_le_listsum_nat:
+ (n :: nat) \in set ns \Longrightarrow n \le listsum ns
+ by (induct ns) auto
+
+lemma elem_le_listsum_nat:
+ k size ns \Longrightarrow ns ! k \le listsum (ns::nat list)
+ by (rule member_le_listsum_nat) simp
+
+lemma listsum_update_nat:
+ k size ns \Longrightarrow listsum (ns[k := (n::nat)]) = listsum ns + n
- ns ! k
+apply(induct ns arbitrary:k)
+ apply (auto split:nat.split)
+apply(drule elem_le_listsum_nat)
+apply arith
+done
+
+lemma (in monoid_add) listsum_triv:
+ (\Sumx\leftarrowxs. r) = of_nat (length xs) * r
+ by (induct xs) (simp_all add: distrib_right)
+
+lemma (in monoid_add) listsum_0 [simp]:
+ (\Sumx\leftarrowxs. 0) = 0
+ by (induct xs) (simp_all add: distrib_right)
+
+text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
+lemma (in ab_group_add) uminus_listsum_map:
+ - listsum (map f xs) = listsum (map (uminus \circ f) xs)
+ by (induct xs) simp_all
+
+lemma (in comm_monoid_add) listsum_addf:
+ (\Sumx\leftarrowxs. f x + g x) = listsum (map f xs) + listsum (map g
xs)
+ by (induct xs) (simp_all add: algebra_simps)
+
+lemma (in ab_group_add) listsum_subtractf:
+ (\Sumx\leftarrowxs. f x - g x) = listsum (map f xs) - listsum (map g
xs)
+ by (induct xs) (simp_all add: algebra_simps)
+
+lemma (in semiring_0) listsum_const_mult:
+
Re: [isabelle-dev] JEdit FAILED
On 28.06.2014 17:24, Makarius wrote: On Sat, 28 Jun 2014, Makarius wrote: On Sat, 28 Jun 2014, Florian Haftmann wrote: suggests that something is bad with $JEDIT_HOME in the mira build environment. JEDIT_HOME is a normal Isabelle setting, provided by the etc/settings of that component within Isabelle. So it should normally be there, although I don't understand the mira setup. Another guess: Isabelle/jEdit is really missing, because of a lacking isabelle jedit -b that is done in regular makedist (e.g. in isatest). mira just executes isabelle build -s -v with job specific options (can be seen in Admin/mira.py). If isabelle jedit -b is a necessary step to setup a fresh Isabelle installation, I can add that to the setup script. BTW: Admin/mira.py is the Isabelle specific part of the mira setup. Unfortunately, the version of the script used is not the one for the version which is tested, but the one which is current on mira startup. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
