theory Overview_Demo
  imports Main
begin

section \<open>A simple recursive function example\<close>

fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
  "add 0 n = n"
| "add (Suc m) n = Suc (add m n)"

text \<open>"Suc" is the successor constructor for natural numbers.\<close>

text \<open>Here's a simple lemma about this function, proved by induction:\<close>

lemma add_02: "add m 0 = m"
  apply(induction m)
   apply (auto)
  done

thm add_02

text \<open>Executing the above function:\<close>

value "add 5 3"

text \<open>... or generating code in a language like Haskell from it:\<close>

export_code add in Haskell

(* A simple comment *)

text \<open>This is also a comment but it generates nice \LaTeX-text!\<close>

section \<open>Types and terms\<close>

term True

text \<open>Note that variables and constants (eg True, &) are displayed differently.\<close>

term False
term true
term "True & False" (* compound terms and formulas need to enclosed in quotes *)
term "True \<and> False"
term "True \<and> false"

value "True \<and> False"
value "True \<and> P"

value "if True then x else y"
value "(if True then x else y) = x" (* if subterms need to enclosed in parentheses *)

value "case n of 0 \<Rightarrow> 0 | Suc n \<Rightarrow> n"
value "(case n of 0 \<Rightarrow> 0 | Suc n \<Rightarrow> n) \<le> n" (* same for case subterms *)

value "A \<and> B = A \<and> B" (* equality has higher precedence than conjunction *)
value "(A \<and> B) = (A \<and> B)"
value "A \<and> B \<longleftrightarrow> A \<and> B" (* conjunction has lower precedence than if-and-only-if *)

(* To display types in jedit: press ctrl (Mac: cmd) and hover over text.
   To view the definition of a constant: press ctrl (Mac: cmd) and click on the text.
*)

text \<open>Warning: "+" and numbers are overloaded:\<close>

term "n + n"
term "n + n = 0"
term "(n::nat) + n = 0"

text \<open>Numbers need type annotations unless the type is clear from the context, e.g.:\<close>

term "Suc n"

(*Try this:

term "True + False"

Terms must be type correct!*)

text \<open>Type inference:\<close>

term "f (g x) y"
term "h (%x. f(g x))"
term "\<lambda>x. x + x"

text \<open>Currying of function arguments (e.g. @{typ "int \<Rightarrow> int \<Rightarrow> int"}} instead of
  tupling them (e.g. @{typ "(int \<times> int) \<Rightarrow> int"}) allows for partial application\<close>

term "add"
term "add 3"
term map
term "map (add 3)"
value "map (add 3) [0, 1, 2]"

section \<open>More on proofs\<close>

text \<open>General schema:

\<open>lemma name[attributes]: "..."
   apply (...)
   apply (...)
   done\<close>

Lemma names and attributes are optional.

Adding the \<open>simp\<close> attribute to a lemma will make the simplifier use it as a rewrite rule by default.

The \<open>oops\<close> command can be used to abort a proof attempt.

The \<open>sorry\<close> command can be used to make Isabelle accept a lemma without a complete proof.
This can be useful for top-down proof development:  assume some lemmas using \<open>sorry\<close> while working
on a higher-level proof, then come back later to finish up the remaining lemmas.

The \<open>apply\<close> commands take proof methods like \<open>auto\<close>, \<open>induction\<close>, or \<open>simp\<close>.\<close>

lemma "add m 0 = m"
  apply(induction m)
   apply (simp) (* unlike auto, simp only works on the first subgoal, leaving any others untouched *)
  (* proof state at this point:

     goal (1 subgoal):
      1. \<And>m. add m 0 = m \<Longrightarrow> add (Suc m) 0 = Suc m

     One remaining subgoal "add (Suc m) 0 = Suc m" with a locally fixed variable "m" and one
     assumption "add m 0 = m".

     Multiple assumptions are written using multiple arrows, e.g. "A1 \<Longrightarrow> A2 \<Longrightarrow> A3 \<Longrightarrow> B". *)
  by auto (* "by" can also finish a proof, taking one or two proof methods *)

end