src/HOL/Datatype_Examples/IsaFoR.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58313 57d2e5006d29
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/Datatype_Examples/IsaFoR.thy
     2     Author:     Rene Thiemann, UIBK
     3     Copyright   2014
     4 
     5 Benchmark consisting of datatypes defined in IsaFoR.
     6 *)
     7 
     8 header {* Benchmark Consisting of Datatypes Defined in IsaFoR *}
     9 
    10 theory IsaFoR
    11 imports Real
    12 begin
    13 
    14 datatype (discs_sels) ('f, 'l) lab =
    15     Lab "('f, 'l) lab" 'l
    16   | FunLab "('f, 'l) lab" "('f, 'l) lab list"
    17   | UnLab 'f
    18   | Sharp "('f, 'l) lab"
    19 
    20 datatype (discs_sels) 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
    21 
    22 datatype (discs_sels) ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
    23 datatype (discs_sels) ('f, 'v) ctxt =
    24     Hole ("\<box>")
    25   | More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
    26 
    27 type_synonym ('f, 'v) rule = "('f, 'v) term \<times> ('f, 'v) term"
    28 type_synonym ('f, 'v) trs  = "('f, 'v) rule set"
    29 
    30 type_synonym ('f, 'v) rules = "('f, 'v) rule list"
    31 type_synonym ('f, 'l, 'v) ruleLL  = "(('f, 'l) lab, 'v) rule"
    32 type_synonym ('f, 'l, 'v) trsLL   = "(('f, 'l) lab, 'v) rules"
    33 type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list"
    34 
    35 datatype (discs_sels) pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
    36 
    37 type_synonym  ('f, 'v) prseq = "(pos \<times> ('f, 'v) rule \<times> bool \<times> ('f, 'v) term) list"
    38 type_synonym  ('f, 'v) rseq = "(pos \<times> ('f, 'v) rule \<times> ('f, 'v) term) list"
    39 
    40 type_synonym ('f, 'l, 'v) rseqL   = "((('f, 'l) lab, 'v) rule \<times> (('f, 'l) lab, 'v) rseq) list"
    41 type_synonym ('f, 'l, 'v) dppLL   =
    42   "bool \<times> bool \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL \<times>
    43   ('f, 'l, 'v) termsLL \<times>
    44   ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL"
    45 
    46 type_synonym ('f, 'l, 'v) qreltrsLL =
    47   "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL"
    48 
    49 type_synonym ('f, 'l, 'v) qtrsLL =
    50   "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL"
    51 
    52 datatype (discs_sels) location = H | A | B | R
    53 
    54 type_synonym ('f, 'v) forb_pattern = "('f, 'v) ctxt \<times> ('f, 'v) term \<times> location"
    55 type_synonym ('f, 'v) forb_patterns = "('f, 'v) forb_pattern set"
    56 
    57 type_synonym ('f, 'l, 'v) fptrsLL =
    58   "(('f, 'l) lab, 'v) forb_pattern list \<times> ('f, 'l, 'v) trsLL"
    59 
    60 type_synonym ('f, 'l, 'v) prob = "('f, 'l, 'v) qreltrsLL + ('f, 'l, 'v) dppLL"
    61 
    62 type_synonym ('f, 'a) lpoly_inter = "'f \<times> nat \<Rightarrow> ('a \<times> 'a list)"
    63 type_synonym ('f, 'a) lpoly_interL = "(('f \<times> nat) \<times> ('a \<times> 'a list)) list"
    64 
    65 type_synonym 'v monom = "('v \<times> nat) list"
    66 type_synonym ('v, 'a) poly = "('v monom \<times> 'a) list"
    67 type_synonym ('f, 'a) poly_inter_list = "(('f \<times> nat) \<times> (nat, 'a) poly) list"
    68 type_synonym 'a vec = "'a list"
    69 type_synonym 'a mat = "'a vec list"
    70 
    71 datatype (discs_sels) arctic = MinInfty | Num_arc int
    72 datatype (discs_sels) 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
    73 datatype (discs_sels) order_tag = Lex | Mul
    74 
    75 type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag)) list"
    76 
    77 datatype (discs_sels) af_entry =
    78     Collapse nat
    79   | AFList "nat list"
    80 
    81 type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry) list"
    82 type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option))) list \<times> nat"
    83 
    84 datatype (discs_sels) 'f redtriple_impl =
    85     Int_carrier "('f, int) lpoly_interL"
    86   | Int_nl_carrier "('f, int) poly_inter_list"
    87   | Rat_carrier "('f, rat) lpoly_interL"
    88   | Rat_nl_carrier rat "('f, rat) poly_inter_list"
    89   | Real_carrier "('f, real) lpoly_interL"
    90   | Real_nl_carrier real "('f, real) poly_inter_list"
    91   | Arctic_carrier "('f, arctic) lpoly_interL"
    92   | Arctic_rat_carrier "('f, rat arctic_delta) lpoly_interL"
    93   | Int_mat_carrier nat nat "('f, int mat) lpoly_interL"
    94   | Rat_mat_carrier nat nat "('f, rat mat) lpoly_interL"
    95   | Real_mat_carrier nat nat "('f, real mat) lpoly_interL"
    96   | Arctic_mat_carrier nat "('f, arctic mat) lpoly_interL"
    97   | Arctic_rat_mat_carrier nat "('f, rat arctic_delta mat) lpoly_interL"
    98   | RPO "'f status_prec_repr" "'f afs_list"
    99   | KBO "'f prec_weight_repr" "'f afs_list"
   100 
   101 datatype (discs_sels) list_order_type = MS_Ext | Max_Ext | Min_Ext  | Dms_Ext
   102 type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list"
   103 
   104 datatype (discs_sels) 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
   105 
   106 type_synonym 'f sig_map_list = "(('f \<times> nat) \<times> 'f list) list"
   107 type_synonym ('f, 'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f, 'v) rules \<times> ('f, 'v) rules"
   108 
   109 datatype (discs_sels) arithFun =
   110     Arg nat
   111   | Const nat
   112   | Sum "arithFun list"
   113   | Max "arithFun list"
   114   | Min "arithFun list"
   115   | Prod "arithFun list"
   116   | IfEqual arithFun arithFun arithFun arithFun
   117 
   118 datatype (discs_sels) 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
   119 datatype (discs_sels) ('f, 'v) sl_variant =
   120     Rootlab "('f \<times> nat) option"
   121   | Finitelab "'f sl_inter"
   122   | QuasiFinitelab "'f sl_inter" 'v
   123 
   124 type_synonym ('f, 'v) crit_pair_joins = "(('f, 'v) term \<times> ('f, 'v) rseq \<times> ('f, 'v) term \<times> ('f, 'v) rseq) list"
   125 
   126 datatype (discs_sels) 'f join_info = Guided "('f, string) crit_pair_joins" | Join_NF | Join_BFS nat
   127 
   128 type_synonym unknown_info = string
   129 
   130 type_synonym dummy_prf = unit
   131 
   132 datatype (discs_sels) ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
   133   "('f, 'v) term"
   134   "(('f, 'v) rule \<times> ('f, 'v) rule) list"
   135 
   136 datatype (discs_sels) ('f, 'v) cond_constraint =
   137     CC_cond bool "('f, 'v) rule"
   138   | CC_rewr "('f, 'v) term" "('f, 'v) term"
   139   | CC_impl "('f, 'v) cond_constraint list" "('f, 'v) cond_constraint"
   140   | CC_all 'v "('f, 'v) cond_constraint"
   141 
   142 type_synonym ('f, 'v, 'w) gsubstL = "('v \<times> ('f, 'w) term) list"
   143 type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL"
   144 
   145 datatype (discs_sels) ('f, 'v) cond_constraint_prf =
   146     Final
   147   | Delete_Condition "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   148   | Different_Constructor "('f, 'v) cond_constraint"
   149   | Same_Constructor "('f, 'v) cond_constraint" "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   150   | Variable_Equation 'v "('f, 'v) term" "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   151   | Funarg_Into_Var "('f, 'v) cond_constraint" nat 'v "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   152   | Simplify_Condition "('f, 'v) cond_constraint" "('f, 'v) substL" "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   153   | Induction "('f, 'v) cond_constraint" "('f, 'v) cond_constraint list" "(('f, 'v) rule \<times> (('f, 'v) term \<times> 'v list) list \<times> ('f, 'v) cond_constraint \<times> ('f, 'v) cond_constraint_prf) list"
   154 
   155 datatype (discs_sels) ('f, 'v) cond_red_pair_prf =
   156   Cond_Red_Pair_Prf
   157     'f "(('f, 'v) cond_constraint \<times> ('f, 'v) rules \<times> ('f, 'v) cond_constraint_prf) list" nat nat
   158 
   159 datatype (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
   160 datatype (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \<times> 'q) list"
   161 datatype (discs_sels) 'q ta_relation =
   162     Decision_Proc
   163   | Id_Relation
   164   | Some_Relation "('q \<times> 'q) list"
   165 
   166 datatype (discs_sels) boundstype = Roof | Match
   167 datatype (discs_sels) ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
   168 
   169 datatype (discs_sels) ('f, 'v) pat_eqv_prf =
   170     Pat_Dom_Renaming "('f, 'v) substL"
   171   | Pat_Irrelevant "('f, 'v) substL" "('f, 'v) substL"
   172   | Pat_Simplify "('f, 'v) substL" "('f, 'v) substL"
   173 
   174 datatype (discs_sels) pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
   175 
   176 datatype (discs_sels) ('f, 'v) pat_rule_prf =
   177     Pat_OrigRule "('f, 'v) rule" bool
   178   | Pat_InitPump "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL"
   179   | Pat_InitPumpCtxt "('f, 'v) pat_rule_prf" "('f, 'v) substL" pos 'v
   180   | Pat_Equiv "('f, 'v) pat_rule_prf" bool "('f, 'v) pat_eqv_prf"
   181   | Pat_Narrow "('f, 'v) pat_rule_prf" "('f, 'v) pat_rule_prf" pos
   182   | Pat_Inst "('f, 'v) pat_rule_prf" "('f, 'v) substL" pat_rule_pos
   183   | Pat_Rewr "('f, 'v) pat_rule_prf" "('f, 'v) term \<times> ('f, 'v) rseq" pat_rule_pos 'v
   184   | Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat
   185 
   186 datatype (discs_sels) ('f, 'v) non_loop_prf =
   187     Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos
   188 
   189 datatype (discs_sels) ('f, 'l, 'v) problem =
   190     SN_TRS "('f, 'l, 'v) qreltrsLL"
   191   | SN_FP_TRS "('f, 'l, 'v) fptrsLL"
   192   | Finite_DPP "('f, 'l, 'v) dppLL"
   193   | Unknown_Problem unknown_info
   194   | Not_SN_TRS "('f, 'l, 'v) qtrsLL"
   195   | Not_RelSN_TRS "('f, 'l, 'v) qreltrsLL"
   196   | Infinite_DPP "('f, 'l, 'v) dppLL"
   197   | Not_SN_FP_TRS "('f, 'l, 'v) fptrsLL"
   198 
   199 declare [[bnf_timing]]
   200 
   201 datatype (discs_sels) ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof =
   202     SN_assm_proof "('f, 'l, 'v) qreltrsLL" 'a
   203   | Finite_assm_proof "('f, 'l, 'v) dppLL" 'b
   204   | SN_FP_assm_proof "('f, 'l, 'v) fptrsLL" 'c
   205   | Not_SN_assm_proof "('f, 'l, 'v) qtrsLL" 'a
   206   | Infinite_assm_proof "('f, 'l, 'v) dppLL" 'b
   207   | Not_RelSN_assm_proof "('f, 'l, 'v) qreltrsLL" 'c
   208   | Not_SN_FP_assm_proof "('f, 'l, 'v) fptrsLL" 'd
   209   | Unknown_assm_proof unknown_info 'e
   210 
   211 type_synonym ('f, 'l, 'v, 'a, 'b, 'c, 'd) assm_proof = "('f, 'l, 'v, 'a, 'b, 'c, dummy_prf, 'd) generic_assm_proof"
   212 
   213 datatype (discs_sels) ('f, 'l, 'v) assm =
   214     SN_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) qreltrsLL"
   215   | SN_FP_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) fptrsLL"
   216   | Finite_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) dppLL"
   217   | Unknown_assm "('f, 'l, 'v) problem list" unknown_info
   218   | Not_SN_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) qtrsLL"
   219   | Not_RelSN_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) qreltrsLL"
   220   | Not_SN_FP_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) fptrsLL"
   221   | Infinite_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) dppLL"
   222 
   223 fun satisfied :: "('f, 'l, 'v) problem \<Rightarrow> bool" where
   224   "satisfied (SN_TRS t) = (t = t)"
   225 | "satisfied (SN_FP_TRS t) = (t \<noteq> t)"
   226 | "satisfied (Finite_DPP d) = (d \<noteq> d)"
   227 | "satisfied (Unknown_Problem s) = (s = ''foo'')"
   228 | "satisfied (Not_SN_TRS (nfs, q, r)) = (length q = length r)"
   229 | "satisfied (Not_RelSN_TRS (nfs, q, r, rw)) = (r = rw)"
   230 | "satisfied (Infinite_DPP d) = (d = d)"
   231 | "satisfied (Not_SN_FP_TRS t) = (t = t)"
   232 
   233 fun collect_assms :: "('tp \<Rightarrow> ('f, 'l, 'v) assm list)
   234   \<Rightarrow> ('dpp \<Rightarrow> ('f, 'l, 'v) assm list)
   235   \<Rightarrow> ('fptp \<Rightarrow> ('f, 'l, 'v) assm list)
   236   \<Rightarrow> ('unk \<Rightarrow> ('f, 'l, 'v) assm list)
   237   \<Rightarrow> ('f, 'l, 'v, 'tp, 'dpp, 'fptp, 'unk) assm_proof \<Rightarrow> ('f, 'l, 'v) assm list" where
   238   "collect_assms tp dpp fptp unk (SN_assm_proof t prf) = tp prf"
   239 | "collect_assms tp dpp fptp unk (SN_FP_assm_proof t prf) = fptp prf"
   240 | "collect_assms tp dpp fptp unk (Finite_assm_proof d prf) = dpp prf"
   241 | "collect_assms tp dpp fptp unk (Unknown_assm_proof p prf) = unk prf"
   242 | "collect_assms _ _ _ _ _ = []"
   243 
   244 fun collect_neg_assms :: "('tp \<Rightarrow> ('f, 'l, 'v) assm list)
   245   \<Rightarrow> ('dpp \<Rightarrow> ('f, 'l, 'v) assm list)
   246   \<Rightarrow> ('rtp \<Rightarrow> ('f, 'l, 'v) assm list)
   247   \<Rightarrow> ('fptp \<Rightarrow> ('f, 'l, 'v) assm list)
   248   \<Rightarrow> ('unk \<Rightarrow> ('f, 'l, 'v) assm list)
   249   \<Rightarrow> ('f, 'l, 'v, 'tp, 'dpp, 'rtp, 'fptp, 'unk) generic_assm_proof \<Rightarrow> ('f, 'l, 'v) assm list" where
   250   "collect_neg_assms tp dpp rtp fptp unk (Not_SN_assm_proof t prf) = tp prf"
   251 | "collect_neg_assms tp dpp rtp fptp unk (Infinite_assm_proof d prf) = dpp prf"
   252 | "collect_neg_assms tp dpp rtp fptp unk (Not_RelSN_assm_proof t prf) = rtp prf"
   253 | "collect_neg_assms tp dpp rtp fptp unk (Not_SN_FP_assm_proof t prf) = fptp prf"
   254 | "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf"
   255 | "collect_neg_assms tp dpp rtp fptp unk _ = []"
   256 
   257 datatype (discs_sels) ('f, 'l, 'v) dp_nontermination_proof =
   258     DP_Loop "(('f, 'l) lab, 'v) term" "(('f, 'l) lab, 'v) prseq" "(('f, 'l) lab, 'v) substL" "(('f, 'l) lab, 'v) ctxt"
   259   | DP_Nonloop "(('f, 'l) lab, 'v) non_loop_prf"
   260   | DP_Rule_Removal "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_nontermination_proof"
   261   | DP_Q_Increase "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_nontermination_proof"
   262   | DP_Q_Reduction "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_nontermination_proof"
   263   | DP_Termination_Switch "('f, 'l) lab join_info" "('f, 'l, 'v) dp_nontermination_proof"
   264   | DP_Instantiation "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_nontermination_proof"
   265   | DP_Rewriting "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" "(('f, 'l) lab, 'v) rule" pos "('f, 'l, 'v) dp_nontermination_proof"
   266   | DP_Narrowing "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_nontermination_proof"
   267   | DP_Assume_Infinite  "('f, 'l, 'v) dppLL"
   268       "('f, 'l, 'v, ('f, 'l, 'v) trs_nontermination_proof,
   269        ('f, 'l, 'v) dp_nontermination_proof,
   270        ('f, 'l, 'v) reltrs_nontermination_proof,
   271        ('f, 'l, 'v) fp_nontermination_proof,
   272        ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   273 and ('f, 'l, 'v) "trs_nontermination_proof" =
   274     TRS_Loop "(('f, 'l) lab, 'v) term" "(('f, 'l) lab, 'v) rseq" "(('f, 'l) lab, 'v) substL" "(('f, 'l) lab, 'v) ctxt"
   275   | TRS_Not_Well_Formed
   276   | TRS_Rule_Removal "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_nontermination_proof"
   277   | TRS_String_Reversal "('f, 'l, 'v) trs_nontermination_proof"
   278   | TRS_DP_Trans "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_nontermination_proof"
   279   | TRS_Nonloop "(('f, 'l) lab, 'v) non_loop_prf"
   280   | TRS_Q_Increase "('f, 'l, 'v) termsLL" "('f, 'l, 'v) trs_nontermination_proof"
   281   | TRS_Assume_Not_SN  "('f, 'l, 'v) qtrsLL"
   282       "('f, 'l, 'v, ('f, 'l, 'v) trs_nontermination_proof,
   283        ('f, 'l, 'v) dp_nontermination_proof,
   284        ('f, 'l, 'v) reltrs_nontermination_proof,
   285        ('f, 'l, 'v) fp_nontermination_proof,
   286        ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   287 and ('f, 'l, 'v)"reltrs_nontermination_proof" =
   288     Rel_Loop "(('f, 'l) lab, 'v) term" "(('f, 'l) lab, 'v) prseq" "(('f, 'l) lab, 'v) substL" "(('f, 'l) lab, 'v) ctxt"
   289   | Rel_Not_Well_Formed
   290   | Rel_Rule_Removal "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) reltrs_nontermination_proof"
   291   | Rel_R_Not_SN "('f, 'l, 'v) trs_nontermination_proof"
   292   | Rel_TRS_Assume_Not_SN  "('f, 'l, 'v) qreltrsLL"
   293       "('f, 'l, 'v, ('f, 'l, 'v) trs_nontermination_proof,
   294        ('f, 'l, 'v) dp_nontermination_proof,
   295        ('f, 'l, 'v) reltrs_nontermination_proof,
   296        ('f, 'l, 'v) fp_nontermination_proof,
   297        ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   298 and ('f, 'l, 'v) "fp_nontermination_proof" =
   299     FPTRS_Loop "(('f, 'l) lab, 'v) term" "(('f, 'l) lab, 'v) rseq" "(('f, 'l) lab, 'v) substL" "(('f, 'l) lab, 'v) ctxt"
   300   | FPTRS_Rule_Removal "('f, 'l, 'v) trsLL" "('f, 'l, 'v) fp_nontermination_proof"
   301   | FPTRS_Assume_Not_SN  "('f, 'l, 'v) fptrsLL"
   302       "('f, 'l, 'v, ('f, 'l, 'v) trs_nontermination_proof,
   303        ('f, 'l, 'v) dp_nontermination_proof,
   304        ('f, 'l, 'v) reltrs_nontermination_proof,
   305        ('f, 'l, 'v) fp_nontermination_proof,
   306        ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   307 and ('f, 'l, 'v) neg_unknown_proof =
   308     Assume_NT_Unknown unknown_info
   309       "('f, 'l, 'v, ('f, 'l, 'v) trs_nontermination_proof,
   310        ('f, 'l, 'v) dp_nontermination_proof,
   311        ('f, 'l, 'v) reltrs_nontermination_proof,
   312        ('f, 'l, 'v) fp_nontermination_proof,
   313        ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   314 
   315 datatype (discs_sels) ('f, 'l, 'v) dp_termination_proof =
   316     P_is_Empty
   317   | Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL"
   318       "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   319   | Redpair_Proc "('f, 'l) lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL"  "('f, 'l, 'v) dp_termination_proof"
   320   | Redpair_UR_Proc "('f, 'l) lab root_redtriple_impl + ('f, 'l) lab redtriple_impl"
   321       "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   322   | Usable_Rules_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   323   | Dep_Graph_Proc "(('f, 'l, 'v) dp_termination_proof option \<times> ('f, 'l, 'v) trsLL) list"
   324   | Mono_Redpair_Proc "('f, 'l) lab redtriple_impl"
   325       "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   326   | Mono_Redpair_UR_Proc "('f, 'l) lab redtriple_impl"
   327       "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   328   | Size_Change_Subterm_Proc "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
   329   | Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option"
   330       "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
   331   | Uncurry_Proc "nat option" "(('f, 'l) lab, 'v) uncurry_info"
   332       "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   333   | Fcc_Proc "('f, 'l) lab" "(('f, 'l) lab, 'v) ctxt list"
   334       "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   335   | Split_Proc
   336       "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL"
   337       "('f, 'l, 'v) dp_termination_proof" "('f, 'l, 'v) dp_termination_proof"
   338   | Semlab_Proc
   339       "(('f, 'l) lab, 'v) sl_variant" "('f, 'l, 'v) trsLL"
   340       "(('f, 'l) lab, 'v) term list" "('f, 'l, 'v) trsLL"
   341       "('f, 'l, 'v) dp_termination_proof"
   342   | Switch_Innermost_Proc "('f, 'l) lab join_info" "('f, 'l, 'v) dp_termination_proof"
   343   | Rewriting_Proc
   344       "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL"
   345       "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) dp_termination_proof"
   346   | Instantiation_Proc "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   347   | Forward_Instantiation_Proc
   348       "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_termination_proof"
   349   | Narrowing_Proc "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   350   | Assume_Finite
   351       "('f, 'l, 'v) dppLL" "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list"
   352   | Unlab_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   353   | Q_Reduction_Proc "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_termination_proof"
   354   | Complex_Constant_Removal_Proc "(('f, 'l) lab, 'v) complex_constant_removal_prf" "('f, 'l, 'v) dp_termination_proof"
   355   | General_Redpair_Proc
   356       "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL"
   357       "(('f, 'l) lab, 'v) cond_red_pair_prf" "('f, 'l, 'v) dp_termination_proof list"
   358   | To_Trs_Proc "('f, 'l, 'v) trs_termination_proof"
   359 and ('f, 'l, 'v) trs_termination_proof =
   360     DP_Trans bool bool "(('f, 'l) lab, 'v) rules" "('f, 'l, 'v) dp_termination_proof"
   361   | Rule_Removal "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   362   | String_Reversal "('f, 'l, 'v) trs_termination_proof"
   363   | Bounds "(('f, 'l) lab, 'v) bounds_info"
   364   | Uncurry "(('f, 'l) lab, 'v) uncurry_info" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   365   | Semlab
   366       "(('f, 'l) lab, 'v) sl_variant" "(('f, 'l) lab, 'v) term list"
   367       "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   368   | R_is_Empty
   369   | Fcc "(('f, 'l) lab, 'v) ctxt list" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   370   | Split "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" "('f, 'l, 'v) trs_termination_proof"
   371   | Switch_Innermost "('f, 'l) lab join_info" "('f, 'l, 'v) trs_termination_proof"
   372   | Drop_Equality "('f, 'l, 'v) trs_termination_proof"
   373   | Remove_Nonapplicable_Rules "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   374   | Assume_SN "('f, 'l, 'v) qreltrsLL" "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list"
   375 and ('f, 'l, 'v) unknown_proof =
   376     Assume_Unknown unknown_info "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list"
   377 and ('f, 'l, 'v) fptrs_termination_proof =
   378     Assume_FP_SN "('f, 'l, 'v) fptrsLL" "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list"
   379 
   380 end