[isabelle-dev] HOL Importer failure

[Florian Haftmann]

> I have tried funny things like
> 
>> definition even :: "nat ⇒ bool"
>> where
>>   "even = Parity.even"
>>
>> lemma EVEN [import_const "EVEN" : even]:
>>   "even (id 0∷nat) ⟷ True ∧ (∀n. even (Suc n) ⟷ ¬ even n)"
>>   by (simp add: even_def)

After a second careful look I came up with the solution attached.

I do not remember what went wrong when I tried this first.  Maybe a
simple typo.

I will take care for this patch ASAP.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
# HG changeset patch
# Parent c78d35ec6bb0f0af5e9dc955bd724160bb05d351
explicit definition restores HOL Light import after cb9d84d3e7f2

diff -r c78d35ec6bb0 -r 24ff52315d01 src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Thu Oct 23 14:14:54 2014 +0200
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Thu Oct 23 14:40:29 2014 +0200
@@ -181,9 +181,13 @@
   "min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
   by (auto simp add: min.absorb_iff1 fun_eq_iff)
 
+definition even
+where
+  "even = Parity.even"
+  
 lemma EVEN[import_const "EVEN" : even]:
   "even (id 0\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
-  by simp
+  by (simp add: even_def)
 
 lemma SUB[import_const "-" : minus]:
   "(\<forall>m\<Colon>nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))"
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141023/078644d0/attachment.sig>