src/HOL/Tools/function_package/fundef_package.ML
author wenzelm
Thu May 11 19:19:31 2006 +0200 (2006-05-11)
changeset 19617 7cb4b67d4b97
parent 19611 da2a0014c461
child 19770 be5c23ebe1eb
permissions -rw-r--r--
avoid raw equality on type thm;
     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 -> 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 end
    19 
    20 
    21 structure FundefPackage : FUNDEF_PACKAGE =
    22 struct
    23 
    24 open FundefCommon
    25 
    26 val True_implies = thm "True_implies"
    27 
    28 
    29 fun fundef_afterqed congs curry_info name data names atts thmss thy =
    30     let
    31 	val (complete_thm :: compat_thms) = map hd thmss
    32 	val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
    33 	val FundefResult {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
    34 
    35 
    36 	val Prep {names = Names {acc_R=accR, ...}, ...} = data
    37 	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    38 	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    39 
    40 	val thy = thy |> Theory.add_path name 
    41 
    42 	val thy = thy |> Theory.add_path "psimps"
    43 	val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy;
    44 	val thy = thy |> Theory.parent_path
    45 
    46 	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy
    47 	val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy
    48 	val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy
    49 	val (_,thy) = PureThy.add_thms [(("pinduct", simple_pinduct), [RuleCases.case_names names, InductAttrib.induct_set ""])] thy
    50 	val (_, thy) = PureThy.add_thmss [(("psimps", psimps), [Simplifier.simp_add])] thy
    51 	val thy = thy |> Theory.parent_path
    52     in
    53 	add_fundef_data name fundef_data thy
    54     end
    55 
    56 fun gen_add_fundef prep_att eqns_atts thy =
    57     let
    58 	val (natts, eqns) = split_list eqns_atts
    59 	val (names, raw_atts) = split_list natts
    60 
    61 	val atts = map (map (prep_att thy)) raw_atts
    62 
    63 	val congs = get_fundef_congs (Context.Theory thy)
    64 
    65 	val t_eqns = map (Sign.read_prop thy) eqns
    66 			 |> map (term_of o cterm_of thy) (* HACK to prevent strange things from happening with abbreviations *)
    67 
    68 	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs t_eqns thy
    69 	val Prep {complete, compat, ...} = data
    70 
    71 	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
    72     in
    73 	thy |> ProofContext.init
    74 	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data names atts) NONE ("", [])
    75 	    (map (fn t => (("", []), [(t, [])])) props)
    76     end
    77 
    78 
    79 fun total_termination_afterqed name thmss thy =
    80     let
    81 	val totality = hd (hd thmss)
    82 
    83 	val FundefResult {psimps, simple_pinduct, ... }
    84 	  = the (get_fundef_data name thy)
    85 
    86 	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
    87 
    88 	val tsimps = map remove_domain_condition psimps
    89 	val tinduct = remove_domain_condition simple_pinduct
    90 
    91 	val thy = Theory.add_path name thy
    92 		  
    93 		  (* Need the names and attributes. Apply the attributes again? *)
    94 (*	val thy = thy |> Theory.add_path "simps"
    95 	val (_, thy) = PureThy.add_thms ((names ~~ tsimps) ~~ atts) thy;
    96 	val thy = thy |> Theory.parent_path*)
    97 
    98 	val (_, thy) = PureThy.add_thms [(("induct", tinduct), [])] thy 
    99 	val (_, thy) = PureThy.add_thmss [(("simps", tsimps), [Simplifier.simp_add, RecfunCodegen.add NONE])] thy
   100 	val thy = Theory.parent_path thy
   101     in
   102 	thy
   103     end
   104 
   105 (*
   106 fun mk_partial_rules name D_name D domT idomT thmss thy =
   107     let
   108 	val [subs, dcl] = (hd thmss)
   109 
   110 	val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
   111 	  = the (Symtab.lookup (FundefData.get thy) name)
   112 
   113 	val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] 
   114 						    [SOME (cterm_of thy D)]
   115 						    subsetD)
   116 
   117 	val D_simps = map (curry op RS D_implies_dom) f_simps
   118 
   119 	val D_induct = subset_induct
   120 			   |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
   121 			   |> curry op COMP subs
   122 			   |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
   123 						 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
   124 
   125 	val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
   126 	val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
   127     in
   128 	thy3
   129     end
   130 *)
   131  
   132 
   133 fun fundef_setup_termination_proof name NONE thy = 
   134     let
   135 	val name = if name = "" then get_last_fundef thy else name
   136 	val data = the (get_fundef_data name thy)
   137 
   138 	val FundefResult {total_intro, ...} = data
   139 	val goal = FundefTermination.mk_total_termination_goal data
   140     in
   141 	thy |> ProofContext.init
   142 	    |> ProofContext.note_thmss_i [(("termination_intro", 
   143 					    [ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd
   144 	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", [])
   145 	    [(("", []), [(goal, [])])]
   146     end	
   147   | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
   148     let
   149 	val name = if name = "" then get_last_fundef thy else name
   150 	val data = the (get_fundef_data name thy)
   151 	val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
   152     in
   153 	thy |> ProofContext.init
   154 	    |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
   155 	    [(("", []), [(subs, []), (dcl, [])])]
   156     end	
   157 
   158 
   159 val add_fundef = gen_add_fundef Attrib.attribute
   160 
   161 
   162 
   163 (* congruence rules *)
   164 
   165 val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
   166 val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
   167 
   168 
   169 (* setup *)
   170 
   171 val setup = FundefData.init #> FundefCongs.init 
   172 	#>  Attrib.add_attributes
   173 		[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
   174 
   175 
   176 (* outer syntax *)
   177 
   178 local structure P = OuterParse and K = OuterKeyword in
   179 
   180 val function_decl =
   181     Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
   182 
   183 val functionP =
   184   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   185     (function_decl >> (fn eqns =>
   186       Toplevel.print o Toplevel.theory_to_proof (add_fundef eqns)));
   187 
   188 val terminationP =
   189   OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   190   ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
   191        >> (fn (name,dom) =>
   192 	      Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
   193 
   194 val _ = OuterSyntax.add_parsers [functionP];
   195 val _ = OuterSyntax.add_parsers [terminationP];
   196 
   197 
   198 end;
   199 
   200 
   201 end