23 May 2013 22:46

### fully automated methods(superposition etc.)

```It worked like a charm, thanks.

Are techniques used by fully automated systems(like the E-prover and
superposition) applicable to human-assisted systems, or do they not
really fit well with the kinds of proofs humans produce?

For example, in IsarMathLib there is a lemma, "A trivial fact:identity
is the only function from a singleton to itself,"  where it appears
that humans still have to type several lines of proof to get something
trivial.  Could "fully automated" techniques/systems simplify that?

Thanks again,
Reza.

```
23 May 2013 18:46

### prove set (tl L) ⊆ set L

```Hello!

how can i prove this result:

lemma "set (tl L) ⊆ set L"

Thank you!
```
23 May 2013 15:18

### Isabelle/HOL, the book

```Hi people,

I just discovered there exist a book for Isabelle/HOL at Amazon:

I searched for something similar about one year ago and found nothing at
that time, so that's a good news. However, as it's a bit expansive (my
average price range for books is in €15 to €25), I would like to know
about its content before any attempt to get it. I clicked on the cover
picture as it says “Click to look inside”, but nothing happened (no
preview).

So I would like to know if someone here already get that book and if it's
worth the price.

P.S. As a question aside, if there are exclusive contents in this book, is
there an electronic version planned? (may be an electronic version would
be more affordable and I'm planning to get an ebook reader sooner of later
this year).

--

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

```
22 May 2013 16:13

### THE-operator

```Hello,

i would like to prove the following:

( THE A. {a. f a = {c1, c2, c3}} = {a. f a = A}  )         =        {c1, c2, c3}

It may well be a 1 line proof but unfortunately im unfamiliar with substitution on THE-operator).

Many thanks!

```
22 May 2013 20:51

### SOME-operator

```
Hello,

is this lemma true?

lemma "Domain (SOME r. Domain r = {2,3}) = {2,3}"

if yes, how can it be proved?

Thank you!

```
22 May 2013 09:06

### I/O error after "Isabelle build -o browser_info -v -c -a"

```I have Ubuntu Linux 12.04 and downloaded Isabelle 2013 Feb.

I do this:
../Isabelle2013/bin/isabelle build -o browser_info -v -c -a

and everything seems fine.  I even get fine looking HTML pages in places
like
HOME/.isabelle/Isabelle2013/browser_info/FOL/FOL.html

But for ZF I get errors:
### I/O error:
/home/reza/.isabelle/Isabelle2013/browser_info/ZF/.session/entries (No
such file or directory)
### Browser info: failed to update session index of
"\$ISABELLE_BROWSER_INFO/ZF"

Thank you,
Reza.

```
22 May 2013 13:35

### Re: Partial functions

```
Hallo,

i want to create a datatype that allows me to write functions from a nat subset to another nat subset.
for example i wanna be able to write:

definition f: {1,2,3} => {4,5}
1 -->4,  2-->4, 3-->5

or another one:

definition g : {6,8} => {2,3,4}

So the thing i want to somehow parametrize is  "which subset of the nat im using each time as domain and range" ,

I thought about creating a new datatype :    'a nat
The problem with this is that 'a  is instantiated with datatypes, and not sets like {1,2,3}.

1.  Everytime i want declare a new function, i have to declare by "typedef" the nat subsets i want as domain and range

2.  definition f :  "nat => nat" where
"f x = (if x : {1,2,3} then ....  else undefined)

This second approach is bad, cause i dont want the domain to be decided as late as the second line of the
declaration, cause after this i want to be able to program a selector "domain f"
that returns me the domain of f, thats why i want the domain of f to be somehow incapsulated (parametrized) in
the first line "f: nat =>nat " so that i can use it later.

```

22 May 2013 21:37

### Set of functions

```Hello,

how do you denote the set of all functions from nat to nat?

what about the set of all partial functions from nat to nat?

Thank you!

```
22 May 2013 19:16

### Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide

```Dear Isabelle community,

I am currently working with lists constructed from finite sets, and I'm
missing the following two lemmas that would really help me to get my
work done.  At the moment my Isabelle experience is not sufficient for
proving them myself, plus I think it would make sense if they were part
of the library (List.thy).

lemma sorted_list_of_set_not_empty [simp] :
assumes "finite S" and "S ≠ {}"
shows "sorted_list_of_set S ≠ []"
sorry

lemma sorted_list_of_set_distinct [simp] :
shows "distinct (sorted_list_of_set S)"
sorry

Would any of the developers feel up to proving them, or alternatively
teaching me how to do it?

BTW, for my work I actually don't need these lists-from-sets to be
_sorted_.  However sorted_list_of_set is the only result that

find_consts "'a set ⇒ 'a list"

gives me.  Efficient computation is not yet that crucial for my work,
but would it be possible to provide a list-from-set constructor that
does not guarantee sorting?  I mean something that simply rearranges the
internal data structure of a finite set (which is not guaranteed to be
sorted either) into a list.
```

22 May 2013 16:12

### Re: Want to use Rep_Integ or lifting after [quot_del] in Int.thy

```On Wed, May 22, 2013 at 2:45 PM, Christoph LANGE <
math.semantic.web@...> wrote:

> 2013-05-22 14:26 Lawrence Paulson:
> > Coq and Isabelle/HOL are proof assistants, not programming languages. I
> can't imagine what gave you that idea. In Coq and Isabelle/HOL you write
> specifications, not code.
>
> Well, but there _is_ a notion of "programming" in Isabelle, given that
> it is based on a functional programming language, isn't it?

I would not put it that way.
Both Isabelle/HOL and <your favourite functional programming language> are
based on some flavour of lambda calculus. That's the connection.
However, there is no evaluation strategy specified for Isabelle/HOL terms,
and several constants don't have reducible definitions.
It's possible (and even common) to write uncomputable specifications in HOL
whereas you can't write anything uncomputable in a programming language.

>  I recall
> this earlier discussion on the title of the "programming and proving"
> tutorial:
>
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/msg00148.html
>
> Cheers,
>
> Christoph
>
> --
```

22 May 2013 05:06

### LFMTP'13: Logical Frameworks and Meta-Languages (CFP)

```=====================================================

ACM SIGPLAN International Workshop on Logical Frameworks
and Meta-Languages: Theory and Practice (LFMTP'13)

http://complogic.cs.mcgill.ca/lfmtp13

23 September, 2013 Boston, USA

Co-located with with ICFP'13

CALL FOR PAPERS
=====================================================

IMPORTANT DATES

Paper submission:        June 14, 2013
Final versions due:       July 18, 2013

=====================================================

Logical frameworks and meta-languages form a common substrate for
representing, implementing, and reasoning about a wide variety of
deductive systems of interest in logic and computer science. Their
design and implementation on the one hand and their use in reasoning
tasks ranging from the correctness of software to the properties of
formal computational systems on the other hand have been the focus of
considerable research over the last two decades. This workshop will
bring together designers, implementors, and practitioners to discuss
```