headers
Reza Roboubi | 23 May 2013 22:46
Picon

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.
Permalink | Reply | 0 comments |
headers
Roger H. | 23 May 2013 18:46
Picon
Favicon

prove set (tl L) ⊆ set L

Hello!


how can i prove this result:


lemma "set (tl L) ⊆ set L"


Thank you!
Permalink | Reply | 4 comments |
headers
Yannick Duchêne (Hibou57 | 23 May 2013 15:18
Picon
Favicon

Isabelle/HOL, the book

Hi people,

I just discovered there exist a book for Isabelle/HOL at Amazon:
http://www.amazon.com/gp/reader/3540433767/ref=sib_dp_ptu/182-9131467-6281732

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.

Thanks for any advices.

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
Permalink | Reply | 3 comments |
headers
Roger H. | 22 May 2013 16:13
Picon
Favicon

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!
Permalink | Reply | 1 comment |
headers
Roger H. | 22 May 2013 20:51
Picon
Favicon

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!
Permalink | Reply | 4 comments |
headers
Reza Roboubi | 22 May 2013 09:06
Picon

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"

Can you help please.

Thank you,
Reza.
Permalink | Reply | 3 comments |
headers
Roger H. | 22 May 2013 13:35
Picon
Favicon

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}.

Following solutions are bad:

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.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Roger H. | 22 May 2013 21:37
Picon
Favicon

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!
Permalink | Reply | 2 comments |
headers
Christoph LANGE | 22 May 2013 19:16
Picon

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.
(Continue reading)

Permalink | Reply | 8 comments |
headers
Ramana Kumar | 22 May 2013 16:12
Picon
Picon
Favicon

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
>
> --
(Continue reading)

Permalink | Reply | 0 comments |
headers
Brigitte Pientka | 22 May 2013 05:06
Picon
Favicon

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
Author notification:        July 7, 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
(Continue reading)

Permalink | Reply | 0 comments |

Gmane