Eine aufbereitete Darstellung der Quelle
Stufen
Anforderungen
|
Konzepte
|
Entwurf
|
Entwicklung
|
Qualitätssicherung
|
Lebenszyklus
|
Steuerung
Ziele
Untersuchung
mit Columbo
Integrität von
Datenbanken
Interaktion und
Portierbarkeit
Ergonomie der
Schnittstellen
Angebot
Produkte
Projekt
Beratung
Mittel
Analytik
Modellierung
Sprachen
Algebra
Logik
Hardware
Denken
Kreativität
Zusammenhänge
Gesellschaft
Wirtschaft
Branche
Firma
Benutzer
products
/
Sources
/
formale Sprachen
/
C
/
Linux
/
include
/
sound
/ (
Linux Kernel
Version 6.17.9
©
) Datei vom 24.10.2025 mit Größe 476 B
Bilddatei
TLList.thy
products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Coinductive/TLList.thy
(* Title: Terminated coinductive list Author: Andreas Lochbihler Maintainer: Andreas Lochbihler *) section \
Terminated coinductive lists and their operations\
theory TLList imports Coinductive_List begin text \
Terminated coinductive lists \
('a, 'b) tllist\
are the codatatype defined by the construtors \
TNil\
of type \
'b \
('a, 'b) tllist\
and \
TCons\
of type \
'a \
('a, 'b) tllist \
('a, 'b) tllist\
. \
subsection \
Auxiliary lemmas\
lemma split_fst: "R (fst p) = (\
x y. p = (x, y) \
R x)" by(cases p) simp lemma split_fst_asm: "R (fst p) \
(\
(\
x y. p = (x, y) \
\
R x))" by(cases p) simp subsection \
Type definition\
consts terminal0 :: "'a" codatatype (tset: 'a, 'b) tllist = TNil (terminal : 'b) | TCons (thd : 'a) (ttl : "('a, 'b) tllist") for map: tmap rel: tllist_all2 where "thd (TNil _) = undefined" | "ttl (TNil b) = TNil b" | "terminal (TCons _ xs) = terminal0 xs" overloading terminal0 == "terminal0::('a, 'b) tllist \
'b" begin partial_function (tailrec) terminal0 where "terminal0 xs = (if is_TNil xs then case_tllist id undefined xs else terminal0 (ttl xs))" end lemma terminal0_terminal [simp]: "terminal0 = terminal" apply(rule ext) apply(subst terminal0.simps) apply(case_tac x) apply(simp_all add: terminal_def) done lemmas terminal_TNil [code, nitpick_simp] = tllist.sel(1) lemma terminal_TCons [simp, code, nitpick_simp]: "terminal (TCons x xs) = terminal xs" by simp declare tllist.sel(2) [simp del] primcorec unfold_tllist :: "('a \
bool) \
('a \
'b) \
('a \
'c) \
('a \
'a) \
'a \
('c, 'b) tllist" where "p a \
unfold_tllist p g1 g21 g22 a = TNil (g1 a)" | "_ \
unfold_tllist p g1 g21 g22 a = TCons (g21 a) (unfold_tllist p g1 g21 g22 (g22 a))" declare unfold_tllist.ctr(1) [simp] tllist.corec(1) [simp] subsection \
Code generator setup\
text \
Test quickcheck setup\
lemma "xs = TNil x" quickcheck[random, expect=counterexample] quickcheck[exhaustive, expect=counterexample] oops lemma "TCons x xs = TCons x xs" quickcheck[narrowing, expect=no_counterexample] oops text \
More lemmas about generated constants\
lemma ttl_unfold_tllist: "ttl (unfold_tllist IS_TNIL TNIL THD TTL a) = (if IS_TNIL a then TNil (TNIL a) else unfold_tllist IS_TNIL TNIL THD TTL (TTL a))" by(simp) lemma is_TNil_ttl [simp]: "is_TNil xs \
is_TNil (ttl xs)" by(cases xs) simp_all lemma terminal_ttl [simp]: "terminal (ttl xs) = terminal xs" by(cases xs) simp_all lemma unfold_tllist_eq_TNil [simp]: "unfold_tllist IS_TNIL TNIL THD TTL a = TNil b \
IS_TNIL a \
b = TNIL a" by(auto simp add: unfold_tllist.code) lemma TNil_eq_unfold_tllist [simp]: "TNil b = unfold_tllist IS_TNIL TNIL THD TTL a \
IS_TNIL a \
b = TNIL a" by(auto simp add: unfold_tllist.code) lemma tmap_is_TNil: "is_TNil xs \
tmap f g xs = TNil (g (terminal xs))" by(clarsimp simp add: is_TNil_def) declare tllist.map_sel(2)[simp] lemma ttl_tmap [simp]: "ttl (tmap f g xs) = tmap f g (ttl xs)" by(cases xs) simp_all lemma tmap_eq_TNil_conv: "tmap f g xs = TNil y \
(\
y'. xs = TNil y' \
g y' = y)" by(cases xs) simp_all lemma TNil_eq_tmap_conv: "TNil y = tmap f g xs \
(\
y'. xs = TNil y' \
g y' = y)" by(cases xs) auto declare tllist.set_sel(1)[simp] lemma tset_ttl: "tset (ttl xs) \
tset xs" by(cases xs) auto lemma in_tset_ttlD: "x \
tset (ttl xs) \
x \
tset xs" using tset_ttl[of xs] by auto theorem tllist_set_induct[consumes 1, case_names find step]: assumes "x \
tset xs" and "\
xs. \
is_TNil xs \
P (thd xs) xs" and "\
xs y. \
\
is_TNil xs; y \
tset (ttl xs); P y (ttl xs)\
\
P y xs" shows "P x xs" using assms by(induct)(fastforce simp del: tllist.disc(2) iff: tllist.disc(2), auto) theorem set2_tllist_induct[consumes 1, case_names find step]: assumes "x \
set2_tllist xs" and "\
xs. is_TNil xs \
P (terminal xs) xs" and "\
xs y. \
\
is_TNil xs; y \
set2_tllist (ttl xs); P y (ttl xs)\
\
P y xs" shows "P x xs" using assms by(induct)(fastforce simp del: tllist.disc(1) iff: tllist.disc(1), auto) subsection \
Connection with @{typ "'a llist"}\
context fixes b :: 'b begin primcorec tllist_of_llist :: "'a llist \
('a, 'b) tllist" where "tllist_of_llist xs = (case xs of LNil \
TNil b | LCons x xs' \
TCons x (tllist_of_llist xs'))" end primcorec llist_of_tllist :: "('a, 'b) tllist \
'a llist" where "llist_of_tllist xs = (case xs of TNil _ \
LNil | TCons x xs' \
LCons x (llist_of_tllist xs'))" simps_of_case tllist_of_llist_simps [simp, code, nitpick_simp]: tllist_of_llist.code lemmas tllist_of_llist_LNil = tllist_of_llist_simps(1) and tllist_of_llist_LCons = tllist_of_llist_simps(2) lemma terminal_tllist_of_llist_lnull [simp]: "lnull xs \
terminal (tllist_of_llist b xs) = b" unfolding lnull_def by simp declare tllist_of_llist.sel(1)[simp del] lemma lhd_LNil: "lhd LNil = undefined" by(simp add: lhd_def) lemma thd_TNil: "thd (TNil b) = undefined" by(simp add: thd_def) lemma thd_tllist_of_llist [simp]: "thd (tllist_of_llist b xs) = lhd xs" by(cases xs)(simp_all add: thd_TNil lhd_LNil) lemma ttl_tllist_of_llist [simp]: "ttl (tllist_of_llist b xs) = tllist_of_llist b (ltl xs)" by(cases xs) simp_all lemma llist_of_tllist_eq_LNil: "llist_of_tllist xs = LNil \
is_TNil xs" using llist_of_tllist.disc_iff(1) unfolding lnull_def . simps_of_case llist_of_tllist_simps [simp, code, nitpick_simp]: llist_of_tllist.code lemmas llist_of_tllist_TNil = llist_of_tllist_simps(1) and llist_of_tllist_TCons = llist_of_tllist_simps(2) declare llist_of_tllist.sel [simp del] lemma lhd_llist_of_tllist [simp]: "\
is_TNil xs \
lhd (llist_of_tllist xs) = thd xs" by(cases xs) simp_all lemma ltl_llist_of_tllist [simp]: "ltl (llist_of_tllist xs) = llist_of_tllist (ttl xs)" by(cases xs) simp_all lemma tllist_of_llist_cong [cong]: assumes "xs = xs'" "lfinite xs' \
b = b'" shows "tllist_of_llist b xs = tllist_of_llist b' xs'" proof(unfold \
xs = xs'\
) from assms have "lfinite xs' \
b = b'" by simp thus "tllist_of_llist b xs' = tllist_of_llist b' xs'" by(coinduction arbitrary: xs') auto qed lemma llist_of_tllist_inverse [simp]: "tllist_of_llist (terminal b) (llist_of_tllist b) = b" by(coinduction arbitrary: b) simp_all lemma tllist_of_llist_eq [simp]: "tllist_of_llist b' xs = TNil b \
b = b' \
xs = LNil" by(cases xs) auto lemma TNil_eq_tllist_of_llist [simp]: "TNil b = tllist_of_llist b' xs \
b = b' \
xs = LNil" by(cases xs) auto lemma tllist_of_llist_inject [simp]: "tllist_of_llist b xs = tllist_of_llist c ys \
xs = ys \
(lfinite ys \
b = c)" (is "?lhs \
?rhs") proof(intro iffI conjI impI) assume ?rhs thus ?lhs by(auto intro: tllist_of_llist_cong) next assume ?lhs thus "xs = ys" by(coinduction arbitrary: xs ys)(auto simp add: lnull_def neq_LNil_conv) assume "lfinite ys" thus "b = c" using \
?lhs\
unfolding \
xs = ys\
by(induct) simp_all qed lemma tllist_of_llist_inverse [simp]: "llist_of_tllist (tllist_of_llist b xs) = xs" by(coinduction arbitrary: xs) auto definition cr_tllist :: "('a llist \
'b) \
('a, 'b) tllist \
bool" where "cr_tllist \
(\
(xs, b) ys. tllist_of_llist b xs = ys)" lemma Quotient_tllist: "Quotient (\
(xs, a) (ys, b). xs = ys \
(lfinite ys \
a = b)) (\
(xs, a). tllist_of_llist a xs) (\
ys. (llist_of_tllist ys, terminal ys)) cr_tllist" unfolding Quotient_alt_def cr_tllist_def by(auto intro: tllist_of_llist_cong) lemma reflp_tllist: "reflp (\
(xs, a) (ys, b). xs = ys \
(lfinite ys \
a = b))" by(simp add: reflp_def) setup_lifting Quotient_tllist reflp_tllist context includes lifting_syntax begin lemma TNil_transfer [transfer_rule]: "(B ===> pcr_tllist A B) (Pair LNil) TNil" by(force simp add: pcr_tllist_def cr_tllist_def) lemma TCons_transfer [transfer_rule]: "(A ===> pcr_tllist A B ===> pcr_tllist A B) (apfst \
LCons) TCons" by(force simp add: pcr_tllist_def llist_all2_LCons1 cr_tllist_def) lemma tmap_tllist_of_llist: "tmap f g (tllist_of_llist b xs) = tllist_of_llist (g b) (lmap f xs)" by(coinduction arbitrary: xs)(auto simp add: tmap_is_TNil) lemma tmap_transfer [transfer_rule]: "((=) ===> (=) ===> pcr_tllist (=) (=) ===> pcr_tllist (=) (=)) (map_prod \
lmap) tmap" by(force simp add: cr_tllist_def tllist.pcr_cr_eq tmap_tllist_of_llist) lemma lset_llist_of_tllist [simp]: "lset (llist_of_tllist xs) = tset xs" (is "?lhs = ?rhs") proof(intro set_eqI iffI) fix x assume "x \
?lhs" thus "x \
?rhs" by(induct "llist_of_tllist xs" arbitrary: xs rule: llist_set_induct)(auto simp: tllist.set_sel(2)) next fix x assume "x \
?rhs" thus "x \
?lhs" proof(induct rule: tllist_set_induct) case (find xs) thus ?case by(cases xs) auto next case step thus ?case by(auto simp add: ltl_llist_of_tllist[symmetric] simp del: ltl_llist_of_tllist dest: in_lset_ltlD) qed qed lemma tset_tllist_of_llist [simp]: "tset (tllist_of_llist b xs) = lset xs" by(simp add: lset_llist_of_tllist[symmetric] del: lset_llist_of_tllist) lemma tset_transfer [transfer_rule]: "(pcr_tllist (=) (=) ===> (=)) (lset \
fst) tset" by(auto simp add: cr_tllist_def tllist.pcr_cr_eq) lemma is_TNil_transfer [transfer_rule]: "(pcr_tllist (=) (=) ===> (=)) (\
(xs, b). lnull xs) is_TNil" by(auto simp add: tllist.pcr_cr_eq cr_tllist_def) lemma thd_transfer [transfer_rule]: "(pcr_tllist (=) (=) ===> (=)) (lhd \
fst) thd" by(auto simp add: cr_tllist_def tllist.pcr_cr_eq) lemma ttl_transfer [transfer_rule]: "(pcr_tllist A B ===> pcr_tllist A B) (apfst ltl) ttl" by(force simp add: pcr_tllist_def cr_tllist_def intro: llist_all2_ltlI) lemma llist_of_tllist_transfer [transfer_rule]: "(pcr_tllist (=) B ===> (=)) fst llist_of_tllist" by(auto simp add: pcr_tllist_def cr_tllist_def llist.rel_eq) lemma tllist_of_llist_transfer [transfer_rule]: "((=) ===> (=) ===> pcr_tllist (=) (=)) (\
b xs. (xs, b)) tllist_of_llist" by(auto simp add: tllist.pcr_cr_eq cr_tllist_def) lemma terminal_tllist_of_llist_lfinite [simp]: "lfinite xs \
terminal (tllist_of_llist b xs) = b" by(induct rule: lfinite.induct) simp_all lemma set2_tllist_tllist_of_llist [simp]: "set2_tllist (tllist_of_llist b xs) = (if lfinite xs then {b} else {})" proof(cases "lfinite xs") case True thus ?thesis by(induct) auto next case False { fix x assume "x \
set2_tllist (tllist_of_llist b xs)" hence False using False by(induct "tllist_of_llist b xs" arbitrary: xs rule: set2_tllist_induct) fastforce+ } thus ?thesis using False by auto qed lemma set2_tllist_transfer [transfer_rule]: "(pcr_tllist A B ===> rel_set B) (\
(xs, b). if lfinite xs then {b} else {}) set2_tllist" by(auto 4 4 simp add: pcr_tllist_def cr_tllist_def dest: llist_all2_lfiniteD intro: rel_setI) lemma tllist_all2_transfer [transfer_rule]: "((=) ===> (=) ===> pcr_tllist (=) (=) ===> pcr_tllist (=) (=) ===> (=)) (\
P Q (xs, b) (ys, b'). llist_all2 P xs ys \
(lfinite xs \
Q b b')) tllist_all2" unfolding tllist.pcr_cr_eq apply(rule rel_funI)+ apply(clarsimp simp add: cr_tllist_def llist_all2_def tllist_all2_def) apply(safe elim!: GrpE) apply simp_all apply(rule_tac b="tllist_of_llist (b, ba) bb" in relcomppI) apply(auto intro!: GrpI simp add: tmap_tllist_of_llist)[2] apply(rule_tac b="tllist_of_llist (b, ba) bb" in relcomppI) apply(auto simp add: tmap_tllist_of_llist intro!: GrpI split: if_split_asm)[2] apply(rule_tac b="llist_of_tllist bb" in relcomppI) apply(auto intro!: GrpI) apply(transfer, auto intro: GrpI split: if_split_asm)+ done subsection \
Library function definitions\
text \
We lift the constants from @{typ "'a llist"} to @{typ "('a, 'b) tllist"} using the lifting package. This way, many results are transferred easily. \
lift_definition tappend :: "('a, 'b) tllist \
('b \
('a, 'c) tllist) \
('a, 'c) tllist" is "\
(xs, b) f. apfst (lappend xs) (f b)" by(auto simp add: split_def lappend_inf) lift_definition lappendt :: "'a llist \
('a, 'b) tllist \
('a, 'b) tllist" is "apfst \
lappend" by(simp add: split_def) lift_definition tfilter :: "'b \
('a \
bool) \
('a, 'b) tllist \
('a, 'b) tllist" is "\
b P (xs, b'). (lfilter P xs, if lfinite xs then b' else b)" by(simp add: split_beta) lift_definition tconcat :: "'b \
('a llist, 'b) tllist \
('a, 'b) tllist" is "\
b (xss, b'). (lconcat xss, if lfinite xss then b' else b)" by(simp add: split_beta) lift_definition tnth :: "('a, 'b) tllist \
nat \
'a" is "lnth \
fst" by(auto) lift_definition tlength :: "('a, 'b) tllist \
enat" is "llength \
fst" by auto lift_definition tdropn :: "nat \
('a, 'b) tllist \
('a, 'b) tllist" is "apfst \
ldropn" by auto abbreviation tfinite :: "('a, 'b) tllist \
bool" where "tfinite xs \
lfinite (llist_of_tllist xs)" subsection \
@{term "tfinite"}\
lemma tfinite_induct [consumes 1, case_names TNil TCons]: assumes "tfinite xs" and "\
y. P (TNil y)" and "\
x xs. \
tfinite xs; P xs\
\
P (TCons x xs)" shows "P xs" using assms by transfer (clarsimp, erule lfinite.induct) lemma is_TNil_tfinite [simp]: "is_TNil xs \
tfinite xs" by transfer clarsimp subsection \
The terminal element @{term "terminal"}\
lemma terminal_tinfinite: assumes "\
tfinite xs" shows "terminal xs = undefined" unfolding terminal0_terminal[symmetric] using assms apply(rule contrapos_np) by(induct xs rule: terminal0.raw_induct[rotated 1, OF refl, consumes 1])(auto split: tllist.split_asm) lemma terminal_tllist_of_llist: "terminal (tllist_of_llist y xs) = (if lfinite xs then y else undefined)" by(simp add: terminal_tinfinite) lemma terminal_transfer [transfer_rule]: "(pcr_tllist A (=) ===> (=)) (\
(xs, b). if lfinite xs then b else undefined) terminal" by(force simp add: cr_tllist_def pcr_tllist_def terminal_tllist_of_llist dest: llist_all2_lfiniteD) lemma terminal_tmap [simp]: "tfinite xs \
terminal (tmap f g xs) = g (terminal xs)" by(induct rule: tfinite_induct) simp_all subsection \
@{term "tmap"}\
lemma tmap_eq_TCons_conv: "tmap f g xs = TCons y ys \
(\
z zs. xs = TCons z zs \
f z = y \
tmap f g zs = ys)" by(cases xs) simp_all lemma TCons_eq_tmap_conv: "TCons y ys = tmap f g xs \
(\
z zs. xs = TCons z zs \
f z = y \
tmap f g zs = ys)" by(cases xs) auto subsection \
Appending two terminated lazy lists @{term "tappend" }\
lemma tappend_TNil [simp, code, nitpick_simp]: "tappend (TNil b) f = f b" by transfer auto lemma tappend_TCons [simp, code, nitpick_simp]: "tappend (TCons a tr) f = TCons a (tappend tr f)" by transfer(auto simp add: apfst_def map_prod_def split: prod.splits) lemma tappend_TNil2 [simp]: "tappend xs TNil = xs" by transfer auto lemma tappend_assoc: "tappend (tappend xs f) g = tappend xs (\
b. tappend (f b) g)" by transfer(auto simp add: split_beta lappend_assoc) lemma terminal_tappend: "terminal (tappend xs f) = (if tfinite xs then terminal (f (terminal xs)) else terminal xs)" by transfer(auto simp add: split_beta) lemma tfinite_tappend: "tfinite (tappend xs f) \
tfinite xs \
tfinite (f (terminal xs))" by transfer auto lift_definition tcast :: "('a, 'b) tllist \
('a, 'c) tllist" is "\
(xs, a). (xs, undefined)" by clarsimp lemma tappend_inf: "\
tfinite xs \
tappend xs f = tcast xs" by(transfer)(auto simp add: apfst_def map_prod_def split_beta lappend_inf) text \
@{term tappend} is the monadic bind on @{typ "('a, 'b) tllist"}\
lemmas tllist_monad = tappend_TNil tappend_TNil2 tappend_assoc subsection \
Appending a terminated lazy list to a lazy list @{term "lappendt"}\
lemma lappendt_LNil [simp, code, nitpick_simp]: "lappendt LNil tr = tr" by transfer auto lemma lappendt_LCons [simp, code, nitpick_simp]: "lappendt (LCons x xs) tr = TCons x (lappendt xs tr)" by transfer auto lemma terminal_lappendt_lfinite [simp]: "lfinite xs \
terminal (lappendt xs ys) = terminal ys" by transfer auto lemma tllist_of_llist_eq_lappendt_conv: "tllist_of_llist a xs = lappendt ys zs \
(\
xs' a'. xs = lappend ys xs' \
zs = tllist_of_llist a' xs' \
(lfinite ys \
a = a'))" by transfer auto lemma tset_lappendt_lfinite [simp]: "lfinite xs \
tset (lappendt xs ys) = lset xs \
tset ys" by transfer auto subsection \
Filtering terminated lazy lists @{term tfilter}\
lemma tfilter_TNil [simp]: "tfilter b' P (TNil b) = TNil b" by transfer auto lemma tfilter_TCons [simp]: "tfilter b P (TCons a tr) = (if P a then TCons a (tfilter b P tr) else tfilter b P tr)" by transfer auto lemma is_TNil_tfilter[simp]: "is_TNil (tfilter y P xs) \
(\
x \
tset xs. \
P x)" by transfer auto lemma tfilter_empty_conv: "tfilter y P xs = TNil y' \
(\
x \
tset xs. \
P x) \
(if tfinite xs then terminal xs = y' else y = y')" by transfer(clarsimp simp add: lfilter_eq_LNil) lemma tfilter_eq_TConsD: "tfilter a P ys = TCons x xs \
\
us vs. ys = lappendt us (TCons x vs) \
lfinite us \
(\
u\
lset us. \
P u) \
P x \
xs = tfilter a P vs" by transfer(fastforce dest: lfilter_eq_LConsD[OF sym]) text \
Use a version of @{term "tfilter"} for code generation that does not evaluate the first argument\
definition tfilter' :: "(unit \
'b) \
('a \
bool) \
('a, 'b) tllist \
('a, 'b) tllist" where [simp]: "tfilter' b = tfilter (b ())" lemma tfilter_code [code, code_unfold]: "tfilter = (\
b. tfilter' (\
