author  krauss 
Wed, 02 Aug 2006 18:33:46 +0200  
changeset 20285  23f5cd23c1e1 
parent 20270  3abe7dae681e 
child 20320  a5368278a72c 
permissions  rwrr 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

1 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

2 
(* Title: HOL/Tools/function_package/fundef_package.ML 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

3 
ID: $Id$ 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

4 
Author: Alexander Krauss, TU Muenchen 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

5 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

6 
A package for general recursive function definitions. 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

7 
Isar commands. 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

8 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

9 
*) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

10 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

11 
signature FUNDEF_PACKAGE = 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

12 
sig 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

13 
val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list > bool > theory > Proof.state (* Need an _i variant *) 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

14 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

15 
val cong_add: attribute 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

16 
val cong_del: attribute 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

17 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

18 
val setup : theory > theory 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

19 
val get_congs : theory > thm list 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

20 
end 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

21 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

22 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

23 
structure FundefPackage : FUNDEF_PACKAGE = 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

24 
struct 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

25 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

26 
open FundefCommon 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

27 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

28 
val True_implies = thm "True_implies" 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

29 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

30 

20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

31 
fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy = 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

32 
let 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

33 
val psimpss = Library.unflat (map snd spec_part) psimps 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

34 
val (names, attss) = split_list (map fst spec_part) 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

35 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

36 
val thy = thy > Theory.add_path f_name 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

37 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

38 
val thy = thy > Theory.add_path label 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

39 
val spsimpss = map (map standard) psimpss (* FIXME *) 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

40 
val add_list = (names ~~ spsimpss) ~~ attss 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

41 
val (_, thy) = PureThy.add_thmss add_list thy 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

42 
val thy = thy > Theory.parent_path 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

43 

20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

44 
val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

45 
val thy = thy > Theory.parent_path 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

46 
in 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

47 
thy 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

48 
end 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

49 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

50 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

51 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

52 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

53 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

54 

20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

55 
fun fundef_afterqed congs mutual_info name data spec [[result]] thy = 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

56 
let 
19922  57 
val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result 
58 
val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data 

59 
val Mutual {parts, ...} = mutual_info 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

60 

19583
c5fa77b03442
functionpackage: Changed record usage to make sml/nj happy...
krauss
parents:
19564
diff
changeset

61 
val Prep {names = Names {acc_R=accR, ...}, ...} = data 
c5fa77b03442
functionpackage: Changed record usage to make sml/nj happy...
krauss
parents:
19564
diff
changeset

62 
val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR) 
c5fa77b03442
functionpackage: Changed record usage to make sml/nj happy...
krauss
parents:
19564
diff
changeset

63 
val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

64 

20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

65 
val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

66 

3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

67 
val casenames = flat (map (map (fst o fst)) spec) 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

68 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

69 
val thy = thy > Theory.add_path name 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

70 
val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

71 
val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy 
19922  72 
val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

73 
val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

74 
val thy = thy > Theory.parent_path 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

75 
in 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

76 
add_fundef_data name (fundef_data, mutual_info, spec) thy 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

77 
end 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

78 

20285  79 
fun gen_add_fundef prep_att eqns_attss (preprocess : bool) thy = 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

80 
let 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

81 
fun prep_eqns neqs = 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

82 
neqs 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

83 
> map (apsnd (Sign.read_prop thy)) 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

84 
> map (apfst (apsnd (apfst (map (prep_att thy))))) 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

85 
> FundefSplit.split_some_equations (ProofContext.init thy) 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

86 

3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

87 
val spec = map prep_eqns eqns_attss 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

88 
val t_eqnss = map (flat o map snd) spec 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

89 

20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

90 
(* 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

91 
val t_eqns = if preprocess then map (FundefSplit.split_all_equations (ProofContext.init thy)) t_eqns 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

92 
else t_eqns 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

93 
*) 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

94 

20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

95 
val congs = get_fundef_congs (Context.Theory thy) 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

96 

20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

97 
val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

98 
val Prep {goal, goalI, ...} = data 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

99 
in 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

100 
thy > ProofContext.init 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

101 
> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data spec) NONE ("", []) 
19922  102 
[(("", []), [(goal, [])])] 
103 
> Proof.refine (Method.primitive_text (fn _ => goalI)) 

104 
> Seq.hd 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

105 
end 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

106 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

107 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

108 
fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy = 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

109 
let 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

110 
val totality = hd (hd thmss) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

111 

20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

112 
val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec) 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

113 
= the (get_fundef_data name thy) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

114 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

115 
val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies]) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

116 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

117 
val tsimps = map (map remove_domain_condition) psimps 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

118 
val tinduct = map remove_domain_condition simple_pinducts 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

119 

19784
fa5080577da9
HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
krauss
parents:
19782
diff
changeset

120 
val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false  _ => true) o prop_of) (flat tsimps) 
fa5080577da9
HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
krauss
parents:
19782
diff
changeset

121 
val allatts = if has_guards then [] else [RecfunCodegen.add NONE] 
fa5080577da9
HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
krauss
parents:
19782
diff
changeset

122 

20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

123 
val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

124 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

125 
val thy = Theory.add_path name thy 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

126 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

127 
val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

