function-package: Changed record usage to make sml/nj happy...
--- a/src/HOL/Tools/function_package/fundef_common.ML Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Sun May 07 00:00:13 2006 +0200
@@ -29,8 +29,8 @@
(* A record containing all the relevant symbols and types needed during the proof.
This is set up at the beginning and does not change. *)
-type naming_context =
- { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ,
+datatype naming_context =
+ Names of { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ,
G: term, R: term, acc_R: term, h: term, y: term, x: term, z: term, a:term, P: term,
D: term, Pbool:term,
glrs: (term list * term list * term * term) list,
@@ -41,10 +41,11 @@
}
-type rec_call_info =
- {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm}
+datatype rec_call_info =
+ RCInfo of {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm}
-type clause_info =
+datatype clause_info =
+ ClauseInfo of
{
no: int,
@@ -72,11 +73,12 @@
}
-type curry_info =
- { argTs: typ list, curry_ss: simpset }
+datatype curry_info =
+ Curry of { argTs: typ list, curry_ss: simpset }
-type prep_result =
+datatype prep_result =
+ Prep of
{
names: naming_context,
complete : term,
@@ -84,7 +86,8 @@
clauses: clause_info list
}
-type fundef_result =
+datatype fundef_result =
+ FundefResult of
{
f: term,
G : term,
--- a/src/HOL/Tools/function_package/fundef_package.ML Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Sun May 07 00:00:13 2006 +0200
@@ -26,19 +26,18 @@
val True_implies = thm "True_implies"
-(*#> FundefTermination.setup #> FundefDatatype.setup*)
-
fun fundef_afterqed congs curry_info name data natts thmss thy =
let
val (complete_thm :: compat_thms) = map hd thmss
val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
- val {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
+ val FundefResult {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
val (names, attsrcs) = split_list natts
val atts = map (map (Attrib.attribute thy)) attsrcs
- val accR = (#acc_R(#names(data)))
- val dom_abbrev = Logic.mk_equals (Free ("dom", fastype_of accR), accR)
+ val Prep {names = Names {acc_R=accR, ...}, ...} = data
+ val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
+ val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
val thy = thy |> Theory.add_path name
@@ -46,7 +45,6 @@
val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy;
val thy = thy |> Theory.parent_path
- val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy
val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy
val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy
@@ -64,7 +62,7 @@
val congs = get_fundef_congs (Context.Theory thy)
val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs (map (Sign.read_prop thy) eqns) thy
- val {complete, compat, ...} = data
+ val Prep {complete, compat, ...} = data
val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
in
@@ -78,7 +76,7 @@
let
val totality = hd (hd thmss)
- val {psimps, simple_pinduct, ... }
+ val FundefResult {psimps, simple_pinduct, ... }
= the (get_fundef_data name thy)
val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
@@ -133,7 +131,7 @@
val name = if name = "" then get_last_fundef thy else name
val data = the (get_fundef_data name thy)
- val {total_intro, ...} = data
+ val FundefResult {total_intro, ...} = data
val goal = FundefTermination.mk_total_termination_goal data
in
thy |> ProofContext.init
--- a/src/HOL/Tools/function_package/fundef_prep.ML Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Sun May 07 00:00:13 2006 +0200
@@ -87,7 +87,7 @@
fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs =
let
- val {domT, G, R, h, f, fvar, used, x, ...} = names
+ val Names {domT, G, R, h, f, fvar, used, x, ...} = names
val zv = Var (("z",0), domT) (* for generating h_assums *)
val xv = Var (("x",0), domT)
@@ -130,19 +130,20 @@
val Gh = assume (cterm_of thy Gh_term)
val Gh' = assume (cterm_of thy (rename_vars Gh_term))
in
- {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
+ RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
end
val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
in
- {
- no=no,
- qs=qs, gs=gs, lhs=lhs, rhs=rhs,
- cqs=cqs, cvqs=cvqs, ags=ags,
- cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
- GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
- tree=tree, case_hyp = case_hyp
- }
+ ClauseInfo
+ {
+ no=no,
+ qs=qs, gs=gs, lhs=lhs, rhs=rhs,
+ cqs=cqs, cvqs=cvqs, ags=ags,
+ cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
+ GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
+ tree=tree, case_hyp = case_hyp
+ }
end
@@ -191,7 +192,7 @@
val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", f_eq), [])] thy
in
- ({f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, used=allused, trees=trees}, thy)
+ (Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, used=allused, trees=trees}, thy)
end
@@ -222,7 +223,7 @@
fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
let
- val { domT, R, G, f, fvar, h, y, Pbool, ... } = names
+ val Names { domT, R, G, f, fvar, h, y, Pbool, ... } = names
val z = Var (("z",0), domT)
val x = Var (("x",0), domT)
@@ -241,7 +242,7 @@
fun mk_completeness names glrs =
let
- val {domT, x, Pbool, ...} = names
+ val Names {domT, x, Pbool, ...} = names
fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
@@ -255,7 +256,7 @@
fun extract_conditions thy names trees congs =
let
- val {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
+ val Names {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
val Gis = map2 (mk_GIntro thy names) glrs preRiss
@@ -294,7 +295,7 @@
fun prepare_fundef congs eqs fname thy =
let
val (names, thy) = setup_context (analyze_eqs eqs) fname congs thy
- val {G, R, glrs, trees, ...} = names
+ val Names {G, R, glrs, trees, ...} = names
val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
@@ -304,7 +305,7 @@
val n = length glrs
val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
in
- ({names = names, complete=complete, compat=compat, clauses = clauses},
+ (Prep {names = names, complete=complete, compat=compat, clauses = clauses},
thy)
end
@@ -346,7 +347,7 @@
val g_to_f_ss = HOL_basic_ss addsimps [symmetric f_def]
val eqs_tupled = map (Pattern.rewrite_term thy [(f, f_lambda)] []) eqs
in
- (SOME {curry_ss = g_to_f_ss, argTs = caTs}, fxname, prepare_fundef congs eqs_tupled fxname thy)
+ (SOME (Curry {curry_ss = g_to_f_ss, argTs = caTs}), fxname, prepare_fundef congs eqs_tupled fxname thy)
end
end
--- a/src/HOL/Tools/function_package/fundef_proof.ML Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_proof.ML Sun May 07 00:00:13 2006 +0200
@@ -42,10 +42,10 @@
-fun mk_simp thy (names:naming_context) f_iff graph_is_function clause valthm =
+fun mk_simp thy names f_iff graph_is_function clause valthm =
let
- val {R, acc_R, domT, z, ...} = names
- val {qs, cqs, gs, lhs, rhs, ...} = clause
+ val Names {R, acc_R, domT, z, ...} = names
+ val ClauseInfo {qs, cqs, gs, lhs, rhs, ...} = clause
val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, acc_R))) (* "lhs : acc R" *)
val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *)
in
@@ -65,9 +65,9 @@
-fun mk_partial_induct_rule thy (names:naming_context) complete_thm clauses =
+fun mk_partial_induct_rule thy names complete_thm clauses =
let
- val {domT, R, acc_R, x, z, a, P, D, ...} = names
+ val Names {domT, R, acc_R, x, z, a, P, D, ...} = names
val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D))))
val a_D = cterm_of thy (Trueprop (mk_mem (a, D)))
@@ -92,14 +92,14 @@
fun prove_case clause =
let
- val {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause
+ val ClauseInfo {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause
val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
val sih = full_simplify replace_x_ss aihyp
(* FIXME: Variable order destroyed by forall_intr_vars *)
- val P_recs = map (fn {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs (* [P rec1, P rec2, ... ] *)
+ val P_recs = map (fn RCInfo {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs (* [P rec1, P rec2, ... ] *)
val step = Trueprop (P $ lhs)
|> fold_rev (curry Logic.mk_implies o prop_of) P_recs
@@ -183,16 +183,16 @@
(* recover the order of Vars *)
-fun get_var_order thy (clauses: clause_info list) =
- map (fn ({cqs,...}, {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
+fun get_var_order thy clauses =
+ map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
(* if j < i, then turn around *)
fun get_compat_thm thy cts clausei clausej =
let
- val {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
- val {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
+ val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
+ val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
in if j < i then
@@ -227,14 +227,14 @@
here. *)
fun mk_replacement_lemma thy (names:naming_context) ih_elim clause =
let
- val {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names
- val {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
+ val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names
+ val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
- val Ris = map #lRIq RCs
- val h_assums = map #Gh RCs
- val h_assums' = map #Gh' RCs
+ val Ris = map (fn RCInfo {lRIq, ...} => lRIq) RCs
+ val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
+ val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
@@ -255,15 +255,15 @@
-fun mk_uniqueness_clause thy (names:naming_context) compat_store (clausei:clause_info) (clausej:clause_info) RLj =
+fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
let
- val {f, h, y, ...} = names
- val {no=i, lhs=lhsi, case_hyp, ...} = clausei
- val {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
+ val Names {f, h, y, ...} = names
+ val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
+ val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
val compat = get_compat_thm thy compat_store clausei clausej
- val Ghsj' = map (fn {Gh', ...} => Gh') RCsj
+ val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
@@ -286,17 +286,17 @@
-fun mk_uniqueness_case thy (names:naming_context) ihyp ih_intro G_cases compat_store clauses rep_lemmas (clausei:clause_info) =
+fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
let
- val {x, y, G, fvar, f, ranT, ...} = names
- val {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
+ val Names {x, y, G, fvar, f, ranT, ...} = names
+ val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
- fun prep_RC ({lRIq,RIvs, ...} : rec_call_info) = lRIq
- |> fold (forall_elim o cterm_of thy o Free) RIvs
- |> (fn it => it RS ih_intro_case)
- |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+ fun prep_RC (RCInfo {lRIq,RIvs, ...}) = lRIq
+ |> fold (forall_elim o cterm_of thy o Free) RIvs
+ |> (fn it => it RS ih_intro_case)
+ |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
val existence = lGI |> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])
|> fold (curry op COMP o prep_RC) RCs
@@ -340,10 +340,10 @@
(* Does this work with Guards??? *)
-fun mk_domain_intro thy (names:naming_context) R_cases clause =
+fun mk_domain_intro thy names R_cases clause =
let
- val {z, R, acc_R, ...} = names
- val {qs, gs, lhs, rhs, ...} = clause
+ val Names {z, R, acc_R, ...} = names
+ val ClauseInfo {qs, gs, lhs, rhs, ...} = clause
val z_lhs = cterm_of thy (HOLogic.mk_prod (z,lhs))
val z_acc = cterm_of thy (HOLogic.mk_mem (z,acc_R))
@@ -368,10 +368,10 @@
-fun mk_nest_term_case thy (names:naming_context) R' ihyp clause =
+fun mk_nest_term_case thy names R' ihyp clause =
let
- val {x, z, ...} = names
- val {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause
+ val Names {x, z, ...} = names
+ val ClauseInfo {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause
val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
@@ -421,9 +421,9 @@
end
-fun mk_nest_term_rule thy (names:naming_context) clauses =
+fun mk_nest_term_rule thy names clauses =
let
- val { R, acc_R, domT, x, z, ... } = names
+ val Names { R, acc_R, domT, x, z, ... } = names
val R_elim = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R))))))
@@ -469,8 +469,8 @@
fun mk_partial_rules thy congs data complete_thm compat_thms =
let
- val {names, clauses, complete, compat, ...} = data
- val {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
+ val Prep {names, clauses, complete, compat, ...} = data
+ val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
(* val _ = Output.debug "closing derivation: completeness"
val _ = Output.debug (Proofterm.size_of_proof (proof_of complete_thm))
@@ -541,7 +541,7 @@
val _ = Output.debug "Proving domain introduction rules"
val dom_intros = map (mk_domain_intro thy names R_cases) clauses
in
- {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm,
+ FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm,
psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
dom_intros=dom_intros}
end
@@ -566,9 +566,9 @@
fun mk_partial_rules_curried thy congs NONE data complete_thm compat_thms =
mk_partial_rules thy congs data complete_thm compat_thms
- | mk_partial_rules_curried thy congs (SOME {curry_ss, argTs}) data complete_thm compat_thms =
+ | mk_partial_rules_curried thy congs (SOME (Curry {curry_ss, argTs})) data complete_thm compat_thms =
let
- val {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} =
+ val FundefResult {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} =
mk_partial_rules thy congs data complete_thm compat_thms
val cpsimps = map (simplify curry_ss) psimps
val cpinduct = full_simplify curry_ss simple_pinduct
@@ -576,7 +576,7 @@
val cdom_intros = map (full_simplify curry_ss) dom_intros
val ctotal_intro = full_simplify curry_ss total_intro
in
- {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm,
+ FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm,
psimps=cpsimps, subset_pinduct=subset_pinduct, simple_pinduct=cpinduct, total_intro=ctotal_intro, dom_intros=cdom_intros}
end
--- a/src/HOL/Tools/function_package/termination.ML Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/Tools/function_package/termination.ML Sun May 07 00:00:13 2006 +0200
@@ -20,9 +20,9 @@
open FundefCommon
open FundefAbbrev
-fun mk_total_termination_goal (data: fundef_result) =
+fun mk_total_termination_goal data =
let
- val {R, f, ... } = data
+ val FundefResult {R, f, ... } = data
val domT = domain_type (fastype_of f)
val x = Free ("x", domT)
@@ -30,9 +30,9 @@
Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
end
-fun mk_partial_termination_goal thy (data: fundef_result) dom =
+fun mk_partial_termination_goal thy data dom =
let
- val {R, f, ... } = data
+ val FundefResult {R, f, ... } = data
val domT = domain_type (fastype_of f)
val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom
--- a/src/HOL/ex/Fundefs.thy Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/ex/Fundefs.thy Sun May 07 00:00:13 2006 +0200
@@ -58,7 +58,7 @@
by pat_completeness auto
lemma nz_is_zero: (* A lemma we need to prove termination *)
- assumes trm: "x \<in> nz.dom"
+ assumes trm: "x \<in> nz_dom"
shows "nz x = 0"
using trm
by induct auto