| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Mon, 20 Jun 2011 08:50:13 +0900 | |
| changeset 2871 | b58073719b06 |
| parent 2686 | 52e1e98edb34 |
| child 3132 | 87eca760dcba |
| permissions | -rw-r--r-- |
|
2679
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Minimal |
|
2681
0e4c5fa26fa1
theory name as it should be
Christian Urban <urbanc@in.tum.de>
parents:
2679
diff
changeset
|
2 |
imports "Nominal2" |
|
2679
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
atom_decl name |
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
nominal_datatype lam = |
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
Var "name" |
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
| App "lam" "lam" |
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
|
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
|
|
2686
52e1e98edb34
added a very rough version of the tutorial; all seems to work
Christian Urban <urbanc@in.tum.de>
parents:
2681
diff
changeset
|
12 |
|
|
52e1e98edb34
added a very rough version of the tutorial; all seems to work
Christian Urban <urbanc@in.tum.de>
parents:
2681
diff
changeset
|
13 |
|
|
2679
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
lemma alpha_test: |
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
shows "Lam [x]. (Var x) = Lam [y]. (Var y)" |
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base) |
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
|
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
end |