1795
+ − 1
theory TypeSchemes
2454
+ − 2
imports "../Nominal2"
1795
+ − 3
begin
+ − 4
+ − 5
section {*** Type Schemes ***}
+ − 6
2556
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 7
atom_decl name
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 8
2486
+ − 9
(* defined as a single nominal datatype *)
1795
+ − 10
+ − 11
nominal_datatype ty =
+ − 12
Var "name"
+ − 13
| Fun "ty" "ty"
+ − 14
and tys =
2714
+ − 15
All xs::"name fset" ty::"ty" bind (set+) xs in ty
2434
+ − 16
2885
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 17
ML {*
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 18
get_all_info @{context}
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 19
*}
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 20
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 21
ML {*
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 22
get_info @{context} "TypeSchemes.ty"
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23
*}
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 25
ML {*
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 26
#strong_exhaust (the_info @{context} "TypeSchemes.tys")
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 27
*}
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 28
2468
+ − 29
thm ty_tys.distinct
+ − 30
thm ty_tys.induct
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 31
thm ty_tys.inducts
2885
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 32
thm ty_tys.exhaust
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33
thm ty_tys.strong_exhaust
2468
+ − 34
thm ty_tys.fv_defs
+ − 35
thm ty_tys.bn_defs
+ − 36
thm ty_tys.perm_simps
+ − 37
thm ty_tys.eq_iff
+ − 38
thm ty_tys.fv_bn_eqvt
+ − 39
thm ty_tys.size_eqvt
+ − 40
thm ty_tys.supports
2493
+ − 41
thm ty_tys.supp
2494
+ − 42
thm ty_tys.fresh
1795
+ − 43
2707
+ − 44
fun
+ − 45
lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
+ − 46
where
+ − 47
"lookup [] Y = Var Y"
+ − 48
| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
+ − 49
+ − 50
lemma lookup_eqvt[eqvt]:
+ − 51
shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
+ − 52
apply(induct Ts T rule: lookup.induct)
+ − 53
apply(simp_all)
+ − 54
done
+ − 55
2709
+ − 56
lemma test:
2850
+ − 57
assumes a: "\<exists>y. f x = Inl y"
2709
+ − 58
shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
2850
+ − 59
using a
+ − 60
apply clarify
2709
+ − 61
apply(frule_tac p="p" in permute_boolI)
+ − 62
apply(simp (no_asm_use) only: eqvts)
+ − 63
apply(subst (asm) permute_fun_app_eq)
+ − 64
back
+ − 65
apply(simp)
+ − 66
done
+ − 67
2710
+ − 68
lemma test2:
2850
+ − 69
assumes a: "\<exists>y. f x = Inl y"
2710
+ − 70
shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"
2850
+ − 71
using a
+ − 72
apply clarify
2710
+ − 73
apply(frule_tac p="p" in permute_boolI)
+ − 74
apply(simp (no_asm_use) only: eqvts)
+ − 75
apply(subst (asm) permute_fun_app_eq)
+ − 76
back
2709
+ − 77
apply(simp)
2710
+ − 78
done
2709
+ − 79
2848
da7e6655cd4c
fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 80
nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
2838
+ − 81
subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
+ − 82
and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
+ − 83
where
+ − 84
"subst \<theta> (Var X) = lookup \<theta> X"
+ − 85
| "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
+ − 86
| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
2850
+ − 87
(*unfolding subst_substs_graph_def eqvt_def
+ − 88
apply rule
+ − 89
apply perm_simp
+ − 90
apply (subst test3)
+ − 91
defer
+ − 92
apply (subst test3)
+ − 93
defer
+ − 94
apply (subst test3)
+ − 95
defer
+ − 96
apply rule*)
2885
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 97
thm subst_substs_graph.intros
2707
+ − 98
apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
+ − 99
apply(simp add: eqvt_def)
+ − 100
apply(rule allI)
+ − 101
apply(simp add: permute_fun_def permute_bool_def)
+ − 102
apply(rule ext)
+ − 103
apply(rule ext)
+ − 104
apply(rule iffI)
+ − 105
apply(drule_tac x="p" in meta_spec)
+ − 106
apply(drule_tac x="- p \<bullet> x" in meta_spec)
+ − 107
apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+ − 108
apply(simp)
+ − 109
apply(drule_tac x="-p" in meta_spec)
+ − 110
apply(drule_tac x="x" in meta_spec)
+ − 111
apply(drule_tac x="xa" in meta_spec)
+ − 112
apply(simp)
2710
+ − 113
--"Eqvt One way"
2707
+ − 114
apply(erule subst_substs_graph.induct)
+ − 115
apply(perm_simp)
+ − 116
apply(rule subst_substs_graph.intros)
2709
+ − 117
apply(erule subst_substs_graph.cases)
+ − 118
apply(simp (no_asm_use) only: eqvts)
+ − 119
apply(subst test)
+ − 120
back
2850
+ − 121
apply (rule exI)
2709
+ − 122
apply(assumption)
+ − 123
apply(rotate_tac 1)
+ − 124
apply(erule subst_substs_graph.cases)
+ − 125
apply(subst test)
+ − 126
back
2850
+ − 127
apply (rule exI)
2709
+ − 128
apply(assumption)
+ − 129
apply(perm_simp)
+ − 130
apply(rule subst_substs_graph.intros)
+ − 131
apply(assumption)
+ − 132
apply(assumption)
+ − 133
apply(subst test)
+ − 134
back
2850
+ − 135
apply (rule exI)
2709
+ − 136
apply(assumption)
+ − 137
apply(perm_simp)
+ − 138
apply(rule subst_substs_graph.intros)
+ − 139
apply(assumption)
+ − 140
apply(assumption)
+ − 141
apply(simp)
+ − 142
--"A"
+ − 143
apply(simp (no_asm_use) only: eqvts)
+ − 144
apply(subst test)
+ − 145
back
2850
+ − 146
apply (rule exI)
2709
+ − 147
apply(assumption)
+ − 148
apply(rotate_tac 1)
+ − 149
apply(erule subst_substs_graph.cases)
+ − 150
apply(subst test)
+ − 151
back
2850
+ − 152
apply (rule exI)
2709
+ − 153
apply(assumption)
+ − 154
apply(perm_simp)
+ − 155
apply(rule subst_substs_graph.intros)
+ − 156
apply(assumption)
+ − 157
apply(assumption)
+ − 158
apply(subst test)
+ − 159
back
2850
+ − 160
apply (rule exI)
2709
+ − 161
apply(assumption)
+ − 162
apply(perm_simp)
+ − 163
apply(rule subst_substs_graph.intros)
+ − 164
apply(assumption)
+ − 165
apply(assumption)
+ − 166
apply(simp)
+ − 167
--"A"
+ − 168
apply(simp)
+ − 169
apply(erule subst_substs_graph.cases)
+ − 170
apply(simp (no_asm_use) only: eqvts)
+ − 171
apply(subst test)
+ − 172
back
+ − 173
back
2850
+ − 174
apply (rule exI)
2709
+ − 175
apply(assumption)
+ − 176
apply(rule subst_substs_graph.intros)
2710
+ − 177
apply (simp add: eqvts)
+ − 178
apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
+ − 179
apply (simp add: image_eqvt eqvts_raw eqvts)
+ − 180
apply (simp add: fresh_star_permute_iff)
2709
+ − 181
apply(perm_simp)
+ − 182
apply(assumption)
+ − 183
apply(simp (no_asm_use) only: eqvts)
+ − 184
apply(subst test)
+ − 185
back
+ − 186
back
2850
+ − 187
apply (rule exI)
2709
+ − 188
apply(assumption)
+ − 189
apply(rule subst_substs_graph.intros)
2710
+ − 190
apply (simp add: eqvts)
+ − 191
apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
+ − 192
apply (simp add: image_eqvt eqvts_raw eqvts)
+ − 193
apply (simp add: fresh_star_permute_iff)
2709
+ − 194
apply(perm_simp)
+ − 195
apply(assumption)
+ − 196
apply(simp)
2710
+ − 197
--"Eqvt done"
2822
23befefc6e73
cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 198
apply(rule TrueI)
2710
+ − 199
apply (case_tac x)
+ − 200
apply simp apply clarify
+ − 201
apply (rule_tac y="b" in ty_tys.exhaust(1))
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 202
apply (auto)[1]
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 203
apply (auto)[1]
2710
+ − 204
apply simp apply clarify
+ − 205
apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2))
2787
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 206
apply (auto)[1]
1a6593bc494d
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 207
apply (auto)[5]
2710
+ − 208
--"LAST GOAL"
+ − 209
apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
+ − 210
apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
+ − 211
apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")
2867
+ − 212
apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', Ta))")
2839
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 213
prefer 2
2710
+ − 214
apply (simp add: eqvt_at_def subst_def)
+ − 215
apply rule
+ − 216
apply (subst test2)
2850
+ − 217
apply (simp add: subst_substs_sumC_def)
2710
+ − 218
apply (simp add: THE_default_def)
2850
+ − 219
apply (case_tac "Ex1 (subst_substs_graph (Inl (\<theta>', T)))")
2710
+ − 220
prefer 2
+ − 221
apply simp
+ − 222
apply (simp add: the1_equality)
+ − 223
apply auto[1]
+ − 224
apply (erule_tac x="x" in allE)
+ − 225
apply simp
+ − 226
apply(cases rule: subst_substs_graph.cases)
+ − 227
apply assumption
+ − 228
apply (rule_tac x="lookup \<theta> X" in exI)
+ − 229
apply clarify
+ − 230
apply (rule the1_equality)
2867
+ − 231
apply blast apply assumption
2710
+ − 232
apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))
+ − 233
(Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
+ − 234
apply clarify
+ − 235
apply (rule the1_equality)
2867
+ − 236
apply blast apply assumption
2710
+ − 237
apply clarify
2850
+ − 238
apply simp
+ − 239
--"-"
2839
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 240
apply clarify
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 241
apply (frule supp_eqvt_at)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 242
apply (simp add: finite_supp)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 243
apply (erule Abs_res_fcb)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 244
apply (simp add: Abs_fresh_iff)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 245
apply (simp add: Abs_fresh_iff)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 246
apply auto[1]
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 247
apply (simp add: fresh_def fresh_star_def)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 248
apply (erule contra_subsetD)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 249
apply (simp add: supp_Pair)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 250
apply blast
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 251
apply clarify
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 252
apply (simp)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 253
apply (simp add: eqvt_at_def)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 254
apply (subst Abs_eq_iff)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 255
apply (rule_tac x="0::perm" in exI)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 256
apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 257
apply (simp add: alphas fresh_star_zero)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 258
apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 259
apply blast
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 260
apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 261
apply (simp add: supp_Pair eqvts eqvts_raw)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 262
apply auto[1]
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 263
apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 264
apply (simp add: fresh_star_def fresh_def)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 265
apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 266
apply (simp add: eqvts eqvts_raw)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 267
apply (simp add: fresh_star_def fresh_def)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 268
apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric])
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 269
apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 270
apply (erule subsetD)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 271
apply (simp add: supp_eqvt)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 272
apply (metis le_eqvt permute_boolI)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 273
apply (rule perm_supp_eq)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 274
apply (simp add: fresh_def fresh_star_def)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 275
apply blast
2850
+ − 276
done
2707
+ − 277
2676
+ − 278
section {* defined as two separate nominal datatypes *}
2486
+ − 279
2308
+ − 280
nominal_datatype ty2 =
+ − 281
Var2 "name"
+ − 282
| Fun2 "ty2" "ty2"
+ − 283
+ − 284
nominal_datatype tys2 =
2634
3ce1089cdbf3
changed res keyword to set+ for restrictions; comment by a referee
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 285
All2 xs::"name fset" ty::"ty2" bind (set+) xs in ty
2337
+ − 286
2468
+ − 287
thm tys2.distinct
2630
+ − 288
thm tys2.induct tys2.strong_induct
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 289
thm tys2.exhaust tys2.strong_exhaust
2468
+ − 290
thm tys2.fv_defs
+ − 291
thm tys2.bn_defs
+ − 292
thm tys2.perm_simps
+ − 293
thm tys2.eq_iff
+ − 294
thm tys2.fv_bn_eqvt
+ − 295
thm tys2.size_eqvt
+ − 296
thm tys2.supports
2493
+ − 297
thm tys2.supp
2494
+ − 298
thm tys2.fresh
2468
+ − 299
2676
+ − 300
fun
2707
+ − 301
lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
2676
+ − 302
where
2707
+ − 303
"lookup2 [] Y = Var2 Y"
+ − 304
| "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)"
2556
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 305
2707
+ − 306
lemma lookup2_eqvt[eqvt]:
+ − 307
shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"
2801
+ − 308
by (induct Ts T rule: lookup2.induct) simp_all
2676
+ − 309
2707
+ − 310
nominal_primrec
2859
+ − 311
subst2 :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
2676
+ − 312
where
2859
+ − 313
"subst2 \<theta> (Var2 X) = lookup2 \<theta> X"
+ − 314
| "subst2 \<theta> (Fun2 T1 T2) = Fun2 (subst2 \<theta> T1) (subst2 \<theta> T2)"
+ − 315
unfolding eqvt_def subst2_graph_def
2801
+ − 316
apply (rule, perm_simp, rule)
2822
23befefc6e73
cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 317
apply(rule TrueI)
2801
+ − 318
apply(case_tac x)
+ − 319
apply(rule_tac y="b" in ty2.exhaust)
+ − 320
apply(blast)
+ − 321
apply(blast)
+ − 322
apply(simp_all add: ty2.distinct)
+ − 323
done
2676
+ − 324
+ − 325
termination
2859
+ − 326
by lexicographic_order
2676
+ − 327
+ − 328
lemma subst_eqvt[eqvt]:
2859
+ − 329
shows "(p \<bullet> subst2 \<theta> T) = subst2 (p \<bullet> \<theta>) (p \<bullet> T)"
+ − 330
by (induct \<theta> T rule: subst2.induct) (simp_all add: lookup2_eqvt)
2676
+ − 331
2801
+ − 332
lemma supp_fun_app2_eqvt:
+ − 333
assumes e: "eqvt f"
+ − 334
shows "supp (f a b) \<subseteq> supp a \<union> supp b"
+ − 335
using supp_fun_app_eqvt[OF e] supp_fun_app
+ − 336
by blast
+ − 337
+ − 338
lemma supp_subst:
2859
+ − 339
"supp (subst2 \<theta> t) \<subseteq> supp \<theta> \<union> supp t"
2801
+ − 340
apply (rule supp_fun_app2_eqvt)
+ − 341
unfolding eqvt_def by (simp add: eqvts_raw)
+ − 342
+ − 343
lemma fresh_star_inter1:
+ − 344
"xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
+ − 345
unfolding fresh_star_def by blast
2830
297cff1d1048
FCB for res binding and simplified proof of subst for type schemes
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 346
2676
+ − 347
nominal_primrec
2859
+ − 348
substs2 :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
2676
+ − 349
where
2859
+ − 350
"fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs2 \<theta> (All2 xs t) = All2 xs (subst2 \<theta> t)"
+ − 351
unfolding eqvt_def substs2_graph_def
2801
+ − 352
apply (rule, perm_simp, rule)
2822
23befefc6e73
cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 353
apply auto[2]
2801
+ − 354
apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)
+ − 355
apply auto
2830
297cff1d1048
FCB for res binding and simplified proof of subst for type schemes
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 356
apply (erule Abs_res_fcb)
297cff1d1048
FCB for res binding and simplified proof of subst for type schemes
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 357
apply (simp add: Abs_fresh_iff)
2801
+ − 358
apply (simp add: Abs_fresh_iff)
+ − 359
apply auto[1]
2830
297cff1d1048
FCB for res binding and simplified proof of subst for type schemes
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 360
apply (simp add: fresh_def fresh_star_def)
2832
+ − 361
apply (rule contra_subsetD[OF supp_subst])
2801
+ − 362
apply simp
2830
297cff1d1048
FCB for res binding and simplified proof of subst for type schemes
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 363
apply blast
2832
+ − 364
apply clarify
2830
297cff1d1048
FCB for res binding and simplified proof of subst for type schemes
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 365
apply (simp add: subst_eqvt)
2801
+ − 366
apply (subst Abs_eq_iff)
+ − 367
apply (rule_tac x="0::perm" in exI)
2832
+ − 368
apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
2801
+ − 369
apply (simp add: alphas fresh_star_zero)
2859
+ − 370
apply (subgoal_tac "\<And>x. x \<in> supp (subst2 \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
2804
+ − 371
apply blast
2839
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 372
apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)")
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 373
apply (simp add: supp_Pair eqvts eqvts_raw)
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 374
apply auto[1]
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 375
apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")
2801
+ − 376
apply (simp add: fresh_star_def fresh_def)
2839
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 377
apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 378
apply (simp add: eqvts eqvts_raw)
2801
+ − 379
apply (simp add: fresh_star_def fresh_def)
2839
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 380
apply (drule subsetD[OF supp_subst])
bcf48a1cb24b
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 381
apply (simp add: supp_Pair)
2832
+ − 382
apply (rule perm_supp_eq)
+ − 383
apply (simp add: fresh_def fresh_star_def)
2801
+ − 384
apply blast
+ − 385
done
2676
+ − 386
+ − 387
+ − 388
text {* Some Tests about Alpha-Equality *}
1795
+ − 389
+ − 390
lemma
+ − 391
shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
2676
+ − 392
apply(simp add: ty_tys.eq_iff Abs_eq_iff)
1795
+ − 393
apply(rule_tac x="0::perm" in exI)
2676
+ − 394
apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
1795
+ − 395
done
+ − 396
+ − 397
lemma
+ − 398
shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 399
apply(simp add: ty_tys.eq_iff Abs_eq_iff)
1795
+ − 400
apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 401
apply(simp add: alphas fresh_star_def supp_at_base ty_tys.supp)
1795
+ − 402
done
+ − 403
+ − 404
lemma
+ − 405
shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 406
apply(simp add: ty_tys.eq_iff Abs_eq_iff)
1795
+ − 407
apply(rule_tac x="0::perm" in exI)
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 408
apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
1795
+ − 409
done
+ − 410
+ − 411
lemma
+ − 412
assumes a: "a \<noteq> b"
+ − 413
shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
+ − 414
using a
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 415
apply(simp add: ty_tys.eq_iff Abs_eq_iff)
1795
+ − 416
apply(clarify)
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 417
apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base)
1795
+ − 418
apply auto
+ − 419
done
+ − 420
2566
a59d8e1e3a17
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 421
1795
+ − 422
+ − 423
+ − 424
end