equal
deleted
inserted
replaced
49 | "permute_trm pi (Const i) = Const (pi \<bullet> i)" |
49 | "permute_trm pi (Const i) = Const (pi \<bullet> i)" |
50 | "permute_trm pi (Var x) = Var (pi \<bullet> x)" |
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)" |
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)" |
52 | "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)" |
53 |
53 |
54 lemma rperm_zero_ok: "0 \<bullet> (x :: kind) = x \<and> 0 \<bullet> (y :: ty) = y \<and> 0 \<bullet> (z :: trm) = z" |
54 lemma rperm_zero_ok: |
55 apply(induct_tac rule: kind_ty_trm.induct) |
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) |
56 apply(simp_all) |
59 apply(simp_all) |
57 done |
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 |
58 instance |
70 instance |
59 apply default |
71 apply default |
60 apply (simp_all only:rperm_zero_ok) |
72 apply (simp_all only:rperm_zero_ok rperm_plus_ok) |
61 apply(induct_tac[!] x) |
|
62 apply(simp_all) |
|
63 apply(induct_tac ty) |
|
64 apply(simp_all) |
|
65 apply(induct_tac trm) |
|
66 apply(simp_all) |
|
67 apply(induct_tac trm) |
|
68 apply(simp_all) |
|
69 done |
73 done |
70 |
74 |
71 end |
75 end |
72 |
76 |
73 inductive |
77 inductive |