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