isabelle: src/HOLCF/Cont.thy@2454493bd77b (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/cont.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	Results about continuity and monotonicity
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	9	theory Cont = Fun3:
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11	(*
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13	Now we change the default class! Form now on all untyped typevariables are
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 2838 diff changeset	14	of default class po
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	19	defaultsort po
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	21	consts
2838 2e908f29bc3d changed continuous functions from pcpo to cpo (including instances) slotosch parents: 1479 diff changeset	22	monofun :: "('a => 'b) => bool" (* monotonicity *)
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances) slotosch parents: 1479 diff changeset	23	contlub :: "('a::cpo => 'b::cpo) => bool" (* first cont. def *)
2e908f29bc3d changed continuous functions from pcpo to cpo (including instances) slotosch parents: 1479 diff changeset	24	cont :: "('a::cpo => 'b::cpo) => bool" (* secnd cont. def *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	25
1168 74be52691d62 The curried version of HOLCF is now just called HOLCF. The old regensbu parents: 1150 diff changeset	26	defs
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	28	monofun: "monofun(f) == ! x y. x << y --> f(x) << f(y)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	30	contlub: "contlub(f) == ! Y. chain(Y) -->
3842 b55686a7b22c fixed dots; wenzelm parents: 3323 diff changeset	31	f(lub(range(Y))) = lub(range(% i. f(Y(i))))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	32
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	33	cont: "cont(f) == ! Y. chain(Y) -->
3842 b55686a7b22c fixed dots; wenzelm parents: 3323 diff changeset	34	range(% i. f(Y(i))) <<\| f(lub(range(Y)))"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	35
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	36	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	37	(* the main purpose of cont.thy is to show: *)
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1168 diff changeset	38	(* monofun(f) & contlub(f) <==> cont(f) *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	39	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	40
15565 2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	41	(* Title: HOLCF/Cont.ML
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	42	ID: $Id$
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	43	Author: Franz Regensburger
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	44	License: GPL (GNU GENERAL PUBLIC LICENSE)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	45
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	46	Results about continuity and monotonicity
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	47	*)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	48
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	49	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	50	(* access to definition *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	51	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	52
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	53	lemma contlubI:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	54	"! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	55	contlub(f)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	56	apply (unfold contlub)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	57	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	58	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	59
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	60	lemma contlubE:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	61	" contlub(f)==>
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	62	! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	63	apply (unfold contlub)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	64	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	65	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	66
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	67
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	68	lemma contI:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	69	"! Y. chain(Y) --> range(% i. f(Y(i))) <<\| f(lub(range(Y))) ==> cont(f)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	70
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	71	apply (unfold cont)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	72	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	73	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	74
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	75	lemma contE:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	76	"cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<\| f(lub(range(Y)))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	77	apply (unfold cont)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	78	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	79	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	80
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	81
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	82	lemma monofunI:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	83	"! x y. x << y --> f(x) << f(y) ==> monofun(f)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	84	apply (unfold monofun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	85	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	86	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	87
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	88	lemma monofunE:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	89	"monofun(f) ==> ! x y. x << y --> f(x) << f(y)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	90	apply (unfold monofun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	91	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	92	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	93
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	94	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	95	(* the main purpose of cont.thy is to show: *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	96	(* monofun(f) & contlub(f) <==> cont(f) *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	97	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	98
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	99	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	100	(* monotone functions map chains to chains *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	101	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	102
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	103	lemma ch2ch_monofun:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	104	"[\| monofun(f); chain(Y) \|] ==> chain(%i. f(Y(i)))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	105	apply (rule chainI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	106	apply (erule monofunE [THEN spec, THEN spec, THEN mp])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	107	apply (erule chainE)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	108	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	109
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	110	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	111	(* monotone functions map upper bound to upper bounds *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	112	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	113
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	114	lemma ub2ub_monofun:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	115	"[\| monofun(f); range(Y) <\| u\|] ==> range(%i. f(Y(i))) <\| f(u)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	116	apply (rule ub_rangeI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	117	apply (erule monofunE [THEN spec, THEN spec, THEN mp])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	118	apply (erule ub_rangeD)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	119	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	120
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	121	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	122	(* left to right: monofun(f) & contlub(f) ==> cont(f) *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	123	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	124
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	125	lemma monocontlub2cont:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	126	"[\|monofun(f);contlub(f)\|] ==> cont(f)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	127	apply (unfold cont)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	128	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	129	apply (rule thelubE)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	130	apply (erule ch2ch_monofun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	131	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	132	apply (erule contlubE [THEN spec, THEN mp, symmetric])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	133	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	134	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	135
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	136	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	137	(* first a lemma about binary chains *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	138	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	139
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	140	lemma binchain_cont: "[\| cont(f); x << y \|]
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	141	==> range(%i::nat. f(if i = 0 then x else y)) <<\| f(y)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	142	apply (rule subst)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	143	prefer 2 apply (erule contE [THEN spec, THEN mp])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	144	apply (erule bin_chain)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	145	apply (rule_tac y = "y" in arg_cong)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	146	apply (erule lub_bin_chain [THEN thelubI])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	147	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	148
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	149	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	150	(* right to left: cont(f) ==> monofun(f) & contlub(f) *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	151	(* part1: cont(f) ==> monofun(f *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	152	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	153
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	154	lemma cont2mono: "cont(f) ==> monofun(f)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	155	apply (unfold monofun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	156	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	157	apply (drule binchain_cont [THEN is_ub_lub])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	158	apply (auto split add: split_if_asm)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	159	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	160
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	161	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	162	(* right to left: cont(f) ==> monofun(f) & contlub(f) *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	163	(* part2: cont(f) ==> contlub(f) *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	164	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	165
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	166	lemma cont2contlub: "cont(f) ==> contlub(f)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	167	apply (unfold contlub)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	168	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	169	apply (rule thelubI [symmetric])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	170	apply (erule contE [THEN spec, THEN mp])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	171	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	172	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	173
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	174	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	175	(* monotone functions map finite chains to finite chains *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	176	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	177
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	178	lemma monofun_finch2finch:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	179	"[\| monofun f; finite_chain Y \|] ==> finite_chain (%n. f (Y n))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	180	apply (unfold finite_chain_def)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	181	apply (force elim!: ch2ch_monofun simp add: max_in_chain_def)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	182	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	183
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	184	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	185	(* The same holds for continuous functions *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	186	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	187
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	188	lemmas cont_finch2finch = cont2mono [THEN monofun_finch2finch, standard]
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	189	(* [\| cont ?f; finite_chain ?Y \|] ==> finite_chain (%n. ?f (?Y n)) *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	190
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	191
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	192	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	193	(* The following results are about a curried function that is monotone *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	194	(* in both arguments *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	195	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	196
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	197	lemma ch2ch_MF2L:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	198	"[\|monofun(MF2); chain(F)\|] ==> chain(%i. MF2 (F i) x)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	199	apply (erule ch2ch_monofun [THEN ch2ch_fun])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	200	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	201	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	202
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	203
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	204	lemma ch2ch_MF2R:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	205	"[\|monofun(MF2(f)); chain(Y)\|] ==> chain(%i. MF2 f (Y i))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	206	apply (erule ch2ch_monofun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	207	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	208	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	209
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	210	lemma ch2ch_MF2LR:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	211	"[\|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)\|] ==>
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	212	chain(%i. MF2(F(i))(Y(i)))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	213	apply (rule chainI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	214	apply (rule trans_less)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	215	apply (erule ch2ch_MF2L [THEN chainE])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	216	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	217	apply (rule monofunE [THEN spec, THEN spec, THEN mp], erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	218	apply (erule chainE)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	219	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	220
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	221
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	222	lemma ch2ch_lubMF2R:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	223	"[\|monofun(MF2::('a::po=>'b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	224	!f. monofun(MF2(f)::('b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	225	chain(F);chain(Y)\|] ==>
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	226	chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	227	apply (rule lub_mono [THEN chainI])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	228	apply (rule ch2ch_MF2R, erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	229	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	230	apply (rule ch2ch_MF2R, erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	231	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	232	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	233	apply (rule chainE)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	234	apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	235	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	236	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	237
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	238
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	239	lemma ch2ch_lubMF2L:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	240	"[\|monofun(MF2::('a::po=>'b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	241	!f. monofun(MF2(f)::('b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	242	chain(F);chain(Y)\|] ==>
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	243	chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	244	apply (rule lub_mono [THEN chainI])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	245	apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	246	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	247	apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	248	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	249	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	250	apply (rule chainE)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	251	apply (rule ch2ch_MF2R, erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	252	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	253	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	254
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	255
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	256	lemma lub_MF2_mono:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	257	"[\|monofun(MF2::('a::po=>'b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	258	!f. monofun(MF2(f)::('b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	259	chain(F)\|] ==>
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	260	monofun(% x. lub(range(% j. MF2 (F j) (x))))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	261	apply (rule monofunI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	262	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	263	apply (rule lub_mono)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	264	apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	265	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	266	apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	267	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	268	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	269	apply (rule monofunE [THEN spec, THEN spec, THEN mp], erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	270	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	271	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	272
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	273	lemma ex_lubMF2:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	274	"[\|monofun(MF2::('a::po=>'b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	275	!f. monofun(MF2(f)::('b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	276	chain(F); chain(Y)\|] ==>
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	277	lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	278	lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	279	apply (rule antisym_less)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	280	apply (rule is_lub_thelub[OF _ ub_rangeI])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	281	apply (erule ch2ch_lubMF2R)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	282	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	283	apply (rule lub_mono)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	284	apply (rule ch2ch_MF2R, erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	285	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	286	apply (erule ch2ch_lubMF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	287	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	288	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	289	apply (rule is_ub_thelub)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	290	apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	291	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	292	apply (rule is_lub_thelub[OF _ ub_rangeI])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	293	apply (erule ch2ch_lubMF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	294	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	295	apply (rule lub_mono)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	296	apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	297	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	298	apply (erule ch2ch_lubMF2R)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	299	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	300	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	301	apply (rule is_ub_thelub)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	302	apply (rule ch2ch_MF2R, erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	303	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	304	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	305
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	306
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	307	lemma diag_lubMF2_1:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	308	"[\|monofun(MF2::('a::po=>'b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	309	!f. monofun(MF2(f)::('b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	310	chain(FY);chain(TY)\|] ==>
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	311	lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	312	lub(range(%i. MF2(FY(i))(TY(i))))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	313	apply (rule antisym_less)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	314	apply (rule is_lub_thelub[OF _ ub_rangeI])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	315	apply (erule ch2ch_lubMF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	316	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	317	apply (rule lub_mono3)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	318	apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	319	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	320	apply (erule ch2ch_MF2LR)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	321	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	322	apply (rule allI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	323	apply (rule_tac m = "i" and n = "ia" in nat_less_cases)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	324	apply (rule_tac x = "ia" in exI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	325	apply (rule chain_mono)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	326	apply (erule allE)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	327	apply (erule ch2ch_MF2R)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	328	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	329	apply (erule ssubst)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	330	apply (rule_tac x = "ia" in exI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	331	apply (rule refl_less)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	332	apply (rule_tac x = "i" in exI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	333	apply (rule chain_mono)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	334	apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	335	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	336	apply (rule lub_mono)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	337	apply (erule ch2ch_MF2LR)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	338	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	339	apply (erule ch2ch_lubMF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	340	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	341	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	342	apply (rule is_ub_thelub)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	343	apply (erule ch2ch_MF2L)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	344	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	345	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	346
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	347	lemma diag_lubMF2_2:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	348	"[\|monofun(MF2::('a::po=>'b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	349	!f. monofun(MF2(f)::('b::po=>'c::cpo));
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	350	chain(FY);chain(TY)\|] ==>
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	351	lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	352	lub(range(%i. MF2(FY(i))(TY(i))))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	353	apply (rule trans)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	354	apply (rule ex_lubMF2)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	355	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	356	apply (erule diag_lubMF2_1)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	357	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	358	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	359
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	360
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	361	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	362	(* The following results are about a curried function that is continuous *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	363	(* in both arguments *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	364	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	365
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	366	lemma contlub_CF2:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	367	assumes prem1: "cont(CF2)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	368	assumes prem2: "!f. cont(CF2(f))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	369	assumes prem3: "chain(FY)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	370	assumes prem4: "chain(TY)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	371	shows "CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	372	apply (subst prem1 [THEN cont2contlub, THEN contlubE, THEN spec, THEN mp])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	373	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	374	apply (subst thelub_fun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	375	apply (rule prem1 [THEN cont2mono [THEN ch2ch_monofun]])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	376	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	377	apply (rule trans)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	378	apply (rule prem2 [THEN spec, THEN cont2contlub, THEN contlubE, THEN spec, THEN mp, THEN ext, THEN arg_cong, THEN arg_cong])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	379	apply (rule prem4)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	380	apply (rule diag_lubMF2_2)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	381	apply (auto simp add: cont2mono prems)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	382	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	383
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	384	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	385	(* The following results are about application for functions in 'a=>'b *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	386	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	387
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	388	lemma monofun_fun_fun: "f1 << f2 ==> f1(x) << f2(x)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	389	apply (erule less_fun [THEN iffD1, THEN spec])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	390	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	391
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	392	lemma monofun_fun_arg: "[\|monofun(f); x1 << x2\|] ==> f(x1) << f(x2)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	393	apply (erule monofunE [THEN spec, THEN spec, THEN mp])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	394	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	395	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	396
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	397	lemma monofun_fun: "[\|monofun(f1); monofun(f2); f1 << f2; x1 << x2\|] ==> f1(x1) << f2(x2)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	398	apply (rule trans_less)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	399	apply (erule monofun_fun_arg)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	400	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	401	apply (erule monofun_fun_fun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	402	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	403
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	404
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	405	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	406	(* The following results are about the propagation of monotonicity and *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	407	(* continuity *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	408	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	409
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	410	lemma mono2mono_MF1L: "[\|monofun(c1)\|] ==> monofun(%x. c1 x y)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	411	apply (rule monofunI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	412	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	413	apply (erule monofun_fun_arg [THEN monofun_fun_fun])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	414	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	415	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	416
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	417	lemma cont2cont_CF1L: "[\|cont(c1)\|] ==> cont(%x. c1 x y)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	418	apply (rule monocontlub2cont)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	419	apply (erule cont2mono [THEN mono2mono_MF1L])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	420	apply (rule contlubI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	421	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	422	apply (frule asm_rl)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	423	apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN ssubst])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	424	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	425	apply (subst thelub_fun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	426	apply (rule ch2ch_monofun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	427	apply (erule cont2mono)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	428	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	429	apply (rule refl)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	430	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	431
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	432	(******* Note "(%x.%y.c1 x y) = c1" *********)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	433
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	434	lemma mono2mono_MF1L_rev: "!y. monofun(%x. c1 x y) ==> monofun(c1)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	435	apply (rule monofunI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	436	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	437	apply (rule less_fun [THEN iffD2])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	438	apply (blast dest: monofunE)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	439	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	440
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	441	lemma cont2cont_CF1L_rev: "!y. cont(%x. c1 x y) ==> cont(c1)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	442	apply (rule monocontlub2cont)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	443	apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	444	apply (erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	445	apply (rule contlubI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	446	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	447	apply (rule ext)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	448	apply (subst thelub_fun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	449	apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev, THEN ch2ch_monofun])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	450	apply (erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	451	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	452	apply (blast dest: cont2contlub [THEN contlubE])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	453	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	454
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	455	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	456	(* What D.A.Schmidt calls continuity of abstraction *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	457	(* never used here *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	458	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	459
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	460	lemma contlub_abstraction:
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	461	"[\|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)\|] ==>
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	462	(%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	463	apply (rule trans)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	464	prefer 2 apply (rule cont2contlub [THEN contlubE, THEN spec, THEN mp])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	465	prefer 2 apply (assumption)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	466	apply (erule cont2cont_CF1L_rev)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	467	apply (rule ext)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	468	apply (rule cont2contlub [THEN contlubE, THEN spec, THEN mp, symmetric])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	469	apply (erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	470	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	471	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	472
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	473	lemma mono2mono_app: "[\|monofun(ft);!x. monofun(ft(x));monofun(tt)\|] ==>
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	474	monofun(%x.(ft(x))(tt(x)))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	475	apply (rule monofunI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	476	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	477	apply (rule_tac ?f1.0 = "ft(x)" and ?f2.0 = "ft(y)" in monofun_fun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	478	apply (erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	479	apply (erule spec)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	480	apply (erule monofunE [THEN spec, THEN spec, THEN mp])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	481	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	482	apply (erule monofunE [THEN spec, THEN spec, THEN mp])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	483	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	484	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	485
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	486
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	487	lemma cont2contlub_app: "[\|cont(ft);!x. cont(ft(x));cont(tt)\|] ==> contlub(%x.(ft(x))(tt(x)))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	488	apply (rule contlubI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	489	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	490	apply (rule_tac f3 = "tt" in contlubE [THEN spec, THEN mp, THEN ssubst])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	491	apply (erule cont2contlub)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	492	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	493	apply (rule contlub_CF2)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	494	apply (assumption+)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	495	apply (erule cont2mono [THEN ch2ch_monofun])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	496	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	497	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	498
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	499
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	500	lemma cont2cont_app: "[\|cont(ft); !x. cont(ft(x)); cont(tt)\|] ==> cont(%x.(ft(x))(tt(x)))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	501	apply (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	502	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	503
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	504
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	505	lemmas cont2cont_app2 = cont2cont_app[OF _ allI]
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	506	(* [\| cont ?ft; !!x. cont (?ft x); cont ?tt \|] ==> *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	507	(* cont (%x. ?ft x (?tt x)) *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	508
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	509
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	510	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	511	(* The identity function is continuous *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	512	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	513
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	514	lemma cont_id: "cont(% x. x)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	515	apply (rule contI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	516	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	517	apply (erule thelubE)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	518	apply (rule refl)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	519	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	520
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	521	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	522	(* constant functions are continuous *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	523	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	524
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	525	lemma cont_const: "cont(%x. c)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	526	apply (unfold cont)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	527	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	528	apply (blast intro: is_lubI ub_rangeI dest: ub_rangeD)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	529	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	530
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	531
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	532	lemma cont2cont_app3: "[\|cont(f); cont(t) \|] ==> cont(%x. f(t(x)))"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	533	apply (best intro: cont2cont_app2 cont_const)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	534	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	535
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	536	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	537	(* A non-emptyness result for Cfun *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	538	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	539
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	540	lemma CfunI: "?x:Collect cont"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	541	apply (rule CollectI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	542	apply (rule cont_const)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	543	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	544
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	545	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	546	(* some properties of flat *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	547	(* ------------------------------------------------------------------------ *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	548
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	549	lemma flatdom2monofun: "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	550
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	551	apply (unfold monofun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	552	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	553	apply (drule ax_flat [THEN spec, THEN spec, THEN mp])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	554	apply auto
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	555	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	556
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	557	declare range_composition [simp del]
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	558	lemma chfindom_monofun2cont: "monofun f ==> cont(f::'a::chfin=>'b::pcpo)"
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	559	apply (rule monocontlub2cont)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	560	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	561	apply (rule contlubI)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	562	apply (intro strip)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	563	apply (frule chfin2finch)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	564	apply (rule antisym_less)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	565	apply (clarsimp simp add: finite_chain_def maxinch_is_thelub)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	566	apply (rule is_ub_thelub)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	567	apply (erule ch2ch_monofun)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	568	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	569	apply (drule monofun_finch2finch[COMP swap_prems_rl])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	570	apply assumption
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	571	apply (simp add: finite_chain_def)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	572	apply (erule conjE)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	573	apply (erule exE)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	574	apply (simp add: maxinch_is_thelub)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	575	apply (erule monofunE [THEN spec, THEN spec, THEN mp])
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	576	apply (erule is_ub_thelub)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	577	done
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	578
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	579	lemmas flatdom_strict2cont = flatdom2monofun [THEN chfindom_monofun2cont, standard]
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	580	(* f UU = UU ==> cont (f::'a=>'b::pcpo)" *)
2454493bd77b converted to new-style theory huffman parents: 14981 diff changeset	581
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	582	end

author	huffman
	Wed, 02 Mar 2005 23:28:17 +0100
changeset 15565	2454493bd77b
parent 14981	e73f8140af78
child 15576	efb95d0d01f7
permissions	-rw-r--r--