[isabelle-dev] Float

[Makarius]

On Mon, 14 Nov 2011, Johannes Hölzl wrote:

> Am Montag, den 14.11.2011, 21:05 +0100 schrieb Alexander Krauss:
>> On 11/14/2011 08:43 PM, Johannes Hölzl wrote:
>> > Am Montag, den 14.11.2011, 19:27 +0100 schrieb Florian Haftmann:
>> >> Hi Johannes,
>> >>
>> >> two remarks:
>> >>
>> >> * http://isabelle.in.tum.de/reports/Isabelle/rev/e828ccc5c110
>> >>
>> >> With `notepad` you can prove everything without a trace in theory, which
>> >> eliminates the need for fiddling around with quick_and_dirty.
>> >
>> > I want to enforce that the user needs to activate quick_and_dirty in
>> > ROOT.ML, to remind him that there is something dirty.
>> 
>> This is rather non-standard and also breaks the test, cf.
>> 
>> http://isabelle.in.tum.de/reports/Isabelle/report/d6e6227d86634c02890a3e60e508abc3
>> 
>> (Tests are run without quick_and_dirty, and rightfully so.)
>
> Oh, I didn't look at that. I removed the check now.

You really have to run a full "isabelle makeall all" before pushing 
anything.  Otherwise it wastes other people's time unnecessarily.


>> lemma "False" sorry is indeed a strange kind of markup...
>
> Well False is proven anyway

You probably mean this one:
http://isabelle.in.tum.de/reports/Isabelle/diff/34d07cf7d207/src/HOL/Library/Code_Real_Approx_By_Float.thy#l1.139

That is a slightly different False theorem, since the kernel adds an 
official oracle tag, which can be seen like this

...

lemma a: "False"
proof-
   have "cos(pi/2) = 0" by(rule cos_pi_half)
   moreover have "cos(pi/2) ≠ 0" by eval
   ultimately show "False" by blast
qed

ML {* Thm.status_of @{thm a} *}

val it = {failed = false, oracle = true, unfinished = false}: {failed: 
bool, oracle: bool, unfinished: bool}

ML {* Proofterm.all_oracles_of (Thm.proof_body_of @{thm a}) *}

val it = [("Code_Generator.holds_by_evaluation", Const ("dummy_pattern", 
"_"))]: Proofterm.oracle list


Nonetheless, I agree with Florian that regular Library stuff should not 
make it easy to get wrong oracular results.


> and it is a easy check for quick_and_dirty.

That is actually not so easy.  Since it is an old-style global reference 
it depends on many side-conditions what it value is in a certain 
situation.  I still need to find ways to handle "session parameters" in a 
robust manner.  Old-style ROOT.ML is a bit too crude for that in the 
general situation, i.e. interaction vs. batch mode.


 	Makarius