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