|
1 theory TySch |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 text {* type schemes *} |
|
8 datatype ty = |
|
9 Var "name" |
|
10 | Fun "ty" "ty" |
|
11 |
|
12 setup {* snd o define_raw_perms ["ty"] ["TySch.ty"] *} |
|
13 print_theorems |
|
14 |
|
15 datatype tyS = |
|
16 All "name set" "ty" |
|
17 |
|
18 setup {* snd o define_raw_perms ["tyS"] ["TySch.tyS"] *} |
|
19 print_theorems |
|
20 |
|
21 local_setup {* snd o define_fv_alpha "TySch.ty" [[[[]], [[], []]]] *} |
|
22 print_theorems |
|
23 |
|
24 (* |
|
25 Doesnot work yet since we do not refer to fv_ty |
|
26 local_setup {* define_raw_fv "TySch.tyS" [[[[], []]]] *} |
|
27 print_theorems |
|
28 *) |
|
29 |
|
30 primrec |
|
31 fv_tyS |
|
32 where |
|
33 "fv_tyS (All xs T) = (fv_ty T - atom ` xs)" |
|
34 |
|
35 inductive |
|
36 alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100) |
|
37 where |
|
38 a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2)) |
|
39 \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2" |
|
40 |
|
41 lemma |
|
42 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))" |
|
43 apply(rule a1) |
|
44 apply(simp add: alpha_gen) |
|
45 apply(rule_tac x="0::perm" in exI) |
|
46 apply(simp add: fresh_star_def) |
|
47 done |
|
48 |
|
49 lemma |
|
50 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))" |
|
51 apply(rule a1) |
|
52 apply(simp add: alpha_gen) |
|
53 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
|
54 apply(simp add: fresh_star_def) |
|
55 done |
|
56 |
|
57 lemma |
|
58 shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))" |
|
59 apply(rule a1) |
|
60 apply(simp add: alpha_gen) |
|
61 apply(rule_tac x="0::perm" in exI) |
|
62 apply(simp add: fresh_star_def) |
|
63 done |
|
64 |
|
65 lemma |
|
66 assumes a: "a \<noteq> b" |
|
67 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))" |
|
68 using a |
|
69 apply(clarify) |
|
70 apply(erule alpha_tyS.cases) |
|
71 apply(simp add: alpha_gen) |
|
72 apply(erule conjE)+ |
|
73 apply(erule exE) |
|
74 apply(erule conjE)+ |
|
75 apply(clarify) |
|
76 apply(simp) |
|
77 apply(simp add: fresh_star_def) |
|
78 apply(auto) |
|
79 done |
|
80 |
|
81 |
|
82 end |