| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Tue, 09 Mar 2010 17:25:35 +0100 | |
| changeset 1378 | 5c6c950812b1 |
| 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 |