397 val _ = message "Proving equations for size function ..."; |
397 val _ = message "Proving equations for size function ..."; |
398 |
398 |
399 val big_name = space_implode "_" new_type_names; |
399 val big_name = space_implode "_" new_type_names; |
400 val thy1 = add_path flat_names big_name thy; |
400 val thy1 = add_path flat_names big_name thy; |
401 |
401 |
402 val descr' = List.concat descr; |
402 val descr' = flat descr; |
403 val recTs = get_rec_types descr' sorts; |
403 val recTs = get_rec_types descr' sorts; |
404 |
404 |
405 val size_name = "Nat.size"; |
405 val size_name = "Nat.size"; |
406 val size_names = replicate (length (hd descr)) size_name @ |
406 val size_names = replicate (length (hd descr)) size_name @ |
407 map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names |
407 map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names |
412 fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2; |
412 fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2; |
413 |
413 |
414 fun make_sizefun (_, cargs) = |
414 fun make_sizefun (_, cargs) = |
415 let |
415 let |
416 val Ts = map (typ_of_dtyp descr' sorts) cargs; |
416 val Ts = map (typ_of_dtyp descr' sorts) cargs; |
417 val k = length (List.filter is_rec_type cargs); |
417 val k = length (filter is_rec_type cargs); |
418 val t = if k = 0 then HOLogic.zero else |
418 val t = if k = 0 then HOLogic.zero else |
419 foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1]) |
419 foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1]) |
420 in |
420 in |
421 foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT) |
421 foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT) |
422 end; |
422 end; |
423 |
423 |
424 val fs = List.concat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr'); |
424 val fs = maps (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr'; |
425 val fTs = map fastype_of fs; |
425 val fTs = map fastype_of fs; |
|
426 |
|
427 fun instance_size_class tyco thy = |
|
428 let |
|
429 val size_sort = ["Nat.size"]; |
|
430 val n = Sign.arity_number thy tyco; |
|
431 in |
|
432 thy |
|
433 |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, size_sort) |
|
434 (ClassPackage.intro_classes_tac []) |
|
435 end |
426 |
436 |
427 val (size_def_thms, thy') = |
437 val (size_def_thms, thy') = |
428 thy1 |
438 thy1 |
429 |> Theory.add_consts_i (map (fn (s, T) => |
439 |> Theory.add_consts_i (map (fn (s, T) => |
430 (Sign.base_name s, T --> HOLogic.natT, NoSyn)) |
440 (Sign.base_name s, T --> HOLogic.natT, NoSyn)) |
431 (Library.drop (length (hd descr), size_names ~~ recTs))) |
441 (Library.drop (length (hd descr), size_names ~~ recTs))) |
432 |> (PureThy.add_defs_i true o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) => |
442 |> fold (fn (_, (name, _, _)) => instance_size_class name) descr' |
|
443 |> PureThy.add_defs_i true (map (Thm.no_attributes o (fn (((s, T), def_name), rec_name) => |
433 (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT), |
444 (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT), |
434 list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs)))) |
445 list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))) |
435 (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |
446 (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |
436 ||> parent_path flat_names; |
447 ||> parent_path flat_names; |
437 |
448 |
438 val rewrites = size_def_thms @ map mk_meta_eq primrec_thms; |
449 val rewrites = size_def_thms @ map mk_meta_eq primrec_thms; |
439 |
450 |