wneuper/isa: doc-src/IsarRef/Thy/document/Synopsis.tex@8c0a49d72857 (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@44121	263	Adhoc-simplication (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@44123	484	\isamarkupsection{Calculational reasoning%
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@44124	846	\isamarkupsection{Structured Natural Deduction%
wenzelm@44124	847	}
wenzelm@44124	848	\isamarkuptrue%
wenzelm@44124	849	%
wenzelm@44124	850	\isamarkupsubsection{Rule statements%
wenzelm@44124	851	}
wenzelm@44124	852	\isamarkuptrue%
wenzelm@44124	853	%
wenzelm@44124	854	\begin{isamarkuptext}%
wenzelm@44124	855	Isabelle/Pure ``theorems'' are always natural deduction rules,
wenzelm@44124	856	which sometimes happen to consist of a conclusion only.
wenzelm@44124	857
wenzelm@44124	858	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	859	rule structure declaratively. For example:%
wenzelm@44124	860	\end{isamarkuptext}%
wenzelm@44124	861	\isamarkuptrue%
wenzelm@44124	862	\isacommand{thm}\isamarkupfalse%
wenzelm@44124	863	\ conjI\isanewline
wenzelm@44124	864	\isacommand{thm}\isamarkupfalse%
wenzelm@44124	865	\ impI\isanewline
wenzelm@44124	866	\isacommand{thm}\isamarkupfalse%
wenzelm@44124	867	\ nat{\isaliteral{2E}{\isachardot}}induct%
wenzelm@44124	868	\begin{isamarkuptext}%
wenzelm@44124	869	The object-logic is embedded into the Pure framework via an implicit
wenzelm@44124	870	derivability judgment \isa{{\isaliteral{22}{\isachardoublequote}}Trueprop\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop{\isaliteral{22}{\isachardoublequote}}}.
wenzelm@44124	871
wenzelm@44124	872	Thus any HOL formulae appears atomic to the Pure framework, while
wenzelm@44124	873	the rule structure outlines the corresponding proof pattern.
wenzelm@44124	874
wenzelm@44124	875	This can be made explicit as follows:%
wenzelm@44124	876	\end{isamarkuptext}%
wenzelm@44124	877	\isamarkuptrue%
wenzelm@44124	878	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	879	\isanewline
wenzelm@44124	880	\isakeyword{begin}\isanewline
wenzelm@44124	881	%
wenzelm@44124	882	\isadelimproof
wenzelm@44124	883	\ \ %
wenzelm@44124	884	\endisadelimproof
wenzelm@44124	885	%
wenzelm@44124	886	\isatagproof
wenzelm@44124	887	\isacommand{write}\isamarkupfalse%
wenzelm@44124	888	\ Trueprop\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}Tr{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
wenzelm@44124	889	\endisatagproof
wenzelm@44124	890	{\isafoldproof}%
wenzelm@44124	891	%
wenzelm@44124	892	\isadelimproof
wenzelm@44124	893	\isanewline
wenzelm@44124	894	%
wenzelm@44124	895	\endisadelimproof
wenzelm@44124	896	\isanewline
wenzelm@44124	897	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	898	\ conjI\isanewline
wenzelm@44124	899	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	900	\ impI\isanewline
wenzelm@44124	901	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	902	\ nat{\isaliteral{2E}{\isachardot}}induct\isanewline
wenzelm@44124	903	\isacommand{end}\isamarkupfalse%
wenzelm@44124	904	%
wenzelm@44124	905	\begin{isamarkuptext}%
wenzelm@44124	906	Isar provides first-class notation for rule statements as follows.%
wenzelm@44124	907	\end{isamarkuptext}%
wenzelm@44124	908	\isamarkuptrue%
wenzelm@44124	909	\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44124	910	\ conjI\isanewline
wenzelm@44124	911	\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44124	912	\ impI\isanewline
wenzelm@44124	913	\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
wenzelm@44124	914	\ nat{\isaliteral{2E}{\isachardot}}induct%
wenzelm@44124	915	\isamarkupsubsubsection{Examples%
wenzelm@44124	916	}
wenzelm@44124	917	\isamarkuptrue%
wenzelm@44124	918	%
wenzelm@44124	919	\begin{isamarkuptext}%
wenzelm@44124	920	Introductions and eliminations of some standard connectives of
wenzelm@44124	921	the object-logic can be written as rule statements as follows. (The
wenzelm@44124	922	proof ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.blast}{\mbox{\isa{blast}}}'' serves as sanity check.)%
wenzelm@44124	923	\end{isamarkuptext}%
wenzelm@44124	924	\isamarkuptrue%
wenzelm@44124	925	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	926	\ {\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	927	\isadelimproof
wenzelm@44124	928	\ %
wenzelm@44124	929	\endisadelimproof
wenzelm@44124	930	%
wenzelm@44124	931	\isatagproof
wenzelm@44124	932	\isacommand{by}\isamarkupfalse%
wenzelm@44124	933	\ blast%
wenzelm@44124	934	\endisatagproof
wenzelm@44124	935	{\isafoldproof}%
wenzelm@44124	936	%
wenzelm@44124	937	\isadelimproof
wenzelm@44124	938	%
wenzelm@44124	939	\endisadelimproof
wenzelm@44124	940	\isanewline
wenzelm@44124	941	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	942	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	943	\isadelimproof
wenzelm@44124	944	\ %
wenzelm@44124	945	\endisadelimproof
wenzelm@44124	946	%
wenzelm@44124	947	\isatagproof
wenzelm@44124	948	\isacommand{by}\isamarkupfalse%
wenzelm@44124	949	\ blast%
wenzelm@44124	950	\endisatagproof
wenzelm@44124	951	{\isafoldproof}%
wenzelm@44124	952	%
wenzelm@44124	953	\isadelimproof
wenzelm@44124	954	%
wenzelm@44124	955	\endisadelimproof
wenzelm@44124	956	\isanewline
wenzelm@44124	957	\isanewline
wenzelm@44124	958	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	959	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	960	\isadelimproof
wenzelm@44124	961	\ %
wenzelm@44124	962	\endisadelimproof
wenzelm@44124	963	%
wenzelm@44124	964	\isatagproof
wenzelm@44124	965	\isacommand{by}\isamarkupfalse%
wenzelm@44124	966	\ blast%
wenzelm@44124	967	\endisatagproof
wenzelm@44124	968	{\isafoldproof}%
wenzelm@44124	969	%
wenzelm@44124	970	\isadelimproof
wenzelm@44124	971	%
wenzelm@44124	972	\endisadelimproof
wenzelm@44124	973	\isanewline
wenzelm@44124	974	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	975	\ {\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	976	\isadelimproof
wenzelm@44124	977	\ %
wenzelm@44124	978	\endisadelimproof
wenzelm@44124	979	%
wenzelm@44124	980	\isatagproof
wenzelm@44124	981	\isacommand{by}\isamarkupfalse%
wenzelm@44124	982	\ blast%
wenzelm@44124	983	\endisatagproof
wenzelm@44124	984	{\isafoldproof}%
wenzelm@44124	985	%
wenzelm@44124	986	\isadelimproof
wenzelm@44124	987	%
wenzelm@44124	988	\endisadelimproof
wenzelm@44124	989	\isanewline
wenzelm@44124	990	\isanewline
wenzelm@44124	991	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	992	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	993	\isadelimproof
wenzelm@44124	994	\ %
wenzelm@44124	995	\endisadelimproof
wenzelm@44124	996	%
wenzelm@44124	997	\isatagproof
wenzelm@44124	998	\isacommand{by}\isamarkupfalse%
wenzelm@44124	999	\ blast%
wenzelm@44124	1000	\endisatagproof
wenzelm@44124	1001	{\isafoldproof}%
wenzelm@44124	1002	%
wenzelm@44124	1003	\isadelimproof
wenzelm@44124	1004	%
wenzelm@44124	1005	\endisadelimproof
wenzelm@44124	1006	\isanewline
wenzelm@44124	1007	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1008	\ {\isaliteral{22}{\isachardoublequoteopen}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}%
wenzelm@44124	1009	\isadelimproof
wenzelm@44124	1010	\ %
wenzelm@44124	1011	\endisadelimproof
wenzelm@44124	1012	%
wenzelm@44124	1013	\isatagproof
wenzelm@44124	1014	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1015	\ blast%
wenzelm@44124	1016	\endisatagproof
wenzelm@44124	1017	{\isafoldproof}%
wenzelm@44124	1018	%
wenzelm@44124	1019	\isadelimproof
wenzelm@44124	1020	%
wenzelm@44124	1021	\endisadelimproof
wenzelm@44124	1022	\isanewline
wenzelm@44124	1023	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1024	\ {\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	1025	\isadelimproof
wenzelm@44124	1026	\ %
wenzelm@44124	1027	\endisadelimproof
wenzelm@44124	1028	%
wenzelm@44124	1029	\isatagproof
wenzelm@44124	1030	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1031	\ blast%
wenzelm@44124	1032	\endisatagproof
wenzelm@44124	1033	{\isafoldproof}%
wenzelm@44124	1034	%
wenzelm@44124	1035	\isadelimproof
wenzelm@44124	1036	%
wenzelm@44124	1037	\endisadelimproof
wenzelm@44124	1038	\isanewline
wenzelm@44124	1039	\isanewline
wenzelm@44124	1040	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1041	\ {\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	1042	\isadelimproof
wenzelm@44124	1043	\ %
wenzelm@44124	1044	\endisadelimproof
wenzelm@44124	1045	%
wenzelm@44124	1046	\isatagproof
wenzelm@44124	1047	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1048	\ blast%
wenzelm@44124	1049	\endisatagproof
wenzelm@44124	1050	{\isafoldproof}%
wenzelm@44124	1051	%
wenzelm@44124	1052	\isadelimproof
wenzelm@44124	1053	%
wenzelm@44124	1054	\endisadelimproof
wenzelm@44124	1055	\isanewline
wenzelm@44124	1056	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1057	\ {\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	1058	\isadelimproof
wenzelm@44124	1059	\ %
wenzelm@44124	1060	\endisadelimproof
wenzelm@44124	1061	%
wenzelm@44124	1062	\isatagproof
wenzelm@44124	1063	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1064	\ blast%
wenzelm@44124	1065	\endisatagproof
wenzelm@44124	1066	{\isafoldproof}%
wenzelm@44124	1067	%
wenzelm@44124	1068	\isadelimproof
wenzelm@44124	1069	%
wenzelm@44124	1070	\endisadelimproof
wenzelm@44124	1071	\isanewline
wenzelm@44124	1072	\isanewline
wenzelm@44124	1073	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1074	\ {\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	1075	\isadelimproof
wenzelm@44124	1076	\ %
wenzelm@44124	1077	\endisadelimproof
wenzelm@44124	1078	%
wenzelm@44124	1079	\isatagproof
wenzelm@44124	1080	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1081	\ blast%
wenzelm@44124	1082	\endisatagproof
wenzelm@44124	1083	{\isafoldproof}%
wenzelm@44124	1084	%
wenzelm@44124	1085	\isadelimproof
wenzelm@44124	1086	%
wenzelm@44124	1087	\endisadelimproof
wenzelm@44124	1088	\isanewline
wenzelm@44124	1089	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1090	\ {\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	1091	\isadelimproof
wenzelm@44124	1092	\ %
wenzelm@44124	1093	\endisadelimproof
wenzelm@44124	1094	%
wenzelm@44124	1095	\isatagproof
wenzelm@44124	1096	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1097	\ blast%
wenzelm@44124	1098	\endisatagproof
wenzelm@44124	1099	{\isafoldproof}%
wenzelm@44124	1100	%
wenzelm@44124	1101	\isadelimproof
wenzelm@44124	1102	%
wenzelm@44124	1103	\endisadelimproof
wenzelm@44124	1104	\isanewline
wenzelm@44124	1105	\isanewline
wenzelm@44124	1106	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1107	\ {\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	1108	\isadelimproof
wenzelm@44124	1109	\ %
wenzelm@44124	1110	\endisadelimproof
wenzelm@44124	1111	%
wenzelm@44124	1112	\isatagproof
wenzelm@44124	1113	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1114	\ blast%
wenzelm@44124	1115	\endisatagproof
wenzelm@44124	1116	{\isafoldproof}%
wenzelm@44124	1117	%
wenzelm@44124	1118	\isadelimproof
wenzelm@44124	1119	%
wenzelm@44124	1120	\endisadelimproof
wenzelm@44124	1121	\isanewline
wenzelm@44124	1122	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1123	\ {\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	1124	\isadelimproof
wenzelm@44124	1125	\ %
wenzelm@44124	1126	\endisadelimproof
wenzelm@44124	1127	%
wenzelm@44124	1128	\isatagproof
wenzelm@44124	1129	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1130	\ blast%
wenzelm@44124	1131	\endisatagproof
wenzelm@44124	1132	{\isafoldproof}%
wenzelm@44124	1133	%
wenzelm@44124	1134	\isadelimproof
wenzelm@44124	1135	%
wenzelm@44124	1136	\endisadelimproof
wenzelm@44124	1137	\isanewline
wenzelm@44124	1138	\isanewline
wenzelm@44124	1139	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1140	\ {\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	1141	\isadelimproof
wenzelm@44124	1142	\ %
wenzelm@44124	1143	\endisadelimproof
wenzelm@44124	1144	%
wenzelm@44124	1145	\isatagproof
wenzelm@44124	1146	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1147	\ blast%
wenzelm@44124	1148	\endisatagproof
wenzelm@44124	1149	{\isafoldproof}%
wenzelm@44124	1150	%
wenzelm@44124	1151	\isadelimproof
wenzelm@44124	1152	%
wenzelm@44124	1153	\endisadelimproof
wenzelm@44124	1154	\isanewline
wenzelm@44124	1155	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1156	\ {\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	1157	\isadelimproof
wenzelm@44124	1158	\ %
wenzelm@44124	1159	\endisadelimproof
wenzelm@44124	1160	%
wenzelm@44124	1161	\isatagproof
wenzelm@44124	1162	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1163	\ blast%
wenzelm@44124	1164	\endisatagproof
wenzelm@44124	1165	{\isafoldproof}%
wenzelm@44124	1166	%
wenzelm@44124	1167	\isadelimproof
wenzelm@44124	1168	%
wenzelm@44124	1169	\endisadelimproof
wenzelm@44124	1170	\isanewline
wenzelm@44124	1171	\isacommand{lemma}\isamarkupfalse%
wenzelm@44124	1172	\ {\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	1173	\isadelimproof
wenzelm@44124	1174	\ %
wenzelm@44124	1175	\endisadelimproof
wenzelm@44124	1176	%
wenzelm@44124	1177	\isatagproof
wenzelm@44124	1178	\isacommand{by}\isamarkupfalse%
wenzelm@44124	1179	\ blast%
wenzelm@44124	1180	\endisatagproof
wenzelm@44124	1181	{\isafoldproof}%
wenzelm@44124	1182	%
wenzelm@44124	1183	\isadelimproof
wenzelm@44124	1184	%
wenzelm@44124	1185	\endisadelimproof
wenzelm@44124	1186	%
wenzelm@44124	1187	\isamarkupsubsection{Isar context elements%
wenzelm@44124	1188	}
wenzelm@44124	1189	\isamarkuptrue%
wenzelm@44124	1190	%
wenzelm@44124	1191	\begin{isamarkuptext}%
wenzelm@44124	1192	We derive some results out of the blue, using Isar context
wenzelm@44124	1193	elements and some explicit blocks. This illustrates their meaning
wenzelm@44124	1194	wrt.\ Pure connectives, without goal states getting in the way.%
wenzelm@44124	1195	\end{isamarkuptext}%
wenzelm@44124	1196	\isamarkuptrue%
wenzelm@44124	1197	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1198	\isanewline
wenzelm@44124	1199	\isakeyword{begin}\isanewline
wenzelm@44124	1200	%
wenzelm@44124	1201	\isadelimproof
wenzelm@44124	1202	\ \ %
wenzelm@44124	1203	\endisadelimproof
wenzelm@44124	1204	%
wenzelm@44124	1205	\isatagproof
wenzelm@44124	1206	\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124	1207	\isanewline
wenzelm@44124	1208	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	1209	\ x\isanewline
wenzelm@44124	1210	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1211	\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1212	\isanewline
wenzelm@44124	1213	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124	1214	\isanewline
wenzelm@44124	1215	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1216	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44124	1217	\ fact\isanewline
wenzelm@44124	1218	\isanewline
wenzelm@44124	1219	\isacommand{next}\isamarkupfalse%
wenzelm@44124	1220	\isanewline
wenzelm@44124	1221	\isanewline
wenzelm@44124	1222	\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124	1223	\isanewline
wenzelm@44124	1224	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1225	\ A\isanewline
wenzelm@44124	1226	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1227	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1228	\isanewline
wenzelm@44124	1229	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124	1230	\isanewline
wenzelm@44124	1231	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1232	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44124	1233	\ fact\isanewline
wenzelm@44124	1234	\isanewline
wenzelm@44124	1235	\isacommand{next}\isamarkupfalse%
wenzelm@44124	1236	\isanewline
wenzelm@44124	1237	\isanewline
wenzelm@44124	1238	\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124	1239	\isanewline
wenzelm@44124	1240	\ \ \ \ \isacommand{def}\isamarkupfalse%
wenzelm@44124	1241	\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\isanewline
wenzelm@44124	1242	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1243	\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1244	\isanewline
wenzelm@44124	1245	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124	1246	\isanewline
wenzelm@44124	1247	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1248	\ {\isaliteral{22}{\isachardoublequoteopen}}B\ t{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
wenzelm@44124	1249	\ fact\isanewline
wenzelm@44124	1250	\isanewline
wenzelm@44124	1251	\isacommand{next}\isamarkupfalse%
wenzelm@44124	1252	\isanewline
wenzelm@44124	1253	\isanewline
wenzelm@44124	1254	\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124	1255	\isanewline
wenzelm@44124	1256	\ \ \ \ \isacommand{obtain}\isamarkupfalse%
wenzelm@44124	1257	\ 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	1258	\isanewline
wenzelm@44124	1259	\ \ \ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1260	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1261	\isanewline
wenzelm@44124	1262	\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124	1263	\isanewline
wenzelm@44124	1264	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1265	\ C\ \isacommand{by}\isamarkupfalse%
wenzelm@44124	1266	\ fact%
wenzelm@44124	1267	\endisatagproof
wenzelm@44124	1268	{\isafoldproof}%
wenzelm@44124	1269	%
wenzelm@44124	1270	\isadelimproof
wenzelm@44124	1271	\isanewline
wenzelm@44124	1272	%
wenzelm@44124	1273	\endisadelimproof
wenzelm@44124	1274	\isanewline
wenzelm@44124	1275	\isacommand{end}\isamarkupfalse%
wenzelm@44124	1276	%
wenzelm@44124	1277	\isamarkupsubsection{Pure rule composition%
wenzelm@44124	1278	}
wenzelm@44124	1279	\isamarkuptrue%
wenzelm@44124	1280	%
wenzelm@44124	1281	\begin{isamarkuptext}%
wenzelm@44124	1282	The Pure framework provides means for:
wenzelm@44124	1283
wenzelm@44124	1284	\begin{itemize}
wenzelm@44124	1285
wenzelm@44124	1286	\item backward-chaining of rules by \hyperlink{inference.resolution}{\mbox{\isa{resolution}}}
wenzelm@44124	1287
wenzelm@44124	1288	\item closing of branches by \hyperlink{inference.assumption}{\mbox{\isa{assumption}}}
wenzelm@44124	1289
wenzelm@44124	1290	\end{itemize}
wenzelm@44124	1291
wenzelm@44124	1292	Both principles involve higher-order unification of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms
wenzelm@44124	1293	modulo \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-equivalence (cf.\ Huet and Miller).%
wenzelm@44124	1294	\end{isamarkuptext}%
wenzelm@44124	1295	\isamarkuptrue%
wenzelm@44124	1296	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1297	\isanewline
wenzelm@44124	1298	\isakeyword{begin}\isanewline
wenzelm@44124	1299	%
wenzelm@44124	1300	\isadelimproof
wenzelm@44124	1301	\ \ %
wenzelm@44124	1302	\endisadelimproof
wenzelm@44124	1303	%
wenzelm@44124	1304	\isatagproof
wenzelm@44124	1305	\isacommand{assume}\isamarkupfalse%
wenzelm@44124	1306	\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ B%
wenzelm@44124	1307	\endisatagproof
wenzelm@44124	1308	{\isafoldproof}%
wenzelm@44124	1309	%
wenzelm@44124	1310	\isadelimproof
wenzelm@44124	1311	\isanewline
wenzelm@44124	1312	%
wenzelm@44124	1313	\endisadelimproof
wenzelm@44124	1314	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1315	\ conjI\isanewline
wenzelm@44124	1316	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1317	\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{5D}{\isacharbrackright}}\ \ %
wenzelm@44124	1318	\isamarkupcmt{instantiation%
wenzelm@44124	1319	}
wenzelm@44124	1320	\isanewline
wenzelm@44124	1321	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1322	\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{2C}{\isacharcomma}}\ OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ %
wenzelm@44124	1323	\isamarkupcmt{instantiation and composition%
wenzelm@44124	1324	}
wenzelm@44124	1325	\isanewline
wenzelm@44124	1326	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1327	\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ %
wenzelm@44124	1328	\isamarkupcmt{composition via unification (trivial)%
wenzelm@44124	1329	}
wenzelm@44124	1330	\isanewline
wenzelm@44124	1331	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1332	\ 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	1333	\isanewline
wenzelm@44124	1334	\ \ \isacommand{thm}\isamarkupfalse%
wenzelm@44124	1335	\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ disjI{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
wenzelm@44124	1336	\isacommand{end}\isamarkupfalse%
wenzelm@44124	1337	%
wenzelm@44124	1338	\begin{isamarkuptext}%
wenzelm@44124	1339	Note: Low-level rule composition is tedious and leads to
wenzelm@44124	1340	unreadable~/ unmaintainable expressions in the text.%
wenzelm@44124	1341	\end{isamarkuptext}%
wenzelm@44124	1342	\isamarkuptrue%
wenzelm@44124	1343	%
wenzelm@44124	1344	\isamarkupsubsection{Structured backward reasoning%
wenzelm@44124	1345	}
wenzelm@44124	1346	\isamarkuptrue%
wenzelm@44124	1347	%
wenzelm@44124	1348	\begin{isamarkuptext}%
wenzelm@44124	1349	Idea: Canonical proof decomposition via \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~/
wenzelm@44124	1350	\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~/ \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, where the body produces a
wenzelm@44124	1351	natural deduction rule to refine some goal.%
wenzelm@44124	1352	\end{isamarkuptext}%
wenzelm@44124	1353	\isamarkuptrue%
wenzelm@44124	1354	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1355	\isanewline
wenzelm@44124	1356	\isakeyword{begin}\isanewline
wenzelm@44124	1357	%
wenzelm@44124	1358	\isadelimproof
wenzelm@44124	1359	\ \ %
wenzelm@44124	1360	\endisadelimproof
wenzelm@44124	1361	%
wenzelm@44124	1362	\isatagproof
wenzelm@44124	1363	\isacommand{fix}\isamarkupfalse%
wenzelm@44124	1364	\ 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	1365	\isanewline
wenzelm@44124	1366	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1367	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1368	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1369	\ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44124	1370	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	1371	\ x\isanewline
wenzelm@44124	1372	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1373	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1374	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1375	\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1376	\isanewline
wenzelm@44124	1377	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1378	\isanewline
wenzelm@44124	1379	\isanewline
wenzelm@44124	1380	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1381	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1382	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1383	\ {\isaliteral{2D}{\isacharminus}}\isanewline
wenzelm@44124	1384	\ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
wenzelm@44124	1385	\isanewline
wenzelm@44124	1386	\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	1387	\ x\isanewline
wenzelm@44124	1388	\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1389	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1390	\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1391	\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1392	\isanewline
wenzelm@44124	1393	\ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
wenzelm@44124	1394	\ %
wenzelm@44124	1395	\isamarkupcmt{implicit block structure made explicit%
wenzelm@44124	1396	}
wenzelm@44124	1397	\isanewline
wenzelm@44124	1398	\ \ \ \ \isacommand{note}\isamarkupfalse%
wenzelm@44124	1399	\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
wenzelm@44124	1400	\ \ \ \ \ \ %
wenzelm@44124	1401	\isamarkupcmt{side exit for the resulting rule%
wenzelm@44124	1402	}
wenzelm@44124	1403	\isanewline
wenzelm@44124	1404	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1405	%
wenzelm@44124	1406	\endisatagproof
wenzelm@44124	1407	{\isafoldproof}%
wenzelm@44124	1408	%
wenzelm@44124	1409	\isadelimproof
wenzelm@44124	1410	\isanewline
wenzelm@44124	1411	%
wenzelm@44124	1412	\endisadelimproof
wenzelm@44124	1413	\isacommand{end}\isamarkupfalse%
wenzelm@44124	1414	%
wenzelm@44124	1415	\isamarkupsubsection{Structured rule application%
wenzelm@44124	1416	}
wenzelm@44124	1417	\isamarkuptrue%
wenzelm@44124	1418	%
wenzelm@44124	1419	\begin{isamarkuptext}%
wenzelm@44124	1420	Idea: Previous facts and new claims are composed with a rule from
wenzelm@44124	1421	the context (or background library).%
wenzelm@44124	1422	\end{isamarkuptext}%
wenzelm@44124	1423	\isamarkuptrue%
wenzelm@44124	1424	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1425	\isanewline
wenzelm@44124	1426	\isakeyword{begin}\isanewline
wenzelm@44124	1427	%
wenzelm@44124	1428	\isadelimproof
wenzelm@44124	1429	\ \ %
wenzelm@44124	1430	\endisadelimproof
wenzelm@44124	1431	%
wenzelm@44124	1432	\isatagproof
wenzelm@44124	1433	\isacommand{assume}\isamarkupfalse%
wenzelm@44124	1434	\ r{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
wenzelm@44124	1435	\isamarkupcmt{simple rule (Horn clause)%
wenzelm@44124	1436	}
wenzelm@44124	1437	\isanewline
wenzelm@44124	1438	\isanewline
wenzelm@44124	1439	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1440	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1441	\ \ %
wenzelm@44124	1442	\isamarkupcmt{prefix of facts via outer sub-proof%
wenzelm@44124	1443	}
wenzelm@44124	1444	\isanewline
wenzelm@44124	1445	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1446	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1447	\ C\isanewline
wenzelm@44124	1448	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1449	\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124	1450	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1451	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1452	\ \ %
wenzelm@44124	1453	\isamarkupcmt{remaining rule premises via inner sub-proof%
wenzelm@44124	1454	}
wenzelm@44124	1455	\isanewline
wenzelm@44124	1456	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1457	\isanewline
wenzelm@44124	1458	\isanewline
wenzelm@44124	1459	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1460	\ C\isanewline
wenzelm@44124	1461	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1462	\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124	1463	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1464	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1465	\isanewline
wenzelm@44124	1466	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1467	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1468	\isanewline
wenzelm@44124	1469	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1470	\isanewline
wenzelm@44124	1471	\isanewline
wenzelm@44124	1472	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1473	\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1474	\isanewline
wenzelm@44124	1475	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1476	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1477	\ C\isanewline
wenzelm@44124	1478	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1479	\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124	1480	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1481	\isanewline
wenzelm@44124	1482	\isanewline
wenzelm@44124	1483	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1484	\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1485	\isanewline
wenzelm@44124	1486	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1487	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1488	\ C\ \isacommand{by}\isamarkupfalse%
wenzelm@44124	1489	\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124	1490	\isanewline
wenzelm@44124	1491	\isacommand{next}\isamarkupfalse%
wenzelm@44124	1492	\isanewline
wenzelm@44124	1493	\isanewline
wenzelm@44124	1494	\ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1495	\ 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	1496	\isamarkupcmt{nested rule%
wenzelm@44124	1497	}
wenzelm@44124	1498	\isanewline
wenzelm@44124	1499	\isanewline
wenzelm@44124	1500	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1501	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1502	\isanewline
wenzelm@44124	1503	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1504	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1505	\ C\isanewline
wenzelm@44124	1506	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1507	\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\isanewline
wenzelm@44124	1508	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	1509	\ x\isanewline
wenzelm@44124	1510	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1511	\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1512	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1513	\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1514	\isanewline
wenzelm@44124	1515	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1516	%
wenzelm@44124	1517	\begin{isamarkuptxt}%
wenzelm@44124	1518	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	1519	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	1520	in the nested proof body.%
wenzelm@44124	1521	\end{isamarkuptxt}%
wenzelm@44124	1522	\isamarkuptrue%
wenzelm@44124	1523	%
wenzelm@44124	1524	\endisatagproof
wenzelm@44124	1525	{\isafoldproof}%
wenzelm@44124	1526	%
wenzelm@44124	1527	\isadelimproof
wenzelm@44124	1528	%
wenzelm@44124	1529	\endisadelimproof
wenzelm@44124	1530	\isacommand{end}\isamarkupfalse%
wenzelm@44124	1531	%
wenzelm@44124	1532	\isamarkupsubsection{Example: predicate logic%
wenzelm@44124	1533	}
wenzelm@44124	1534	\isamarkuptrue%
wenzelm@44124	1535	%
wenzelm@44124	1536	\begin{isamarkuptext}%
wenzelm@44124	1537	Using the above principles, standard introduction and elimination proofs
wenzelm@44124	1538	of predicate logic connectives of HOL work as follows.%
wenzelm@44124	1539	\end{isamarkuptext}%
wenzelm@44124	1540	\isamarkuptrue%
wenzelm@44124	1541	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1542	\isanewline
wenzelm@44124	1543	\isakeyword{begin}\isanewline
wenzelm@44124	1544	%
wenzelm@44124	1545	\isadelimproof
wenzelm@44124	1546	\ \ %
wenzelm@44124	1547	\endisadelimproof
wenzelm@44124	1548	%
wenzelm@44124	1549	\isatagproof
wenzelm@44124	1550	\isacommand{have}\isamarkupfalse%
wenzelm@44124	1551	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1552	\isanewline
wenzelm@44124	1553	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1554	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1555	\ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1556	\isanewline
wenzelm@44124	1557	\isanewline
wenzelm@44124	1558	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1559	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1560	\isanewline
wenzelm@44124	1561	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1562	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1563	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1564	\isanewline
wenzelm@44124	1565	\isanewline
wenzelm@44124	1566	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1567	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1568	\isanewline
wenzelm@44124	1569	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1570	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1571	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1572	\isanewline
wenzelm@44124	1573	\isanewline
wenzelm@44124	1574	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1575	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1576	\isanewline
wenzelm@44124	1577	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1578	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1579	\ C\isanewline
wenzelm@44124	1580	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1581	\isanewline
wenzelm@44124	1582	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1583	\ A\isanewline
wenzelm@44124	1584	\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1585	\ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1586	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1587	\isanewline
wenzelm@44124	1588	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44124	1589	\isanewline
wenzelm@44124	1590	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1591	\ B\isanewline
wenzelm@44124	1592	\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1593	\ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1594	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1595	\isanewline
wenzelm@44124	1596	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1597	\isanewline
wenzelm@44124	1598	\isanewline
wenzelm@44124	1599	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1600	\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1601	\isanewline
wenzelm@44124	1602	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1603	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1604	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1605	\isanewline
wenzelm@44124	1606	\isanewline
wenzelm@44124	1607	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1608	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1609	\isanewline
wenzelm@44124	1610	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1611	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1612	\ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1613	\isanewline
wenzelm@44124	1614	\isanewline
wenzelm@44124	1615	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1616	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1617	\isanewline
wenzelm@44124	1618	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1619	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1620	\ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1621	\isanewline
wenzelm@44124	1622	\isanewline
wenzelm@44124	1623	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1624	\ False\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1625	\isanewline
wenzelm@44124	1626	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1627	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1628	\ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1629	\isanewline
wenzelm@44124	1630	\isanewline
wenzelm@44124	1631	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1632	\ True\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1633	\isanewline
wenzelm@44124	1634	\isanewline
wenzelm@44124	1635	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1636	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1637	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1638	\isanewline
wenzelm@44124	1639	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1640	\ A\isanewline
wenzelm@44124	1641	\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1642	\ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1643	\ False\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1644	\isanewline
wenzelm@44124	1645	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1646	\isanewline
wenzelm@44124	1647	\isanewline
wenzelm@44124	1648	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1649	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1650	\isanewline
wenzelm@44124	1651	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1652	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1653	\ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1654	\isanewline
wenzelm@44124	1655	\isanewline
wenzelm@44124	1656	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1657	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1658	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1659	\isanewline
wenzelm@44124	1660	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	1661	\ x\isanewline
wenzelm@44124	1662	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1663	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1664	\isanewline
wenzelm@44124	1665	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1666	\isanewline
wenzelm@44124	1667	\isanewline
wenzelm@44124	1668	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1669	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1670	\isanewline
wenzelm@44124	1671	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1672	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1673	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1674	\isanewline
wenzelm@44124	1675	\isanewline
wenzelm@44124	1676	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1677	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1678	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1679	\isanewline
wenzelm@44124	1680	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1681	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1682	\isanewline
wenzelm@44124	1683	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1684	\isanewline
wenzelm@44124	1685	\isanewline
wenzelm@44124	1686	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1687	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1688	\isanewline
wenzelm@44124	1689	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1690	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1691	\ C\isanewline
wenzelm@44124	1692	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1693	\isanewline
wenzelm@44124	1694	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	1695	\ a\isanewline
wenzelm@44124	1696	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1697	\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1698	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1699	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1700	\isanewline
wenzelm@44124	1701	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1702	%
wenzelm@44124	1703	\begin{isamarkuptxt}%
wenzelm@44124	1704	Less awkward version using \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}:%
wenzelm@44124	1705	\end{isamarkuptxt}%
wenzelm@44124	1706	\isamarkuptrue%
wenzelm@44124	1707	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1708	\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1709	\isanewline
wenzelm@44124	1710	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1711	\ \isacommand{obtain}\isamarkupfalse%
wenzelm@44124	1712	\ a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1713	%
wenzelm@44124	1714	\endisatagproof
wenzelm@44124	1715	{\isafoldproof}%
wenzelm@44124	1716	%
wenzelm@44124	1717	\isadelimproof
wenzelm@44124	1718	\isanewline
wenzelm@44124	1719	%
wenzelm@44124	1720	\endisadelimproof
wenzelm@44124	1721	\isacommand{end}\isamarkupfalse%
wenzelm@44124	1722	%
wenzelm@44124	1723	\begin{isamarkuptext}%
wenzelm@44124	1724	Further variations to illustrate Isar sub-proofs involving
wenzelm@44124	1725	\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}:%
wenzelm@44124	1726	\end{isamarkuptext}%
wenzelm@44124	1727	\isamarkuptrue%
wenzelm@44124	1728	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1729	\isanewline
wenzelm@44124	1730	\isakeyword{begin}\isanewline
wenzelm@44124	1731	%
wenzelm@44124	1732	\isadelimproof
wenzelm@44124	1733	\ \ %
wenzelm@44124	1734	\endisadelimproof
wenzelm@44124	1735	%
wenzelm@44124	1736	\isatagproof
wenzelm@44124	1737	\isacommand{have}\isamarkupfalse%
wenzelm@44124	1738	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1739	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1740	\ \ %
wenzelm@44124	1741	\isamarkupcmt{two strictly isolated subproofs%
wenzelm@44124	1742	}
wenzelm@44124	1743	\isanewline
wenzelm@44124	1744	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1745	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1746	\isanewline
wenzelm@44124	1747	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44124	1748	\isanewline
wenzelm@44124	1749	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1750	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1751	\isanewline
wenzelm@44124	1752	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1753	\isanewline
wenzelm@44124	1754	\isanewline
wenzelm@44124	1755	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1756	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1757	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1758	\ \ %
wenzelm@44124	1759	\isamarkupcmt{one simultaneous sub-proof%
wenzelm@44124	1760	}
wenzelm@44124	1761	\isanewline
wenzelm@44124	1762	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1763	\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1764	\isanewline
wenzelm@44124	1765	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1766	\isanewline
wenzelm@44124	1767	\isanewline
wenzelm@44124	1768	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1769	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1770	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1771	\ \ %
wenzelm@44124	1772	\isamarkupcmt{two subproofs in the same context%
wenzelm@44124	1773	}
wenzelm@44124	1774	\isanewline
wenzelm@44124	1775	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1776	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1777	\isanewline
wenzelm@44124	1778	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1779	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1780	\isanewline
wenzelm@44124	1781	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1782	\isanewline
wenzelm@44124	1783	\isanewline
wenzelm@44124	1784	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1785	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1786	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1787	\ \ %
wenzelm@44124	1788	\isamarkupcmt{swapped order%
wenzelm@44124	1789	}
wenzelm@44124	1790	\isanewline
wenzelm@44124	1791	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1792	\ B\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1793	\isanewline
wenzelm@44124	1794	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1795	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1796	\isanewline
wenzelm@44124	1797	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1798	\isanewline
wenzelm@44124	1799	\isanewline
wenzelm@44124	1800	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1801	\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1802	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1803	\ \ %
wenzelm@44124	1804	\isamarkupcmt{sequential subproofs%
wenzelm@44124	1805	}
wenzelm@44124	1806	\isanewline
wenzelm@44124	1807	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1808	\ A\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1809	\isanewline
wenzelm@44124	1810	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1811	\ B\ \isacommand{using}\isamarkupfalse%
wenzelm@44124	1812	\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1813	\isanewline
wenzelm@44124	1814	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1815	%
wenzelm@44124	1816	\endisatagproof
wenzelm@44124	1817	{\isafoldproof}%
wenzelm@44124	1818	%
wenzelm@44124	1819	\isadelimproof
wenzelm@44124	1820	\isanewline
wenzelm@44124	1821	%
wenzelm@44124	1822	\endisadelimproof
wenzelm@44124	1823	\isacommand{end}\isamarkupfalse%
wenzelm@44124	1824	%
wenzelm@44124	1825	\isamarkupsubsubsection{Example: set-theoretic operators%
wenzelm@44124	1826	}
wenzelm@44124	1827	\isamarkuptrue%
wenzelm@44124	1828	%
wenzelm@44124	1829	\begin{isamarkuptext}%
wenzelm@44124	1830	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@44124	1831	set-theory or lattice-theory for analogously. It is only a matter
wenzelm@44124	1832	of rule declarations in the library; rules can be also specified
wenzelm@44124	1833	explicitly.%
wenzelm@44124	1834	\end{isamarkuptext}%
wenzelm@44124	1835	\isamarkuptrue%
wenzelm@44124	1836	\isacommand{notepad}\isamarkupfalse%
wenzelm@44124	1837	\isanewline
wenzelm@44124	1838	\isakeyword{begin}\isanewline
wenzelm@44124	1839	%
wenzelm@44124	1840	\isadelimproof
wenzelm@44124	1841	\ \ %
wenzelm@44124	1842	\endisadelimproof
wenzelm@44124	1843	%
wenzelm@44124	1844	\isatagproof
wenzelm@44124	1845	\isacommand{have}\isamarkupfalse%
wenzelm@44124	1846	\ {\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	1847	\isanewline
wenzelm@44124	1848	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1849	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1850	\ {\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	1851	\isanewline
wenzelm@44124	1852	\isanewline
wenzelm@44124	1853	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1854	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1855	\isanewline
wenzelm@44124	1856	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1857	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1858	\ {\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	1859	\isanewline
wenzelm@44124	1860	\isanewline
wenzelm@44124	1861	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1862	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1863	\isanewline
wenzelm@44124	1864	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1865	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1866	\ {\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	1867	\isanewline
wenzelm@44124	1868	\isanewline
wenzelm@44124	1869	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1870	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1871	\isanewline
wenzelm@44124	1872	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1873	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1874	\ C\isanewline
wenzelm@44124	1875	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1876	\isanewline
wenzelm@44124	1877	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1878	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1879	\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1880	\ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1881	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1882	\isanewline
wenzelm@44124	1883	\ \ \isacommand{next}\isamarkupfalse%
wenzelm@44124	1884	\isanewline
wenzelm@44124	1885	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1886	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1887	\ \ \ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1888	\ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1889	\ C\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1890	\isanewline
wenzelm@44124	1891	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1892	\isanewline
wenzelm@44124	1893	\isanewline
wenzelm@44124	1894	\isacommand{next}\isamarkupfalse%
wenzelm@44124	1895	\isanewline
wenzelm@44124	1896	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1897	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1898	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1899	\isanewline
wenzelm@44124	1900	\ \ \ \ \isacommand{fix}\isamarkupfalse%
wenzelm@44124	1901	\ a\isanewline
wenzelm@44124	1902	\ \ \ \ \isacommand{assume}\isamarkupfalse%
wenzelm@44124	1903	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1904	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1905	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1906	\isanewline
wenzelm@44124	1907	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1908	\isanewline
wenzelm@44124	1909	\isanewline
wenzelm@44124	1910	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1911	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1912	\isanewline
wenzelm@44124	1913	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1914	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1915	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
wenzelm@44124	1916	\ \ \isacommand{proof}\isamarkupfalse%
wenzelm@44124	1917	\isanewline
wenzelm@44124	1918	\ \ \ \ \isacommand{show}\isamarkupfalse%
wenzelm@44124	1919	\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1920	\isanewline
wenzelm@44124	1921	\ \ \isacommand{qed}\isamarkupfalse%
wenzelm@44124	1922	\isanewline
wenzelm@44124	1923	\isanewline
wenzelm@44124	1924	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1925	\ {\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	1926	\isanewline
wenzelm@44124	1927	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1928	\ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1929	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
wenzelm@44124	1930	\isanewline
wenzelm@44124	1931	\isanewline
wenzelm@44124	1932	\ \ \isacommand{have}\isamarkupfalse%
wenzelm@44124	1933	\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
wenzelm@44124	1934	\isanewline
wenzelm@44124	1935	\ \ \isacommand{then}\isamarkupfalse%
wenzelm@44124	1936	\ \isacommand{obtain}\isamarkupfalse%
wenzelm@44124	1937	\ 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	1938	%
wenzelm@44124	1939	\endisatagproof
wenzelm@44124	1940	{\isafoldproof}%
wenzelm@44124	1941	%
wenzelm@44124	1942	\isadelimproof
wenzelm@44124	1943	\isanewline
wenzelm@44124	1944	%
wenzelm@44124	1945	\endisadelimproof
wenzelm@44124	1946	\isacommand{end}\isamarkupfalse%
wenzelm@44121	1947	\isanewline
wenzelm@44121	1948	%
wenzelm@44121	1949	\isadelimtheory
wenzelm@44121	1950	\isanewline
wenzelm@44121	1951	%
wenzelm@44121	1952	\endisadelimtheory
wenzelm@44121	1953	%
wenzelm@44121	1954	\isatagtheory
wenzelm@44121	1955	\isacommand{end}\isamarkupfalse%
wenzelm@44121	1956	%
wenzelm@44121	1957	\endisatagtheory
wenzelm@44121	1958	{\isafoldtheory}%
wenzelm@44121	1959	%
wenzelm@44121	1960	\isadelimtheory
wenzelm@44121	1961	%
wenzelm@44121	1962	\endisadelimtheory
wenzelm@44121	1963	\end{isabellebody}%
wenzelm@44121	1964	%%% Local Variables:
wenzelm@44121	1965	%%% mode: latex
wenzelm@44121	1966	%%% TeX-master: "root"
wenzelm@44121	1967	%%% End:

author	wenzelm
	Wed, 01 Jun 2011 13:06:45 +0200
changeset 44124	8c0a49d72857
parent 44123	6e83c2f73240
child 44125	ec270c6cb942
permissions	-rw-r--r--