src/HOL/Tools/function_package/fundef_package.ML
changeset 19922 984ae977f7aa
parent 19876 11d447d5d68c
child 19938 241a7777a3ff
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jun 19 18:02:49 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jun 19 18:25:34 2006 +0200
     1.3 @@ -48,12 +48,11 @@
     1.4  
     1.5  
     1.6  
     1.7 -fun fundef_afterqed congs curry_info name data names atts thmss thy =
     1.8 +fun fundef_afterqed congs mutual_info name data names atts [[result]] thy =
     1.9      let
    1.10 -	val (complete_thm :: compat_thms) = map hd thmss
    1.11 -	val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (Thm.freezeT complete_thm) (map Thm.freezeT compat_thms)
    1.12 -	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data
    1.13 -        val Mutual {parts, ...} = curry_info
    1.14 +	val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
    1.15 +	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    1.16 +        val Mutual {parts, ...} = mutual_info
    1.17  
    1.18  	val Prep {names = Names {acc_R=accR, ...}, ...} = data
    1.19  	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    1.20 @@ -62,13 +61,13 @@
    1.21          val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) (names ~~ atts) thy
    1.22  
    1.23  	val thy = thy |> Theory.add_path name
    1.24 -	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names (flat names)])] thy
    1.25 +	val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names (flat names)])] thy
    1.26  	val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
    1.27 -	val (_, thy) = PureThy.add_thms [(("termination", termination), [])] thy
    1.28 +	val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
    1.29  	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names (flat names), InductAttrib.induct_set ""])] thy
    1.30  	val thy = thy |> Theory.parent_path
    1.31      in
    1.32 -	add_fundef_data name (fundef_data, curry_info, names, atts) thy
    1.33 +	add_fundef_data name (fundef_data, mutual_info, names, atts) thy
    1.34      end
    1.35  
    1.36  fun gen_add_fundef prep_att eqns_attss thy =
    1.37 @@ -93,14 +92,14 @@
    1.38  	val t_eqns = map (map (Sign.read_prop thy)) eqns
    1.39  			 |> map (map (term_of o cterm_of thy)) (* HACK to prevent strange things from happening with abbreviations *)
    1.40  
    1.41 -	val (curry_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
    1.42 -	val Prep {complete, compat, ...} = data
    1.43 -
    1.44 -	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
    1.45 +	val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
    1.46 +	val Prep {goal, goalI, ...} = data
    1.47      in
    1.48  	thy |> ProofContext.init
    1.49 -	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data names atts) NONE ("", [])
    1.50 -	    (map (fn t => (("", []), [(t, [])])) props)
    1.51 +	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data names atts) NONE ("", [])
    1.52 +	    [(("", []), [(goal, [])])]
    1.53 +            |> Proof.refine (Method.primitive_text (fn _ => goalI))
    1.54 +            |> Seq.hd
    1.55      end
    1.56  
    1.57  
    1.58 @@ -167,7 +166,7 @@
    1.59      in
    1.60  	thy |> ProofContext.init
    1.61  	    |> ProofContext.note_thmss_i [(("termination", 
    1.62 -					    [ContextRules.intro_query NONE]), [([termination], [])])] |> snd
    1.63 +					    [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
    1.64  	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", [])
    1.65  	    [(("", []), [(goal, [])])]
    1.66      end