985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 1
theory LFex
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 2
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 3
begin
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 4
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 5
atom_decl name
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 6
atom_decl ident
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 7
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 8
datatype kind =
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 9
Type
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 10
| KPi "ty" "name" "kind"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 11
and ty =
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 12
TConst "ident"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 13
| TApp "ty" "trm"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 14
| TPi "ty" "name" "ty"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 15
and trm =
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 16
Const "ident"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 17
| Var "name"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 18
| App "trm" "trm"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 19
| Lam "ty" "name" "trm"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 20
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 21
fun
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 22
rfv_kind :: "kind \<Rightarrow> atom set"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 23
and rfv_ty :: "ty \<Rightarrow> atom set"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 24
and rfv_trm :: "trm \<Rightarrow> atom set"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 25
where
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 26
"rfv_kind (Type) = {}"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 27
| "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 28
| "rfv_ty (TConst i) = {}"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 29
| "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 30
| "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 31
| "rfv_trm (Const i) = {}"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 32
| "rfv_trm (Var x) = {atom x}"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 33
| "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 34
| "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 35
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 36
instantiation kind and ty and trm :: pt
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 37
begin
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 38
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 39
primrec
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 40
permute_kind
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 41
and permute_ty
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 42
and permute_trm
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 43
where
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 44
"permute_kind pi Type = Type"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 45
| "permute_kind pi (KPi t n k) = KPi (permute_ty pi t) (pi \<bullet> n) (permute_kind pi k)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 46
| "permute_ty pi (TConst i) = TConst (pi \<bullet> i)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 47
| "permute_ty pi (TApp A M) = TApp (permute_ty pi A) (permute_trm pi M)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 48
| "permute_ty pi (TPi A x B) = TPi (permute_ty pi A) (pi \<bullet> x) (permute_ty pi B)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 49
| "permute_trm pi (Const i) = Const (pi \<bullet> i)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 50
| "permute_trm pi (Var x) = Var (pi \<bullet> x)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 51
| "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 52
| "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 53
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 54
lemma rperm_zero_ok: "0 \<bullet> (x :: kind) = x \<and> 0 \<bullet> (y :: ty) = y \<and> 0 \<bullet> (z :: trm) = z"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 55
apply(induct_tac rule: kind_ty_trm.induct)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 56
apply(simp_all)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 57
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 58
instance
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 59
apply default
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 60
apply (simp_all only:rperm_zero_ok)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 61
apply(induct_tac [!] x)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 62
apply(simp_all)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 63
apply(induct_tac ty)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 64
apply(simp_all)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 65
apply(induct_tac trm)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 66
apply(simp_all)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 67
apply(induct_tac trm)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 68
apply(simp_all)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 69
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 70
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 71
end
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 72
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 73
inductive
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 74
akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 75
and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 76
and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 77
where
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 78
a1: "(Type) \<approx>ki (Type)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 79
| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 80
| a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 81
| a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 82
| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 83
| a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 84
| a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 85
| a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 86
| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 87
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 88
lemma al_refl:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 89
fixes K::"kind"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 90
and A::"ty"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 91
and M::"trm"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 92
shows "K \<approx>ki K"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 93
and "A \<approx>ty A"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 94
and "M \<approx>tr M"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 95
apply(induct K and A and M rule: kind_ty_trm.inducts)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 96
apply(auto intro: akind_aty_atrm.intros)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 97
apply (rule a2)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 98
apply auto
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 99
apply(rule_tac x="0" in exI)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 100
apply(simp_all add: fresh_star_def fresh_zero_perm)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 101
apply (rule a5)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 102
apply auto
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 103
apply(rule_tac x="0" in exI)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 104
apply(simp_all add: fresh_star_def fresh_zero_perm)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 105
apply (rule a9)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 106
apply auto
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 107
apply(rule_tac x="0" in exI)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 108
apply(simp_all add: fresh_star_def fresh_zero_perm)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 109
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 110
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 111
lemma alpha_equivps:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 112
shows "equivp akind"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 113
and "equivp aty"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 114
and "equivp atrm"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 115
sorry
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 116
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 117
quotient_type KIND = kind / akind
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 118
by (rule alpha_equivps)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 119
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 120
quotient_type
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 121
TY = ty / aty and
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 122
TRM = trm / atrm
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 123
by (auto intro: alpha_equivps)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 124
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 125
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 126
"TYP :: KIND"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 127
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 128
"Type"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 129
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 130
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 131
"KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 132
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 133
"KPi"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 134
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 135
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 136
"TCONST :: ident \<Rightarrow> TY"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 137
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 138
"TConst"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 139
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 140
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 141
"TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 142
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 143
"TApp"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 144
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 145
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 146
"TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 147
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 148
"TPi"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 149
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 150
(* FIXME: does not work with CONST *)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 151
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 152
"CONS :: ident \<Rightarrow> TRM"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 153
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 154
"Const"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 155
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 156
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 157
"VAR :: name \<Rightarrow> TRM"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 158
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 159
"Var"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 160
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 161
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 162
"APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 163
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 164
"App"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 165
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 166
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 167
"LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 168
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 169
"Lam"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 170
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 171
(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 172
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 173
"fv_kind :: KIND \<Rightarrow> atom set"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 174
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 175
"rfv_kind"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 176
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 177
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 178
"fv_ty :: TY \<Rightarrow> atom set"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 179
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 180
"rfv_ty"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 181
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 182
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 183
"fv_trm :: TRM \<Rightarrow> atom set"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 184
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 185
"rfv_trm"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 186
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 187
thm akind_aty_atrm.induct
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 188
lemma alpha_rfv:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 189
shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 190
(t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 191
(t2 \<approx>tr s2 \<longrightarrow> rfv_trm t2 = rfv_trm s2)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 192
apply(rule akind_aty_atrm.induct)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 193
apply(simp_all)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 194
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 195
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 196
lemma perm_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 197
"(op = ===> akind ===> akind) permute permute"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 198
"(op = ===> aty ===> aty) permute permute"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 199
"(op = ===> atrm ===> atrm) permute permute"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 200
apply simp_all
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 201
sorry (* by eqvt *)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 202
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 203
lemma kpi_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 204
"(aty ===> op = ===> akind ===> akind) KPi KPi"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 205
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 206
lemma tconst_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 207
"(op = ===> aty) TConst TConst"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 208
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 209
lemma tapp_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 210
"(aty ===> atrm ===> aty) TApp TApp"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 211
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 212
lemma tpi_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 213
"(aty ===> op = ===> aty ===> aty) TPi TPi"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 214
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 215
lemma var_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 216
"(op = ===> atrm) Var Var"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 217
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 218
lemma app_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 219
"(atrm ===> atrm ===> atrm) App App"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 220
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 221
lemma const_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 222
"(op = ===> atrm) Const Const"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 223
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 224
lemma lam_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 225
"(aty ===> op = ===> atrm ===> atrm) Lam Lam"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 226
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 227
lemma rfv_ty_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 228
"(aty ===> op =) rfv_ty rfv_ty"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 229
by (simp add: alpha_rfv)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 230
lemma rfv_kind_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 231
"(akind ===> op =) rfv_kind rfv_kind"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 232
by (simp add: alpha_rfv)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 233
lemma rfv_trm_rsp[quot_respect]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 234
"(atrm ===> op =) rfv_trm rfv_trm"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 235
by (simp add: alpha_rfv)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 236
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 237
thm akind_aty_atrm.induct
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 238
thm kind_ty_trm.induct
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 239
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 240
lemma KIND_TY_TRM_induct: "\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 241
\<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 242
\<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 243
\<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 244
\<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 245
\<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 246
by (lifting kind_ty_trm.induct)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 247
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 248
instantiation KIND and TY and TRM :: pt
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 249
begin
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 250
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 251
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 252
"permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 253
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 254
"permute :: perm \<Rightarrow> kind \<Rightarrow> kind"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 255
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 256
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 257
"permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 258
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 259
"permute :: perm \<Rightarrow> ty \<Rightarrow> ty"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 260
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 261
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 262
"permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 263
as
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 264
"permute :: perm \<Rightarrow> trm \<Rightarrow> trm"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 265
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 266
term "permute_TRM"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 267
thm permute_kind_permute_ty_permute_trm.simps
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 268
lemma [simp]:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 269
shows "pi \<bullet> TYP = TYP"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 270
and "pi \<bullet> (KPI t n k) = KPI (pi \<bullet> t) (pi \<bullet> n) (pi \<bullet> k)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 271
and "pi \<bullet> (TCONST i) = TCONST (pi \<bullet> i)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 272
and "pi \<bullet> (TAPP A M) = TAPP (pi \<bullet> A) (pi \<bullet> M)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 273
and "pi \<bullet> (TPI A x B) = TPI (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> B)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 274
and "pi \<bullet> (CONS i) = CONS (pi \<bullet> i)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 275
and "pi \<bullet> (VAR x) = VAR (pi \<bullet> x)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 276
and "pi \<bullet> (APP M N) = APP (pi \<bullet> M) (pi \<bullet> N)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 277
and "pi \<bullet> (LAM A x M) = LAM (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> M)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 278
apply (lifting permute_kind_permute_ty_permute_trm.simps)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 279
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 280
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 281
lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 282
apply (induct rule: KIND_TY_TRM_induct)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 283
apply simp_all
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 284
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 285
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 286
lemma perm_add_ok: "((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> (x1 :: KIND))) \<and> ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2) \<and> ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 287
apply(induct_tac [!] rule: KIND_TY_TRM_induct)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 288
apply (simp_all)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 289
(* Sth went wrong... *)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 290
sorry
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 291
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 292
instance
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 293
apply default
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 294
apply (simp_all add: perm_zero_ok perm_add_ok)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 295
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 296
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 297
end
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 298
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 299
lemma "\<lbrakk>P10 TYP TYP;
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 300
\<And>A A' K x K' x'.
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 301
\<lbrakk>(A :: TY) = A'; P20 A A';
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 302
\<exists>pi. fv_kind K - {atom x} = fv_kind K' - {atom x'} \<and>
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 303
(fv_kind K - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> K) = K' \<and> P10 (pi \<bullet> K) K') \<and> pi \<bullet> x = x'\<rbrakk>
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 304
\<Longrightarrow> P10 (KPI A x K) (KPI A' x' K');
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 305
\<And>i j. i = j \<Longrightarrow> P20 (TCONST i) (TCONST j);
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 306
\<And>A A' M M'. \<lbrakk>A = A'; P20 A A'; M = M'; P30 M M'\<rbrakk> \<Longrightarrow> P20 (TAPP A M) (TAPP A' M');
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 307
\<And>A A' B x B' x'.
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 308
\<lbrakk>A = A'; P20 A A';
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 309
\<exists>pi. fv_ty B - {atom x} = fv_ty B' - {atom x'} \<and>
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 310
(fv_ty B - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> B) = B' \<and> P20 (pi \<bullet> B) B') \<and> pi \<bullet> x = x'\<rbrakk>
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 311
\<Longrightarrow> P20 (TPI A x B) (TPI A' x' B');
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 312
\<And>i j. i = j \<Longrightarrow> P30 (CONS i) (CONS j); \<And>x y. x = y \<Longrightarrow> P30 (VAR x) (VAR y);
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 313
\<And>M M' N N'. \<lbrakk>M = M'; P30 M M'; N = N'; P30 N N'\<rbrakk> \<Longrightarrow> P30 (APP M N) (APP M' N');
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 314
\<And>A A' M x M' x'.
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 315
\<lbrakk>A = A'; P20 A A';
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 316
\<exists>pi. fv_trm M - {atom x} = fv_trm M' - {atom x'} \<and>
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 317
(fv_trm M - {atom x}) \<sharp>* pi \<and> ((pi \<bullet> M) = M' \<and> P30 (pi \<bullet> M) M') \<and> pi \<bullet> x = x'\<rbrakk>
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 318
\<Longrightarrow> P30 (LAM A x M) (LAM A' x' M')\<rbrakk>
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 319
\<Longrightarrow> (x10 = x20 \<longrightarrow> P10 x10 x20) \<and>
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 320
(x30 = x40 \<longrightarrow> P20 x30 x40) \<and> (x50 = x60 \<longrightarrow> P30 x50 x60)"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 321
apply (lifting akind_aty_atrm.induct)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 322
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 323
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 324
end
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 325
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 326
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 327
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 328