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
1171
+ − 2
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm"
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
1171
+ − 42
setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.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
+ − 43
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 44
inductive
1028
+ − 45
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
+ − 46
where
1028
+ − 47
a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)"
+ − 48
| a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2"
+ − 49
| a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"
+ − 50
| 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"
+ − 51
1029
+ − 52
lemma alpha1_inj:
1028
+ − 53
"(rVr1 a \<approx>1 rVr1 b) = (a = b)"
+ − 54
"(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"
+ − 55
"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s)))"
+ − 56
"(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))))"
+ − 57
apply -
+ − 58
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 59
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 60
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 61
apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+ − 62
done
+ − 63
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 64
(* 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
+ − 65
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
+ − 66
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
+ − 67
apply (induct x)
1043
+ − 68
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
+ − 69
done
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 70
1031
+ − 71
lemma rfv_trm1_eqvt[eqvt]:
+ − 72
shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
+ − 73
apply (induct t)
1043
+ − 74
apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)
1031
+ − 75
done
+ − 76
+ − 77
1028
+ − 78
lemma alpha1_eqvt:
+ − 79
shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
1031
+ − 80
apply (induct t s rule: alpha1.inducts)
+ − 81
apply (simp_all add:eqvts alpha1_inj)
1033
+ − 82
apply (erule exE)
+ − 83
apply (rule_tac x="pi \<bullet> pia" in exI)
+ − 84
apply (simp add: alpha_gen)
+ − 85
apply(erule conjE)+
+ − 86
apply(rule conjI)
+ − 87
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
1043
+ − 88
apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt rfv_trm1_eqvt)
1033
+ − 89
apply(rule conjI)
+ − 90
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
1043
+ − 91
apply(simp add: atom_eqvt Diff_eqvt rfv_trm1_eqvt insert_eqvt empty_eqvt)
1033
+ − 92
apply(simp add: permute_eqvt[symmetric])
+ − 93
apply (erule exE)
+ − 94
apply (rule_tac x="pi \<bullet> pia" in exI)
+ − 95
apply (simp add: alpha_gen)
+ − 96
apply(erule conjE)+
+ − 97
apply(rule conjI)
+ − 98
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
1043
+ − 99
apply(simp add: rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
1033
+ − 100
apply(rule conjI)
+ − 101
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
1043
+ − 102
apply(simp add: atom_eqvt rfv_trm1_eqvt Diff_eqvt bv1_eqvt)
1033
+ − 103
apply(simp add: permute_eqvt[symmetric])
+ − 104
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
+ − 105
957
+ − 106
lemma alpha1_equivp: "equivp alpha1"
+ − 107
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
+ − 108
1028
+ − 109
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
+ − 110
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
+ − 111
1028
+ − 112
quotient_definition
+ − 113
"Vr1 :: name \<Rightarrow> trm1"
1139
+ − 114
is
1028
+ − 115
"rVr1"
+ − 116
1029
+ − 117
quotient_definition
+ − 118
"Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
1139
+ − 119
is
1029
+ − 120
"rAp1"
+ − 121
+ − 122
quotient_definition
+ − 123
"Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
1139
+ − 124
is
1029
+ − 125
"rLm1"
+ − 126
+ − 127
quotient_definition
+ − 128
"Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
1139
+ − 129
is
1029
+ − 130
"rLt1"
+ − 131
+ − 132
quotient_definition
+ − 133
"fv_trm1 :: trm1 \<Rightarrow> atom set"
1139
+ − 134
is
1029
+ − 135
"rfv_trm1"
+ − 136
+ − 137
lemma alpha_rfv1:
+ − 138
shows "t \<approx>1 s \<Longrightarrow> rfv_trm1 t = rfv_trm1 s"
+ − 139
apply(induct rule: alpha1.induct)
+ − 140
apply(simp_all add: alpha_gen.simps)
+ − 141
done
+ − 142
+ − 143
lemma [quot_respect]:
+ − 144
"(op = ===> alpha1) rVr1 rVr1"
+ − 145
"(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"
+ − 146
"(op = ===> alpha1 ===> alpha1) rLm1 rLm1"
+ − 147
"(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"
+ − 148
apply (auto intro: alpha1.intros)
+ − 149
apply(rule a3) apply (rule_tac x="0" in exI)
+ − 150
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
+ − 151
apply(rule a4) apply assumption apply (rule_tac x="0" in exI)
+ − 152
apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
+ − 153
done
+ − 154
+ − 155
lemma [quot_respect]:
+ − 156
"(op = ===> alpha1 ===> alpha1) permute permute"
+ − 157
apply auto
+ − 158
apply (rule alpha1_eqvt)
+ − 159
apply simp
+ − 160
done
+ − 161
+ − 162
lemma [quot_respect]:
+ − 163
"(alpha1 ===> op =) rfv_trm1 rfv_trm1"
+ − 164
apply (simp add: alpha_rfv1)
+ − 165
done
+ − 166
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 167
lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 168
lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
1029
+ − 169
+ − 170
instantiation trm1 and bp :: pt
+ − 171
begin
+ − 172
+ − 173
quotient_definition
+ − 174
"permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
1139
+ − 175
is
1029
+ − 176
"permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
+ − 177
1083
+ − 178
lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
+ − 179
1029
+ − 180
instance
+ − 181
apply default
+ − 182
apply(induct_tac [!] x rule: trm1_bp_inducts(1))
1083
+ − 183
apply(simp_all)
1029
+ − 184
done
+ − 185
+ − 186
end
+ − 187
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 188
lemmas fv_trm1 = rfv_trm1_rfv_bp.simps[quot_lifted]
1029
+ − 189
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 190
lemmas fv_trm1_eqvt = rfv_trm1_eqvt[quot_lifted]
1029
+ − 191
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 192
lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
1029
+ − 193
1031
+ − 194
lemma lm1_supp_pre:
+ − 195
shows "(supp (atom x, t)) supports (Lm1 x t) "
+ − 196
apply(simp add: supports_def)
+ − 197
apply(fold fresh_def)
+ − 198
apply(simp add: fresh_Pair swap_fresh_fresh)
+ − 199
apply(clarify)
+ − 200
apply(subst swap_at_base_simps(3))
+ − 201
apply(simp_all add: fresh_atom)
+ − 202
done
+ − 203
+ − 204
lemma lt1_supp_pre:
+ − 205
shows "(supp (x, t, s)) supports (Lt1 t x s) "
+ − 206
apply(simp add: supports_def)
+ − 207
apply(fold fresh_def)
+ − 208
apply(simp add: fresh_Pair swap_fresh_fresh)
+ − 209
done
+ − 210
+ − 211
lemma bp_supp: "finite (supp (bp :: bp))"
+ − 212
apply (induct bp)
+ − 213
apply(simp_all add: supp_def)
+ − 214
apply (fold supp_def)
+ − 215
apply (simp add: supp_at_base)
+ − 216
apply(simp add: Collect_imp_eq)
+ − 217
apply(simp add: Collect_neg_eq[symmetric])
+ − 218
apply (fold supp_def)
+ − 219
apply (simp)
+ − 220
done
+ − 221
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 222
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
+ − 223
apply default
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 224
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
+ − 225
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
+ − 226
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
+ − 227
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
+ − 228
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
+ − 229
apply(simp add: Collect_imp_eq Collect_neg_eq)
1031
+ − 230
apply(rule supports_finite)
+ − 231
apply(rule lm1_supp_pre)
+ − 232
apply(simp add: supp_Pair supp_atom)
+ − 233
apply(rule supports_finite)
+ − 234
apply(rule lt1_supp_pre)
+ − 235
apply(simp add: supp_Pair supp_atom bp_supp)
+ − 236
done
1030
07f97267a392
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 237
1029
+ − 238
lemma supp_fv:
+ − 239
shows "supp t = fv_trm1 t"
+ − 240
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
+ − 241
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
+ − 242
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
+ − 243
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
+ − 244
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
+ − 245
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
+ − 246
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
+ − 247
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
+ − 248
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
+ − 249
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
+ − 250
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
+ − 251
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
+ − 252
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
+ − 253
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
+ − 254
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
+ − 255
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
+ − 256
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
+ − 257
apply(simp add: Abs_eq_iff)
1033
+ − 258
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
+ − 259
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
+ − 260
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
+ − 261
done
1029
+ − 262
1032
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 263
lemma trm1_supp:
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 264
"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
+ − 265
"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
+ − 266
"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
+ − 267
"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
+ − 268
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
+ − 269
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 270
lemma trm1_induct_strong:
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 271
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
+ − 272
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
+ − 273
and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
1179
+ − 274
and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
1032
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 275
shows "P a rtrma"
1035
+ − 276
sorry
1032
135bf399c036
The trm1_support lemma explicitly and stated a strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 277
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 278
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
+ − 279
1091
+ − 280
datatype rtrm2 =
+ − 281
rVr2 "name"
+ − 282
| rAp2 "rtrm2" "rtrm2"
1093
+ − 283
| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"
+ − 284
| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"
1091
+ − 285
and rassign =
+ − 286
rAs "name" "rtrm2"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 287
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 288
(* 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
+ − 289
primrec
1091
+ − 290
rbv2
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 291
where
1091
+ − 292
"rbv2 (rAs 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
+ − 293
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 294
(* 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
+ − 295
primrec
1091
+ − 296
fv_rtrm2 and fv_rassign
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 297
where
1091
+ − 298
"fv_rtrm2 (rVr2 x) = {atom x}"
+ − 299
| "fv_rtrm2 (rAp2 t1 t2) = (fv_rtrm2 t1) \<union> (fv_rtrm2 t2)"
+ − 300
| "fv_rtrm2 (rLm2 x t) = (fv_rtrm2 t) - {atom x}"
+ − 301
| "fv_rtrm2 (rLt2 as t) = (fv_rtrm2 t - rbv2 as) \<union> (fv_rassign as)"
+ − 302
| "fv_rassign (rAs x t) = fv_rtrm2 t"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 303
1171
+ − 304
setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 305
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 306
inductive
1091
+ − 307
alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
+ − 308
and
+ − 309
alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [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
+ − 310
where
1091
+ − 311
a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)"
+ − 312
| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2"
+ − 313
| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s"
1092
+ − 314
| a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s));
+ − 315
\<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk>
+ − 316
\<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"
+ − 317
| a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 318
1091
+ − 319
lemma alpha2_equivp:
+ − 320
"equivp alpha2"
+ − 321
"equivp alpha2a"
957
+ − 322
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
+ − 323
1091
+ − 324
quotient_type
+ − 325
trm2 = rtrm2 / alpha2
+ − 326
and
+ − 327
assign = rassign / alpha2a
+ − 328
by (auto intro: alpha2_equivp)
+ − 329
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 330
1092
+ − 331
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 332
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
+ − 333
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 334
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
+ − 335
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
+ − 336
| Ap3 "trm3" "trm3"
1093
+ − 337
| Lm3 "name" "trm3" --"bind (name) in (trm3)"
+ − 338
| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 339
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
+ − 340
ANil
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 341
| 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
+ − 342
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 343
(* 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
+ − 344
primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 345
bv3
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 346
where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 347
"bv3 ANil = {}"
957
+ − 348
| "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
+ − 349
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 350
primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 351
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
+ − 352
where
957
+ − 353
"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
+ − 354
| "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)"
957
+ − 355
| "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
+ − 356
| "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
+ − 357
| "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
+ − 358
| "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
+ − 359
1171
+ − 360
setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.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
+ − 361
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 362
inductive
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 363
alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)
1092
+ − 364
and
+ − 365
alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [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
+ − 366
where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 367
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
+ − 368
| a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
1092
+ − 369
| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
+ − 370
| a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s));
+ − 371
\<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk>
+ − 372
\<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s"
+ − 373
| a5: "ANil \<approx>3a ANil"
+ − 374
| a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 375
1092
+ − 376
lemma alpha3_equivp:
+ − 377
"equivp alpha3"
+ − 378
"equivp alpha3a"
957
+ − 379
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
+ − 380
1092
+ − 381
quotient_type
+ − 382
qtrm3 = trm3 / alpha3
+ − 383
and
+ − 384
qassigns = assigns / alpha3a
+ − 385
by (auto intro: alpha3_equivp)
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 386
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 387
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 388
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
+ − 389
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 390
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
+ − 391
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
+ − 392
| Ap4 "trm4" "trm4 list"
1093
+ − 393
| Lm4 "name" "trm4" --"bind (name) in (trm)"
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
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 395
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
+ − 396
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 397
primrec
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 398
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
+ − 399
where
957
+ − 400
"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
+ − 401
| "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
957
+ − 402
| "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
+ − 403
| "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
+ − 404
| "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
+ − 405
1171
+ − 406
(* there cannot be a clause for lists, as *)
1092
+ − 407
(* permutations are already defined in Nominal (also functions, options, and so on) *)
1171
+ − 408
setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *}
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
963
+ − 410
(* "repairing" of the permute function *)
+ − 411
lemma repaired:
+ − 412
fixes ts::"trm4 list"
+ − 413
shows "permute_trm4_list p ts = p \<bullet> ts"
+ − 414
apply(induct ts)
+ − 415
apply(simp_all)
+ − 416
done
+ − 417
976
+ − 418
thm permute_trm4_permute_trm4_list.simps
963
+ − 419
thm permute_trm4_permute_trm4_list.simps[simplified repaired]
+ − 420
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 421
inductive
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 422
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
+ − 423
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
+ − 424
where
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 425
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
+ − 426
| a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"
1092
+ − 427
| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"
950
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 428
| 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
+ − 429
| 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
+ − 430
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 431
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
+ − 432
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
+ − 433
98764f25f012
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 434
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
+ − 435
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
+ − 436
qtrm4list = "trm4 list" / alpha4list
1042
+ − 437
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
+ − 438
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 439
1035
+ − 440
datatype rtrm5 =
+ − 441
rVr5 "name"
+ − 442
| rAp5 "rtrm5" "rtrm5"
1093
+ − 443
| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
1035
+ − 444
and rlts =
+ − 445
rLnil
+ − 446
| rLcons "name" "rtrm5" "rlts"
+ − 447
+ − 448
primrec
1050
+ − 449
rbv5
1035
+ − 450
where
1050
+ − 451
"rbv5 rLnil = {}"
+ − 452
| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
1035
+ − 453
+ − 454
primrec
+ − 455
rfv_trm5 and rfv_lts
+ − 456
where
+ − 457
"rfv_trm5 (rVr5 n) = {atom n}"
+ − 458
| "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)"
1050
+ − 459
| "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - rbv5 lts) \<union> (rfv_lts lts - rbv5 lts)"
1035
+ − 460
| "rfv_lts (rLnil) = {}"
+ − 461
| "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)"
+ − 462
1171
+ − 463
setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
+ − 464
print_theorems
1035
+ − 465
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 466
inductive
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 467
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
+ − 468
and
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 469
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
+ − 470
where
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 471
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
+ − 472
| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"
1057
+ − 473
| a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2));
+ − 474
\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2))\<rbrakk>
1036
aaac8274f08c
The alpha-equivalence relation for let-rec. Not sure if correct...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 475
\<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
+ − 476
| a4: "rLnil \<approx>l rLnil"
1040
+ − 477
| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"
+ − 478
+ − 479
print_theorems
1035
+ − 480
1040
+ − 481
lemma alpha5_inj:
+ − 482
"((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"
+ − 483
"(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"
1057
+ − 484
"(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (rbv5 l2, t2))) \<and>
+ − 485
(\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts rfv_lts pi (rbv5 l2, l2))))"
1040
+ − 486
"rLnil \<approx>l rLnil"
1057
+ − 487
"(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"
1040
+ − 488
apply -
+ − 489
apply (simp_all add: alpha5_alphalts.intros)
+ − 490
apply rule
+ − 491
apply (erule alpha5.cases)
+ − 492
apply (simp_all add: alpha5_alphalts.intros)
+ − 493
apply rule
+ − 494
apply (erule alpha5.cases)
+ − 495
apply (simp_all add: alpha5_alphalts.intros)
+ − 496
apply rule
+ − 497
apply (erule alpha5.cases)
+ − 498
apply (simp_all add: alpha5_alphalts.intros)
+ − 499
apply rule
+ − 500
apply (erule alphalts.cases)
+ − 501
apply (simp_all add: alpha5_alphalts.intros)
+ − 502
done
+ − 503
+ − 504
lemma alpha5_equivps:
+ − 505
shows "equivp alpha5"
+ − 506
and "equivp alphalts"
+ − 507
sorry
+ − 508
+ − 509
quotient_type
+ − 510
trm5 = rtrm5 / alpha5
+ − 511
and
+ − 512
lts = rlts / alphalts
+ − 513
by (auto intro: alpha5_equivps)
+ − 514
1046
+ − 515
quotient_definition
+ − 516
"Vr5 :: name \<Rightarrow> trm5"
1139
+ − 517
is
1046
+ − 518
"rVr5"
+ − 519
+ − 520
quotient_definition
+ − 521
"Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
1139
+ − 522
is
1046
+ − 523
"rAp5"
+ − 524
+ − 525
quotient_definition
+ − 526
"Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
1139
+ − 527
is
1046
+ − 528
"rLt5"
+ − 529
+ − 530
quotient_definition
+ − 531
"Lnil :: lts"
1139
+ − 532
is
1046
+ − 533
"rLnil"
+ − 534
+ − 535
quotient_definition
+ − 536
"Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
1139
+ − 537
is
1046
+ − 538
"rLcons"
+ − 539
+ − 540
quotient_definition
+ − 541
"fv_trm5 :: trm5 \<Rightarrow> atom set"
1139
+ − 542
is
1046
+ − 543
"rfv_trm5"
+ − 544
+ − 545
quotient_definition
1050
+ − 546
"fv_lts :: lts \<Rightarrow> atom set"
1139
+ − 547
is
1046
+ − 548
"rfv_lts"
+ − 549
1050
+ − 550
quotient_definition
+ − 551
"bv5 :: lts \<Rightarrow> atom set"
1139
+ − 552
is
1050
+ − 553
"rbv5"
+ − 554
1092
+ − 555
lemma rbv5_eqvt:
+ − 556
"pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
+ − 557
sorry
+ − 558
+ − 559
lemma rfv_trm5_eqvt:
+ − 560
"pi \<bullet> (rfv_trm5 x) = rfv_trm5 (pi \<bullet> x)"
+ − 561
sorry
+ − 562
+ − 563
lemma rfv_lts_eqvt:
+ − 564
"pi \<bullet> (rfv_lts x) = rfv_lts (pi \<bullet> x)"
+ − 565
sorry
+ − 566
+ − 567
lemma alpha5_eqvt:
+ − 568
"xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
+ − 569
"xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
+ − 570
apply(induct rule: alpha5_alphalts.inducts)
+ − 571
apply (simp_all add: alpha5_inj)
+ − 572
apply (erule exE)+
+ − 573
apply(unfold alpha_gen)
+ − 574
apply (erule conjE)+
+ − 575
apply (rule conjI)
+ − 576
apply (rule_tac x="x \<bullet> pi" in exI)
+ − 577
apply (rule conjI)
+ − 578
apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
+ − 579
apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_trm5_eqvt)
+ − 580
apply(rule conjI)
+ − 581
apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
+ − 582
apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_trm5_eqvt)
+ − 583
apply (subst permute_eqvt[symmetric])
+ − 584
apply (simp)
+ − 585
apply (rule_tac x="x \<bullet> pia" in exI)
+ − 586
apply (rule conjI)
+ − 587
apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1])
+ − 588
apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_lts_eqvt)
+ − 589
apply(rule conjI)
+ − 590
apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1])
+ − 591
apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt rfv_lts_eqvt)
+ − 592
apply (subst permute_eqvt[symmetric])
+ − 593
apply (simp)
+ − 594
done
+ − 595
1050
+ − 596
lemma alpha5_rfv:
+ − 597
"(t \<approx>5 s \<Longrightarrow> rfv_trm5 t = rfv_trm5 s)"
+ − 598
"(l \<approx>l m \<Longrightarrow> rfv_lts l = rfv_lts m)"
+ − 599
apply(induct rule: alpha5_alphalts.inducts)
+ − 600
apply(simp_all add: alpha_gen)
+ − 601
done
+ − 602
1053
+ − 603
lemma bv_list_rsp:
1055
+ − 604
shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
1092
+ − 605
apply(induct rule: alpha5_alphalts.inducts(2))
+ − 606
apply(simp_all)
+ − 607
done
1053
+ − 608
1092
+ − 609
lemma [quot_respect]:
+ − 610
"(alphalts ===> op =) rfv_lts rfv_lts"
+ − 611
"(alpha5 ===> op =) rfv_trm5 rfv_trm5"
+ − 612
"(alphalts ===> op =) rbv5 rbv5"
+ − 613
"(op = ===> alpha5) rVr5 rVr5"
+ − 614
"(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5"
+ − 615
"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+ − 616
"(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5"
+ − 617
"(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons"
+ − 618
"(op = ===> alpha5 ===> alpha5) permute permute"
+ − 619
"(op = ===> alphalts ===> alphalts) permute permute"
+ − 620
apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
+ − 621
apply (auto)
+ − 622
apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+ − 623
apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+ − 624
apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+ − 625
apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+ − 626
done
1057
+ − 627
1092
+ − 628
lemma
1053
+ − 629
shows "(alphalts ===> op =) rbv5 rbv5"
+ − 630
by (simp add: bv_list_rsp)
+ − 631
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 632
lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 633
1050
+ − 634
instantiation trm5 and lts :: pt
+ − 635
begin
+ − 636
+ − 637
quotient_definition
+ − 638
"permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
1139
+ − 639
is
1050
+ − 640
"permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
+ − 641
+ − 642
quotient_definition
+ − 643
"permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
1139
+ − 644
is
1050
+ − 645
"permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
+ − 646
+ − 647
lemma trm5_lts_zero:
+ − 648
"0 \<bullet> (x\<Colon>trm5) = x"
+ − 649
"0 \<bullet> (y\<Colon>lts) = y"
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 650
apply(induct x and y rule: trm5_lts_inducts)
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 651
apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 652
done
1050
+ − 653
+ − 654
lemma trm5_lts_plus:
+ − 655
"(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
+ − 656
"(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 657
apply(induct x and y rule: trm5_lts_inducts)
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 658
apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 659
done
1050
+ − 660
+ − 661
instance
+ − 662
apply default
+ − 663
apply (simp_all add: trm5_lts_zero trm5_lts_plus)
+ − 664
done
1040
+ − 665
1035
+ − 666
end
1050
+ − 667
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 668
lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 669
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 670
lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
1050
+ − 671
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 672
lemmas bv5[simp] = rbv5.simps[quot_lifted]
1050
+ − 673
1073
53350d409473
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 674
lemmas fv_trm5_lts[simp] = rfv_trm5_rfv_lts.simps[quot_lifted]
1050
+ − 675
+ − 676
lemma lets_ok:
+ − 677
"(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
+ − 678
apply (subst alpha5_INJ)
1057
+ − 679
apply (rule conjI)
+ − 680
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 681
apply (simp only: alpha_gen)
+ − 682
apply (simp add: permute_trm5_lts fresh_star_def)
1050
+ − 683
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 684
apply (simp only: alpha_gen)
1052
+ − 685
apply (simp add: permute_trm5_lts fresh_star_def)
+ − 686
done
1050
+ − 687
1058
+ − 688
lemma lets_ok2:
+ − 689
"(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =
+ − 690
(Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+ − 691
apply (subst alpha5_INJ)
+ − 692
apply (rule conjI)
+ − 693
apply (rule_tac x="0 :: perm" in exI)
+ − 694
apply (simp only: alpha_gen)
+ − 695
apply (simp add: permute_trm5_lts fresh_star_def)
+ − 696
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 697
apply (simp only: alpha_gen)
+ − 698
apply (simp add: permute_trm5_lts fresh_star_def)
+ − 699
done
+ − 700
+ − 701
1057
+ − 702
lemma lets_not_ok1:
1056
+ − 703
"x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
1057
+ − 704
(Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+ − 705
apply (subst alpha5_INJ(3))
+ − 706
apply(clarify)
1056
+ − 707
apply (simp add: alpha_gen)
+ − 708
apply (simp add: permute_trm5_lts fresh_star_def)
1057
+ − 709
apply (simp add: alpha5_INJ(5))
+ − 710
apply(clarify)
+ − 711
apply (simp add: alpha5_INJ(2))
+ − 712
apply (simp only: alpha5_INJ(1))
1056
+ − 713
done
+ − 714
1058
+ − 715
lemma distinct_helper:
+ − 716
shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"
+ − 717
apply auto
+ − 718
apply (erule alpha5.cases)
+ − 719
apply (simp_all only: rtrm5.distinct)
+ − 720
done
1057
+ − 721
1058
+ − 722
lemma distinct_helper2:
+ − 723
shows "(Vr5 x) \<noteq> (Ap5 y z)"
+ − 724
by (lifting distinct_helper)
1057
+ − 725
1058
+ − 726
lemma lets_nok:
+ − 727
"x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ − 728
(Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
+ − 729
(Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
+ − 730
apply (subst alpha5_INJ)
+ − 731
apply (simp only: alpha_gen permute_trm5_lts fresh_star_def)
+ − 732
apply (subst alpha5_INJ(5))
+ − 733
apply (subst alpha5_INJ(5))
+ − 734
apply (simp add: distinct_helper2)
+ − 735
done
1057
+ − 736
1103
+ − 737
1105
+ − 738
(* example with a bn function defined over the type itself *)
1103
+ − 739
datatype rtrm6 =
+ − 740
rVr6 "name"
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 741
| rLm6 "name" "rtrm6"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 742
| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
1103
+ − 743
+ − 744
primrec
+ − 745
rbv6
+ − 746
where
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 747
"rbv6 (rVr6 n) = {}"
1117
+ − 748
| "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 749
| "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
1103
+ − 750
+ − 751
primrec
+ − 752
rfv_trm6
+ − 753
where
+ − 754
"rfv_trm6 (rVr6 n) = {atom n}"
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 755
| "rfv_trm6 (rLm6 n t) = (rfv_trm6 t) - {atom n}"
1119
+ − 756
| "rfv_trm6 (rLt6 l r) = (rfv_trm6 r - rbv6 l) \<union> rfv_trm6 l"
1103
+ − 757
1171
+ − 758
setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *}
+ − 759
print_theorems
1103
+ − 760
+ − 761
inductive
+ − 762
alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100)
+ − 763
where
+ − 764
a1: "a = b \<Longrightarrow> (rVr6 a) \<approx>6 (rVr6 b)"
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 765
| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha6 rfv_trm6 pi ({atom b}, s))) \<Longrightarrow> rLm6 a t \<approx>6 rLm6 b s"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 766
| a3: "(\<exists>pi. (((rbv6 t1), s1) \<approx>gen alpha6 rfv_trm6 pi ((rbv6 t2), s2))) \<Longrightarrow> rLt6 t1 s1 \<approx>6 rLt6 t2 s2"
1103
+ − 767
+ − 768
lemma alpha6_equivps:
+ − 769
shows "equivp alpha6"
+ − 770
sorry
+ − 771
+ − 772
quotient_type
+ − 773
trm6 = rtrm6 / alpha6
+ − 774
by (auto intro: alpha6_equivps)
+ − 775
+ − 776
quotient_definition
+ − 777
"Vr6 :: name \<Rightarrow> trm6"
1139
+ − 778
is
1103
+ − 779
"rVr6"
+ − 780
+ − 781
quotient_definition
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 782
"Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6"
1139
+ − 783
is
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 784
"rLm6"
1103
+ − 785
+ − 786
quotient_definition
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 787
"Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
1139
+ − 788
is
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 789
"rLt6"
1103
+ − 790
+ − 791
quotient_definition
+ − 792
"fv_trm6 :: trm6 \<Rightarrow> atom set"
1139
+ − 793
is
1103
+ − 794
"rfv_trm6"
+ − 795
+ − 796
quotient_definition
+ − 797
"bv6 :: trm6 \<Rightarrow> atom set"
1139
+ − 798
is
1103
+ − 799
"rbv6"
+ − 800
1106
+ − 801
lemma [quot_respect]:
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 802
"(op = ===> alpha6 ===> alpha6) permute permute"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 803
apply auto (* will work with eqvt *)
1106
+ − 804
sorry
+ − 805
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 806
(* Definitely not true , see lemma below *)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 807
1104
+ − 808
lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6"
+ − 809
apply simp apply clarify
+ − 810
apply (erule alpha6.induct)
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 811
oops
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 812
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 813
lemma "(a :: name) \<noteq> b \<Longrightarrow> \<not> (alpha6 ===> op =) rbv6 rbv6"
1104
+ − 814
apply simp
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 815
apply (rule_tac x="rLm6 (a::name) (rVr6 (a :: name))" in exI)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 816
apply (rule_tac x="rLm6 (b::name) (rVr6 (b :: name))" in exI)
1104
+ − 817
apply simp
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 818
apply (rule a2)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 819
apply (rule_tac x="(a \<leftrightarrow> b)" in exI)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 820
apply (simp add: alpha_gen fresh_star_def)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 821
apply (rule a1)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 822
apply (rule refl)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 823
done
1103
+ − 824
1104
+ − 825
lemma [quot_respect]:"(alpha6 ===> op =) rfv_trm6 rfv_trm6"
1106
+ − 826
apply simp apply clarify
+ − 827
apply (induct_tac x y rule: alpha6.induct)
+ − 828
apply simp_all
+ − 829
apply (erule exE)
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 830
apply (simp_all add: alpha_gen)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 831
apply (erule conjE)+
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 832
apply (erule exE)
1106
+ − 833
apply (erule conjE)+
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 834
apply (simp)
1106
+ − 835
oops
1103
+ − 836
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 837
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 838
lemma [quot_respect]: "(op = ===> alpha6) rVr6 rVr6"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 839
by (simp_all add: a1)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 840
1103
+ − 841
lemma [quot_respect]:
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 842
"(op = ===> alpha6 ===> alpha6) rLm6 rLm6"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 843
"(alpha6 ===> alpha6 ===> alpha6) rLt6 rLt6"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 844
apply simp_all apply (clarify)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 845
apply (rule a2)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 846
apply (rule_tac x="0::perm" in exI)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 847
apply (simp add: alpha_gen)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 848
(* needs rfv6_rsp *) defer
1103
+ − 849
apply clarify
+ − 850
apply (rule a3)
+ − 851
apply (rule_tac x="0::perm" in exI)
+ − 852
apply (simp add: alpha_gen)
+ − 853
(* needs rbv6_rsp *)
1106
+ − 854
oops
1103
+ − 855
+ − 856
instantiation trm6 :: pt begin
+ − 857
1104
+ − 858
quotient_definition
+ − 859
"permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6"
1139
+ − 860
is
1104
+ − 861
"permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"
+ − 862
1103
+ − 863
instance
1106
+ − 864
apply default
1103
+ − 865
sorry
+ − 866
end
+ − 867
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 868
lemma lifted_induct:
1106
+ − 869
"\<lbrakk>x1 = x2; \<And>a b. a = b \<Longrightarrow> P (Vr6 a) (Vr6 b);
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 870
\<And>a t b s.
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 871
\<exists>pi. fv_trm6 t - {atom a} = fv_trm6 s - {atom b} \<and>
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 872
(fv_trm6 t - {atom a}) \<sharp>* pi \<and> pi \<bullet> t = s \<and> P (pi \<bullet> t) s \<Longrightarrow>
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 873
P (Lm6 a t) (Lm6 b s);
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 874
\<And>t1 s1 t2 s2.
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 875
\<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 876
(fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<and> P (pi \<bullet> s1) s2 \<Longrightarrow>
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 877
P (Lt6 t1 s1) (Lt6 t2 s2)\<rbrakk>
1106
+ − 878
\<Longrightarrow> P x1 x2"
+ − 879
unfolding alpha_gen
+ − 880
apply (lifting alpha6.induct[unfolded alpha_gen])
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 881
apply injection
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 882
(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 883
oops
1106
+ − 884
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 885
lemma lifted_inject_a3:
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 886
"\<exists>pi. fv_trm6 s1 - bv6 t1 = fv_trm6 s2 - bv6 t2 \<and>
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 887
(fv_trm6 s1 - bv6 t1) \<sharp>* pi \<and> pi \<bullet> s1 = s2 \<Longrightarrow> Lt6 t1 s1 = Lt6 t2 s2"
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 888
apply(lifting a3[unfolded alpha_gen])
1103
+ − 889
apply injection
1111
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 890
(* notice unsolvable goals: (alpha6 ===> op =) rbv6 rbv6 *)
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 891
oops
ee276c9f12f0
A concrete example, with a proof that rbv is not regular and
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 892
1103
+ − 893
+ − 894
+ − 895
1121
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 896
(* example with a respectful bn function defined over the type itself *)
1131
+ − 897
1121
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 898
datatype rtrm7 =
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 899
rVr7 "name"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 900
| rLm7 "name" "rtrm7"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 901
| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 902
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 903
primrec
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 904
rbv7
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 905
where
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 906
"rbv7 (rVr7 n) = {atom n}"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 907
| "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 908
| "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 909
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 910
primrec
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 911
rfv_trm7
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 912
where
1131
+ − 913
"rfv_trm7 (rVr7 n) = {atom n}"
+ − 914
| "rfv_trm7 (rLm7 n t) = (rfv_trm7 t) - {atom n}"
+ − 915
| "rfv_trm7 (rLt7 l r) = (rfv_trm7 l) \<union> (rfv_trm7 r - rbv7 l)"
+ − 916
1171
+ − 917
setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *}
+ − 918
print_theorems
1131
+ − 919
+ − 920
inductive
+ − 921
alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
+ − 922
where
+ − 923
a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"
+ − 924
| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 rfv_trm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
+ − 925
| a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 rfv_trm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
1121
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 926
1131
+ − 927
lemma bvfv7: "rbv7 x = rfv_trm7 x"
+ − 928
apply induct
+ − 929
apply simp_all
+ − 930
done
1121
8d3f92694e85
example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 931
1131
+ − 932
lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
+ − 933
apply simp
+ − 934
apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
+ − 935
apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)
+ − 936
apply simp
+ − 937
apply (rule a3)
+ − 938
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 939
apply (simp_all add: alpha_gen fresh_star_def)
+ − 940
apply (rule a1)
+ − 941
apply (rule refl)
+ − 942
done
1103
+ − 943
1133
+ − 944
+ − 945
+ − 946
+ − 947
1132
+ − 948
datatype rfoo8 =
+ − 949
Foo0 "name"
+ − 950
| Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"
+ − 951
and rbar8 =
1135
+ − 952
Bar0 "name"
+ − 953
| Bar1 "name" "name" "rbar8" --"bind second name in b"
1132
+ − 954
+ − 955
primrec
+ − 956
rbv8
+ − 957
where
+ − 958
"rbv8 (Bar0 x) = {}"
+ − 959
| "rbv8 (Bar1 v x b) = {atom v}"
+ − 960
+ − 961
primrec
+ − 962
rfv_foo8 and rfv_bar8
+ − 963
where
+ − 964
"rfv_foo8 (Foo0 x) = {atom x}"
+ − 965
| "rfv_foo8 (Foo1 b t) = (rfv_foo8 t - rbv8 b) \<union> (rfv_bar8 b)"
+ − 966
| "rfv_bar8 (Bar0 x) = {atom x}"
+ − 967
| "rfv_bar8 (Bar1 v x t) = {atom v} \<union> (rfv_bar8 t - {atom x})"
1134
+ − 968
print_theorems
1132
+ − 969
1171
+ − 970
setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *}
+ − 971
print_theorems
1132
+ − 972
+ − 973
inductive
+ − 974
alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
+ − 975
and
+ − 976
alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)
+ − 977
where
+ − 978
a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"
+ − 979
| a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"
1134
+ − 980
| a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f rfv_foo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
1132
+ − 981
| a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b rfv_bar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"
+ − 982
+ − 983
lemma "(alpha8b ===> op =) rbv8 rbv8"
+ − 984
apply simp apply clarify
+ − 985
apply (erule alpha8f_alpha8b.inducts(2))
+ − 986
apply (simp_all)
+ − 987
done
1134
+ − 988
+ − 989
lemma rfv_bar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> rfv_bar8 x = rfv_bar8 y"
1132
+ − 990
apply (erule alpha8f_alpha8b.inducts(2))
1133
+ − 991
apply (simp_all add: alpha_gen)
1132
+ − 992
done
1134
+ − 993
lemma "(alpha8b ===> op =) rfv_bar8 rfv_bar8"
+ − 994
apply simp apply clarify apply (simp add: rfv_bar8_rsp_hlp)
+ − 995
done
1132
+ − 996
1134
+ − 997
lemma "(alpha8f ===> op =) rfv_foo8 rfv_foo8"
+ − 998
apply simp apply clarify
+ − 999
apply (erule alpha8f_alpha8b.inducts(1))
+ − 1000
apply (simp_all add: alpha_gen rfv_bar8_rsp_hlp)
1133
+ − 1001
done
1132
+ − 1002
+ − 1003
+ − 1004
1103
+ − 1005
1134
+ − 1006
1135
+ − 1007
+ − 1008
datatype rlam9 =
+ − 1009
Var9 "name"
+ − 1010
| Lam9 "name" "rlam9" --"bind name in rlam"
+ − 1011
and rbla9 =
+ − 1012
Bla9 "rlam9" "rlam9" --"bind bv(first) in second"
+ − 1013
+ − 1014
primrec
+ − 1015
rbv9
+ − 1016
where
+ − 1017
"rbv9 (Var9 x) = {}"
+ − 1018
| "rbv9 (Lam9 x b) = {atom x}"
+ − 1019
+ − 1020
primrec
+ − 1021
rfv_lam9 and rfv_bla9
+ − 1022
where
+ − 1023
"rfv_lam9 (Var9 x) = {atom x}"
+ − 1024
| "rfv_lam9 (Lam9 b t) = (rfv_lam9 t - {atom b})"
+ − 1025
| "rfv_bla9 (Bla9 l r) = (rfv_lam9 r - rbv9 l) \<union> rfv_lam9 l"
+ − 1026
1171
+ − 1027
setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *}
+ − 1028
print_theorems
1135
+ − 1029
+ − 1030
inductive
+ − 1031
alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100)
+ − 1032
and
+ − 1033
alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100)
+ − 1034
where
+ − 1035
a1: "a = b \<Longrightarrow> (Var9 a) \<approx>9l (Var9 b)"
+ − 1036
| a4: "(\<exists>pi. (({atom x1}, t1) \<approx>gen alpha9l rfv_lam9 pi ({atom x2}, t2))) \<Longrightarrow> Lam9 x1 t1 \<approx>9l Lam9 x2 t2"
+ − 1037
| a3: "b1 \<approx>9l b2 \<Longrightarrow> (\<exists>pi. (((rbv9 b1), t1) \<approx>gen alpha9l rfv_lam9 pi ((rbv9 b2), t2))) \<Longrightarrow> Bla9 b1 t1 \<approx>9b Bla9 b2 t2"
+ − 1038
+ − 1039
quotient_type
+ − 1040
lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b
+ − 1041
sorry
+ − 1042
+ − 1043
quotient_definition
+ − 1044
"qVar9 :: name \<Rightarrow> lam9"
1139
+ − 1045
is
1135
+ − 1046
"Var9"
+ − 1047
+ − 1048
quotient_definition
+ − 1049
"qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9"
1139
+ − 1050
is
1135
+ − 1051
"Lam9"
+ − 1052
+ − 1053
quotient_definition
+ − 1054
"qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9"
1139
+ − 1055
is
1135
+ − 1056
"Bla9"
+ − 1057
+ − 1058
quotient_definition
+ − 1059
"fv_lam9 :: lam9 \<Rightarrow> atom set"
1139
+ − 1060
is
1135
+ − 1061
"rfv_lam9"
+ − 1062
+ − 1063
quotient_definition
+ − 1064
"fv_bla9 :: bla9 \<Rightarrow> atom set"
1139
+ − 1065
is
1135
+ − 1066
"rfv_bla9"
+ − 1067
+ − 1068
quotient_definition
+ − 1069
"bv9 :: lam9 \<Rightarrow> atom set"
1139
+ − 1070
is
1135
+ − 1071
"rbv9"
+ − 1072
+ − 1073
instantiation lam9 and bla9 :: pt
+ − 1074
begin
+ − 1075
+ − 1076
quotient_definition
+ − 1077
"permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9"
1139
+ − 1078
is
1135
+ − 1079
"permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9"
+ − 1080
+ − 1081
quotient_definition
+ − 1082
"permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9"
1139
+ − 1083
is
1135
+ − 1084
"permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9"
+ − 1085
+ − 1086
instance
+ − 1087
sorry
+ − 1088
+ − 1089
end
+ − 1090
+ − 1091
lemma "\<lbrakk>b1 = b2; \<exists>pi. fv_lam9 t1 - bv9 b1 = fv_lam9 t2 - bv9 b2 \<and> (fv_lam9 t1 - bv9 b1) \<sharp>* pi \<and> pi \<bullet> t1 = t2\<rbrakk>
+ − 1092
\<Longrightarrow> qBla9 b1 t1 = qBla9 b2 t2"
+ − 1093
apply (lifting a3[unfolded alpha_gen])
+ − 1094
apply injection
+ − 1095
sorry
+ − 1096
+ − 1097
+ − 1098
+ − 1099
+ − 1100
+ − 1101
+ − 1102
+ − 1103
1048
+ − 1104
text {* type schemes *}
+ − 1105
datatype ty =
+ − 1106
Var "name"
+ − 1107
| Fun "ty" "ty"
+ − 1108
1171
+ − 1109
setup {* snd o define_raw_perms ["ty"] ["Terms.ty"] *}
+ − 1110
print_theorems
1048
+ − 1111
+ − 1112
datatype tyS =
+ − 1113
All "name set" "ty"
1046
+ − 1114
1171
+ − 1115
setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
+ − 1116
print_theorems
1040
+ − 1117
1048
+ − 1118
abbreviation
+ − 1119
"atoms xs \<equiv> {atom x| x. x \<in> xs}"
+ − 1120
+ − 1121
primrec
+ − 1122
rfv_ty
+ − 1123
where
+ − 1124
"rfv_ty (Var n) = {atom n}"
+ − 1125
| "rfv_ty (Fun T1 T2) = (rfv_ty T1) \<union> (rfv_ty T2)"
+ − 1126
+ − 1127
primrec
+ − 1128
rfv_tyS
+ − 1129
where
+ − 1130
"rfv_tyS (All xs T) = (rfv_ty T - atoms xs)"
+ − 1131
+ − 1132
inductive
+ − 1133
alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
+ − 1134
where
+ − 1135
a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) rfv_ty pi (atoms xs2, T2))
+ − 1136
\<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
+ − 1137
+ − 1138
lemma
+ − 1139
shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))"
+ − 1140
apply(rule a1)
+ − 1141
apply(simp add: alpha_gen)
+ − 1142
apply(rule_tac x="0::perm" in exI)
+ − 1143
apply(simp add: fresh_star_def)
+ − 1144
done
+ − 1145
+ − 1146
lemma
+ − 1147
shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var b) (Var a))"
+ − 1148
apply(rule a1)
+ − 1149
apply(simp add: alpha_gen)
+ − 1150
apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+ − 1151
apply(simp add: fresh_star_def)
+ − 1152
done
+ − 1153
+ − 1154
lemma
+ − 1155
shows "All {a, b, c} (Fun (Var a) (Var b)) \<approx>tyS All {a, b} (Fun (Var a) (Var b))"
+ − 1156
apply(rule a1)
+ − 1157
apply(simp add: alpha_gen)
+ − 1158
apply(rule_tac x="0::perm" in exI)
+ − 1159
apply(simp add: fresh_star_def)
+ − 1160
done
+ − 1161
+ − 1162
lemma
+ − 1163
assumes a: "a \<noteq> b"
+ − 1164
shows "\<not>(All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {c} (Fun (Var c) (Var c)))"
+ − 1165
using a
+ − 1166
apply(clarify)
+ − 1167
apply(erule alpha_tyS.cases)
+ − 1168
apply(simp add: alpha_gen)
+ − 1169
apply(erule conjE)+
+ − 1170
apply(erule exE)
+ − 1171
apply(erule conjE)+
+ − 1172
apply(clarify)
+ − 1173
apply(simp)
+ − 1174
apply(simp add: fresh_star_def)
+ − 1175
apply(auto)
+ − 1176
done
1051
+ − 1177
1048
+ − 1178
1035
+ − 1179
end