Exercice 1
Dans la spécification des booléens vue en cours et rappelée ci-dessous, démontrer formellement les théorèmes suivants :
{$\def\OR{\,\,.\mkern -3mu\vee.\,}$}
- {$a \OR \mbox{false} = a$}
- {$a \OR b = b \OR a$}
- {$(a \OR b) \OR c = a \OR (b \OR c)$}
theorem "a .∨. false = a"
proof -
from b7[where b= "false"] have "a .∨. false = ¬.(¬.a .∧. ¬.false)" .
also from notfalse have "... = ¬.(¬.a .∧. true)" .. (* congruence par .∧. puis par ¬. *)
also from b3[where a = "¬.a"] have "... = ¬.(¬.a)" .. (* congruence par ¬. *)
also from b2 have "... = a" .
finally show ?thesis .
qed
theorem "a .∨. b = b .∨. a"
proof -
from b7 have "a .∨. b = ¬.(¬.a .∧. ¬.b)" .
also from b6[where a = "¬.a" and b = "¬.b"] have "... = ¬.(¬.b .∧. ¬.a)" .. (* congruence par ¬. *)
also from b7[where a = "b" and b = "a", symmetric] have "... = b .∨. a" .
finally show ?thesis .
qed
theorem "(a .∨. b) .∨. c = a .∨. (b .∨. c)"
proof -
from b7[where a = "a .∨. b" and b = "c"] have "(a .∨. b) .∨. c = ¬.(¬.(a .∨. b) .∧. ¬.c)" .
also from b7 have "... = ¬.(¬.(¬.(¬.a .∧. ¬.b)) .∧. ¬.c)" .. (* congruence par .∧. et ¬. *)
also from b2[where a = "¬.a .∧. ¬.b"] have "... = ¬.((¬.a .∧. ¬.b) .∧. ¬.c)" .. (* cong. idem *)
also from b5[where a = "¬.a" and b = "¬.b" and c = "¬.c"] have "... = ¬.(¬.a .∧. (¬.b .∧. ¬.c))" ..
also from b2[where a = "¬.b .∧. ¬.c", symmetric] have "... = ¬.(¬.a .∧. ¬. (¬.(¬.b .∧. ¬.c)))" ..
also from b7[where b = "¬.(¬.b .∧. ¬.c)", symmetric] have "... = a .∨. ¬.(¬.b .∧. ¬.c)" .
also from b7[where a = "b" and b = "c", symmetric] have "... = a .∨. (b .∨. c)" ..
finally have "(a .∨. b) .∨. c = a .∨. (b .∨. c)" .
thus ?thesis .
qed
theory Bool
imports Main
begin
(* This type is called boolean because bool is already defined in Isabelle *)
(* Since "True" and "False" are of type bool, we use "true" and "false" instead *)
(* The Not, And and Or operations are noted ¬., .∧. and .∨. to distinguish them *)
(* from the operations on the predefined bool type. *)
(* Signature of the specification = name of the sort + constants and operations *)
datatype boolean =
true
| false
(* Logical Not, with prefix notation "¬." *)
| Not boolean ("¬.")
(* Logical And, with infix notation ".∧." with precedence 65 ("=" has precedence 50) *)
| And boolean boolean (infix ".∧." 65)
(* Logical Or, with infix notation ".∨." with precedence 65 ("=" has precedence 50) *)
| Or boolean boolean (infix ".∨." 65)
(* The signature determines the set of terms of the specification *)
(* Examples of closed terms (without variables) *)
term "true"
term "false"
term "Not faux"
term "¬. faux" (* using the notation *)
term "And true false"
term "true .∧. false" (* using the infix notation *)
term "(true .∧. false) .∨. true"
(* Examples of things that are not terms *)
term "Not true false"
term "true Or"
(* Examples of terms with variables *)
term "(a::boolean) .∧. true" (* The type of the variable is stated explicitely *)
term "a .∧. true" (* The type of the variable is infered automatically *)
(* Axioms of the specification: determine which terms are intrinsically congruent *)
axiomatization
where
b1 : "¬. true = false" and
b2 : "¬.(¬.a) = a" and
b3 : "a .∧. true = a" and
b4 : "a .∧. false = false" and
b5 : "(a .∧. b) .∧. c = a .∧. (b .∧. c)" and
b6 : "a .∧. b = b .∧. a" and
b7 : "a .∨. b = ¬.(¬.a .∧. ¬.b)"
end
(* Show that ¬.false = true *)
(* proof methods are: *)
(* . : deduce fact from raw facts *)
(* .. : deduce fact from facts and congruence *)
(* by simp : deduce fact from facts using congruence, symmetry and simplifications *)
(* (functions, axioms which are marked [simp]) *)
(* by (metis fact1 fact2 ... factn) : deduce fact from list of facts *)
(* *)
(* "..." in a cascade of facts (marked by "also" and closed by "finally") refers to *)
(* the previous right hand side of the equality. This is a common shorthand when *)
(* using transitivity in a proof. *)
theorem notfalse:
"¬. false = true"
proof -
from b1 [symmetric] have "false = ¬.true" .
from this have "¬.false = ¬.(¬.true)" ..
also from b2 [where a = true] have "... = true" .
finally show ?thesis .
qed
(* Can also be proved by (metis b1 b2)*)
theorem ortrue:
"a .∨. true = true"
proof -
from b7 [where b = true] have "a .∨. true = ¬.(¬.a .∧. ¬.true)" .
also from b1 have "... = ¬.(¬.a .∧. false)" ..
also from b4 [where a = "¬.a"] have "... = ¬.false" ..
also from notfalse have "... = true" .
finally show ?thesis .
qed
(* can also be proved by (metis b1 b4 b7 notfalse)*)
theorem morgan2:
"a .∧. b = ¬.(¬.a .∨. ¬.b)"
proof -
from b7 [where a = "¬.a" and b = "¬.b"]
have "¬.a .∨. ¬.b = ¬.(¬.(¬.a) .∧. ¬.(¬.b))" .
also from b2 and b2 [where a = b] have "... = ¬.(a .∧. b)" by simp
finally have "¬.a .∨. ¬.b = ¬.(a .∧. b)" .
from this have "¬.(¬.a .∨. ¬.b) = ¬.(¬.(a .∧. b))" ..
also from b2 [where a = "a .∧. b"] have "... = a .∧. b" .
finally have "¬.(¬.a .∨. ¬.b) = a .∧. b" .
from this [symmetric] show ?thesis .
qed
(* can also be proved by (metis b2 b7)*)
(* Proof that all booleans are either true or false *)
(* Here we use the regular ∨ operator in the theorem *)
(* because (a = true) and (a = false) are propositions in the *)
(* logic framework used for the proof. *)
theorem alltruefalse: "(a = true) ∨ (a = false)"
(is "?P a") (* We define ?P as an abbreviation of the property *)
proof (induct a) (* structural induction *)
case (true)
have "true = true" .. (* Reflexivity *)
hence "?P true" ..
thus ?case .
next
case (false)
have "false = false" ..
hence "?P false" ..
thus ?case .
next
case (Not b) thus ?case
proof (cases "b = true")
case True (* b = true *)
from b1 have "(¬.b) = false" ..
thus ?thesis ..
next
case False (* b ≠ true *)
from notfalse have "(¬.b) = true" ..
thus ?thesis ..
qed
next
case (And b c) thus ?case
proof (cases "c = true")
case True (* c = true *)
from this and b3[where a = "b"] have "b .∧. c = b" by simp
with And.hyps(1) have "?P (b .∧. c)" by simp
thus ?thesis .
next
case False (* c ≠ true *)
from this and And.hyps(2) have "c = false" by simp
with b4[where a = "b"] have "b .∧. c = false" by simp
thus ?thesis ..
qed
next
case (Or b c) thus ?case using b7[where a = "b" and b = "c"] by simp
qed
(* A more automated version of the same proof *)
theorem alltruefalse_auto: "(a = true) ∨ (a = false)"
proof (induct a) (* structural induction *)
case "true" thus ?case by simp
next
case "false" thus ?case by simp
next
case Not thus ?case by (metis b1 notfalse)
next
case And thus ?case by (metis b3 b4)
next
case Or thus ?case using b7 by simp
qed
Exercice 2
On considère la spécification suivante des listes :
theory ListTD1
imports Main
begin
(* A list of strings *)
datatype list =
nil
| cons string list
(* Tell whether a list is nil *)
fun null :: "list ⇒ bool"
where
"null nil = True"
| "null (cons e l) = False"
(* Get the first item of a list (not defined for the empty list) *)
fun first :: "list ⇒ string"
where
"first (cons e l) = e"
(* Get the rest of a list (all its items but the first one) *)
fun rest :: "list ⇒ list"
where
"rest nil = nil"
| "rest (cons e l) = l"
end
Question 1
Donner une extension de cette spécification définissant les opérations :
length- qui donne la longueur d'une liste
contains- qui indique si un élément est présent dans une liste
index- qui donne la position d'un élément dans une liste
reverse- qui rend l'inverse d'une liste (les éléments sont dans l'ordre inverse)
get- qui rend l'élément se trouvant à une position donnée dans une liste
insert- qui insère un élément à une position donnée dans une liste
theory ListTD_Extended
(* Extension of ListTD1 with new operations *)
imports ListTD1
begin
(*
* In the definition of the functions, we give a name to the axioms
* so that we can use them later in proofs.
* The name of an axiom is set by putting a name followed by ':' in front of the definition.
*)
(* Length of a list = number of items in the list *)
fun length:: "list ⇒ nat"
where
len_nil: "length nil = 0" (* known as axiom len_nil *)
| len_cons: "length (cons e l) = Suc (length l)"
value "length nil"
value "length (cons ''a'' (cons ''b'' nil))"
(* Tells whether a list contains a given string. *)
fun contains:: "list ⇒ string ⇒ bool"
where
cont_nil: "contains nil elem = False" (* The empty list contains nothing *)
| cont_cons: "contains (cons e l) elem = ( (* A list contains an item *)
if (elem = e) (* if the item if the first one *)
then True
else contains l elem (* or if the rest of the list contains the item *)
)"
(* Return the position of the first occurrence of a string in a list *)
(* "index l s" is defined only if "contains l s" *)
fun index:: "list ⇒ string ⇒ nat"
where
"index (cons e l) elem = (
if (elem = e)
then Suc 0 (* if the string is the first element, the index is 1 *)
else Suc (index l elem) (* else, it is the successor (+1) of the position of the element in the rest of the list *)
)"
| "index l s = undefined"
value "index (cons ''a'' (cons ''b'' (cons ''c'' (cons ''a'' nil)))) ''b''"
(* Append a string at the end of a list *)
fun snoc:: "list ⇒ string ⇒ list"
where
snoc_nil: "snoc nil e = cons e nil"
| snoc_cons: "snoc (cons e1 l) e = cons e1 (snoc l e)"
(* Reverse the order of the items of a list *)
fun reverse:: "list ⇒ list"
where
rev_nil: "reverse nil = nil"
| rev_cons: "reverse (cons e l) = snoc (reverse l) e"
value "reverse (cons ''a'' (cons ''b'' (cons ''c'' (cons ''d'' nil))))"
(* Get the string at a given position in a list *)
(* "get l n" is defined only if n > 0 and n ≤ length l *)
fun get:: "list ⇒ nat ⇒ string"
where
get_0: "get (cons e l) (Suc 0) = e"
| get_suc: "get (cons e l) (Suc n) = get l n"
| "get l i = undefined"
(* Insert a string at a given position in a list *)
(* "insert l n s" is defined only if n > 0 and n ≤ (Suc length l) *)
(* because it is possible to insert after the last item, at position Suc length l *)
fun insert:: "list ⇒ nat ⇒ string ⇒ list"
where
insert_0: "insert l (Suc 0) elem = cons elem l"
| insert_suc: "insert (cons e l) (Suc n) elem = cons e (insert l n elem)"
| "insert l i s = undefined"
Question 2
Démontrer par induction structurelle que length (snoc l x) = length (cons x l).
(* The notation [of "t1" "t2" ... "tn"] is another way to perform substitution *)
(* It substitutes terms t1, t2 ... tn to the first n variables of a fact. *)
(* The notation [where v1="t1" and v2="t2" ... and vn="tn"] we have already seen *)
(* gives the name of the variables explicitely, while [of ...] uses their position. *)
theorem "length (snoc l x) = length (cons x l)"
proof (induction l)
case nil
from snoc_nil[of "x"] have "snoc nil x = cons x nil" .
hence "length (snoc nil x) = length (cons x nil)" by simp (* congruence by length *)
thus ?case .
next
case (cons e ll)
(* Firstly, show that length (snoc (cons e ll) x) = Suc (Suc (length ll)) *)
from snoc_cons[of "e" "ll" "x"] have "snoc (cons e ll) x = cons e (snoc ll x)" .
hence "length (snoc (cons e ll) x) = length (cons e (snoc ll x))" by simp
also from len_cons[of "e" "snoc ll x"] have "... = Suc (length (snoc ll x))" .
also from cons.IH have "... = Suc (length (cons x ll))" ..
also from len_cons[of "x" "ll"] have "... = Suc (Suc (length ll))" ..
finally have 1: "length (snoc (cons e ll) x) = Suc (Suc (length ll))" .
(* Secondly, show that length (cons x (cons e ll)) is also Suc (Suc (length ll)) *)
from len_cons[of "x" "cons e ll"] have "length (cons x (cons e ll)) = Suc (length (cons e ll))" .
also from len_cons[of "e" "l"] have "... = Suc (Suc (length ll))" by simp
finally have 2: "length (cons x (cons e ll)) = Suc (Suc (length ll))" .
(* Now, conclude... *)
from 1 and 2 have "length (snoc (cons e ll) x) = length (cons x (cons e ll))" ..
thus ?case .
qed
Question 3
Démontrer par induction structurelle que snoc l e = insert l e (Suc (length l))
theorem "snoc l e = insert l (Suc (length l)) e"
proof (induction l)
case nil
from snoc_nil have "snoc nil e = cons e nil" .
also from len_nil and insert_0[of "nil" "e", symmetric] have "cons e nil = insert nil (Suc (length nil)) e" by simp
finally show ?case .
next
case (cons e' l')
from snoc_cons[of "e'" "l'" "e"] have "snoc (cons e' l') e = cons e' (snoc l' e)" .
also from cons.IH have "... = cons e' (insert l' (Suc (length l')) e)" by simp
also from insert_suc[of "e'" "l'" "length l'" "e", symmetric]
have "... = insert (cons e' l') (Suc (Suc (length l'))) e" .
also from len_cons[of "e'" "l'", symmetric]
have "... = insert (cons e' l') (Suc (length (cons e' l'))) e" by simp
finally show ?case .
qed
Exercice supplémentaire (non traité en TD)
Donner une spécification des booléens sans axiomes (uniquement avec des constantes et des fonctions).
Vérifiez que chaque fonction est complètement définie.
Démontrer la commutativité du ET par induction.
Utilisez le squelette ci-dessous pour débuter :
theory Bool
imports Main
begin
datatype boolean =
true
| false
(* Logical Not, with prefix notation "¬." to avoid confusion with the predefined ¬ operation *)
fun Not :: "boolean ⇒ boolean" ("¬.")
where
"¬.true = false"
| "¬.false = true"
(* Logical And, with infix notation ".∧." with precedence 65 ("=" has precedence 50) *)
fun And :: "boolean ⇒ boolean ⇒ boolean" (infix ".∧." 65)
where
(* to be completed *)
(* Logical Or, with infix notation ".∨." with precedence 65 ("=" has precedence 50) *)
fun Or :: "boolean ⇒ boolean ⇒ boolean" (infix ".∨." 65)
where
(* to be completed *)
(* Test how some simple terms are evaluated *)
value "false .∨. true"
value "(a .∨. true) .∧. true"
(* Proof by induction that logical And is commutative *)
theorem and_commutative: "a .∧. b = b .∧. a"
proof (cases a)
(* to be completed *)
qed