985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 1
theory LFex
1129
+ − 2
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
985
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
992
+ − 8
datatype kind =
985
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"
992
+ − 11
and ty =
985
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"
992
+ − 15
and trm =
985
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"
992
+ − 19
| Lam "ty" "name" "trm"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 20
992
+ − 21
primrec
985
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})"
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 28
| "rfv_ty (TConst i) = {atom i}"
985
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})"
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 31
| "rfv_trm (Const i) = {atom i}"
985
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
1022
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 54
lemma rperm_zero_ok:
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 55
"0 \<bullet> (x :: kind) = x"
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 56
"0 \<bullet> (y :: ty) = y"
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 57
"0 \<bullet> (z :: trm) = z"
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 58
apply(induct x and y and z rule: kind_ty_trm.inducts)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 59
apply(simp_all)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 60
done
1022
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 61
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 62
lemma rperm_plus_ok:
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 63
"(p + q) \<bullet> (x :: kind) = p \<bullet> q \<bullet> x"
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 64
"(p + q) \<bullet> (y :: ty) = p \<bullet> q \<bullet> y"
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 65
"(p + q) \<bullet> (z :: trm) = p \<bullet> q \<bullet> z"
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 66
apply(induct x and y and z rule: kind_ty_trm.inducts)
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 67
apply(simp_all)
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 68
done
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 69
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 70
instance
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 71
apply default
1022
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 72
apply (simp_all only:rperm_zero_ok rperm_plus_ok)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 73
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 74
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 75
end
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 76
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 77
inductive
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 78
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
+ − 79
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
+ − 80
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
+ − 81
where
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 82
a1: "(Type) \<approx>ki (Type)"
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 83
| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 84
| 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
+ − 85
| a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 86
| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>ty (TPi A' b B')"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 87
| 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
+ − 88
| 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
+ − 89
| a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 90
| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
991
+ − 91
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 92
lemma akind_aty_atrm_inj:
992
+ − 93
"(Type) \<approx>ki (Type) = True"
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 94
"((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>ty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K')))"
992
+ − 95
"(TConst i) \<approx>ty (TConst j) = (i = j)"
+ − 96
"(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 97
"((TPi A a B) \<approx>ty (TPi A' b B')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))))"
992
+ − 98
"(Const i) \<approx>tr (Const j) = (i = j)"
+ − 99
"(Var x) \<approx>tr (Var y) = (x = y)"
+ − 100
"(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 101
"((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))))"
992
+ − 102
apply -
+ − 103
apply (simp add: akind_aty_atrm.intros)
+ − 104
+ − 105
apply rule apply (erule akind.cases) apply simp apply blast
+ − 106
apply (simp only: akind_aty_atrm.intros)
+ − 107
+ − 108
apply rule apply (erule aty.cases) apply simp apply simp apply simp
+ − 109
apply (simp only: akind_aty_atrm.intros)
+ − 110
+ − 111
apply rule apply (erule aty.cases) apply simp apply simp apply simp
+ − 112
apply (simp only: akind_aty_atrm.intros)
+ − 113
+ − 114
apply rule apply (erule aty.cases) apply simp apply simp apply blast
+ − 115
apply (simp only: akind_aty_atrm.intros)
+ − 116
+ − 117
apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+ − 118
apply (simp only: akind_aty_atrm.intros)
+ − 119
+ − 120
apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+ − 121
apply (simp only: akind_aty_atrm.intros)
+ − 122
+ − 123
apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+ − 124
apply (simp only: akind_aty_atrm.intros)
+ − 125
+ − 126
apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast
+ − 127
apply (simp only: akind_aty_atrm.intros)
+ − 128
done
+ − 129
+ − 130
lemma rfv_eqvt[eqvt]:
+ − 131
"((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
+ − 132
"((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
+ − 133
"((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
993
+ − 134
apply(induct t1 and t2 and t3 rule: kind_ty_trm.inducts)
+ − 135
apply(simp_all add: union_eqvt Diff_eqvt)
+ − 136
apply(simp_all add: permute_set_eq atom_eqvt)
992
+ − 137
done
+ − 138
+ − 139
lemma alpha_eqvt:
+ − 140
"t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
+ − 141
"t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
+ − 142
"t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
+ − 143
apply(induct rule: akind_aty_atrm.inducts)
+ − 144
apply (simp_all add: akind_aty_atrm.intros)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 145
apply (simp_all add: akind_aty_atrm_inj)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 146
apply (rule alpha_gen_atom_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 147
apply (simp add: rfv_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 148
apply assumption
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 149
apply (rule alpha_gen_atom_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 150
apply (simp add: rfv_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 151
apply assumption
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 152
apply (rule alpha_gen_atom_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 153
apply (simp add: rfv_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 154
apply assumption
992
+ − 155
done
+ − 156
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 157
lemma al_refl:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 158
fixes K::"kind"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 159
and A::"ty"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 160
and M::"trm"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 161
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
+ − 162
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
+ − 163
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
+ − 164
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
+ − 165
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
+ − 166
apply (rule a2)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 167
apply auto
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 168
apply(rule_tac x="0" in exI)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 169
apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 170
apply (rule a5)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 171
apply auto
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 172
apply(rule_tac x="0" in exI)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 173
apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 174
apply (rule a9)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 175
apply auto
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 176
apply(rule_tac x="0" in exI)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 177
apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 178
done
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 179
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 180
lemma al_sym:
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 181
fixes K K'::"kind" and A A'::"ty" and M M'::"trm"
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 182
shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 183
and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A"
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 184
and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 185
apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 186
apply(simp_all add: akind_aty_atrm.intros)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 187
apply (simp_all add: akind_aty_atrm_inj)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 188
apply(rule alpha_gen_atom_sym)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 189
apply(rule alpha_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 190
apply(assumption)+
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 191
apply(rule alpha_gen_atom_sym)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 192
apply(rule alpha_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 193
apply(assumption)+
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 194
apply(rule alpha_gen_atom_sym)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 195
apply(rule alpha_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 196
apply(assumption)+
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 197
done
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 198
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 199
lemma al_trans:
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 200
fixes K K' K''::"kind" and A A' A''::"ty" and M M' M''::"trm"
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 201
shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 202
and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A'' \<Longrightarrow> A \<approx>ty A''"
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 203
and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 204
apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: akind_aty_atrm.inducts)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 205
apply(simp_all add: akind_aty_atrm.intros)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 206
apply(erule akind.cases)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 207
apply(simp_all add: akind_aty_atrm.intros)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 208
apply(simp add: akind_aty_atrm_inj)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 209
apply(rule alpha_gen_atom_trans)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 210
apply(rule alpha_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 211
apply(assumption)+
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 212
apply(rotate_tac 4)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 213
apply(erule aty.cases)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 214
apply(simp_all add: akind_aty_atrm.intros)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 215
apply(rotate_tac 3)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 216
apply(erule aty.cases)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 217
apply(simp_all add: akind_aty_atrm.intros)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 218
apply(simp add: akind_aty_atrm_inj)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 219
apply(rule alpha_gen_atom_trans)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 220
apply(rule alpha_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 221
apply(assumption)+
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 222
apply(rotate_tac 4)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 223
apply(erule atrm.cases)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 224
apply(simp_all add: akind_aty_atrm.intros)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 225
apply(rotate_tac 3)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 226
apply(erule atrm.cases)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 227
apply(simp_all add: akind_aty_atrm.intros)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 228
apply(simp add: akind_aty_atrm_inj)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 229
apply(rule alpha_gen_atom_trans)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 230
apply(rule alpha_eqvt)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 231
apply(assumption)+
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 232
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 233
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 234
lemma alpha_equivps:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 235
shows "equivp akind"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 236
and "equivp aty"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 237
and "equivp atrm"
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 238
apply(rule equivpI)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 239
unfolding reflp_def symp_def transp_def
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 240
apply(auto intro: al_refl al_sym al_trans)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 241
apply(rule equivpI)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 242
unfolding reflp_def symp_def transp_def
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 243
apply(auto intro: al_refl al_sym al_trans)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 244
apply(rule equivpI)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 245
unfolding reflp_def symp_def transp_def
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 246
apply(auto intro: al_refl al_sym al_trans)
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 247
done
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 248
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 249
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
+ − 250
by (rule alpha_equivps)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 251
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 252
quotient_type
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 253
TY = ty / aty and
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 254
TRM = trm / atrm
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 255
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
+ − 256
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 257
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 258
"TYP :: KIND"
1139
+ − 259
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 260
"Type"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 261
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 262
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 263
"KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
1139
+ − 264
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 265
"KPi"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 266
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 267
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 268
"TCONST :: ident \<Rightarrow> TY"
1139
+ − 269
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 270
"TConst"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 271
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 272
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 273
"TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
1139
+ − 274
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 275
"TApp"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 276
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 277
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 278
"TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
1139
+ − 279
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 280
"TPi"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 281
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 282
(* 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
+ − 283
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 284
"CONS :: ident \<Rightarrow> TRM"
1139
+ − 285
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 286
"Const"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 287
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 288
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 289
"VAR :: name \<Rightarrow> TRM"
1139
+ − 290
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 291
"Var"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 292
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 293
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 294
"APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
1139
+ − 295
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 296
"App"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 297
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 298
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 299
"LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
1139
+ − 300
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 301
"Lam"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 302
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 303
(* 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
+ − 304
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 305
"fv_kind :: KIND \<Rightarrow> atom set"
1139
+ − 306
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 307
"rfv_kind"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 308
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 309
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 310
"fv_ty :: TY \<Rightarrow> atom set"
1139
+ − 311
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 312
"rfv_ty"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 313
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 314
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 315
"fv_trm :: TRM \<Rightarrow> atom set"
1139
+ − 316
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 317
"rfv_trm"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 318
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 319
lemma alpha_rfv:
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 320
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
+ − 321
(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
+ − 322
(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
+ − 323
apply(rule akind_aty_atrm.induct)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 324
apply(simp_all add: alpha_gen)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 325
done
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
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
+ − 328
"(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
+ − 329
"(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
+ − 330
"(op = ===> atrm ===> atrm) permute permute"
992
+ − 331
by (simp_all add:alpha_eqvt)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 332
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 333
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
+ − 334
"(op = ===> aty) TConst TConst"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 335
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
+ − 336
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
+ − 337
"(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
+ − 338
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
+ − 339
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
+ − 340
"(op = ===> atrm) Var Var"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 341
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
+ − 342
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
+ − 343
"(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
+ − 344
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
+ − 345
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
+ − 346
"(op = ===> atrm) Const Const"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 347
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
992
+ − 348
+ − 349
lemma kpi_rsp[quot_respect]:
+ − 350
"(aty ===> op = ===> akind ===> akind) KPi KPi"
993
+ − 351
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 352
apply (rule a2) apply assumption
993
+ − 353
apply (rule_tac x="0" in exI)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 354
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
993
+ − 355
done
+ − 356
992
+ − 357
lemma tpi_rsp[quot_respect]:
+ − 358
"(aty ===> op = ===> aty ===> aty) TPi TPi"
993
+ − 359
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 360
apply (rule a5) apply assumption
993
+ − 361
apply (rule_tac x="0" in exI)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 362
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
993
+ − 363
done
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 364
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
+ − 365
"(aty ===> op = ===> atrm ===> atrm) Lam Lam"
993
+ − 366
apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 367
apply (rule a9) apply assumption
993
+ − 368
apply (rule_tac x="0" in exI)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 369
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
993
+ − 370
done
992
+ − 371
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 372
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
+ − 373
"(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
+ − 374
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
+ − 375
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
+ − 376
"(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
+ − 377
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
+ − 378
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
+ − 379
"(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
+ − 380
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
+ − 381
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 382
thm kind_ty_trm.induct
1082
+ − 383
lemmas KIND_TY_TRM_induct = kind_ty_trm.induct[quot_lifted]
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 384
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 385
thm kind_ty_trm.inducts
1082
+ − 386
lemmas KIND_TY_TRM_inducts = kind_ty_trm.inducts[quot_lifted]
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 387
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 388
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
+ − 389
begin
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 390
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 391
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 392
"permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"
1139
+ − 393
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 394
"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
+ − 395
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 396
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 397
"permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"
1139
+ − 398
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 399
"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
+ − 400
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 401
quotient_definition
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 402
"permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"
1139
+ − 403
is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 404
"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
+ − 405
1083
+ − 406
lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted]
+ − 407
1082
+ − 408
lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"
+ − 409
apply (induct rule: KIND_TY_TRM_induct)
1083
+ − 410
apply (simp_all)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 411
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 412
1082
+ − 413
lemma perm_add_ok:
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 414
"((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))"
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 415
"((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)"
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 416
"((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)"
1082
+ − 417
apply (induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts)
1083
+ − 418
apply (simp_all)
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 419
done
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 420
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 421
instance
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 422
apply default
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 423
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
+ − 424
done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 425
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 426
end
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 427
1082
+ − 428
lemmas AKIND_ATY_ATRM_inducts = akind_aty_atrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 429
1082
+ − 430
lemmas KIND_TY_TRM_INJECT = akind_aty_atrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 431
1082
+ − 432
lemmas fv_kind_ty_trm = rfv_kind_rfv_ty_rfv_trm.simps[quot_lifted]
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 433
1082
+ − 434
lemmas fv_eqvt = rfv_eqvt[quot_lifted]
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 435
1002
+ − 436
lemma supp_kind_ty_trm_easy:
+ − 437
"supp TYP = {}"
+ − 438
"supp (TCONST i) = {atom i}"
+ − 439
"supp (TAPP A M) = supp A \<union> supp M"
+ − 440
"supp (CONS i) = {atom i}"
+ − 441
"supp (VAR x) = {atom x}"
+ − 442
"supp (APP M N) = supp M \<union> supp N"
+ − 443
apply (simp_all add: supp_def permute_ktt KIND_TY_TRM_INJECT)
+ − 444
apply (simp_all only: supp_at_base[simplified supp_def])
+ − 445
apply (simp_all add: Collect_imp_eq Collect_neg_eq)
+ − 446
done
+ − 447
+ − 448
lemma supp_bind:
+ − 449
"(supp (atom na, (ty, ki))) supports (KPI ty na ki)"
+ − 450
"(supp (atom na, (ty, ty2))) supports (TPI ty na ty2)"
+ − 451
"(supp (atom na, (ty, trm))) supports (LAM ty na trm)"
+ − 452
apply(simp_all add: supports_def)
+ − 453
apply(fold fresh_def)
+ − 454
apply(simp_all add: fresh_Pair swap_fresh_fresh)
+ − 455
apply(clarify)
+ − 456
apply(subst swap_at_base_simps(3))
+ − 457
apply(simp_all add: fresh_atom)
+ − 458
apply(clarify)
+ − 459
apply(subst swap_at_base_simps(3))
+ − 460
apply(simp_all add: fresh_atom)
+ − 461
apply(clarify)
+ − 462
apply(subst swap_at_base_simps(3))
+ − 463
apply(simp_all add: fresh_atom)
+ − 464
done
+ − 465
+ − 466
lemma KIND_TY_TRM_fs:
+ − 467
"finite (supp (x\<Colon>KIND))"
+ − 468
"finite (supp (y\<Colon>TY))"
+ − 469
"finite (supp (z\<Colon>TRM))"
+ − 470
apply(induct x and y and z rule: KIND_TY_TRM_inducts)
+ − 471
apply(simp_all add: supp_kind_ty_trm_easy)
+ − 472
apply(rule supports_finite)
+ − 473
apply(rule supp_bind(1))
+ − 474
apply(simp add: supp_Pair supp_atom)
+ − 475
apply(rule supports_finite)
+ − 476
apply(rule supp_bind(2))
+ − 477
apply(simp add: supp_Pair supp_atom)
+ − 478
apply(rule supports_finite)
+ − 479
apply(rule supp_bind(3))
+ − 480
apply(simp add: supp_Pair supp_atom)
+ − 481
done
+ − 482
+ − 483
instance KIND and TY and TRM :: fs
+ − 484
apply(default)
+ − 485
apply(simp_all only: KIND_TY_TRM_fs)
+ − 486
done
+ − 487
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 488
lemma supp_fv:
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 489
"supp t1 = fv_kind t1"
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 490
"supp t2 = fv_ty t2"
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 491
"supp t3 = fv_trm t3"
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 492
apply(induct t1 and t2 and t3 rule: KIND_TY_TRM_inducts)
1002
+ − 493
apply (simp_all add: supp_kind_ty_trm_easy)
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 494
apply (simp_all add: fv_kind_ty_trm)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 495
apply(subgoal_tac "supp (KPI ty name kind) = supp ty \<union> supp (Abs {atom name} kind)")
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 496
apply(simp add: supp_Abs Set.Un_commute)
1002
+ − 497
apply(simp (no_asm) add: supp_def)
+ − 498
apply(simp add: KIND_TY_TRM_INJECT)
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 499
apply(simp add: Abs_eq_iff)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 500
apply(simp add: alpha_gen)
1045
+ − 501
apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt)
+ − 502
apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 503
apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)")
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 504
apply(simp add: supp_Abs Set.Un_commute)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 505
apply(simp (no_asm) add: supp_def)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 506
apply(simp add: KIND_TY_TRM_INJECT)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 507
apply(simp add: Abs_eq_iff)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 508
apply(simp add: alpha_gen)
1045
+ − 509
apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
1002
+ − 510
apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 511
apply(subgoal_tac "supp (LAM ty name trm) = supp ty \<union> supp (Abs {atom name} trm)")
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 512
apply(simp add: supp_Abs Set.Un_commute)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 513
apply(simp (no_asm) add: supp_def)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 514
apply(simp add: KIND_TY_TRM_INJECT)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 515
apply(simp add: Abs_eq_iff)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 516
apply(simp add: alpha_gen)
1045
+ − 517
apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 518
apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 519
done
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 520
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 521
(* Not needed anymore *)
1027
163d6917af62
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 522
lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 523
apply (simp add: permute_set_eq supp_def Abs_eq_iff KIND_TY_TRM_INJECT)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 524
apply (simp add: alpha_gen supp_fv)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 525
apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute)
997
b7d259ded92e
Ported LF to the generic lambda and solved the simpler _supp cases.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 526
done
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 527
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 528
lemma supp_kind_ty_trm:
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 529
"supp TYP = {}"
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 530
"supp (KPI A x K) = supp A \<union> (supp K - {atom x})"
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 531
"supp (TCONST i) = {atom i}"
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 532
"supp (TAPP A M) = supp A \<union> supp M"
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 533
"supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 534
"supp (CONS i) = {atom i}"
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 535
"supp (VAR x) = {atom x}"
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 536
"supp (APP M N) = supp M \<union> supp N"
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 537
"supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
1002
+ − 538
apply (simp_all only: supp_kind_ty_trm_easy)
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 539
apply (simp_all only: supp_fv fv_kind_ty_trm)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 540
done
994
333c24bd595d
More in the LF example in the new nominal way, all is clear until support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 541
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 542
end
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 543
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 544
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 545
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 546