summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Wed, 11 Jun 2014 11:28:46 +0200 | |

changeset 57214 | c4986877deea |

parent 57213 | 9daec42f6784 |

child 57215 | 6fc0e3d4e1e5 |

adapted SMT examples to new, corrected handling of 'typedef'

--- 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 *}