950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 1 theory Terms
1028
+ − 2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 3 begin
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 4
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 5 atom_decl name
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 6
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 7 text {* primrec seems to be genarally faster than fun *}
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 8
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 9 section {*** lets with binding patterns ***}
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 10
1028
+ − 11 datatype rtrm1 =
+ − 12 rVr1 "name"
+ − 13 | rAp1 "rtrm1" "rtrm1"
+ − 14 | rLm1 "name" "rtrm1" --"name is bound in trm1"
+ − 15 | rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 16 and bp =
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 17 BUnit
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 18 | BVr "name"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 19 | BPr "bp" "bp"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 20
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 21 (* to be given by the user *)
1029
+ − 22
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 23 primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 24 bv1
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 25 where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 26 "bv1 (BUnit) = {}"
957
+ − 27 | "bv1 (BVr x) = {atom x}"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 29
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 30 (* needs to be calculated by the package *)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 31 primrec
1028
+ − 32 rfv_trm1 and rfv_bp
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 33 where
1028
+ − 34 "rfv_trm1 (rVr1 x) = {atom x}"
+ − 35 | "rfv_trm1 (rAp1 t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2)"
+ − 36 | "rfv_trm1 (rLm1 x t) = (rfv_trm1 t) - {atom x}"
+ − 37 | "rfv_trm1 (rLt1 bp t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2 - bv1 bp)"
+ − 38 | "rfv_bp (BUnit) = {}"
+ − 39 | "rfv_bp (BVr x) = {atom x}"
+ − 40 | "rfv_bp (BPr b1 b2) = (rfv_bp b1) \<union> (rfv_bp b2)"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 41
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 42 (* needs to be stated by the package *)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 43 instantiation
1028
+ − 44 rtrm1 and bp :: pt
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 45 begin
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 46
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 47 primrec
1028
+ − 48 permute_rtrm1 and permute_bp
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 49 where
1028
+ − 50 "permute_rtrm1 pi (rVr1 a) = rVr1 (pi \<bullet> a)"
+ − 51 | "permute_rtrm1 pi (rAp1 t1 t2) = rAp1 (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"
+ − 52 | "permute_rtrm1 pi (rLm1 a t) = rLm1 (pi \<bullet> a) (permute_rtrm1 pi t)"
+ − 53 | "permute_rtrm1 pi (rLt1 bp t1 t2) = rLt1 (permute_bp pi bp) (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"
957
+ − 54 | "permute_bp pi (BUnit) = BUnit"
+ − 55 | "permute_bp pi (BVr a) = BVr (pi \<bullet> a)"
+ − 56 | "permute_bp pi (BPr bp1 bp2) = BPr (permute_bp pi bp1) (permute_bp pi bp2)"
+ − 57
1028
+ − 58 lemma pt_rtrm1_bp_zero:
+ − 59 fixes t::rtrm1
957
+ − 60 and b::bp
+ − 61 shows "0 \<bullet> t = t"
+ − 62 and "0 \<bullet> b = b"
1028
+ − 63 apply(induct t and b rule: rtrm1_bp.inducts)
957
+ − 64 apply(simp_all)
+ − 65 done
+ − 66
1028
+ − 67 lemma pt_rtrm1_bp_plus:
+ − 68 fixes t::rtrm1
957
+ − 69 and b::bp
+ − 70 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ − 71 and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
1028
+ − 72 apply(induct t and b rule: rtrm1_bp.inducts)
957
+ − 73 apply(simp_all)
+ − 74 done
+ − 75
+ − 76 instance
+ − 77 apply default
1028
+ − 78 apply(simp_all add: pt_rtrm1_bp_zero pt_rtrm1_bp_plus)
957
+ − 79 done
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 80
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 81 end
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 82
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 83 inductive
1028
+ − 84 alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 85 where
1028
+ − 86 a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)"
+ − 87 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2"
+ − 88 | a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"
+ − 89 | a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2"
+ − 90
1029
+ − 91 lemma alpha1_inj:
1028
+ − 92 "(rVr1 a \<approx>1 rVr1 b) = (a = b)"
+ − 93 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"
+ − 94 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s)))"
+ − 95 "(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))))"
+ − 96 apply -
+ − 97 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 98 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 99 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 100 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 101 done
+ − 102
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 103 (* Shouyld we derive it? But bv is given by the user? *)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 104 lemma bv1_eqvt[eqvt]:
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 105 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 106 apply (induct x)
1043
+ − 107 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 108 done
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 109
1031
+ − 110 lemma rfv_trm1_eqvt[eqvt]:
+ − 111 shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
+ − 112 apply (induct t)
1043
+ − 113 apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
1031
+ − 114 done
+ − 115
+ − 116
1028
+ − 117 lemma alpha1_eqvt:
+ − 118 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
1031
+ − 119 apply (induct t s rule: alpha1.inducts)
+ − 120 apply (simp_all add:eqvts alpha1_inj)
1033
+ − 121 apply (erule exE)
+ − 122 apply (rule_tac x="pi \<bullet> pia" in exI)
+ − 123 apply (simp add: alpha_gen)
+ − 124 apply(erule conjE)+
+ − 125 apply(rule conjI)
+ − 126 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
1043
+ − 127 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt rfv_trm1_eqvt)
1033
+ − 128 apply(rule conjI)
+ − 129 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
1043
+ − 130 apply(simp add: atom_eqvt Diff_eqvt rfv_trm1_eqvt insert_eqvt empty_eqvt)
1033
+ − 131 apply(simp add: permute_eqvt[symmetric])
+ − 132 apply (erule exE)
+ − 133 apply (rule_tac x="pi \<bullet> pia" in exI)
+ − 134 apply (simp add: alpha_gen)
+ − 135 apply(erule conjE)+
+ − 136 apply(rule conjI)
+ − 137 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
1043
+ − 138 apply(simp add: rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
1033
+ − 139 apply(rule conjI)
+ − 140 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
1043
+ − 141 apply(simp add: atom_eqvt rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
1033
+ − 142 apply(simp add: permute_eqvt[symmetric])
+ − 143 done
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 144
957
+ − 145 lemma alpha1_equivp: "equivp alpha1"
+ − 146 sorry
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 147
1028
+ − 148 quotient_type trm1 = rtrm1 / alpha1
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 149 by (rule alpha1_equivp)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 150
1028
+ − 151 quotient_definition
+ − 152 "Vr1 :: name \<Rightarrow> trm1"
+ − 153 as
+ − 154 "rVr1"
+ − 155
1029
+ − 156 quotient_definition
+ − 157 "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
+ − 158 as
+ − 159 "rAp1"
+ − 160
+ − 161 quotient_definition
+ − 162 "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
+ − 163 as
+ − 164 "rLm1"
+ − 165
+ − 166 quotient_definition
+ − 167 "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
+ − 168 as
+ − 169 "rLt1"
+ − 170
+ − 171 quotient_definition
+ − 172 "fv_trm1 :: trm1 \<Rightarrow> atom set"
+ − 173 as
+ − 174 "rfv_trm1"
+ − 175
+ − 176 lemma alpha_rfv1:
+ − 177 shows "t \<approx>1 s \<Longrightarrow> rfv_trm1 t = rfv_trm1 s"
+ − 178 apply(induct rule: alpha1.induct)
+ − 179 apply(simp_all add: alpha_gen.simps)
+ − 180 done
+ − 181
+ − 182 lemma [quot_respect]:
+ − 183 "(op = ===> alpha1) rVr1 rVr1"
+ − 184 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"
+ − 185 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1"
+ − 186 "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"
+ − 187 apply (auto intro: alpha1.intros)
+ − 188 apply(rule a3) apply (rule_tac x="0" in exI)
+ − 189 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
+ − 190 apply(rule a4) apply assumption apply (rule_tac x="0" in exI)
+ − 191 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
+ − 192 done
+ − 193
+ − 194 lemma [quot_respect]:
+ − 195 "(op = ===> alpha1 ===> alpha1) permute permute"
+ − 196 apply auto
+ − 197 apply (rule alpha1_eqvt)
+ − 198 apply simp
+ − 199 done
+ − 200
+ − 201 lemma [quot_respect]:
+ − 202 "(alpha1 ===> op =) rfv_trm1 rfv_trm1"
+ − 203 apply (simp add: alpha_rfv1)
+ − 204 done
+ − 205
+ − 206 lemma trm1_bp_induct: "
+ − 207 \<lbrakk>\<And>name. P1 (Vr1 name);
+ − 208 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);
+ − 209 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);
+ − 210 \<And>bp rtrm11 rtrm12.
+ − 211 \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);
+ − 212 P2 BUnit; \<And>name. P2 (BVr name);
+ − 213 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>
+ − 214 \<Longrightarrow> P1 rtrma \<and> P2 bpa"
+ − 215 apply (lifting rtrm1_bp.induct)
+ − 216 done
+ − 217
+ − 218 lemma trm1_bp_inducts: "
+ − 219 \<lbrakk>\<And>name. P1 (Vr1 name);
+ − 220 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);
+ − 221 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);
+ − 222 \<And>bp rtrm11 rtrm12.
+ − 223 \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);
+ − 224 P2 BUnit; \<And>name. P2 (BVr name);
+ − 225 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>
+ − 226 \<Longrightarrow> P1 rtrma"
+ − 227 "\<lbrakk>\<And>name. P1 (Vr1 name);
+ − 228 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);
+ − 229 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);
+ − 230 \<And>bp rtrm11 rtrm12.
+ − 231 \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);
+ − 232 P2 BUnit; \<And>name. P2 (BVr name);
+ − 233 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>
+ − 234 \<Longrightarrow> P2 bpa"
+ − 235 by (lifting rtrm1_bp.inducts)
+ − 236
+ − 237 instantiation trm1 and bp :: pt
+ − 238 begin
+ − 239
+ − 240 quotient_definition
+ − 241 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
+ − 242 as
+ − 243 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
+ − 244
+ − 245 lemma permute_trm1 [simp]:
+ − 246 shows "pi \<bullet> Vr1 a = Vr1 (pi \<bullet> a)"
+ − 247 and "pi \<bullet> Ap1 t1 t2 = Ap1 (pi \<bullet> t1) (pi \<bullet> t2)"
+ − 248 and "pi \<bullet> Lm1 a t = Lm1 (pi \<bullet> a) (pi \<bullet> t)"
+ − 249 and "pi \<bullet> Lt1 b t s = Lt1 (pi \<bullet> b) (pi \<bullet> t) (pi \<bullet> s)"
+ − 250 apply -
+ − 251 apply(lifting permute_rtrm1_permute_bp.simps(1))
+ − 252 apply(lifting permute_rtrm1_permute_bp.simps(2))
+ − 253 apply(lifting permute_rtrm1_permute_bp.simps(3))
+ − 254 apply(lifting permute_rtrm1_permute_bp.simps(4))
+ − 255 done
+ − 256 instance
+ − 257 apply default
+ − 258 apply(induct_tac [!] x rule: trm1_bp_inducts(1))
+ − 259 apply(simp_all)
+ − 260 done
+ − 261
+ − 262 end
+ − 263
+ − 264 lemma fv_trm1:
+ − 265 "fv_trm1 (Vr1 x) = {atom x}"
+ − 266 "fv_trm1 (Ap1 t1 t2) = fv_trm1 t1 \<union> fv_trm1 t2"
+ − 267 "fv_trm1 (Lm1 x t) = fv_trm1 t - {atom x}"
+ − 268 "fv_trm1 (Lt1 bp t1 t2) = fv_trm1 t1 \<union> (fv_trm1 t2 - bv1 bp)"
+ − 269 apply -
+ − 270 apply (lifting rfv_trm1_rfv_bp.simps(1))
+ − 271 apply (lifting rfv_trm1_rfv_bp.simps(2))
+ − 272 apply (lifting rfv_trm1_rfv_bp.simps(3))
+ − 273 apply (lifting rfv_trm1_rfv_bp.simps(4))
+ − 274 done
+ − 275
+ − 276 lemma fv_trm1_eqvt:
+ − 277 shows "(p \<bullet> fv_trm1 t) = fv_trm1 (p \<bullet> t)"
+ − 278 apply(lifting rfv_trm1_eqvt)
+ − 279 done
+ − 280
+ − 281 lemma alpha1_INJ:
+ − 282 "(Vr1 a = Vr1 b) = (a = b)"
+ − 283 "(Ap1 t1 s1 = Ap1 t2 s2) = (t1 = t2 \<and> s1 = s2)"
+ − 284 "(Lm1 aa t = Lm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen (op =) fv_trm1 pi ({atom ab}, s)))"
+ − 285 "(Lt1 b1 t1 s1 = Lt1 b2 t2 s2) = (t1 = t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen (op =) fv_trm1 pi ((bv1 b2), s2))))"
+ − 286 unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen])
+ − 287 done
+ − 288
1031
+ − 289 lemma lm1_supp_pre:
+ − 290 shows "(supp (atom x, t)) supports (Lm1 x t) "
+ − 291 apply(simp add: supports_def)
+ − 292 apply(fold fresh_def)
+ − 293 apply(simp add: fresh_Pair swap_fresh_fresh)
+ − 294 apply(clarify)
+ − 295 apply(subst swap_at_base_simps(3))
+ − 296 apply(simp_all add: fresh_atom)
+ − 297 done
+ − 298
+ − 299 lemma lt1_supp_pre:
+ − 300 shows "(supp (x, t, s)) supports (Lt1 t x s) "
+ − 301 apply(simp add: supports_def)
+ − 302 apply(fold fresh_def)
+ − 303 apply(simp add: fresh_Pair swap_fresh_fresh)
+ − 304 done
+ − 305
+ − 306 lemma bp_supp: "finite (supp (bp :: bp))"
+ − 307 apply (induct bp)
+ − 308 apply(simp_all add: supp_def)
+ − 309 apply (fold supp_def)
+ − 310 apply (simp add: supp_at_base)
+ − 311 apply(simp add: Collect_imp_eq)
+ − 312 apply(simp add: Collect_neg_eq[symmetric])
+ − 313 apply (fold supp_def)
+ − 314 apply (simp)
+ − 315 done
+ − 316
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 317 instance trm1 :: fs
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 318 apply default
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 319 apply(induct_tac x rule: trm1_bp_inducts(1))
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 320 apply(simp_all)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 321 apply(simp add: supp_def alpha1_INJ eqvts)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 322 apply(simp add: supp_def[symmetric] supp_at_base)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 323 apply(simp only: supp_def alpha1_INJ eqvts permute_trm1)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 324 apply(simp add: Collect_imp_eq Collect_neg_eq)
1031
+ − 325 apply(rule supports_finite)
+ − 326 apply(rule lm1_supp_pre)
+ − 327 apply(simp add: supp_Pair supp_atom)
+ − 328 apply(rule supports_finite)
+ − 329 apply(rule lt1_supp_pre)
+ − 330 apply(simp add: supp_Pair supp_atom bp_supp)
+ − 331 done
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 332
1029
+ − 333 lemma supp_fv:
+ − 334 shows "supp t = fv_trm1 t"
+ − 335 apply(induct t rule: trm1_bp_inducts(1))
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 336 apply(simp_all)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 337 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 338 apply(simp only: supp_at_base[simplified supp_def])
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 339 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 340 apply(simp add: Collect_imp_eq Collect_neg_eq)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 341 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 342 apply(simp add: supp_Abs fv_trm1)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 343 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 344 apply(simp add: alpha1_INJ)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 345 apply(simp add: Abs_eq_iff)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 346 apply(simp add: alpha_gen.simps)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 347 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 348 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 349 apply(simp add: supp_Abs fv_trm1)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 350 apply(simp (no_asm) add: supp_def)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 351 apply(simp add: alpha1_INJ)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 352 apply(simp add: Abs_eq_iff)
1033
+ − 353 apply(simp add: alpha_gen)
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 354 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 355 apply(simp add: Collect_imp_eq Collect_neg_eq)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 356 done
1029
+ − 357
1032
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 358 lemma trm1_supp:
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 359 "supp (Vr1 x) = {atom x}"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 360 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 361 "supp (Lm1 x t) = (supp t) - {atom x}"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 362 "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 363 by (simp_all only: supp_fv fv_trm1)
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 364
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 365 lemma trm1_induct_strong:
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 366 assumes "\<And>name b. P b (Vr1 name)"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 367 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 368 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 369 and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 370 shows "P a rtrma"
1035
+ − 371 sorry
1032
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 372
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 373 section {*** lets with single assignments ***}
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 374
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 375 datatype trm2 =
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 376 Vr2 "name"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 377 | Ap2 "trm2" "trm2"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 378 | Lm2 "name" "trm2"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 379 | Lt2 "assign" "trm2"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 380 and assign =
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 381 As "name" "trm2"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 382
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 383 (* to be given by the user *)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 384 primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 385 bv2
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 386 where
957
+ − 387 "bv2 (As x t) = {atom x}"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 388
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 389 (* needs to be calculated by the package *)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 390 primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 391 fv_trm2 and fv_assign
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 392 where
957
+ − 393 "fv_trm2 (Vr2 x) = {atom x}"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 394 | "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)"
957
+ − 395 | "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {atom x}"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 396 | "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 397 | "fv_assign (As x t) = (fv_trm2 t)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 398
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 399 (* needs to be stated by the package *)
957
+ − 400 instantiation
+ − 401 trm2 and assign :: pt
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 402 begin
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 403
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 404 primrec
957
+ − 405 permute_trm2 and permute_assign
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 406 where
957
+ − 407 "permute_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"
+ − 408 | "permute_trm2 pi (Ap2 t1 t2) = Ap2 (permute_trm2 pi t1) (permute_trm2 pi t2)"
+ − 409 | "permute_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (permute_trm2 pi t)"
+ − 410 | "permute_trm2 pi (Lt2 as t) = Lt2 (permute_assign pi as) (permute_trm2 pi t)"
+ − 411 | "permute_assign pi (As a t) = As (pi \<bullet> a) (permute_trm2 pi t)"
+ − 412
+ − 413 lemma pt_trm2_assign_zero:
+ − 414 fixes t::trm2
+ − 415 and b::assign
+ − 416 shows "0 \<bullet> t = t"
+ − 417 and "0 \<bullet> b = b"
+ − 418 apply(induct t and b rule: trm2_assign.inducts)
+ − 419 apply(simp_all)
+ − 420 done
+ − 421
+ − 422 lemma pt_trm2_assign_plus:
+ − 423 fixes t::trm2
+ − 424 and b::assign
+ − 425 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ − 426 and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
+ − 427 apply(induct t and b rule: trm2_assign.inducts)
+ − 428 apply(simp_all)
+ − 429 done
+ − 430
+ − 431 instance
+ − 432 apply default
+ − 433 apply(simp_all add: pt_trm2_assign_zero pt_trm2_assign_plus)
+ − 434 done
+ − 435
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 436
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 437 end
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 438
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 439 inductive
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 440 alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 441 where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 442 a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 443 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2"
957
+ − 444 | a3: "\<exists>pi. (fv_trm2 t - {atom a} = fv_trm2 s - {atom b} \<and>
+ − 445 (fv_trm2 t - {atom a})\<sharp>* pi \<and>
+ − 446 (pi \<bullet> t) \<approx>2 s \<and>
+ − 447 (pi \<bullet> a) = b)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 448 \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s"
957
+ − 449 | a4: "\<exists>pi. (
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 450 fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and>
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 451 (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and>
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 452 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 453 ) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 454
957
+ − 455 lemma alpha2_equivp: "equivp alpha2"
+ − 456 sorry
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 457
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 458 quotient_type qtrm2 = trm2 / alpha2
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 459 by (rule alpha2_equivp)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 460
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 461 section {*** lets with many assignments ***}
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 462
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 463 datatype trm3 =
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 464 Vr3 "name"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 465 | Ap3 "trm3" "trm3"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 466 | Lm3 "name" "trm3"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 467 | Lt3 "assigns" "trm3"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 468 and assigns =
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 469 ANil
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 470 | ACons "name" "trm3" "assigns"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 471
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 472 (* to be given by the user *)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 473 primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 474 bv3
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 475 where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 476 "bv3 ANil = {}"
957
+ − 477 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 478
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 479 primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 480 fv_trm3 and fv_assigns
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 481 where
957
+ − 482 "fv_trm3 (Vr3 x) = {atom x}"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 483 | "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)"
957
+ − 484 | "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {atom x}"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 485 | "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 486 | "fv_assigns (ANil) = {}"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 487 | "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 488
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 489 (* needs to be stated by the package *)
957
+ − 490 instantiation
+ − 491 trm3 and assigns :: pt
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 492 begin
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 493
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 494 primrec
957
+ − 495 permute_trm3 and permute_assigns
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 496 where
957
+ − 497 "permute_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)"
+ − 498 | "permute_trm3 pi (Ap3 t1 t2) = Ap3 (permute_trm3 pi t1) (permute_trm3 pi t2)"
+ − 499 | "permute_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (permute_trm3 pi t)"
+ − 500 | "permute_trm3 pi (Lt3 as t) = Lt3 (permute_assigns pi as) (permute_trm3 pi t)"
+ − 501 | "permute_assigns pi (ANil) = ANil"
+ − 502 | "permute_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (permute_trm3 pi t) (permute_assigns pi as)"
+ − 503
+ − 504 lemma pt_trm3_assigns_zero:
+ − 505 fixes t::trm3
+ − 506 and b::assigns
+ − 507 shows "0 \<bullet> t = t"
+ − 508 and "0 \<bullet> b = b"
+ − 509 apply(induct t and b rule: trm3_assigns.inducts)
+ − 510 apply(simp_all)
+ − 511 done
+ − 512
+ − 513 lemma pt_trm3_assigns_plus:
+ − 514 fixes t::trm3
+ − 515 and b::assigns
+ − 516 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ − 517 and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
+ − 518 apply(induct t and b rule: trm3_assigns.inducts)
+ − 519 apply(simp_all)
+ − 520 done
+ − 521
+ − 522 instance
+ − 523 apply default
+ − 524 apply(simp_all add: pt_trm3_assigns_zero pt_trm3_assigns_plus)
+ − 525 done
+ − 526
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 527
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 528 end
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 529
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 530 inductive
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 531 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 532 where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 533 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 534 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
957
+ − 535 | a3: "\<exists>pi. (fv_trm3 t - {atom a} = fv_trm3 s - {atom b} \<and>
+ − 536 (fv_trm3 t - {atom a})\<sharp>* pi \<and>
+ − 537 (pi \<bullet> t) \<approx>3 s \<and>
+ − 538 (pi \<bullet> a) = b)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 539 \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
957
+ − 540 | a4: "\<exists>pi. (
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 541 fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and>
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 542 (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and>
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 543 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 544 ) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 545
957
+ − 546 lemma alpha3_equivp: "equivp alpha3"
+ − 547 sorry
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 548
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 549 quotient_type qtrm3 = trm3 / alpha3
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 550 by (rule alpha3_equivp)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 551
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 552
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 553 section {*** lam with indirect list recursion ***}
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 554
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 555 datatype trm4 =
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 556 Vr4 "name"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 557 | Ap4 "trm4" "trm4 list"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 558 | Lm4 "name" "trm4"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 559
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 560 thm trm4.recs
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 561
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 562 primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 563 fv_trm4 and fv_trm4_list
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 564 where
957
+ − 565 "fv_trm4 (Vr4 x) = {atom x}"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 566 | "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
957
+ − 567 | "fv_trm4 (Lm4 x t) = (fv_trm4 t) - {atom x}"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 568 | "fv_trm4_list ([]) = {}"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 569 | "fv_trm4_list (t#ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 570
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 571
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 572 (* needs to be stated by the package *)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 573 (* there cannot be a clause for lists, as *)
957
+ − 574 (* permuteutations are already defined in Nominal (also functions, options, and so on) *)
+ − 575 instantiation
+ − 576 trm4 :: pt
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 577 begin
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 578
957
+ − 579 (* does not work yet *)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 580 primrec
963
+ − 581 permute_trm4 and permute_trm4_list
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 582 where
957
+ − 583 "permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)"
963
+ − 584 | "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute_trm4_list pi ts)"
957
+ − 585 | "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)"
963
+ − 586 | "permute_trm4_list pi ([]) = []"
+ − 587 | "permute_trm4_list pi (t#ts) = (permute_trm4 pi t) # (permute_trm4_list pi ts)"
+ − 588
+ − 589 lemma pt_trm4_list_zero:
+ − 590 fixes t::trm4
+ − 591 and ts::"trm4 list"
+ − 592 shows "0 \<bullet> t = t"
+ − 593 and "permute_trm4_list 0 ts = ts"
+ − 594 apply(induct t and ts rule: trm4.inducts)
+ − 595 apply(simp_all)
+ − 596 done
+ − 597
+ − 598 lemma pt_trm4_list_plus:
+ − 599 fixes t::trm4
+ − 600 and ts::"trm4 list"
+ − 601 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ − 602 and "(permute_trm4_list (p + q) ts) = permute_trm4_list p (permute_trm4_list q ts)"
+ − 603 apply(induct t and ts rule: trm4.inducts)
+ − 604 apply(simp_all)
+ − 605 done
+ − 606
+ − 607
+ − 608 instance
+ − 609 apply(default)
+ − 610 apply(simp_all add: pt_trm4_list_zero pt_trm4_list_plus)
+ − 611 done
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 612
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 613 end
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 614
963
+ − 615 (* "repairing" of the permute function *)
+ − 616 lemma repaired:
+ − 617 fixes ts::"trm4 list"
+ − 618 shows "permute_trm4_list p ts = p \<bullet> ts"
+ − 619 apply(induct ts)
+ − 620 apply(simp_all)
+ − 621 done
+ − 622
976
+ − 623 thm permute_trm4_permute_trm4_list.simps
963
+ − 624 thm permute_trm4_permute_trm4_list.simps[simplified repaired]
+ − 625
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 626 inductive
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 627 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 628 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100)
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 629 where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 630 a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 631 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"
963
+ − 632 | a4: "\<exists>pi. (fv_trm4 t - {atom a} = fv_trm4 s - {atom b} \<and>
+ − 633 (fv_trm4 t - {atom a})\<sharp>* pi \<and>
+ − 634 (pi \<bullet> t) \<approx>4 s \<and>
+ − 635 (pi \<bullet> a) = b)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 636 \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 637 | a5: "[] \<approx>4list []"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 638 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 639
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 640 lemma alpha4_equivp: "equivp alpha4" sorry
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 641 lemma alpha4list_equivp: "equivp alpha4list" sorry
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 642
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 643 quotient_type
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 644 qtrm4 = trm4 / alpha4 and
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 645 qtrm4list = "trm4 list" / alpha4list
1042
+ − 646 by (simp_all add: alpha4_equivp alpha4list_equivp)
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 647
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 648
1035
+ − 649 datatype rtrm5 =
+ − 650 rVr5 "name"
+ − 651 | rAp5 "rtrm5" "rtrm5"
+ − 652 | rLt5 "rlts" "rtrm5"
+ − 653 and rlts =
+ − 654 rLnil
+ − 655 | rLcons "name" "rtrm5" "rlts"
+ − 656
+ − 657 primrec
1050
+ − 658 rbv5
1035
+ − 659 where
1050
+ − 660 "rbv5 rLnil = {}"
+ − 661 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
1035
+ − 662
+ − 663 primrec
+ − 664 rfv_trm5 and rfv_lts
+ − 665 where
+ − 666 "rfv_trm5 (rVr5 n) = {atom n}"
+ − 667 | "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)"
1050
+ − 668 | "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - rbv5 lts) \<union> (rfv_lts lts - rbv5 lts)"
1035
+ − 669 | "rfv_lts (rLnil) = {}"
+ − 670 | "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)"
+ − 671
+ − 672 instantiation
+ − 673 rtrm5 and rlts :: pt
+ − 674 begin
+ − 675
+ − 676 primrec
+ − 677 permute_rtrm5 and permute_rlts
+ − 678 where
+ − 679 "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)"
+ − 680 | "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)"
1050
+ − 681 | "permute_rtrm5 pi (rLt5 ls t) = rLt5 (permute_rlts pi ls) (permute_rtrm5 pi t)"
1035
+ − 682 | "permute_rlts pi (rLnil) = rLnil"
+ − 683 | "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)"
+ − 684
+ − 685 lemma pt_rtrm5_zero:
+ − 686 fixes t::rtrm5
+ − 687 and l::rlts
+ − 688 shows "0 \<bullet> t = t"
+ − 689 and "0 \<bullet> l = l"
+ − 690 apply(induct t and l rule: rtrm5_rlts.inducts)
+ − 691 apply(simp_all)
+ − 692 done
+ − 693
+ − 694 lemma pt_rtrm5_plus:
+ − 695 fixes t::rtrm5
+ − 696 and l::rlts
+ − 697 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ − 698 and "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)"
+ − 699 apply(induct t and l rule: rtrm5_rlts.inducts)
+ − 700 apply(simp_all)
+ − 701 done
+ − 702
+ − 703 instance
+ − 704 apply default
+ − 705 apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)
+ − 706 done
+ − 707
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 708 end
1035
+ − 709
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 710 inductive
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 711 alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 712 and
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 713 alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 714 where
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 715 a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 716 | a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
1050
+ − 717 | a3: "\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and>
+ − 718 (rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and>
+ − 719 (pi \<bullet> (rbv5 l1) = rbv5 l2))
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 720 \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 721 | a4: "rLnil \<approx>l rLnil"
1040
+ − 722 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
+ − 723
+ − 724 print_theorems
1035
+ − 725
1040
+ − 726 lemma alpha5_inj:
+ − 727 "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
+ − 728 "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
1050
+ − 729 "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2) \<and>
+ − 730 (rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2) \<and>
+ − 731 (pi \<bullet> (rbv5 l1) = rbv5 l2)))"
1040
+ − 732 "rLnil \<approx>l rLnil"
+ − 733 "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2 \<and> n1 = n2)"
+ − 734 apply -
+ − 735 apply (simp_all add: alpha5_alphalts.intros)
+ − 736 apply rule
+ − 737 apply (erule alpha5.cases)
+ − 738 apply (simp_all add: alpha5_alphalts.intros)
+ − 739 apply rule
+ − 740 apply (erule alpha5.cases)
+ − 741 apply (simp_all add: alpha5_alphalts.intros)
+ − 742 apply rule
+ − 743 apply (erule alpha5.cases)
+ − 744 apply (simp_all add: alpha5_alphalts.intros)
+ − 745 apply rule
+ − 746 apply (erule alphalts.cases)
+ − 747 apply (simp_all add: alpha5_alphalts.intros)
+ − 748 done
+ − 749
+ − 750 lemma alpha5_equivps:
+ − 751 shows "equivp alpha5"
+ − 752 and "equivp alphalts"
+ − 753 sorry
+ − 754
+ − 755 quotient_type
+ − 756 trm5 = rtrm5 / alpha5
+ − 757 and
+ − 758 lts = rlts / alphalts
+ − 759 by (auto intro: alpha5_equivps)
+ − 760
1046
+ − 761 quotient_definition
+ − 762 "Vr5 :: name \<Rightarrow> trm5"
+ − 763 as
+ − 764 "rVr5"
+ − 765
+ − 766 quotient_definition
+ − 767 "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
+ − 768 as
+ − 769 "rAp5"
+ − 770
+ − 771 quotient_definition
+ − 772 "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
+ − 773 as
+ − 774 "rLt5"
+ − 775
+ − 776 quotient_definition
+ − 777 "Lnil :: lts"
+ − 778 as
+ − 779 "rLnil"
+ − 780
+ − 781 quotient_definition
+ − 782 "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
+ − 783 as
+ − 784 "rLcons"
+ − 785
+ − 786 quotient_definition
+ − 787 "fv_trm5 :: trm5 \<Rightarrow> atom set"
+ − 788 as
+ − 789 "rfv_trm5"
+ − 790
+ − 791 quotient_definition
1050
+ − 792 "fv_lts :: lts \<Rightarrow> atom set"
1046
+ − 793 as
+ − 794 "rfv_lts"
+ − 795
1050
+ − 796 quotient_definition
+ − 797 "bv5 :: lts \<Rightarrow> atom set"
+ − 798 as
+ − 799 "rbv5"
+ − 800
+ − 801 lemma alpha5_rfv:
+ − 802 "(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)"
+ − 803 "(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
+ − 804 apply(induct rule: alpha5_alphalts.inducts)
+ − 805 apply(simp_all add: alpha_gen)
+ − 806 apply(erule conjE)+
+ − 807 apply(erule exE)
+ − 808 apply(erule conjE)+
+ − 809 apply simp
+ − 810 done
+ − 811
+ − 812 lemma [quot_respect]:
+ − 813 "(op = ===> alpha5 ===> alpha5) permute permute"
+ − 814 "(op = ===> alphalts ===> alphalts) permute permute"
+ − 815 "(op = ===> alpha5) rVr5 rVr5"
+ − 816 "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
+ − 817 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+ − 818 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+ − 819 "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
+ − 820 "(alpha5 ===> op =) rfv_trm5 rfv_trm5"
+ − 821 "(alphalts ===> op =) rfv_lts rfv_lts"
+ − 822 "(alphalts ===> op =) rbv5 rbv5"
+ − 823 sorry
+ − 824
1053
+ − 825 lemma bv_list_rsp:
1055
+ − 826 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
+ − 827 apply(induct rule: alpha5_alphalts.inducts(2))
1053
+ − 828 apply(simp_all)
+ − 829 done
+ − 830
+ − 831 lemma
+ − 832 shows "(alphalts ===> op =) rbv5 rbv5"
+ − 833 by (simp add: bv_list_rsp)
+ − 834
+ − 835
1050
+ − 836 instantiation trm5 and lts :: pt
+ − 837 begin
+ − 838
+ − 839 quotient_definition
+ − 840 "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
+ − 841 as
+ − 842 "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
+ − 843
+ − 844 quotient_definition
+ − 845 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
+ − 846 as
+ − 847 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
+ − 848
+ − 849 lemma permute_trm5_lts:
+ − 850 "pi \<bullet> (Vr5 a) = Vr5 (pi \<bullet> a)"
+ − 851 "pi \<bullet> (Ap5 t1 t2) = Ap5 (pi \<bullet> t1) (pi \<bullet> t2)"
+ − 852 "pi \<bullet> (Lt5 ls t) = Lt5 (pi \<bullet> ls) (pi \<bullet> t)"
+ − 853 "pi \<bullet> Lnil = Lnil"
+ − 854 "pi \<bullet> (Lcons n t ls) = Lcons (pi \<bullet> n) (pi \<bullet> t) (pi \<bullet> ls)"
+ − 855 by (lifting permute_rtrm5_permute_rlts.simps)
+ − 856
+ − 857 lemma trm5_lts_zero:
+ − 858 "0 \<bullet> (x\<Colon>trm5) = x"
+ − 859 "0 \<bullet> (y\<Colon>lts) = y"
+ − 860 sorry
+ − 861
+ − 862 lemma trm5_lts_plus:
+ − 863 "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
+ − 864 "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
+ − 865 sorry
+ − 866
+ − 867 instance
+ − 868 apply default
+ − 869 apply (simp_all add: trm5_lts_zero trm5_lts_plus)
+ − 870 done
1040
+ − 871
1035
+ − 872 end
1050
+ − 873
+ − 874 lemma alpha5_INJ:
+ − 875 "((Vr5 a) = (Vr5 b)) = (a = b)"
+ − 876 "(Ap5 t1 s1 = Ap5 t2 s2) = (t1 = t2 \<and> s1 = s2)"
+ − 877 "(Lt5 l1 t1 = Lt5 l2 t2) =
+ − 878 (\<exists>pi. ((bv5 l1, t1) \<approx>gen (op =) fv_trm5 pi (bv5 l2, t2) \<and>
+ − 879 (bv5 l1, l1) \<approx>gen (op =) fv_lts pi (bv5 l2, l2) \<and>
+ − 880 (pi \<bullet> (bv5 l1) = bv5 l2)))"
+ − 881 "Lnil = Lnil"
+ − 882 "(Lcons n1 t1 ls1 = Lcons n2 t2 ls2) = (ls1 = ls2 \<and> t1 = t2 \<and> n1 = n2)"
+ − 883 unfolding alpha_gen
+ − 884 apply(lifting alpha5_inj[unfolded alpha_gen])
+ − 885 done
+ − 886
+ − 887 lemma bv5[simp]:
+ − 888 "bv5 Lnil = {}"
+ − 889 "bv5 (Lcons n t ltl) = {atom n} \<union> bv5 ltl"
+ − 890 by (lifting rbv5.simps)
+ − 891
+ − 892 lemma fv_trm5_lts[simp]:
+ − 893 "fv_trm5 (Vr5 n) = {atom n}"
+ − 894 "fv_trm5 (Ap5 t s) = fv_trm5 t \<union> fv_trm5 s"
+ − 895 "fv_trm5 (Lt5 lts t) = fv_trm5 t - bv5 lts \<union> (fv_lts lts - bv5 lts)"
+ − 896 "fv_lts Lnil = {}"
+ − 897 "fv_lts (Lcons n t ltl) = fv_trm5 t \<union> fv_lts ltl"
+ − 898 by (lifting rfv_trm5_rfv_lts.simps)
+ − 899
+ − 900 lemma lets_ok:
+ − 901 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
+ − 902 apply (subst alpha5_INJ)
+ − 903 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 904 apply (simp only: alpha_gen)
1052
+ − 905 apply (simp add: permute_trm5_lts fresh_star_def)
+ − 906 apply (simp add: insert_eqvt eqvts atom_eqvt)
+ − 907 done
1050
+ − 908
1056
+ − 909 lemma lets_ok2:
+ − 910 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+ − 911 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+ − 912 apply (subst alpha5_INJ)
+ − 913 apply (simp add: alpha_gen)
+ − 914 apply (simp add: permute_trm5_lts fresh_star_def)
+ − 915 apply (rule allI)
+ − 916 apply (subst alpha5_INJ)
+ − 917 apply (subst alpha5_INJ)
+ − 918 apply (subst alpha5_INJ)
+ − 919 apply (simp add: insert_eqvt eqvts atom_eqvt)
+ − 920 apply (subst alpha5_INJ(5))
+ − 921 apply (subst alpha5_INJ)
+ − 922 apply (subst alpha5_INJ(5))
+ − 923 apply (subst alpha5_INJ)
+ − 924 apply (rule impI)+
+ − 925 apply (simp)
+ − 926 done
+ − 927
1048
+ − 928 text {* type schemes *}
+ − 929 datatype ty =
+ − 930 Var "name"
+ − 931 | Fun "ty" "ty"
+ − 932
+ − 933 instantiation
+ − 934 ty :: pt
+ − 935 begin
+ − 936
+ − 937 primrec
+ − 938 permute_ty
+ − 939 where
+ − 940 "permute_ty pi (Var a) = Var (pi \<bullet> a)"
+ − 941 | "permute_ty pi (Fun T1 T2) = Fun (permute_ty pi T1) (permute_ty pi T2)"
1046
+ − 942
1048
+ − 943 lemma pt_ty_zero:
+ − 944 fixes T::ty
+ − 945 shows "0 \<bullet> T = T"
+ − 946 apply(induct T rule: ty.inducts)
+ − 947 apply(simp_all)
+ − 948 done
1046
+ − 949
1048
+ − 950 lemma pt_ty_plus:
+ − 951 fixes T::ty
+ − 952 shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"
+ − 953 apply(induct T rule: ty.inducts)
+ − 954 apply(simp_all)
+ − 955 done
+ − 956
+ − 957 instance
+ − 958 apply default
+ − 959 apply(simp_all add: pt_ty_zero pt_ty_plus)
+ − 960 done
1046
+ − 961
1035
+ − 962 end
1048
+ − 963
+ − 964 datatype tyS =
+ − 965 All "name set" "ty"
1046
+ − 966
1048
+ − 967 instantiation
+ − 968 tyS :: pt
+ − 969 begin
+ − 970
+ − 971 primrec
+ − 972 permute_tyS
+ − 973 where
+ − 974 "permute_tyS pi (All xs T) = All (pi \<bullet> xs) (pi \<bullet> T)"
1046
+ − 975
1048
+ − 976 lemma pt_tyS_zero:
+ − 977 fixes T::tyS
+ − 978 shows "0 \<bullet> T = T"
+ − 979 apply(induct T rule: tyS.inducts)
+ − 980 apply(simp_all)
+ − 981 done
1046
+ − 982
1048
+ − 983 lemma pt_tyS_plus:
+ − 984 fixes T::tyS
+ − 985 shows "((p + q) \<bullet> T) = p \<bullet> (q \<bullet> T)"
+ − 986 apply(induct T rule: tyS.inducts)
+ − 987 apply(simp_all)
+ − 988 done
+ − 989
+ − 990 instance
+ − 991 apply default
+ − 992 apply(simp_all add: pt_tyS_zero pt_tyS_plus)
+ − 993 done
+ − 994
+ − 995 end
1046
+ − 996
1040
+ − 997
1048
+ − 998 abbreviation
+ − 999 "atoms xs \<equiv> {atom x| x. x \<in> xs}"
+ − 1000
+ − 1001 primrec
+ − 1002 rfv_ty
+ − 1003 where
+ − 1004 "rfv_ty (Var n) = {atom n}"
+ − 1005 | "rfv_ty (Fun T1 T2) = (rfv_ty T1) \<union> (rfv_ty T2)"
+ − 1006
+ − 1007 primrec
+ − 1008 rfv_tyS
+ − 1009 where
+ − 1010 "rfv_tyS (All xs T) = (rfv_ty T - atoms xs)"
+ − 1011
+ − 1012 inductive
+ − 1013 alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
+ − 1014 where
+ − 1015 a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) rfv_ty pi (atoms xs2, T2))
+ − 1016 \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
+ − 1017
+ − 1018 lemma
+ − 1019 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"
+ − 1020 apply(rule a1)
+ − 1021 apply(simp add: alpha_gen)
+ − 1022 apply(rule_tac x="0::perm" in exI)
+ − 1023 apply(simp add: fresh_star_def)
+ − 1024 done
+ − 1025
+ − 1026 lemma
+ − 1027 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"
+ − 1028 apply(rule a1)
+ − 1029 apply(simp add: alpha_gen)
+ − 1030 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+ − 1031 apply(simp add: fresh_star_def)
+ − 1032 done
+ − 1033
+ − 1034 lemma
+ − 1035 shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"
+ − 1036 apply(rule a1)
+ − 1037 apply(simp add: alpha_gen)
+ − 1038 apply(rule_tac x="0::perm" in exI)
+ − 1039 apply(simp add: fresh_star_def)
+ − 1040 done
+ − 1041
+ − 1042 lemma
+ − 1043 assumes a: "a \<noteq> b"
+ − 1044 shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"
+ − 1045 using a
+ − 1046 apply(clarify)
+ − 1047 apply(erule alpha_tyS.cases)
+ − 1048 apply(simp add: alpha_gen)
+ − 1049 apply(erule conjE)+
+ − 1050 apply(erule exE)
+ − 1051 apply(erule conjE)+
+ − 1052 apply(clarify)
+ − 1053 apply(simp)
+ − 1054 apply(simp add: fresh_star_def)
+ − 1055 apply(auto)
+ − 1056 done
1051
+ − 1057
1048
+ − 1058
1035
+ − 1059 end