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