src/HOL/Tools/function_package/fundef_package.ML
author krauss
Mon, 31 Jul 2006 18:07:42 +0200
changeset 20270 3abe7dae681e
parent 19938 241a7777a3ff
child 20285 23f5cd23c1e1
permissions -rw-r--r--
Function package can now do automatic splits of overlapping datatype patterns
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
     1
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
     2
(*  Title:      HOL/Tools/function_package/fundef_package.ML
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
     3
    ID:         $Id$
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
     4
    Author:     Alexander Krauss, TU Muenchen
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
     5
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
     6
A package for general recursive function definitions. 
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
     7
Isar commands.
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
     8
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
     9
*)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    10
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    11
signature FUNDEF_PACKAGE = 
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    12
sig
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    13
    val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *)
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    14
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    15
    val cong_add: attribute
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    16
    val cong_del: attribute
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    17
							 
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    18
    val setup : theory -> theory
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    19
    val get_congs : theory -> thm list
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    20
end
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    21
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    22
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    23
structure FundefPackage : FUNDEF_PACKAGE =
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    24
struct
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    25
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    26
open FundefCommon
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    27
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    28
val True_implies = thm "True_implies"
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    29
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    30
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    31
fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy =
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    32
    let 
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    33
      val psimpss = Library.unflat (map snd spec_part) psimps
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    34
      val (names, attss) = split_list (map fst spec_part) 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    35
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    36
      val thy = thy |> Theory.add_path f_name 
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    37
                
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    38
      val thy = thy |> Theory.add_path label
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    39
      val spsimpss = map (map standard) psimpss (* FIXME *)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    40
      val add_list = (names ~~ spsimpss) ~~ attss
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    41
      val (_, thy) = PureThy.add_thmss add_list thy
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    42
      val thy = thy |> Theory.parent_path
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    43
                
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    44
      val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    45
      val thy = thy |> Theory.parent_path
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    46
    in
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    47
      thy
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    48
    end
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    49
    
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    50
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    51
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    52
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    53
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    54
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    55
fun fundef_afterqed congs mutual_info name data spec [[result]] thy =
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    56
    let
19922
984ae977f7aa Fixed name clash.
krauss
parents: 19876
diff changeset
    57
	val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
984ae977f7aa Fixed name clash.
krauss
parents: 19876
diff changeset
    58
	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
984ae977f7aa Fixed name clash.
krauss
parents: 19876
diff changeset
    59
        val Mutual {parts, ...} = mutual_info
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    60
19583
c5fa77b03442 function-package: Changed record usage to make sml/nj happy...
krauss
parents: 19564
diff changeset
    61
	val Prep {names = Names {acc_R=accR, ...}, ...} = data
c5fa77b03442 function-package: Changed record usage to make sml/nj happy...
krauss
parents: 19564
diff changeset
    62
	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
c5fa77b03442 function-package: Changed record usage to make sml/nj happy...
krauss
parents: 19564
diff changeset
    63
	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    64
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    65
        val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    66
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    67
        val casenames = flat (map (map (fst o fst)) spec)
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    68
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    69
	val thy = thy |> Theory.add_path name
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    70
	val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    71
	val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
19922
984ae977f7aa Fixed name clash.
krauss
parents: 19876
diff changeset
    72
	val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    73
	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    74
	val thy = thy |> Theory.parent_path
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    75
    in
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    76
      add_fundef_data name (fundef_data, mutual_info, spec) thy
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    77
    end
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    78
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    79
fun gen_add_fundef prep_att eqns_attss preprocess thy =
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    80
    let
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    81
      fun prep_eqns neqs =
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    82
          neqs
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    83
            |> map (apsnd (Sign.read_prop thy))    
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    84
            |> map (apfst (apsnd (apfst (map (prep_att thy)))))
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    85
            |> FundefSplit.split_some_equations (ProofContext.init thy)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    86
      
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    87
      val spec = map prep_eqns eqns_attss
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    88
      val t_eqnss = map (flat o map snd) spec
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
    89
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    90
(*
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    91
 val t_eqns = if preprocess then map (FundefSplit.split_all_equations (ProofContext.init thy)) t_eqns
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    92
              else t_eqns
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    93
*)
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    94
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    95
      val congs = get_fundef_congs (Context.Theory thy)
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    96
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    97
      val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
    98
      val Prep {goal, goalI, ...} = data
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
    99
    in
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   100
	thy |> ProofContext.init
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   101
	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data spec) NONE ("", [])
19922
984ae977f7aa Fixed name clash.
krauss
parents: 19876
diff changeset
   102
	    [(("", []), [(goal, [])])]
984ae977f7aa Fixed name clash.
krauss
parents: 19876
diff changeset
   103
            |> Proof.refine (Method.primitive_text (fn _ => goalI))
984ae977f7aa Fixed name clash.
krauss
parents: 19876
diff changeset
   104
            |> Seq.hd
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   105
    end
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   106
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   107
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
   108
fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy =
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   109
    let
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   110
	val totality = hd (hd thmss)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   111
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   112
	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   113
	  = the (get_fundef_data name thy)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   114
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   115
	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   116
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
   117
	val tsimps = map (map remove_domain_condition) psimps
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
   118
	val tinduct = map remove_domain_condition simple_pinducts
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
   119
