src/HOL/ex/Eval_Examples.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Eval_Examples.thy	Tue Jun 05 22:46:55 2007 +0200
@@ -0,0 +1,38 @@
+(*  ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Small examples for evaluation mechanisms *}
+
+theory Eval_Examples
+imports Eval
+begin
+
+text {* evaluation oracle *}
+
+lemma "True \<or> False" by eval
+lemma "\<not> (Suc 0 = Suc 1)" by eval
+
+text {* term evaluation *}
+
+value (overloaded) "(Suc 2 + 1) * 4"
+value (overloaded) "(Suc 2 + 1) * 4"
+value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
+value (overloaded) "[]::nat list"
+value (overloaded) "fst ([]::nat list, Suc 0) = []"
+value (overloaded) "nat 100"
+value (overloaded) "[(nat 100, ())]"
+value (overloaded) "int 10 \<le> 12"
+
+text {* a fancy datatype *}
+
+datatype ('a, 'b) bair =
+    Bair "'a\<Colon>order" 'b
+  | Shift "('a, 'b) cair"
+  | Dummy unit
+and ('a, 'b) cair =
+    Cair 'a 'b
+
+value (overloaded) "Shift (Cair (4::nat) [Suc 0])"
+
+end