(* Author: *)
theory Day1
imports Complex_Main
begin
chapter {* First encounter *}
\ \This is how we write short comments.\
section {* Lower Panel *}
subsection {* Output *}
text{* Click anywhere on a line with a mathematical expression (e.g. the two lines below) and
observe what Isabelle shows in Output. *}
term "{23 - 3, (1 + 1005) / 2 - (3::real)}"
value "{23 - 3, (1 + 1005) / 2 - (3::real)}"
\ \What is the difference between @{command term} and @{command value}?\
(* type your answer here *)
subsection {* Query *}
\ \Search for the expression @{term "x + y = z"}?\
(* just the string "x + y = z" including quotations*)
\ \How many theorems has Isabelle found?\
(* type your answer here *)
\ \Replace each variable with an underscore in your search. How many theorems has Isabelle found?\
(* type your answer here *)
\ \Copy the name of a theorem in your query and paste it next to thm. Check it with Output.\
thm
\ \Let's search for "\". Use ``name: pi''. Paste one result here: \
thm
\ \Refine your search. Use ``name: pi_''. Paste one result here: \
thm
\ \Do not forget to check the content of ``Output''. \
subsection {* Symbols *}
\ \Use the command term and symbols panel to write an expression with Greek letters below: \
term
\ \WARNING: Isabelle complains if the symbol is not defined. Try a symbols in ``Punctuation'': \
term
\ \We can use backslash like in LaTeX. Try to type "\ \ \" (i.e. \xi \inter \Xi)\
term
text{* You can change the ``completion delay'' in Preferences > Plugin Options > Isabelle >
General > Completion Delay. *}
\ \The red cursor keeps the history of where it has been placed. Use arrows at the end of the toolbar.\
section {* Right Panel *}
subsection {* Documentation *}
\ \ In panel Documentation open "Drinker.thy" file in "Examples" folder.\
subsection {* Sidekick *}
\ \Use sidekick to move to another place in this file, then come back.\
\ \Use sidekick's filter box to move to another place in this file, then come back.\
subsection {* State *}
text{* Mainly for debugging. "Output" shows too much while "State" is clean. *}
lemma (in comm_semiring) "x + y = y + x"
using add.commute by blast
subsection {* Theories (and navigation) *}
\ \On "Theories" double-click a theory. Then come back.\
\ \On address bar, click on a theory. Then close it with red x in toolbar.\
text{* Did the theory disappear in the right panel ("Theories")? Did it disappear in the address-bar? *}
(* you may type your answer here *)
text{* You can visit the declaration of some things by holding the Ctrl/Cmmd key
and clicking the thing you want to consult. *}
\ \Consult the theory containing the theorem called ``add.commute''. Paste its contents below.\
\ \Consult the declaration of the + symbol.\
section {* Variables *}
text {* Different color codes for different kinds of variables. *}
\ \Free Variables are blue.\
term "x"
\ \Bound Variables are green.\
term "\ x. x = x"
\ \Schematic variables are blue and preceded by a question mark.\
thm Groups.add_0
\ \Type variables are magenta and preceded by an apostrophe.\
typ "'a"
\ \Constants, functions and other punctuation symbols are black.\
term "[0, 1, 2]"
\ \Indicate for each variable in the next expression whether it occurs bound or free.\
term "\ x. \ z. f (x::'a) + y + z = 0"
text {* In a logical sense, free and schematic variables are indiscernible. In an
operational sense, schematic variable can be substituted for any specific term.*}
thm Groups.group_add_class.add.group_left_neutral
thm Groups.group_add_class.add.group_left_neutral[of 2]
thm Groups.group_add_class.add.group_left_neutral [where ?a = "f 1 y"]
section {* Types *}
text {* Every term has a specific type. Basic types are booleans (bool), natural numbers (nat),
integers (int), rational numbers (rat), real numbers (real), complex numbers (complex) or
generic (type variables). *}
text {* Use Ctrl/Cmmnd hover to see the type of n in each line below. *}
prop "n + 1 = 0"
prop "n + 1 = (0::real)"
prop "Suc n = 0"
\ \What is the type of the following terms? Try to answer before consulting Output.\
(* type your answer here *)
term "0::nat"
(* type your answer here *)
term "x::int"
(* type your answer here *)
term "0"
(* type your answer here *)
term "y"
(* type your answer here *)
term "True"
text {* We also have type constructors, e.g. the product of types, the coproduct (sum) of types, the
type of functions from one type to another, the type of lists over a type, and the type of sets
over a type. Examples provided below: *}
term "(x, y) :: 'a \ 'b"
term "Inl x :: 'a + 'b"
term "\x. f x :: 'a \ 'b"
term "[x1, x2, x3, x4] :: 'a list"
term "{x1, x2, x3, x4} :: 'a set"
\ \ What is the type of "Suc n"?\
(* type your answer here *)
\ \ What is the type of the constant @{term "False"}?\
(* type your answer here *)
\ \ What is the type of an equality?\
(* type your answer here *)
term "(=) :: nat \ nat \ bool"
term "(=)"
\ \ What happens if you equate two expressions of different types?\
(* type your answer here *)
section {* Theorems *}
text{* A theorem in Isabelle has the form "P\<^sub>1 \ P\<^sub>2 \ \ \ P\<^sub>n \ Q" where "Q" is the conclusion
of the statement, and "P\<^sub>1, P\<^sub>2, \, P\<^sub>n" are its hypotheses. *}
text{* For a non-comprehensive list of impressive formalisations of mathematical theorems see
http://www.cse.unsw.edu.au/~kleing/top100/ *}
subsection{* Proof styles *}
text{* There are several ways to show that theorems are true:*}
\\Automatic proofs\
lemma "\ x. P x \ \ x. P x \ Q x \ \ x. Q x"
by auto
\\Apply-style proofs (with rules)\
lemma "\ x. P x \ \ x. P x \ Q x \ \ x. Q x"
apply(rule allI)
apply (erule allE)
apply (erule allE)
apply (erule impE)
apply assumption
apply assumption
done
\\Math-like (or structured) proofs\
lemma (in field)
shows "2 dvd x \ 2 dvd x\<^sup>2"
proof-
assume "2 dvd x"
then obtain k where "x = 2 * k"
by blast
hence "x\<^sup>2 = (2 * k)\<^sup>2"
by simp
also have "... = 4 * k\<^sup>2"
by (simp add: local.power_mult_distrib)
ultimately have "\ k. x\<^sup>2 = 2 * k"
by (metis semiring_normalization_rules(18) semiring_normalization_rules(29))
thus "2 dvd x\<^sup>2"
by auto
qed
subsection{* Theorem Presentation *}
text{* Isabelle provides suggestions. *}
text{* Change "lemma" with "theorem", "corollary" and "proposition" respectively. *}
lemma "\ x. P x \ \ x. P x \ Q x \ \ x. Q x"
by blast
lemma "\ x. P x \ \ x. P x \ Q x \ \ x. Q x"
by blast
lemma "\ x. P x \ \ x. P x \ Q x \ \ x. Q x"
by blast
text{* The name you give to your lemma is important. Follow the suggestion: *}
lemma my_personal_theorem1: "\ x. P x \ \ x. P x \ Q x \ \ x. Q x"
by blast
lemma my_personal_theorem2: "\ x. R x \ \ x. R x \ Q x \ \ x. Q x"
sorry
text{* You can even name the assumptions of a theorem. *}
lemma my_personal_theorem3:
assumes "x < c"
and "x < c \ S x"
shows "S x"
sorry
text{* Use schematic variables to simplify long expressions: *}
lemma my_personal_theorem4:
assumes "x < c"
and "x < c \ super_ultra_big_name_for_a_predicate x" (is "?P \ ?Q")
shows "?Q"
proof-
show ?thesis
sorry
qed
text{* Use command named_theorems when grouping many properties under one name: *}
named_theorems personal_theorems "compilation of personal theorems"
declare my_personal_theorem1 [personal_theorems]
\\Use "and" or a separate "declare" to add more theorems to the list.\
\\Check the result with thm and Output.\
\\You can also add a theorem directly to the list when proving it:\
lemma my_personal_theorem6[personal_theorems]:"\ x. F x \ \ x. F x \ R x \ \ x. R x"
by blast
thm personal_theorems(2)
subsection{* Oops and sorry *}
lemma p_eq_np: "P = NP"
\ \I do not believe in this.\
oops
(* thm p_eq_np *)
lemma p_neq_np: "P \ NP"
\ \I have a proof of this theorem that does not fit here.\
sorry
thm p_neq_np
subsection{* Quickcheck and nitpick *}
lemma "P = NP"
oops
lemma "{a} \ {b} = {a,c}"
oops
lemma "A \ B = C"
oops
section {* Sledgehammer *}
lemma "continuous_on X f \ Y \ X \ Z \ Y \ continuous_on Z f"
oops
chapter {* Apply-style Proofs *}
section{* Natural Deduction *}
subsection{* Propositional Logic *}
text{* Conjunction @{text "(\)"} *}
thm conjI \ \@{thm conjI[no_vars]}\
thm conjunct1 \ \@{thm conjunct1[no_vars]}\
thm conjunct2 \ \@{thm conjunct2[no_vars]}\
thm conjE \ \@{thm conjE[no_vars]}\
text{* Disjunction @{text "(\)"} *}
thm disjI1 \ \@{thm disjI1[no_vars]}\
thm disjI2 \ \@{thm disjI2[no_vars]}\
thm disjE \ \@{thm disjE[no_vars]}\
text{* Implication @{text "(\)"} *}
thm impI \ \@{thm impI[no_vars]}\
thm mp \ \@{thm mp[no_vars]}\
thm impE \ \@{thm impE[no_vars]}\
text{* Negation @{text "(\)"} *}
thm notI \ \@{thm notI[no_vars]}\
thm notE \ \@{thm notE[no_vars]}\
text{* True *}
thm TrueI \ \@{thm TrueI[no_vars]}\
text{* False *}
thm FalseE \ \@{thm FalseE[no_vars]}\
text{* Biconditional @{text "(\)"} *}
thm iff_conv_conj_imp \ \@{thm iff_conv_conj_imp[no_vars]}\
thm iffI \ \@{thm iffI[no_vars]}\
subsection {* Classical Rules *}
thm excluded_middle \ \@{thm excluded_middle[no_vars]}\
thm ccontr \ \@{thm ccontr[no_vars]}\
thm notnotD \