src/HOL/SMT_Examples/SMT_Tests.thy

 (*  Title:      HOL/SMT_Examples/SMT_Tests.thy
     Author:     Sascha Boehme, TU Muenchen
 *)
 
-section {* Tests for the SMT binding *}
+section \<open>Tests for the SMT binding\<close>
 
 theory SMT_Tests
 imports Complex_Main
 begin
 
 smt_status
 
-text {* Most examples are taken from various Isabelle theories and from HOL4. *}
-
-
-section {* Propositional logic *}
+text \<open>Most examples are taken from various Isabelle theories and from HOL4.\<close>
+
+
+section \<open>Propositional logic\<close>
 
 lemma
   "True"
   "\<not> False"
   "\<not> \<not> True"

   "case \<not> P of True \<Rightarrow> \<not> P | False \<Rightarrow> P"
   "case P of True \<Rightarrow> (Q \<longrightarrow> P) | False \<Rightarrow> (P \<longrightarrow> Q)"
   by smt+
 
 
-section {* First-order logic with equality *}
+section \<open>First-order logic with equality\<close>
 
 lemma
   "x = x"
   "x = y \<longrightarrow> y = x"
   "x = y \<and> y = z \<longrightarrow> x = z"

   "(\<forall>x y z. f x y = f x z \<longrightarrow> y = z) \<and> b \<noteq> c \<longrightarrow> f a b \<noteq> f a c"
   "(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b"
   by smt+
 
 
-section {* Guidance for quantifier heuristics: patterns *}
+section \<open>Guidance for quantifier heuristics: patterns\<close>
 
 lemma
   assumes "\<forall>x.
     SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat (f x)) SMT.Symb_Nil) SMT.Symb_Nil)
     (f x = x)"

       (SMT.Symb_Cons (SMT.pat (g y)) SMT.Symb_Nil)) SMT.Symb_Nil) (f x = g y)"
   shows "f a = g b"
   using assms by smt
 
 
-section {* Meta-logical connectives *}
+section \<open>Meta-logical connectives\<close>
 
 lemma
   "True \<Longrightarrow> True"
   "False \<Longrightarrow> True"
   "False \<Longrightarrow> False"

   "(p \<or> q) \<and> \<not> p \<Longrightarrow> q"
   "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)"
   by smt+
 
 
-section {* Integers *}
+section \<open>Integers\<close>
 
 lemma
   "(0::int) = 0"
   "(0::int) = (- 0)"
   "(1::int) = 1"

   "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   by smt+
 
 
-section {* Reals *}
+section \<open>Reals\<close>
 
 lemma
   "(0::real) = 0"
   "(0::real) = -0"
   "(0::real) = (- 0)"

   "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   by smt+
 
 
-section {* Datatypes, Records, and Typedefs *}
-
-subsection {* Without support by the SMT solver *}
-
-subsubsection {* Algebraic datatypes *}
+section \<open>Datatypes, Records, and Typedefs\<close>
+
+subsection \<open>Without support by the SMT solver\<close>
+
+subsubsection \<open>Algebraic datatypes\<close>
 
 lemma
   "x = fst (x, y)"
   "y = snd (x, y)"
   "((x, y) = (y, x)) = (x = y)"

   "snd (hd [(a, b)]) = b"
   using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps
   by smt+
 
 
-subsubsection {* Records *}
+subsubsection \<open>Records\<close>
 
 record point =
   cx :: int
   cy :: int
 

    apply (smt bw_point.update_convs(1))
   apply (smt bw_point.cases_scheme bw_point.update_convs(1) point.update_convs(1,2))
   done
 
 
-subsubsection {* Type definitions *}
+subsubsection \<open>Type definitions\<close>
 
 typedef int' = "UNIV::int set" by (rule UNIV_witness)
 
 definition n0 where "n0 = Abs_int' 0"
 definition n1 where "n1 = Abs_int' 1"

   "plus' n1 n1 = n2"
   "plus' n0 n2 = n2"
   by (smt 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) *}
-
-subsubsection {* Algebraic datatypes *}
+subsection \<open>With support by the SMT solver (but without proofs)\<close>
+
+subsubsection \<open>Algebraic datatypes\<close>
 
 lemma
   "x = fst (x, y)"
   "y = snd (x, y)"
   "((x, y) = (y, x)) = (x = y)"

   using fst_conv snd_conv prod.collapse list.sel(1,3)
   using [[smt_oracle, z3_extensions]]
   by smt+
 
 
-subsubsection {* Records *}
+subsubsection \<open>Records\<close>
 
 lemma
   "\<lparr>cx = x, cy = y\<rparr> = \<lparr>cx = x', cy = y'\<rparr> \<Longrightarrow> x = x' \<and> y = y'"
   using [[smt_oracle, z3_extensions]]
   by smt+

   using point.simps bw_point.simps
   using [[smt_oracle, z3_extensions]]
   by smt
 
 
-subsubsection {* Type definitions *}
+subsubsection \<open>Type definitions\<close>
 
 lemma
   "n0 \<noteq> n1"
   "plus' n1 n1 = n2"
   "plus' n0 n2 = n2"
   using [[smt_oracle, z3_extensions]]
   by (smt n0_def n1_def n2_def plus'_def)+
 
 
-section {* Function updates *}
+section \<open>Function updates\<close>
 
 lemma
   "(f (i := v)) i = v"
   "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v)) i2 = f i2"
   "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v1"

   "i1 \<noteq> i2 \<and>i1 \<noteq> i3 \<and>  i2 \<noteq> i3 \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
   using fun_upd_same fun_upd_apply
   by smt+
 
 
-section {* Sets *}
+section \<open>Sets\<close>
 
 lemma Empty: "x \<notin> {}" by simp
 
 lemmas smt_sets = Empty UNIV_I Un_iff Int_iff