# HG changeset patch
# User blanchet
# Date 1402478926 -7200
# Node ID c4986877deea27ea34901f497339723986629dd6
# Parent  9daec42f67842245189cd50f9c96753afe311db5
adapted SMT examples to new, corrected handling of 'typedef'

diff -r 9daec42f6784 -r c4986877deea src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Jun 11 11:28:46 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Jun 11 11:28:46 2014 +0200
@@ -730,28 +730,18 @@
 
 subsubsection {* Type definitions *}
 
-definition "three = {1, 2, 3::int}"
-
-typedef three = three
-  unfolding three_def by auto
+typedef int' = "UNIV::int set" by (rule UNIV_witness)
 
-definition n1 where "n1 = Abs_three 1"
-definition n2 where "n2 = Abs_three 2"
-definition n3 where "n3 = Abs_three 3"
-definition nplus where "nplus n m = Abs_three (Rep_three n + Rep_three m)"
-
-lemma three_def': "(n \<in> three) = (n = 1 \<or> n = 2 \<or> n = 3)"
-  by (auto simp add: three_def)
+definition n0 where "n0 = Abs_int' 0"
+definition n1 where "n1 = Abs_int' 1"
+definition n2 where "n2 = Abs_int' 2"
+definition plus' where "plus' n m = Abs_int' (Rep_int' n + Rep_int' m)"
 
 lemma
-  "n1 = n1"
-  "n2 = n2"
-  "n1 \<noteq> n2"
-  "nplus n1 n1 = n2"
-  "nplus n1 n2 = n3"
-  using n1_def n2_def n3_def nplus_def
-  using three_def' Rep_three Abs_three_inverse
-  by smt2+
+  "n0 \<noteq> n1"
+  "plus' n1 n1 = n2"
+  "plus' n0 n2 = n2"
+  by (smt2 n0_def n1_def n2_def plus'_def Abs_int'_inverse Rep_int'_inverse UNIV_I)+
 
 
 subsection {* With support by the SMT solver (but without proofs) *}
@@ -873,14 +863,11 @@
 subsubsection {* Type definitions *}
 
 lemma
-  "n1 = n1"
-  "n2 = n2"
-  "n1 \<noteq> n2"
-  "nplus n1 n1 = n2"
-  "nplus n1 n2 = n3"
-  using n1_def n2_def n3_def nplus_def
+  "n0 \<noteq> n1"
+  "plus' n1 n1 = n2"
+  "plus' n0 n2 = n2"
   using [[smt2_oracle, z3_new_extensions]]
-  by smt2+
+  by (smt2 n0_def n1_def n2_def plus'_def)+
 
 
 section {* Function updates *}