|
73846
|
1 |
theory Interpretation_in_nested_targets
|
|
|
2 |
imports Main
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
locale injection =
|
|
|
6 |
fixes f :: \<open>'a \<Rightarrow> 'b\<close>
|
|
|
7 |
assumes eqI: \<open>f x = f y \<Longrightarrow> x = y\<close>
|
|
|
8 |
begin
|
|
|
9 |
|
|
|
10 |
lemma eq_iff:
|
|
|
11 |
\<open>x = y \<longleftrightarrow> f x = f y\<close>
|
|
|
12 |
by (auto intro: eqI)
|
|
|
13 |
|
|
|
14 |
lemma inv_apply:
|
|
|
15 |
\<open>inv f (f x) = x\<close>
|
|
|
16 |
by (rule inv_f_f) (simp add: eqI injI)
|
|
|
17 |
|
|
|
18 |
end
|
|
|
19 |
|
|
|
20 |
context
|
|
|
21 |
fixes f :: \<open>'a::linorder \<Rightarrow> 'b::linorder\<close>
|
|
|
22 |
assumes \<open>strict_mono f\<close>
|
|
|
23 |
begin
|
|
|
24 |
|
|
|
25 |
global_interpretation strict_mono: injection f
|
|
|
26 |
by standard (simp add: \<open>strict_mono f\<close> strict_mono_eq)
|
|
|
27 |
|
|
|
28 |
thm strict_mono.eq_iff
|
|
|
29 |
thm strict_mono.inv_apply
|
|
|
30 |
|
|
|
31 |
end
|
|
|
32 |
|
|
|
33 |
thm strict_mono.eq_iff
|
|
|
34 |
thm strict_mono.inv_apply
|
|
|
35 |
|
|
|
36 |
end
|