theory TestProp goal Test0 : true goal Test0_5 : true -> false logic a logic b goal Test1: a and b -> a end theory TestInt use import int.Int 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 = 2 and 2 = 3 and 4 = 5 and 6 = 7 goal Test8: 2+2=4 and 3+3=6 axiom A : 1 = 2 goal Test9: 2+2=5 and 3+3=8 end theory TestSplit logic aa int logic bb int goal G : aa 0 /\ bb 1 -> false 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 TestList use import int.Int use import list.List logic x : list int (* goal Test1: match x with | Nil -> 1 = 0 and 2 = 3 | Cons _ Nil -> 4 = 5 and 6 = 7 | Cons _ _ -> 8 = 9 /\ 10 = 11 end *) 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