src/HOL/Tools/function_package/fundef_package.ML
changeset 19770 be5c23ebe1eb
parent 19617 7cb4b67d4b97
child 19782 48c4632e2c28
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jun 05 14:22:58 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jun 05 14:26:07 2006 +0200
     1.3 @@ -9,12 +9,13 @@
     1.4  
     1.5  signature FUNDEF_PACKAGE = 
     1.6  sig
     1.7 -    val add_fundef : ((bstring * Attrib.src list) * string) list -> theory -> Proof.state (* Need an _i variant *)
     1.8 +    val add_fundef : ((bstring * Attrib.src list) * string) list list -> theory -> Proof.state (* Need an _i variant *)
     1.9  
    1.10      val cong_add: attribute
    1.11      val cong_del: attribute
    1.12  							 
    1.13      val setup : theory -> theory
    1.14 +    val get_congs : theory -> thm list
    1.15  end
    1.16  
    1.17  
    1.18 @@ -26,46 +27,73 @@
    1.19  val True_implies = thm "True_implies"
    1.20  
    1.21  
    1.22 +fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) (names, attss) thy =
    1.23 +    let 
    1.24 +      val thy = thy |> Theory.add_path f_name 
    1.25 +                
    1.26 +      val thy = thy |> Theory.add_path label
    1.27 +      val spsimps = map standard psimps
    1.28 +      val add_list = (names ~~ spsimps) ~~ attss
    1.29 +      val (_, thy) = PureThy.add_thms add_list thy
    1.30 +      val thy = thy |> Theory.parent_path
    1.31 +                
    1.32 +      val (_, thy) = PureThy.add_thmss [((label, spsimps), Simplifier.simp_add :: moreatts)] thy
    1.33 +      val thy = thy |> Theory.parent_path
    1.34 +    in
    1.35 +      thy
    1.36 +    end
    1.37 +    
    1.38 +
    1.39 +
    1.40 +
    1.41 +
    1.42 +
    1.43  fun fundef_afterqed congs curry_info name data names atts thmss thy =
    1.44      let
    1.45  	val (complete_thm :: compat_thms) = map hd thmss
    1.46 -	val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
    1.47 -	val FundefResult {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
    1.48 -
    1.49 +	val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
    1.50 +	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data
    1.51 +        val Mutual {parts, ...} = curry_info
    1.52  
    1.53  	val Prep {names = Names {acc_R=accR, ...}, ...} = data
    1.54  	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    1.55  	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    1.56  
    1.57 -	val thy = thy |> Theory.add_path name 
    1.58 -
    1.59 -	val thy = thy |> Theory.add_path "psimps"
    1.60 -	val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy;
    1.61 -	val thy = thy |> Theory.parent_path
    1.62 +        val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) (names ~~ atts) thy
    1.63  
    1.64 -	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy
    1.65 -	val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy
    1.66 -	val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy
    1.67 -	val (_,thy) = PureThy.add_thms [(("pinduct", simple_pinduct), [RuleCases.case_names names, InductAttrib.induct_set ""])] thy
    1.68 -	val (_, thy) = PureThy.add_thmss [(("psimps", psimps), [Simplifier.simp_add])] thy
    1.69 +	val thy = thy |> Theory.add_path name
    1.70 +	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names (flat names)])] thy
    1.71 +	val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
    1.72 +	val (_, thy) = PureThy.add_thms [(("termination", termination), [])] thy
    1.73 +	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names (flat names), InductAttrib.induct_set ""])] thy
    1.74  	val thy = thy |> Theory.parent_path
    1.75      in
    1.76 -	add_fundef_data name fundef_data thy
    1.77 +	add_fundef_data name (fundef_data, curry_info, names, atts) thy
    1.78      end
    1.79  
    1.80 -fun gen_add_fundef prep_att eqns_atts thy =
    1.81 +fun gen_add_fundef prep_att eqns_attss thy =
    1.82      let
    1.83 -	val (natts, eqns) = split_list eqns_atts
    1.84 -	val (names, raw_atts) = split_list natts
    1.85 +	fun split eqns_atts =
    1.86 +	    let 
    1.87 +		val (natts, eqns) = split_list eqns_atts
    1.88 +		val (names, raw_atts) = split_list natts
    1.89 +		val atts = map (map (prep_att thy)) raw_atts
    1.90 +	    in
    1.91 +		((names, atts), eqns)
    1.92 +	    end
    1.93  
    1.94 -	val atts = map (map (prep_att thy)) raw_atts
    1.95 +
    1.96 +	val (natts, eqns) = split_list (map split_list eqns_attss)
    1.97 +	val (names, raw_atts) = split_list (map split_list natts)
    1.98 +
    1.99 +	val atts = map (map (map (prep_att thy))) raw_atts
   1.100  
   1.101  	val congs = get_fundef_congs (Context.Theory thy)
   1.102  
   1.103 -	val t_eqns = map (Sign.read_prop thy) eqns
   1.104 -			 |> map (term_of o cterm_of thy) (* HACK to prevent strange things from happening with abbreviations *)
   1.105 +	val t_eqns = map (map (Sign.read_prop thy)) eqns
   1.106 +			 |> map (map (term_of o cterm_of thy)) (* HACK to prevent strange things from happening with abbreviations *)
   1.107  
   1.108 -	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs t_eqns thy
   1.109 +	val (curry_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
   1.110  	val Prep {complete, compat, ...} = data
   1.111  
   1.112  	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
   1.113 @@ -76,27 +104,23 @@
   1.114      end
   1.115  
   1.116  
   1.117 -fun total_termination_afterqed name thmss thy =
   1.118 +fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy =
   1.119      let
   1.120  	val totality = hd (hd thmss)
   1.121  
   1.122 -	val FundefResult {psimps, simple_pinduct, ... }
   1.123 +	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, names, atts)
   1.124  	  = the (get_fundef_data name thy)
   1.125  
   1.126  	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
   1.127  
   1.128 -	val tsimps = map remove_domain_condition psimps
   1.129 -	val tinduct = remove_domain_condition simple_pinduct
   1.130 +	val tsimps = map (map remove_domain_condition) psimps
   1.131 +	val tinduct = map remove_domain_condition simple_pinducts
   1.132 +
   1.133 +        val thy = fold2 (add_simps "simps" [RecfunCodegen.add NONE]) (parts ~~ tsimps) (names ~~ atts) thy
   1.134  
   1.135  	val thy = Theory.add_path name thy
   1.136  		  
   1.137 -		  (* Need the names and attributes. Apply the attributes again? *)
   1.138 -(*	val thy = thy |> Theory.add_path "simps"
   1.139 -	val (_, thy) = PureThy.add_thms ((names ~~ tsimps) ~~ atts) thy;
   1.140 -	val thy = thy |> Theory.parent_path*)
   1.141 -
   1.142 -	val (_, thy) = PureThy.add_thms [(("induct", tinduct), [])] thy 
   1.143 -	val (_, thy) = PureThy.add_thmss [(("simps", tsimps), [Simplifier.simp_add, RecfunCodegen.add NONE])] thy
   1.144 +	val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy 
   1.145  	val thy = Theory.parent_path thy
   1.146      in
   1.147  	thy
   1.148 @@ -135,13 +159,13 @@
   1.149  	val name = if name = "" then get_last_fundef thy else name
   1.150  	val data = the (get_fundef_data name thy)
   1.151  
   1.152 -	val FundefResult {total_intro, ...} = data
   1.153 +	val (res as FundefMResult {termination, ...}, mutual, _, _) = data
   1.154  	val goal = FundefTermination.mk_total_termination_goal data
   1.155      in
   1.156  	thy |> ProofContext.init
   1.157 -	    |> ProofContext.note_thmss_i [(("termination_intro", 
   1.158 -					    [ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd
   1.159 -	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", [])
   1.160 +	    |> ProofContext.note_thmss_i [(("termination", 
   1.161 +					    [ContextRules.intro_query NONE]), [([termination], [])])] |> snd
   1.162 +	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", [])
   1.163  	    [(("", []), [(goal, [])])]
   1.164      end	
   1.165    | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
   1.166 @@ -173,6 +197,9 @@
   1.167  		[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
   1.168  
   1.169  
   1.170 +val get_congs = FundefCommon.get_fundef_congs o Context.Theory
   1.171 +
   1.172 +
   1.173  (* outer syntax *)
   1.174  
   1.175  local structure P = OuterParse and K = OuterKeyword in
   1.176 @@ -182,8 +209,8 @@
   1.177  
   1.178  val functionP =
   1.179    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   1.180 -    (function_decl >> (fn eqns =>
   1.181 -      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqns)));
   1.182 +    (P.and_list1 function_decl >> (fn eqnss =>
   1.183 +      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss)));
   1.184  
   1.185  val terminationP =
   1.186    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal