| author | Cezary Kaliszyk <cezarykaliszyk@gmail.com> |
| Fri, 30 Mar 2012 07:15:24 +0200 | |
| changeset 3143 | 1da802bd2ab1 |
| parent 3132 | 87eca760dcba |
| child 3235 | 5ebd327ffb96 |
| 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" |
|
3132
87eca760dcba
updated tutorial to latest version and added it to the tests
Christian Urban <urbanc@in.tum.de>
parents:
2686
diff
changeset
|
10 |
| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
|
|
2679
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 |