| author | wenzelm |
| Thu, 30 Mar 2023 16:02:25 +0200 | |
| changeset 77763 | 2abc452d0ee9 |
| parent 74287 | f79dfc7656ae |
| permissions | -rw-r--r-- |
|
74287
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ex/Def_Examples.thy |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
3 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
4 |
Some examples for primitive definitions. |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
5 |
*) |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
6 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
7 |
theory Def_Examples |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
8 |
imports Def |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
9 |
begin |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
10 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
11 |
section \<open>Global definitions\<close> |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
12 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
13 |
def "I x \<equiv> x" |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
14 |
def "K x y \<equiv> x" |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
15 |
def "S x y z \<equiv> (x z) (y z)" |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
16 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
17 |
lemma "I (I x) \<equiv> x" |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
18 |
by simp |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
19 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
20 |
lemma "K a x \<equiv> K a y" |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
21 |
by simp |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
22 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
23 |
lemma "S K K \<equiv> I" |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
24 |
by simp |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
25 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
26 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
27 |
section \<open>Locale definitions\<close> |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
28 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
29 |
locale const = |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
30 |
fixes a :: 'a |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
31 |
begin |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
32 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
33 |
def "fun b \<equiv> a" |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
34 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
35 |
lemma "fun x \<equiv> fun y" |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
36 |
by simp |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
37 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
38 |
end |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
39 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
40 |
lemma "const.fun a x \<equiv> const.fun a y" |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
41 |
by simp |
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
42 |
|
|
f79dfc7656ae
miscellaneous examples and experiments for Isabelle/Pure;
wenzelm
parents:
diff
changeset
|
43 |
end |