2665
+ − 1
(* Nominal Function Core
+ − 2
Author: Christian Urban
+ − 3
+ − 4
heavily based on the code of Alexander Krauss
+ − 5
(code forked on 14 January 2011)
+ − 6
+ − 7
Core of the nominal function package.
+ − 8
*)
+ − 9
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 10
2665
+ − 11
signature NOMINAL_FUNCTION_CORE =
+ − 12
sig
+ − 13
val trace: bool Unsynchronized.ref
+ − 14
2819
+ − 15
val prepare_nominal_function : Nominal_Function_Common.nominal_function_config
2665
+ − 16
-> string (* defname *)
+ − 17
-> ((bstring * typ) * mixfix) list (* defined symbol *)
+ − 18
-> ((bstring * typ) list * term list * term * term) list (* specification *)
+ − 19
-> local_theory
+ − 20
-> (term (* f *)
+ − 21
* thm (* goalstate *)
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 22
* (thm -> Function_Common.function_result) (* continuation *)
2665
+ − 23
) * local_theory
+ − 24
+ − 25
end
+ − 26
+ − 27
structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE =
+ − 28
struct
+ − 29
+ − 30
val trace = Unsynchronized.ref false
+ − 31
fun trace_msg msg = if ! trace then tracing (msg ()) else ()
+ − 32
+ − 33
val boolT = HOLogic.boolT
+ − 34
val mk_eq = HOLogic.mk_eq
+ − 35
+ − 36
open Function_Lib
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37
open Function_Common
2819
+ − 38
open Nominal_Function_Common
2665
+ − 39
+ − 40
datatype globals = Globals of
+ − 41
{fvar: term,
+ − 42
domT: typ,
+ − 43
ranT: typ,
+ − 44
h: term,
+ − 45
y: term,
+ − 46
x: term,
+ − 47
z: term,
+ − 48
a: term,
+ − 49
P: term,
+ − 50
D: term,
+ − 51
Pbool:term}
+ − 52
+ − 53
datatype rec_call_info = RCInfo of
+ − 54
{RIvs: (string * typ) list, (* Call context: fixes and assumes *)
+ − 55
CCas: thm list,
+ − 56
rcarg: term, (* The recursive argument *)
+ − 57
llRI: thm,
+ − 58
h_assum: term}
+ − 59
+ − 60
+ − 61
datatype clause_context = ClauseContext of
+ − 62
{ctxt : Proof.context,
+ − 63
qs : term list,
+ − 64
gs : term list,
+ − 65
lhs: term,
+ − 66
rhs: term,
+ − 67
cqs: cterm list,
+ − 68
ags: thm list,
+ − 69
case_hyp : thm}
+ − 70
+ − 71
+ − 72
fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
+ − 73
ClauseContext { ctxt = ProofContext.transfer thy ctxt,
+ − 74
qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
+ − 75
+ − 76
+ − 77
datatype clause_info = ClauseInfo of
+ − 78
{no: int,
+ − 79
qglr : ((string * typ) list * term list * term * term),
+ − 80
cdata : clause_context,
+ − 81
tree: Function_Ctx_Tree.ctx_tree,
+ − 82
lGI: thm,
+ − 83
RCs: rec_call_info list}
+ − 84
+ − 85
+ − 86
(* Theory dependencies. *)
+ − 87
val acc_induct_rule = @{thm accp_induct_rule}
+ − 88
+ − 89
val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}
+ − 90
val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}
+ − 91
val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}
+ − 92
+ − 93
val acc_downward = @{thm accp_downward}
+ − 94
val accI = @{thm accp.accI}
+ − 95
val case_split = @{thm HOL.case_split}
+ − 96
val fundef_default_value = @{thm FunDef.fundef_default_value}
+ − 97
val not_acc_down = @{thm not_accp_down}
+ − 98
+ − 99
+ − 100
+ − 101
fun find_calls tree =
+ − 102
let
+ − 103
fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) =
+ − 104
([], (fixes, assumes, arg) :: xs)
+ − 105
| add_Ri _ _ _ _ = raise Match
+ − 106
in
+ − 107
rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
+ − 108
end
+ − 109
+ − 110
(* nominal *)
+ − 111
fun mk_eqvt_at (f_trm, arg_trm) =
+ − 112
let
+ − 113
val f_ty = fastype_of f_trm
+ − 114
val arg_ty = domain_type f_ty
+ − 115
in
+ − 116
Const (@{const_name eqvt_at}, [f_ty, arg_ty] ---> @{typ bool}) $ f_trm $ arg_trm
+ − 117
|> HOLogic.mk_Trueprop
+ − 118
end
+ − 119
2707
+ − 120
fun mk_eqvt trm =
+ − 121
let
+ − 122
val ty = fastype_of trm
+ − 123
in
+ − 124
Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm
+ − 125
|> HOLogic.mk_Trueprop
+ − 126
end
+ − 127
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 128
fun mk_inv inv (f_trm, arg_trm) =
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 129
betapplys (inv, [arg_trm, (f_trm $ arg_trm)])
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 130
|> HOLogic.mk_Trueprop
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 131
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 132
fun mk_invariant (Globals {x, y, ...}) G invariant =
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 133
let
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 134
val prem = HOLogic.mk_Trueprop (G $ x $ y)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 135
val concl = HOLogic.mk_Trueprop (betapplys (invariant, [x, y]))
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 136
in
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 137
Logic.mk_implies (prem, concl)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 138
|> mk_forall_rename ("y", y)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 139
|> mk_forall_rename ("x", x)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 140
end
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 141
2790
+ − 142
(** building proof obligations *)
2802
+ − 143
fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) =
2789
32979078bfe9
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 144
mk_eqvt_at (fvar, arg)
2803
+ − 145
|> curry Logic.list_implies (map prop_of assms)
2802
+ − 146
|> curry Term.list_all_free vs
2789
32979078bfe9
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 147
|> curry Term.list_abs_free qs
32979078bfe9
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 148
|> strip_abs_body
2665
+ − 149
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 150
fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) =
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 151
mk_inv inv (fvar, arg)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 152
|> curry Logic.list_implies (map prop_of assms)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
|> curry Term.list_all_free vs
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 154
|> curry Term.list_abs_free qs
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 155
|> strip_abs_body
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 156
2665
+ − 157
(** building proof obligations *)
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 158
fun mk_compat_proof_obligations domT ranT fvar f RCss inv glrs =
2665
+ − 159
let
2862
+ − 160
fun mk_impl (((qs, gs, lhs, rhs), RCs_lhs), ((qs', gs', lhs', rhs'), RCs_rhs)) =
2665
+ − 161
let
+ − 162
val shift = incr_boundvars (length qs')
2862
+ − 163
val eqvts_obligations_lhs = map (shift o mk_eqvt_proof_obligation qs fvar) RCs_lhs
+ − 164
val eqvts_obligations_rhs = map (mk_eqvt_proof_obligation qs' fvar) RCs_rhs
+ − 165
val invs_obligations_lhs = map (shift o mk_inv_proof_obligation inv qs fvar) RCs_lhs
+ − 166
val invs_obligations_rhs = map (mk_inv_proof_obligation inv qs' fvar) RCs_rhs
2665
+ − 167
in
+ − 168
Logic.mk_implies
+ − 169
(HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
+ − 170
HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
+ − 171
|> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
2862
+ − 172
|> fold_rev (curry Logic.mk_implies) invs_obligations_rhs (* nominal *)
+ − 173
|> fold_rev (curry Logic.mk_implies) invs_obligations_lhs (* nominal *)
+ − 174
|> fold_rev (curry Logic.mk_implies) eqvts_obligations_rhs (* nominal *)
+ − 175
|> fold_rev (curry Logic.mk_implies) eqvts_obligations_lhs (* nominal *)
2665
+ − 176
|> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
+ − 177
|> curry abstract_over fvar
+ − 178
|> curry subst_bound f
+ − 179
end
+ − 180
in
2789
32979078bfe9
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 181
map mk_impl (unordered_pairs (glrs ~~ RCss))
2665
+ − 182
end
+ − 183
+ − 184
fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
+ − 185
let
+ − 186
fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
+ − 187
HOLogic.mk_Trueprop Pbool
+ − 188
|> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
+ − 189
|> fold_rev (curry Logic.mk_implies) gs
+ − 190
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ − 191
in
+ − 192
HOLogic.mk_Trueprop Pbool
+ − 193
|> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
+ − 194
|> mk_forall_rename ("x", x)
+ − 195
|> mk_forall_rename ("P", Pbool)
+ − 196
end
+ − 197
+ − 198
(** making a context with it's own local bindings **)
+ − 199
+ − 200
fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
+ − 201
let
+ − 202
val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
+ − 203
|>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
+ − 204
+ − 205
val thy = ProofContext.theory_of ctxt'
+ − 206
+ − 207
fun inst t = subst_bounds (rev qs, t)
+ − 208
val gs = map inst pre_gs
+ − 209
val lhs = inst pre_lhs
+ − 210
val rhs = inst pre_rhs
+ − 211
+ − 212
val cqs = map (cterm_of thy) qs
+ − 213
val ags = map (Thm.assume o cterm_of thy) gs
+ − 214
+ − 215
val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
+ − 216
in
+ − 217
ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
+ − 218
cqs = cqs, ags = ags, case_hyp = case_hyp }
+ − 219
end
+ − 220
+ − 221
+ − 222
(* lowlevel term function. FIXME: remove *)
+ − 223
fun abstract_over_list vs body =
+ − 224
let
+ − 225
fun abs lev v tm =
+ − 226
if v aconv tm then Bound lev
+ − 227
else
+ − 228
(case tm of
+ − 229
Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
+ − 230
| t $ u => abs lev v t $ abs lev v u
+ − 231
| t => t)
+ − 232
in
+ − 233
fold_index (fn (i, v) => fn t => abs i v t) vs body
+ − 234
end
+ − 235
+ − 236
+ − 237
+ − 238
fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
+ − 239
let
+ − 240
val Globals {h, ...} = globals
+ − 241
+ − 242
val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
+ − 243
val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+ − 244
+ − 245
(* Instantiate the GIntro thm with "f" and import into the clause context. *)
+ − 246
val lGI = GIntro_thm
+ − 247
|> Thm.forall_elim (cert f)
+ − 248
|> fold Thm.forall_elim cqs
+ − 249
|> fold Thm.elim_implies ags
+ − 250
+ − 251
fun mk_call_info (rcfix, rcassm, rcarg) RI =
+ − 252
let
+ − 253
val llRI = RI
+ − 254
|> fold Thm.forall_elim cqs
+ − 255
|> fold (Thm.forall_elim o cert o Free) rcfix
+ − 256
|> fold Thm.elim_implies ags
+ − 257
|> fold Thm.elim_implies rcassm
+ − 258
+ − 259
val h_assum =
+ − 260
HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
+ − 261
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ − 262
|> fold_rev (Logic.all o Free) rcfix
+ − 263
|> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
+ − 264
|> abstract_over_list (rev qs)
+ − 265
in
+ − 266
RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
+ − 267
end
+ − 268
+ − 269
val RC_infos = map2 mk_call_info RCs RIntro_thms
+ − 270
in
+ − 271
ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos,
+ − 272
tree=tree}
+ − 273
end
+ − 274
+ − 275
+ − 276
fun store_compat_thms 0 thms = []
+ − 277
| store_compat_thms n thms =
+ − 278
let
+ − 279
val (thms1, thms2) = chop n thms
+ − 280
in
+ − 281
(thms1 :: store_compat_thms (n - 1) thms2)
+ − 282
end
+ − 283
+ − 284
(* expects i <= j *)
+ − 285
fun lookup_compat_thm i j cts =
+ − 286
nth (nth cts (i - 1)) (j - i)
+ − 287
+ − 288
(* nominal *)
+ − 289
(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
+ − 290
(* if j < i, then turn around *)
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 291
fun get_compat_thm thy cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj =
2665
+ − 292
let
2789
32979078bfe9
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 293
val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi
32979078bfe9
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 294
val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj
2665
+ − 295
+ − 296
val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
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
+ − 297
2665
+ − 298
in if j < i then
+ − 299
let
+ − 300
val compat = lookup_compat_thm j i cts
+ − 301
in
+ − 302
compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
+ − 303
|> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
2789
32979078bfe9
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 304
|> fold Thm.elim_implies eqvtsj (* nominal *)
2862
+ − 305
|> fold Thm.elim_implies eqvtsi (* nominal *)
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 306
|> fold Thm.elim_implies invsj (* nominal *)
2862
+ − 307
|> fold Thm.elim_implies invsi (* nominal *)
2665
+ − 308
|> fold Thm.elim_implies agsj
+ − 309
|> fold Thm.elim_implies agsi
+ − 310
|> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
+ − 311
end
+ − 312
else
+ − 313
let
+ − 314
val compat = lookup_compat_thm i j cts
+ − 315
in
+ − 316
compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
+ − 317
|> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
2789
32979078bfe9
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 318
|> fold Thm.elim_implies eqvtsi (* nominal *)
2862
+ − 319
|> fold Thm.elim_implies eqvtsj (* nominal *)
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 320
|> fold Thm.elim_implies invsi (* nominal *)
2862
+ − 321
|> fold Thm.elim_implies invsj (* nominal *)
2665
+ − 322
|> fold Thm.elim_implies agsi
+ − 323
|> fold Thm.elim_implies agsj
+ − 324
|> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
+ − 325
|> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
+ − 326
end
+ − 327
end
+ − 328
+ − 329
+ − 330
(* Generates the replacement lemma in fully quantified form. *)
+ − 331
fun mk_replacement_lemma thy h ih_elim clause =
+ − 332
let
+ − 333
val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
+ − 334
RCs, tree, ...} = clause
+ − 335
local open Conv in
+ − 336
val ih_conv = arg1_conv o arg_conv o arg_conv
+ − 337
end
+ − 338
+ − 339
val ih_elim_case =
+ − 340
Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
+ − 341
+ − 342
val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
+ − 343
val h_assums = map (fn RCInfo {h_assum, ...} =>
+ − 344
Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
+ − 345
+ − 346
val (eql, _) =
+ − 347
Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
+ − 348
+ − 349
val replace_lemma = (eql RS meta_eq_to_obj_eq)
+ − 350
|> Thm.implies_intr (cprop_of case_hyp)
+ − 351
|> fold_rev (Thm.implies_intr o cprop_of) h_assums
+ − 352
|> fold_rev (Thm.implies_intr o cprop_of) ags
+ − 353
|> fold_rev Thm.forall_intr cqs
+ − 354
|> Thm.close_derivation
+ − 355
in
+ − 356
replace_lemma
+ − 357
end
+ − 358
+ − 359
(* nominal *)
+ − 360
(* Generates the eqvt lemmas for each clause *)
+ − 361
fun mk_eqvt_lemma thy ih_eqvt clause =
+ − 362
let
+ − 363
val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
2789
32979078bfe9
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 364
2665
+ − 365
local open Conv in
+ − 366
val ih_conv = arg1_conv o arg_conv o arg_conv
+ − 367
end
+ − 368
+ − 369
val ih_eqvt_case =
+ − 370
Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt
+ − 371
+ − 372
fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) =
+ − 373
(llRI RS ih_eqvt_case)
+ − 374
|> fold_rev (Thm.implies_intr o cprop_of) CCas
2802
+ − 375
|> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
2665
+ − 376
in
+ − 377
map prep_eqvt RCs
+ − 378
|> map (fold_rev (Thm.implies_intr o cprop_of) ags)
+ − 379
|> map (Thm.implies_intr (cprop_of case_hyp))
+ − 380
|> map (fold_rev Thm.forall_intr cqs)
+ − 381
|> map (Thm.close_derivation)
+ − 382
end
+ − 383
+ − 384
(* nominal *)
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 385
fun mk_invariant_lemma thy ih_inv clause =
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 386
let
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 387
val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 388
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 389
local open Conv in
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 390
val ih_conv = arg1_conv o arg_conv o arg_conv
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 391
end
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 392
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 393
val ih_inv_case =
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 394
Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_inv
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 395
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 396
fun prep_inv (RCInfo {llRI, RIvs, CCas, ...}) =
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 397
(llRI RS ih_inv_case)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 398
|> fold_rev (Thm.implies_intr o cprop_of) CCas
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 399
|> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 400
in
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 401
map prep_inv RCs
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 402
|> map (fold_rev (Thm.implies_intr o cprop_of) ags)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 403
|> map (Thm.implies_intr (cprop_of case_hyp))
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 404
|> map (fold_rev Thm.forall_intr cqs)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 405
|> map (Thm.close_derivation)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 406
end
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 407
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 408
(* nominal *)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 409
fun mk_uniqueness_clause thy globals compat_store eqvts invs clausei clausej RLj =
2665
+ − 410
let
+ − 411
val Globals {h, y, x, fvar, ...} = globals
+ − 412
val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi,
+ − 413
ags = agsi, ...}, ...} = clausei
+ − 414
val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
+ − 415
+ − 416
val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} =
+ − 417
mk_clause_context x ctxti cdescj
+ − 418
+ − 419
val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
+ − 420
+ − 421
val Ghsj' = map
+ − 422
(fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
+ − 423
+ − 424
val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
+ − 425
val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
+ − 426
(* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
+ − 427
+ − 428
val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']
+ − 429
+ − 430
val RLj_import = RLj
+ − 431
|> fold Thm.forall_elim cqsj'
+ − 432
|> fold Thm.elim_implies agsj'
+ − 433
|> fold Thm.elim_implies Ghsj'
+ − 434
+ − 435
val eqvtsi = nth eqvts (i - 1)
+ − 436
|> map (fold Thm.forall_elim cqsi)
+ − 437
|> map (fold Thm.elim_implies [case_hyp])
+ − 438
|> map (fold Thm.elim_implies agsi)
+ − 439
+ − 440
val eqvtsj = nth eqvts (j - 1)
+ − 441
|> map (fold Thm.forall_elim cqsj')
+ − 442
|> map (fold Thm.elim_implies [case_hypj'])
+ − 443
|> map (fold Thm.elim_implies agsj')
+ − 444
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 445
val invsi = nth invs (i - 1)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 446
|> map (fold Thm.forall_elim cqsi)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 447
|> map (fold Thm.elim_implies [case_hyp])
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 448
|> map (fold Thm.elim_implies agsi)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 449
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 450
val invsj = nth invs (j - 1)
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 451
|> map (fold Thm.forall_elim cqsj')
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 452
|> map (fold Thm.elim_implies [case_hypj'])
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 453
|> map (fold Thm.elim_implies agsj')
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 454
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 455
val compat = get_compat_thm thy compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj
2665
+ − 456
+ − 457
in
+ − 458
(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
+ − 459
|> Thm.implies_elim RLj_import
+ − 460
(* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
+ − 461
|> (fn it => trans OF [it, compat])
+ − 462
(* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
+ − 463
|> (fn it => trans OF [y_eq_rhsj'h, it])
+ − 464
(* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
+ − 465
|> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
+ − 466
|> fold_rev (Thm.implies_intr o cprop_of) agsj'
+ − 467
(* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
+ − 468
|> Thm.implies_intr (cprop_of y_eq_rhsj'h)
+ − 469
|> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
+ − 470
|> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
+ − 471
end
+ − 472
+ − 473
(* nominal *)
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 474
fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 475
clausei =
2665
+ − 476
let
+ − 477
val Globals {x, y, ranT, fvar, ...} = globals
+ − 478
val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
+ − 479
val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
+ − 480
+ − 481
val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
+ − 482
+ − 483
fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) =
+ − 484
(llRI RS ih_intro_case)
+ − 485
|> fold_rev (Thm.implies_intr o cprop_of) CCas
+ − 486
|> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
2789
32979078bfe9
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 487
2665
+ − 488
val existence = fold (curry op COMP o prep_RC) RCs lGI
+ − 489
+ − 490
val P = cterm_of thy (mk_eq (y, rhsC))
+ − 491
val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
+ − 492
+ − 493
val unique_clauses =
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 494
map2 (mk_uniqueness_clause thy globals compat_store eqvtlems invlems clausei) clauses replems
2665
+ − 495
+ − 496
fun elim_implies_eta A AB =
+ − 497
Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
2789
32979078bfe9
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 498
2665
+ − 499
val uniqueness = G_cases
+ − 500
|> Thm.forall_elim (cterm_of thy lhs)
+ − 501
|> Thm.forall_elim (cterm_of thy y)
+ − 502
|> Thm.forall_elim P
+ − 503
|> Thm.elim_implies G_lhs_y
+ − 504
|> fold elim_implies_eta unique_clauses
+ − 505
|> Thm.implies_intr (cprop_of G_lhs_y)
+ − 506
|> Thm.forall_intr (cterm_of thy y)
+ − 507
+ − 508
val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
+ − 509
+ − 510
val exactly_one =
+ − 511
ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
+ − 512
|> curry (op COMP) existence
+ − 513
|> curry (op COMP) uniqueness
+ − 514
|> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
+ − 515
|> Thm.implies_intr (cprop_of case_hyp)
+ − 516
|> fold_rev (Thm.implies_intr o cprop_of) ags
+ − 517
|> fold_rev Thm.forall_intr cqs
+ − 518
+ − 519
val function_value =
+ − 520
existence
+ − 521
|> Thm.implies_intr ihyp
+ − 522
|> Thm.implies_intr (cprop_of case_hyp)
+ − 523
|> Thm.forall_intr (cterm_of thy x)
+ − 524
|> Thm.forall_elim (cterm_of thy lhs)
+ − 525
|> curry (op RS) refl
+ − 526
in
+ − 527
(exactly_one, function_value)
+ − 528
end
+ − 529
+ − 530
+ − 531
(* nominal *)
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 532
fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def =
2665
+ − 533
let
+ − 534
val Globals {h, domT, ranT, x, ...} = globals
+ − 535
val thy = ProofContext.theory_of ctxt
+ − 536
+ − 537
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
+ − 538
val ihyp = Term.all domT $ Abs ("z", domT,
+ − 539
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
+ − 540
HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
+ − 541
Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
+ − 542
|> cterm_of thy
+ − 543
+ − 544
val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
+ − 545
val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
+ − 546
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
+ − 547
|> instantiate' [] [NONE, SOME (cterm_of thy h)]
+ − 548
val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 549
val ih_inv = ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop}))
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 550
2665
+ − 551
val _ = trace_msg (K "Proving Replacement lemmas...")
+ − 552
val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
+ − 553
+ − 554
val _ = trace_msg (K "Proving Equivariance lemmas...")
+ − 555
val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses
+ − 556
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 557
val _ = trace_msg (K "Proving Invariance lemmas...")
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 558
val invLemmas = map (mk_invariant_lemma thy ih_inv) clauses
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 559
2665
+ − 560
val _ = trace_msg (K "Proving cases for unique existence...")
+ − 561
val (ex1s, values) =
+ − 562
split_list (map (mk_uniqueness_case thy globals G f
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 563
ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas invLemmas) clauses)
2665
+ − 564
+ − 565
val _ = trace_msg (K "Proving: Graph is a function")
+ − 566
val graph_is_function = complete
+ − 567
|> Thm.forall_elim_vars 0
+ − 568
|> fold (curry op COMP) ex1s
+ − 569
|> Thm.implies_intr (ihyp)
+ − 570
|> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
+ − 571
|> Thm.forall_intr (cterm_of thy x)
+ − 572
|> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
+ − 573
|> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
+ − 574
2707
+ − 575
val goalstate =
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 576
Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt
2665
+ − 577
|> Thm.close_derivation
+ − 578
|> Goal.protect
+ − 579
|> fold_rev (Thm.implies_intr o cprop_of) compat
+ − 580
|> Thm.implies_intr (cprop_of complete)
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 581
|> Thm.implies_intr (cprop_of invariant)
2707
+ − 582
|> Thm.implies_intr (cprop_of G_eqvt)
2665
+ − 583
in
+ − 584
(goalstate, values)
+ − 585
end
+ − 586
+ − 587
(* wrapper -- restores quantifiers in rule specifications *)
2707
+ − 588
fun inductive_def (binding as ((R, T), _)) intrs lthy =
2665
+ − 589
let
+ − 590
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
+ − 591
lthy
2885
1264f2a21ea9
some rudimentary infrastructure for storing data about nominal datatypes
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 592
|> Local_Theory.conceal
2665
+ − 593
|> Inductive.add_inductive_i
+ − 594
{quiet_mode = true,
+ − 595
verbose = ! trace,
+ − 596
alt_name = Binding.empty,
+ − 597
coind = false,
+ − 598
no_elim = false,
+ − 599
no_ind = false,
+ − 600
skip_mono = true,
+ − 601
fork_mono = false}
+ − 602
[binding] (* relation *)
+ − 603
[] (* no parameters *)
+ − 604
(map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
+ − 605
[] (* no special monos *)
+ − 606
||> Local_Theory.restore_naming lthy
+ − 607
+ − 608
val cert = cterm_of (ProofContext.theory_of lthy)
+ − 609
fun requantify orig_intro thm =
+ − 610
let
+ − 611
val (qs, t) = dest_all_all orig_intro
2781
+ − 612
val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T)
+ − 613
val vars = Term.add_vars (prop_of thm) []
2665
+ − 614
val varmap = AList.lookup (op =) (frees ~~ map fst vars)
2781
+ − 615
#> the_default ("",0)
2665
+ − 616
in
+ − 617
fold_rev (fn Free (n, T) =>
+ − 618
forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
+ − 619
end
+ − 620
in
2707
+ − 621
((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
2665
+ − 622
end
+ − 623
+ − 624
(* nominal *)
+ − 625
fun define_graph Gname fvar domT ranT clauses RCss lthy =
+ − 626
let
+ − 627
val GT = domT --> ranT --> boolT
+ − 628
val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT)
+ − 629
+ − 630
fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
+ − 631
let
+ − 632
fun mk_h_assm (rcfix, rcassm, rcarg) =
+ − 633
HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
+ − 634
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ − 635
|> fold_rev (Logic.all o Free) rcfix
+ − 636
in
+ − 637
HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
+ − 638
|> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
+ − 639
|> fold_rev (curry Logic.mk_implies) gs
+ − 640
|> fold_rev Logic.all (fvar :: qs)
+ − 641
end
+ − 642
+ − 643
val G_intros = map2 mk_GIntro clauses RCss
+ − 644
in
2707
+ − 645
inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
2665
+ − 646
end
+ − 647
+ − 648
fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
+ − 649
let
+ − 650
val f_def =
+ − 651
Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT)
+ − 652
$ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
+ − 653
|> Syntax.check_term lthy
+ − 654
in
+ − 655
Local_Theory.define
+ − 656
((Binding.name (function_name fname), mixfix),
+ − 657
((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
+ − 658
end
+ − 659
+ − 660
(* nominal *)
+ − 661
fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
+ − 662
let
+ − 663
val RT = domT --> domT --> boolT
+ − 664
val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
+ − 665
+ − 666
fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
+ − 667
HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
+ − 668
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ − 669
|> fold_rev (curry Logic.mk_implies) gs
+ − 670
|> fold_rev (Logic.all o Free) rcfix
+ − 671
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ − 672
(* "!!qs xs. CS ==> G => (r, lhs) : R" *)
+ − 673
+ − 674
val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
+ − 675
2707
+ − 676
val ((R, RIntro_thms, R_elim, _), lthy) =
+ − 677
inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
2665
+ − 678
in
+ − 679
((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
+ − 680
end
+ − 681
+ − 682
+ − 683
fun fix_globals domT ranT fvar ctxt =
+ − 684
let
+ − 685
val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes
+ − 686
["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
+ − 687
in
+ − 688
(Globals {h = Free (h, domT --> ranT),
+ − 689
y = Free (y, ranT),
+ − 690
x = Free (x, domT),
+ − 691
z = Free (z, domT),
+ − 692
a = Free (a, domT),
+ − 693
D = Free (D, domT --> boolT),
+ − 694
P = Free (P, domT --> boolT),
+ − 695
Pbool = Free (Pbool, boolT),
+ − 696
fvar = fvar,
+ − 697
domT = domT,
+ − 698
ranT = ranT},
+ − 699
ctxt')
+ − 700
end
+ − 701
+ − 702
fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
+ − 703
let
+ − 704
fun inst_term t = subst_bound(f, abstract_over (fvar, t))
+ − 705
in
+ − 706
(rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
+ − 707
end
+ − 708
+ − 709
+ − 710
+ − 711
(**********************************************************
+ − 712
* PROVING THE RULES
+ − 713
**********************************************************)
+ − 714
+ − 715
fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
+ − 716
let
+ − 717
val Globals {domT, z, ...} = globals
+ − 718
+ − 719
fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
+ − 720
let
+ − 721
val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+ − 722
val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
+ − 723
in
+ − 724
((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))
+ − 725
|> (fn it => it COMP graph_is_function)
+ − 726
|> Thm.implies_intr z_smaller
+ − 727
|> Thm.forall_intr (cterm_of thy z)
+ − 728
|> (fn it => it COMP valthm)
+ − 729
|> Thm.implies_intr lhs_acc
+ − 730
|> asm_simplify (HOL_basic_ss addsimps [f_iff])
+ − 731
|> fold_rev (Thm.implies_intr o cprop_of) ags
+ − 732
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+ − 733
end
+ − 734
in
+ − 735
map2 mk_psimp clauses valthms
+ − 736
end
+ − 737
+ − 738
+ − 739
(** Induction rule **)
+ − 740
+ − 741
+ − 742
val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct}
+ − 743
+ − 744
+ − 745
fun mk_partial_induct_rule thy globals R complete_thm clauses =
+ − 746
let
+ − 747
val Globals {domT, x, z, a, P, D, ...} = globals
+ − 748
val acc_R = mk_acc domT R
+ − 749
+ − 750
val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
+ − 751
val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
+ − 752
+ − 753
val D_subset = cterm_of thy (Logic.all x
+ − 754
(Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
+ − 755
+ − 756
val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
+ − 757
Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
+ − 758
Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
+ − 759
HOLogic.mk_Trueprop (D $ z)))))
+ − 760
|> cterm_of thy
+ − 761
+ − 762
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
+ − 763
val ihyp = Term.all domT $ Abs ("z", domT,
+ − 764
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
+ − 765
HOLogic.mk_Trueprop (P $ Bound 0)))
+ − 766
|> cterm_of thy
+ − 767
+ − 768
val aihyp = Thm.assume ihyp
+ − 769
+ − 770
fun prove_case clause =
+ − 771
let
+ − 772
val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...},
+ − 773
RCs, qglr = (oqs, _, _, _), ...} = clause
+ − 774
+ − 775
val case_hyp_conv = K (case_hyp RS eq_reflection)
+ − 776
local open Conv in
+ − 777
val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
+ − 778
val sih =
+ − 779
fconv_rule (Conv.binder_conv
+ − 780
(K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
+ − 781
end
+ − 782
+ − 783
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
+ − 784
|> Thm.forall_elim (cterm_of thy rcarg)
+ − 785
|> Thm.elim_implies llRI
+ − 786
|> fold_rev (Thm.implies_intr o cprop_of) CCas
+ − 787
|> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+ − 788
+ − 789
val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
+ − 790
+ − 791
val step = HOLogic.mk_Trueprop (P $ lhs)
+ − 792
|> fold_rev (curry Logic.mk_implies o prop_of) P_recs
+ − 793
|> fold_rev (curry Logic.mk_implies) gs
+ − 794
|> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
+ − 795
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ − 796
|> cterm_of thy
+ − 797
+ − 798
val P_lhs = Thm.assume step
+ − 799
|> fold Thm.forall_elim cqs
+ − 800
|> Thm.elim_implies lhs_D
+ − 801
|> fold Thm.elim_implies ags
+ − 802
|> fold Thm.elim_implies P_recs
+ − 803
+ − 804
val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
+ − 805
|> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
+ − 806
|> Thm.symmetric (* P lhs == P x *)
+ − 807
|> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)
+ − 808
|> Thm.implies_intr (cprop_of case_hyp)
+ − 809
|> fold_rev (Thm.implies_intr o cprop_of) ags
+ − 810
|> fold_rev Thm.forall_intr cqs
+ − 811
in
+ − 812
(res, step)
+ − 813
end
+ − 814
+ − 815
val (cases, steps) = split_list (map prove_case clauses)
+ − 816
+ − 817
val istep = complete_thm
+ − 818
|> Thm.forall_elim_vars 0
+ − 819
|> fold (curry op COMP) cases (* P x *)
+ − 820
|> Thm.implies_intr ihyp
+ − 821
|> Thm.implies_intr (cprop_of x_D)
+ − 822
|> Thm.forall_intr (cterm_of thy x)
+ − 823
+ − 824
val subset_induct_rule =
+ − 825
acc_subset_induct
+ − 826
|> (curry op COMP) (Thm.assume D_subset)
+ − 827
|> (curry op COMP) (Thm.assume D_dcl)
+ − 828
|> (curry op COMP) (Thm.assume a_D)
+ − 829
|> (curry op COMP) istep
+ − 830
|> fold_rev Thm.implies_intr steps
+ − 831
|> Thm.implies_intr a_D
+ − 832
|> Thm.implies_intr D_dcl
+ − 833
|> Thm.implies_intr D_subset
+ − 834
+ − 835
val simple_induct_rule =
+ − 836
subset_induct_rule
+ − 837
|> Thm.forall_intr (cterm_of thy D)
+ − 838
|> Thm.forall_elim (cterm_of thy acc_R)
+ − 839
|> assume_tac 1 |> Seq.hd
+ − 840
|> (curry op COMP) (acc_downward
+ − 841
|> (instantiate' [SOME (ctyp_of thy domT)]
+ − 842
(map (SOME o cterm_of thy) [R, x, z]))
+ − 843
|> Thm.forall_intr (cterm_of thy z)
+ − 844
|> Thm.forall_intr (cterm_of thy x))
+ − 845
|> Thm.forall_intr (cterm_of thy a)
+ − 846
|> Thm.forall_intr (cterm_of thy P)
+ − 847
in
+ − 848
simple_induct_rule
+ − 849
end
+ − 850
+ − 851
+ − 852
(* FIXME: broken by design *)
+ − 853
fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
+ − 854
let
+ − 855
val thy = ProofContext.theory_of ctxt
+ − 856
val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
+ − 857
qglr = (oqs, _, _, _), ...} = clause
+ − 858
val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
+ − 859
|> fold_rev (curry Logic.mk_implies) gs
+ − 860
|> cterm_of thy
+ − 861
in
+ − 862
Goal.init goal
+ − 863
|> (SINGLE (resolve_tac [accI] 1)) |> the
+ − 864
|> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
2788
+ − 865
|> (SINGLE (auto_tac ctxt)) |> the
2665
+ − 866
|> Goal.conclude
+ − 867
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+ − 868
end
+ − 869
+ − 870
+ − 871
+ − 872
(** Termination rule **)
+ − 873
+ − 874
val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
+ − 875
val wf_in_rel = @{thm FunDef.wf_in_rel}
+ − 876
val in_rel_def = @{thm FunDef.in_rel_def}
+ − 877
+ − 878
fun mk_nest_term_case thy globals R' ihyp clause =
+ − 879
let
+ − 880
val Globals {z, ...} = globals
+ − 881
val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree,
+ − 882
qglr=(oqs, _, _, _), ...} = clause
+ − 883
+ − 884
val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
+ − 885
+ − 886
fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
+ − 887
let
+ − 888
val used = (u @ sub)
+ − 889
|> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm)
+ − 890
+ − 891
val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
+ − 892
|> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
+ − 893
|> Function_Ctx_Tree.export_term (fixes, assumes)
+ − 894
|> fold_rev (curry Logic.mk_implies o prop_of) ags
+ − 895
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ − 896
|> cterm_of thy
+ − 897
+ − 898
val thm = Thm.assume hyp
+ − 899
|> fold Thm.forall_elim cqs
+ − 900
|> fold Thm.elim_implies ags
+ − 901
|> Function_Ctx_Tree.import_thm thy (fixes, assumes)
+ − 902
|> fold Thm.elim_implies used (* "(arg, lhs) : R'" *)
+ − 903
+ − 904
val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
+ − 905
|> cterm_of thy |> Thm.assume
+ − 906
+ − 907
val acc = thm COMP ih_case
+ − 908
val z_acc_local = acc
+ − 909
|> Conv.fconv_rule
+ − 910
(Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
+ − 911
+ − 912
val ethm = z_acc_local
+ − 913
|> Function_Ctx_Tree.export_thm thy (fixes,
+ − 914
z_eq_arg :: case_hyp :: ags @ assumes)
+ − 915
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+ − 916
+ − 917
val sub' = sub @ [(([],[]), acc)]
+ − 918
in
+ − 919
(sub', (hyp :: hyps, ethm :: thms))
+ − 920
end
+ − 921
| step _ _ _ _ = raise Match
+ − 922
in
+ − 923
Function_Ctx_Tree.traverse_tree step tree
+ − 924
end
+ − 925
+ − 926
+ − 927
fun mk_nest_term_rule thy globals R R_cases clauses =
+ − 928
let
+ − 929
val Globals { domT, x, z, ... } = globals
+ − 930
val acc_R = mk_acc domT R
+ − 931
+ − 932
val R' = Free ("R", fastype_of R)
+ − 933
+ − 934
val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
+ − 935
val inrel_R = Const (@{const_name FunDef.in_rel},
+ − 936
HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
+ − 937
+ − 938
val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
+ − 939
(domT --> domT --> boolT) --> boolT) $ R')
+ − 940
|> cterm_of thy (* "wf R'" *)
+ − 941
+ − 942
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
+ − 943
val ihyp = Term.all domT $ Abs ("z", domT,
+ − 944
Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
+ − 945
HOLogic.mk_Trueprop (acc_R $ Bound 0)))
+ − 946
|> cterm_of thy
+ − 947
+ − 948
val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
+ − 949
+ − 950
val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
+ − 951
+ − 952
val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])
+ − 953
in
+ − 954
R_cases
+ − 955
|> Thm.forall_elim (cterm_of thy z)
+ − 956
|> Thm.forall_elim (cterm_of thy x)
+ − 957
|> Thm.forall_elim (cterm_of thy (acc_R $ z))
+ − 958
|> curry op COMP (Thm.assume R_z_x)
+ − 959
|> fold_rev (curry op COMP) cases
+ − 960
|> Thm.implies_intr R_z_x
+ − 961
|> Thm.forall_intr (cterm_of thy z)
+ − 962
|> (fn it => it COMP accI)
+ − 963
|> Thm.implies_intr ihyp
+ − 964
|> Thm.forall_intr (cterm_of thy x)
+ − 965
|> (fn it => Drule.compose_single(it,2,wf_induct_rule))
+ − 966
|> curry op RS (Thm.assume wfR')
+ − 967
|> forall_intr_vars
+ − 968
|> (fn it => it COMP allI)
+ − 969
|> fold Thm.implies_intr hyps
+ − 970
|> Thm.implies_intr wfR'
+ − 971
|> Thm.forall_intr (cterm_of thy R')
+ − 972
|> Thm.forall_elim (cterm_of thy (inrel_R))
+ − 973
|> curry op RS wf_in_rel
+ − 974
|> full_simplify (HOL_basic_ss addsimps [in_rel_def])
+ − 975
|> Thm.forall_intr (cterm_of thy Rrel)
+ − 976
end
+ − 977
+ − 978
+ − 979
+ − 980
(* nominal *)
+ − 981
fun prepare_nominal_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
+ − 982
let
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 983
val NominalFunctionConfig {domintros, default=default_opt, inv=invariant_opt,...} = config
2665
+ − 984
+ − 985
val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 986
val invariant_str = the_default "%x y. True" invariant_opt
2665
+ − 987
val fvar = Free (fname, fT)
+ − 988
val domT = domain_type fT
+ − 989
val ranT = range_type fT
+ − 990
+ − 991
val default = Syntax.parse_term lthy default_str
+ − 992
|> Type.constraint fT |> Syntax.check_term lthy
+ − 993
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 994
val invariant_trm = Syntax.parse_term lthy invariant_str
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 995
|> Type.constraint ([domT, ranT] ---> @{typ bool}) |> Syntax.check_term lthy
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 996
2665
+ − 997
val (globals, ctxt') = fix_globals domT ranT fvar lthy
+ − 998
+ − 999
val Globals { x, h, ... } = globals
+ − 1000
+ − 1001
val clauses = map (mk_clause_context x ctxt') abstract_qglrs
+ − 1002
+ − 1003
val n = length abstract_qglrs
+ − 1004
+ − 1005
fun build_tree (ClauseContext { ctxt, rhs, ...}) =
+ − 1006
Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
+ − 1007
+ − 1008
val trees = map build_tree clauses
+ − 1009
val RCss = map find_calls trees
+ − 1010
2707
+ − 1011
val ((G, GIntro_thms, G_elim, G_induct), lthy) =
2665
+ − 1012
PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
+ − 1013
+ − 1014
val ((f, (_, f_defthm)), lthy) =
+ − 1015
PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
+ − 1016
+ − 1017
val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
+ − 1018
val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
+ − 1019
+ − 1020
val ((R, RIntro_thmss, R_elim), lthy) =
+ − 1021
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
+ − 1022
+ − 1023
val (_, lthy) =
+ − 1024
Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
+ − 1025
+ − 1026
val newthy = ProofContext.theory_of lthy
+ − 1027
val clauses = map (transfer_clause_ctx newthy) clauses
+ − 1028
+ − 1029
val cert = cterm_of (ProofContext.theory_of lthy)
+ − 1030
+ − 1031
val xclauses = PROFILE "xclauses"
+ − 1032
(map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
+ − 1033
RCss GIntro_thms) RIntro_thmss
+ − 1034
+ − 1035
val complete =
+ − 1036
mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
+ − 1037
+ − 1038
val compat =
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1039
mk_compat_proof_obligations domT ranT fvar f RCss invariant_trm abstract_qglrs
2665
+ − 1040
|> map (cert #> Thm.assume)
+ − 1041
2707
+ − 1042
val G_eqvt = mk_eqvt G |> cert |> Thm.assume
+ − 1043
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1044
val invariant = mk_invariant globals G invariant_trm |> cert |> Thm.assume
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1045
2665
+ − 1046
val compat_store = store_compat_thms n compat
+ − 1047
+ − 1048
val (goalstate, values) = PROFILE "prove_stuff"
+ − 1049
(prove_stuff lthy globals G f R xclauses complete compat
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1050
compat_store G_elim G_eqvt invariant) f_defthm
2665
+ − 1051
+ − 1052
fun mk_partial_rules provedgoal =
+ − 1053
let
+ − 1054
val newthy = theory_of_thm provedgoal (*FIXME*)
+ − 1055
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1056
val (graph_is_function, complete_thm) =
2665
+ − 1057
provedgoal
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1058
|> fst o Conjunction.elim
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1059
|> fst o Conjunction.elim
2665
+ − 1060
|> Conjunction.elim
2821
c7d4bd9e89e0
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1061
|> apfst (Thm.forall_elim_vars 0)
2665
+ − 1062
+ − 1063
val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
+ − 1064
+ − 1065
val psimps = PROFILE "Proving simplification rules"
+ − 1066
(mk_psimps newthy globals R xclauses values f_iff) graph_is_function
+ − 1067
+ − 1068
val simple_pinduct = PROFILE "Proving partial induction rule"
+ − 1069
(mk_partial_induct_rule newthy globals R complete_thm) xclauses
+ − 1070
+ − 1071
val total_intro = PROFILE "Proving nested termination rule"
+ − 1072
(mk_nest_term_rule newthy globals R R_elim) xclauses
+ − 1073
+ − 1074
val dom_intros =
+ − 1075
if domintros then SOME (PROFILE "Proving domain introduction rules"
+ − 1076
(map (mk_domain_intro lthy globals R R_elim)) xclauses)
+ − 1077
else NONE
+ − 1078
+ − 1079
in
+ − 1080
FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
+ − 1081
psimps=psimps, simple_pinducts=[simple_pinduct],
2745
34df2cffe259
ported changes from function package....needs Isabelle 16 March or above
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1082
termination=total_intro, domintros=dom_intros}
2665
+ − 1083
end
+ − 1084
in
+ − 1085
((f, goalstate, mk_partial_rules), lthy)
+ − 1086
end
+ − 1087
+ − 1088
+ − 1089
end