985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 1 theory LFex
1219
+ − 2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"
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
1234
+ − 8 datatype rkind =
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 9 Type
1234
+ − 10 | KPi "rty" "name" "rkind"
+ − 11 and rty =
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 12 TConst "ident"
1234
+ − 13 | TApp "rty" "rtrm"
+ − 14 | TPi "rty" "name" "rty"
+ − 15 and rtrm =
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"
1234
+ − 18 | App "rtrm" "rtrm"
+ − 19 | Lam "rty" "name" "rtrm"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 20
1234
+ − 21
+ − 22 instantiation rkind and rty and rtrm :: pt
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 23 begin
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 24
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 25 primrec
1234
+ − 26 permute_rkind
+ − 27 and permute_rty
+ − 28 and permute_rtrm
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 29 where
1234
+ − 30 "permute_rkind pi Type = Type"
+ − 31 | "permute_rkind pi (KPi t n k) = KPi (permute_rty pi t) (pi \<bullet> n) (permute_rkind pi k)"
+ − 32 | "permute_rty pi (TConst i) = TConst (pi \<bullet> i)"
+ − 33 | "permute_rty pi (TApp A M) = TApp (permute_rty pi A) (permute_rtrm pi M)"
+ − 34 | "permute_rty pi (TPi A x B) = TPi (permute_rty pi A) (pi \<bullet> x) (permute_rty pi B)"
+ − 35 | "permute_rtrm pi (Const i) = Const (pi \<bullet> i)"
+ − 36 | "permute_rtrm pi (Var x) = Var (pi \<bullet> x)"
+ − 37 | "permute_rtrm pi (App M N) = App (permute_rtrm pi M) (permute_rtrm pi N)"
+ − 38 | "permute_rtrm pi (Lam A x M) = Lam (permute_rty pi A) (pi \<bullet> x) (permute_rtrm pi M)"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 39
1022
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 40 lemma rperm_zero_ok:
1234
+ − 41 "0 \<bullet> (x :: rkind) = x"
+ − 42 "0 \<bullet> (y :: rty) = y"
+ − 43 "0 \<bullet> (z :: rtrm) = z"
+ − 44 apply(induct x and y and z rule: rkind_rty_rtrm.inducts)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 45 apply(simp_all)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 46 done
1022
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 47
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 48 lemma rperm_plus_ok:
1234
+ − 49 "(p + q) \<bullet> (x :: rkind) = p \<bullet> q \<bullet> x"
+ − 50 "(p + q) \<bullet> (y :: rty) = p \<bullet> q \<bullet> y"
+ − 51 "(p + q) \<bullet> (z :: rtrm) = p \<bullet> q \<bullet> z"
+ − 52 apply(induct x and y and z rule: rkind_rty_rtrm.inducts)
1022
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 53 apply(simp_all)
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 54 done
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 55
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 56 instance
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 57 apply default
1022
cc5830c452c4
With induct instead of induct_tac, just one induction is sufficient.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 58 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
+ − 59 done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 60
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 61 end
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 62
1219
+ − 63 (*
1234
+ − 64 setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}
1219
+ − 65 local_setup {*
1234
+ − 66 snd o define_fv_alpha "LFex.rkind"
1219
+ − 67 [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
+ − 68 [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
+ − 69 [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+ − 70 notation
1234
+ − 71 alpha_rkind ("_ \<approx>ki _" [100, 100] 100)
+ − 72 and alpha_rty ("_ \<approx>rty _" [100, 100] 100)
+ − 73 and alpha_rtrm ("_ \<approx>tr _" [100, 100] 100)
+ − 74 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros
+ − 75 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *}
1219
+ − 76 thm alphas_inj
+ − 77
+ − 78 lemma alphas_eqvt:
+ − 79 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
1234
+ − 80 "t2 \<approx>rty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>rty (pi \<bullet> s2)"
1219
+ − 81 "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
+ − 82 sorry
+ − 83
+ − 84 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []),
1234
+ − 85 (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}]
+ − 86 @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct}
+ − 87 @{thms rkind.inject rty.inject rtrm.inject} @{thms alphas_inj}
+ − 88 @{thms rkind.distinct rty.distinct rtrm.distinct}
+ − 89 @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases}
1219
+ − 90 @{thms alphas_eqvt} ctxt)) ctxt)) *}
+ − 91 thm alphas_equivp
+ − 92 *)
+ − 93
1218
+ − 94 primrec
1234
+ − 95 rfv_rkind :: "rkind \<Rightarrow> atom set"
+ − 96 and rfv_rty :: "rty \<Rightarrow> atom set"
+ − 97 and rfv_rtrm :: "rtrm \<Rightarrow> atom set"
1218
+ − 98 where
1234
+ − 99 "rfv_rkind (Type) = {}"
+ − 100 | "rfv_rkind (KPi A x K) = (rfv_rty A) \<union> ((rfv_rkind K) - {atom x})"
+ − 101 | "rfv_rty (TConst i) = {atom i}"
+ − 102 | "rfv_rty (TApp A M) = (rfv_rty A) \<union> (rfv_rtrm M)"
+ − 103 | "rfv_rty (TPi A x B) = (rfv_rty A) \<union> ((rfv_rty B) - {atom x})"
+ − 104 | "rfv_rtrm (Const i) = {atom i}"
+ − 105 | "rfv_rtrm (Var x) = {atom x}"
+ − 106 | "rfv_rtrm (App M N) = (rfv_rtrm M) \<union> (rfv_rtrm N)"
+ − 107 | "rfv_rtrm (Lam A x M) = (rfv_rty A) \<union> ((rfv_rtrm M) - {atom x})"
1218
+ − 108
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 109 inductive
1234
+ − 110 arkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
+ − 111 and arty :: "rty \<Rightarrow> rty \<Rightarrow> bool" ("_ \<approx>rty _" [100, 100] 100)
+ − 112 and artrm :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 113 where
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 114 a1: "(Type) \<approx>ki (Type)"
1234
+ − 115 | a2: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, K) \<approx>gen arkind rfv_rkind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
+ − 116 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>rty (TConst j)"
+ − 117 | a4: "\<lbrakk>A \<approx>rty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>rty (TApp A' M')"
+ − 118 | a5: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, B) \<approx>gen arty rfv_rty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>rty (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
+ − 119 | 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
+ − 120 | 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
+ − 121 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
1234
+ − 122 | a9: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, M) \<approx>gen artrm rfv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
991
+ − 123
1234
+ − 124 lemma arkind_arty_artrm_inj:
992
+ − 125 "(Type) \<approx>ki (Type) = True"
1234
+ − 126 "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>rty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen arkind rfv_rkind pi ({atom b}, K')))"
+ − 127 "(TConst i) \<approx>rty (TConst j) = (i = j)"
+ − 128 "(TApp A M) \<approx>rty (TApp A' M') = (A \<approx>rty A' \<and> M \<approx>tr M')"
+ − 129 "((TPi A a B) \<approx>rty (TPi A' b B')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen arty rfv_rty pi ({atom b}, B'))))"
992
+ − 130 "(Const i) \<approx>tr (Const j) = (i = j)"
+ − 131 "(Var x) \<approx>tr (Var y) = (x = y)"
+ − 132 "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
1234
+ − 133 "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen artrm rfv_rtrm pi ({atom b}, M'))))"
992
+ − 134 apply -
1234
+ − 135 apply (simp add: arkind_arty_artrm.intros)
992
+ − 136
1234
+ − 137 apply rule apply (erule arkind.cases) apply simp apply blast
+ − 138 apply (simp only: arkind_arty_artrm.intros)
992
+ − 139
1234
+ − 140 apply rule apply (erule arty.cases) apply simp apply simp apply simp
+ − 141 apply (simp only: arkind_arty_artrm.intros)
992
+ − 142
1234
+ − 143 apply rule apply (erule arty.cases) apply simp apply simp apply simp
+ − 144 apply (simp only: arkind_arty_artrm.intros)
992
+ − 145
1234
+ − 146 apply rule apply (erule arty.cases) apply simp apply simp apply blast
+ − 147 apply (simp only: arkind_arty_artrm.intros)
992
+ − 148
1234
+ − 149 apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
+ − 150 apply (simp only: arkind_arty_artrm.intros)
992
+ − 151
1234
+ − 152 apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
+ − 153 apply (simp only: arkind_arty_artrm.intros)
992
+ − 154
1234
+ − 155 apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
+ − 156 apply (simp only: arkind_arty_artrm.intros)
992
+ − 157
1234
+ − 158 apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
+ − 159 apply (simp only: arkind_arty_artrm.intros)
992
+ − 160 done
+ − 161
+ − 162 lemma rfv_eqvt[eqvt]:
1234
+ − 163 "((pi\<bullet>rfv_rkind t1) = rfv_rkind (pi\<bullet>t1))"
+ − 164 "((pi\<bullet>rfv_rty t2) = rfv_rty (pi\<bullet>t2))"
+ − 165 "((pi\<bullet>rfv_rtrm t3) = rfv_rtrm (pi\<bullet>t3))"
+ − 166 apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts)
993
+ − 167 apply(simp_all add: union_eqvt Diff_eqvt)
+ − 168 apply(simp_all add: permute_set_eq atom_eqvt)
992
+ − 169 done
+ − 170
+ − 171 lemma alpha_eqvt:
+ − 172 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
1234
+ − 173 "t2 \<approx>rty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>rty (pi \<bullet> s2)"
992
+ − 174 "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
1234
+ − 175 apply(induct rule: arkind_arty_artrm.inducts)
+ − 176 apply (simp_all add: arkind_arty_artrm.intros)
+ − 177 apply (simp_all add: arkind_arty_artrm_inj)
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
+ − 178 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
+ − 179 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
+ − 180 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
+ − 181 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
+ − 182 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
+ − 183 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
+ − 184 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
+ − 185 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
+ − 186 apply assumption
992
+ − 187 done
+ − 188
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 189 lemma al_refl:
1234
+ − 190 fixes K::"rkind"
+ − 191 and A::"rty"
+ − 192 and M::"rtrm"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 193 shows "K \<approx>ki K"
1234
+ − 194 and "A \<approx>rty A"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 195 and "M \<approx>tr M"
1234
+ − 196 apply(induct K and A and M rule: rkind_rty_rtrm.inducts)
+ − 197 apply(auto intro: arkind_arty_artrm.intros)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 198 apply (rule a2)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 199 apply auto
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 200 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
+ − 201 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
+ − 202 apply (rule a5)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 203 apply auto
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 204 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
+ − 205 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
+ − 206 apply (rule a9)
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 207 apply auto
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 208 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
+ − 209 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
+ − 210 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
+ − 211
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 lemma al_sym:
1234
+ − 213 fixes K K'::"rkind" and A A'::"rty" and M M'::"rtrm"
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
+ − 214 shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"
1234
+ − 215 and "A \<approx>rty A' \<Longrightarrow> A' \<approx>rty A"
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
+ − 216 and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"
1234
+ − 217 apply(induct K K' and A A' and M M' rule: arkind_arty_artrm.inducts)
+ − 218 apply(simp_all add: arkind_arty_artrm.intros)
+ − 219 apply (simp_all add: arkind_arty_artrm_inj)
1210
+ − 220 apply(erule alpha_gen_compose_sym)
+ − 221 apply(erule alpha_eqvt)
+ − 222 apply(erule alpha_gen_compose_sym)
+ − 223 apply(erule alpha_eqvt)
+ − 224 apply(erule alpha_gen_compose_sym)
+ − 225 apply(erule alpha_eqvt)
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
+ − 226 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
+ − 227
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 lemma al_trans:
1234
+ − 229 fixes K K' K''::"rkind" and A A' A''::"rty" and M M' M''::"rtrm"
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
+ − 230 shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"
1234
+ − 231 and "A \<approx>rty A' \<Longrightarrow> A' \<approx>rty A'' \<Longrightarrow> A \<approx>rty A''"
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
+ − 232 and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"
1234
+ − 233 apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: arkind_arty_artrm.inducts)
+ − 234 apply(simp_all add: arkind_arty_artrm.intros)
+ − 235 apply(erule arkind.cases)
+ − 236 apply(simp_all add: arkind_arty_artrm.intros)
+ − 237 apply(simp add: arkind_arty_artrm_inj)
1210
+ − 238 apply(erule alpha_gen_compose_trans)
+ − 239 apply(assumption)
+ − 240 apply(erule alpha_eqvt)
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
+ − 241 apply(rotate_tac 4)
1234
+ − 242 apply(erule arty.cases)
+ − 243 apply(simp_all add: arkind_arty_artrm.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
+ − 244 apply(rotate_tac 3)
1234
+ − 245 apply(erule arty.cases)
+ − 246 apply(simp_all add: arkind_arty_artrm.intros)
+ − 247 apply(simp add: arkind_arty_artrm_inj)
1210
+ − 248 apply(erule alpha_gen_compose_trans)
+ − 249 apply(assumption)
+ − 250 apply(erule alpha_eqvt)
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
+ − 251 apply(rotate_tac 4)
1234
+ − 252 apply(erule artrm.cases)
+ − 253 apply(simp_all add: arkind_arty_artrm.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
+ − 254 apply(rotate_tac 3)
1234
+ − 255 apply(erule artrm.cases)
+ − 256 apply(simp_all add: arkind_arty_artrm.intros)
+ − 257 apply(simp add: arkind_arty_artrm_inj)
1210
+ − 258 apply(erule alpha_gen_compose_trans)
+ − 259 apply(assumption)
+ − 260 apply(erule alpha_eqvt)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 261 done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 262
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 263 lemma alpha_equivps:
1234
+ − 264 shows "equivp arkind"
+ − 265 and "equivp arty"
+ − 266 and "equivp artrm"
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
+ − 267 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
+ − 268 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
+ − 269 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
+ − 270 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
+ − 271 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
+ − 272 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
+ − 273 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
+ − 274 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
+ − 275 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
+ − 276 done
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 277
1234
+ − 278 quotient_type RKIND = rkind / arkind
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 279 by (rule alpha_equivps)
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 quotient_type
1234
+ − 282 RTY = rty / arty and
+ − 283 RTRM = rtrm / artrm
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 284 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
+ − 285
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 286 quotient_definition
1234
+ − 287 "TYP :: RKIND"
1139
+ − 288 is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 289 "Type"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 290
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 291 quotient_definition
1234
+ − 292 "KPI :: RTY \<Rightarrow> name \<Rightarrow> RKIND \<Rightarrow> RKIND"
1139
+ − 293 is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 294 "KPi"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 295
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 296 quotient_definition
1234
+ − 297 "TCONST :: ident \<Rightarrow> RTY"
1139
+ − 298 is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 299 "TConst"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 300
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 301 quotient_definition
1234
+ − 302 "TAPP :: RTY \<Rightarrow> RTRM \<Rightarrow> RTY"
1139
+ − 303 is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 304 "TApp"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 305
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 306 quotient_definition
1234
+ − 307 "TPI :: RTY \<Rightarrow> name \<Rightarrow> RTY \<Rightarrow> RTY"
1139
+ − 308 is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 309 "TPi"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 310
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 311 (* 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
+ − 312 quotient_definition
1234
+ − 313 "CONS :: ident \<Rightarrow> RTRM"
1139
+ − 314 is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 315 "Const"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 316
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 317 quotient_definition
1234
+ − 318 "VAR :: name \<Rightarrow> RTRM"
1139
+ − 319 is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 320 "Var"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 321
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 322 quotient_definition
1234
+ − 323 "APP :: RTRM \<Rightarrow> RTRM \<Rightarrow> RTRM"
1139
+ − 324 is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 325 "App"
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 quotient_definition
1234
+ − 328 "LAM :: RTY \<Rightarrow> name \<Rightarrow> RTRM \<Rightarrow> RTRM"
1139
+ − 329 is
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 330 "Lam"
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 331
1234
+ − 332 (* FIXME: print out a warning if the type contains a liftet type, like rkind \<Rightarrow> name set *)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 333 quotient_definition
1234
+ − 334 "fv_rkind :: RKIND \<Rightarrow> atom set"
1139
+ − 335 is
1234
+ − 336 "rfv_rkind"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 337
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 338 quotient_definition
1234
+ − 339 "fv_rty :: RTY \<Rightarrow> atom set"
1139
+ − 340 is
1234
+ − 341 "rfv_rty"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 342
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 343 quotient_definition
1234
+ − 344 "fv_rtrm :: RTRM \<Rightarrow> atom set"
1139
+ − 345 is
1234
+ − 346 "rfv_rtrm"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 347
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 348 lemma alpha_rfv:
1234
+ − 349 shows "(t \<approx>ki s \<longrightarrow> rfv_rkind t = rfv_rkind s) \<and>
+ − 350 (t1 \<approx>rty s1 \<longrightarrow> rfv_rty t1 = rfv_rty s1) \<and>
+ − 351 (t2 \<approx>tr s2 \<longrightarrow> rfv_rtrm t2 = rfv_rtrm s2)"
+ − 352 apply(rule arkind_arty_artrm.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
+ − 353 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
+ − 354 done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 355
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 356 lemma perm_rsp[quot_respect]:
1234
+ − 357 "(op = ===> arkind ===> arkind) permute permute"
+ − 358 "(op = ===> arty ===> arty) permute permute"
+ − 359 "(op = ===> artrm ===> artrm) permute permute"
992
+ − 360 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
+ − 361
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 362 lemma tconst_rsp[quot_respect]:
1234
+ − 363 "(op = ===> arty) TConst TConst"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 364 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
+ − 365 lemma tapp_rsp[quot_respect]:
1234
+ − 366 "(arty ===> artrm ===> arty) TApp TApp"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 367 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
+ − 368 lemma var_rsp[quot_respect]:
1234
+ − 369 "(op = ===> artrm) Var Var"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 370 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
+ − 371 lemma app_rsp[quot_respect]:
1234
+ − 372 "(artrm ===> artrm ===> artrm) App App"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 373 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
+ − 374 lemma const_rsp[quot_respect]:
1234
+ − 375 "(op = ===> artrm) Const Const"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 376 apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
992
+ − 377
+ − 378 lemma kpi_rsp[quot_respect]:
1234
+ − 379 "(arty ===> op = ===> arkind ===> arkind) KPi KPi"
993
+ − 380 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
+ − 381 apply (rule a2) apply assumption
993
+ − 382 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
+ − 383 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
993
+ − 384 done
+ − 385
992
+ − 386 lemma tpi_rsp[quot_respect]:
1234
+ − 387 "(arty ===> op = ===> arty ===> arty) TPi TPi"
993
+ − 388 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
+ − 389 apply (rule a5) apply assumption
993
+ − 390 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
+ − 391 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
993
+ − 392 done
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 393 lemma lam_rsp[quot_respect]:
1234
+ − 394 "(arty ===> op = ===> artrm ===> artrm) Lam Lam"
993
+ − 395 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
+ − 396 apply (rule a9) apply assumption
993
+ − 397 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
+ − 398 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
993
+ − 399 done
992
+ − 400
1234
+ − 401 lemma rfv_rty_rsp[quot_respect]:
+ − 402 "(arty ===> op =) rfv_rty rfv_rty"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 403 by (simp add: alpha_rfv)
1234
+ − 404 lemma rfv_rkind_rsp[quot_respect]:
+ − 405 "(arkind ===> op =) rfv_rkind rfv_rkind"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 406 by (simp add: alpha_rfv)
1234
+ − 407 lemma rfv_rtrm_rsp[quot_respect]:
+ − 408 "(artrm ===> op =) rfv_rtrm rfv_rtrm"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 409 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
+ − 410
1234
+ − 411 thm rkind_rty_rtrm.induct
+ − 412 lemmas RKIND_RTY_RTRM_induct = rkind_rty_rtrm.induct[quot_lifted]
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 413
1234
+ − 414 thm rkind_rty_rtrm.inducts
+ − 415 lemmas RKIND_RTY_RTRM_inducts = rkind_rty_rtrm.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
+ − 416
1234
+ − 417 instantiation RKIND and RTY and RTRM :: pt
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 418 begin
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 419
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 420 quotient_definition
1234
+ − 421 "permute_RKIND :: perm \<Rightarrow> RKIND \<Rightarrow> RKIND"
1139
+ − 422 is
1234
+ − 423 "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 424
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 425 quotient_definition
1234
+ − 426 "permute_RTY :: perm \<Rightarrow> RTY \<Rightarrow> RTY"
1139
+ − 427 is
1234
+ − 428 "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 429
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 430 quotient_definition
1234
+ − 431 "permute_RTRM :: perm \<Rightarrow> RTRM \<Rightarrow> RTRM"
1139
+ − 432 is
1234
+ − 433 "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 434
1234
+ − 435 lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]
1083
+ − 436
1234
+ − 437 lemma perm_zero_ok: "0 \<bullet> (x :: RKIND) = x \<and> 0 \<bullet> (y :: RTY) = y \<and> 0 \<bullet> (z :: RTRM) = z"
+ − 438 apply (induct rule: RKIND_RTY_RTRM_induct)
1083
+ − 439 apply (simp_all)
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 440 done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 441
1082
+ − 442 lemma perm_add_ok:
1234
+ − 443 "((p + q) \<bullet> (x1 :: RKIND) = (p \<bullet> q \<bullet> x1))"
+ − 444 "((p + q) \<bullet> (x2 :: RTY) = p \<bullet> q \<bullet> x2)"
+ − 445 "((p + q) \<bullet> (x3 :: RTRM) = p \<bullet> q \<bullet> x3)"
+ − 446 apply (induct x1 and x2 and x3 rule: RKIND_RTY_RTRM_inducts)
1083
+ − 447 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
+ − 448 done
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 449
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 450 instance
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 451 apply default
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 452 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
+ − 453 done
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 454
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 455 end
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 456
1234
+ − 457 lemmas ARKIND_ARTY_ARTRM_inducts = arkind_arty_artrm.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
+ − 458
1234
+ − 459 lemmas RKIND_RTY_RTRM_INJECT = arkind_arty_artrm_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
+ − 460
1234
+ − 461 lemmas fv_rkind_rty_rtrm = rfv_rkind_rfv_rty_rfv_rtrm.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
+ − 462
1082
+ − 463 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
+ − 464
1234
+ − 465 lemma supp_rkind_rty_rtrm_easy:
1002
+ − 466 "supp TYP = {}"
+ − 467 "supp (TCONST i) = {atom i}"
+ − 468 "supp (TAPP A M) = supp A \<union> supp M"
+ − 469 "supp (CONS i) = {atom i}"
+ − 470 "supp (VAR x) = {atom x}"
+ − 471 "supp (APP M N) = supp M \<union> supp N"
1234
+ − 472 apply (simp_all add: supp_def permute_ktt RKIND_RTY_RTRM_INJECT)
1002
+ − 473 apply (simp_all only: supp_at_base[simplified supp_def])
+ − 474 apply (simp_all add: Collect_imp_eq Collect_neg_eq)
+ − 475 done
+ − 476
+ − 477 lemma supp_bind:
+ − 478 "(supp (atom na, (ty, ki))) supports (KPI ty na ki)"
+ − 479 "(supp (atom na, (ty, ty2))) supports (TPI ty na ty2)"
1234
+ − 480 "(supp (atom na, (ty, rtrm))) supports (LAM ty na rtrm)"
1002
+ − 481 apply(simp_all add: supports_def)
+ − 482 apply(fold fresh_def)
+ − 483 apply(simp_all add: fresh_Pair swap_fresh_fresh)
+ − 484 apply(clarify)
+ − 485 apply(subst swap_at_base_simps(3))
+ − 486 apply(simp_all add: fresh_atom)
+ − 487 apply(clarify)
+ − 488 apply(subst swap_at_base_simps(3))
+ − 489 apply(simp_all add: fresh_atom)
+ − 490 apply(clarify)
+ − 491 apply(subst swap_at_base_simps(3))
+ − 492 apply(simp_all add: fresh_atom)
+ − 493 done
+ − 494
1234
+ − 495 lemma RKIND_RTY_RTRM_fs:
+ − 496 "finite (supp (x\<Colon>RKIND))"
+ − 497 "finite (supp (y\<Colon>RTY))"
+ − 498 "finite (supp (z\<Colon>RTRM))"
+ − 499 apply(induct x and y and z rule: RKIND_RTY_RTRM_inducts)
+ − 500 apply(simp_all add: supp_rkind_rty_rtrm_easy)
1002
+ − 501 apply(rule supports_finite)
+ − 502 apply(rule supp_bind(1))
+ − 503 apply(simp add: supp_Pair supp_atom)
+ − 504 apply(rule supports_finite)
+ − 505 apply(rule supp_bind(2))
+ − 506 apply(simp add: supp_Pair supp_atom)
+ − 507 apply(rule supports_finite)
+ − 508 apply(rule supp_bind(3))
+ − 509 apply(simp add: supp_Pair supp_atom)
+ − 510 done
+ − 511
1234
+ − 512 instance RKIND and RTY and RTRM :: fs
1002
+ − 513 apply(default)
1234
+ − 514 apply(simp_all only: RKIND_RTY_RTRM_fs)
1002
+ − 515 done
+ − 516
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
+ − 517 lemma supp_fv:
1234
+ − 518 "supp t1 = fv_rkind t1"
+ − 519 "supp t2 = fv_rty t2"
+ − 520 "supp t3 = fv_rtrm t3"
+ − 521 apply(induct t1 and t2 and t3 rule: RKIND_RTY_RTRM_inducts)
+ − 522 apply (simp_all add: supp_rkind_rty_rtrm_easy)
+ − 523 apply (simp_all add: fv_rkind_rty_rtrm)
+ − 524 apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)")
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
+ − 525 apply(simp add: supp_Abs Set.Un_commute)
1002
+ − 526 apply(simp (no_asm) add: supp_def)
1234
+ − 527 apply(simp add: RKIND_RTY_RTRM_INJECT)
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 528 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
+ − 529 apply(simp add: alpha_gen)
1045
+ − 530 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt)
+ − 531 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
1234
+ − 532 apply(subgoal_tac "supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)")
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 533 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
+ − 534 apply(simp (no_asm) add: supp_def)
1234
+ − 535 apply(simp add: RKIND_RTY_RTRM_INJECT)
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 536 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
+ − 537 apply(simp add: alpha_gen)
1045
+ − 538 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt)
1002
+ − 539 apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute)
1234
+ − 540 apply(subgoal_tac "supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)")
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 541 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
+ − 542 apply(simp (no_asm) add: supp_def)
1234
+ − 543 apply(simp add: RKIND_RTY_RTRM_INJECT)
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 544 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
+ − 545 apply(simp add: alpha_gen)
1045
+ − 546 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
+ − 547 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
+ − 548 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
+ − 549
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 550 (* 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
+ − 551 lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \<union> supp A"
1234
+ − 552 apply (simp add: permute_set_eq supp_def Abs_eq_iff RKIND_RTY_RTRM_INJECT)
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 553 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
+ − 554 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
+ − 555 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
+ − 556
1234
+ − 557 lemma supp_rkind_rty_rtrm:
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
+ − 558 "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
+ − 559 "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
+ − 560 "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
+ − 561 "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
+ − 562 "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
+ − 563 "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
+ − 564 "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
+ − 565 "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
+ − 566 "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
1234
+ − 567 apply (simp_all only: supp_rkind_rty_rtrm_easy)
+ − 568 apply (simp_all only: supp_fv fv_rkind_rty_rtrm)
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 569 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
+ − 570
985
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 571 end
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 572
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 573
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 574
ef8a2b0b237a
Ported existing part of LF to new permutations and alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 575