19784
fa5080577da9 HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
krauss
parents: 19782
diff changeset
   120
        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
fa5080577da9 HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
krauss
parents: 19782
diff changeset
   121
        val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
fa5080577da9 HOL/Tools/function_package: Applies CodeGen attributes again, where possible.
krauss
parents: 19782
diff changeset
   122
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   123
        val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   124
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   125
	val thy = Theory.add_path name thy
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   126
		  
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
   127
	val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy 
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   128
	val thy = Theory.parent_path thy
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   129
    in
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   130
	thy
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   131
    end
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   132
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   133
(*
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   134
fun mk_partial_rules name D_name D domT idomT thmss thy =
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   135
    let
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   136
	val [subs, dcl] = (hd thmss)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   137
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   138
	val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   139
	  = the (Symtab.lookup (FundefData.get thy) name)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   140
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   141
	val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] 
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   142
						    [SOME (cterm_of thy D)]
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   143
						    subsetD)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   144
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   145
	val D_simps = map (curry op RS D_implies_dom) f_simps
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   146
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   147
	val D_induct = subset_induct
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   148
			   |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   149
			   |> curry op COMP subs
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   150
			   |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   151
						 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   152
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   153
	val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   154
	val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   155
    in
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   156
	thy3
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   157
    end
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   158
*)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   159
 
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   160
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   161
fun fundef_setup_termination_proof name NONE thy = 
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   162
    let
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   163
	val name = if name = "" then get_last_fundef thy else name
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   164
	val data = the (get_fundef_data name thy)
19938
241a7777a3ff Removed (term_of o cterm_of)-Hack, Added error message for unknown definition at "termination"-command
krauss
parents: 19922
diff changeset
   165
                   handle Option.Option => raise ERROR ("No such function definition: " ^ name)
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   166
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   167
	val (res as FundefMResult {termination, ...}, mutual, _) = data
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   168
	val goal = FundefTermination.mk_total_termination_goal data
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   169
    in
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   170
	thy |> ProofContext.init
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
   171
	    |> ProofContext.note_thmss_i [(("termination", 
19922
984ae977f7aa Fixed name clash.
krauss
parents: 19876
diff changeset
   172
					    [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
   173
	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", [])
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19583
diff changeset
   174
	    [(("", []), [(goal, [])])]
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   175
    end	
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   176
  | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   177
    let
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   178
	val name = if name = "" then get_last_fundef thy else name
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   179
	val data = the (get_fundef_data name thy)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   180
	val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   181
    in
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   182
	thy |> ProofContext.init
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   183
	    |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19583
diff changeset
   184
	    [(("", []), [(subs, []), (dcl, [])])]
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   185
    end	
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   186
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   187
19611
da2a0014c461 Function Package: Quick-and-dirty-fixed strange "Proved a different theorem bug"
krauss
parents: 19585
diff changeset
   188
val add_fundef = gen_add_fundef Attrib.attribute
da2a0014c461 Function Package: Quick-and-dirty-fixed strange "Proved a different theorem bug"
krauss
parents: 19585
diff changeset
   189
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   190
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   191
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   192
(* congruence rules *)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   193
19617
7cb4b67d4b97 avoid raw equality on type thm;
wenzelm
parents: 19611
diff changeset
   194
val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
7cb4b67d4b97 avoid raw equality on type thm;
wenzelm
parents: 19611
diff changeset
   195
val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   196
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   197
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   198
(* setup *)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   199
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   200
val setup = FundefData.init #> FundefCongs.init 
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   201
	#>  Attrib.add_attributes
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   202
		[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   203
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   204
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
   205
val get_congs = FundefCommon.get_fundef_congs o Context.Theory
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
   206
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19617
diff changeset
   207
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   208
(* outer syntax *)
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   209
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   210
local structure P = OuterParse and K = OuterKeyword in
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   211
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   212
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   213
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   214
val star = Scan.one (fn t => (OuterLex.val_of t = "*"));
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   215
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   216
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   217
val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME)) 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   218
                                               >> (fn x => (map_filter I x, exists is_none x)))
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   219
                              --| P.$$$ "]";
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   220
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   221
val opt_attribs_with_star = Scan.optional attribs_with_star ([], false);
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   222
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   223
fun opt_thm_name_star s =
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   224
  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ s) ("", ([], false));
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   225
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   226
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   227
val function_decl =
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   228
    Scan.repeat1 (opt_thm_name_star ":" -- P.prop);
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   229
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   230
val functionP =
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   231
  OuterSyntax.command "function" "define general recursive functions" K.thy_goal
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   232
  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "pre" -- P.$$$ ")") >> K true) false) --    
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   233
  P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19938
diff changeset
   234
                                    Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   235
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   236
val terminationP =
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   237
  OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   238
  ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   239
       >> (fn (name,dom) =>
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   240
	      Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   241
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   242
val _ = OuterSyntax.add_parsers [functionP];
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   243
val _ = OuterSyntax.add_parsers [terminationP];
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   244
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   245
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   246
end;
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   247
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff changeset
   248
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19583
diff changeset
   249
end