15 and trm = |
15 and trm = |
16 Const "ident" |
16 Const "ident" |
17 | Var "name" |
17 | Var "name" |
18 | App "trm" "trm" |
18 | App "trm" "trm" |
19 | Lam "ty" "name" "trm" |
19 | Lam "ty" "name" "trm" |
|
20 |
|
21 instantiation kind and ty and trm :: pt |
|
22 begin |
|
23 |
|
24 primrec |
|
25 permute_kind |
|
26 and permute_ty |
|
27 and permute_trm |
|
28 where |
|
29 "permute_kind pi Type = Type" |
|
30 | "permute_kind pi (KPi t n k) = KPi (permute_ty pi t) (pi \<bullet> n) (permute_kind pi k)" |
|
31 | "permute_ty pi (TConst i) = TConst (pi \<bullet> i)" |
|
32 | "permute_ty pi (TApp A M) = TApp (permute_ty pi A) (permute_trm pi M)" |
|
33 | "permute_ty pi (TPi A x B) = TPi (permute_ty pi A) (pi \<bullet> x) (permute_ty pi B)" |
|
34 | "permute_trm pi (Const i) = Const (pi \<bullet> i)" |
|
35 | "permute_trm pi (Var x) = Var (pi \<bullet> x)" |
|
36 | "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)" |
|
37 | "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)" |
|
38 |
|
39 lemma rperm_zero_ok: |
|
40 "0 \<bullet> (x :: kind) = x" |
|
41 "0 \<bullet> (y :: ty) = y" |
|
42 "0 \<bullet> (z :: trm) = z" |
|
43 apply(induct x and y and z rule: kind_ty_trm.inducts) |
|
44 apply(simp_all) |
|
45 done |
|
46 |
|
47 lemma rperm_plus_ok: |
|
48 "(p + q) \<bullet> (x :: kind) = p \<bullet> q \<bullet> x" |
|
49 "(p + q) \<bullet> (y :: ty) = p \<bullet> q \<bullet> y" |
|
50 "(p + q) \<bullet> (z :: trm) = p \<bullet> q \<bullet> z" |
|
51 apply(induct x and y and z rule: kind_ty_trm.inducts) |
|
52 apply(simp_all) |
|
53 done |
|
54 |
|
55 instance |
|
56 apply default |
|
57 apply (simp_all only:rperm_zero_ok rperm_plus_ok) |
|
58 done |
|
59 |
|
60 end |
20 |
61 |
21 primrec |
62 primrec |
22 rfv_kind :: "kind \<Rightarrow> atom set" |
63 rfv_kind :: "kind \<Rightarrow> atom set" |
23 and rfv_ty :: "ty \<Rightarrow> atom set" |
64 and rfv_ty :: "ty \<Rightarrow> atom set" |
24 and rfv_trm :: "trm \<Rightarrow> atom set" |
65 and rfv_trm :: "trm \<Rightarrow> atom set" |
30 | "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})" |
71 | "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})" |
31 | "rfv_trm (Const i) = {atom i}" |
72 | "rfv_trm (Const i) = {atom i}" |
32 | "rfv_trm (Var x) = {atom x}" |
73 | "rfv_trm (Var x) = {atom x}" |
33 | "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)" |
74 | "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)" |
34 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})" |
75 | "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})" |
35 |
|
36 instantiation kind and ty and trm :: pt |
|
37 begin |
|
38 |
|
39 primrec |
|
40 permute_kind |
|
41 and permute_ty |
|
42 and permute_trm |
|
43 where |
|
44 "permute_kind pi Type = Type" |
|
45 | "permute_kind pi (KPi t n k) = KPi (permute_ty pi t) (pi \<bullet> n) (permute_kind pi k)" |
|
46 | "permute_ty pi (TConst i) = TConst (pi \<bullet> i)" |
|
47 | "permute_ty pi (TApp A M) = TApp (permute_ty pi A) (permute_trm pi M)" |
|
48 | "permute_ty pi (TPi A x B) = TPi (permute_ty pi A) (pi \<bullet> x) (permute_ty pi B)" |
|
49 | "permute_trm pi (Const i) = Const (pi \<bullet> i)" |
|
50 | "permute_trm pi (Var x) = Var (pi \<bullet> x)" |
|
51 | "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)" |
|
52 | "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)" |
|
53 |
|
54 lemma rperm_zero_ok: |
|
55 "0 \<bullet> (x :: kind) = x" |
|
56 "0 \<bullet> (y :: ty) = y" |
|
57 "0 \<bullet> (z :: trm) = z" |
|
58 apply(induct x and y and z rule: kind_ty_trm.inducts) |
|
59 apply(simp_all) |
|
60 done |
|
61 |
|
62 lemma rperm_plus_ok: |
|
63 "(p + q) \<bullet> (x :: kind) = p \<bullet> q \<bullet> x" |
|
64 "(p + q) \<bullet> (y :: ty) = p \<bullet> q \<bullet> y" |
|
65 "(p + q) \<bullet> (z :: trm) = p \<bullet> q \<bullet> z" |
|
66 apply(induct x and y and z rule: kind_ty_trm.inducts) |
|
67 apply(simp_all) |
|
68 done |
|
69 |
|
70 instance |
|
71 apply default |
|
72 apply (simp_all only:rperm_zero_ok rperm_plus_ok) |
|
73 done |
|
74 |
|
75 end |
|
76 |
76 |
77 inductive |
77 inductive |
78 akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100) |
78 akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100) |
79 and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100) |
79 and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100) |
80 and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100) |
80 and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100) |