| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 16 Mar 2010 18:13:34 +0100 | |
| changeset 1461 | c79bcbe1983d |
| parent 1277 | 6eacf60ce41d |
| permissions | -rw-r--r-- |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Term7 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
atom_decl name |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
(* example with a respectful bn function defined over the type itself *) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
datatype rtrm7 = |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
rVr7 "name" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
| rLm7 "name" "rtrm7" --"bind left in right" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
primrec |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
rbv7 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
where |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
"rbv7 (rVr7 n) = {atom n}"
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
| "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
| "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
|
|
1277
6eacf60ce41d
Permutation and FV_Alpha interface change.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1270
diff
changeset
|
21 |
setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term7.rtrm7") 1 *}
|
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
thm permute_rtrm7.simps |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
|
|
1277
6eacf60ce41d
Permutation and FV_Alpha interface change.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1270
diff
changeset
|
24 |
local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term7.rtrm7") [
|
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
[[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
print_theorems |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
notation |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100)
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
thm alpha_rtrm7.intros |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
thm fv_rtrm7.simps |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
inductive |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
where |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
| a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
37 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
apply simp |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
apply simp |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
apply (rule a3) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
apply (simp_all add: alpha_gen fresh_star_def) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
apply (rule a1) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
apply (rule refl) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
done |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
49 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
end |