isabelle: src/HOLCF/Fix.ML@46a7e133f802 (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
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	4	val adm_chfindom = thm "adm_chfindom";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	5	val adm_impl_admw = thm "adm_impl_admw";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	6	val admw_def = thm "admw_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	7	val chain_iterate2 = thm "chain_iterate2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	8	val chain_iterate = thm "chain_iterate";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	9	val def_fix_ind = thm "def_fix_ind";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	10	val def_wfix_ind = thm "def_wfix_ind";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	11	val fix_const = thm "fix_const";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	12	val fix_def2 = thm "fix_def2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	13	val fix_defined = thm "fix_defined";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	14	val fix_defined_iff = thm "fix_defined_iff";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	15	val fix_def = thm "fix_def";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	16	val fix_eq2 = thm "fix_eq2";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	17	val fix_eq3 = thm "fix_eq3";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	18	val fix_eq4 = thm "fix_eq4";
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	19	val fix_eq5 = thm "fix_eq5";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	20	val fix_eqI = thm "fix_eqI";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	21	val fix_eq = thm "fix_eq";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	22	val fix_id = thm "fix_id";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	23	val fix_ind = thm "fix_ind";
16922 2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	24	val fix_least = thm "fix_least";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	25	val fix_strict = thm "fix_strict";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	26	val iterate_0 = thm "iterate_0";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	27	val iterate_Suc2 = thm "iterate_Suc2";
2128ac2aa5db brought ML files up to date with new lemmas huffman parents: 16214 diff changeset	28	val iterate_Suc = thm "iterate_Suc";
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	29	val wfix_ind = thm "wfix_ind";
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	31	structure Fix =
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	32	struct
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	33	val thy = the_context ();
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	34	val fix_def = fix_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	35	val adm_def = adm_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	36	val admw_def = admw_def;
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	37	end;
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	38
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	39	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	40
15576 efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	41	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	42
10834 a7897aebbffc * empty log message * nipkow parents: 10230 diff changeset	43	(* proves the unfolding theorem for function equations f = fix$... *)
3652 4c484f03079c added case_prover oheimb parents: 3460 diff changeset	44	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	45	(rtac trans 1),
3652 4c484f03079c added case_prover oheimb parents: 3460 diff changeset	46	(rtac (fixeq RS fix_eq4) 1),
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	47	(rtac trans 1),
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	48	(rtac beta_cfun 1),
2566 cbf02fc74332 changed handling of cont_lemmas and adm_lemmas oheimb parents: 2354 diff changeset	49	(Simp_tac 1)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	50	]);
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	51
10834 a7897aebbffc * empty log message * nipkow parents: 10230 diff changeset	52	(* proves the unfolding theorem for function definitions f == fix$... *)
3652 4c484f03079c added case_prover oheimb parents: 3460 diff changeset	53	fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1410 diff changeset	54	(rtac trans 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1410 diff changeset	55	(rtac (fix_eq2) 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1410 diff changeset	56	(rtac fixdef 1),
6bcb44e4d6e5 expanded tabs clasohm parents: 1410 diff changeset	57	(rtac beta_cfun 1),
2566 cbf02fc74332 changed handling of cont_lemmas and adm_lemmas oheimb parents: 2354 diff changeset	58	(Simp_tac 1)
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 892 diff changeset	59	]);
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	60
3652 4c484f03079c added case_prover oheimb parents: 3460 diff changeset	61	(* proves an application case for a function from its unfolding thm *)
4c484f03079c added case_prover oheimb parents: 3460 diff changeset	62	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	63	(cut_facts_tac prems 1),
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	64	(rtac trans 1),
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	65	(stac unfold 1),
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	66	Auto_tac
efb95d0d01f7 converted to new-style theories, and combined numbered files huffman parents: 14981 diff changeset	67	]);

author	haftmann
	Mon, 24 Apr 2006 16:35:30 +0200
changeset 19454	46a7e133f802
parent 18074	a92b7c5133de
permissions	-rw-r--r--