Changes

Summary

simplify applicative declaration in Stern_Brocot
update change history for Applicative_Lifting
Applicative_Lifting: derive combinators, lift relations, support locales - The "applicative" command derives combinator reductions automatically, e.g. for I if C and K are provided. Therefore, the command no longer emits redundant proof obligations in such cases. This includes the derivation of C from BKW and interchange, as well as the derivation of the interchange law from C and I. Also added the S combinator, such that SK can be used instead of BCKW. - Added support for arbitrary lifted relations via relators. An optional "set" operator can be provided, which may produce weaker subgoals (with additional premises) after application of a lifting proof method. - Improved compatibility with locale interpretation; see Applicative_Sum for a use case. - Small user-facing changes: more intuitive assignment of type variables, modified order of subgoals in the proof for "applicative"; changed some theorem names.

Changeset 6762:27c339fa0e78 by joshua schneider _joshuas@student.ethz.ch_: simplify applicative declaration in Stern_Brocot
The file was modified	`thys/Stern_Brocot/Cotree.thy` (diff)
Changeset 6761:2aa1deb75faa by joshua schneider _joshuas@student.ethz.ch_: update change history for Applicative_Lifting
The file was modified	`metadata/metadata` (diff)
Changeset 6760:ec336f354f37 by joshua schneider _joshuas@student.ethz.ch_: Applicative_Lifting: derive combinators, lift relations, support locales<br><br>- The "applicative" command derives combinator reductions automatically, e.g.<br>  for I if C and K are provided. Therefore, the command no longer emits<br>  redundant proof obligations in such cases. This includes the derivation of<br>  C from BKW and interchange, as well as the derivation of the interchange law<br>  from C and I. Also added the S combinator, such that SK can be used instead<br>  of BCKW.<br><br>- Added support for arbitrary lifted relations via relators. An optional "set"<br>  operator can be provided, which may produce weaker subgoals (with additional<br>  premises) after application of a lifting proof method.<br><br>- Improved compatibility with locale interpretation; see Applicative_Sum for<br>  a use case.<br><br>- Small user-facing changes: more intuitive assignment of type variables,<br>  modified order of subgoals in the proof for "applicative"; changed some<br>  theorem names.
The file was modified	`thys/Applicative_Lifting/Abstract_AF.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_DNEList.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Environment.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_List.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Monoid.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Option.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_PMF.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Set.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Star.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Stream.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Sum.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Test.thy` (diff)
The file was modified	`thys/Applicative_Lifting/applicative.ML` (diff)