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