isabelle: src/Doc/Logics_ZF/FOL_examples.thy@13dc5fe14a49 (annotated)

67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 66453 diff changeset	1	section\<open>Examples of Classical Reasoning\<close>
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	2
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 58889 diff changeset	3	theory FOL_examples imports FOL begin
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	4
12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	5	lemma "EX y. ALL x. P(y)-->P(x)"
67443 3abf6a722518 standardized towards new-style formal comments: isabelle update_comments; wenzelm parents: 67406 diff changeset	6	\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	7	apply (rule exCI)
67443 3abf6a722518 standardized towards new-style formal comments: isabelle update_comments; wenzelm parents: 67406 diff changeset	8	\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	9	apply (rule allI)
67443 3abf6a722518 standardized towards new-style formal comments: isabelle update_comments; wenzelm parents: 67406 diff changeset	10	\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	11	apply (rule impI)
67443 3abf6a722518 standardized towards new-style formal comments: isabelle update_comments; wenzelm parents: 67406 diff changeset	12	\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	13	apply (erule allE)
67443 3abf6a722518 standardized towards new-style formal comments: isabelle update_comments; wenzelm parents: 67406 diff changeset	14	\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
69505 cc2d676d5395 isabelle update_cartouches -t; wenzelm parents: 67443 diff changeset	15	txt\<open>see below for \<open>allI\<close> combined with \<open>swap\<close>\<close>
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	16	apply (erule allI [THEN [2] swap])
67443 3abf6a722518 standardized towards new-style formal comments: isabelle update_comments; wenzelm parents: 67406 diff changeset	17	\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	18	apply (rule impI)
67443 3abf6a722518 standardized towards new-style formal comments: isabelle update_comments; wenzelm parents: 67406 diff changeset	19	\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	20	apply (erule notE)
67443 3abf6a722518 standardized towards new-style formal comments: isabelle update_comments; wenzelm parents: 67406 diff changeset	21	\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	22	apply assumption
12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	23	done
12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	24
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 66453 diff changeset	25	text \<open>
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	26	@{thm[display] allI [THEN [2] swap]}
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 66453 diff changeset	27	\<close>
14152 12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	28
12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	29	lemma "EX y. ALL x. P(y)-->P(x)"
12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	30	by blast
12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	31
12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	32	end
12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	33
12f6f18e7afc For the Isar version of the ZF logics manual paulson parents: diff changeset	34

author	wenzelm
	Thu, 20 Aug 2020 21:56:28 +0200
changeset 72183	13dc5fe14a49
parent 69505	cc2d676d5395
permissions	-rw-r--r--