src/HOL/Tools/function_package/fundef_package.ML
author krauss
Mon Jun 19 18:25:34 2006 +0200 (2006-06-19)
changeset 19922 984ae977f7aa
parent 19876 11d447d5d68c
child 19938 241a7777a3ff
permissions -rw-r--r--
Fixed name clash.
Function-goals are now fully quantified.
Avoiding large meta-conjunctions when setting up the goal.
Cleanup.
     1 (*  Title:      HOL/Tools/function_package/fundef_package.ML
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 
     5 A package for general recursive function definitions. 
     6 Isar commands.
     7 
     8 *)
     9 
    10 signature FUNDEF_PACKAGE = 
    11 sig
    12     val add_fundef : ((bstring * Attrib.src list) * string) list list -> theory -> Proof.state (* Need an _i variant *)
    13 
    14     val cong_add: attribute
    15     val cong_del: attribute
    16 							 
    17     val setup : theory -> theory
    18     val get_congs : theory -> thm list
    19 end
    20 
    21 
    22 structure FundefPackage : FUNDEF_PACKAGE =
    23 struct
    24 
    25 open FundefCommon
    26 
    27 val True_implies = thm "True_implies"
    28 
    29 
    30 fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) (names, attss) thy =
    31     let 
    32       val thy = thy |> Theory.add_path f_name 
    33                 
    34       val thy = thy |> Theory.add_path label
    35       val spsimps = map standard psimps
    36       val add_list = (names ~~ spsimps) ~~ attss
    37       val (_, thy) = PureThy.add_thms add_list thy
    38       val thy = thy |> Theory.parent_path
    39                 
    40       val (_, thy) = PureThy.add_thmss [((label, spsimps), Simplifier.simp_add :: moreatts)] thy
    41       val thy = thy |> Theory.parent_path
    42     in
    43       thy
    44     end
    45     
    46 
    47 
    48 
    49 
    50 
    51 fun fundef_afterqed congs mutual_info name data names atts [[result]] thy =
    52     let
    53 	val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
    54 	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    55         val Mutual {parts, ...} = mutual_info
    56 
    57 	val Prep {names = Names {acc_R=accR, ...}, ...} = data
    58 	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    59 	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    60 
    61         val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) (names ~~ atts) thy
    62 
    63 	val thy = thy |> Theory.add_path name
    64 	val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names (flat names)])] thy
    65 	val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
    66 	val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
    67 	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names (flat names), InductAttrib.induct_set ""])] thy
    68 	val thy = thy |> Theory.parent_path
    69     in
    70 	add_fundef_data name (fundef_data, mutual_info, names, atts) thy
    71     end
    72 
    73 fun gen_add_fundef prep_att eqns_attss thy =
    74     let
    75 	fun split eqns_atts =
    76 	    let 
    77 		val (natts, eqns) = split_list eqns_atts
    78 		val (names, raw_atts) = split_list natts
    79 		val atts = map (map (prep_att thy)) raw_atts
    80 	    in
    81 		((names, atts), eqns)
    82 	    end
    83 
    84 
    85 	val (natts, eqns) = split_list (map split_list eqns_attss)
    86 	val (names, raw_atts) = split_list (map split_list natts)
    87 
    88 	val atts = map (map (map (prep_att thy))) raw_atts
    89 
    90 	val congs = get_fundef_congs (Context.Theory thy)
    91 
    92 	val t_eqns = map (map (Sign.read_prop thy)) eqns
    93 			 |> map (map (term_of o cterm_of thy)) (* HACK to prevent strange things from happening with abbreviations *)
    94 
    95 	val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
    96 	val Prep {goal, goalI, ...} = data
    97     in
    98 	thy |> ProofContext.init
    99 	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data names atts) NONE ("", [])
   100 	    [(("", []), [(goal, [])])]
   101             |> Proof.refine (Method.primitive_text (fn _ => goalI))
   102             |> Seq.hd
   103     end
   104 
   105 
   106 fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy =
   107     let
   108 	val totality = hd (hd thmss)
   109 
   110 	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, names, atts)
   111 	  = the (get_fundef_data name thy)
   112 
   113 	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
   114 
   115 	val tsimps = map (map remove_domain_condition) psimps
   116 	val tinduct = map remove_domain_condition simple_pinducts
   117 
   118         val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
   119         val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
   120 
   121         val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) (names ~~ atts) thy
   122 
   123 	val thy = Theory.add_path name thy
   124 		  
   125 	val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy 
   126 	val thy = Theory.parent_path thy
   127     in
   128 	thy
   129     end
   130 
   131 (*
   132 fun mk_partial_rules name D_name D domT idomT thmss thy =
   133     let
   134 	val [subs, dcl] = (hd thmss)
   135 
   136 	val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
   137 	  = the (Symtab.lookup (FundefData.get thy) name)
   138 
   139 	val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] 
   140 						    [SOME (cterm_of thy D)]
   141 						    subsetD)
   142 
   143 	val D_simps = map (curry op RS D_implies_dom) f_simps
   144 
   145 	val D_induct = subset_induct
   146 			   |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
   147 			   |> curry op COMP subs
   148 			   |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
   149 						 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
   150 
   151 	val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
   152 	val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
   153     in
   154 	thy3
   155     end
   156 *)
   157  
   158 
   159 fun fundef_setup_termination_proof name NONE thy = 
   160     let
   161 	val name = if name = "" then get_last_fundef thy else name
   162 	val data = the (get_fundef_data name thy)
   163 
   164 	val (res as FundefMResult {termination, ...}, mutual, _, _) = data
   165 	val goal = FundefTermination.mk_total_termination_goal data
   166     in
   167 	thy |> ProofContext.init
   168 	    |> ProofContext.note_thmss_i [(("termination", 
   169 					    [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
   170 	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", [])
   171 	    [(("", []), [(goal, [])])]
   172     end	
   173   | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
   174     let
   175 	val name = if name = "" then get_last_fundef thy else name
   176 	val data = the (get_fundef_data name thy)
   177 	val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
   178     in
   179 	thy |> ProofContext.init
   180 	    |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
   181 	    [(("", []), [(subs, []), (dcl, [])])]
   182     end	
   183 
   184 
   185 val add_fundef = gen_add_fundef Attrib.attribute
   186 
   187 
   188 
   189 (* congruence rules *)
   190 
   191 val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
   192 val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
   193 
   194 
   195 (* setup *)
   196 
   197 val setup = FundefData.init #> FundefCongs.init 
   198 	#>  Attrib.add_attributes
   199 		[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
   200 
   201 
   202 val get_congs = FundefCommon.get_fundef_congs o Context.Theory
   203 
   204 
   205 (* outer syntax *)
   206 
   207 local structure P = OuterParse and K = OuterKeyword in
   208 
   209 val function_decl =
   210     Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
   211 
   212 val functionP =
   213   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   214     (P.and_list1 function_decl >> (fn eqnss =>
   215       Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss)));
   216 
   217 val terminationP =
   218   OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   219   ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
   220        >> (fn (name,dom) =>
   221 	      Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
   222 
   223 val _ = OuterSyntax.add_parsers [functionP];
   224 val _ = OuterSyntax.add_parsers [terminationP];
   225 
   226 
   227 end;
   228 
   229 
   230 end