|
1 theory Term9 |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 datatype rlam9 = |
|
8 Var9 "name" |
|
9 | Lam9 "name" "rlam9" --"bind name in rlam" |
|
10 and rbla9 = |
|
11 Bla9 "rlam9" "rlam9" --"bind bv(first) in second" |
|
12 |
|
13 primrec |
|
14 rbv9 |
|
15 where |
|
16 "rbv9 (Var9 x) = {}" |
|
17 | "rbv9 (Lam9 x b) = {atom x}" |
|
18 |
|
19 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Term9.rlam9", "Term9.rbla9"] *} |
|
20 print_theorems |
|
21 |
|
22 local_setup {* snd o define_fv_alpha "Term9.rlam9" [ |
|
23 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} |
|
24 notation |
|
25 alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and |
|
26 alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100) |
|
27 thm alpha_rlam9_alpha_rbla9.intros |
|
28 |
|
29 |
|
30 inductive |
|
31 alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100) |
|
32 and |
|
33 alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100) |
|
34 where |
|
35 a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)" |
|
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" |
|
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" |
|
38 |
|
39 quotient_type |
|
40 lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b |
|
41 sorry |
|
42 |
|
43 local_setup {* |
|
44 (fn ctxt => ctxt |
|
45 |> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9})) |
|
46 |> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9})) |
|
47 |> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9})) |
|
48 |> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9})) |
|
49 |> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9})) |
|
50 |> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9}))) |
|
51 *} |
|
52 print_theorems |
|
53 |
|
54 instantiation lam9 and bla9 :: pt |
|
55 begin |
|
56 |
|
57 quotient_definition |
|
58 "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9" |
|
59 is |
|
60 "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9" |
|
61 |
|
62 quotient_definition |
|
63 "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9" |
|
64 is |
|
65 "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9" |
|
66 |
|
67 instance |
|
68 sorry |
|
69 |
|
70 end |
|
71 |
|
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> |
|
73 \<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2" |
|
74 apply (lifting a3[unfolded alpha_gen]) |
|
75 apply injection |
|
76 sorry |
|
77 |
|
78 end |