|
%%% ADT file generated from Outcome
Outcome_adt: THEORY
BEGIN
Outcome: TYPE
IMPORTING list[real]
istrue?, isfalse?, unknown?: [Outcome -> boolean]
counterexample: [(isfalse?) -> (cons?)]
IsTrue: (istrue?)
Counterexample: [(cons?) -> (isfalse?)]
Unknown: (unknown?)
Outcome_ord: [Outcome -> upto(2)]
Outcome_ord_defaxiom: AXIOM
Outcome_ord(IsTrue) = 0 AND
(FORALL (counterexample: (cons?)):
Outcome_ord(Counterexample(counterexample)) = 1)
AND Outcome_ord(Unknown) = 2;
ord(x: Outcome): [Outcome -> upto(2)] =
CASES x
OF IsTrue: 0, Counterexample(Counterexample1_var): 1, Unknown: 2
ENDCASES
Outcome_IsTrue_extensionality: AXIOM
FORALL (istrue?_var: (istrue?), istrue?_var2: (istrue?)):
istrue?_var = istrue?_var2;
Outcome_Counterexample_extensionality: AXIOM
FORALL (isfalse?_var: (isfalse?), isfalse?_var2: (isfalse?)):
counterexample(isfalse?_var) = counterexample(isfalse?_var2) IMPLIES
isfalse?_var = isfalse?_var2;
Outcome_Counterexample_eta: AXIOM
FORALL (isfalse?_var: (isfalse?)):
Counterexample(counterexample(isfalse?_var)) = isfalse?_var;
Outcome_Unknown_extensionality: AXIOM
FORALL (unknown?_var: (unknown?), unknown?_var2: (unknown?)):
unknown?_var = unknown?_var2;
Outcome_counterexample_Counterexample: AXIOM
FORALL (Counterexample1_var: (cons?)):
counterexample(Counterexample(Counterexample1_var)) =
Counterexample1_var;
Outcome_inclusive: AXIOM
FORALL (Outcome_var: Outcome):
istrue?(Outcome_var) OR
isfalse?(Outcome_var) OR unknown?(Outcome_var);
Outcome_induction: AXIOM
FORALL (p: [Outcome -> boolean]):
p(IsTrue) AND
(FORALL (Counterexample1_var: (cons?)):
p(Counterexample(Counterexample1_var)))
AND p(Unknown)
IMPLIES (FORALL (Outcome_var: Outcome): p(Outcome_var));
subterm(x: Outcome, y: Outcome): boolean = x = y;
<<: (strict_well_founded?[Outcome]) = LAMBDA (x, y: Outcome): FALSE;
Outcome_well_founded: AXIOM strict_well_founded?[Outcome](<<);
reduce_nat(istrue?_fun: nat, isfalse?_fun: [(cons?) -> nat],
unknown?_fun: nat):
[Outcome -> nat] =
LAMBDA (Outcome_adtvar: Outcome):
LET red: [Outcome -> nat] =
reduce_nat(istrue?_fun, isfalse?_fun, unknown?_fun)
IN
CASES Outcome_adtvar
OF IsTrue: istrue?_fun,
Counterexample(Counterexample1_var):
isfalse?_fun(Counterexample1_var),
Unknown: unknown?_fun
ENDCASES;
REDUCE_nat(istrue?_fun: [Outcome -> nat],
isfalse?_fun: [[(cons?), Outcome] -> nat],
unknown?_fun: [Outcome -> nat]):
[Outcome -> nat] =
LAMBDA (Outcome_adtvar: Outcome):
LET red: [Outcome -> nat] =
REDUCE_nat(istrue?_fun, isfalse?_fun, unknown?_fun)
IN
CASES Outcome_adtvar
OF IsTrue: istrue?_fun(Outcome_adtvar),
Counterexample(Counterexample1_var):
isfalse?_fun(Counterexample1_var, Outcome_adtvar),
Unknown: unknown?_fun(Outcome_adtvar)
ENDCASES;
reduce_ordinal(istrue?_fun: ordinal, isfalse?_fun: [(cons?) -> ordinal],
unknown?_fun: ordinal):
[Outcome -> ordinal] =
LAMBDA (Outcome_adtvar: Outcome):
LET red: [Outcome -> ordinal] =
reduce_ordinal(istrue?_fun, isfalse?_fun, unknown?_fun)
IN
CASES Outcome_adtvar
OF IsTrue: istrue?_fun,
Counterexample(Counterexample1_var):
isfalse?_fun(Counterexample1_var),
Unknown: unknown?_fun
ENDCASES;
REDUCE_ordinal(istrue?_fun: [Outcome -> ordinal],
isfalse?_fun: [[(cons?), Outcome] -> ordinal],
unknown?_fun: [Outcome -> ordinal]):
[Outcome -> ordinal] =
LAMBDA (Outcome_adtvar: Outcome):
LET red: [Outcome -> ordinal] =
REDUCE_ordinal(istrue?_fun, isfalse?_fun, unknown?_fun)
IN
CASES Outcome_adtvar
OF IsTrue: istrue?_fun(Outcome_adtvar),
Counterexample(Counterexample1_var):
isfalse?_fun(Counterexample1_var, Outcome_adtvar),
Unknown: unknown?_fun(Outcome_adtvar)
ENDCASES;
END Outcome_adt
Outcome_adt_reduce[range: TYPE]: THEORY
BEGIN
IMPORTING Outcome_adt
IMPORTING list[real]
reduce(istrue?_fun: range, isfalse?_fun: [(cons?) -> range],
unknown?_fun: range):
[Outcome -> range] =
LAMBDA (Outcome_adtvar: Outcome):
LET red: [Outcome -> range] =
reduce(istrue?_fun, isfalse?_fun, unknown?_fun)
IN
CASES Outcome_adtvar
OF IsTrue: istrue?_fun,
Counterexample(Counterexample1_var):
isfalse?_fun(Counterexample1_var),
Unknown: unknown?_fun
ENDCASES;
REDUCE(istrue?_fun: [Outcome -> range],
isfalse?_fun: [[(cons?), Outcome] -> range],
unknown?_fun: [Outcome -> range]):
[Outcome -> range] =
LAMBDA (Outcome_adtvar: Outcome):
LET red: [Outcome -> range] =
REDUCE(istrue?_fun, isfalse?_fun, unknown?_fun)
IN
CASES Outcome_adtvar
OF IsTrue: istrue?_fun(Outcome_adtvar),
Counterexample(Counterexample1_var):
isfalse?_fun(Counterexample1_var, Outcome_adtvar),
Unknown: unknown?_fun(Outcome_adtvar)
ENDCASES;
END Outcome_adt_reduce
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
