1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/IsarRef/Thy/Synopsis.thy Tue May 31 22:47:18 2011 +0200
1.3 @@ -0,0 +1,216 @@
1.4 +theory Synopsis
1.5 +imports Base Main
1.6 +begin
1.7 +
1.8 +chapter {* Synopsis *}
1.9 +
1.10 +section {* Notepad *}
1.11 +
1.12 +text {*
1.13 + An Isar proof body serves as mathematical notepad to compose logical
1.14 + content, consisting of facts, terms, types.
1.15 +*}
1.16 +
1.17 +
1.18 +subsection {* Facts *}
1.19 +
1.20 +text {*
1.21 + A fact is a simultaneous list of theorems.
1.22 +*}
1.23 +
1.24 +
1.25 +subsubsection {* Producing facts *}
1.26 +
1.27 +notepad
1.28 +begin
1.29 +
1.30 + txt {* Via assumption (``lambda''): *}
1.31 + assume a: A
1.32 +
1.33 + txt {* Via proof (``let''): *}
1.34 + have b: B sorry
1.35 +
1.36 + txt {* Via abbreviation (``let''): *}
1.37 + note c = a b
1.38 +
1.39 +end
1.40 +
1.41 +
1.42 +subsubsection {* Referencing facts *}
1.43 +
1.44 +notepad
1.45 +begin
1.46 + txt {* Via explicit name: *}
1.47 + assume a: A
1.48 + note a
1.49 +
1.50 + txt {* Via implicit name: *}
1.51 + assume A
1.52 + note this
1.53 +
1.54 + txt {* Via literal proposition (unification with results from the proof text): *}
1.55 + assume A
1.56 + note `A`
1.57 +
1.58 + assume "\<And>x. B x"
1.59 + note `B a`
1.60 + note `B b`
1.61 +end
1.62 +
1.63 +
1.64 +subsubsection {* Manipulating facts *}
1.65 +
1.66 +notepad
1.67 +begin
1.68 + txt {* Instantiation: *}
1.69 + assume a: "\<And>x. B x"
1.70 + note a
1.71 + note a [of b]
1.72 + note a [where x = b]
1.73 +
1.74 + txt {* Backchaining: *}
1.75 + assume 1: A
1.76 + assume 2: "A \<Longrightarrow> C"
1.77 + note 2 [OF 1]
1.78 + note 1 [THEN 2]
1.79 +
1.80 + txt {* Symmetric results: *}
1.81 + assume "x = y"
1.82 + note this [symmetric]
1.83 +
1.84 + assume "x \<noteq> y"
1.85 + note this [symmetric]
1.86 +
1.87 + txt {* Adhoc-simplication (take care!): *}
1.88 + assume "P ([] @ xs)"
1.89 + note this [simplified]
1.90 +end
1.91 +
1.92 +
1.93 +subsubsection {* Projections *}
1.94 +
1.95 +text {*
1.96 + Isar facts consist of multiple theorems. There is notation to project
1.97 + interval ranges.
1.98 +*}
1.99 +
1.100 +notepad
1.101 +begin
1.102 + assume stuff: A B C D
1.103 + note stuff(1)
1.104 + note stuff(2-3)
1.105 + note stuff(2-)
1.106 +end
1.107 +
1.108 +
1.109 +subsubsection {* Naming conventions *}
1.110 +
1.111 +text {*
1.112 + \begin{itemize}
1.113 +
1.114 + \item Lower-case identifiers are usually preferred.
1.115 +
1.116 + \item Facts can be named after the main term within the proposition.
1.117 +
1.118 + \item Facts should \emph{not} be named after the command that
1.119 + introduced them (@{command "assume"}, @{command "have"}). This is
1.120 + misleading and hard to maintain.
1.121 +
1.122 + \item Natural numbers can be used as ``meaningless'' names (more
1.123 + appropriate than @{text "a1"}, @{text "a2"} etc.)
1.124 +
1.125 + \item Symbolic identifiers are supported (e.g. @{text "*"}, @{text
1.126 + "**"}, @{text "***"}).
1.127 +
1.128 + \end{itemize}
1.129 +*}
1.130 +
1.131 +
1.132 +subsection {* Block structure *}
1.133 +
1.134 +text {*
1.135 + The formal notepad is block structured. The fact produced by the last
1.136 + entry of a block is exported into the outer context.
1.137 +*}
1.138 +
1.139 +notepad
1.140 +begin
1.141 + {
1.142 + have a: A sorry
1.143 + have b: B sorry
1.144 + note a b
1.145 + }
1.146 + note this
1.147 + note `A`
1.148 + note `B`
1.149 +end
1.150 +
1.151 +text {* Explicit blocks as well as implicit blocks of nested goal
1.152 + statements (e.g.\ @{command have}) automatically introduce one extra
1.153 + pair of parentheses in reserve. The @{command next} command allows
1.154 + to ``jump'' between these sub-blocks. *}
1.155 +
1.156 +notepad
1.157 +begin
1.158 +
1.159 + {
1.160 + have a: A sorry
1.161 + next
1.162 + have b: B
1.163 + proof -
1.164 + show B sorry
1.165 + next
1.166 + have c: C sorry
1.167 + next
1.168 + have d: D sorry
1.169 + qed
1.170 + }
1.171 +
1.172 + txt {* Alternative version with explicit parentheses everywhere: *}
1.173 +
1.174 + {
1.175 + {
1.176 + have a: A sorry
1.177 + }
1.178 + {
1.179 + have b: B
1.180 + proof -
1.181 + {
1.182 + show B sorry
1.183 + }
1.184 + {
1.185 + have c: C sorry
1.186 + }
1.187 + {
1.188 + have d: D sorry
1.189 + }
1.190 + qed
1.191 + }
1.192 + }
1.193 +
1.194 +end
1.195 +
1.196 +
1.197 +subsection {* Terms and Types *}
1.198 +
1.199 +notepad
1.200 +begin
1.201 + txt {* Locally fixed entities: *}
1.202 + fix x -- {* local constant, without any type information yet *}
1.203 + fix x :: 'a -- {* variant with explicit type-constraint for subsequent use*}
1.204 +
1.205 + fix a b
1.206 + assume "a = b" -- {* type assignment at first occurrence in concrete term *}
1.207 +
1.208 + txt {* Definitions (non-polymorphic): *}
1.209 + def x \<equiv> "t::'a"
1.210 +
1.211 + txt {* Abbreviations (polymorphic): *}
1.212 + let ?f = "\<lambda>x. x"
1.213 + term "?f ?f"
1.214 +
1.215 + txt {* Notation: *}
1.216 + write x ("***")
1.217 +end
1.218 +
1.219 +end
1.220 \ No newline at end of file