author | Christian Urban <urbanc@in.tum.de> |
Wed, 10 Mar 2010 12:48:55 +0100 | |
changeset 1393 | 4eaae533efc3 |
parent 1362 | e72d9d9eada3 |
permissions | -rw-r--r-- |
1362
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Term5 |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
imports "Parser" |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
atom_decl name |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
ML {* restricted_nominal := 2 *} |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
|
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
nominal_datatype trm5 = |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
Vr5 "name" |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
| Ap5 "trm5" "trm5" |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
| Lt5 l::"lts" t::"trm5" bind "bv5 l" in t |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
and lts = |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
Lnil |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
| Lcons "name" "trm5" "lts" |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
binder |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
bv5 |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
where |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
"bv5 Lnil = {}" |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)" |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
|
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
lemma lets_ok: |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
"(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
apply (simp add: trm5_lts_inject) |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
apply (simp_all add: alpha_gen) |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn) |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
done |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
|
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
lemma lets_nok: |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
"x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons y (Vr5 x) Lnil) (Vr5 y))" |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
apply (simp only: trm5_lts_inject not_ex) |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
apply (rule allI) |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
apply (simp add: alpha_gen) |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn trm5_lts_inject) |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
done |
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
37 |
|
e72d9d9eada3
Term5 written as nominal_datatype is the recursive let.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
end |