1830
+ − 1
theory Equivp
2296
+ − 2
imports "Abs" "Perm" "Tacs" "Rsp"
1830
+ − 3
begin
+ − 4
+ − 5
ML {*
+ − 6
fun build_alpha_sym_trans_gl alphas (x, y, z) =
+ − 7
let
+ − 8
fun build_alpha alpha =
+ − 9
let
+ − 10
val ty = domain_type (fastype_of alpha);
+ − 11
val var = Free(x, ty);
+ − 12
val var2 = Free(y, ty);
+ − 13
val var3 = Free(z, ty);
+ − 14
val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
+ − 15
val transp = HOLogic.mk_imp (alpha $ var $ var2,
+ − 16
HOLogic.mk_all (z, ty,
+ − 17
HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
+ − 18
in
+ − 19
(symp, transp)
+ − 20
end;
+ − 21
val eqs = map build_alpha alphas
+ − 22
val (sym_eqs, trans_eqs) = split_list eqs
+ − 23
fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
+ − 24
in
+ − 25
(conj sym_eqs, conj trans_eqs)
+ − 26
end
+ − 27
*}
+ − 28
+ − 29
ML {*
+ − 30
fun build_alpha_refl_gl fv_alphas_lst alphas =
+ − 31
let
+ − 32
val (fvs_alphas, _) = split_list fv_alphas_lst;
+ − 33
val (_, alpha_ts) = split_list fvs_alphas;
+ − 34
val tys = map (domain_type o fastype_of) alpha_ts;
+ − 35
val names = Datatype_Prop.make_tnames tys;
+ − 36
val args = map Free (names ~~ tys);
+ − 37
fun find_alphas ty x =
+ − 38
domain_type (fastype_of x) = ty;
+ − 39
fun refl_eq_arg (ty, arg) =
+ − 40
let
+ − 41
val rel_alphas = filter (find_alphas ty) alphas;
+ − 42
in
+ − 43
map (fn x => x $ arg $ arg) rel_alphas
+ − 44
end;
+ − 45
(* Flattening loses the induction structure *)
+ − 46
val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args))
+ − 47
in
+ − 48
(names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
+ − 49
end
+ − 50
*}
+ − 51
+ − 52
ML {*
+ − 53
fun reflp_tac induct eq_iff =
+ − 54
rtac induct THEN_ALL_NEW
+ − 55
simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
+ − 56
split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
+ − 57
THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
+ − 58
@{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
2070
+ − 59
add_0_left supp_zero_perm Int_empty_left split_conv prod_rel.simps})
1830
+ − 60
*}
+ − 61
+ − 62
ML {*
+ − 63
fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
+ − 64
let
+ − 65
val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
+ − 66
val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1);
+ − 67
in
+ − 68
HOLogic.conj_elims refl_conj
+ − 69
end
+ − 70
*}
+ − 71
+ − 72
lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
+ − 73
apply (erule exE)
+ − 74
apply (rule_tac x="-pi" in exI)
+ − 75
by auto
+ − 76
+ − 77
ML {*
+ − 78
fun symp_tac induct inj eqvt ctxt =
2108
+ − 79
rtac induct THEN_ALL_NEW
1830
+ − 80
simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac
+ − 81
THEN_ALL_NEW
+ − 82
REPEAT o etac @{thm exi_neg}
+ − 83
THEN_ALL_NEW
+ − 84
split_conj_tac THEN_ALL_NEW
+ − 85
asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
+ − 86
TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW
+ − 87
(asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
+ − 88
*}
+ − 89
+ − 90
+ − 91
lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
+ − 92
apply (erule exE)+
+ − 93
apply (rule_tac x="pia + pi" in exI)
+ − 94
by auto
+ − 95
+ − 96
+ − 97
ML {*
+ − 98
fun eetac rule =
+ − 99
Subgoal.FOCUS_PARAMS (fn focus =>
+ − 100
let
+ − 101
val concl = #concl focus
+ − 102
val prems = Logic.strip_imp_prems (term_of concl)
+ − 103
val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
+ − 104
val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
+ − 105
val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
+ − 106
in
+ − 107
(etac rule THEN' RANGE[atac, eresolve_tac thins]) 1
+ − 108
end
+ − 109
)
+ − 110
*}
+ − 111
+ − 112
ML {*
+ − 113
fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
2108
+ − 114
rtac induct THEN_ALL_NEW
1830
+ − 115
(TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
+ − 116
asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW
+ − 117
split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
+ − 118
THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
+ − 119
THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
+ − 120
TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW
+ − 121
(asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
+ − 122
*}
+ − 123
+ − 124
lemma transpI:
+ − 125
"(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
+ − 126
unfolding transp_def
+ − 127
by blast
+ − 128
+ − 129
ML {*
+ − 130
fun equivp_tac reflps symps transps =
+ − 131
(*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *)
+ − 132
simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
+ − 133
THEN' rtac conjI THEN' rtac allI THEN'
+ − 134
resolve_tac reflps THEN'
+ − 135
rtac conjI THEN' rtac allI THEN' rtac allI THEN'
+ − 136
resolve_tac symps THEN'
+ − 137
rtac @{thm transpI} THEN' resolve_tac transps
+ − 138
*}
+ − 139
+ − 140
ML {*
+ − 141
fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
+ − 142
let
+ − 143
val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
+ − 144
val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z)
+ − 145
fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
+ − 146
fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
+ − 147
val symp_loc = Goal.prove ctxt' [] [] symg symp_tac';
+ − 148
val transp_loc = Goal.prove ctxt' [] [] transg transp_tac';
+ − 149
val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc]
+ − 150
val symps = HOLogic.conj_elims symp
+ − 151
val transps = HOLogic.conj_elims transp
+ − 152
fun equivp alpha =
+ − 153
let
+ − 154
val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
+ − 155
val goal = @{term Trueprop} $ (equivp $ alpha)
+ − 156
fun tac _ = equivp_tac reflps symps transps 1
+ − 157
in
+ − 158
Goal.prove ctxt [] [] goal tac
+ − 159
end
+ − 160
in
+ − 161
map equivp alphas
+ − 162
end
+ − 163
*}
+ − 164
+ − 165
lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
+ − 166
by auto
+ − 167
+ − 168
ML {*
+ − 169
fun supports_tac perm =
+ − 170
simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
+ − 171
REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN'
+ − 172
asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
+ − 173
swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh
+ − 174
supp_fset_to_set supp_fmap_atom}))
+ − 175
*}
+ − 176
+ − 177
ML {*
+ − 178
fun mk_supp ty x =
+ − 179
Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x
+ − 180
*}
+ − 181
+ − 182
ML {*
+ − 183
fun mk_supports_eq thy cnstr =
+ − 184
let
+ − 185
val (tys, ty) = (strip_type o fastype_of) cnstr
+ − 186
val names = Datatype_Prop.make_tnames tys
+ − 187
val frees = map Free (names ~~ tys)
+ − 188
val rhs = list_comb (cnstr, frees)
+ − 189
+ − 190
fun mk_supp_arg (x, ty) =
2008
1bddffddc03f
attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 191
if is_atom thy ty then mk_supp @{typ atom} (mk_atom_ty ty x) else
1830
+ − 192
if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else
+ − 193
if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x)
+ − 194
else mk_supp ty x
+ − 195
val lhss = map mk_supp_arg (frees ~~ tys)
+ − 196
val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 197
val eq = HOLogic.mk_Trueprop (supports $ fold_union lhss $ rhs)
1830
+ − 198
in
+ − 199
(names, eq)
+ − 200
end
+ − 201
*}
+ − 202
+ − 203
ML {*
+ − 204
fun prove_supports ctxt perms cnst =
+ − 205
let
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 206
val (names, eq) = mk_supports_eq ctxt cnst
1830
+ − 207
in
+ − 208
Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1)
+ − 209
end
+ − 210
*}
+ − 211
+ − 212
ML {*
+ − 213
fun mk_fs tys =
+ − 214
let
+ − 215
val names = Datatype_Prop.make_tnames tys
+ − 216
val frees = map Free (names ~~ tys)
+ − 217
val supps = map2 mk_supp tys frees
+ − 218
val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps
+ − 219
in
+ − 220
(names, HOLogic.mk_Trueprop (mk_conjl fin_supps))
+ − 221
end
+ − 222
*}
+ − 223
+ − 224
ML {*
2108
+ − 225
fun fs_tac induct supports = rtac induct THEN_ALL_NEW (
1830
+ − 226
rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
+ − 227
asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
+ − 228
supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})
+ − 229
*}
+ − 230
+ − 231
ML {*
+ − 232
fun prove_fs ctxt induct supports tys =
+ − 233
let
+ − 234
val (names, eq) = mk_fs tys
+ − 235
in
+ − 236
Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1)
+ − 237
end
+ − 238
*}
+ − 239
+ − 240
ML {*
+ − 241
fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x;
+ − 242
+ − 243
fun mk_supp_neq arg (fv, alpha) =
+ − 244
let
+ − 245
val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"});
+ − 246
val ty = fastype_of arg;
+ − 247
val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty);
+ − 248
val finite = @{term "finite :: atom set \<Rightarrow> bool"}
+ − 249
val rhs = collect $ Abs ("a", @{typ atom},
+ − 250
HOLogic.mk_not (finite $
+ − 251
(collect $ Abs ("b", @{typ atom},
+ − 252
HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg)))))
+ − 253
in
+ − 254
HOLogic.mk_eq (fv $ arg, rhs)
+ − 255
end;
+ − 256
+ − 257
fun supp_eq fv_alphas_lst =
+ − 258
let
+ − 259
val (fvs_alphas, ls) = split_list fv_alphas_lst;
+ − 260
val (fv_ts, _) = split_list fvs_alphas;
+ − 261
val tys = map (domain_type o fastype_of) fv_ts;
+ − 262
val names = Datatype_Prop.make_tnames tys;
+ − 263
val args = map Free (names ~~ tys);
+ − 264
fun supp_eq_arg ((fv, arg), l) =
+ − 265
mk_conjl
+ − 266
((HOLogic.mk_eq (fv $ arg, mk_supp arg)) ::
+ − 267
(map (mk_supp_neq arg) l))
+ − 268
val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls))
+ − 269
in
+ − 270
(names, HOLogic.mk_Trueprop eqs)
+ − 271
end
+ − 272
*}
+ − 273
+ − 274
ML {*
+ − 275
fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos =
+ − 276
if length fv_ts_bn < length alpha_ts_bn then
+ − 277
(fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) [])
+ − 278
else let
+ − 279
val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1);
+ − 280
fun filter_fn i (x, j) = if j = i then SOME x else NONE;
+ − 281
val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos;
+ − 282
val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos;
+ − 283
in
+ − 284
(fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all
+ − 285
end
+ − 286
*}
+ − 287
+ − 288
(* TODO: this is a hack, it assumes that only one type of Abs's is present
+ − 289
in the type and chooses this supp_abs. Additionally single atoms are
+ − 290
treated properly. *)
+ − 291
ML {*
+ − 292
fun choose_alpha_abs eqiff =
+ − 293
let
2070
+ − 294
fun exists_subterms f ts = member (op =) (map (exists_subterm f) ts) true;
1830
+ − 295
val terms = map prop_of eqiff;
+ − 296
fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms
+ − 297
val no =
+ − 298
if check @{const_name alpha_lst} then 2 else
+ − 299
if check @{const_name alpha_res} then 1 else
+ − 300
if check @{const_name alpha_gen} then 0 else
+ − 301
error "Failure choosing supp_abs"
+ − 302
in
+ − 303
nth @{thms supp_abs[symmetric]} no
+ − 304
end
+ − 305
*}
+ − 306
lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}"
+ − 307
by (rule supp_abs(1))
+ − 308
+ − 309
lemma supp_abs_sum:
+ − 310
"supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
+ − 311
"supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"
+ − 312
"supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))"
+ − 313
apply (simp_all add: supp_abs supp_Pair)
+ − 314
apply blast+
+ − 315
done
+ − 316
+ − 317
+ − 318
ML {*
+ − 319
fun supp_eq_tac ind fv perm eqiff ctxt =
2108
+ − 320
rtac ind THEN_ALL_NEW
1830
+ − 321
asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
+ − 322
asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW
+ − 323
asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW
+ − 324
simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
+ − 325
simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
+ − 326
simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW
+ − 327
simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
+ − 328
simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW
+ − 329
simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
+ − 330
asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
+ − 331
asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
+ − 332
simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
+ − 333
simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+ − 334
simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW
+ − 335
simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+ − 336
simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW
+ − 337
simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW
+ − 338
simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
+ − 339
*}
+ − 340
+ − 341
+ − 342
+ − 343
+ − 344
+ − 345
end