128 
val thy = Theory.parent_path thy 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

129 
in 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

130 
thy 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

131 
end 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

132 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

133 
(* 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

134 
fun mk_partial_rules name D_name D domT idomT thmss thy = 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

135 
let 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

136 
val [subs, dcl] = (hd thmss) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

137 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

138 
val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... } 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

139 
= the (Symtab.lookup (FundefData.get thy) name) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

140 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

141 
val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

142 
[SOME (cterm_of thy D)] 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

143 
subsetD) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

144 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

145 
val D_simps = map (curry op RS D_implies_dom) f_simps 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

146 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

147 
val D_induct = subset_induct 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

148 
> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)] 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

149 
> curry op COMP subs 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

150 
> curry op COMP (dcl > forall_intr (cterm_of thy (Var (("z",0), idomT))) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

151 
> forall_intr (cterm_of thy (Var (("x",0), idomT)))) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

152 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

153 
val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

154 
val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

155 
in 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

156 
thy3 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

157 
end 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

158 
*) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

159 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

160 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

161 
fun fundef_setup_termination_proof name NONE thy = 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

162 
let 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

163 
val name = if name = "" then get_last_fundef thy else name 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

164 
val data = the (get_fundef_data name thy) 
19938
241a7777a3ff
Removed (term_of o cterm_of)Hack, Added error message for unknown definition at "termination"command
krauss
parents:
19922
diff
changeset

165 
handle Option.Option => raise ERROR ("No such function definition: " ^ name) 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

166 

20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

167 
val (res as FundefMResult {termination, ...}, mutual, _) = data 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

168 
val goal = FundefTermination.mk_total_termination_goal data 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

169 
in 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

170 
thy > ProofContext.init 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

171 
> ProofContext.note_thmss_i [(("termination", 
19922  172 
[ContextRules.intro_query NONE]), [([standard termination], [])])] > snd 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

173 
> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", []) 
19585  174 
[(("", []), [(goal, [])])] 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

175 
end 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

176 
 fundef_setup_termination_proof name (SOME (dom_name, dom)) thy = 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

177 
let 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

178 
val name = if name = "" then get_last_fundef thy else name 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

179 
val data = the (get_fundef_data name thy) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

180 
val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

181 
in 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

182 
thy > ProofContext.init 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

183 
> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", []) 
19585  184 
[(("", []), [(subs, []), (dcl, [])])] 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

185 
end 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

186 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

187 

19611
da2a0014c461
Function Package: Quickanddirtyfixed strange "Proved a different theorem bug"
krauss
parents:
19585
diff
changeset

188 
val add_fundef = gen_add_fundef Attrib.attribute 
da2a0014c461
Function Package: Quickanddirtyfixed strange "Proved a different theorem bug"
krauss
parents:
19585
diff
changeset

189 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

190 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

191 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

192 
(* congruence rules *) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

193 

19617  194 
val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq); 
195 
val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq); 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

196 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

197 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

198 
(* setup *) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

199 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

200 
val setup = FundefData.init #> FundefCongs.init 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

201 
#> Attrib.add_attributes 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

202 
[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")] 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

203 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

204 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

205 
val get_congs = FundefCommon.get_fundef_congs o Context.Theory 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

206 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset

207 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

208 
(* outer syntax *) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

209 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

210 
local structure P = OuterParse and K = OuterKeyword in 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

211 

20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

212 

3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

213 

3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

214 
val star = Scan.one (fn t => (OuterLex.val_of t = "*")); 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

215 

3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

216 

3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

217 
val attribs_with_star = P.$$$ "["  P.!!! ((P.list (star >> K NONE  P.attrib >> SOME)) 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

218 
>> (fn x => (map_filter I x, exists is_none x))) 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

219 
 P.$$$ "]"; 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

220 

3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

221 
val opt_attribs_with_star = Scan.optional attribs_with_star ([], false); 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

222 

3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

223 
fun opt_thm_name_star s = 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

224 
Scan.optional ((P.name  opt_attribs_with_star  (attribs_with_star >> pair ""))  P.$$$ s) ("", ([], false)); 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

225 

3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

226 

19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

227 
val function_decl = 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

228 
Scan.repeat1 (opt_thm_name_star ":"  P.prop); 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

229 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

230 
val functionP = 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

231 
OuterSyntax.command "function" "define general recursive functions" K.thy_goal 
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

232 
(((Scan.optional (P.$$$ "("  P.!!! (P.$$$ "pre"  P.$$$ ")") >> K true) false)  
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

233 
P.and_list1 function_decl) >> (fn (prepr, eqnss) => 
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19938
diff
changeset

234 
Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr))); 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

235 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

236 
val terminationP = 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

237 
OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

238 
((Scan.optional P.name ""  Scan.option (P.$$$ "("  Scan.optional (P.name  P.$$$ ":") "dom"  P.term  P.$$$ ")")) 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

239 
>> (fn (name,dom) => 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

240 
Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom))); 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

241 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

242 
val _ = OuterSyntax.add_parsers [functionP]; 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

243 
val _ = OuterSyntax.add_parsers [terminationP]; 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

244 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

245 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

246 
end; 
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

247 

d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset

248 

19585  249 
end 