Re: [isabelle-dev] Explicit representation of multisets
> but this leads to the rather lengthy "insert_mset x M" as opposed to the
> current "{#x#} + M". This would come up in all inductive proofs. If we want
> to mimic sets, it actually seems unavoidable...
With completion, it might actually be easier to type "insert_mset x M" than
"{#x#} + M". (The former is visually longer, for sure.)
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Syntax for lattice operations?
On 10/03/2016 11:00, Florian Haftmann wrote: Hi all, traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been kept in a separate library theory, to allow use of that quite generic notation for unforeseen applications. Meanwhile however all those operations to which that syntax is attached to are members of syntactic type classes. It could be worth to attempt to make that syntax standard, using funny subscripts or similar for the more exotic cases. Florian, what are the more exotic cases? Tobias Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Explicit representation of multisets
Although I suggested we do this, and still think logically it is the right thing
to do, I see one issue, the naming of insert#. The canonical name is
insert_mset, but this leads to the rather lengthy "insert_mset x M" as opposed
to the current "{#x#} + M". This would come up in all inductive proofs. If we
want to mimic sets, it actually seems unavoidable...
Tobias
On 10/03/2016 10:53, Florian Haftmann wrote:
Hi all,
in recent private discussion the question was raised whether the
explicit representation of multisets should follow that of sets.
For sets, we have:
{a, b, c} = insert a (insert b (insert c empty))
For multisets, we currently have:
{#a, b, c#} = single a + single b + single c
But the following would also be possible:
{#a, b, c#} = insert# a (insert# b (insert# c empty#))
Is there any evidence that we should not attempt this?
Cheers,
Florian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sketch for generic interval notation [_..<_] / [_.._]
Hi all,
the attached patches (based on f26dc26f2161) sketch how a generic
interval [_..<_] / [_.._] could look like in List.thy.
Key points:
* The required logical properties are obtained by a specialization of
linordered_semidom with
a <= b <--> (EX n. b = a + of_nat n)"
This avoids introducing yet another auxiliary operation like succ etc.
I am still in search for a better name than pointed_linordered_semidom,
though.
* nat and int are instances of pointed_linordered_semidom.
* "finite {a.. nat set => 'a list" where
-"sublist xs A = map fst (filter (\p. snd p \ A) (zip xs [0.. 'a list list" where
-"sublists [] = [[]]" |
-"sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
-
primrec n_lists :: "nat \ 'a list \ 'a list list" where
"n_lists 0 xs = [[]]" |
"n_lists (Suc n) xs = concat (map (\ys. map (\y. y # ys) xs)
(n_lists n xs))"
@@ -280,7 +266,6 @@
@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
@{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 "enumerate 3 [a,b,c] = [(3,a),(4,b),(5,c)]" by normalization}\\
@{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by
simp}\\
@{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d],
[b,c,e]]" by simp}\\
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
@@ -306,13 +291,10 @@
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
-@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
-@{lemma "sublists [a,b] = [[a, b], [a], [b], []]" by simp}\\
@{lemma "List.n_lists 2 [a,b,c] = [[a, a], [b, a], [c, a], [a, b], [b, b], [c,
b], [a, c], [b, c], [c, c]]" by (simp add: eval_nat_numeral)}\\
@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add: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)}
\end{tabular}}
\caption{Characteristic examples}
\label{fig:Characteristic}
@@ -1290,9 +1272,6 @@
lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \ P x}"
by (induct xs) auto
-lemma set_upt [simp]: "set[i.. [i..
