isabelle: src/HOLCF/Fix.ML@f9163c6f69d6 (annotated)

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	2	(* legacy ML bindings *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	4	val iterate_0 = thm "iterate_0";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	5	val iterate_Suc = thm "iterate_Suc";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	6	val Ifix_def = thm "Ifix_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	7	val fix_def = thm "fix_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	8	val adm_def = thm "adm_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	9	val admw_def = thm "admw_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	10	val iterate_Suc2 = thm "iterate_Suc2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	11	val chain_iterate2 = thm "chain_iterate2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	12	val chain_iterate = thm "chain_iterate";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	13	val Ifix_eq = thm "Ifix_eq";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	14	val Ifix_least = thm "Ifix_least";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	15	val monofun_iterate = thm "monofun_iterate";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	16	val contlub_iterate = thm "contlub_iterate";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	17	val cont_iterate = thm "cont_iterate";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	18	val monofun_iterate2 = thm "monofun_iterate2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	19	val contlub_iterate2 = thm "contlub_iterate2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	20	val cont_iterate2 = thm "cont_iterate2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	21	val monofun_Ifix = thm "monofun_Ifix";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	22	val chain_iterate_lub = thm "chain_iterate_lub";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	23	val contlub_Ifix_lemma1 = thm "contlub_Ifix_lemma1";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	24	val ex_lub_iterate = thm "ex_lub_iterate";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	25	val contlub_Ifix = thm "contlub_Ifix";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	26	val cont_Ifix = thm "cont_Ifix";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	27	val fix_eq = thm "fix_eq";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	28	val fix_least = thm "fix_least";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	29	val fix_eqI = thm "fix_eqI";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	30	val fix_eq2 = thm "fix_eq2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	31	val fix_eq3 = thm "fix_eq3";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	32	val fix_eq4 = thm "fix_eq4";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	33	val fix_eq5 = thm "fix_eq5";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	34	val Ifix_def2 = thm "Ifix_def2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	35	val fix_def2 = thm "fix_def2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	36	val admI = thm "admI";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	37	val triv_admI = thm "triv_admI";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	38	val admD = thm "admD";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	39	val admw_def2 = thm "admw_def2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	40	val def_fix_ind = thm "def_fix_ind";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	41	val adm_impl_admw = thm "adm_impl_admw";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	42	val fix_ind = thm "fix_ind";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	43	val def_fix_ind = thm "def_fix_ind";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	44	val wfix_ind = thm "wfix_ind";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	45	val def_wfix_ind = thm "def_wfix_ind";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	46	val adm_max_in_chain = thm "adm_max_in_chain";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	47	val adm_chfin = thm "adm_chfin";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	48	val adm_chfindom = thm "adm_chfindom";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	49	val admI2 = thm "admI2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	50	val adm_less = thm "adm_less";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	51	val adm_conj = thm "adm_conj";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	52	val adm_not_free = thm "adm_not_free";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	53	val adm_not_less = thm "adm_not_less";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	54	val adm_all = thm "adm_all";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	55	val adm_all2 = thm "adm_all2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	56	val adm_subst = thm "adm_subst";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	57	val adm_UU_not_less = thm "adm_UU_not_less";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	58	val adm_not_UU = thm "adm_not_UU";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	59	val adm_eq = thm "adm_eq";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	60	val adm_disj_lemma1 = thm "adm_disj_lemma1";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	61	val adm_disj_lemma2 = thm "adm_disj_lemma2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	62	val adm_disj_lemma3 = thm "adm_disj_lemma3";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	63	val adm_disj_lemma4 = thm "adm_disj_lemma4";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	64	val adm_disj_lemma5 = thm "adm_disj_lemma5";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	65	val adm_disj_lemma6 = thm "adm_disj_lemma6";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	66	val adm_disj_lemma7 = thm "adm_disj_lemma7";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	67	val adm_disj_lemma8 = thm "adm_disj_lemma8";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	68	val adm_disj_lemma9 = thm "adm_disj_lemma9";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	69	val adm_disj_lemma10 = thm "adm_disj_lemma10";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	70	val adm_disj_lemma12 = thm "adm_disj_lemma12";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	71	val adm_lemma11 = thm "adm_lemma11";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	72	val adm_disj = thm "adm_disj";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	73	val adm_imp = thm "adm_imp";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	74	val adm_iff = thm "adm_iff";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	75	val adm_not_conj = thm "adm_not_conj";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	76	val adm_lemmas = [adm_not_free, adm_imp, adm_disj, adm_eq, adm_not_UU,
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	77	adm_UU_not_less, adm_all2, adm_not_less, adm_not_conj, adm_iff]
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	78
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	79	structure Fix =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	80	struct
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	81	val thy = the_context ();
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	82	val Ifix_def = Ifix_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	83	val fix_def = fix_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	84	val adm_def = adm_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	85	val admw_def = admw_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	86	end;
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	87
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	88	fun fix_tac3 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i));
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	89
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	90	fun fix_tac5 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i));
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	91
10834 a7897aebbffc * empty log message * nipkow parents: 10230 diff changeset	92	(* proves the unfolding theorem for function equations f = fix$... *)
3652 4c484f03079c added case_prover oheimb parents: 3460 diff changeset	93	fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	94	(rtac trans 1),
3652 4c484f03079c added case_prover oheimb parents: 3460 diff changeset	95	(rtac (fixeq RS fix_eq4) 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	96	(rtac trans 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	97	(rtac beta_cfun 1),
2566 cbf02fc74332 changed handling of cont_lemmas and adm_lemmas oheimb parents: 2354 diff changeset	98	(Simp_tac 1)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	99	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	100
10834 a7897aebbffc * empty log message * nipkow parents: 10230 diff changeset	101	(* proves the unfolding theorem for function definitions f == fix$... *)
3652 4c484f03079c added case_prover oheimb parents: 3460 diff changeset	102	fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1410 diff changeset	103	(rtac trans 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1410 diff changeset	104	(rtac (fix_eq2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1410 diff changeset	105	(rtac fixdef 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1410 diff changeset	106	(rtac beta_cfun 1),
2566 cbf02fc74332 changed handling of cont_lemmas and adm_lemmas oheimb parents: 2354 diff changeset	107	(Simp_tac 1)
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	108	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	109
3652 4c484f03079c added case_prover oheimb parents: 3460 diff changeset	110	(* proves an application case for a function from its unfolding thm *)
4c484f03079c added case_prover oheimb parents: 3460 diff changeset	111	fun case_prover thy unfold s = prove_goal thy s (fn prems => [
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	112	(cut_facts_tac prems 1),
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	113	(rtac trans 1),
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	114	(stac unfold 1),
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	115	Auto_tac
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	116	]);

author	wenzelm
	Tue, 17 May 2005 09:58:40 +0200
changeset 15967	f9163c6f69d6
parent 15576	efb95d0d01f7
child 16005	42f3f299ee68
permissions	-rw-r--r--