theory pres imports Main begin (* Exemple de définition de fonctions. Ici la fonction f: \ \ \ \ \ x, y \ 3x + 2y + 1 *) fun f ::"nat * nat \ nat" where "f(x,y)= 3*x + 2*y + 1" (* Exemple de calcul de valeurs particulières de cette fonction *) value "f(1,1)" value "f(10,18)" value "f(0,0)" (* Fonction de simplification d'expressions *) function simpl :: "int \ int" where "simpl(y + 0) = y" | "simpl(y * 0) = 0" sorry value "simpl(A + 0)" value "simpl(B * 0)" value "simpl(A + (B * 0))" value "simpl((B + 0) + (B * (A * 0)))" (* On peut définir des programmes qui calculent par réccurence *) fun sum::"nat \ nat" where "sum(0) = 0" | "sum(x) = x + sum(x - 1)" value "sum(2)" value "sum(9)" value "sum(100)" value "sum(1000)" (* etc... *) function fastPower:: "nat * nat \ nat" where "fastPower(_,0)=1" | "fastPower(x,(Suc 0))= x" | "fastPower(x,(Suc (Suc 0)))= x*x" | "fastPower(x,(Suc (Suc (Suc (Suc (Suc 0))))))= x*x*x" | "fastPower(x,(Suc (Suc (Suc y))))= (if ((Suc (Suc (Suc y))) mod 2)=0 then fastPower(fastPower(x,((Suc (Suc (Suc y))) div 2)),2) else (x*fastPower(fastPower(x,((Suc (Suc (Suc y))) div 2)),2)))" sorry termination fastPower apply (relation "measure (%(x,y). y)") apply auto done value "fastPower(2,2)" value "fastPower(3,2)" value "fastPower(4,2)" value "fastPower(2,3)" value "fastPower(3,8)" value "fastPower(1,0)" value "fastPower(0,1)" value "fastPower(0,0)" value "fastPower(2,2)" value "fastPower(2,3)" value "fastPower(2,4)" value "fastPower(2,8)" value "fastPower(2,5)" value "sum(9)" theorem "sum(x) > x" nitpick oops theorem "x>0 \ sum(x)>x" nitpick oops theorem "x>1 \ sum(x) > x" nitpick proof (induction x) case 0 show ?case apply (unfold sum.simps) apply simp done next case (Suc y) show ?case using Suc apply simp apply (smt pres.sum.simps(1) pres.sum.simps(2)) done qed theorem "sum(x)=(x*(x+1)) div 2" apply (induct x) apply auto done fun exp:: "nat*nat \ nat" where "exp(x,0)=1" | "exp(x,Suc(n))=x*exp(x,n)" value "exp(2,3)" (* Trouver automatiquement le bug de fastPower à l'aide de sa spécification *) theorem "exp(x,y)=fastPower(x,y)" quickcheck [size=10] oops lemma "1=(Suc 0)" by auto lemma "3=(Suc (Suc (Suc 0)))" by auto fun addition:: "(nat * nat) \ nat" where "addition(0,x)=x" | "addition(Suc(x),y)=Suc(addition(x,y))" value "addition(10,11)" fun multiplication:: "(nat * nat) \ nat" where "multiplication(0,x)=0"| "multiplication(Suc(x),y)=addition(y,multiplication(x,y))" value "multiplication(9,7)" lemma add_neutral: "addition(x,0)=x" apply (induct x) apply auto done lemma add_suc: "addition(x,Suc(y))=addition(Suc(x),y)" apply (induct x) apply auto done lemma add_assoc: "addition(x,addition(y,z))=addition(addition(x,y),z)" apply (induct x) apply auto done lemma add_commut: "addition(x,y)=addition(y,x)" apply (induct x) apply auto apply (metis add_neutral) by (metis add_suc addition.simps(2)) lemma mult_neg: "multiplication(x,0)=0" apply (induct x) apply auto done lemma mult_Suc: "multiplication(x,Suc(y))=addition(x,multiplication(x,y))" apply (induct x) apply auto apply (metis add_commut pres.add_assoc) done lemma "multiplication(x,y)=multiplication(y,x)" apply (induct x) apply auto apply (metis mult_neg) apply (metis pres.mult_Suc) done datatype mesNat= Zero | Succ mesNat value "Zero" value "Succ(Zero)" (* Fonctions sur les listes. Deux constructeurs de listes: [] et # *) value "[]" value "a#[]" value "(a#(b#[]))" value "a#(b#(c#[]))" fun longueur :: "'a list \ int" where "longueur [] = 0" | "longueur (a#r) = 1 + longueur r" value "longueur [a,b,c,d,e,f,g,h]" theorem "f(x,y) \ 0" nitpick oops fun g:: "int * int \ int" where "g(x,y)= 5*x - 6*y + 4" theorem "f(x,y) \ g(x,y)" by (smt f.simps g.simps) (* Définition propre de la simplification d'expressions *) no_notation Groups.zero_class.zero ("0") no_notation Groups.plus_class.plus (infixl "+" 65) no_notation Groups.times_class.times (infixl "*" 70) datatype exp= A | B | Zero ("0") | Plus exp exp (infixl "+" 65) | Mult exp exp (infixl "*" 65) value "0" value "(y + 0)" value "(y * 0)" fun simpl :: "exp \ exp" where "simpl(y + 0) = y" | "simpl(y * 0) = 0" | "simpl(y) = y" value "simpl(A + 0)" value "simpl(A + 0 + 0)" value "simpl((B + 0) + (B * (A * 0)))" fun simpl_tout :: "exp \ exp" where "simpl_tout(x + y) = simpl(simpl_tout(x)+simpl_tout(y))" | "simpl_tout(x * y) = simpl(simpl_tout(x)*simpl_tout(y))" | "simpl_tout(x) = x" value "simpl_tout(A + 0)" value "simpl_tout(A + 0 + 0)" value "simpl_tout((B + 0) + (B * (A * 0)))" end