src/HOL/Tools/function_package/fundef_package.ML
changeset 19583 c5fa77b03442
parent 19564 d3e2f532459a
child 19585 70a1ce3b23ae
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri May 05 22:11:19 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sun May 07 00:00:13 2006 +0200
     1.3 @@ -26,19 +26,18 @@
     1.4  val True_implies = thm "True_implies"
     1.5  
     1.6  
     1.7 -(*#> FundefTermination.setup #> FundefDatatype.setup*)
     1.8 -
     1.9  fun fundef_afterqed congs curry_info name data natts thmss thy =
    1.10      let
    1.11  	val (complete_thm :: compat_thms) = map hd thmss
    1.12  	val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
    1.13 -	val {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
    1.14 +	val FundefResult {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
    1.15  
    1.16  	val (names, attsrcs) = split_list natts
    1.17  	val atts = map (map (Attrib.attribute thy)) attsrcs
    1.18  
    1.19 -	val accR = (#acc_R(#names(data)))
    1.20 -	val dom_abbrev = Logic.mk_equals (Free ("dom", fastype_of accR), accR)
    1.21 +	val Prep {names = Names {acc_R=accR, ...}, ...} = data
    1.22 +	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    1.23 +	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    1.24  
    1.25  	val thy = thy |> Theory.add_path name 
    1.26  
    1.27 @@ -46,7 +45,6 @@
    1.28  	val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy;
    1.29  	val thy = thy |> Theory.parent_path
    1.30  
    1.31 -	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    1.32  	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy
    1.33  	val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy
    1.34  	val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy
    1.35 @@ -64,7 +62,7 @@
    1.36  	val congs = get_fundef_congs (Context.Theory thy)
    1.37  
    1.38  	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs (map (Sign.read_prop thy) eqns) thy
    1.39 -	val {complete, compat, ...} = data
    1.40 +	val Prep {complete, compat, ...} = data
    1.41  
    1.42  	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
    1.43      in
    1.44 @@ -78,7 +76,7 @@
    1.45      let
    1.46  	val totality = hd (hd thmss)
    1.47  
    1.48 -	val {psimps, simple_pinduct, ... }
    1.49 +	val FundefResult {psimps, simple_pinduct, ... }
    1.50  	  = the (get_fundef_data name thy)
    1.51  
    1.52  	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
    1.53 @@ -133,7 +131,7 @@
    1.54  	val name = if name = "" then get_last_fundef thy else name
    1.55  	val data = the (get_fundef_data name thy)
    1.56  
    1.57 -	val {total_intro, ...} = data
    1.58 +	val FundefResult {total_intro, ...} = data
    1.59  	val goal = FundefTermination.mk_total_termination_goal data
    1.60      in
    1.61  	thy |> ProofContext.init