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
|