ballarin@27063

1 
theory Examples1

ballarin@27063

2 
imports Examples

ballarin@27063

3 
begin

wenzelm@57607

4 

wenzelm@61419

5 
section \<open>Use of Locales in Theories and Proofs

wenzelm@61419

6 
\label{sec:interpretation}\<close>

ballarin@27063

7 

wenzelm@61419

8 
text \<open>

ballarin@32983

9 
Locales can be interpreted in the contexts of theories and

ballarin@27063

10 
structured proofs. These interpretations are dynamic, too.

ballarin@32981

11 
Conclusions of locales will be propagated to the current theory or

ballarin@32981

12 
the current proof context.%

ballarin@32981

13 
\footnote{Strictly speaking, only interpretation in theories is

ballarin@32981

14 
dynamic since it is not possible to change locales or the locale

ballarin@32981

15 
hierarchy from within a proof.}

ballarin@32981

16 
The focus of this section is on

ballarin@32981

17 
interpretation in theories, but we will also encounter

ballarin@32981

18 
interpretations in proofs, in

ballarin@32981

19 
Section~\ref{sec:localinterpretation}.

ballarin@30580

20 

ballarin@32982

21 
As an example, consider the type of integers @{typ int}. The

ballarin@32983

22 
relation @{term "op \<le>"} is a total order over @{typ int}. We start

ballarin@32983

23 
with the interpretation that @{term "op \<le>"} is a partial order. The

ballarin@32983

24 
facilities of the interpretation command are explored gradually in

ballarin@32983

25 
three versions.

wenzelm@61419

26 
\<close>

ballarin@27063

27 

ballarin@27063

28 

wenzelm@61419

29 
subsection \<open>First Version: Replacement of Parameters Only

wenzelm@61419

30 
\label{sec:pofirst}\<close>

ballarin@27063

31 

wenzelm@61419

32 
text \<open>

ballarin@32981

33 
The command \isakeyword{interpretation} is for the interpretation of

ballarin@32981

34 
locale in theories. In the following example, the parameter of locale

ballarin@32982

35 
@{text partial_order} is replaced by @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow>

ballarin@32981

36 
bool"} and the locale instance is interpreted in the current

wenzelm@61419

37 
theory.\<close>

ballarin@27063

38 

ballarin@32982

39 
interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"

wenzelm@61419

40 
txt \<open>\normalsize

ballarin@32981

41 
The argument of the command is a simple \emph{locale expression}

ballarin@32981

42 
consisting of the name of the interpreted locale, which is

ballarin@32982

43 
preceded by the qualifier @{text "int:"} and succeeded by a

ballarin@32981

44 
whitespaceseparated list of terms, which provide a full

ballarin@32981

45 
instantiation of the locale parameters. The parameters are referred

ballarin@32981

46 
to by order of declaration, which is also the order in which

ballarin@32983

47 
\isakeyword{print\_locale} outputs them. The locale has only a

ballarin@32983

48 
single parameter, hence the list of instantiation terms is a

ballarin@32983

49 
singleton.

ballarin@32981

50 

ballarin@32981

51 
The command creates the goal

ballarin@30580

52 
@{subgoals [display]} which can be shown easily:

wenzelm@61419

53 
\<close>

ballarin@27063

54 
by unfold_locales auto

ballarin@27063

55 

wenzelm@61419

56 
text \<open>The effect of the command is that instances of all

ballarin@32981

57 
conclusions of the locale are available in the theory, where names

ballarin@32981

58 
are prefixed by the qualifier. For example, transitivity for @{typ

ballarin@32982

59 
int} is named @{thm [source] int.trans} and is the following

ballarin@32981

60 
theorem:

ballarin@32982

61 
@{thm [display, indent=2] int.trans}

ballarin@32981

62 
It is not possible to reference this theorem simply as @{text

ballarin@32983

63 
trans}. This prevents unwanted hiding of existing theorems of the

wenzelm@61419

64 
theory by an interpretation.\<close>

ballarin@27063

65 

ballarin@27063

66 

wenzelm@61419

67 
subsection \<open>Second Version: Replacement of Definitions\<close>

ballarin@27063

68 

wenzelm@61419

69 
text \<open>Not only does the above interpretation qualify theorem names.

ballarin@32982

70 
The prefix @{text int} is applied to all names introduced in locale

ballarin@32981

71 
conclusions including names introduced in definitions. The

ballarin@32983

72 
qualified name @{text int.less} is short for

ballarin@61701

73 
the interpretation of the definition, which is @{text "partial_order.less op \<le>"}.

ballarin@32981

74 
Qualified name and expanded form may be used almost

ballarin@32981

75 
interchangeably.%

ballarin@61701

76 
\footnote{Since @{term "op \<le>"} is polymorphic, for @{text "partial_order.less op \<le>"} a

ballarin@32982

77 
more general type will be inferred than for @{text int.less} which

ballarin@32982

78 
is over type @{typ int}.}

ballarin@61701

79 
The former is preferred on output, as for example in the theorem

ballarin@32982

80 
@{thm [source] int.less_le_trans}: @{thm [display, indent=2]

ballarin@32982

81 
int.less_le_trans}

ballarin@32981

82 
Both notations for the strict order are not satisfactory. The

ballarin@32982

83 
constant @{term "op <"} is the strict order for @{typ int}.

ballarin@32981

84 
In order to allow for the desired replacement, interpretation

ballarin@32981

85 
accepts \emph{equations} in addition to the parameter instantiation.

ballarin@32981

86 
These follow the locale expression and are indicated with the

ballarin@61566

87 
keyword \isakeyword{rewrites}. This is the revised interpretation:

wenzelm@61419

88 
\<close>

ballarin@27063

89 
end
