TFL/tfl.ML
changeset 20062 60de4603e645
parent 19927 9286e99b2808
child 20088 bffda4cd0f79
equal deleted inserted replaced
20061:2b142bfb162a 20062:60de4603e645
    13   val trace_cterms: string -> cterm list -> unit
    13   val trace_cterms: string -> cterm list -> unit
    14   type pattern
    14   type pattern
    15   val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
    15   val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
    16   val wfrec_definition0: theory -> string -> term -> term -> theory * thm
    16   val wfrec_definition0: theory -> string -> term -> term -> theory * thm
    17   val post_definition: thm list -> theory * (thm * pattern list) ->
    17   val post_definition: thm list -> theory * (thm * pattern list) ->
    18    {theory: theory,
    18    {rules: thm,
    19     rules: thm,
       
    20     rows: int list,
    19     rows: int list,
    21     TCs: term list list,
    20     TCs: term list list,
    22     full_pats_TCs: (term * term list) list}
    21     full_pats_TCs: (term * term list) list}
    23   val wfrec_eqns: theory -> xstring -> thm list -> term list ->
    22   val wfrec_eqns: theory -> xstring -> thm list -> term list ->
    24    {WFR: term,
    23    {WFR: term,
   446                            given_pats
   445                            given_pats
   447      val (case_rewrites,context_congs) = extraction_thms theory
   446      val (case_rewrites,context_congs) = extraction_thms theory
   448      (*case_ss causes minimal simplification: bodies of case expressions are
   447      (*case_ss causes minimal simplification: bodies of case expressions are
   449        not simplified. Otherwise large examples (Red-Black trees) are too
   448        not simplified. Otherwise large examples (Red-Black trees) are too
   450        slow.*)
   449        slow.*)
   451      val case_ss = HOL_basic_ss addcongs
   450      val case_ss = Simplifier.theory_context theory
   452        (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) theory addsimps case_rewrites
   451        (HOL_basic_ss addcongs
       
   452          (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) theory addsimps case_rewrites)
   453      val corollaries' = map (Simplifier.simplify case_ss) corollaries
   453      val corollaries' = map (Simplifier.simplify case_ss) corollaries
   454      val extract = R.CONTEXT_REWRITE_RULE
   454      val extract = R.CONTEXT_REWRITE_RULE
   455                      (f, [R], cut_apply, meta_tflCongs@context_congs)
   455                      (f, [R], cut_apply, meta_tflCongs@context_congs)
   456      val (rules, TCs) = ListPair.unzip (map extract corollaries')
   456      val (rules, TCs) = ListPair.unzip (map extract corollaries')
   457      val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
   457      val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
   458      val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
   458      val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
   459      val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
   459      val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
   460  in
   460  in
   461  {theory = theory,
   461  {rules = rules1,
   462   rules = rules1,
       
   463   rows = rows,
   462   rows = rows,
   464   full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
   463   full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
   465   TCs = TCs}
   464   TCs = TCs}
   466  end;
   465  end;
   467 
   466