Camelia, the Perl 6 bug

IRC log for #isabelle, 2011-11-04

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
15:59 phimuemue_ joined #isabelle
16:00 phimuemue_ hi
16:00 phimuemue_ can somebody tell me why the following does not work:
16:00 phimuemue_ definition ble :: "aexp => aexp => bexp" where
16:00 phimuemue_ "ble a b = Not (Less b a)"
16:01 phimuemue_ lemma "ble a b = Not (Less b a)"
16:01 phimuemue_ apply(auto)
16:01 phimuemue_ ...
16:01 phimuemue_ it seems that isabelle is kinda not able to do simplifications on definitions.
16:01 phimuemue_ is this correct?
17:50 int-e try (simp add: ble.simps) or (auto simp: ble.simps)
17:50 int-e err
17:50 int-e not ble.simps but ble_def since it's a definition.
17:51 int-e (*.simps rules are generated for fun/function)

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary