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