wneuper/isa: doc-src/IsarRef/Thy/document/Synopsis.tex@a45121ffcfcb (annotated)

wenzelm@44121	1	%
wenzelm@44121	2	\begin{isabellebody}%
wenzelm@44121	3	\def\isabellecontext{Synopsis}%
wenzelm@44121	4	%
wenzelm@44121	5	\isadelimtheory
wenzelm@44121	6	%
wenzelm@44121	7	\endisadelimtheory
wenzelm@44121	8	%
wenzelm@44121	9	\isatagtheory
wenzelm@44121	10	\isacommand{theory}\isamarkupfalse%
wenzelm@44121	11	\ Synopsis\isanewline
wenzelm@44121	12	\isakeyword{imports}\ Base\ Main\isanewline
wenzelm@44121	13	\isakeyword{begin}%
wenzelm@44121	14	\endisatagtheory
wenzelm@44121	15	{\isafoldtheory}%
wenzelm@44121	16	%
wenzelm@44121	17	\isadelimtheory
wenzelm@44121	18	%
wenzelm@44121	19	\endisadelimtheory
wenzelm@44121	20	%
wenzelm@44121	21	\isamarkupchapter{Synopsis%
wenzelm@44121	22	}
wenzelm@44121	23	\isamarkuptrue%
wenzelm@44121	24	%
wenzelm@44121	25	\isamarkupsection{Notepad%
wenzelm@44121	26	}
wenzelm@44121	27	\isamarkuptrue%
wenzelm@44121	28	%
wenzelm@44121	29	\begin{isamarkuptext}%
wenzelm@44121	30	An Isar proof body serves as mathematical notepad to compose logical
wenzelm@44122	31	content, consisting of types, terms, facts.%
wenzelm@44121	32	\end{isamarkuptext}%
wenzelm@44121	33	\isamarkuptrue%
wenzelm@44121	34	%
wenzelm@44122	35	\isamarkupsubsection{Types and terms%
wenzelm@44122	36	}
wenzelm@44122	37	\isamarkuptrue%
wenzelm@44122	38	\isacommand{notepad}\isamarkupfalse%
wenzelm@44122	39	\isanewline
wenzelm@44122	40	\isakeyword{begin}%
wenzelm@44122	41	\isadelimproof
wenzelm@44122	42	%
wenzelm@44122	43	\endisadelimproof
wenzelm@44122	44	%
wenzelm@44122	45	\isatagproof
wenzelm@44122	46	%
wenzelm@44122	47	\begin{isamarkuptxt}%
wenzelm@44122	48	Locally fixed entities:%
wenzelm@44122	49	\end{isamarkuptxt}%
wenzelm@44122	50	\isamarkuptrue%
wenzelm@44122	51	\ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44122	52	\ x\ \ \ %
wenzelm@44122	53	\isamarkupcmt{local constant, without any type information yet%
wenzelm@44122	54	}
wenzelm@44122	55	\isanewline
wenzelm@44122	56	\ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44122	57	\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ \ %
wenzelm@44122	58	\isamarkupcmt{variant with explicit type-constraint for subsequent use%
wenzelm@44122	59	}
wenzelm@44122	60	\isanewline
wenzelm@44122	61	\isanewline
wenzelm@44122	62	\ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44122	63	\ a\ b\isanewline
wenzelm@44122	64	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44122	65	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
wenzelm@44122	66	\isamarkupcmt{type assignment at first occurrence in concrete term%
wenzelm@44122	67	}
wenzelm@44122	68	%
wenzelm@44122	69	\begin{isamarkuptxt}%
wenzelm@44122	70	Definitions (non-polymorphic):%
wenzelm@44122	71	\end{isamarkuptxt}%
wenzelm@44122	72	\isamarkuptrue%
wenzelm@44122	73	\ \ \isacommand{def}\isamarkupfalse%
wenzelm@44122	74	\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{22}{\isachardoublequoteopen}}t{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44122	75	\begin{isamarkuptxt}%
wenzelm@44122	76	Abbreviations (polymorphic):%
wenzelm@44122	77	\end{isamarkuptxt}%
wenzelm@44122	78	\isamarkuptrue%
wenzelm@44122	79	\ \ \isacommand{let}\isamarkupfalse%
wenzelm@44122	80	\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44122	81	\endisatagproof
wenzelm@44122	82	{\isafoldproof}%
wenzelm@44122	83	%
wenzelm@44122	84	\isadelimproof
wenzelm@44122	85	%
wenzelm@44122	86	\endisadelimproof
wenzelm@44122	87	\isanewline
wenzelm@44122	88	\ \ \isacommand{term}\isamarkupfalse%
wenzelm@44122	89	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44122	90	\isadelimproof
wenzelm@44122	91	%
wenzelm@44122	92	\endisadelimproof
wenzelm@44122	93	%
wenzelm@44122	94	\isatagproof
wenzelm@44122	95	%
wenzelm@44122	96	\begin{isamarkuptxt}%
wenzelm@44122	97	Notation:%
wenzelm@44122	98	\end{isamarkuptxt}%
wenzelm@44122	99	\isamarkuptrue%
wenzelm@44122	100	\ \ \isacommand{write}\isamarkupfalse%
wenzelm@44122	101	\ x\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
wenzelm@44122	102	\endisatagproof
wenzelm@44122	103	{\isafoldproof}%
wenzelm@44122	104	%
wenzelm@44122	105	\isadelimproof
wenzelm@44122	106	%
wenzelm@44122	107	\endisadelimproof
wenzelm@44122	108	\isanewline
wenzelm@44122	109	\isacommand{end}\isamarkupfalse%
wenzelm@44122	110	%
wenzelm@44121	111	\isamarkupsubsection{Facts%
wenzelm@44121	112	}
wenzelm@44121	113	\isamarkuptrue%
wenzelm@44121	114	%
wenzelm@44121	115	\begin{isamarkuptext}%
wenzelm@44121	116	A fact is a simultaneous list of theorems.%
wenzelm@44121	117	\end{isamarkuptext}%
wenzelm@44121	118	\isamarkuptrue%
wenzelm@44121	119	%
wenzelm@44121	120	\isamarkupsubsubsection{Producing facts%
wenzelm@44121	121	}
wenzelm@44121	122	\isamarkuptrue%
wenzelm@44121	123	\isacommand{notepad}\isamarkupfalse%
wenzelm@44121	124	\isanewline
wenzelm@44121	125	\isakeyword{begin}%
wenzelm@44121	126	\isadelimproof
wenzelm@44121	127	%
wenzelm@44121	128	\endisadelimproof
wenzelm@44121	129	%
wenzelm@44121	130	\isatagproof
wenzelm@44121	131	%
wenzelm@44121	132	\begin{isamarkuptxt}%
wenzelm@44121	133	Via assumption (``lambda''):%
wenzelm@44121	134	\end{isamarkuptxt}%
wenzelm@44121	135	\isamarkuptrue%
wenzelm@44121	136	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121	137	\ a{\isaliteral{3A}{\isacharcolon}}\ A%
wenzelm@44121	138	\begin{isamarkuptxt}%
wenzelm@44121	139	Via proof (``let''):%
wenzelm@44121	140	\end{isamarkuptxt}%
wenzelm@44121	141	\isamarkuptrue%
wenzelm@44121	142	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121	143	\ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121	144	%
wenzelm@44121	145	\begin{isamarkuptxt}%
wenzelm@44121	146	Via abbreviation (``let''):%
wenzelm@44121	147	\end{isamarkuptxt}%
wenzelm@44121	148	\isamarkuptrue%
wenzelm@44121	149	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	150	\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ b%
wenzelm@44121	151	\endisatagproof
wenzelm@44121	152	{\isafoldproof}%
wenzelm@44121	153	%
wenzelm@44121	154	\isadelimproof
wenzelm@44121	155	%
wenzelm@44121	156	\endisadelimproof
wenzelm@44121	157	\isanewline
wenzelm@44121	158	\isanewline
wenzelm@44121	159	\isacommand{end}\isamarkupfalse%
wenzelm@44121	160	%
wenzelm@44121	161	\isamarkupsubsubsection{Referencing facts%
wenzelm@44121	162	}
wenzelm@44121	163	\isamarkuptrue%
wenzelm@44121	164	\isacommand{notepad}\isamarkupfalse%
wenzelm@44121	165	\isanewline
wenzelm@44121	166	\isakeyword{begin}%
wenzelm@44121	167	\isadelimproof
wenzelm@44121	168	%
wenzelm@44121	169	\endisadelimproof
wenzelm@44121	170	%
wenzelm@44121	171	\isatagproof
wenzelm@44121	172	%
wenzelm@44121	173	\begin{isamarkuptxt}%
wenzelm@44121	174	Via explicit name:%
wenzelm@44121	175	\end{isamarkuptxt}%
wenzelm@44121	176	\isamarkuptrue%
wenzelm@44121	177	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121	178	\ a{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
wenzelm@44121	179	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	180	\ a%
wenzelm@44121	181	\begin{isamarkuptxt}%
wenzelm@44121	182	Via implicit name:%
wenzelm@44121	183	\end{isamarkuptxt}%
wenzelm@44121	184	\isamarkuptrue%
wenzelm@44121	185	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121	186	\ A\isanewline
wenzelm@44121	187	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	188	\ this%
wenzelm@44121	189	\begin{isamarkuptxt}%
wenzelm@44121	190	Via literal proposition (unification with results from the proof text):%
wenzelm@44121	191	\end{isamarkuptxt}%
wenzelm@44121	192	\isamarkuptrue%
wenzelm@44121	193	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121	194	\ A\isanewline
wenzelm@44121	195	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	196	\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44121	197	\isanewline
wenzelm@44121	198	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121	199	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121	200	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	201	\ {\isaliteral{60}{\isacharbackquoteopen}}B\ a{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44121	202	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	203	\ {\isaliteral{60}{\isacharbackquoteopen}}B\ b{\isaliteral{60}{\isacharbackquoteclose}}%
wenzelm@44121	204	\endisatagproof
wenzelm@44121	205	{\isafoldproof}%
wenzelm@44121	206	%
wenzelm@44121	207	\isadelimproof
wenzelm@44121	208	%
wenzelm@44121	209	\endisadelimproof
wenzelm@44121	210	\isanewline
wenzelm@44121	211	\isacommand{end}\isamarkupfalse%
wenzelm@44121	212	%
wenzelm@44121	213	\isamarkupsubsubsection{Manipulating facts%
wenzelm@44121	214	}
wenzelm@44121	215	\isamarkuptrue%
wenzelm@44121	216	\isacommand{notepad}\isamarkupfalse%
wenzelm@44121	217	\isanewline
wenzelm@44121	218	\isakeyword{begin}%
wenzelm@44121	219	\isadelimproof
wenzelm@44121	220	%
wenzelm@44121	221	\endisadelimproof
wenzelm@44121	222	%
wenzelm@44121	223	\isatagproof
wenzelm@44121	224	%
wenzelm@44121	225	\begin{isamarkuptxt}%
wenzelm@44121	226	Instantiation:%
wenzelm@44121	227	\end{isamarkuptxt}%
wenzelm@44121	228	\isamarkuptrue%
wenzelm@44121	229	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121	230	\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121	231	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	232	\ a\isanewline
wenzelm@44121	233	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	234	\ a\ {\isaliteral{5B}{\isacharbrackleft}}of\ b{\isaliteral{5D}{\isacharbrackright}}\isanewline
wenzelm@44121	235	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	236	\ a\ {\isaliteral{5B}{\isacharbrackleft}}\isakeyword{where}\ x\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5D}{\isacharbrackright}}%
wenzelm@44121	237	\begin{isamarkuptxt}%
wenzelm@44121	238	Backchaining:%
wenzelm@44121	239	\end{isamarkuptxt}%
wenzelm@44121	240	\isamarkuptrue%
wenzelm@44121	241	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121	242	\ {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
wenzelm@44121	243	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121	244	\ {\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121	245	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	246	\ {\isadigit{2}}\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
wenzelm@44121	247	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	248	\ {\isadigit{1}}\ {\isaliteral{5B}{\isacharbrackleft}}THEN\ {\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}%
wenzelm@44121	249	\begin{isamarkuptxt}%
wenzelm@44121	250	Symmetric results:%
wenzelm@44121	251	\end{isamarkuptxt}%
wenzelm@44121	252	\isamarkuptrue%
wenzelm@44121	253	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121	254	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121	255	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	256	\ this\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}\isanewline
wenzelm@44121	257	\isanewline
wenzelm@44121	258	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121	259	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121	260	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	261	\ this\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}%
wenzelm@44121	262	\begin{isamarkuptxt}%
wenzelm@44126	263	Adhoc-simplification (take care!):%
wenzelm@44121	264	\end{isamarkuptxt}%
wenzelm@44121	265	\isamarkuptrue%
wenzelm@44121	266	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44121	267	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44121	268	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	269	\ this\ {\isaliteral{5B}{\isacharbrackleft}}simplified{\isaliteral{5D}{\isacharbrackright}}%
wenzelm@44121	270	\endisatagproof
wenzelm@44121	271	{\isafoldproof}%
wenzelm@44121	272	%
wenzelm@44121	273	\isadelimproof
wenzelm@44121	274	%
wenzelm@44121	275	\endisadelimproof
wenzelm@44121	276	\isanewline
wenzelm@44121	277	\isacommand{end}\isamarkupfalse%
wenzelm@44121	278	%
wenzelm@44121	279	\isamarkupsubsubsection{Projections%
wenzelm@44121	280	}
wenzelm@44121	281	\isamarkuptrue%
wenzelm@44121	282	%
wenzelm@44121	283	\begin{isamarkuptext}%
wenzelm@44121	284	Isar facts consist of multiple theorems. There is notation to project
wenzelm@44121	285	interval ranges.%
wenzelm@44121	286	\end{isamarkuptext}%
wenzelm@44121	287	\isamarkuptrue%
wenzelm@44121	288	\isacommand{notepad}\isamarkupfalse%
wenzelm@44121	289	\isanewline
wenzelm@44121	290	\isakeyword{begin}\isanewline
wenzelm@44121	291	%
wenzelm@44121	292	\isadelimproof
wenzelm@44121	293	\ \ %
wenzelm@44121	294	\endisadelimproof
wenzelm@44121	295	%
wenzelm@44121	296	\isatagproof
wenzelm@44121	297	\isacommand{assume}\isamarkupfalse%
wenzelm@44121	298	\ stuff{\isaliteral{3A}{\isacharcolon}}\ A\ B\ C\ D\isanewline
wenzelm@44121	299	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	300	\ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44121	301	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	302	\ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44121	303	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	304	\ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{29}{\isacharparenright}}%
wenzelm@44121	305	\endisatagproof
wenzelm@44121	306	{\isafoldproof}%
wenzelm@44121	307	%
wenzelm@44121	308	\isadelimproof
wenzelm@44121	309	\isanewline
wenzelm@44121	310	%
wenzelm@44121	311	\endisadelimproof
wenzelm@44121	312	\isacommand{end}\isamarkupfalse%
wenzelm@44121	313	%
wenzelm@44121	314	\isamarkupsubsubsection{Naming conventions%
wenzelm@44121	315	}
wenzelm@44121	316	\isamarkuptrue%
wenzelm@44121	317	%
wenzelm@44121	318	\begin{isamarkuptext}%
wenzelm@44121	319	\begin{itemize}
wenzelm@44121	320
wenzelm@44121	321	\item Lower-case identifiers are usually preferred.
wenzelm@44121	322
wenzelm@44121	323	\item Facts can be named after the main term within the proposition.
wenzelm@44121	324
wenzelm@44121	325	\item Facts should \emph{not} be named after the command that
wenzelm@44121	326	introduced them (\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}). This is
wenzelm@44121	327	misleading and hard to maintain.
wenzelm@44121	328
wenzelm@44121	329	\item Natural numbers can be used as ``meaningless'' names (more
wenzelm@44121	330	appropriate than \isa{{\isaliteral{22}{\isachardoublequote}}a{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}a{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} etc.)
wenzelm@44121	331
wenzelm@44121	332	\item Symbolic identifiers are supported (e.g. \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}).
wenzelm@44121	333
wenzelm@44121	334	\end{itemize}%
wenzelm@44121	335	\end{isamarkuptext}%
wenzelm@44121	336	\isamarkuptrue%
wenzelm@44121	337	%
wenzelm@44121	338	\isamarkupsubsection{Block structure%
wenzelm@44121	339	}
wenzelm@44121	340	\isamarkuptrue%
wenzelm@44121	341	%
wenzelm@44121	342	\begin{isamarkuptext}%
wenzelm@44121	343	The formal notepad is block structured. The fact produced by the last
wenzelm@44121	344	entry of a block is exported into the outer context.%
wenzelm@44121	345	\end{isamarkuptext}%
wenzelm@44121	346	\isamarkuptrue%
wenzelm@44121	347	\isacommand{notepad}\isamarkupfalse%
wenzelm@44121	348	\isanewline
wenzelm@44121	349	\isakeyword{begin}\isanewline
wenzelm@44121	350	%
wenzelm@44121	351	\isadelimproof
wenzelm@44121	352	\ \ %
wenzelm@44121	353	\endisadelimproof
wenzelm@44121	354	%
wenzelm@44121	355	\isatagproof
wenzelm@44121	356	\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121	357	\isanewline
wenzelm@44121	358	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121	359	\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121	360	\isanewline
wenzelm@44121	361	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121	362	\ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121	363	\isanewline
wenzelm@44121	364	\ \ \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	365	\ a\ b\isanewline
wenzelm@44121	366	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121	367	\isanewline
wenzelm@44121	368	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	369	\ this\isanewline
wenzelm@44121	370	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	371	\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44121	372	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44121	373	\ {\isaliteral{60}{\isacharbackquoteopen}}B{\isaliteral{60}{\isacharbackquoteclose}}%
wenzelm@44121	374	\endisatagproof
wenzelm@44121	375	{\isafoldproof}%
wenzelm@44121	376	%
wenzelm@44121	377	\isadelimproof
wenzelm@44121	378	\isanewline
wenzelm@44121	379	%
wenzelm@44121	380	\endisadelimproof
wenzelm@44121	381	\isacommand{end}\isamarkupfalse%
wenzelm@44121	382	%
wenzelm@44121	383	\begin{isamarkuptext}%
wenzelm@44121	384	Explicit blocks as well as implicit blocks of nested goal
wenzelm@44121	385	statements (e.g.\ \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}) automatically introduce one extra
wenzelm@44121	386	pair of parentheses in reserve. The \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} command allows
wenzelm@44122	387	to ``jump'' between these sub-blocks.%
wenzelm@44121	388	\end{isamarkuptext}%
wenzelm@44121	389	\isamarkuptrue%
wenzelm@44121	390	\isacommand{notepad}\isamarkupfalse%
wenzelm@44121	391	\isanewline
wenzelm@44121	392	\isakeyword{begin}\isanewline
wenzelm@44121	393	%
wenzelm@44121	394	\isadelimproof
wenzelm@44121	395	\isanewline
wenzelm@44121	396	\ \ %
wenzelm@44121	397	\endisadelimproof
wenzelm@44121	398	%
wenzelm@44121	399	\isatagproof
wenzelm@44121	400	\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121	401	\isanewline
wenzelm@44121	402	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121	403	\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121	404	\isanewline
wenzelm@44121	405	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44121	406	\isanewline
wenzelm@44121	407	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121	408	\ b{\isaliteral{3A}{\isacharcolon}}\ B\isanewline
wenzelm@44121	409	\ \ \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44121	410	\ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44121	411	\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44121	412	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121	413	\isanewline
wenzelm@44121	414	\ \ \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44121	415	\isanewline
wenzelm@44121	416	\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121	417	\ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121	418	\isanewline
wenzelm@44121	419	\ \ \ \ \isacommand{next}\isamarkupfalse%
wenzelm@44121	420	\isanewline
wenzelm@44121	421	\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121	422	\ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121	423	\isanewline
wenzelm@44121	424	\ \ \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44121	425	\isanewline
wenzelm@44121	426	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121	427	%
wenzelm@44121	428	\begin{isamarkuptxt}%
wenzelm@44121	429	Alternative version with explicit parentheses everywhere:%
wenzelm@44121	430	\end{isamarkuptxt}%
wenzelm@44121	431	\isamarkuptrue%
wenzelm@44121	432	\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121	433	\isanewline
wenzelm@44121	434	\ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121	435	\isanewline
wenzelm@44121	436	\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121	437	\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121	438	\isanewline
wenzelm@44121	439	\ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121	440	\isanewline
wenzelm@44121	441	\ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121	442	\isanewline
wenzelm@44121	443	\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121	444	\ b{\isaliteral{3A}{\isacharcolon}}\ B\isanewline
wenzelm@44121	445	\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44121	446	\ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44121	447	\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121	448	\isanewline
wenzelm@44121	449	\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44121	450	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121	451	\isanewline
wenzelm@44121	452	\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121	453	\isanewline
wenzelm@44121	454	\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121	455	\isanewline
wenzelm@44121	456	\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121	457	\ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121	458	\isanewline
wenzelm@44121	459	\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121	460	\isanewline
wenzelm@44121	461	\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44121	462	\isanewline
wenzelm@44121	463	\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44121	464	\ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44121	465	\isanewline
wenzelm@44121	466	\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121	467	\isanewline
wenzelm@44121	468	\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44121	469	\isanewline
wenzelm@44121	470	\ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121	471	\isanewline
wenzelm@44121	472	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44121	473	%
wenzelm@44121	474	\endisatagproof
wenzelm@44121	475	{\isafoldproof}%
wenzelm@44121	476	%
wenzelm@44121	477	\isadelimproof
wenzelm@44121	478	\isanewline
wenzelm@44121	479	%
wenzelm@44121	480	\endisadelimproof
wenzelm@44121	481	\isanewline
wenzelm@44121	482	\isacommand{end}\isamarkupfalse%
wenzelm@44123	483	%
wenzelm@44125	484	\isamarkupsection{Calculational reasoning \label{sec:calculations-synopsis}%
wenzelm@44123	485	}
wenzelm@44123	486	\isamarkuptrue%
wenzelm@44123	487	%
wenzelm@44123	488	\begin{isamarkuptext}%
wenzelm@44123	489	For example, see \verb\|~~/src/HOL/Isar_Examples/Group.thy\|.%
wenzelm@44123	490	\end{isamarkuptext}%
wenzelm@44123	491	\isamarkuptrue%
wenzelm@44123	492	%
wenzelm@44123	493	\isamarkupsubsection{Special names in Isar proofs%
wenzelm@44123	494	}
wenzelm@44123	495	\isamarkuptrue%
wenzelm@44123	496	%
wenzelm@44123	497	\begin{isamarkuptext}%
wenzelm@44123	498	\begin{itemize}
wenzelm@44123	499
wenzelm@44123	500	\item term \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}thesis{\isaliteral{22}{\isachardoublequote}}} --- the main conclusion of the
wenzelm@44123	501	innermost pending claim
wenzelm@44123	502
wenzelm@44123	503	\item term \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} --- the argument of the last explicitly
wenzelm@44123	504	stated result (for infix application this is the right-hand side)
wenzelm@44123	505
wenzelm@44123	506	\item fact \isa{{\isaliteral{22}{\isachardoublequote}}this{\isaliteral{22}{\isachardoublequote}}} --- the last result produced in the text
wenzelm@44123	507
wenzelm@44123	508	\end{itemize}%
wenzelm@44123	509	\end{isamarkuptext}%
wenzelm@44123	510	\isamarkuptrue%
wenzelm@44123	511	\isacommand{notepad}\isamarkupfalse%
wenzelm@44123	512	\isanewline
wenzelm@44123	513	\isakeyword{begin}\isanewline
wenzelm@44123	514	%
wenzelm@44123	515	\isadelimproof
wenzelm@44123	516	\ \ %
wenzelm@44123	517	\endisadelimproof
wenzelm@44123	518	%
wenzelm@44123	519	\isatagproof
wenzelm@44123	520	\isacommand{have}\isamarkupfalse%
wenzelm@44123	521	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44123	522	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44123	523	\ {\isaliteral{2D}{\isacharminus}}%
wenzelm@44123	524	\endisatagproof
wenzelm@44123	525	{\isafoldproof}%
wenzelm@44123	526	%
wenzelm@44123	527	\isadelimproof
wenzelm@44123	528	\isanewline
wenzelm@44123	529	%
wenzelm@44123	530	\endisadelimproof
wenzelm@44123	531	\ \ \ \ \isacommand{term}\isamarkupfalse%
wenzelm@44123	532	\ {\isaliteral{3F}{\isacharquery}}thesis\isanewline
wenzelm@44123	533	%
wenzelm@44123	534	\isadelimproof
wenzelm@44123	535	\ \ \ \ %
wenzelm@44123	536	\endisadelimproof
wenzelm@44123	537	%
wenzelm@44123	538	\isatagproof
wenzelm@44123	539	\isacommand{show}\isamarkupfalse%
wenzelm@44123	540	\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	541	%
wenzelm@44123	542	\endisatagproof
wenzelm@44123	543	{\isafoldproof}%
wenzelm@44123	544	%
wenzelm@44123	545	\isadelimproof
wenzelm@44123	546	\isanewline
wenzelm@44123	547	%
wenzelm@44123	548	\endisadelimproof
wenzelm@44123	549	\ \ \ \ \isacommand{term}\isamarkupfalse%
wenzelm@44123	550	\ {\isaliteral{3F}{\isacharquery}}thesis\ \ %
wenzelm@44123	551	\isamarkupcmt{static!%
wenzelm@44123	552	}
wenzelm@44123	553	\isanewline
wenzelm@44123	554	%
wenzelm@44123	555	\isadelimproof
wenzelm@44123	556	\ \ %
wenzelm@44123	557	\endisadelimproof
wenzelm@44123	558	%
wenzelm@44123	559	\isatagproof
wenzelm@44123	560	\isacommand{qed}\isamarkupfalse%
wenzelm@44123	561	%
wenzelm@44123	562	\endisatagproof
wenzelm@44123	563	{\isafoldproof}%
wenzelm@44123	564	%
wenzelm@44123	565	\isadelimproof
wenzelm@44123	566	\isanewline
wenzelm@44123	567	%
wenzelm@44123	568	\endisadelimproof
wenzelm@44123	569	\ \ \isacommand{term}\isamarkupfalse%
wenzelm@44123	570	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44123	571	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44123	572	\ this\isanewline
wenzelm@44123	573	\isacommand{end}\isamarkupfalse%
wenzelm@44123	574	%
wenzelm@44123	575	\begin{isamarkuptext}%
wenzelm@44123	576	Calculational reasoning maintains the special fact called
wenzelm@44123	577	``\isa{calculation}'' in the background. Certain language
wenzelm@44123	578	elements combine primary \isa{this} with secondary \isa{calculation}.%
wenzelm@44123	579	\end{isamarkuptext}%
wenzelm@44123	580	\isamarkuptrue%
wenzelm@44123	581	%
wenzelm@44123	582	\isamarkupsubsection{Transitive chains%
wenzelm@44123	583	}
wenzelm@44123	584	\isamarkuptrue%
wenzelm@44123	585	%
wenzelm@44123	586	\begin{isamarkuptext}%
wenzelm@44123	587	The Idea is to combine \isa{this} and \isa{calculation}
wenzelm@44123	588	via typical \isa{trans} rules (see also \hyperlink{command.print-trans-rules}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}trans{\isaliteral{5F}{\isacharunderscore}}rules}}}}):%
wenzelm@44123	589	\end{isamarkuptext}%
wenzelm@44123	590	\isamarkuptrue%
wenzelm@44123	591	\isacommand{thm}\isamarkupfalse%
wenzelm@44123	592	\ trans\isanewline
wenzelm@44123	593	\isacommand{thm}\isamarkupfalse%
wenzelm@44123	594	\ less{\isaliteral{5F}{\isacharunderscore}}trans\isanewline
wenzelm@44123	595	\isacommand{thm}\isamarkupfalse%
wenzelm@44123	596	\ less{\isaliteral{5F}{\isacharunderscore}}le{\isaliteral{5F}{\isacharunderscore}}trans\isanewline
wenzelm@44123	597	\isanewline
wenzelm@44123	598	\isacommand{notepad}\isamarkupfalse%
wenzelm@44123	599	\isanewline
wenzelm@44123	600	\isakeyword{begin}%
wenzelm@44123	601	\isadelimproof
wenzelm@44123	602	%
wenzelm@44123	603	\endisadelimproof
wenzelm@44123	604	%
wenzelm@44123	605	\isatagproof
wenzelm@44123	606	%
wenzelm@44123	607	\begin{isamarkuptxt}%
wenzelm@44123	608	Plain bottom-up calculation:%
wenzelm@44123	609	\end{isamarkuptxt}%
wenzelm@44123	610	\isamarkuptrue%
wenzelm@44123	611	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	612	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	613	\isanewline
wenzelm@44123	614	\ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123	615	\isanewline
wenzelm@44123	616	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	617	\ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	618	\isanewline
wenzelm@44123	619	\ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123	620	\isanewline
wenzelm@44123	621	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	622	\ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	623	\isanewline
wenzelm@44123	624	\ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44123	625	\isanewline
wenzelm@44123	626	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	627	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44123	628	%
wenzelm@44123	629	\begin{isamarkuptxt}%
wenzelm@44123	630	Variant using the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} abbreviation:%
wenzelm@44123	631	\end{isamarkuptxt}%
wenzelm@44123	632	\isamarkuptrue%
wenzelm@44123	633	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	634	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	635	\isanewline
wenzelm@44123	636	\ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123	637	\isanewline
wenzelm@44123	638	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	639	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	640	\isanewline
wenzelm@44123	641	\ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123	642	\isanewline
wenzelm@44123	643	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	644	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	645	\isanewline
wenzelm@44123	646	\ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44123	647	\isanewline
wenzelm@44123	648	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	649	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44123	650	%
wenzelm@44123	651	\begin{isamarkuptxt}%
wenzelm@44123	652	Top-down version with explicit claim at the head:%
wenzelm@44123	653	\end{isamarkuptxt}%
wenzelm@44123	654	\isamarkuptrue%
wenzelm@44123	655	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	656	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44123	657	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44123	658	\ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44123	659	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	660	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	661	\isanewline
wenzelm@44123	662	\ \ \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123	663	\isanewline
wenzelm@44123	664	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	665	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	666	\isanewline
wenzelm@44123	667	\ \ \ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123	668	\isanewline
wenzelm@44123	669	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	670	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	671	\isanewline
wenzelm@44123	672	\ \ \ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44123	673	\isanewline
wenzelm@44123	674	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44123	675	\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44123	676	\isanewline
wenzelm@44123	677	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44123	678	\isanewline
wenzelm@44123	679	\isacommand{next}\isamarkupfalse%
wenzelm@44123	680	%
wenzelm@44123	681	\begin{isamarkuptxt}%
wenzelm@44123	682	Mixed inequalities (require suitable base type):%
wenzelm@44123	683	\end{isamarkuptxt}%
wenzelm@44123	684	\isamarkuptrue%
wenzelm@44123	685	\ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44123	686	\ a\ b\ c\ d\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44123	687	\isanewline
wenzelm@44123	688	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	689	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3C}{\isacharless}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	690	\isanewline
wenzelm@44123	691	\ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123	692	\isanewline
wenzelm@44123	693	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	694	\ {\isaliteral{22}{\isachardoublequoteopen}}b{\isaliteral{5C3C6C653E}{\isasymle}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	695	\isanewline
wenzelm@44123	696	\ \ \isacommand{also}\isamarkupfalse%
wenzelm@44123	697	\isanewline
wenzelm@44123	698	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	699	\ {\isaliteral{22}{\isachardoublequoteopen}}c\ {\isaliteral{3D}{\isacharequal}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	700	\isanewline
wenzelm@44123	701	\ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44123	702	\isanewline
wenzelm@44123	703	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	704	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3C}{\isacharless}}\ d{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44123	705	%
wenzelm@44123	706	\endisatagproof
wenzelm@44123	707	{\isafoldproof}%
wenzelm@44123	708	%
wenzelm@44123	709	\isadelimproof
wenzelm@44123	710	%
wenzelm@44123	711	\endisadelimproof
wenzelm@44123	712	\isanewline
wenzelm@44123	713	\isacommand{end}\isamarkupfalse%
wenzelm@44123	714	%
wenzelm@44123	715	\isamarkupsubsubsection{Notes%
wenzelm@44123	716	}
wenzelm@44123	717	\isamarkuptrue%
wenzelm@44123	718	%
wenzelm@44123	719	\begin{isamarkuptext}%
wenzelm@44123	720	\begin{itemize}
wenzelm@44123	721
wenzelm@44123	722	\item The notion of \isa{trans} rule is very general due to the
wenzelm@44123	723	flexibility of Isabelle/Pure rule composition.
wenzelm@44123	724
wenzelm@44123	725	\item User applications may declare there own rules, with some care
wenzelm@44123	726	about the operational details of higher-order unification.
wenzelm@44123	727
wenzelm@44123	728	\end{itemize}%
wenzelm@44123	729	\end{isamarkuptext}%
wenzelm@44123	730	\isamarkuptrue%
wenzelm@44123	731	%
wenzelm@44123	732	\isamarkupsubsection{Degenerate calculations and bigstep reasoning%
wenzelm@44123	733	}
wenzelm@44123	734	\isamarkuptrue%
wenzelm@44123	735	%
wenzelm@44123	736	\begin{isamarkuptext}%
wenzelm@44123	737	The Idea is to append \isa{this} to \isa{calculation},
wenzelm@44123	738	without rule composition.%
wenzelm@44123	739	\end{isamarkuptext}%
wenzelm@44123	740	\isamarkuptrue%
wenzelm@44123	741	\isacommand{notepad}\isamarkupfalse%
wenzelm@44123	742	\isanewline
wenzelm@44123	743	\isakeyword{begin}%
wenzelm@44123	744	\isadelimproof
wenzelm@44123	745	%
wenzelm@44123	746	\endisadelimproof
wenzelm@44123	747	%
wenzelm@44123	748	\isatagproof
wenzelm@44123	749	%
wenzelm@44123	750	\begin{isamarkuptxt}%
wenzelm@44124	751	A vacuous proof:%
wenzelm@44123	752	\end{isamarkuptxt}%
wenzelm@44123	753	\isamarkuptrue%
wenzelm@44123	754	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	755	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	756	\isanewline
wenzelm@44123	757	\ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123	758	\isanewline
wenzelm@44123	759	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	760	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	761	\isanewline
wenzelm@44123	762	\ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123	763	\isanewline
wenzelm@44123	764	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	765	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	766	\isanewline
wenzelm@44123	767	\ \ \isacommand{ultimately}\isamarkupfalse%
wenzelm@44123	768	\isanewline
wenzelm@44123	769	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	770	\ A\ \isakeyword{and}\ B\ \isakeyword{and}\ C\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44123	771	\isanewline
wenzelm@44123	772	\isacommand{next}\isamarkupfalse%
wenzelm@44123	773	%
wenzelm@44123	774	\begin{isamarkuptxt}%
wenzelm@44123	775	Slightly more content (trivial bigstep reasoning):%
wenzelm@44123	776	\end{isamarkuptxt}%
wenzelm@44123	777	\isamarkuptrue%
wenzelm@44123	778	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	779	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	780	\isanewline
wenzelm@44123	781	\ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123	782	\isanewline
wenzelm@44123	783	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	784	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	785	\isanewline
wenzelm@44123	786	\ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123	787	\isanewline
wenzelm@44123	788	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	789	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	790	\isanewline
wenzelm@44123	791	\ \ \isacommand{ultimately}\isamarkupfalse%
wenzelm@44123	792	\isanewline
wenzelm@44123	793	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	794	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44123	795	\ blast\isanewline
wenzelm@44123	796	\isacommand{next}\isamarkupfalse%
wenzelm@44123	797	%
wenzelm@44123	798	\begin{isamarkuptxt}%
wenzelm@44124	799	More ambitious bigstep reasoning involving structured results:%
wenzelm@44123	800	\end{isamarkuptxt}%
wenzelm@44123	801	\isamarkuptrue%
wenzelm@44123	802	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	803	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	804	\isanewline
wenzelm@44123	805	\ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123	806	\isanewline
wenzelm@44123	807	\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44123	808	\ \isacommand{assume}\isamarkupfalse%
wenzelm@44123	809	\ A\ \isacommand{have}\isamarkupfalse%
wenzelm@44123	810	\ R\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	811	\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44123	812	\isanewline
wenzelm@44123	813	\ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123	814	\isanewline
wenzelm@44123	815	\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44123	816	\ \isacommand{assume}\isamarkupfalse%
wenzelm@44123	817	\ B\ \isacommand{have}\isamarkupfalse%
wenzelm@44123	818	\ R\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	819	\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44123	820	\isanewline
wenzelm@44123	821	\ \ \isacommand{moreover}\isamarkupfalse%
wenzelm@44123	822	\isanewline
wenzelm@44123	823	\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44123	824	\ \isacommand{assume}\isamarkupfalse%
wenzelm@44123	825	\ C\ \isacommand{have}\isamarkupfalse%
wenzelm@44123	826	\ R\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44123	827	\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44123	828	\isanewline
wenzelm@44123	829	\ \ \isacommand{ultimately}\isamarkupfalse%
wenzelm@44123	830	\isanewline
wenzelm@44123	831	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44123	832	\ R\ \isacommand{by}\isamarkupfalse%
wenzelm@44123	833	\ blast\ \ %
wenzelm@44123	834	\isamarkupcmt{``big-bang integration'' of proof blocks (occasionally fragile)%
wenzelm@44123	835	}
wenzelm@44123	836	%
wenzelm@44123	837	\endisatagproof
wenzelm@44123	838	{\isafoldproof}%
wenzelm@44123	839	%
wenzelm@44123	840	\isadelimproof
wenzelm@44123	841	%
wenzelm@44123	842	\endisadelimproof
wenzelm@44123	843	\isanewline
wenzelm@44123	844	\isacommand{end}\isamarkupfalse%
wenzelm@44124	845	%
wenzelm@44127	846	\isamarkupsection{Induction%
wenzelm@44125	847	}
wenzelm@44125	848	\isamarkuptrue%
wenzelm@44125	849	%
wenzelm@44125	850	\isamarkupsubsection{Induction as Natural Deduction%
wenzelm@44125	851	}
wenzelm@44125	852	\isamarkuptrue%
wenzelm@44125	853	%
wenzelm@44125	854	\begin{isamarkuptext}%
wenzelm@44125	855	In principle, induction is just a special case of Natural
wenzelm@44125	856	Deduction (see also \secref{sec:natural-deduction-synopsis}). For
wenzelm@44125	857	example:%
wenzelm@44125	858	\end{isamarkuptext}%
wenzelm@44125	859	\isamarkuptrue%
wenzelm@44125	860	\isacommand{thm}\isamarkupfalse%
wenzelm@44125	861	\ nat{\isaliteral{2E}{\isachardot}}induct\isanewline
wenzelm@44125	862	\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44125	863	\ nat{\isaliteral{2E}{\isachardot}}induct\isanewline
wenzelm@44125	864	\isanewline
wenzelm@44125	865	\isacommand{notepad}\isamarkupfalse%
wenzelm@44125	866	\isanewline
wenzelm@44125	867	\isakeyword{begin}\isanewline
wenzelm@44125	868	%
wenzelm@44125	869	\isadelimproof
wenzelm@44125	870	\ \ %
wenzelm@44125	871	\endisadelimproof
wenzelm@44125	872	%
wenzelm@44125	873	\isatagproof
wenzelm@44125	874	\isacommand{fix}\isamarkupfalse%
wenzelm@44125	875	\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125	876	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125	877	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	878	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125	879	\ {\isaliteral{28}{\isacharparenleft}}rule\ nat{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\ \ %
wenzelm@44125	880	\isamarkupcmt{fragile rule application!%
wenzelm@44125	881	}
wenzelm@44125	882	\isanewline
wenzelm@44125	883	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125	884	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	885	\isanewline
wenzelm@44125	886	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125	887	\isanewline
wenzelm@44125	888	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125	889	\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125	890	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44125	891	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	892	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125	893	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	894	\isanewline
wenzelm@44125	895	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125	896	%
wenzelm@44125	897	\endisatagproof
wenzelm@44125	898	{\isafoldproof}%
wenzelm@44125	899	%
wenzelm@44125	900	\isadelimproof
wenzelm@44125	901	\isanewline
wenzelm@44125	902	%
wenzelm@44125	903	\endisadelimproof
wenzelm@44125	904	\isacommand{end}\isamarkupfalse%
wenzelm@44125	905	%
wenzelm@44125	906	\begin{isamarkuptext}%
wenzelm@44125	907	In practice, much more proof infrastructure is required.
wenzelm@44125	908
wenzelm@44125	909	The proof method \hyperlink{method.induct}{\mbox{\isa{induct}}} provides:
wenzelm@44125	910	\begin{itemize}
wenzelm@44125	911
wenzelm@44125	912	\item implicit rule selection and robust instantiation
wenzelm@44125	913
wenzelm@44125	914	\item context elements via symbolic case names
wenzelm@44125	915
wenzelm@44125	916	\item support for rule-structured induction statements, with local
wenzelm@44125	917	parameters, premises, etc.
wenzelm@44125	918
wenzelm@44125	919	\end{itemize}%
wenzelm@44125	920	\end{isamarkuptext}%
wenzelm@44125	921	\isamarkuptrue%
wenzelm@44125	922	\isacommand{notepad}\isamarkupfalse%
wenzelm@44125	923	\isanewline
wenzelm@44125	924	\isakeyword{begin}\isanewline
wenzelm@44125	925	%
wenzelm@44125	926	\isadelimproof
wenzelm@44125	927	\ \ %
wenzelm@44125	928	\endisadelimproof
wenzelm@44125	929	%
wenzelm@44125	930	\isatagproof
wenzelm@44125	931	\isacommand{fix}\isamarkupfalse%
wenzelm@44125	932	\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125	933	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125	934	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	935	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125	936	\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	937	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	938	\ {\isadigit{0}}\isanewline
wenzelm@44125	939	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125	940	\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	941	\isanewline
wenzelm@44125	942	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125	943	\isanewline
wenzelm@44125	944	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	945	\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	946	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125	947	\ Suc{\isaliteral{2E}{\isachardot}}hyps\ \isacommand{show}\isamarkupfalse%
wenzelm@44125	948	\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	949	\isanewline
wenzelm@44125	950	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125	951	%
wenzelm@44125	952	\endisatagproof
wenzelm@44125	953	{\isafoldproof}%
wenzelm@44125	954	%
wenzelm@44125	955	\isadelimproof
wenzelm@44125	956	\isanewline
wenzelm@44125	957	%
wenzelm@44125	958	\endisadelimproof
wenzelm@44125	959	\isacommand{end}\isamarkupfalse%
wenzelm@44125	960	%
wenzelm@44125	961	\isamarkupsubsubsection{Example%
wenzelm@44125	962	}
wenzelm@44125	963	\isamarkuptrue%
wenzelm@44125	964	%
wenzelm@44125	965	\begin{isamarkuptext}%
wenzelm@44125	966	The subsequent example combines the following proof patterns:
wenzelm@44125	967	\begin{itemize}
wenzelm@44125	968
wenzelm@44125	969	\item outermost induction (over the datatype structure of natural
wenzelm@44125	970	numbers), to decompose the proof problem in top-down manner
wenzelm@44125	971
wenzelm@44125	972	\item calculational reasoning (\secref{sec:calculations-synopsis})
wenzelm@44125	973	to compose the result in each case
wenzelm@44125	974
wenzelm@44125	975	\item solving local claims within the calculation by simplification
wenzelm@44125	976
wenzelm@44125	977	\end{itemize}%
wenzelm@44125	978	\end{isamarkuptext}%
wenzelm@44125	979	\isamarkuptrue%
wenzelm@44125	980	\isacommand{lemma}\isamarkupfalse%
wenzelm@44125	981	\isanewline
wenzelm@44125	982	\ \ \isakeyword{fixes}\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125	983	\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	984	%
wenzelm@44125	985	\isadelimproof
wenzelm@44125	986	%
wenzelm@44125	987	\endisadelimproof
wenzelm@44125	988	%
wenzelm@44125	989	\isatagproof
wenzelm@44125	990	\isacommand{proof}\isamarkupfalse%
wenzelm@44125	991	\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	992	\ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	993	\ {\isadigit{0}}\isanewline
wenzelm@44125	994	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125	995	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44125	996	\ simp\isanewline
wenzelm@44125	997	\ \ \isacommand{also}\isamarkupfalse%
wenzelm@44125	998	\ \isacommand{have}\isamarkupfalse%
wenzelm@44125	999	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44125	1000	\ simp\isanewline
wenzelm@44125	1001	\ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44125	1002	\ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1003	\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44125	1004	\isanewline
wenzelm@44125	1005	\isacommand{next}\isamarkupfalse%
wenzelm@44125	1006	\isanewline
wenzelm@44125	1007	\ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	1008	\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1009	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125	1010	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}Suc\ n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44125	1011	\ simp\isanewline
wenzelm@44125	1012	\ \ \isacommand{also}\isamarkupfalse%
wenzelm@44125	1013	\ \isacommand{have}\isamarkupfalse%
wenzelm@44125	1014	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44125	1015	\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ Suc{\isaliteral{2E}{\isachardot}}hyps{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1016	\ \ \isacommand{also}\isamarkupfalse%
wenzelm@44125	1017	\ \isacommand{have}\isamarkupfalse%
wenzelm@44125	1018	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44125	1019	\ simp\isanewline
wenzelm@44125	1020	\ \ \isacommand{also}\isamarkupfalse%
wenzelm@44125	1021	\ \isacommand{have}\isamarkupfalse%
wenzelm@44125	1022	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ div\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44125	1023	\ simp\isanewline
wenzelm@44125	1024	\ \ \isacommand{finally}\isamarkupfalse%
wenzelm@44125	1025	\ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1026	\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44125	1027	\isanewline
wenzelm@44125	1028	\isacommand{qed}\isamarkupfalse%
wenzelm@44125	1029	%
wenzelm@44125	1030	\endisatagproof
wenzelm@44125	1031	{\isafoldproof}%
wenzelm@44125	1032	%
wenzelm@44125	1033	\isadelimproof
wenzelm@44125	1034	%
wenzelm@44125	1035	\endisadelimproof
wenzelm@44125	1036	%
wenzelm@44125	1037	\begin{isamarkuptext}%
wenzelm@44125	1038	This demonstrates how induction proofs can be done without
wenzelm@44125	1039	having to consider the raw Natural Deduction structure.%
wenzelm@44125	1040	\end{isamarkuptext}%
wenzelm@44125	1041	\isamarkuptrue%
wenzelm@44125	1042	%
wenzelm@44125	1043	\isamarkupsubsection{Induction with local parameters and premises%
wenzelm@44125	1044	}
wenzelm@44125	1045	\isamarkuptrue%
wenzelm@44125	1046	%
wenzelm@44125	1047	\begin{isamarkuptext}%
wenzelm@44125	1048	Idea: Pure rule statements are passed through the induction
wenzelm@44125	1049	rule. This achieves convenient proof patterns, thanks to some
wenzelm@44125	1050	internal trickery in the \hyperlink{method.induct}{\mbox{\isa{induct}}} method.
wenzelm@44125	1051
wenzelm@44125	1052	Important: Using compact HOL formulae with \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} is a
wenzelm@44125	1053	well-known anti-pattern! It would produce useless formal noise.%
wenzelm@44125	1054	\end{isamarkuptext}%
wenzelm@44125	1055	\isamarkuptrue%
wenzelm@44125	1056	\isacommand{notepad}\isamarkupfalse%
wenzelm@44125	1057	\isanewline
wenzelm@44125	1058	\isakeyword{begin}\isanewline
wenzelm@44125	1059	%
wenzelm@44125	1060	\isadelimproof
wenzelm@44125	1061	\ \ %
wenzelm@44125	1062	\endisadelimproof
wenzelm@44125	1063	%
wenzelm@44125	1064	\isatagproof
wenzelm@44125	1065	\isacommand{fix}\isamarkupfalse%
wenzelm@44125	1066	\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125	1067	\ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125	1068	\ P\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1069	\ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125	1070	\ Q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1071	\isanewline
wenzelm@44125	1072	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125	1073	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1074	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125	1075	\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1076	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	1077	\ {\isadigit{0}}\isanewline
wenzelm@44125	1078	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1079	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	1080	\isanewline
wenzelm@44125	1081	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125	1082	\isanewline
wenzelm@44125	1083	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	1084	\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1085	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125	1086	\ {\isaliteral{60}{\isacharbackquoteopen}}P\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1087	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	1088	\isanewline
wenzelm@44125	1089	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125	1090	\isanewline
wenzelm@44125	1091	\isanewline
wenzelm@44125	1092	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125	1093	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1094	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125	1095	\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1096	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	1097	\ {\isadigit{0}}\isanewline
wenzelm@44125	1098	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125	1099	\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isadigit{0}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1100	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	1101	\isanewline
wenzelm@44125	1102	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125	1103	\isanewline
wenzelm@44125	1104	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	1105	\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1106	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125	1107	\ {\isaliteral{60}{\isacharbackquoteopen}}A\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125	1108	\ \ \ \ \ \ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1109	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	1110	\isanewline
wenzelm@44125	1111	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125	1112	\isanewline
wenzelm@44125	1113	\isanewline
wenzelm@44125	1114	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44125	1115	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ Q\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1116	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125	1117	\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1118	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	1119	\ {\isadigit{0}}\isanewline
wenzelm@44125	1120	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1121	\ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	1122	\isanewline
wenzelm@44125	1123	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125	1124	\isanewline
wenzelm@44125	1125	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	1126	\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1127	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125	1128	\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ Q\ x\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1129	\ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	1130	%
wenzelm@44125	1131	\begin{isamarkuptxt}%
wenzelm@44125	1132	Local quantification admits arbitrary instances:%
wenzelm@44125	1133	\end{isamarkuptxt}%
wenzelm@44125	1134	\isamarkuptrue%
wenzelm@44125	1135	\ \ \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44125	1136	\ {\isaliteral{60}{\isacharbackquoteopen}}Q\ a\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}Q\ b\ n{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125	1137	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125	1138	%
wenzelm@44125	1139	\endisatagproof
wenzelm@44125	1140	{\isafoldproof}%
wenzelm@44125	1141	%
wenzelm@44125	1142	\isadelimproof
wenzelm@44125	1143	\isanewline
wenzelm@44125	1144	%
wenzelm@44125	1145	\endisadelimproof
wenzelm@44125	1146	\isacommand{end}\isamarkupfalse%
wenzelm@44125	1147	%
wenzelm@44125	1148	\isamarkupsubsection{Implicit induction context%
wenzelm@44125	1149	}
wenzelm@44125	1150	\isamarkuptrue%
wenzelm@44125	1151	%
wenzelm@44125	1152	\begin{isamarkuptext}%
wenzelm@44125	1153	The \hyperlink{method.induct}{\mbox{\isa{induct}}} method can isolate local parameters and
wenzelm@44125	1154	premises directly from the given statement. This is convenient in
wenzelm@44125	1155	practical applications, but requires some understanding of what is
wenzelm@44125	1156	going on internally (as explained above).%
wenzelm@44125	1157	\end{isamarkuptext}%
wenzelm@44125	1158	\isamarkuptrue%
wenzelm@44125	1159	\isacommand{notepad}\isamarkupfalse%
wenzelm@44125	1160	\isanewline
wenzelm@44125	1161	\isakeyword{begin}\isanewline
wenzelm@44125	1162	%
wenzelm@44125	1163	\isadelimproof
wenzelm@44125	1164	\ \ %
wenzelm@44125	1165	\endisadelimproof
wenzelm@44125	1166	%
wenzelm@44125	1167	\isatagproof
wenzelm@44125	1168	\isacommand{fix}\isamarkupfalse%
wenzelm@44125	1169	\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
wenzelm@44125	1170	\ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125	1171	\ Q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1172	\isanewline
wenzelm@44125	1173	\ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125	1174	\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
wenzelm@44125	1175	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44125	1176	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1177	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44125	1178	\ \isacommand{have}\isamarkupfalse%
wenzelm@44125	1179	\ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1180	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125	1181	\ {\isaliteral{28}{\isacharparenleft}}induct\ n\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1182	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	1183	\ {\isadigit{0}}\isanewline
wenzelm@44125	1184	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125	1185	\ {\isaliteral{60}{\isacharbackquoteopen}}A\ x\ {\isadigit{0}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1186	\ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	1187	\isanewline
wenzelm@44125	1188	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125	1189	\isanewline
wenzelm@44125	1190	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	1191	\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1192	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44125	1193	\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ x\ n{\isaliteral{60}{\isacharbackquoteclose}}\ \ %
wenzelm@44125	1194	\isamarkupcmt{arbitrary instances can be produced here%
wenzelm@44125	1195	}
wenzelm@44125	1196	\isanewline
wenzelm@44125	1197	\ \ \ \ \ \ \isakeyword{and}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1198	\ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	1199	\isanewline
wenzelm@44125	1200	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125	1201	%
wenzelm@44125	1202	\endisatagproof
wenzelm@44125	1203	{\isafoldproof}%
wenzelm@44125	1204	%
wenzelm@44125	1205	\isadelimproof
wenzelm@44125	1206	\isanewline
wenzelm@44125	1207	%
wenzelm@44125	1208	\endisadelimproof
wenzelm@44125	1209	\isacommand{end}\isamarkupfalse%
wenzelm@44125	1210	%
wenzelm@44125	1211	\isamarkupsubsection{Advanced induction with term definitions%
wenzelm@44125	1212	}
wenzelm@44125	1213	\isamarkuptrue%
wenzelm@44125	1214	%
wenzelm@44125	1215	\begin{isamarkuptext}%
wenzelm@44125	1216	Induction over subexpressions of a certain shape are delicate
wenzelm@44125	1217	to formalize. The Isar \hyperlink{method.induct}{\mbox{\isa{induct}}} method provides
wenzelm@44125	1218	infrastructure for this.
wenzelm@44125	1219
wenzelm@44125	1220	Idea: sub-expressions of the problem are turned into a defined
wenzelm@44125	1221	induction variable; often accompanied with fixing of auxiliary
wenzelm@44125	1222	parameters in the original expression.%
wenzelm@44125	1223	\end{isamarkuptext}%
wenzelm@44125	1224	\isamarkuptrue%
wenzelm@44125	1225	\isacommand{notepad}\isamarkupfalse%
wenzelm@44125	1226	\isanewline
wenzelm@44125	1227	\isakeyword{begin}\isanewline
wenzelm@44125	1228	%
wenzelm@44125	1229	\isadelimproof
wenzelm@44125	1230	\ \ %
wenzelm@44125	1231	\endisadelimproof
wenzelm@44125	1232	%
wenzelm@44125	1233	\isatagproof
wenzelm@44125	1234	\isacommand{fix}\isamarkupfalse%
wenzelm@44125	1235	\ a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1236	\ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44125	1237	\ A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1238	\isanewline
wenzelm@44125	1239	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44125	1240	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1241	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44125	1242	\ \isacommand{have}\isamarkupfalse%
wenzelm@44125	1243	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44125	1244	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44125	1245	\ {\isaliteral{28}{\isacharparenleft}}induct\ {\isaliteral{22}{\isachardoublequoteopen}}a\ x{\isaliteral{22}{\isachardoublequoteclose}}\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1246	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	1247	\ {\isadigit{0}}\isanewline
wenzelm@44125	1248	\ \ \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44125	1249	\ prem\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125	1250	\ \ \ \ \ \ \isakeyword{and}\ defn\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ a\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125	1251	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1252	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	1253	\isanewline
wenzelm@44125	1254	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44125	1255	\isanewline
wenzelm@44125	1256	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44125	1257	\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44125	1258	\ \ \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44125	1259	\ hyp\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ a\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125	1260	\ \ \ \ \ \ \isakeyword{and}\ prem\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125	1261	\ \ \ \ \ \ \isakeyword{and}\ defn\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{60}{\isacharbackquoteopen}}Suc\ n\ {\isaliteral{3D}{\isacharequal}}\ a\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44125	1262	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44125	1263	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}a\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44125	1264	\isanewline
wenzelm@44125	1265	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44125	1266	%
wenzelm@44125	1267	\endisatagproof
wenzelm@44125	1268	{\isafoldproof}%
wenzelm@44125	1269	%
wenzelm@44125	1270	\isadelimproof
wenzelm@44125	1271	\isanewline
wenzelm@44125	1272	%
wenzelm@44125	1273	\endisadelimproof
wenzelm@44125	1274	\isacommand{end}\isamarkupfalse%
wenzelm@44125	1275	%
wenzelm@44127	1276	\isamarkupsection{Natural Deduction \label{sec:natural-deduction-synopsis}%
wenzelm@44124	1277	}
wenzelm@44124	1278	\isamarkuptrue%
wenzelm@44124	1279	%
wenzelm@44124	1280	\isamarkupsubsection{Rule statements%
wenzelm@44124	1281	}
wenzelm@44124	1282	\isamarkuptrue%
wenzelm@44124	1283	%
wenzelm@44124	1284	\begin{isamarkuptext}%
wenzelm@44124	1285	Isabelle/Pure ``theorems'' are always natural deduction rules,
wenzelm@44124	1286	which sometimes happen to consist of a conclusion only.
wenzelm@44124	1287
wenzelm@44124	1288	The framework connectives \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} indicate the
wenzelm@44124	1289	rule structure declaratively. For example:%
wenzelm@44124	1290	\end{isamarkuptext}%
wenzelm@44124	1291	\isamarkuptrue%
wenzelm@44124	1292	\isacommand{thm}\isamarkupfalse%
wenzelm@44124	1293	\ conjI\isanewline
wenzelm@44124	1294	\isacommand{thm}\isamarkupfalse%
wenzelm@44124	1295	\ impI\isanewline
wenzelm@44124	1296	\isacommand{thm}\isamarkupfalse%
wenzelm@44124	1297	\ nat{\isaliteral{2E}{\isachardot}}induct%
wenzelm@44124	1298	\begin{isamarkuptext}%
wenzelm@44124	1299	The object-logic is embedded into the Pure framework via an implicit
wenzelm@44124	1300	derivability judgment \isa{{\isaliteral{22}{\isachardoublequote}}Trueprop\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@44124	1301
wenzelm@44124	1302	Thus any HOL formulae appears atomic to the Pure framework, while
wenzelm@44124	1303	the rule structure outlines the corresponding proof pattern.
wenzelm@44124	1304
wenzelm@44124	1305	This can be made explicit as follows:%
wenzelm@44124	1306	\end{isamarkuptext}%
wenzelm@44124	1307	\isamarkuptrue%
wenzelm@44124	1308	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1309	\isanewline
wenzelm@44124	1310	\isakeyword{begin}\isanewline
wenzelm@44124	1311	%
wenzelm@44124	1312	\isadelimproof
wenzelm@44124	1313	\ \ %
wenzelm@44124	1314	\endisadelimproof
wenzelm@44124	1315	%
wenzelm@44124	1316	\isatagproof
wenzelm@44124	1317	\isacommand{write}\isamarkupfalse%
wenzelm@44124	1318	\ Trueprop\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}Tr{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
wenzelm@44124	1319	\endisatagproof
wenzelm@44124	1320	{\isafoldproof}%
wenzelm@44124	1321	%
wenzelm@44124	1322	\isadelimproof
wenzelm@44124	1323	\isanewline
wenzelm@44124	1324	%
wenzelm@44124	1325	\endisadelimproof
wenzelm@44124	1326	\isanewline
wenzelm@44124	1327	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1328	\ conjI\isanewline
wenzelm@44124	1329	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1330	\ impI\isanewline
wenzelm@44124	1331	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1332	\ nat{\isaliteral{2E}{\isachardot}}induct\isanewline
wenzelm@44124	1333	\isacommand{end}\isamarkupfalse%
wenzelm@44124	1334	%
wenzelm@44124	1335	\begin{isamarkuptext}%
wenzelm@44124	1336	Isar provides first-class notation for rule statements as follows.%
wenzelm@44124	1337	\end{isamarkuptext}%
wenzelm@44124	1338	\isamarkuptrue%
wenzelm@44124	1339	\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44124	1340	\ conjI\isanewline
wenzelm@44124	1341	\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44124	1342	\ impI\isanewline
wenzelm@44124	1343	\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44124	1344	\ nat{\isaliteral{2E}{\isachardot}}induct%
wenzelm@44124	1345	\isamarkupsubsubsection{Examples%
wenzelm@44124	1346	}
wenzelm@44124	1347	\isamarkuptrue%
wenzelm@44124	1348	%
wenzelm@44124	1349	\begin{isamarkuptext}%
wenzelm@44124	1350	Introductions and eliminations of some standard connectives of
wenzelm@44124	1351	the object-logic can be written as rule statements as follows. (The
wenzelm@44124	1352	proof ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.blast}{\mbox{\isa{blast}}}'' serves as sanity check.)%
wenzelm@44124	1353	\end{isamarkuptext}%
wenzelm@44124	1354	\isamarkuptrue%
wenzelm@44124	1355	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1356	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1357	\isadelimproof
wenzelm@44124	1358	\ %
wenzelm@44124	1359	\endisadelimproof
wenzelm@44124	1360	%
wenzelm@44124	1361	\isatagproof
wenzelm@44124	1362	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1363	\ blast%
wenzelm@44124	1364	\endisatagproof
wenzelm@44124	1365	{\isafoldproof}%
wenzelm@44124	1366	%
wenzelm@44124	1367	\isadelimproof
wenzelm@44124	1368	%
wenzelm@44124	1369	\endisadelimproof
wenzelm@44124	1370	\isanewline
wenzelm@44124	1371	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1372	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1373	\isadelimproof
wenzelm@44124	1374	\ %
wenzelm@44124	1375	\endisadelimproof
wenzelm@44124	1376	%
wenzelm@44124	1377	\isatagproof
wenzelm@44124	1378	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1379	\ blast%
wenzelm@44124	1380	\endisatagproof
wenzelm@44124	1381	{\isafoldproof}%
wenzelm@44124	1382	%
wenzelm@44124	1383	\isadelimproof
wenzelm@44124	1384	%
wenzelm@44124	1385	\endisadelimproof
wenzelm@44124	1386	\isanewline
wenzelm@44124	1387	\isanewline
wenzelm@44124	1388	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1389	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1390	\isadelimproof
wenzelm@44124	1391	\ %
wenzelm@44124	1392	\endisadelimproof
wenzelm@44124	1393	%
wenzelm@44124	1394	\isatagproof
wenzelm@44124	1395	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1396	\ blast%
wenzelm@44124	1397	\endisatagproof
wenzelm@44124	1398	{\isafoldproof}%
wenzelm@44124	1399	%
wenzelm@44124	1400	\isadelimproof
wenzelm@44124	1401	%
wenzelm@44124	1402	\endisadelimproof
wenzelm@44124	1403	\isanewline
wenzelm@44124	1404	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1405	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1406	\isadelimproof
wenzelm@44124	1407	\ %
wenzelm@44124	1408	\endisadelimproof
wenzelm@44124	1409	%
wenzelm@44124	1410	\isatagproof
wenzelm@44124	1411	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1412	\ blast%
wenzelm@44124	1413	\endisatagproof
wenzelm@44124	1414	{\isafoldproof}%
wenzelm@44124	1415	%
wenzelm@44124	1416	\isadelimproof
wenzelm@44124	1417	%
wenzelm@44124	1418	\endisadelimproof
wenzelm@44124	1419	\isanewline
wenzelm@44124	1420	\isanewline
wenzelm@44124	1421	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1422	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1423	\isadelimproof
wenzelm@44124	1424	\ %
wenzelm@44124	1425	\endisadelimproof
wenzelm@44124	1426	%
wenzelm@44124	1427	\isatagproof
wenzelm@44124	1428	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1429	\ blast%
wenzelm@44124	1430	\endisatagproof
wenzelm@44124	1431	{\isafoldproof}%
wenzelm@44124	1432	%
wenzelm@44124	1433	\isadelimproof
wenzelm@44124	1434	%
wenzelm@44124	1435	\endisadelimproof
wenzelm@44124	1436	\isanewline
wenzelm@44124	1437	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1438	\ {\isaliteral{22}{\isachardoublequoteopen}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1439	\isadelimproof
wenzelm@44124	1440	\ %
wenzelm@44124	1441	\endisadelimproof
wenzelm@44124	1442	%
wenzelm@44124	1443	\isatagproof
wenzelm@44124	1444	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1445	\ blast%
wenzelm@44124	1446	\endisatagproof
wenzelm@44124	1447	{\isafoldproof}%
wenzelm@44124	1448	%
wenzelm@44124	1449	\isadelimproof
wenzelm@44124	1450	%
wenzelm@44124	1451	\endisadelimproof
wenzelm@44124	1452	\isanewline
wenzelm@44124	1453	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1454	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1455	\isadelimproof
wenzelm@44124	1456	\ %
wenzelm@44124	1457	\endisadelimproof
wenzelm@44124	1458	%
wenzelm@44124	1459	\isatagproof
wenzelm@44124	1460	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1461	\ blast%
wenzelm@44124	1462	\endisatagproof
wenzelm@44124	1463	{\isafoldproof}%
wenzelm@44124	1464	%
wenzelm@44124	1465	\isadelimproof
wenzelm@44124	1466	%
wenzelm@44124	1467	\endisadelimproof
wenzelm@44124	1468	\isanewline
wenzelm@44124	1469	\isanewline
wenzelm@44124	1470	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1471	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1472	\isadelimproof
wenzelm@44124	1473	\ %
wenzelm@44124	1474	\endisadelimproof
wenzelm@44124	1475	%
wenzelm@44124	1476	\isatagproof
wenzelm@44124	1477	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1478	\ blast%
wenzelm@44124	1479	\endisatagproof
wenzelm@44124	1480	{\isafoldproof}%
wenzelm@44124	1481	%
wenzelm@44124	1482	\isadelimproof
wenzelm@44124	1483	%
wenzelm@44124	1484	\endisadelimproof
wenzelm@44124	1485	\isanewline
wenzelm@44124	1486	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1487	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1488	\isadelimproof
wenzelm@44124	1489	\ %
wenzelm@44124	1490	\endisadelimproof
wenzelm@44124	1491	%
wenzelm@44124	1492	\isatagproof
wenzelm@44124	1493	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1494	\ blast%
wenzelm@44124	1495	\endisatagproof
wenzelm@44124	1496	{\isafoldproof}%
wenzelm@44124	1497	%
wenzelm@44124	1498	\isadelimproof
wenzelm@44124	1499	%
wenzelm@44124	1500	\endisadelimproof
wenzelm@44124	1501	\isanewline
wenzelm@44124	1502	\isanewline
wenzelm@44124	1503	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1504	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1505	\isadelimproof
wenzelm@44124	1506	\ %
wenzelm@44124	1507	\endisadelimproof
wenzelm@44124	1508	%
wenzelm@44124	1509	\isatagproof
wenzelm@44124	1510	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1511	\ blast%
wenzelm@44124	1512	\endisatagproof
wenzelm@44124	1513	{\isafoldproof}%
wenzelm@44124	1514	%
wenzelm@44124	1515	\isadelimproof
wenzelm@44124	1516	%
wenzelm@44124	1517	\endisadelimproof
wenzelm@44124	1518	\isanewline
wenzelm@44124	1519	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1520	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1521	\isadelimproof
wenzelm@44124	1522	\ %
wenzelm@44124	1523	\endisadelimproof
wenzelm@44124	1524	%
wenzelm@44124	1525	\isatagproof
wenzelm@44124	1526	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1527	\ blast%
wenzelm@44124	1528	\endisatagproof
wenzelm@44124	1529	{\isafoldproof}%
wenzelm@44124	1530	%
wenzelm@44124	1531	\isadelimproof
wenzelm@44124	1532	%
wenzelm@44124	1533	\endisadelimproof
wenzelm@44124	1534	\isanewline
wenzelm@44124	1535	\isanewline
wenzelm@44124	1536	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1537	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1538	\isadelimproof
wenzelm@44124	1539	\ %
wenzelm@44124	1540	\endisadelimproof
wenzelm@44124	1541	%
wenzelm@44124	1542	\isatagproof
wenzelm@44124	1543	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1544	\ blast%
wenzelm@44124	1545	\endisatagproof
wenzelm@44124	1546	{\isafoldproof}%
wenzelm@44124	1547	%
wenzelm@44124	1548	\isadelimproof
wenzelm@44124	1549	%
wenzelm@44124	1550	\endisadelimproof
wenzelm@44124	1551	\isanewline
wenzelm@44124	1552	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1553	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1554	\isadelimproof
wenzelm@44124	1555	\ %
wenzelm@44124	1556	\endisadelimproof
wenzelm@44124	1557	%
wenzelm@44124	1558	\isatagproof
wenzelm@44124	1559	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1560	\ blast%
wenzelm@44124	1561	\endisatagproof
wenzelm@44124	1562	{\isafoldproof}%
wenzelm@44124	1563	%
wenzelm@44124	1564	\isadelimproof
wenzelm@44124	1565	%
wenzelm@44124	1566	\endisadelimproof
wenzelm@44124	1567	\isanewline
wenzelm@44124	1568	\isanewline
wenzelm@44124	1569	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1570	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1571	\isadelimproof
wenzelm@44124	1572	\ %
wenzelm@44124	1573	\endisadelimproof
wenzelm@44124	1574	%
wenzelm@44124	1575	\isatagproof
wenzelm@44124	1576	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1577	\ blast%
wenzelm@44124	1578	\endisatagproof
wenzelm@44124	1579	{\isafoldproof}%
wenzelm@44124	1580	%
wenzelm@44124	1581	\isadelimproof
wenzelm@44124	1582	%
wenzelm@44124	1583	\endisadelimproof
wenzelm@44124	1584	\isanewline
wenzelm@44124	1585	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1586	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1587	\isadelimproof
wenzelm@44124	1588	\ %
wenzelm@44124	1589	\endisadelimproof
wenzelm@44124	1590	%
wenzelm@44124	1591	\isatagproof
wenzelm@44124	1592	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1593	\ blast%
wenzelm@44124	1594	\endisatagproof
wenzelm@44124	1595	{\isafoldproof}%
wenzelm@44124	1596	%
wenzelm@44124	1597	\isadelimproof
wenzelm@44124	1598	%
wenzelm@44124	1599	\endisadelimproof
wenzelm@44124	1600	\isanewline
wenzelm@44124	1601	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1602	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1603	\isadelimproof
wenzelm@44124	1604	\ %
wenzelm@44124	1605	\endisadelimproof
wenzelm@44124	1606	%
wenzelm@44124	1607	\isatagproof
wenzelm@44124	1608	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1609	\ blast%
wenzelm@44124	1610	\endisatagproof
wenzelm@44124	1611	{\isafoldproof}%
wenzelm@44124	1612	%
wenzelm@44124	1613	\isadelimproof
wenzelm@44124	1614	%
wenzelm@44124	1615	\endisadelimproof
wenzelm@44124	1616	%
wenzelm@44124	1617	\isamarkupsubsection{Isar context elements%
wenzelm@44124	1618	}
wenzelm@44124	1619	\isamarkuptrue%
wenzelm@44124	1620	%
wenzelm@44124	1621	\begin{isamarkuptext}%
wenzelm@44124	1622	We derive some results out of the blue, using Isar context
wenzelm@44124	1623	elements and some explicit blocks. This illustrates their meaning
wenzelm@44124	1624	wrt.\ Pure connectives, without goal states getting in the way.%
wenzelm@44124	1625	\end{isamarkuptext}%
wenzelm@44124	1626	\isamarkuptrue%
wenzelm@44124	1627	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1628	\isanewline
wenzelm@44124	1629	\isakeyword{begin}\isanewline
wenzelm@44124	1630	%
wenzelm@44124	1631	\isadelimproof
wenzelm@44124	1632	\ \ %
wenzelm@44124	1633	\endisadelimproof
wenzelm@44124	1634	%
wenzelm@44124	1635	\isatagproof
wenzelm@44124	1636	\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124	1637	\isanewline
wenzelm@44124	1638	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	1639	\ x\isanewline
wenzelm@44124	1640	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1641	\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1642	\isanewline
wenzelm@44124	1643	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124	1644	\isanewline
wenzelm@44124	1645	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1646	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44124	1647	\ fact\isanewline
wenzelm@44124	1648	\isanewline
wenzelm@44124	1649	\isacommand{next}\isamarkupfalse%
wenzelm@44124	1650	\isanewline
wenzelm@44124	1651	\isanewline
wenzelm@44124	1652	\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124	1653	\isanewline
wenzelm@44124	1654	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1655	\ A\isanewline
wenzelm@44124	1656	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1657	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1658	\isanewline
wenzelm@44124	1659	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124	1660	\isanewline
wenzelm@44124	1661	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1662	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44124	1663	\ fact\isanewline
wenzelm@44124	1664	\isanewline
wenzelm@44124	1665	\isacommand{next}\isamarkupfalse%
wenzelm@44124	1666	\isanewline
wenzelm@44124	1667	\isanewline
wenzelm@44124	1668	\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124	1669	\isanewline
wenzelm@44124	1670	\ \ \ \ \isacommand{def}\isamarkupfalse%
wenzelm@44124	1671	\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\isanewline
wenzelm@44124	1672	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1673	\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1674	\isanewline
wenzelm@44124	1675	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124	1676	\isanewline
wenzelm@44124	1677	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1678	\ {\isaliteral{22}{\isachardoublequoteopen}}B\ t{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44124	1679	\ fact\isanewline
wenzelm@44124	1680	\isanewline
wenzelm@44124	1681	\isacommand{next}\isamarkupfalse%
wenzelm@44124	1682	\isanewline
wenzelm@44124	1683	\isanewline
wenzelm@44124	1684	\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124	1685	\isanewline
wenzelm@44124	1686	\ \ \ \ \isacommand{obtain}\isamarkupfalse%
wenzelm@44124	1687	\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1688	\isanewline
wenzelm@44124	1689	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1690	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1691	\isanewline
wenzelm@44124	1692	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124	1693	\isanewline
wenzelm@44124	1694	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1695	\ C\ \isacommand{by}\isamarkupfalse%
wenzelm@44124	1696	\ fact%
wenzelm@44124	1697	\endisatagproof
wenzelm@44124	1698	{\isafoldproof}%
wenzelm@44124	1699	%
wenzelm@44124	1700	\isadelimproof
wenzelm@44124	1701	\isanewline
wenzelm@44124	1702	%
wenzelm@44124	1703	\endisadelimproof
wenzelm@44124	1704	\isanewline
wenzelm@44124	1705	\isacommand{end}\isamarkupfalse%
wenzelm@44124	1706	%
wenzelm@44124	1707	\isamarkupsubsection{Pure rule composition%
wenzelm@44124	1708	}
wenzelm@44124	1709	\isamarkuptrue%
wenzelm@44124	1710	%
wenzelm@44124	1711	\begin{isamarkuptext}%
wenzelm@44124	1712	The Pure framework provides means for:
wenzelm@44124	1713
wenzelm@44124	1714	\begin{itemize}
wenzelm@44124	1715
wenzelm@44124	1716	\item backward-chaining of rules by \hyperlink{inference.resolution}{\mbox{\isa{resolution}}}
wenzelm@44124	1717
wenzelm@44124	1718	\item closing of branches by \hyperlink{inference.assumption}{\mbox{\isa{assumption}}}
wenzelm@44124	1719
wenzelm@44124	1720	\end{itemize}
wenzelm@44124	1721
wenzelm@44124	1722	Both principles involve higher-order unification of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms
wenzelm@44124	1723	modulo \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-equivalence (cf.\ Huet and Miller).%
wenzelm@44124	1724	\end{isamarkuptext}%
wenzelm@44124	1725	\isamarkuptrue%
wenzelm@44124	1726	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1727	\isanewline
wenzelm@44124	1728	\isakeyword{begin}\isanewline
wenzelm@44124	1729	%
wenzelm@44124	1730	\isadelimproof
wenzelm@44124	1731	\ \ %
wenzelm@44124	1732	\endisadelimproof
wenzelm@44124	1733	%
wenzelm@44124	1734	\isatagproof
wenzelm@44124	1735	\isacommand{assume}\isamarkupfalse%
wenzelm@44124	1736	\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ B%
wenzelm@44124	1737	\endisatagproof
wenzelm@44124	1738	{\isafoldproof}%
wenzelm@44124	1739	%
wenzelm@44124	1740	\isadelimproof
wenzelm@44124	1741	\isanewline
wenzelm@44124	1742	%
wenzelm@44124	1743	\endisadelimproof
wenzelm@44124	1744	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1745	\ conjI\isanewline
wenzelm@44124	1746	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1747	\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{5D}{\isacharbrackright}}\ \ %
wenzelm@44124	1748	\isamarkupcmt{instantiation%
wenzelm@44124	1749	}
wenzelm@44124	1750	\isanewline
wenzelm@44124	1751	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1752	\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{2C}{\isacharcomma}}\ OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ %
wenzelm@44124	1753	\isamarkupcmt{instantiation and composition%
wenzelm@44124	1754	}
wenzelm@44124	1755	\isanewline
wenzelm@44124	1756	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1757	\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ %
wenzelm@44124	1758	\isamarkupcmt{composition via unification (trivial)%
wenzelm@44124	1759	}
wenzelm@44124	1760	\isanewline
wenzelm@44124	1761	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1762	\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ {\isaliteral{60}{\isacharbackquoteopen}}B{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
wenzelm@44124	1763	\isanewline
wenzelm@44124	1764	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1765	\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ disjI{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
wenzelm@44124	1766	\isacommand{end}\isamarkupfalse%
wenzelm@44124	1767	%
wenzelm@44124	1768	\begin{isamarkuptext}%
wenzelm@44124	1769	Note: Low-level rule composition is tedious and leads to
wenzelm@44124	1770	unreadable~/ unmaintainable expressions in the text.%
wenzelm@44124	1771	\end{isamarkuptext}%
wenzelm@44124	1772	\isamarkuptrue%
wenzelm@44124	1773	%
wenzelm@44124	1774	\isamarkupsubsection{Structured backward reasoning%
wenzelm@44124	1775	}
wenzelm@44124	1776	\isamarkuptrue%
wenzelm@44124	1777	%
wenzelm@44124	1778	\begin{isamarkuptext}%
wenzelm@44124	1779	Idea: Canonical proof decomposition via \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~/
wenzelm@44124	1780	\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~/ \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, where the body produces a
wenzelm@44124	1781	natural deduction rule to refine some goal.%
wenzelm@44124	1782	\end{isamarkuptext}%
wenzelm@44124	1783	\isamarkuptrue%
wenzelm@44124	1784	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1785	\isanewline
wenzelm@44124	1786	\isakeyword{begin}\isanewline
wenzelm@44124	1787	%
wenzelm@44124	1788	\isadelimproof
wenzelm@44124	1789	\ \ %
wenzelm@44124	1790	\endisadelimproof
wenzelm@44124	1791	%
wenzelm@44124	1792	\isatagproof
wenzelm@44124	1793	\isacommand{fix}\isamarkupfalse%
wenzelm@44124	1794	\ A\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1795	\isanewline
wenzelm@44124	1796	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1797	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1798	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1799	\ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44124	1800	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	1801	\ x\isanewline
wenzelm@44124	1802	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1803	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1804	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1805	\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1806	\isanewline
wenzelm@44124	1807	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1808	\isanewline
wenzelm@44124	1809	\isanewline
wenzelm@44124	1810	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1811	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1812	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1813	\ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44124	1814	\ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124	1815	\isanewline
wenzelm@44124	1816	\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	1817	\ x\isanewline
wenzelm@44124	1818	\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1819	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1820	\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1821	\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1822	\isanewline
wenzelm@44124	1823	\ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124	1824	\ %
wenzelm@44124	1825	\isamarkupcmt{implicit block structure made explicit%
wenzelm@44124	1826	}
wenzelm@44124	1827	\isanewline
wenzelm@44124	1828	\ \ \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44124	1829	\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44124	1830	\ \ \ \ \ \ %
wenzelm@44124	1831	\isamarkupcmt{side exit for the resulting rule%
wenzelm@44124	1832	}
wenzelm@44124	1833	\isanewline
wenzelm@44124	1834	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1835	%
wenzelm@44124	1836	\endisatagproof
wenzelm@44124	1837	{\isafoldproof}%
wenzelm@44124	1838	%
wenzelm@44124	1839	\isadelimproof
wenzelm@44124	1840	\isanewline
wenzelm@44124	1841	%
wenzelm@44124	1842	\endisadelimproof
wenzelm@44124	1843	\isacommand{end}\isamarkupfalse%
wenzelm@44124	1844	%
wenzelm@44124	1845	\isamarkupsubsection{Structured rule application%
wenzelm@44124	1846	}
wenzelm@44124	1847	\isamarkuptrue%
wenzelm@44124	1848	%
wenzelm@44124	1849	\begin{isamarkuptext}%
wenzelm@44124	1850	Idea: Previous facts and new claims are composed with a rule from
wenzelm@44124	1851	the context (or background library).%
wenzelm@44124	1852	\end{isamarkuptext}%
wenzelm@44124	1853	\isamarkuptrue%
wenzelm@44124	1854	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1855	\isanewline
wenzelm@44124	1856	\isakeyword{begin}\isanewline
wenzelm@44124	1857	%
wenzelm@44124	1858	\isadelimproof
wenzelm@44124	1859	\ \ %
wenzelm@44124	1860	\endisadelimproof
wenzelm@44124	1861	%
wenzelm@44124	1862	\isatagproof
wenzelm@44124	1863	\isacommand{assume}\isamarkupfalse%
wenzelm@44124	1864	\ r{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
wenzelm@44124	1865	\isamarkupcmt{simple rule (Horn clause)%
wenzelm@44124	1866	}
wenzelm@44124	1867	\isanewline
wenzelm@44124	1868	\isanewline
wenzelm@44124	1869	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1870	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1871	\ \ %
wenzelm@44124	1872	\isamarkupcmt{prefix of facts via outer sub-proof%
wenzelm@44124	1873	}
wenzelm@44124	1874	\isanewline
wenzelm@44124	1875	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1876	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1877	\ C\isanewline
wenzelm@44124	1878	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1879	\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124	1880	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1881	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1882	\ \ %
wenzelm@44124	1883	\isamarkupcmt{remaining rule premises via inner sub-proof%
wenzelm@44124	1884	}
wenzelm@44124	1885	\isanewline
wenzelm@44124	1886	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1887	\isanewline
wenzelm@44124	1888	\isanewline
wenzelm@44124	1889	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1890	\ C\isanewline
wenzelm@44124	1891	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1892	\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124	1893	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1894	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1895	\isanewline
wenzelm@44124	1896	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1897	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1898	\isanewline
wenzelm@44124	1899	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1900	\isanewline
wenzelm@44124	1901	\isanewline
wenzelm@44124	1902	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1903	\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1904	\isanewline
wenzelm@44124	1905	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1906	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1907	\ C\isanewline
wenzelm@44124	1908	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1909	\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124	1910	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1911	\isanewline
wenzelm@44124	1912	\isanewline
wenzelm@44124	1913	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1914	\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1915	\isanewline
wenzelm@44124	1916	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1917	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1918	\ C\ \isacommand{by}\isamarkupfalse%
wenzelm@44124	1919	\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124	1920	\isanewline
wenzelm@44124	1921	\isacommand{next}\isamarkupfalse%
wenzelm@44124	1922	\isanewline
wenzelm@44124	1923	\isanewline
wenzelm@44124	1924	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1925	\ r{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B{\isadigit{1}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isadigit{2}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
wenzelm@44124	1926	\isamarkupcmt{nested rule%
wenzelm@44124	1927	}
wenzelm@44124	1928	\isanewline
wenzelm@44124	1929	\isanewline
wenzelm@44124	1930	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1931	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1932	\isanewline
wenzelm@44124	1933	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1934	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1935	\ C\isanewline
wenzelm@44124	1936	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1937	\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124	1938	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	1939	\ x\isanewline
wenzelm@44124	1940	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1941	\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1942	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1943	\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1944	\isanewline
wenzelm@44124	1945	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1946	%
wenzelm@44124	1947	\begin{isamarkuptxt}%
wenzelm@44124	1948	The compound rule premise \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B{\isadigit{1}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isadigit{2}}\ x{\isaliteral{22}{\isachardoublequote}}} is better
wenzelm@44124	1949	addressed via \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~/ \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~/ \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}
wenzelm@44124	1950	in the nested proof body.%
wenzelm@44124	1951	\end{isamarkuptxt}%
wenzelm@44124	1952	\isamarkuptrue%
wenzelm@44124	1953	%
wenzelm@44124	1954	\endisatagproof
wenzelm@44124	1955	{\isafoldproof}%
wenzelm@44124	1956	%
wenzelm@44124	1957	\isadelimproof
wenzelm@44124	1958	%
wenzelm@44124	1959	\endisadelimproof
wenzelm@44124	1960	\isacommand{end}\isamarkupfalse%
wenzelm@44124	1961	%
wenzelm@44124	1962	\isamarkupsubsection{Example: predicate logic%
wenzelm@44124	1963	}
wenzelm@44124	1964	\isamarkuptrue%
wenzelm@44124	1965	%
wenzelm@44124	1966	\begin{isamarkuptext}%
wenzelm@44124	1967	Using the above principles, standard introduction and elimination proofs
wenzelm@44124	1968	of predicate logic connectives of HOL work as follows.%
wenzelm@44124	1969	\end{isamarkuptext}%
wenzelm@44124	1970	\isamarkuptrue%
wenzelm@44124	1971	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1972	\isanewline
wenzelm@44124	1973	\isakeyword{begin}\isanewline
wenzelm@44124	1974	%
wenzelm@44124	1975	\isadelimproof
wenzelm@44124	1976	\ \ %
wenzelm@44124	1977	\endisadelimproof
wenzelm@44124	1978	%
wenzelm@44124	1979	\isatagproof
wenzelm@44124	1980	\isacommand{have}\isamarkupfalse%
wenzelm@44124	1981	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1982	\isanewline
wenzelm@44124	1983	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1984	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1985	\ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1986	\isanewline
wenzelm@44124	1987	\isanewline
wenzelm@44124	1988	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1989	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1990	\isanewline
wenzelm@44124	1991	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1992	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1993	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1994	\isanewline
wenzelm@44124	1995	\isanewline
wenzelm@44124	1996	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1997	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1998	\isanewline
wenzelm@44124	1999	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2000	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2001	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2002	\isanewline
wenzelm@44124	2003	\isanewline
wenzelm@44124	2004	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2005	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2006	\isanewline
wenzelm@44124	2007	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2008	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2009	\ C\isanewline
wenzelm@44124	2010	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2011	\isanewline
wenzelm@44124	2012	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	2013	\ A\isanewline
wenzelm@44124	2014	\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2015	\ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2016	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2017	\isanewline
wenzelm@44124	2018	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44124	2019	\isanewline
wenzelm@44124	2020	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	2021	\ B\isanewline
wenzelm@44124	2022	\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2023	\ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2024	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2025	\isanewline
wenzelm@44124	2026	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2027	\isanewline
wenzelm@44124	2028	\isanewline
wenzelm@44124	2029	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2030	\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2031	\isanewline
wenzelm@44124	2032	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2033	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2034	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2035	\isanewline
wenzelm@44124	2036	\isanewline
wenzelm@44124	2037	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2038	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2039	\isanewline
wenzelm@44124	2040	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2041	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2042	\ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2043	\isanewline
wenzelm@44124	2044	\isanewline
wenzelm@44124	2045	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2046	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2047	\isanewline
wenzelm@44124	2048	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2049	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2050	\ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2051	\isanewline
wenzelm@44124	2052	\isanewline
wenzelm@44124	2053	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2054	\ False\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2055	\isanewline
wenzelm@44124	2056	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2057	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2058	\ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2059	\isanewline
wenzelm@44124	2060	\isanewline
wenzelm@44124	2061	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2062	\ True\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2063	\isanewline
wenzelm@44124	2064	\isanewline
wenzelm@44124	2065	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2066	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2067	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2068	\isanewline
wenzelm@44124	2069	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	2070	\ A\isanewline
wenzelm@44124	2071	\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2072	\ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2073	\ False\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2074	\isanewline
wenzelm@44124	2075	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2076	\isanewline
wenzelm@44124	2077	\isanewline
wenzelm@44124	2078	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2079	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2080	\isanewline
wenzelm@44124	2081	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2082	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2083	\ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2084	\isanewline
wenzelm@44124	2085	\isanewline
wenzelm@44124	2086	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2087	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2088	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2089	\isanewline
wenzelm@44124	2090	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	2091	\ x\isanewline
wenzelm@44124	2092	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2093	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2094	\isanewline
wenzelm@44124	2095	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2096	\isanewline
wenzelm@44124	2097	\isanewline
wenzelm@44124	2098	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2099	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2100	\isanewline
wenzelm@44124	2101	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2102	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2103	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2104	\isanewline
wenzelm@44124	2105	\isanewline
wenzelm@44124	2106	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2107	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2108	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2109	\isanewline
wenzelm@44124	2110	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2111	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2112	\isanewline
wenzelm@44124	2113	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2114	\isanewline
wenzelm@44124	2115	\isanewline
wenzelm@44124	2116	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2117	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2118	\isanewline
wenzelm@44124	2119	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2120	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2121	\ C\isanewline
wenzelm@44124	2122	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2123	\isanewline
wenzelm@44124	2124	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	2125	\ a\isanewline
wenzelm@44124	2126	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	2127	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2128	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2129	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2130	\isanewline
wenzelm@44124	2131	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2132	%
wenzelm@44124	2133	\begin{isamarkuptxt}%
wenzelm@44124	2134	Less awkward version using \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}:%
wenzelm@44124	2135	\end{isamarkuptxt}%
wenzelm@44124	2136	\isamarkuptrue%
wenzelm@44124	2137	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2138	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2139	\isanewline
wenzelm@44124	2140	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2141	\ \isacommand{obtain}\isamarkupfalse%
wenzelm@44124	2142	\ a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2143	%
wenzelm@44124	2144	\endisatagproof
wenzelm@44124	2145	{\isafoldproof}%
wenzelm@44124	2146	%
wenzelm@44124	2147	\isadelimproof
wenzelm@44124	2148	\isanewline
wenzelm@44124	2149	%
wenzelm@44124	2150	\endisadelimproof
wenzelm@44124	2151	\isacommand{end}\isamarkupfalse%
wenzelm@44124	2152	%
wenzelm@44124	2153	\begin{isamarkuptext}%
wenzelm@44124	2154	Further variations to illustrate Isar sub-proofs involving
wenzelm@44124	2155	\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}:%
wenzelm@44124	2156	\end{isamarkuptext}%
wenzelm@44124	2157	\isamarkuptrue%
wenzelm@44124	2158	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	2159	\isanewline
wenzelm@44124	2160	\isakeyword{begin}\isanewline
wenzelm@44124	2161	%
wenzelm@44124	2162	\isadelimproof
wenzelm@44124	2163	\ \ %
wenzelm@44124	2164	\endisadelimproof
wenzelm@44124	2165	%
wenzelm@44124	2166	\isatagproof
wenzelm@44124	2167	\isacommand{have}\isamarkupfalse%
wenzelm@44124	2168	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2169	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2170	\ \ %
wenzelm@44124	2171	\isamarkupcmt{two strictly isolated subproofs%
wenzelm@44124	2172	}
wenzelm@44124	2173	\isanewline
wenzelm@44124	2174	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2175	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2176	\isanewline
wenzelm@44124	2177	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44124	2178	\isanewline
wenzelm@44124	2179	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2180	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2181	\isanewline
wenzelm@44124	2182	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2183	\isanewline
wenzelm@44124	2184	\isanewline
wenzelm@44124	2185	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2186	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2187	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2188	\ \ %
wenzelm@44124	2189	\isamarkupcmt{one simultaneous sub-proof%
wenzelm@44124	2190	}
wenzelm@44124	2191	\isanewline
wenzelm@44124	2192	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2193	\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2194	\isanewline
wenzelm@44124	2195	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2196	\isanewline
wenzelm@44124	2197	\isanewline
wenzelm@44124	2198	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2199	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2200	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2201	\ \ %
wenzelm@44124	2202	\isamarkupcmt{two subproofs in the same context%
wenzelm@44124	2203	}
wenzelm@44124	2204	\isanewline
wenzelm@44124	2205	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2206	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2207	\isanewline
wenzelm@44124	2208	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2209	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2210	\isanewline
wenzelm@44124	2211	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2212	\isanewline
wenzelm@44124	2213	\isanewline
wenzelm@44124	2214	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2215	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2216	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2217	\ \ %
wenzelm@44124	2218	\isamarkupcmt{swapped order%
wenzelm@44124	2219	}
wenzelm@44124	2220	\isanewline
wenzelm@44124	2221	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2222	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2223	\isanewline
wenzelm@44124	2224	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2225	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2226	\isanewline
wenzelm@44124	2227	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2228	\isanewline
wenzelm@44124	2229	\isanewline
wenzelm@44124	2230	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2231	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2232	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2233	\ \ %
wenzelm@44124	2234	\isamarkupcmt{sequential subproofs%
wenzelm@44124	2235	}
wenzelm@44124	2236	\isanewline
wenzelm@44124	2237	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2238	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2239	\isanewline
wenzelm@44124	2240	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2241	\ B\ \isacommand{using}\isamarkupfalse%
wenzelm@44124	2242	\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2243	\isanewline
wenzelm@44124	2244	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2245	%
wenzelm@44124	2246	\endisatagproof
wenzelm@44124	2247	{\isafoldproof}%
wenzelm@44124	2248	%
wenzelm@44124	2249	\isadelimproof
wenzelm@44124	2250	\isanewline
wenzelm@44124	2251	%
wenzelm@44124	2252	\endisadelimproof
wenzelm@44124	2253	\isacommand{end}\isamarkupfalse%
wenzelm@44124	2254	%
wenzelm@44124	2255	\isamarkupsubsubsection{Example: set-theoretic operators%
wenzelm@44124	2256	}
wenzelm@44124	2257	\isamarkuptrue%
wenzelm@44124	2258	%
wenzelm@44124	2259	\begin{isamarkuptext}%
wenzelm@44124	2260	There is nothing special about logical connectives (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616E643E}{\isasymand}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{22}{\isachardoublequote}}} etc.). Operators from
wenzelm@45988	2261	set-theory or lattice-theory work analogously. It is only a matter
wenzelm@44124	2262	of rule declarations in the library; rules can be also specified
wenzelm@44124	2263	explicitly.%
wenzelm@44124	2264	\end{isamarkuptext}%
wenzelm@44124	2265	\isamarkuptrue%
wenzelm@44124	2266	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	2267	\isanewline
wenzelm@44124	2268	\isakeyword{begin}\isanewline
wenzelm@44124	2269	%
wenzelm@44124	2270	\isadelimproof
wenzelm@44124	2271	\ \ %
wenzelm@44124	2272	\endisadelimproof
wenzelm@44124	2273	%
wenzelm@44124	2274	\isatagproof
wenzelm@44124	2275	\isacommand{have}\isamarkupfalse%
wenzelm@44124	2276	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2277	\isanewline
wenzelm@44124	2278	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2279	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2280	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2281	\isanewline
wenzelm@44124	2282	\isanewline
wenzelm@44124	2283	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2284	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2285	\isanewline
wenzelm@44124	2286	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2287	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2288	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2289	\isanewline
wenzelm@44124	2290	\isanewline
wenzelm@44124	2291	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2292	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2293	\isanewline
wenzelm@44124	2294	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2295	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2296	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2297	\isanewline
wenzelm@44124	2298	\isanewline
wenzelm@44124	2299	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2300	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2301	\isanewline
wenzelm@44124	2302	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2303	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2304	\ C\isanewline
wenzelm@44124	2305	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2306	\isanewline
wenzelm@44124	2307	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	2308	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2309	\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2310	\ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2311	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2312	\isanewline
wenzelm@44124	2313	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44124	2314	\isanewline
wenzelm@44124	2315	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	2316	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2317	\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2318	\ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2319	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2320	\isanewline
wenzelm@44124	2321	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2322	\isanewline
wenzelm@44124	2323	\isanewline
wenzelm@44124	2324	\isacommand{next}\isamarkupfalse%
wenzelm@44124	2325	\isanewline
wenzelm@44124	2326	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2327	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2328	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2329	\isanewline
wenzelm@44124	2330	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	2331	\ a\isanewline
wenzelm@44124	2332	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	2333	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2334	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2335	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2336	\isanewline
wenzelm@44124	2337	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2338	\isanewline
wenzelm@44124	2339	\isanewline
wenzelm@44124	2340	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2341	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2342	\isanewline
wenzelm@44124	2343	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2344	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2345	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	2346	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	2347	\isanewline
wenzelm@44124	2348	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	2349	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2350	\isanewline
wenzelm@44124	2351	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	2352	\isanewline
wenzelm@44124	2353	\isanewline
wenzelm@44124	2354	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2355	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2356	\isanewline
wenzelm@44124	2357	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2358	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2359	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2360	\isanewline
wenzelm@44124	2361	\isanewline
wenzelm@44124	2362	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	2363	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	2364	\isanewline
wenzelm@44124	2365	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	2366	\ \isacommand{obtain}\isamarkupfalse%
wenzelm@44124	2367	\ a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	2368	%
wenzelm@44124	2369	\endisatagproof
wenzelm@44124	2370	{\isafoldproof}%
wenzelm@44124	2371	%
wenzelm@44124	2372	\isadelimproof
wenzelm@44124	2373	\isanewline
wenzelm@44124	2374	%
wenzelm@44124	2375	\endisadelimproof
wenzelm@44124	2376	\isacommand{end}\isamarkupfalse%
wenzelm@44126	2377	%
wenzelm@44126	2378	\isamarkupsection{Generalized elimination and cases%
wenzelm@44126	2379	}
wenzelm@44126	2380	\isamarkuptrue%
wenzelm@44126	2381	%
wenzelm@44126	2382	\isamarkupsubsection{General elimination rules%
wenzelm@44126	2383	}
wenzelm@44126	2384	\isamarkuptrue%
wenzelm@44126	2385	%
wenzelm@44126	2386	\begin{isamarkuptext}%
wenzelm@44126	2387	The general format of elimination rules is illustrated by the
wenzelm@44126	2388	following typical representatives:%
wenzelm@44126	2389	\end{isamarkuptext}%
wenzelm@44126	2390	\isamarkuptrue%
wenzelm@44126	2391	\isacommand{thm}\isamarkupfalse%
wenzelm@44126	2392	\ exE\ \ \ \ \ %
wenzelm@44126	2393	\isamarkupcmt{local parameter%
wenzelm@44126	2394	}
wenzelm@44126	2395	\isanewline
wenzelm@44126	2396	\isacommand{thm}\isamarkupfalse%
wenzelm@44126	2397	\ conjE\ \ \ %
wenzelm@44126	2398	\isamarkupcmt{local premises%
wenzelm@44126	2399	}
wenzelm@44126	2400	\isanewline
wenzelm@44126	2401	\isacommand{thm}\isamarkupfalse%
wenzelm@44126	2402	\ disjE\ \ \ %
wenzelm@44126	2403	\isamarkupcmt{split into cases%
wenzelm@44126	2404	}
wenzelm@44126	2405	%
wenzelm@44126	2406	\begin{isamarkuptext}%
wenzelm@44126	2407	Combining these characteristics leads to the following general scheme
wenzelm@44126	2408	for elimination rules with cases:
wenzelm@44126	2409
wenzelm@44126	2410	\begin{itemize}
wenzelm@44126	2411
wenzelm@44126	2412	\item prefix of assumptions (or ``major premises'')
wenzelm@44126	2413
wenzelm@44126	2414	\item one or more cases that enable to establish the main conclusion
wenzelm@44126	2415	in an augmented context
wenzelm@44126	2416
wenzelm@44126	2417	\end{itemize}%
wenzelm@44126	2418	\end{isamarkuptext}%
wenzelm@44126	2419	\isamarkuptrue%
wenzelm@44126	2420	\isacommand{notepad}\isamarkupfalse%
wenzelm@44126	2421	\isanewline
wenzelm@44126	2422	\isakeyword{begin}\isanewline
wenzelm@44126	2423	%
wenzelm@44126	2424	\isadelimproof
wenzelm@44126	2425	\ \ %
wenzelm@44126	2426	\endisadelimproof
wenzelm@44126	2427	%
wenzelm@44126	2428	\isatagproof
wenzelm@44126	2429	\isacommand{assume}\isamarkupfalse%
wenzelm@44126	2430	\ r{\isaliteral{3A}{\isacharcolon}}\isanewline
wenzelm@44126	2431	\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}A{\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isadigit{2}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ assumptions\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44126	2432	\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ B{\isadigit{1}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isadigit{1}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ case\ {\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44126	2433	\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ B{\isadigit{2}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isadigit{2}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ case\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44126	2434	\ \ \ \ \ \ R\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ main\ conclusion\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44126	2435	\isanewline
wenzelm@44126	2436	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44126	2437	\ A{\isadigit{1}}\ \isakeyword{and}\ A{\isadigit{2}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126	2438	\isanewline
wenzelm@44126	2439	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44126	2440	\ \isacommand{have}\isamarkupfalse%
wenzelm@44126	2441	\ R\isanewline
wenzelm@44126	2442	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44126	2443	\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44126	2444	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44126	2445	\ x\ y\isanewline
wenzelm@44126	2446	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44126	2447	\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44126	2448	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44126	2449	\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126	2450	\isanewline
wenzelm@44126	2451	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44126	2452	\isanewline
wenzelm@44126	2453	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44126	2454	\ x\ y\isanewline
wenzelm@44126	2455	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44126	2456	\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44126	2457	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44126	2458	\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126	2459	\isanewline
wenzelm@44126	2460	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44126	2461	%
wenzelm@44126	2462	\endisatagproof
wenzelm@44126	2463	{\isafoldproof}%
wenzelm@44126	2464	%
wenzelm@44126	2465	\isadelimproof
wenzelm@44126	2466	\isanewline
wenzelm@44126	2467	%
wenzelm@44126	2468	\endisadelimproof
wenzelm@44126	2469	\isacommand{end}\isamarkupfalse%
wenzelm@44126	2470	%
wenzelm@44126	2471	\begin{isamarkuptext}%
wenzelm@44126	2472	Here \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}thesis{\isaliteral{22}{\isachardoublequote}}} is used to refer to the unchanged goal
wenzelm@44126	2473	statement.%
wenzelm@44126	2474	\end{isamarkuptext}%
wenzelm@44126	2475	\isamarkuptrue%
wenzelm@44126	2476	%
wenzelm@44126	2477	\isamarkupsubsection{Rules with cases%
wenzelm@44126	2478	}
wenzelm@44126	2479	\isamarkuptrue%
wenzelm@44126	2480	%
wenzelm@44126	2481	\begin{isamarkuptext}%
wenzelm@44126	2482	Applying an elimination rule to some goal, leaves that unchanged
wenzelm@44126	2483	but allows to augment the context in the sub-proof of each case.
wenzelm@44126	2484
wenzelm@44126	2485	Isar provides some infrastructure to support this:
wenzelm@44126	2486
wenzelm@44126	2487	\begin{itemize}
wenzelm@44126	2488
wenzelm@44126	2489	\item native language elements to state eliminations
wenzelm@44126	2490
wenzelm@44126	2491	\item symbolic case names
wenzelm@44126	2492
wenzelm@44126	2493	\item method \hyperlink{method.cases}{\mbox{\isa{cases}}} to recover this structure in a
wenzelm@44126	2494	sub-proof
wenzelm@44126	2495
wenzelm@44126	2496	\end{itemize}%
wenzelm@44126	2497	\end{isamarkuptext}%
wenzelm@44126	2498	\isamarkuptrue%
wenzelm@44126	2499	\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44126	2500	\ exE\isanewline
wenzelm@44126	2501	\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44126	2502	\ conjE\isanewline
wenzelm@44126	2503	\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44126	2504	\ disjE\isanewline
wenzelm@44126	2505	\isanewline
wenzelm@44126	2506	\isacommand{lemma}\isamarkupfalse%
wenzelm@44126	2507	\isanewline
wenzelm@44126	2508	\ \ \isakeyword{assumes}\ A{\isadigit{1}}\ \isakeyword{and}\ A{\isadigit{2}}\ \ %
wenzelm@44126	2509	\isamarkupcmt{assumptions%
wenzelm@44126	2510	}
wenzelm@44126	2511	\isanewline
wenzelm@44126	2512	\ \ \isakeyword{obtains}\isanewline
wenzelm@44126	2513	\ \ \ \ {\isaliteral{28}{\isacharparenleft}}case{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ \ x\ y\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44126	2514	\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{28}{\isacharparenleft}}case{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ \ x\ y\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44126	2515	%
wenzelm@44126	2516	\isadelimproof
wenzelm@44126	2517	\ \ %
wenzelm@44126	2518	\endisadelimproof
wenzelm@44126	2519	%
wenzelm@44126	2520	\isatagproof
wenzelm@44126	2521	\isacommand{sorry}\isamarkupfalse%
wenzelm@44126	2522	%
wenzelm@44126	2523	\endisatagproof
wenzelm@44126	2524	{\isafoldproof}%
wenzelm@44126	2525	%
wenzelm@44126	2526	\isadelimproof
wenzelm@44126	2527	%
wenzelm@44126	2528	\endisadelimproof
wenzelm@44126	2529	%
wenzelm@44126	2530	\isamarkupsubsubsection{Example%
wenzelm@44126	2531	}
wenzelm@44126	2532	\isamarkuptrue%
wenzelm@44126	2533	\isacommand{lemma}\isamarkupfalse%
wenzelm@44126	2534	\ tertium{\isaliteral{5F}{\isacharunderscore}}non{\isaliteral{5F}{\isacharunderscore}}datur{\isaliteral{3A}{\isacharcolon}}\isanewline
wenzelm@44126	2535	\ \ \isakeyword{obtains}\isanewline
wenzelm@44126	2536	\ \ \ \ {\isaliteral{28}{\isacharparenleft}}T{\isaliteral{29}{\isacharparenright}}\ \ A\isanewline
wenzelm@44126	2537	\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{28}{\isacharparenleft}}F{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44126	2538	%
wenzelm@44126	2539	\isadelimproof
wenzelm@44126	2540	\ \ %
wenzelm@44126	2541	\endisadelimproof
wenzelm@44126	2542	%
wenzelm@44126	2543	\isatagproof
wenzelm@44126	2544	\isacommand{by}\isamarkupfalse%
wenzelm@44126	2545	\ blast%
wenzelm@44126	2546	\endisatagproof
wenzelm@44126	2547	{\isafoldproof}%
wenzelm@44126	2548	%
wenzelm@44126	2549	\isadelimproof
wenzelm@44126	2550	\isanewline
wenzelm@44126	2551	%
wenzelm@44126	2552	\endisadelimproof
wenzelm@44126	2553	\isanewline
wenzelm@44126	2554	\isacommand{notepad}\isamarkupfalse%
wenzelm@44126	2555	\isanewline
wenzelm@44126	2556	\isakeyword{begin}\isanewline
wenzelm@44126	2557	%
wenzelm@44126	2558	\isadelimproof
wenzelm@44126	2559	\ \ %
wenzelm@44126	2560	\endisadelimproof
wenzelm@44126	2561	%
wenzelm@44126	2562	\isatagproof
wenzelm@44126	2563	\isacommand{fix}\isamarkupfalse%
wenzelm@44126	2564	\ x\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
wenzelm@44126	2565	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44126	2566	\ C\isanewline
wenzelm@44126	2567	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44126	2568	\ {\isaliteral{28}{\isacharparenleft}}cases\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ rule{\isaliteral{3A}{\isacharcolon}}\ tertium{\isaliteral{5F}{\isacharunderscore}}non{\isaliteral{5F}{\isacharunderscore}}datur{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44126	2569	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44126	2570	\ T\isanewline
wenzelm@44126	2571	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44126	2572	\ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44126	2573	\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126	2574	\isanewline
wenzelm@44126	2575	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44126	2576	\isanewline
wenzelm@44126	2577	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44126	2578	\ F\isanewline
wenzelm@44126	2579	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44126	2580	\ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44126	2581	\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126	2582	\isanewline
wenzelm@44126	2583	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44126	2584	%
wenzelm@44126	2585	\endisatagproof
wenzelm@44126	2586	{\isafoldproof}%
wenzelm@44126	2587	%
wenzelm@44126	2588	\isadelimproof
wenzelm@44126	2589	\isanewline
wenzelm@44126	2590	%
wenzelm@44126	2591	\endisadelimproof
wenzelm@44126	2592	\isacommand{end}\isamarkupfalse%
wenzelm@44126	2593	%
wenzelm@44126	2594	\isamarkupsubsubsection{Example%
wenzelm@44126	2595	}
wenzelm@44126	2596	\isamarkuptrue%
wenzelm@44126	2597	%
wenzelm@44126	2598	\begin{isamarkuptext}%
wenzelm@44126	2599	Isabelle/HOL specification mechanisms (datatype, inductive, etc.)
wenzelm@44126	2600	provide suitable derived cases rules.%
wenzelm@44126	2601	\end{isamarkuptext}%
wenzelm@44126	2602	\isamarkuptrue%
wenzelm@44126	2603	\isacommand{datatype}\isamarkupfalse%
wenzelm@44126	2604	\ foo\ {\isaliteral{3D}{\isacharequal}}\ Foo\ {\isaliteral{7C}{\isacharbar}}\ Bar\ foo\isanewline
wenzelm@44126	2605	\isanewline
wenzelm@44126	2606	\isacommand{notepad}\isamarkupfalse%
wenzelm@44126	2607	\isanewline
wenzelm@44126	2608	\isakeyword{begin}\isanewline
wenzelm@44126	2609	%
wenzelm@44126	2610	\isadelimproof
wenzelm@44126	2611	\ \ %
wenzelm@44126	2612	\endisadelimproof
wenzelm@44126	2613	%
wenzelm@44126	2614	\isatagproof
wenzelm@44126	2615	\isacommand{fix}\isamarkupfalse%
wenzelm@44126	2616	\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ foo\isanewline
wenzelm@44126	2617	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44126	2618	\ C\isanewline
wenzelm@44126	2619	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44126	2620	\ {\isaliteral{28}{\isacharparenleft}}cases\ x{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44126	2621	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44126	2622	\ Foo\isanewline
wenzelm@44126	2623	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44126	2624	\ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Foo{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44126	2625	\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126	2626	\isanewline
wenzelm@44126	2627	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44126	2628	\isanewline
wenzelm@44126	2629	\ \ \ \ \isacommand{case}\isamarkupfalse%
wenzelm@44126	2630	\ {\isaliteral{28}{\isacharparenleft}}Bar\ a{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44126	2631	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44126	2632	\ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Bar\ a{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
wenzelm@44126	2633	\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126	2634	\isanewline
wenzelm@44126	2635	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44126	2636	%
wenzelm@44126	2637	\endisatagproof
wenzelm@44126	2638	{\isafoldproof}%
wenzelm@44126	2639	%
wenzelm@44126	2640	\isadelimproof
wenzelm@44126	2641	\isanewline
wenzelm@44126	2642	%
wenzelm@44126	2643	\endisadelimproof
wenzelm@44126	2644	\isacommand{end}\isamarkupfalse%
wenzelm@44126	2645	%
wenzelm@44126	2646	\isamarkupsubsection{Obtaining local contexts%
wenzelm@44126	2647	}
wenzelm@44126	2648	\isamarkuptrue%
wenzelm@44126	2649	%
wenzelm@44126	2650	\begin{isamarkuptext}%
wenzelm@44126	2651	A single ``case'' branch may be inlined into Isar proof text
wenzelm@44126	2652	via \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}. This proves \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{22}{\isachardoublequote}}} on the spot, and augments the context afterwards.%
wenzelm@44126	2653	\end{isamarkuptext}%
wenzelm@44126	2654	\isamarkuptrue%
wenzelm@44126	2655	\isacommand{notepad}\isamarkupfalse%
wenzelm@44126	2656	\isanewline
wenzelm@44126	2657	\isakeyword{begin}\isanewline
wenzelm@44126	2658	%
wenzelm@44126	2659	\isadelimproof
wenzelm@44126	2660	\ \ %
wenzelm@44126	2661	\endisadelimproof
wenzelm@44126	2662	%
wenzelm@44126	2663	\isatagproof
wenzelm@44126	2664	\isacommand{fix}\isamarkupfalse%
wenzelm@44126	2665	\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44126	2666	\isanewline
wenzelm@44126	2667	\ \ \isacommand{obtain}\isamarkupfalse%
wenzelm@44126	2668	\ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126	2669	\isanewline
wenzelm@44126	2670	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44126	2671	\ {\isaliteral{60}{\isacharbackquoteopen}}B\ x{\isaliteral{60}{\isacharbackquoteclose}}%
wenzelm@44126	2672	\begin{isamarkuptxt}%
wenzelm@44126	2673	Conclusions from this context may not mention \isa{x} again!%
wenzelm@44126	2674	\end{isamarkuptxt}%
wenzelm@44126	2675	\isamarkuptrue%
wenzelm@44126	2676	\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44126	2677	\isanewline
wenzelm@44126	2678	\ \ \ \ \isacommand{obtain}\isamarkupfalse%
wenzelm@44126	2679	\ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126	2680	\isanewline
wenzelm@44126	2681	\ \ \ \ \isacommand{from}\isamarkupfalse%
wenzelm@44126	2682	\ {\isaliteral{60}{\isacharbackquoteopen}}B\ x{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{have}\isamarkupfalse%
wenzelm@44126	2683	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44126	2684	\isanewline
wenzelm@44126	2685	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44126	2686	\isanewline
wenzelm@44126	2687	\ \ \isacommand{note}\isamarkupfalse%
wenzelm@44126	2688	\ {\isaliteral{60}{\isacharbackquoteopen}}C{\isaliteral{60}{\isacharbackquoteclose}}%
wenzelm@44126	2689	\endisatagproof
wenzelm@44126	2690	{\isafoldproof}%
wenzelm@44126	2691	%
wenzelm@44126	2692	\isadelimproof
wenzelm@44126	2693	\isanewline
wenzelm@44126	2694	%
wenzelm@44126	2695	\endisadelimproof
wenzelm@44126	2696	\isacommand{end}\isamarkupfalse%
wenzelm@44121	2697	\isanewline
wenzelm@44121	2698	%
wenzelm@44121	2699	\isadelimtheory
wenzelm@44121	2700	\isanewline
wenzelm@44121	2701	%
wenzelm@44121	2702	\endisadelimtheory
wenzelm@44121	2703	%
wenzelm@44121	2704	\isatagtheory
wenzelm@44121	2705	\isacommand{end}\isamarkupfalse%
wenzelm@44121	2706	%
wenzelm@44121	2707	\endisatagtheory
wenzelm@44121	2708	{\isafoldtheory}%
wenzelm@44121	2709	%
wenzelm@44121	2710	\isadelimtheory
wenzelm@45988	2711	\isanewline
wenzelm@44121	2712	%
wenzelm@44121	2713	\endisadelimtheory
wenzelm@44121	2714	\end{isabellebody}%
wenzelm@44121	2715	%%% Local Variables:
wenzelm@44121	2716	%%% mode: latex
wenzelm@44121	2717	%%% TeX-master: "root"
wenzelm@44121	2718	%%% End:

author	wenzelm
	Mon, 03 Oct 2011 11:14:19 +0200
changeset 45988	a45121ffcfcb
parent 44127	3ba51a3acff0
child 46691	1fe2dd6d5086
permissions	-rw-r--r--