201
+ − 1
theory LamEx
1128
+ − 2
imports Nominal "../Quotient" "../Quotient_List"
201
+ − 3
begin
+ − 4
+ − 5
atom_decl name
+ − 6
804
+ − 7
datatype rlam =
201
+ − 8
rVar "name"
+ − 9
| rApp "rlam" "rlam"
+ − 10
| rLam "name" "rlam"
+ − 11
804
+ − 12
fun
243
+ − 13
rfv :: "rlam \<Rightarrow> name set"
+ − 14
where
+ − 15
rfv_var: "rfv (rVar a) = {a}"
+ − 16
| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)"
+ − 17
| rfv_lam: "rfv (rLam a t) = (rfv t) - {a}"
804
+ − 18
+ − 19
overloading
876
+ − 20
perm_rlam \<equiv> "perm :: 'x prm \<Rightarrow> rlam \<Rightarrow> rlam" (unchecked)
804
+ − 21
begin
243
+ − 22
804
+ − 23
fun
+ − 24
perm_rlam
+ − 25
where
+ − 26
"perm_rlam pi (rVar a) = rVar (pi \<bullet> a)"
+ − 27
| "perm_rlam pi (rApp t1 t2) = rApp (perm_rlam pi t1) (perm_rlam pi t2)"
+ − 28
| "perm_rlam pi (rLam a t) = rLam (pi \<bullet> a) (perm_rlam pi t)"
+ − 29
+ − 30
end
243
+ − 31
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 32
declare perm_rlam.simps[eqvt]
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33
895
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 34
instance rlam::pt_name
900
+ − 35
apply(default)
+ − 36
apply(induct_tac [!] x rule: rlam.induct)
+ − 37
apply(simp_all add: pt_name2 pt_name3)
+ − 38
done
895
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 40
instance rlam::fs_name
900
+ − 41
apply(default)
+ − 42
apply(induct_tac [!] x rule: rlam.induct)
+ − 43
apply(simp add: supp_def)
+ − 44
apply(fold supp_def)
+ − 45
apply(simp add: supp_atm)
+ − 46
apply(simp add: supp_def Collect_imp_eq Collect_neg_eq)
+ − 47
apply(simp add: supp_def)
+ − 48
apply(simp add: supp_def Collect_imp_eq Collect_neg_eq[symmetric])
+ − 49
apply(fold supp_def)
+ − 50
apply(simp add: supp_atm)
+ − 51
done
895
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 52
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 53
declare set_diff_eqvt[eqvt]
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 54
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
lemma rfv_eqvt[eqvt]:
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 56
fixes pi::"name prm"
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 57
shows "(pi\<bullet>rfv t) = rfv (pi\<bullet>t)"
1991
+ − 58
apply(induct t)
+ − 59
apply(simp_all)
+ − 60
apply(simp add: perm_set_eq)
+ − 61
apply(simp add: union_eqvt)
+ − 62
apply(simp add: set_diff_eqvt)
+ − 63
apply(simp add: perm_set_eq)
+ − 64
done
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 65
271
+ − 66
inductive
1991
+ − 67
alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
246
+ − 68
where
+ − 69
a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
+ − 70
| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
915
+ − 71
| a3: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b)
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 72
\<Longrightarrow> rLam a t \<approx> rLam b s"
246
+ − 73
918
+ − 74
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 75
(* should be automatic with new version of eqvt-machinery *)
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 76
lemma alpha_eqvt:
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 77
fixes pi::"name prm"
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 78
shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)"
1991
+ − 79
apply(induct rule: alpha.induct)
+ − 80
apply(simp add: a1)
+ − 81
apply(simp add: a2)
+ − 82
apply(simp)
+ − 83
apply(rule a3)
+ − 84
apply(erule conjE)
+ − 85
apply(erule exE)
+ − 86
apply(erule conjE)
+ − 87
apply(rule_tac x="pi \<bullet> pia" in exI)
+ − 88
apply(rule conjI)
+ − 89
apply(rule_tac pi1="rev pi" in perm_bij[THEN iffD1])
+ − 90
apply(perm_simp add: eqvts)
+ − 91
apply(rule conjI)
+ − 92
apply(rule_tac pi1="rev pi" in pt_fresh_star_bij(1)[OF pt_name_inst at_name_inst, THEN iffD1])
+ − 93
apply(perm_simp add: eqvts)
+ − 94
apply(rule conjI)
+ − 95
apply(subst perm_compose[symmetric])
+ − 96
apply(simp)
+ − 97
apply(subst perm_compose[symmetric])
+ − 98
apply(simp)
+ − 99
done
259
+ − 100
271
+ − 101
lemma alpha_refl:
286
+ − 102
shows "t \<approx> t"
1991
+ − 103
apply(induct t rule: rlam.induct)
+ − 104
apply(simp add: a1)
+ − 105
apply(simp add: a2)
+ − 106
apply(rule a3)
+ − 107
apply(rule_tac x="[]" in exI)
+ − 108
apply(simp_all add: fresh_star_def fresh_list_nil)
+ − 109
done
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 110
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 111
lemma alpha_sym:
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 112
shows "t \<approx> s \<Longrightarrow> s \<approx> t"
1991
+ − 113
apply(induct rule: alpha.induct)
+ − 114
apply(simp add: a1)
+ − 115
apply(simp add: a2)
+ − 116
apply(rule a3)
+ − 117
apply(erule exE)
+ − 118
apply(rule_tac x="rev pi" in exI)
+ − 119
apply(simp)
+ − 120
apply(simp add: fresh_star_def fresh_list_rev)
+ − 121
apply(rule conjI)
+ − 122
apply(erule conjE)+
+ − 123
apply(rotate_tac 3)
+ − 124
apply(drule_tac pi="rev pi" in alpha_eqvt)
+ − 125
apply(perm_simp)
+ − 126
apply(rule pt_bij2[OF pt_name_inst at_name_inst])
+ − 127
apply(simp)
+ − 128
done
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 129
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 130
lemma alpha_trans:
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 131
shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3"
1991
+ − 132
apply(induct arbitrary: t3 rule: alpha.induct)
+ − 133
apply(erule alpha.cases)
+ − 134
apply(simp_all)
+ − 135
apply(simp add: a1)
+ − 136
apply(rotate_tac 4)
+ − 137
apply(erule alpha.cases)
+ − 138
apply(simp_all)
+ − 139
apply(simp add: a2)
+ − 140
apply(rotate_tac 1)
+ − 141
apply(erule alpha.cases)
+ − 142
apply(simp_all)
+ − 143
apply(erule conjE)+
+ − 144
apply(erule exE)+
+ − 145
apply(erule conjE)+
+ − 146
apply(rule a3)
+ − 147
apply(rule_tac x="pia @ pi" in exI)
+ − 148
apply(simp add: fresh_star_def fresh_list_append)
+ − 149
apply(simp add: pt_name2)
+ − 150
apply(drule_tac x="rev pia \<bullet> sa" in spec)
+ − 151
apply(drule mp)
+ − 152
apply(rotate_tac 8)
+ − 153
apply(drule_tac pi="rev pia" in alpha_eqvt)
+ − 154
apply(perm_simp)
+ − 155
apply(rotate_tac 11)
+ − 156
apply(drule_tac pi="pia" in alpha_eqvt)
+ − 157
apply(perm_simp)
+ − 158
done
286
+ − 159
534
+ − 160
lemma alpha_equivp:
+ − 161
shows "equivp alpha"
1991
+ − 162
apply(rule equivpI)
+ − 163
unfolding reflp_def symp_def transp_def
+ − 164
apply(auto intro: alpha_refl alpha_sym alpha_trans)
+ − 165
done
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 166
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 167
lemma alpha_rfv:
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 168
shows "t \<approx> s \<Longrightarrow> rfv t = rfv s"
1991
+ − 169
apply(induct rule: alpha.induct)
+ − 170
apply(simp)
+ − 171
apply(simp)
+ − 172
apply(simp)
+ − 173
done
271
+ − 174
766
df053507edba
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 175
quotient_type lam = rlam / alpha
804
+ − 176
by (rule alpha_equivp)
201
+ − 177
203
+ − 178
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 179
quotient_definition
876
+ − 180
"Var :: name \<Rightarrow> lam"
1139
+ − 181
is
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 182
"rVar"
229
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 183
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 184
quotient_definition
705
+ − 185
"App :: lam \<Rightarrow> lam \<Rightarrow> lam"
1139
+ − 186
is
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 187
"rApp"
229
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 188
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 189
quotient_definition
876
+ − 190
"Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
1139
+ − 191
is
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 192
"rLam"
201
+ − 193
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 194
quotient_definition
876
+ − 195
"fv :: lam \<Rightarrow> name set"
1139
+ − 196
is
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 197
"rfv"
243
+ − 198
229
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 199
(* definition of overloaded permutation function *)
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 200
(* for the lifted type lam *)
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 201
overloading
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 202
perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked)
229
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 203
begin
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 204
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 205
quotient_definition
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 206
"perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
1139
+ − 207
is
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 208
"perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"
229
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 209
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 210
end
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 211
636
+ − 212
lemma perm_rsp[quot_respect]:
1991
+ − 213
"(op = ===> alpha ===> alpha) op \<bullet> (op \<bullet> :: (name \<times> name) list \<Rightarrow> rlam \<Rightarrow> rlam)"
+ − 214
apply auto
+ − 215
apply(erule alpha_eqvt)
+ − 216
done
229
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 217
636
+ − 218
lemma rVar_rsp[quot_respect]:
451
586e3dc4afdb
Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 219
"(op = ===> alpha) rVar rVar"
876
+ − 220
by (auto intro: a1)
234
+ − 221
636
+ − 222
lemma rApp_rsp[quot_respect]: "(alpha ===> alpha ===> alpha) rApp rApp"
876
+ − 223
by (auto intro: a2)
234
+ − 224
636
+ − 225
lemma rLam_rsp[quot_respect]: "(op = ===> alpha ===> alpha) rLam rLam"
229
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 226
apply(auto)
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 227
apply(rule a3)
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 228
apply(rule_tac x="[]" in exI)
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 229
unfolding fresh_star_def
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 230
apply(simp add: fresh_list_nil)
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 231
apply(simp add: alpha_rfv)
229
13f985a93dbc
fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 232
done
217
+ − 233
804
+ − 234
lemma rfv_rsp[quot_respect]:
+ − 235
"(alpha ===> op =) rfv rfv"
1991
+ − 236
apply(simp add: alpha_rfv)
+ − 237
done
217
+ − 238
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 239
section {* lifted theorems *}
370
+ − 240
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 241
lemma lam_induct:
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 242
"\<lbrakk>\<And>name. P (Var name);
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 243
\<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 244
\<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk>
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 245
\<Longrightarrow> P lam"
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 246
by (lifting rlam.induct)
249
+ − 247
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 248
lemma perm_lam [simp]:
1991
+ − 249
fixes pi::"name prm"
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 250
shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 251
and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 252
and "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
1991
+ − 253
by (lifting perm_rlam.simps[where 'a="name"])
376
+ − 254
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 255
instance lam::pt_name
1991
+ − 256
apply(default)
+ − 257
apply(induct_tac [!] x rule: lam_induct)
+ − 258
apply(simp_all add: pt_name2 pt_name3)
+ − 259
done
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 260
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 261
lemma fv_lam [simp]:
804
+ − 262
shows "fv (Var a) = {a}"
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 263
and "fv (App t1 t2) = fv t1 \<union> fv t2"
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 264
and "fv (Lam a t) = fv t - {a}"
1991
+ − 265
by(lifting rfv_var rfv_app rfv_lam)
249
+ − 266
1991
+ − 267
lemma a1:
804
+ − 268
"a = b \<Longrightarrow> Var a = Var b"
+ − 269
by (lifting a1)
376
+ − 270
1991
+ − 271
lemma a2:
804
+ − 272
"\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
+ − 273
by (lifting a2)
376
+ − 274
1991
+ − 275
lemma a3:
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 276
"\<lbrakk>\<exists>pi::name prm. (fv t - {a} = fv s - {b} \<and> (fv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) = s \<and> (pi \<bullet> a) = b)\<rbrakk>
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 277
\<Longrightarrow> Lam a t = Lam b s"
804
+ − 278
by (lifting a3)
286
+ − 279
1991
+ − 280
lemma alpha_cases:
804
+ − 281
"\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
+ − 282
\<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
1991
+ − 283
\<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s;
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 284
\<exists>pi::name prm. fv t - {a} = fv s - {b} \<and> (fv t - {a}) \<sharp>* pi \<and> (pi \<bullet> t) = s \<and> pi \<bullet> a = b\<rbrakk> \<Longrightarrow> P\<rbrakk>
370
+ − 285
\<Longrightarrow> P"
804
+ − 286
by (lifting alpha.cases)
378
+ − 287
1991
+ − 288
lemma alpha_induct:
804
+ − 289
"\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
+ − 290
\<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 291
\<And>t a s b.
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 292
\<lbrakk>\<exists>pi::name prm. fv t - {a} = fv s - {b} \<and>
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 293
(fv t - {a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s) \<and> pi \<bullet> a = b\<rbrakk> \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
370
+ − 294
\<Longrightarrow> qxb qx qxa"
804
+ − 295
by (lifting alpha.induct)
+ − 296
897
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 297
lemma lam_inject [simp]:
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 298
shows "(Var a = Var b) = (a = b)"
464619898890
used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 299
and "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)"
1991
+ − 300
apply(lifting rlam.inject(1) rlam.inject(2))
+ − 301
apply(auto)
+ − 302
apply(drule alpha.cases)
+ − 303
apply(simp_all)
+ − 304
apply(simp add: alpha.a1)
+ − 305
apply(drule alpha.cases)
+ − 306
apply(simp_all)
+ − 307
apply(drule alpha.cases)
+ − 308
apply(simp_all)
+ − 309
apply(rule alpha.a2)
+ − 310
apply(simp_all)
+ − 311
done
883
+ − 312
916
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 313
lemma rlam_distinct:
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 314
shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 315
and "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 316
and "\<not>(rVar nam \<approx> rLam nam' rlam')"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 317
and "\<not>(rLam nam' rlam' \<approx> rVar nam)"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 318
and "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 319
and "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)"
1991
+ − 320
apply auto
+ − 321
apply(erule alpha.cases)
+ − 322
apply simp_all
+ − 323
apply(erule alpha.cases)
+ − 324
apply simp_all
+ − 325
apply(erule alpha.cases)
+ − 326
apply simp_all
+ − 327
apply(erule alpha.cases)
+ − 328
apply simp_all
+ − 329
apply(erule alpha.cases)
+ − 330
apply simp_all
+ − 331
apply(erule alpha.cases)
+ − 332
apply simp_all
+ − 333
done
916
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 334
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 335
lemma lam_distinct[simp]:
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 336
shows "Var nam \<noteq> App lam1' lam2'"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 337
and "App lam1' lam2' \<noteq> Var nam"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 338
and "Var nam \<noteq> Lam nam' lam'"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 339
and "Lam nam' lam' \<noteq> Var nam"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 340
and "App lam1 lam2 \<noteq> Lam nam' lam'"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 341
and "Lam nam' lam' \<noteq> App lam1 lam2"
1991
+ − 342
by(lifting rlam_distinct(1) rlam_distinct(2) rlam_distinct(3) rlam_distinct(4) rlam_distinct(5) rlam_distinct(6))
916
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 343
883
+ − 344
lemma var_supp1:
+ − 345
shows "(supp (Var a)) = ((supp a)::name set)"
916
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 346
by (simp add: supp_def)
883
+ − 347
+ − 348
lemma var_supp:
+ − 349
shows "(supp (Var a)) = {a::name}"
916
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 350
using var_supp1 by (simp add: supp_atm)
883
+ − 351
+ − 352
lemma app_supp:
+ − 353
shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)"
1991
+ − 354
apply(simp only: perm_lam supp_def lam_inject)
+ − 355
apply(simp add: Collect_imp_eq Collect_neg_eq)
+ − 356
done
883
+ − 357
+ − 358
lemma lam_supp:
+ − 359
shows "supp (Lam x t) = ((supp ([x].t))::name set)"
1991
+ − 360
apply(simp add: supp_def)
+ − 361
apply(simp add: abs_perm)
+ − 362
sorry
878
+ − 363
+ − 364
instance lam::fs_name
1991
+ − 365
apply(default)
+ − 366
apply(induct_tac x rule: lam_induct)
+ − 367
apply(simp add: var_supp)
+ − 368
apply(simp add: app_supp)
+ − 369
apply(simp add: lam_supp abs_supp)
+ − 370
done
877
+ − 371
881
+ − 372
lemma fresh_lam:
+ − 373
"(a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> a \<sharp> t)"
1991
+ − 374
apply(simp add: fresh_def)
+ − 375
apply(simp add: lam_supp abs_supp)
+ − 376
apply(auto)
+ − 377
done
881
+ − 378
877
+ − 379
lemma lam_induct_strong:
878
+ − 380
fixes a::"'a::fs_name"
879
+ − 381
assumes a1: "\<And>name b. P b (Var name)"
+ − 382
and a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)"
881
+ − 383
and a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lam name lam)"
879
+ − 384
shows "P a lam"
878
+ − 385
proof -
880
+ − 386
have "\<And>(pi::name prm) a. P a (pi \<bullet> lam)"
878
+ − 387
proof (induct lam rule: lam_induct)
+ − 388
case (1 name pi)
879
+ − 389
show "P a (pi \<bullet> Var name)"
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 390
apply (simp)
879
+ − 391
apply (rule a1)
+ − 392
done
878
+ − 393
next
+ − 394
case (2 lam1 lam2 pi)
880
+ − 395
have b1: "\<And>(pi::name prm) a. P a (pi \<bullet> lam1)" by fact
+ − 396
have b2: "\<And>(pi::name prm) a. P a (pi \<bullet> lam2)" by fact
879
+ − 397
show "P a (pi \<bullet> App lam1 lam2)"
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 398
apply (simp)
879
+ − 399
apply (rule a2)
880
+ − 400
apply (rule b1)
+ − 401
apply (rule b2)
+ − 402
done
878
+ − 403
next
881
+ − 404
case (3 name lam pi a)
+ − 405
have b: "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" by fact
882
+ − 406
obtain c::name where fr: "c\<sharp>(a, pi\<bullet>name, pi\<bullet>lam)"
+ − 407
apply(rule exists_fresh[of "(a, pi\<bullet>name, pi\<bullet>lam)"])
+ − 408
apply(simp_all add: fs_name1)
+ − 409
done
881
+ − 410
from b fr have p: "P a (Lam c (([(c, pi\<bullet>name)]@pi)\<bullet>lam))"
+ − 411
apply -
+ − 412
apply(rule a3)
+ − 413
apply(blast)
+ − 414
apply(simp)
+ − 415
done
+ − 416
have eq: "[(c, pi\<bullet>name)] \<bullet> Lam (pi \<bullet> name) (pi \<bullet> lam) = Lam (pi \<bullet> name) (pi \<bullet> lam)"
+ − 417
apply(rule perm_fresh_fresh)
+ − 418
using fr
+ − 419
apply(simp add: fresh_lam)
+ − 420
apply(simp add: fresh_lam)
+ − 421
done
879
+ − 422
show "P a (pi \<bullet> Lam name lam)"
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 423
apply (simp)
881
+ − 424
apply(subst eq[symmetric])
+ − 425
using p
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 426
apply(simp only: perm_lam pt_name2 swap_simps)
881
+ − 427
done
878
+ − 428
qed
+ − 429
then have "P a (([]::name prm) \<bullet> lam)" by blast
+ − 430
then show "P a lam" by simp
+ − 431
qed
877
+ − 432
+ − 433
249
+ − 434
lemma var_fresh:
+ − 435
fixes a::"name"
804
+ − 436
shows "(a \<sharp> (Var b)) = (a \<sharp> b)"
249
+ − 437
apply(simp add: fresh_def)
884
+ − 438
apply(simp add: var_supp1)
249
+ − 439
done
247
+ − 440
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 441
(* lemma hom_reg: *)
887
+ − 442
895
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 443
lemma rlam_rec_eqvt:
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 444
fixes pi::"name prm"
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 445
and f1::"name \<Rightarrow> ('a::pt_name)"
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 446
shows "(pi\<bullet>rlam_rec f1 f2 f3 t) = rlam_rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3) (pi\<bullet>t)"
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 447
apply(induct t)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 448
apply(simp_all)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 449
apply(simp add: perm_fun_def)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 450
apply(perm_simp)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 451
apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 452
back
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 453
apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 454
apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 455
apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 456
apply(simp)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 457
apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 458
back
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 459
apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 460
apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst])
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 461
apply(simp)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 462
done
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 463
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 464
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 465
lemma rlam_rec_respects:
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 466
assumes f1: "f_var \<in> Respects (op= ===> op=)"
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 467
and f2: "f_app \<in> Respects (alpha ===> alpha ===> op= ===> op= ===> op=)"
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 468
and f3: "f_lam \<in> Respects (op= ===> alpha ===> op= ===> op=)"
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 469
shows "rlam_rec f_var f_app f_lam \<in> Respects (alpha ===> op =)"
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 470
apply(simp add: mem_def)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 471
apply(simp add: Respects_def)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 472
apply(rule allI)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 473
apply(rule allI)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 474
apply(rule impI)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 475
apply(erule alpha.induct)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 476
apply(simp)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 477
apply(simp)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 478
using f2
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 479
apply(simp add: mem_def)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 480
apply(simp add: Respects_def)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 481
using f3[simplified mem_def Respects_def]
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 482
apply(simp)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 483
apply(case_tac "a=b")
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 484
apply(clarify)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 485
apply(simp)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 486
(* probably true *)
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 487
sorry
92c43c96027e
added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 488
901
+ − 489
function
903
+ − 490
term1_hom :: "(name \<Rightarrow> 'a) \<Rightarrow>
+ − 491
(rlam \<Rightarrow> rlam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow>
902
+ − 492
((name \<Rightarrow> rlam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> rlam \<Rightarrow> 'a"
901
+ − 493
where
+ − 494
"term1_hom var app abs' (rVar x) = (var x)"
+ − 495
| "term1_hom var app abs' (rApp t u) =
+ − 496
app t u (term1_hom var app abs' t) (term1_hom var app abs' u)"
+ − 497
| "term1_hom var app abs' (rLam x u) =
+ − 498
abs' (\<lambda>y. [(x, y)] \<bullet> u) (\<lambda>y. term1_hom var app abs' ([(x, y)] \<bullet> u))"
902
+ − 499
apply(pat_completeness)
+ − 500
apply(auto)
+ − 501
done
901
+ − 502
902
+ − 503
lemma pi_size:
+ − 504
fixes pi::"name prm"
+ − 505
and t::"rlam"
+ − 506
shows "size (pi \<bullet> t) = size t"
+ − 507
apply(induct t)
+ − 508
apply(auto)
+ − 509
done
+ − 510
+ − 511
termination term1_hom
+ − 512
apply(relation "measure (\<lambda>(f1, f2, f3, t). size t)")
+ − 513
apply(auto simp add: pi_size)
+ − 514
done
901
+ − 515
916
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 516
lemma lam_exhaust:
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 517
"\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; \<And>rlam1 rlam2. y = App rlam1 rlam2 \<Longrightarrow> P; \<And>name rlam. y = Lam name rlam \<Longrightarrow> P\<rbrakk>
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 518
\<Longrightarrow> P"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 519
apply(lifting rlam.exhaust)
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 520
done
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 521
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 522
(* THIS IS NOT TRUE, but it lets prove the existence of the hom function *)
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 523
lemma lam_inject':
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 524
"(Lam a x = Lam b y) = ((\<lambda>c. [(a, c)] \<bullet> x) = (\<lambda>c. [(b, c)] \<bullet> y))"
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 525
sorry
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 526
915
+ − 527
function
+ − 528
hom :: "(name \<Rightarrow> 'a) \<Rightarrow>
+ − 529
(lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow>
+ − 530
((name \<Rightarrow> lam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> lam \<Rightarrow> 'a"
+ − 531
where
+ − 532
"hom f_var f_app f_lam (Var x) = f_var x"
+ − 533
| "hom f_var f_app f_lam (App l r) = f_app l r (hom f_var f_app f_lam l) (hom f_var f_app f_lam r)"
+ − 534
| "hom f_var f_app f_lam (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom f_var f_app f_lam ([(a,b)] \<bullet> x))"
916
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 535
defer
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 536
apply(simp_all add: lam_inject') (* inject, distinct *)
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 537
apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 538
apply(rule refl)
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 539
apply(rule ext)
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 540
apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 541
apply simp_all
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 542
apply(erule conjE)+
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 543
apply(rule_tac x="b" in cong)
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 544
apply simp_all
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 545
apply auto
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 546
apply(rule_tac y="b" in lam_exhaust)
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 547
apply simp_all
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 548
apply auto
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 549
apply meson
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 550
apply(simp_all add: lam_inject')
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 551
apply metis
915
+ − 552
done
916
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 553
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 554
termination hom
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 555
apply -
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 556
(*
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 557
ML_prf {* Size.size_thms @{theory} "LamEx.lam" *}
915
+ − 558
*)
916
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 559
sorry
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 560
a7bf638e9af3
More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 561
thm hom.simps
915
+ − 562
903
+ − 563
lemma term1_hom_rsp:
+ − 564
"\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk>
+ − 565
\<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)"
918
+ − 566
apply(simp)
+ − 567
apply(rule allI)+
+ − 568
apply(rule impI)
+ − 569
apply(erule alpha.induct)
+ − 570
apply(auto)[1]
+ − 571
apply(auto)[1]
+ − 572
apply(simp)
+ − 573
apply(erule conjE)+
+ − 574
apply(erule exE)+
+ − 575
apply(erule conjE)+
+ − 576
apply(clarify)
903
+ − 577
sorry
+ − 578
+ − 579
lemma hom: "
900
+ − 580
\<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =).
+ − 581
\<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =).
+ − 582
\<exists>hom\<in>Respects (alpha ===> op =).
+ − 583
((\<forall>x. hom (rVar x) = f_var x) \<and>
+ − 584
(\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
+ − 585
(\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))"
+ − 586
apply(rule allI)
+ − 587
apply(rule ballI)+
901
+ − 588
apply(rule_tac x="term1_hom f_var f_app f_lam" in bexI)
903
+ − 589
apply(simp_all)
+ − 590
apply(simp only: in_respects)
+ − 591
apply(rule term1_hom_rsp)
+ − 592
apply(assumption)+
+ − 593
done
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 594
889
cff21786d952
Appropriate respects and a statement of the lifted hom lemma
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 595
lemma hom':
903
+ − 596
"\<exists>hom.
894
1d80641a4302
tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 597
((\<forall>x. hom (Var x) = f_var x) \<and>
1d80641a4302
tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 598
(\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and>
1d80641a4302
tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 599
(\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))"
903
+ − 600
apply (lifting hom)
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 601
done
890
+ − 602
896
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 603
(* test test
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 604
lemma raw_hom_correct:
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 605
assumes f1: "f_var \<in> Respects (op= ===> op=)"
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 606
and f2: "f_app \<in> Respects (alpha ===> alpha ===> op= ===> op= ===> op=)"
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 607
and f3: "f_lam \<in> Respects ((op= ===> alpha) ===> (op= ===> op=) ===> op=)"
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 608
shows "\<exists>!hom\<in>Respects (alpha ===> op =).
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 609
((\<forall>x. hom (rVar x) = f_var x) \<and>
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 610
(\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 611
(\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))"
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 612
unfolding Bex1_def
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 613
apply(rule ex1I)
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 614
sorry
4e0b89d886ac
liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 615
*)
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 616
887
+ − 617
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 618
end
891
7bac7dffadeb
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 619