1(* Title: HOL/Tools/Function/function_core.ML 2 Author: Alexander Krauss, TU Muenchen 3 4Core of the function package. 5*) 6 7signature FUNCTION_CORE = 8sig 9 val trace: bool Unsynchronized.ref 10 val prepare_function : Function_Common.function_config 11 -> binding (* defname *) 12 -> ((binding * typ) * mixfix) list (* defined symbol *) 13 -> ((string * typ) list * term list * term * term) list (* specification *) 14 -> local_theory 15 -> (term (* f *) 16 * thm (* goalstate *) 17 * (Proof.context -> thm -> Function_Common.function_result) (* continuation *) 18 ) * local_theory 19 20end 21 22structure Function_Core : FUNCTION_CORE = 23struct 24 25val trace = Unsynchronized.ref false 26fun trace_msg msg = if ! trace then tracing (msg ()) else () 27 28val boolT = HOLogic.boolT 29val mk_eq = HOLogic.mk_eq 30 31open Function_Lib 32open Function_Common 33 34datatype globals = Globals of 35 {fvar: term, 36 domT: typ, 37 ranT: typ, 38 h: term, 39 y: term, 40 x: term, 41 z: term, 42 a: term, 43 P: term, 44 D: term, 45 Pbool:term} 46 47datatype rec_call_info = RCInfo of 48 {RIvs: (string * typ) list, (* Call context: fixes and assumes *) 49 CCas: thm list, 50 rcarg: term, (* The recursive argument *) 51 llRI: thm, 52 h_assum: term} 53 54 55datatype clause_context = ClauseContext of 56 {ctxt : Proof.context, 57 qs : term list, 58 gs : term list, 59 lhs: term, 60 rhs: term, 61 cqs: cterm list, 62 ags: thm list, 63 case_hyp : thm} 64 65 66fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) = 67 ClauseContext { ctxt = Proof_Context.transfer thy ctxt, 68 qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } 69 70 71datatype clause_info = ClauseInfo of 72 {no: int, 73 qglr : ((string * typ) list * term list * term * term), 74 cdata : clause_context, 75 tree: Function_Context_Tree.ctx_tree, 76 lGI: thm, 77 RCs: rec_call_info list} 78 79 80(* Theory dependencies. *) 81val acc_induct_rule = @{thm accp_induct_rule} 82 83val ex1_implies_ex = @{thm Fun_Def.fundef_ex1_existence} 84val ex1_implies_un = @{thm Fun_Def.fundef_ex1_uniqueness} 85val ex1_implies_iff = @{thm Fun_Def.fundef_ex1_iff} 86 87val acc_downward = @{thm accp_downward} 88val accI = @{thm accp.accI} 89 90 91fun find_calls tree = 92 let 93 fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = 94 ([], (fixes, assumes, arg) :: xs) 95 | add_Ri _ _ _ _ = raise Match 96 in 97 rev (Function_Context_Tree.traverse_tree add_Ri tree []) 98 end 99 100 101(** building proof obligations *) 102 103fun mk_compat_proof_obligations domT ranT fvar f glrs = 104 let 105 fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = 106 let 107 val shift = incr_boundvars (length qs') 108 in 109 Logic.mk_implies 110 (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), 111 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) 112 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') 113 |> fold_rev (fn (n,T) => fn b => Logic.all_const T $ Abs(n,T,b)) (qs @ qs') 114 |> curry abstract_over fvar 115 |> curry subst_bound f 116 end 117 in 118 map mk_impl (unordered_pairs glrs) 119 end 120 121 122fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs = 123 let 124 fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = 125 HOLogic.mk_Trueprop Pbool 126 |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs))) 127 |> fold_rev (curry Logic.mk_implies) gs 128 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) 129 in 130 HOLogic.mk_Trueprop Pbool 131 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) 132 |> mk_forall_rename ("x", x) 133 |> mk_forall_rename ("P", Pbool) 134 end 135 136(** making a context with it's own local bindings **) 137 138fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) = 139 let 140 val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt 141 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs 142 143 fun inst t = subst_bounds (rev qs, t) 144 val gs = map inst pre_gs 145 val lhs = inst pre_lhs 146 val rhs = inst pre_rhs 147 148 val cqs = map (Thm.cterm_of ctxt') qs 149 val ags = map (Thm.assume o Thm.cterm_of ctxt') gs 150 151 val case_hyp = 152 Thm.assume (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) 153 in 154 ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, 155 cqs = cqs, ags = ags, case_hyp = case_hyp } 156 end 157 158 159(* lowlevel term function. FIXME: remove *) 160fun abstract_over_list vs body = 161 let 162 fun abs lev v tm = 163 if v aconv tm then Bound lev 164 else 165 (case tm of 166 Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t) 167 | t $ u => abs lev v t $ abs lev v u 168 | t => t) 169 in 170 fold_index (fn (i, v) => fn t => abs i v t) vs body 171 end 172 173 174 175fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms = 176 let 177 val Globals {h, ...} = globals 178 179 val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata 180 181 (* Instantiate the GIntro thm with "f" and import into the clause context. *) 182 val lGI = GIntro_thm 183 |> Thm.forall_elim (Thm.cterm_of ctxt f) 184 |> fold Thm.forall_elim cqs 185 |> fold Thm.elim_implies ags 186 187 fun mk_call_info (rcfix, rcassm, rcarg) RI = 188 let 189 val llRI = RI 190 |> fold Thm.forall_elim cqs 191 |> fold (Thm.forall_elim o Thm.cterm_of ctxt o Free) rcfix 192 |> fold Thm.elim_implies ags 193 |> fold Thm.elim_implies rcassm 194 195 val h_assum = 196 HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) 197 |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm 198 |> fold_rev (Logic.all o Free) rcfix 199 |> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] [] 200 |> abstract_over_list (rev qs) 201 in 202 RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} 203 end 204 205 val RC_infos = map2 mk_call_info RCs RIntro_thms 206 in 207 ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos, 208 tree=tree} 209 end 210 211 212fun store_compat_thms 0 thms = [] 213 | store_compat_thms n thms = 214 let 215 val (thms1, thms2) = chop n thms 216 in 217 (thms1 :: store_compat_thms (n - 1) thms2) 218 end 219 220(* expects i <= j *) 221fun lookup_compat_thm i j cts = 222 nth (nth cts (i - 1)) (j - i) 223 224(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) 225(* if j < i, then turn around *) 226fun get_compat_thm ctxt cts i j ctxi ctxj = 227 let 228 val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi 229 val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj 230 231 val lhsi_eq_lhsj = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) 232 in if j < i then 233 let 234 val compat = lookup_compat_thm j i cts 235 in 236 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) 237 |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) 238 |> fold Thm.elim_implies agsj 239 |> fold Thm.elim_implies agsi 240 |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) 241 end 242 else 243 let 244 val compat = lookup_compat_thm i j cts 245 in 246 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) 247 |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) 248 |> fold Thm.elim_implies agsi 249 |> fold Thm.elim_implies agsj 250 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) 251 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) 252 end 253 end 254 255(* Generates the replacement lemma in fully quantified form. *) 256fun mk_replacement_lemma ctxt h ih_elim clause = 257 let 258 val ClauseInfo {cdata=ClauseContext {qs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause 259 local open Conv in 260 val ih_conv = arg1_conv o arg_conv o arg_conv 261 end 262 263 val ih_elim_case = 264 Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim 265 266 val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs 267 val h_assums = map (fn RCInfo {h_assum, ...} => 268 Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qs, h_assum)))) RCs 269 270 val (eql, _) = 271 Function_Context_Tree.rewrite_by_tree ctxt h ih_elim_case (Ris ~~ h_assums) tree 272 273 val replace_lemma = HOLogic.mk_obj_eq eql 274 |> Thm.implies_intr (Thm.cprop_of case_hyp) 275 |> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums 276 |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags 277 |> fold_rev Thm.forall_intr cqs 278 |> Thm.close_derivation 279 in 280 replace_lemma 281 end 282 283 284fun mk_uniqueness_clause ctxt globals compat_store clausei clausej RLj = 285 let 286 val thy = Proof_Context.theory_of ctxt 287 288 val Globals {h, y, x, fvar, ...} = globals 289 val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = 290 clausei 291 val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej 292 293 val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} = 294 mk_clause_context x ctxti cdescj 295 296 val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' 297 val compat = get_compat_thm ctxt compat_store i j cctxi cctxj 298 val Ghsj' = 299 map (fn RCInfo {h_assum, ...} => 300 Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qsj', h_assum)))) RCsj 301 302 val RLj_import = RLj 303 |> fold Thm.forall_elim cqsj' 304 |> fold Thm.elim_implies agsj' 305 |> fold Thm.elim_implies Ghsj' 306 307 val y_eq_rhsj'h = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) 308 val lhsi_eq_lhsj' = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) 309 (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) 310 in 311 (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) 312 |> Thm.implies_elim RLj_import 313 (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) 314 |> (fn it => trans OF [it, compat]) 315 (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) 316 |> (fn it => trans OF [y_eq_rhsj'h, it]) 317 (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) 318 |> fold_rev (Thm.implies_intr o Thm.cprop_of) Ghsj' 319 |> fold_rev (Thm.implies_intr o Thm.cprop_of) agsj' 320 (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) 321 |> Thm.implies_intr (Thm.cprop_of y_eq_rhsj'h) 322 |> Thm.implies_intr (Thm.cprop_of lhsi_eq_lhsj') 323 |> fold_rev Thm.forall_intr (Thm.cterm_of ctxt h :: cqsj') 324 end 325 326 327 328fun mk_uniqueness_case ctxt 329 globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = 330 let 331 val thy = Proof_Context.theory_of ctxt 332 val Globals {x, y, ranT, fvar, ...} = globals 333 val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei 334 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs 335 336 val ih_intro_case = full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ih_intro 337 338 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) 339 |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas 340 |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs 341 342 val existence = fold (curry op COMP o prep_RC) RCs lGI 343 344 val P = Thm.cterm_of ctxt (mk_eq (y, rhsC)) 345 val G_lhs_y = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y))) 346 347 val unique_clauses = 348 map2 (mk_uniqueness_clause ctxt globals compat_store clausei) clauses rep_lemmas 349 350 fun elim_implies_eta A AB = 351 Thm.bicompose (SOME ctxt) {flatten = false, match = true, incremented = false} 352 (false, A, 0) 1 AB 353 |> Seq.list_of |> the_single 354 355 val uniqueness = G_cases 356 |> Thm.forall_elim (Thm.cterm_of ctxt lhs) 357 |> Thm.forall_elim (Thm.cterm_of ctxt y) 358 |> Thm.forall_elim P 359 |> Thm.elim_implies G_lhs_y 360 |> fold elim_implies_eta unique_clauses 361 |> Thm.implies_intr (Thm.cprop_of G_lhs_y) 362 |> Thm.forall_intr (Thm.cterm_of ctxt y) 363 364 val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) 365 366 val exactly_one = 367 @{thm ex1I} 368 |> Thm.instantiate' 369 [SOME (Thm.ctyp_of ctxt ranT)] 370 [SOME P2, SOME (Thm.cterm_of ctxt rhsC)] 371 |> curry (op COMP) existence 372 |> curry (op COMP) uniqueness 373 |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym]) 374 |> Thm.implies_intr (Thm.cprop_of case_hyp) 375 |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags 376 |> fold_rev Thm.forall_intr cqs 377 378 val function_value = 379 existence 380 |> Thm.implies_intr ihyp 381 |> Thm.implies_intr (Thm.cprop_of case_hyp) 382 |> Thm.forall_intr (Thm.cterm_of ctxt x) 383 |> Thm.forall_elim (Thm.cterm_of ctxt lhs) 384 |> curry (op RS) refl 385 in 386 (exactly_one, function_value) 387 end 388 389 390fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def = 391 let 392 val Globals {h, domT, ranT, x, ...} = globals 393 394 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) 395 val ihyp = Logic.all_const domT $ Abs ("z", domT, 396 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), 397 HOLogic.mk_Trueprop (Const (\<^const_name>\<open>Ex1\<close>, (ranT --> boolT) --> boolT) $ 398 Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) 399 |> Thm.cterm_of ctxt 400 401 val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 402 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) 403 val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) 404 |> Thm.instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)] 405 406 val _ = trace_msg (K "Proving Replacement lemmas...") 407 val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses 408 409 val _ = trace_msg (K "Proving cases for unique existence...") 410 val (ex1s, values) = 411 split_list 412 (map 413 (mk_uniqueness_case ctxt globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) 414 clauses) 415 416 val _ = trace_msg (K "Proving: Graph is a function") 417 val graph_is_function = complete 418 |> Thm.forall_elim_vars 0 419 |> fold (curry op COMP) ex1s 420 |> Thm.implies_intr (ihyp) 421 |> Thm.implies_intr (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ x))) 422 |> Thm.forall_intr (Thm.cterm_of ctxt x) 423 |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) 424 |> (fn it => 425 fold (Thm.forall_intr o Thm.cterm_of ctxt o Var) 426 (Term.add_vars (Thm.prop_of it) []) it) 427 428 val goalstate = Conjunction.intr graph_is_function complete 429 |> Thm.close_derivation 430 |> Goal.protect 0 431 |> fold_rev (Thm.implies_intr o Thm.cprop_of) compat 432 |> Thm.implies_intr (Thm.cprop_of complete) 433 in 434 (goalstate, values) 435 end 436 437(* wrapper -- restores quantifiers in rule specifications *) 438fun inductive_def (binding as ((R, T), _)) intrs lthy = 439 let 440 val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) = 441 lthy 442 |> Proof_Context.concealed 443 |> Inductive.add_inductive_i 444 {quiet_mode = true, 445 verbose = ! trace, 446 alt_name = Binding.empty, 447 coind = false, 448 no_elim = false, 449 no_ind = false, 450 skip_mono = true} 451 [binding] (* relation *) 452 [] (* no parameters *) 453 (map (fn t => (Binding.empty_atts, t)) intrs) (* intro rules *) 454 [] (* no special monos *) 455 ||> Proof_Context.restore_naming lthy 456 457 fun requantify orig_intro thm = 458 let 459 val (qs, t) = dest_all_all orig_intro 460 val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T) 461 val vars = Term.add_vars (Thm.prop_of thm) [] 462 val varmap = AList.lookup (op =) (frees ~~ map fst vars) 463 #> the_default ("", 0) 464 in 465 fold_rev (fn Free (n, T) => 466 forall_intr_rename (n, Thm.cterm_of lthy (Var (varmap (n, T), T)))) qs thm 467 end 468 in 469 ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy) 470 end 471 472fun define_graph (G_binding, G_type) fvar clauses RCss lthy = 473 let 474 val G = Free (Binding.name_of G_binding, G_type) 475 fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs = 476 let 477 fun mk_h_assm (rcfix, rcassm, rcarg) = 478 HOLogic.mk_Trueprop (G $ rcarg $ (fvar $ rcarg)) 479 |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm 480 |> fold_rev (Logic.all o Free) rcfix 481 in 482 HOLogic.mk_Trueprop (G $ lhs $ rhs) 483 |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs 484 |> fold_rev (curry Logic.mk_implies) gs 485 |> fold_rev Logic.all (fvar :: qs) 486 end 487 488 val G_intros = map2 mk_GIntro clauses RCss 489 in inductive_def ((G_binding, G_type), NoSyn) G_intros lthy end 490 491fun define_function defname (fname, mixfix) domT ranT G default lthy = 492 let 493 val f_def_binding = 494 Thm.make_def_binding (Config.get lthy function_internals) 495 (derived_name_suffix defname "_sumC") 496 val f_def = 497 Abs ("x", domT, Const (\<^const_name>\<open>Fun_Def.THE_default\<close>, ranT --> (ranT --> boolT) --> ranT) 498 $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) 499 |> Syntax.check_term lthy 500 in 501 lthy |> Local_Theory.define 502 ((Binding.map_name (suffix "C") fname, mixfix), ((f_def_binding, []), f_def)) 503 end 504 505fun define_recursion_relation (R_binding, R_type) qglrs clauses RCss lthy = 506 let 507 val R = Free (Binding.name_of R_binding, R_type) 508 fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = 509 HOLogic.mk_Trueprop (R $ rcarg $ lhs) 510 |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm 511 |> fold_rev (curry Logic.mk_implies) gs 512 |> fold_rev (Logic.all o Free) rcfix 513 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) 514 (* "!!qs xs. CS ==> G => (r, lhs) : R" *) 515 516 val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss 517 518 val ((R, RIntro_thms, R_elim, _), lthy) = 519 inductive_def ((R_binding, R_type), NoSyn) (flat R_intross) lthy 520 in 521 ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy) 522 end 523 524 525fun fix_globals domT ranT fvar ctxt = 526 let 527 val ([h, y, x, z, a, D, P, Pbool], ctxt') = Variable.variant_fixes 528 ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt 529 in 530 (Globals {h = Free (h, domT --> ranT), 531 y = Free (y, ranT), 532 x = Free (x, domT), 533 z = Free (z, domT), 534 a = Free (a, domT), 535 D = Free (D, domT --> boolT), 536 P = Free (P, domT --> boolT), 537 Pbool = Free (Pbool, boolT), 538 fvar = fvar, 539 domT = domT, 540 ranT = ranT}, 541 ctxt') 542 end 543 544fun inst_RC ctxt fvar f (rcfix, rcassm, rcarg) = 545 let 546 fun inst_term t = subst_bound(f, abstract_over (fvar, t)) 547 in 548 (rcfix, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) rcassm, inst_term rcarg) 549 end 550 551 552 553(********************************************************** 554 * PROVING THE RULES 555 **********************************************************) 556 557fun mk_psimps ctxt globals R clauses valthms f_iff graph_is_function = 558 let 559 val Globals {domT, z, ...} = globals 560 561 fun mk_psimp 562 (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = 563 let 564 val lhs_acc = 565 Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) 566 val z_smaller = 567 Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) 568 in 569 ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward)) 570 |> (fn it => it COMP graph_is_function) 571 |> Thm.implies_intr z_smaller 572 |> Thm.forall_intr (Thm.cterm_of ctxt z) 573 |> (fn it => it COMP valthm) 574 |> Thm.implies_intr lhs_acc 575 |> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff]) 576 |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags 577 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) 578 end 579 in 580 map2 mk_psimp clauses valthms 581 end 582 583 584(** Induction rule **) 585 586 587val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct} 588 589 590fun mk_partial_induct_rule ctxt globals R complete_thm clauses = 591 let 592 val Globals {domT, x, z, a, P, D, ...} = globals 593 val acc_R = mk_acc domT R 594 595 val x_D = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ x))) 596 val a_D = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ a)) 597 598 val D_subset = 599 Thm.cterm_of ctxt (Logic.all x 600 (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) 601 602 val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) 603 Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), 604 Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), 605 HOLogic.mk_Trueprop (D $ z))))) 606 |> Thm.cterm_of ctxt 607 608 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) 609 val ihyp = Logic.all_const domT $ Abs ("z", domT, 610 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), 611 HOLogic.mk_Trueprop (P $ Bound 0))) 612 |> Thm.cterm_of ctxt 613 614 val aihyp = Thm.assume ihyp 615 616 fun prove_case clause = 617 let 618 val ClauseInfo {cdata = ClauseContext {ctxt = ctxt1, qs, cqs, ags, gs, lhs, case_hyp, ...}, 619 RCs, qglr = (oqs, _, _, _), ...} = clause 620 621 val case_hyp_conv = K (case_hyp RS eq_reflection) 622 local open Conv in 623 val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D 624 val sih = 625 fconv_rule (Conv.binder_conv 626 (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt1) aihyp 627 end 628 629 fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih 630 |> Thm.forall_elim (Thm.cterm_of ctxt rcarg) 631 |> Thm.elim_implies llRI 632 |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas 633 |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs 634 635 val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) 636 637 val step = HOLogic.mk_Trueprop (P $ lhs) 638 |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs 639 |> fold_rev (curry Logic.mk_implies) gs 640 |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) 641 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) 642 |> Thm.cterm_of ctxt 643 644 val P_lhs = Thm.assume step 645 |> fold Thm.forall_elim cqs 646 |> Thm.elim_implies lhs_D 647 |> fold Thm.elim_implies ags 648 |> fold Thm.elim_implies P_recs 649 650 val res = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P $ x)) 651 |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) 652 |> Thm.symmetric (* P lhs == P x *) 653 |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *) 654 |> Thm.implies_intr (Thm.cprop_of case_hyp) 655 |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags 656 |> fold_rev Thm.forall_intr cqs 657 in 658 (res, step) 659 end 660 661 val (cases, steps) = split_list (map prove_case clauses) 662 663 val istep = complete_thm 664 |> Thm.forall_elim_vars 0 665 |> fold (curry op COMP) cases (* P x *) 666 |> Thm.implies_intr ihyp 667 |> Thm.implies_intr (Thm.cprop_of x_D) 668 |> Thm.forall_intr (Thm.cterm_of ctxt x) 669 670 val subset_induct_rule = 671 acc_subset_induct 672 |> (curry op COMP) (Thm.assume D_subset) 673 |> (curry op COMP) (Thm.assume D_dcl) 674 |> (curry op COMP) (Thm.assume a_D) 675 |> (curry op COMP) istep 676 |> fold_rev Thm.implies_intr steps 677 |> Thm.implies_intr a_D 678 |> Thm.implies_intr D_dcl 679 |> Thm.implies_intr D_subset 680 681 val simple_induct_rule = 682 subset_induct_rule 683 |> Thm.forall_intr (Thm.cterm_of ctxt D) 684 |> Thm.forall_elim (Thm.cterm_of ctxt acc_R) 685 |> assume_tac ctxt 1 |> Seq.hd 686 |> (curry op COMP) (acc_downward 687 |> (Thm.instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z])) 688 |> Thm.forall_intr (Thm.cterm_of ctxt z) 689 |> Thm.forall_intr (Thm.cterm_of ctxt x)) 690 |> Thm.forall_intr (Thm.cterm_of ctxt a) 691 |> Thm.forall_intr (Thm.cterm_of ctxt P) 692 in 693 simple_induct_rule 694 end 695 696 697(* FIXME: broken by design *) 698fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = 699 let 700 val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, 701 qglr = (oqs, _, _, _), ...} = clause 702 val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) 703 |> fold_rev (curry Logic.mk_implies) gs 704 |> Thm.cterm_of ctxt 705 in 706 Goal.init goal 707 |> (SINGLE (resolve_tac ctxt [accI] 1)) |> the 708 |> (SINGLE (eresolve_tac ctxt [Thm.forall_elim_vars 0 R_cases] 1)) |> the 709 |> (SINGLE (auto_tac ctxt)) |> the 710 |> Goal.conclude 711 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) 712 end 713 714 715 716(** Termination rule **) 717 718val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} 719val wf_in_rel = @{thm Fun_Def.wf_in_rel} 720val in_rel_def = @{thm Fun_Def.in_rel_def} 721 722fun mk_nest_term_case ctxt globals R' ihyp clause = 723 let 724 val Globals {z, ...} = globals 725 val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, 726 qglr=(oqs, _, _, _), ...} = clause 727 728 val ih_case = full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ihyp 729 730 fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 731 let 732 val used = (u @ sub) 733 |> map (fn (ctx, thm) => Function_Context_Tree.export_thm ctxt ctx thm) 734 735 val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) 736 |> fold_rev (curry Logic.mk_implies o Thm.prop_of) used (* additional hyps *) 737 |> Function_Context_Tree.export_term (fixes, assumes) 738 |> fold_rev (curry Logic.mk_implies o Thm.prop_of) ags 739 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) 740 |> Thm.cterm_of ctxt 741 742 val thm = Thm.assume hyp 743 |> fold Thm.forall_elim cqs 744 |> fold Thm.elim_implies ags 745 |> Function_Context_Tree.import_thm ctxt (fixes, assumes) 746 |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) 747 748 val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg)) 749 |> Thm.cterm_of ctxt |> Thm.assume 750 751 val acc = thm COMP ih_case 752 val z_acc_local = acc 753 |> Conv.fconv_rule 754 (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection))))) 755 756 val ethm = z_acc_local 757 |> Function_Context_Tree.export_thm ctxt (fixes, 758 z_eq_arg :: case_hyp :: ags @ assumes) 759 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) 760 761 val sub' = sub @ [(([],[]), acc)] 762 in 763 (sub', (hyp :: hyps, ethm :: thms)) 764 end 765 | step _ _ _ _ = raise Match 766 in 767 Function_Context_Tree.traverse_tree step tree 768 end 769 770 771fun mk_nest_term_rule ctxt globals R R_cases clauses = 772 let 773 val Globals { domT, x, z, ... } = globals 774 val acc_R = mk_acc domT R 775 776 val ([Rn], ctxt') = Variable.variant_fixes ["R"] ctxt 777 val R' = Free (Rn, fastype_of R) 778 779 val Rrel = Free (Rn, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) 780 val inrel_R = Const (\<^const_name>\<open>Fun_Def.in_rel\<close>, 781 HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel 782 783 val wfR' = HOLogic.mk_Trueprop (Const (\<^const_name>\<open>Wellfounded.wfP\<close>, 784 (domT --> domT --> boolT) --> boolT) $ R') 785 |> Thm.cterm_of ctxt' (* "wf R'" *) 786 787 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) 788 val ihyp = Logic.all_const domT $ Abs ("z", domT, 789 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), 790 HOLogic.mk_Trueprop (acc_R $ Bound 0))) 791 |> Thm.cterm_of ctxt' 792 793 val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0 794 795 val R_z_x = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (R $ z $ x)) 796 797 val (hyps, cases) = fold (mk_nest_term_case ctxt' globals R' ihyp_a) clauses ([], []) 798 in 799 R_cases 800 |> Thm.forall_elim (Thm.cterm_of ctxt' z) 801 |> Thm.forall_elim (Thm.cterm_of ctxt' x) 802 |> Thm.forall_elim (Thm.cterm_of ctxt' (acc_R $ z)) 803 |> curry op COMP (Thm.assume R_z_x) 804 |> fold_rev (curry op COMP) cases 805 |> Thm.implies_intr R_z_x 806 |> Thm.forall_intr (Thm.cterm_of ctxt' z) 807 |> (fn it => it COMP accI) 808 |> Thm.implies_intr ihyp 809 |> Thm.forall_intr (Thm.cterm_of ctxt' x) 810 |> (fn it => Drule.compose (it, 2, wf_induct_rule)) 811 |> curry op RS (Thm.assume wfR') 812 |> forall_intr_vars 813 |> (fn it => it COMP allI) 814 |> fold Thm.implies_intr hyps 815 |> Thm.implies_intr wfR' 816 |> Thm.forall_intr (Thm.cterm_of ctxt' R') 817 |> Thm.forall_elim (Thm.cterm_of ctxt' inrel_R) 818 |> curry op RS wf_in_rel 819 |> full_simplify (put_simpset HOL_basic_ss ctxt' addsimps [in_rel_def]) 820 |> Thm.forall_intr_name ("R", Thm.cterm_of ctxt' Rrel) 821 end 822 823 824 825fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = 826 let 827 val FunctionConfig {domintros, default=default_opt, ...} = config 828 829 val default_str = the_default "%x. HOL.undefined" (* FIXME proper term!? *) default_opt 830 val fvar = (Binding.name_of fname, fT) 831 val domT = domain_type fT 832 val ranT = range_type fT 833 834 val default = Syntax.parse_term lthy default_str 835 |> Type.constraint fT |> Syntax.check_term lthy 836 837 val (globals, ctxt') = fix_globals domT ranT (Free fvar) lthy 838 839 val Globals { x, h, ... } = globals 840 841 val clauses = map (mk_clause_context x ctxt') abstract_qglrs 842 843 val n = length abstract_qglrs 844 845 fun build_tree (ClauseContext { ctxt, rhs, ...}) = 846 Function_Context_Tree.mk_tree (Free fvar) h ctxt rhs 847 848 val trees = map build_tree clauses 849 val RCss = map find_calls trees 850 851 val ((G, GIntro_thms, G_elim, G_induct), lthy) = 852 PROFILE "def_graph" 853 (define_graph 854 (derived_name_suffix defname "_graph", domT --> ranT --> boolT) (Free fvar) clauses RCss) 855 lthy 856 857 val ((f, (_, f_defthm)), lthy) = 858 PROFILE "def_fun" (define_function defname (fname, mixfix) domT ranT G default) lthy 859 860 val RCss = map (map (inst_RC lthy (Free fvar) f)) RCss 861 val trees = map (Function_Context_Tree.inst_tree lthy (Free fvar) f) trees 862 863 val ((R, RIntro_thmss, R_elim), lthy) = 864 PROFILE "def_rel" 865 (define_recursion_relation (derived_name_suffix defname "_rel", domT --> domT --> boolT) 866 abstract_qglrs clauses RCss) lthy 867 868 val dom = mk_acc domT R 869 val (_, lthy) = 870 Local_Theory.abbrev Syntax.mode_default 871 ((derived_name_suffix defname "_dom", NoSyn), dom) lthy 872 873 val newthy = Proof_Context.theory_of lthy 874 val clauses = map (transfer_clause_ctx newthy) clauses 875 876 val xclauses = PROFILE "xclauses" 877 (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees 878 RCss GIntro_thms) RIntro_thmss 879 880 val complete = 881 mk_completeness globals clauses abstract_qglrs |> Thm.cterm_of lthy |> Thm.assume 882 883 val compat = 884 mk_compat_proof_obligations domT ranT (Free fvar) f abstract_qglrs 885 |> map (Thm.cterm_of lthy #> Thm.assume) 886 887 val compat_store = store_compat_thms n compat 888 889 val (goalstate, values) = PROFILE "prove_stuff" 890 (prove_stuff lthy globals G f R xclauses complete compat 891 compat_store G_elim) f_defthm 892 893 fun mk_partial_rules newctxt provedgoal = 894 let 895 val (graph_is_function, complete_thm) = 896 provedgoal 897 |> Conjunction.elim 898 |> apfst (Thm.forall_elim_vars 0) 899 900 val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) 901 902 val psimps = PROFILE "Proving simplification rules" 903 (mk_psimps newctxt globals R xclauses values f_iff) graph_is_function 904 905 val simple_pinduct = PROFILE "Proving partial induction rule" 906 (mk_partial_induct_rule newctxt globals R complete_thm) xclauses 907 908 val total_intro = PROFILE "Proving nested termination rule" 909 (mk_nest_term_rule newctxt globals R R_elim) xclauses 910 911 val dom_intros = 912 if domintros then SOME (PROFILE "Proving domain introduction rules" 913 (map (mk_domain_intro lthy globals R R_elim)) xclauses) 914 else NONE 915 in 916 FunctionResult {fs=[f], G=G, R=R, dom=dom, 917 cases=[complete_thm], psimps=psimps, pelims=[], 918 simple_pinducts=[simple_pinduct], 919 termination=total_intro, domintros=dom_intros} 920 end 921 in 922 ((f, goalstate, mk_partial_rules), lthy) 923 end 924 925end 926