| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 09 Mar 2010 22:08:38 +0100 | |
| changeset 1380 | dab8d99b37c1 |
| 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 Term9 |
|
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 |
datatype rlam9 = |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
Var9 "name" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
| Lam9 "name" "rlam9" --"bind name in rlam" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
and rbla9 = |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
Bla9 "rlam9" "rlam9" --"bind bv(first) in second" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
primrec |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
rbv9 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
where |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
"rbv9 (Var9 x) = {}"
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
| "rbv9 (Lam9 x b) = {atom x}"
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
|
|
1277
6eacf60ce41d
Permutation and FV_Alpha interface change.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1270
diff
changeset
|
19 |
setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term9.rlam9") 2 *}
|
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
print_theorems |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
|
|
1277
6eacf60ce41d
Permutation and FV_Alpha interface change.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1270
diff
changeset
|
22 |
local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term9.rlam9") [
|
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
[[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
notation |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100)
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
thm alpha_rlam9_alpha_rbla9.intros |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
inductive |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
and |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100)
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
where |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
| a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l fv_rlam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2"
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
37 |
| a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l fv_rlam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 t2" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
quotient_type |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
sorry |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
local_setup {*
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
(fn ctxt => ctxt |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
|> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9}))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
|> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9}))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
|> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9}))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
|> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9}))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
49 |
|> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9}))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
|> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9})))
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
51 |
*} |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
52 |
print_theorems |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
53 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
54 |
instantiation lam9 and bla9 :: pt |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
55 |
begin |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
quotient_definition |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
58 |
"permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
59 |
is |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
60 |
"permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
61 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
62 |
quotient_definition |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
63 |
"permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
64 |
is |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
65 |
"permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
66 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
67 |
instance |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
68 |
sorry |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
70 |
end |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
71 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |
lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk> |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
\<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2" |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
74 |
apply (lifting a3[unfolded alpha_gen]) |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
75 |
apply injection |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
76 |
sorry |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
77 |
|
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
78 |
end |