*To*: Brendan.Mahony at dsto.defence.gov.au*Subject*: Re: [isabelle] Monotonic operators and calculational reasoning*From*: nipkow at in.tum.de*Date*: Mon, 3 Apr 2006 19:34:48 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4348CF31-3ECE-4D4C-BE10-5F02135EEE4B@dsto.defence.gov.au> (message from Brendan Mahony on Mon, 3 Apr 2006 14:27:09 +0930)*References*: <4348CF31-3ECE-4D4C-BE10-5F02135EEE4B@dsto.defence.gov.au>

have "(1::nat) < 3" by (auto) also have "(3::nat) + 1 < 5" by (auto) You did exactly the right thing. calculation: (!!x y. x < y ==> x + 1 < y + 1) ==> 1 + 1 < 5 As did Isabelle. The principle here is that the monotonicity assumptions that arise in your calculational proof are carried around, accumulate, and get discharged at the end. Thus you cannot simply say finally have "1+1 < (5::nat)" . but need to do something like finally have "1+1 < (5::nat)" by (blast intro:add_less_mono1) There may be slightly slicker proof patters. Tobias

**References**:**[isabelle] Monotonic operators and calculational reasoning***From:*Brendan Mahony

- Previous by Date: [isabelle] [CfP] Mathematical User Interfaces 2006 (MathUI06)
- Next by Date: [isabelle] proof-compat file error
- Previous by Thread: Re: [isabelle] Monotonic operators and calculational reasoning
- Next by Thread: [isabelle] [CfP] Mathematical User Interfaces 2006 (MathUI06)
- Cl-isabelle-users April 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list