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)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 107
apply (simp_all add: eqvts)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 108
apply (rule atom_eqvt)
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 109
done
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 110
1031
+ − 111
lemma rfv_trm1_eqvt[eqvt]:
+ − 112
shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
+ − 113
apply (induct t)
+ − 114
apply (simp_all add: eqvts)
+ − 115
apply (rule atom_eqvt)
+ − 116
apply (simp add: atom_eqvt)
+ − 117
done
+ − 118
+ − 119
1028
+ − 120
lemma alpha1_eqvt:
+ − 121
shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
1031
+ − 122
apply (induct t s rule: alpha1.inducts)
+ − 123
apply (simp_all add:eqvts alpha1_inj)
1033
+ − 124
apply (erule exE)
+ − 125
apply (rule_tac x="pi \<bullet> pia" in exI)
+ − 126
apply (simp add: alpha_gen)
+ − 127
apply(erule conjE)+
+ − 128
apply(rule conjI)
+ − 129
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
+ − 130
apply(simp add: atom_eqvt eqvts)
+ − 131
apply(rule conjI)
+ − 132
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+ − 133
apply(simp add: eqvts atom_eqvt)
+ − 134
apply(simp add: permute_eqvt[symmetric])
+ − 135
apply (erule exE)
+ − 136
apply (rule_tac x="pi \<bullet> pia" in exI)
+ − 137
apply (simp add: alpha_gen)
+ − 138
apply(erule conjE)+
+ − 139
apply(rule conjI)
+ − 140
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
+ − 141
apply(simp add: atom_eqvt eqvts)
+ − 142
apply(rule conjI)
+ − 143
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+ − 144
apply(simp add: eqvts atom_eqvt)
+ − 145
apply(simp add: permute_eqvt[symmetric])
+ − 146
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
+ − 147
957
+ − 148
lemma alpha1_equivp: "equivp alpha1"
+ − 149
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
+ − 150
1028
+ − 151
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
+ − 152
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
+ − 153
1028
+ − 154
quotient_definition
+ − 155
"Vr1 :: name \<Rightarrow> trm1"
+ − 156
as
+ − 157
"rVr1"
+ − 158
1029
+ − 159
quotient_definition
+ − 160
"Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
+ − 161
as
+ − 162
"rAp1"
+ − 163
+ − 164
quotient_definition
+ − 165
"Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
+ − 166
as
+ − 167
"rLm1"
+ − 168
+ − 169
quotient_definition
+ − 170
"Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
+ − 171
as
+ − 172
"rLt1"
+ − 173
+ − 174
quotient_definition
+ − 175
"fv_trm1 :: trm1 \<Rightarrow> atom set"
+ − 176
as
+ − 177
"rfv_trm1"
+ − 178
+ − 179
lemma alpha_rfv1:
+ − 180
shows "t \<approx>1 s \<Longrightarrow> rfv_trm1 t = rfv_trm1 s"
+ − 181
apply(induct rule: alpha1.induct)
+ − 182
apply(simp_all add: alpha_gen.simps)
+ − 183
done
+ − 184
+ − 185
lemma [quot_respect]:
+ − 186
"(op = ===> alpha1) rVr1 rVr1"
+ − 187
"(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"
+ − 188
"(op = ===> alpha1 ===> alpha1) rLm1 rLm1"
+ − 189
"(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"
+ − 190
apply (auto intro: alpha1.intros)
+ − 191
apply(rule a3) apply (rule_tac x="0" in exI)
+ − 192
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
+ − 193
apply(rule a4) apply assumption apply (rule_tac x="0" in exI)
+ − 194
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
+ − 195
done
+ − 196
+ − 197
lemma [quot_respect]:
+ − 198
"(op = ===> alpha1 ===> alpha1) permute permute"
+ − 199
apply auto
+ − 200
apply (rule alpha1_eqvt)
+ − 201
apply simp
+ − 202
done
+ − 203
+ − 204
lemma [quot_respect]:
+ − 205
"(alpha1 ===> op =) rfv_trm1 rfv_trm1"
+ − 206
apply (simp add: alpha_rfv1)
+ − 207
done
+ − 208
+ − 209
lemma trm1_bp_induct: "
+ − 210
\<lbrakk>\<And>name. P1 (Vr1 name);
+ − 211
\<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);
+ − 212
\<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);
+ − 213
\<And>bp rtrm11 rtrm12.
+ − 214
\<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);
+ − 215
P2 BUnit; \<And>name. P2 (BVr name);
+ − 216
\<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>
+ − 217
\<Longrightarrow> P1 rtrma \<and> P2 bpa"
+ − 218
apply (lifting rtrm1_bp.induct)
+ − 219
done
+ − 220
+ − 221
lemma trm1_bp_inducts: "
+ − 222
\<lbrakk>\<And>name. P1 (Vr1 name);
+ − 223
\<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);
+ − 224
\<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);
+ − 225
\<And>bp rtrm11 rtrm12.
+ − 226
\<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);
+ − 227
P2 BUnit; \<And>name. P2 (BVr name);
+ − 228
\<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>
+ − 229
\<Longrightarrow> P1 rtrma"
+ − 230
"\<lbrakk>\<And>name. P1 (Vr1 name);
+ − 231
\<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);
+ − 232
\<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);
+ − 233
\<And>bp rtrm11 rtrm12.
+ − 234
\<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);
+ − 235
P2 BUnit; \<And>name. P2 (BVr name);
+ − 236
\<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>
+ − 237
\<Longrightarrow> P2 bpa"
+ − 238
by (lifting rtrm1_bp.inducts)
+ − 239
+ − 240
instantiation trm1 and bp :: pt
+ − 241
begin
+ − 242
+ − 243
quotient_definition
+ − 244
"permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
+ − 245
as
+ − 246
"permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
+ − 247
+ − 248
lemma permute_trm1 [simp]:
+ − 249
shows "pi \<bullet> Vr1 a = Vr1 (pi \<bullet> a)"
+ − 250
and "pi \<bullet> Ap1 t1 t2 = Ap1 (pi \<bullet> t1) (pi \<bullet> t2)"
+ − 251
and "pi \<bullet> Lm1 a t = Lm1 (pi \<bullet> a) (pi \<bullet> t)"
+ − 252
and "pi \<bullet> Lt1 b t s = Lt1 (pi \<bullet> b) (pi \<bullet> t) (pi \<bullet> s)"
+ − 253
apply -
+ − 254
apply(lifting permute_rtrm1_permute_bp.simps(1))
+ − 255
apply(lifting permute_rtrm1_permute_bp.simps(2))
+ − 256
apply(lifting permute_rtrm1_permute_bp.simps(3))
+ − 257
apply(lifting permute_rtrm1_permute_bp.simps(4))
+ − 258
done
+ − 259
instance
+ − 260
apply default
+ − 261
apply(induct_tac [!] x rule: trm1_bp_inducts(1))
+ − 262
apply(simp_all)
+ − 263
done
+ − 264
+ − 265
end
+ − 266
+ − 267
lemma fv_trm1:
+ − 268
"fv_trm1 (Vr1 x) = {atom x}"
+ − 269
"fv_trm1 (Ap1 t1 t2) = fv_trm1 t1 \<union> fv_trm1 t2"
+ − 270
"fv_trm1 (Lm1 x t) = fv_trm1 t - {atom x}"
+ − 271
"fv_trm1 (Lt1 bp t1 t2) = fv_trm1 t1 \<union> (fv_trm1 t2 - bv1 bp)"
+ − 272
apply -
+ − 273
apply (lifting rfv_trm1_rfv_bp.simps(1))
+ − 274
apply (lifting rfv_trm1_rfv_bp.simps(2))
+ − 275
apply (lifting rfv_trm1_rfv_bp.simps(3))
+ − 276
apply (lifting rfv_trm1_rfv_bp.simps(4))
+ − 277
done
+ − 278
+ − 279
lemma fv_trm1_eqvt:
+ − 280
shows "(p \<bullet> fv_trm1 t) = fv_trm1 (p \<bullet> t)"
+ − 281
apply(lifting rfv_trm1_eqvt)
+ − 282
done
+ − 283
+ − 284
lemma alpha1_INJ:
+ − 285
"(Vr1 a = Vr1 b) = (a = b)"
+ − 286
"(Ap1 t1 s1 = Ap1 t2 s2) = (t1 = t2 \<and> s1 = s2)"
+ − 287
"(Lm1 aa t = Lm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen (op =) fv_trm1 pi ({atom ab}, s)))"
+ − 288
"(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))))"
+ − 289
unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen])
+ − 290
done
+ − 291
1031
+ − 292
lemma lm1_supp_pre:
+ − 293
shows "(supp (atom x, t)) supports (Lm1 x t) "
+ − 294
apply(simp add: supports_def)
+ − 295
apply(fold fresh_def)
+ − 296
apply(simp add: fresh_Pair swap_fresh_fresh)
+ − 297
apply(clarify)
+ − 298
apply(subst swap_at_base_simps(3))
+ − 299
apply(simp_all add: fresh_atom)
+ − 300
done
+ − 301
+ − 302
lemma lt1_supp_pre:
+ − 303
shows "(supp (x, t, s)) supports (Lt1 t x s) "
+ − 304
apply(simp add: supports_def)
+ − 305
apply(fold fresh_def)
+ − 306
apply(simp add: fresh_Pair swap_fresh_fresh)
+ − 307
done
+ − 308
+ − 309
lemma bp_supp: "finite (supp (bp :: bp))"
+ − 310
apply (induct bp)
+ − 311
apply(simp_all add: supp_def)
+ − 312
apply (fold supp_def)
+ − 313
apply (simp add: supp_at_base)
+ − 314
apply(simp add: Collect_imp_eq)
+ − 315
apply(simp add: Collect_neg_eq[symmetric])
+ − 316
apply (fold supp_def)
+ − 317
apply (simp)
+ − 318
done
+ − 319
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 320
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
+ − 321
apply default
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 322
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
+ − 323
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
+ − 324
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
+ − 325
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
+ − 326
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
+ − 327
apply(simp add: Collect_imp_eq Collect_neg_eq)
1031
+ − 328
apply(rule supports_finite)
+ − 329
apply(rule lm1_supp_pre)
+ − 330
apply(simp add: supp_Pair supp_atom)
+ − 331
apply(rule supports_finite)
+ − 332
apply(rule lt1_supp_pre)
+ − 333
apply(simp add: supp_Pair supp_atom bp_supp)
+ − 334
done
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 335
1029
+ − 336
lemma supp_fv:
+ − 337
shows "supp t = fv_trm1 t"
+ − 338
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
+ − 339
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
+ − 340
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
+ − 341
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
+ − 342
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
+ − 343
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
+ − 344
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
+ − 345
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
+ − 346
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
+ − 347
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
+ − 348
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
+ − 349
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
+ − 350
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
+ − 351
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
+ − 352
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
+ − 353
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
+ − 354
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
+ − 355
apply(simp add: Abs_eq_iff)
1033
+ − 356
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
+ − 357
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
+ − 358
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
+ − 359
done
1029
+ − 360
1032
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 361
lemma trm1_supp:
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 362
"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
+ − 363
"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
+ − 364
"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
+ − 365
"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
+ − 366
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
+ − 367
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 368
lemma trm1_induct_strong:
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 369
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
+ − 370
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
+ − 371
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
+ − 372
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
+ − 373
shows "P a rtrma"
1035
+ − 374
sorry
1032
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 375
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 376
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
+ − 377
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 378
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
+ − 379
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
+ − 380
| 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
+ − 381
| 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
+ − 382
| 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
+ − 383
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
+ − 384
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
+ − 385
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 386
(* 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
+ − 387
primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 388
bv2
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 389
where
957
+ − 390
"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
+ − 391
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 392
(* 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
+ − 393
primrec
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 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
+ − 395
where
957
+ − 396
"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
+ − 397
| "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)"
957
+ − 398
| "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
+ − 399
| "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
+ − 400
| "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
+ − 401
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 402
(* needs to be stated by the package *)
957
+ − 403
instantiation
+ − 404
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
+ − 405
begin
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 406
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 407
primrec
957
+ − 408
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
+ − 409
where
957
+ − 410
"permute_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"
+ − 411
| "permute_trm2 pi (Ap2 t1 t2) = Ap2 (permute_trm2 pi t1) (permute_trm2 pi t2)"
+ − 412
| "permute_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (permute_trm2 pi t)"
+ − 413
| "permute_trm2 pi (Lt2 as t) = Lt2 (permute_assign pi as) (permute_trm2 pi t)"
+ − 414
| "permute_assign pi (As a t) = As (pi \<bullet> a) (permute_trm2 pi t)"
+ − 415
+ − 416
lemma pt_trm2_assign_zero:
+ − 417
fixes t::trm2
+ − 418
and b::assign
+ − 419
shows "0 \<bullet> t = t"
+ − 420
and "0 \<bullet> b = b"
+ − 421
apply(induct t and b rule: trm2_assign.inducts)
+ − 422
apply(simp_all)
+ − 423
done
+ − 424
+ − 425
lemma pt_trm2_assign_plus:
+ − 426
fixes t::trm2
+ − 427
and b::assign
+ − 428
shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ − 429
and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
+ − 430
apply(induct t and b rule: trm2_assign.inducts)
+ − 431
apply(simp_all)
+ − 432
done
+ − 433
+ − 434
instance
+ − 435
apply default
+ − 436
apply(simp_all add: pt_trm2_assign_zero pt_trm2_assign_plus)
+ − 437
done
+ − 438
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 439
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 440
end
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 441
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 442
inductive
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 443
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
+ − 444
where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 445
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
+ − 446
| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2"
957
+ − 447
| a3: "\<exists>pi. (fv_trm2 t - {atom a} = fv_trm2 s - {atom b} \<and>
+ − 448
(fv_trm2 t - {atom a})\<sharp>* pi \<and>
+ − 449
(pi \<bullet> t) \<approx>2 s \<and>
+ − 450
(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
+ − 451
\<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s"
957
+ − 452
| 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
+ − 453
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
+ − 454
(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
+ − 455
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
+ − 456
) \<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
+ − 457
957
+ − 458
lemma alpha2_equivp: "equivp alpha2"
+ − 459
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
+ − 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
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
+ − 462
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
+ − 463
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 464
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
+ − 465
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 466
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
+ − 467
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
+ − 468
| 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
+ − 469
| 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
+ − 470
| 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
+ − 471
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
+ − 472
ANil
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 473
| 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
+ − 474
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 475
(* 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
+ − 476
primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 477
bv3
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 478
where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 479
"bv3 ANil = {}"
957
+ − 480
| "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
+ − 481
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 482
primrec
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 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
+ − 484
where
957
+ − 485
"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
+ − 486
| "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)"
957
+ − 487
| "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
+ − 488
| "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
+ − 489
| "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
+ − 490
| "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
+ − 491
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 492
(* needs to be stated by the package *)
957
+ − 493
instantiation
+ − 494
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
+ − 495
begin
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 496
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 497
primrec
957
+ − 498
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
+ − 499
where
957
+ − 500
"permute_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)"
+ − 501
| "permute_trm3 pi (Ap3 t1 t2) = Ap3 (permute_trm3 pi t1) (permute_trm3 pi t2)"
+ − 502
| "permute_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (permute_trm3 pi t)"
+ − 503
| "permute_trm3 pi (Lt3 as t) = Lt3 (permute_assigns pi as) (permute_trm3 pi t)"
+ − 504
| "permute_assigns pi (ANil) = ANil"
+ − 505
| "permute_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (permute_trm3 pi t) (permute_assigns pi as)"
+ − 506
+ − 507
lemma pt_trm3_assigns_zero:
+ − 508
fixes t::trm3
+ − 509
and b::assigns
+ − 510
shows "0 \<bullet> t = t"
+ − 511
and "0 \<bullet> b = b"
+ − 512
apply(induct t and b rule: trm3_assigns.inducts)
+ − 513
apply(simp_all)
+ − 514
done
+ − 515
+ − 516
lemma pt_trm3_assigns_plus:
+ − 517
fixes t::trm3
+ − 518
and b::assigns
+ − 519
shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ − 520
and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
+ − 521
apply(induct t and b rule: trm3_assigns.inducts)
+ − 522
apply(simp_all)
+ − 523
done
+ − 524
+ − 525
instance
+ − 526
apply default
+ − 527
apply(simp_all add: pt_trm3_assigns_zero pt_trm3_assigns_plus)
+ − 528
done
+ − 529
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 530
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 531
end
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 532
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 533
inductive
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 534
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
+ − 535
where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 536
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
+ − 537
| a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
957
+ − 538
| a3: "\<exists>pi. (fv_trm3 t - {atom a} = fv_trm3 s - {atom b} \<and>
+ − 539
(fv_trm3 t - {atom a})\<sharp>* pi \<and>
+ − 540
(pi \<bullet> t) \<approx>3 s \<and>
+ − 541
(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
+ − 542
\<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
957
+ − 543
| 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
+ − 544
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
+ − 545
(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
+ − 546
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
+ − 547
) \<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
+ − 548
957
+ − 549
lemma alpha3_equivp: "equivp alpha3"
+ − 550
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
+ − 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
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
+ − 553
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
+ − 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
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 556
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
+ − 557
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 558
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
+ − 559
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
+ − 560
| 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
+ − 561
| 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
+ − 562
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 563
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
+ − 564
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 565
primrec
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 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
+ − 567
where
957
+ − 568
"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
+ − 569
| "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
957
+ − 570
| "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
+ − 571
| "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
+ − 572
| "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
+ − 573
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 574
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 575
(* 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
+ − 576
(* there cannot be a clause for lists, as *)
957
+ − 577
(* permuteutations are already defined in Nominal (also functions, options, and so on) *)
+ − 578
instantiation
+ − 579
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
+ − 580
begin
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 581
957
+ − 582
(* 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
+ − 583
primrec
963
+ − 584
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
+ − 585
where
957
+ − 586
"permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)"
963
+ − 587
| "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute_trm4_list pi ts)"
957
+ − 588
| "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)"
963
+ − 589
| "permute_trm4_list pi ([]) = []"
+ − 590
| "permute_trm4_list pi (t#ts) = (permute_trm4 pi t) # (permute_trm4_list pi ts)"
+ − 591
+ − 592
lemma pt_trm4_list_zero:
+ − 593
fixes t::trm4
+ − 594
and ts::"trm4 list"
+ − 595
shows "0 \<bullet> t = t"
+ − 596
and "permute_trm4_list 0 ts = ts"
+ − 597
apply(induct t and ts rule: trm4.inducts)
+ − 598
apply(simp_all)
+ − 599
done
+ − 600
+ − 601
lemma pt_trm4_list_plus:
+ − 602
fixes t::trm4
+ − 603
and ts::"trm4 list"
+ − 604
shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ − 605
and "(permute_trm4_list (p + q) ts) = permute_trm4_list p (permute_trm4_list q ts)"
+ − 606
apply(induct t and ts rule: trm4.inducts)
+ − 607
apply(simp_all)
+ − 608
done
+ − 609
+ − 610
+ − 611
instance
+ − 612
apply(default)
+ − 613
apply(simp_all add: pt_trm4_list_zero pt_trm4_list_plus)
+ − 614
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
+ − 615
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 616
end
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 617
963
+ − 618
(* "repairing" of the permute function *)
+ − 619
lemma repaired:
+ − 620
fixes ts::"trm4 list"
+ − 621
shows "permute_trm4_list p ts = p \<bullet> ts"
+ − 622
apply(induct ts)
+ − 623
apply(simp_all)
+ − 624
done
+ − 625
976
+ − 626
thm permute_trm4_permute_trm4_list.simps
963
+ − 627
thm permute_trm4_permute_trm4_list.simps[simplified repaired]
+ − 628
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 629
inductive
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 630
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
+ − 631
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
+ − 632
where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 633
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
+ − 634
| a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"
963
+ − 635
| a4: "\<exists>pi. (fv_trm4 t - {atom a} = fv_trm4 s - {atom b} \<and>
+ − 636
(fv_trm4 t - {atom a})\<sharp>* pi \<and>
+ − 637
(pi \<bullet> t) \<approx>4 s \<and>
+ − 638
(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
+ − 639
\<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
+ − 640
| 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
+ − 641
| 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
+ − 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
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
+ − 644
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
+ − 645
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 646
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
+ − 647
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
+ − 648
qtrm4list = "trm4 list" / alpha4list
1042
+ − 649
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
+ − 650
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 651
1035
+ − 652
datatype rtrm5 =
+ − 653
rVr5 "name"
+ − 654
| rAp5 "rtrm5" "rtrm5"
+ − 655
| rLt5 "rlts" "rtrm5"
+ − 656
and rlts =
+ − 657
rLnil
+ − 658
| rLcons "name" "rtrm5" "rlts"
+ − 659
+ − 660
primrec
+ − 661
bv5
+ − 662
where
+ − 663
"bv5 rLnil = {}"
+ − 664
| "bv5 (rLcons n t ltl) = {atom n} \<union> (bv5 ltl)"
+ − 665
+ − 666
primrec
+ − 667
rfv_trm5 and rfv_lts
+ − 668
where
+ − 669
"rfv_trm5 (rVr5 n) = {atom n}"
+ − 670
| "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)"
+ − 671
| "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - bv5 lts) \<union> (rfv_lts lts - bv5 lts)"
+ − 672
| "rfv_lts (rLnil) = {}"
+ − 673
| "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)"
+ − 674
+ − 675
instantiation
+ − 676
rtrm5 and rlts :: pt
+ − 677
begin
+ − 678
+ − 679
primrec
+ − 680
permute_rtrm5 and permute_rlts
+ − 681
where
+ − 682
"permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)"
+ − 683
| "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)"
+ − 684
| "permute_rtrm5 pi (rLt5 as t) = rLt5 (permute_rlts pi as) (permute_rtrm5 pi t)"
+ − 685
| "permute_rlts pi (rLnil) = rLnil"
+ − 686
| "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)"
+ − 687
+ − 688
lemma pt_rtrm5_zero:
+ − 689
fixes t::rtrm5
+ − 690
and l::rlts
+ − 691
shows "0 \<bullet> t = t"
+ − 692
and "0 \<bullet> l = l"
+ − 693
apply(induct t and l rule: rtrm5_rlts.inducts)
+ − 694
apply(simp_all)
+ − 695
done
+ − 696
+ − 697
lemma pt_rtrm5_plus:
+ − 698
fixes t::rtrm5
+ − 699
and l::rlts
+ − 700
shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ − 701
and "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)"
+ − 702
apply(induct t and l rule: rtrm5_rlts.inducts)
+ − 703
apply(simp_all)
+ − 704
done
+ − 705
+ − 706
instance
+ − 707
apply default
+ − 708
apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)
+ − 709
done
+ − 710
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 711
end
1035
+ − 712
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 713
inductive
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 714
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
+ − 715
and
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 716
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
+ − 717
where
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 718
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
+ − 719
| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 720
| a3: "\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and>
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 721
(bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and>
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 722
(pi \<bullet> (bv5 l1) = bv5 l2))
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 723
\<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
+ − 724
| a4: "rLnil \<approx>l rLnil"
1040
+ − 725
| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
+ − 726
+ − 727
print_theorems
1035
+ − 728
1040
+ − 729
lemma alpha5_inj:
+ − 730
"((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
+ − 731
"(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
+ − 732
"(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and>
+ − 733
(bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and>
+ − 734
(pi \<bullet> (bv5 l1) = bv5 l2)))"
+ − 735
"rLnil \<approx>l rLnil"
+ − 736
"(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2 \<and> n1 = n2)"
+ − 737
apply -
+ − 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 alpha5.cases)
+ − 747
apply (simp_all add: alpha5_alphalts.intros)
+ − 748
apply rule
+ − 749
apply (erule alphalts.cases)
+ − 750
apply (simp_all add: alpha5_alphalts.intros)
+ − 751
done
+ − 752
+ − 753
lemma alpha5_equivps:
+ − 754
shows "equivp alpha5"
+ − 755
and "equivp alphalts"
+ − 756
sorry
+ − 757
+ − 758
quotient_type
+ − 759
trm5 = rtrm5 / alpha5
+ − 760
and
+ − 761
lts = rlts / alphalts
+ − 762
by (auto intro: alpha5_equivps)
+ − 763
+ − 764
1035
+ − 765
end