isabelle: src/HOL/Proofs/Extraction/Util.thy@0b1c830ebf3a (annotated)

39157 b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 32960 diff changeset	1	(* Title: HOL/Proofs/Extraction/Util.thy
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	2	Author: Stefan Berghofer, TU Muenchen
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	3	*)
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	4
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 59730 diff changeset	5	section \<open>Auxiliary lemmas used in program extraction examples\<close>
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	6
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	7	theory Util
66258 2b83dd24b301 dropped superfluous theory imports haftmann parents: 63361 diff changeset	8	imports Main
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	9	begin
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	10
63361 d10eab0672f9 misc tuning and modernization; wenzelm parents: 61986 diff changeset	11	text \<open>Decidability of equality on natural numbers.\<close>
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	12
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	13	lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	14	apply (induct m)
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	15	apply (case_tac n)
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	16	apply (case_tac [3] n)
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	17	apply (simp only: nat.simps, iprover?)+
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	18	done
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	19
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 59730 diff changeset	20	text \<open>
63361 d10eab0672f9 misc tuning and modernization; wenzelm parents: 61986 diff changeset	21	Well-founded induction on natural numbers, derived using the standard
d10eab0672f9 misc tuning and modernization; wenzelm parents: 61986 diff changeset	22	structural induction rule.
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 59730 diff changeset	23	\<close>
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	24
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	25	lemma nat_wf_ind:
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	26	assumes R: "\<And>x::nat. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	27	shows "P z"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	28	proof (rule R)
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	29	show "\<And>y. y < z \<Longrightarrow> P y"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	30	proof (induct z)
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	31	case 0
63361 d10eab0672f9 misc tuning and modernization; wenzelm parents: 61986 diff changeset	32	then show ?case by simp
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	33	next
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	34	case (Suc n y)
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	35	from nat_eq_dec show ?case
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	36	proof
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	37	assume ny: "n = y"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	38	have "P n"
32960 69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	39	by (rule R) (rule Suc)
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	40	with ny show ?case by simp
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	41	next
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	42	assume "n \<noteq> y"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	43	with Suc have "y < n" by simp
63361 d10eab0672f9 misc tuning and modernization; wenzelm parents: 61986 diff changeset	44	then show ?case by (rule Suc)
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	45	qed
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	46	qed
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	47	qed
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	48
63361 d10eab0672f9 misc tuning and modernization; wenzelm parents: 61986 diff changeset	49	text \<open>Bounded search for a natural number satisfying a decidable predicate.\<close>
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	50
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	51	lemma search:
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	52	assumes dec: "\<And>x::nat. P x \<or> \<not> P x"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	53	shows "(\<exists>x<y. P x) \<or> \<not> (\<exists>x<y. P x)"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	54	proof (induct y)
63361 d10eab0672f9 misc tuning and modernization; wenzelm parents: 61986 diff changeset	55	case 0
d10eab0672f9 misc tuning and modernization; wenzelm parents: 61986 diff changeset	56	show ?case by simp
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	57	next
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	58	case (Suc z)
63361 d10eab0672f9 misc tuning and modernization; wenzelm parents: 61986 diff changeset	59	then show ?case
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	60	proof
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	61	assume "\<exists>x<z. P x"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	62	then obtain x where le: "x < z" and P: "P x" by iprover
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	63	from le have "x < Suc z" by simp
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	64	with P show ?case by iprover
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	65	next
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	66	assume nex: "\<not> (\<exists>x<z. P x)"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	67	from dec show ?case
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	68	proof
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	69	assume P: "P z"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	70	have "z < Suc z" by simp
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	71	with P show ?thesis by iprover
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	72	next
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	73	assume nP: "\<not> P z"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	74	have "\<not> (\<exists>x<Suc z. P x)"
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	75	proof
32960 69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	76	assume "\<exists>x<Suc z. P x"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	77	then obtain x where le: "x < Suc z" and P: "P x" by iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	78	have "x < z"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	79	proof (cases "x = z")
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	80	case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	81	with nP and P show ?thesis by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	82	next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	83	case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	84	with le show ?thesis by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	85	qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	86	with P have "\<exists>x<z. P x" by iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 25421 diff changeset	87	with nex show False ..
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	88	qed
63361 d10eab0672f9 misc tuning and modernization; wenzelm parents: 61986 diff changeset	89	then show ?case by iprover
25421 1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	90	qed
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	91	qed
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	92	qed
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	93
1c5b8d54a339 Moved auxiliary lemmas to separate theory. berghofe parents: diff changeset	94	end

author	wenzelm
	Sat, 11 Jul 2020 14:44:50 +0200
changeset 72011	0b1c830ebf3a
parent 66258	2b83dd24b301
permissions	-rw-r--r--