| author | Christian Urban <urbanc@in.tum.de> |
| Wed, 19 Jan 2011 17:11:10 +0100 | |
| changeset 2679 | e003e5e36bae |
| child 2681 | 0e4c5fa26fa1 |
| permissions | -rw-r--r-- |
|
2679
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Minimal |
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports "../Nominal/Nominal2" |
|
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 |
|
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
lemma alpha_test: |
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
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
|
14 |
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
|
15 |
|
|
e003e5e36bae
added Minimal file to test things
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
end |