87 \end{figure} |
87 \end{figure} |
88 |
88 |
89 \<^medskip> |
89 \<^medskip> |
90 Concrete applications require another intermediate layer: an object-logic. |
90 Concrete applications require another intermediate layer: an object-logic. |
91 Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most |
91 Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most |
92 commonly used; elementary examples are given in the directory @{dir |
92 commonly used; elementary examples are given in the directory |
93 "~~/src/HOL/Isar_Examples"}. Some examples demonstrate how to start a fresh |
93 \<^dir>\<open>~~/src/HOL/Isar_Examples\<close>. Some examples demonstrate how to start a fresh |
94 object-logic from Isabelle/Pure, and use Isar proofs from the very start, |
94 object-logic from Isabelle/Pure, and use Isar proofs from the very start, |
95 despite the lack of advanced proof tools at such an early stage (e.g.\ see |
95 despite the lack of advanced proof tools at such an early stage (e.g.\ see |
96 @{file "~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy"}). Isabelle/FOL |
96 \<^file>\<open>~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite |
97 @{cite "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, |
97 "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are |
98 but are much less developed. |
98 much less developed. |
99 |
99 |
100 In order to illustrate natural deduction in Isar, we shall subsequently |
100 In order to illustrate natural deduction in Isar, we shall subsequently |
101 refer to the background theory and library of Isabelle/HOL. This includes |
101 refer to the background theory and library of Isabelle/HOL. This includes |
102 common notions of predicate logic, naive set-theory etc.\ using fairly |
102 common notions of predicate logic, naive set-theory etc.\ using fairly |
103 standard mathematical notation. From the perspective of generic natural |
103 standard mathematical notation. From the perspective of generic natural |
522 |
522 |
523 The \<open>method\<close> category is essentially a parameter of the Isar language and |
523 The \<open>method\<close> category is essentially a parameter of the Isar language and |
524 may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof |
524 may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof |
525 methods semantically in Isabelle/ML. The Eisbach language allows to define |
525 methods semantically in Isabelle/ML. The Eisbach language allows to define |
526 proof methods symbolically, as recursive expressions over existing methods |
526 proof methods symbolically, as recursive expressions over existing methods |
527 @{cite "Matichuk-et-al:2014"}; see also @{dir "~~/src/HOL/Eisbach"}. |
527 @{cite "Matichuk-et-al:2014"}; see also \<^dir>\<open>~~/src/HOL/Eisbach\<close>. |
528 |
528 |
529 Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on |
529 Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on |
530 the goal state. Some basic methods are predefined in Pure: ``@{method "-"}'' |
530 the goal state. Some basic methods are predefined in Pure: ``@{method "-"}'' |
531 leaves the goal unchanged, ``@{method this}'' applies the facts as rules to |
531 leaves the goal unchanged, ``@{method this}'' applies the facts as rules to |
532 the goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and |
532 the goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and |