section \<open>Example theory file for getting acquainted with Isabelle\<close>
(*<*)
theory Example
imports Main

begin
(*>*)
subsection \<open>Terms\<close>
text \<open>
  We can write logical formulae and terms in the usual notation.
  Connectives such as @{text "\<not>"},@{text "\<or>"}, @{text "\<and>"} etc. can be typed using the backslash
  @{text "\\"} followed by the name of the sign. I.e. @{text "\\not"} for @{text "\<not>"}.
  Note that during typing @{text "\\not"} at some point there will be a pop-up menu
  offering you certain auto completion suggestions that you can accept by
  pressing the tab key.
\<close>

subsection \<open>Types\<close>
text \<open>
  All terms (and also constant symbols, variables etc.) are associated
  a type. The type @{type "bool"} is the type of all Boolean-values objects
  (e.g. truth values).
  New types can be inserted at will.
\<close>

typedecl "i" -- "Create a new type i for the type of individuals"


subsection \<open>Constants\<close>
text \<open>
  New constants can be defined using the @{text "consts"} keyword.
  You need to specify the type of the constant explicitly.
\<close>

subsection \<open>Terms and Formulas\<close>
text \<open>
  In higher-order logic (HOL), terms are all well-formed expressions
  that can be expressed within the logic. A term has a unique type, such
  as in @{term "f(A) :: i"} where the term @{term "f(A)"} has type
  @{type "i"}. Terms of type @{type "bool"} are called "formulas".
\<close>

subsubsection \<open>Example formula 1\<close>
text \<open>If it's raining the street will get wet\<close>

consts raining :: "bool" -- "constant symbol for raining"
consts wet :: "i \<Rightarrow> bool" -- "predicate symbol for wet"
consts street :: "i" -- "constant symbol for the street"

prop "raining \<longrightarrow> wet(street)" -- "raining implies street-is-wet"


subsubsection \<open>Example formula 2\<close>
consts good :: "i \<Rightarrow> bool" -- "predicate symbol for being good"

prop "good(A)" -- "A is good"
text \<open>A is a free variable of the above term, hence it is not closed\<close>

subsubsection \<open>Example formula 3\<close>

prop "\<forall>A. good(A)" -- "everything is good"
text \<open>A is a a bound variable of the above term, which is universally qualified.\<close>


subsection \<open>Proofs\<close>
text \<open>We will learn how to formalize proofs in Isabelle throughout this course.\<close>

subsubsection \<open>Proofs with handy keywords\<close>

theorem MyFirstTheorem:
  assumes "A"
  shows "B \<longrightarrow> A"
proof -
  {
    assume "B"
    from assms have "A" by - -- "Iterate the fact that A holds by assumptions using the - sign"
  }
  then have "B \<longrightarrow> A" by (rule impI)
  thus ?thesis .
qed

subsubsection \<open>Proofs with labels\<close>

theorem MyFirstTheorem2:
  assumes 1: "A"
  shows "B \<longrightarrow> A"
proof -
  {
    assume "B"
    from 1 have "A" by -
  } note 2 = this
  from 2 have "B \<longrightarrow> A" by (rule impI)
  thus ?thesis .
qed


subsubsection \<open>Using the proofs\<close>
text \<open>
  We can now derive simple facts of the above theorem.
\<close>

corollary ThatFollowsDirectly:
  assumes "A"
  shows "P(A) \<longrightarrow> A"
using assms by (rule MyFirstTheorem[where B = "P(A)"])


(*<*)
end
(*>*)