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