theory TestInt use import int.Int goal Test0 : true goal Test0_5 : true -> false goal Test1: 2+2 = 4 goal Test2: forall x:int. x*x >= 0 goal Test3: 1<>0 goal Test4: 1=2 -> 3=4 goal Test5: forall x:int. x <> 0 -> x*x > 0 goal Test6: 2+3 = 5 and (forall x:int. x*x >= 0) goal Test7: 0 = 1 /\ 2 = 3 /\ 4 = 5 /\ 6 = 7 (* goal Test8: 3+3=7 *) end theory TestDiv use import int.Int use int.EuclideanDivision goal EDiv1: EuclideanDivision.div 1 2 = 0 goal EDiv2: EuclideanDivision.div (-1) 2 = -1 use int.ComputerDivision goal CDiv1: ComputerDivision.div 1 2 = 0 goal CDiv2: ComputerDivision.div (-1) 2 = 0 end theory TestReal use import real.Real goal Real1: forall x:real. x <> 0.0 -> x*x <> 0.0 use import real.Abs goal RealAbs1: forall x:real. 100.0 >= abs x >= 1.0 -> x*x >= 1.0 end theory TestFloat use import floating_point.Rounding use floating_point.Single lemma Round_single_01: Single.round NearestTiesToEven 0.1 = 0x0.199999Ap0 end theory TestList use import int.Int use import list.List logic x : list int (* goal Test1: match x with | Nil -> 1 = 0 /\ 2 = 3 | Cons _ Nil -> 4 = 5 and 6 = 7 | Cons _ _ -> 8 = 9 /\ 10 = 11 end *) end