regression test for datatypes defined in IsaFoR
authortraytel
Mon Jul 21 18:04:08 2014 +0200 (2014-07-21)
changeset 575865efff4075b63
parent 57585 ce06a901c050
child 57597 5c3484b90d5c
regression test for datatypes defined in IsaFoR
src/HOL/BNF_Examples/IsaFoR_Datatypes.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF_Examples/IsaFoR_Datatypes.thy	Mon Jul 21 18:04:08 2014 +0200
     1.3 @@ -0,0 +1,380 @@
     1.4 +(*  Title:      HOL/BNF_Examples/IsaFoR_Datatypes.thy
     1.5 +    Author:     René Thiemann
     1.6 +    Copyright   2014
     1.7 +
     1.8 +Benchmark of datatypes defined in IsaFoR
     1.9 +*)
    1.10 +
    1.11 +theory IsaFoR_Datatypes
    1.12 +imports
    1.13 +  Real
    1.14 +begin
    1.15 +
    1.16 +datatype_new ('f, 'l) lab =
    1.17 +  Lab "('f, 'l) lab" 'l
    1.18 +| FunLab "('f, 'l) lab" "('f, 'l) lab list"
    1.19 +| UnLab 'f
    1.20 +| Sharp "('f, 'l) lab"
    1.21 +
    1.22 +datatype_new 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
    1.23 +
    1.24 +datatype_new ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
    1.25 +datatype_new ('f, 'v) ctxt =
    1.26 +  Hole ("\<box>")
    1.27 +| More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
    1.28 +
    1.29 +
    1.30 +type_synonym ('f, 'v) rule = "('f, 'v) term \<times> ('f, 'v) term"
    1.31 +type_synonym ('f, 'v) trs  = "('f, 'v) rule set"
    1.32 +
    1.33 +type_synonym ('f, 'v) rules = "('f,'v) rule list"
    1.34 +type_synonym ('f, 'l, 'v) ruleLL  = "(('f, 'l) lab, 'v) rule"
    1.35 +type_synonym ('f, 'l, 'v) trsLL   = "(('f, 'l) lab, 'v) rules"
    1.36 +type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list"
    1.37 +datatype_new pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
    1.38 +type_synonym  ('f, 'v) prseq = "(pos \<times> ('f, 'v) rule \<times> bool \<times> ('f, 'v) term) list"
    1.39 +type_synonym  ('f, 'v) rseq = "(pos \<times> ('f, 'v) rule \<times> ('f, 'v) term) list"
    1.40 +
    1.41 +type_synonym ('f, 'l, 'v) rseqL   = "((('f, 'l) lab, 'v) rule \<times> (('f, 'l) lab, 'v) rseq) list"
    1.42 +type_synonym ('f, 'l, 'v) dppLL   =
    1.43 +  "bool \<times> bool \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL \<times>
    1.44 +  ('f, 'l, 'v) termsLL \<times>
    1.45 +  ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL"
    1.46 +
    1.47 +type_synonym ('f, 'l, 'v) qreltrsLL =
    1.48 +  "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL"
    1.49 +
    1.50 +type_synonym ('f, 'l, 'v) qtrsLL =
    1.51 +  "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL"
    1.52 +
    1.53 +datatype_new location = H | A | B | R
    1.54 +
    1.55 +type_synonym ('f,'v)forb_pattern = "('f,'v)ctxt \<times> ('f,'v)term \<times> location"
    1.56 +type_synonym ('f,'v)forb_patterns = "('f,'v)forb_pattern set"
    1.57 +
    1.58 +type_synonym ('f, 'l, 'v) fptrsLL =
    1.59 +  "(('f, 'l)lab, 'v) forb_pattern list \<times> ('f, 'l, 'v) trsLL"
    1.60 +
    1.61 +type_synonym ('f, 'l, 'v) prob = "('f, 'l, 'v) qreltrsLL + ('f, 'l, 'v) dppLL"
    1.62 +
    1.63 +type_synonym ('f, 'a) lpoly_inter = "'f \<times> nat \<Rightarrow> ('a \<times> 'a list)"
    1.64 +type_synonym ('f, 'a) lpoly_interL = "(('f \<times> nat) \<times> ('a \<times> 'a list)) list"
    1.65 +
    1.66 +type_synonym 'v monom = "('v \<times> nat)list" 
    1.67 +type_synonym ('v,'a)poly = "('v monom \<times> 'a)list"
    1.68 +type_synonym ('f,'a)poly_inter_list = "(('f \<times> nat) \<times> (nat,'a)poly)list"
    1.69 +type_synonym 'a vec = "'a list"
    1.70 +type_synonym 'a mat = "'a vec list" 
    1.71 +
    1.72 +
    1.73 +datatype_new arctic = MinInfty | Num_arc int
    1.74 +datatype_new 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
    1.75 +datatype_new order_tag = Lex | Mul
    1.76 +
    1.77 +type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag))list"
    1.78 +datatype_new af_entry = Collapse nat | AFList "nat list"
    1.79 +type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry)list"
    1.80 +type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option)))list \<times> nat"
    1.81 +
    1.82 +
    1.83 +datatype_new 'f redtriple_impl = 
    1.84 +    Int_carrier "('f, int) lpoly_interL" 
    1.85 +  | Int_nl_carrier "('f, int) poly_inter_list" 
    1.86 +  | Rat_carrier "('f, rat) lpoly_interL"
    1.87 +  | Rat_nl_carrier rat "('f, rat) poly_inter_list"
    1.88 +  | Real_carrier "('f, real) lpoly_interL"
    1.89 +  | Real_nl_carrier real "('f, real) poly_inter_list"
    1.90 +  | Arctic_carrier "('f, arctic) lpoly_interL" 
    1.91 +  | Arctic_rat_carrier "('f, rat arctic_delta) lpoly_interL" 
    1.92 +  | Int_mat_carrier nat nat "('f, int mat) lpoly_interL"
    1.93 +  | Rat_mat_carrier nat nat "('f, rat mat) lpoly_interL"
    1.94 +  | Real_mat_carrier nat nat "('f, real mat) lpoly_interL"
    1.95 +  | Arctic_mat_carrier nat "('f, arctic mat) lpoly_interL"
    1.96 +  | Arctic_rat_mat_carrier nat "('f, rat arctic_delta mat) lpoly_interL"
    1.97 +  | RPO "'f status_prec_repr" "'f afs_list"
    1.98 +  | KBO "'f prec_weight_repr" "'f afs_list"
    1.99 +
   1.100 +datatype_new list_order_type = MS_Ext | Max_Ext | Min_Ext  | Dms_Ext 
   1.101 +type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list"
   1.102 +
   1.103 +datatype_new 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
   1.104 +
   1.105 +type_synonym 'f sig_map_list = "(('f \<times> nat) \<times> 'f list) list"
   1.106 +type_synonym ('f,'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f,'v)rules \<times> ('f,'v)rules"
   1.107 +
   1.108 +datatype_new arithFun =
   1.109 +  Arg nat
   1.110 +| Const nat
   1.111 +| Sum "arithFun list"
   1.112 +| Max "arithFun list"
   1.113 +| Min "arithFun list"
   1.114 +| Prod "arithFun list"
   1.115 +| IfEqual arithFun arithFun arithFun arithFun
   1.116 +
   1.117 +datatype_new 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
   1.118 +datatype_new ('f,'v)sl_variant = Rootlab "('f \<times> nat) option" | Finitelab "'f sl_inter" | QuasiFinitelab "'f sl_inter" 'v
   1.119 +
   1.120 +type_synonym ('f,'v)crit_pair_joins = "(('f,'v)term \<times> ('f,'v)rseq \<times> ('f,'v)term \<times> ('f,'v)rseq)list"
   1.121 +datatype_new 'f join_info = Guided "('f,string)crit_pair_joins" | Join_NF | Join_BFS nat
   1.122 +
   1.123 +type_synonym unknown_info = string
   1.124 +
   1.125 +type_synonym dummy_prf = unit
   1.126 +
   1.127 +
   1.128 +datatype_new ('f,'v)complex_constant_removal_prf = Complex_Constant_Removal_Proof 
   1.129 +  "('f,'v)term" 
   1.130 +  "(('f,'v)rule \<times> ('f,'v)rule) list" 
   1.131 +
   1.132 +datatype_new ('f,'v)cond_constraint 
   1.133 +  = CC_cond bool "('f,'v)rule" 
   1.134 +  | CC_rewr "('f,'v)term" "('f,'v)term"
   1.135 +  | CC_impl "('f,'v)cond_constraint list" "('f,'v)cond_constraint"
   1.136 +  | CC_all 'v "('f,'v)cond_constraint"
   1.137 +
   1.138 +type_synonym ('f, 'v, 'w) gsubstL = "('v \<times> ('f, 'w) term) list"
   1.139 +type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL"
   1.140 +
   1.141 +datatype_new ('f,'v)cond_constraint_prf = 
   1.142 +  Final 
   1.143 +| Delete_Condition "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   1.144 +| Different_Constructor "('f,'v)cond_constraint"
   1.145 +| Same_Constructor "('f,'v)cond_constraint" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   1.146 +| Variable_Equation 'v "('f,'v)term" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   1.147 +| Funarg_Into_Var "('f,'v)cond_constraint" nat 'v "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   1.148 +| Simplify_Condition "('f,'v)cond_constraint" "('f,'v)substL" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   1.149 +| 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"
   1.150 +
   1.151 +
   1.152 +datatype_new ('f,'v)cond_red_pair_prf = Cond_Red_Pair_Prf 
   1.153 +  'f 
   1.154 +  "(('f,'v)cond_constraint \<times> ('f,'v)rules \<times> ('f,'v)cond_constraint_prf) list"
   1.155 +  nat 
   1.156 +  nat 
   1.157 +
   1.158 +datatype_new ('q,'f)ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
   1.159 +datatype_new ('q,'f)tree_automaton = Tree_Automaton "'q list" "('q,'f)ta_rule list" "('q \<times> 'q)list"
   1.160 +datatype_new 'q ta_relation = Decision_Proc | Id_Relation | Some_Relation "('q \<times> 'q) list"
   1.161 +
   1.162 +datatype_new boundstype = Roof | Match
   1.163 +datatype_new ('f,'q)bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
   1.164 +
   1.165 +datatype_new ('f, 'v) pat_eqv_prf =
   1.166 +  Pat_Dom_Renaming "('f, 'v) substL"
   1.167 +| Pat_Irrelevant "('f, 'v) substL" "('f, 'v) substL"
   1.168 +| Pat_Simplify "('f, 'v) substL" "('f, 'v) substL"
   1.169 +
   1.170 +datatype_new pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
   1.171 +
   1.172 +datatype_new ('f, 'v) pat_rule_prf = 
   1.173 +  Pat_OrigRule "('f, 'v) rule" bool
   1.174 +| Pat_InitPump "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL"
   1.175 +| Pat_InitPumpCtxt "('f, 'v) pat_rule_prf" "('f, 'v) substL" pos 'v
   1.176 +| Pat_Equiv "('f, 'v) pat_rule_prf" bool "('f, 'v) pat_eqv_prf"
   1.177 +| Pat_Narrow "('f, 'v) pat_rule_prf" "('f, 'v) pat_rule_prf" pos
   1.178 +| Pat_Inst "('f, 'v) pat_rule_prf" "('f, 'v) substL" pat_rule_pos
   1.179 +| Pat_Rewr "('f, 'v) pat_rule_prf" "('f, 'v) term \<times> ('f, 'v) rseq" pat_rule_pos 'v 
   1.180 +| Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat
   1.181 +
   1.182 +datatype_new ('f, 'v) non_loop_prf =
   1.183 +  Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos
   1.184 +
   1.185 +
   1.186 +datatype_new ('f, 'l, 'v) problem = 
   1.187 +  SN_TRS "('f,'l,'v)qreltrsLL"
   1.188 +| SN_FP_TRS "('f,'l,'v)fptrsLL" 
   1.189 +| Finite_DPP "('f,'l,'v) dppLL"
   1.190 +| Unknown_Problem unknown_info
   1.191 +| Not_SN_TRS "('f,'l,'v)qtrsLL" 
   1.192 +| Not_RelSN_TRS "('f,'l,'v)qreltrsLL" 
   1.193 +| Infinite_DPP "('f,'l,'v) dppLL"
   1.194 +| Not_SN_FP_TRS "('f,'l,'v)fptrsLL" 
   1.195 +declare [[bnf_timing]]
   1.196 +datatype_new ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof = 
   1.197 +  SN_assm_proof "('f,'l,'v)qreltrsLL" 'a
   1.198 +| Finite_assm_proof "('f,'l,'v)dppLL" 'b
   1.199 +| SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'c
   1.200 +| Not_SN_assm_proof "('f,'l,'v)qtrsLL" 'a
   1.201 +| Infinite_assm_proof "('f,'l,'v)dppLL" 'b
   1.202 +| Not_RelSN_assm_proof "('f,'l,'v)qreltrsLL" 'c
   1.203 +| Not_SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'd
   1.204 +| Unknown_assm_proof unknown_info 'e
   1.205 +
   1.206 +type_synonym ('f,'l,'v,'a,'b,'c,'d)assm_proof = "('f,'l,'v,'a,'b,'c,dummy_prf,'d)generic_assm_proof"
   1.207 +
   1.208 +datatype_new ('f, 'l, 'v) assm = 
   1.209 +  SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" 
   1.210 +| SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL"
   1.211 +| Finite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL"
   1.212 +| Unknown_assm "('f,'l,'v)problem list" unknown_info
   1.213 +| Not_SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qtrsLL" 
   1.214 +| Not_RelSN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" 
   1.215 +| Not_SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL"
   1.216 +| Infinite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL"
   1.217 +
   1.218 +fun satisfied :: "('f,'l,'v)problem \<Rightarrow> bool" where
   1.219 +  "satisfied (SN_TRS t) = (t = t)"
   1.220 +| "satisfied (SN_FP_TRS t) = (t \<noteq> t)"
   1.221 +| "satisfied (Finite_DPP d) = (d \<noteq> d)"
   1.222 +| "satisfied (Unknown_Problem s) = (s = ''foo'')"
   1.223 +| "satisfied (Not_SN_TRS (nfs,q,r)) = (length q = length r)"
   1.224 +| "satisfied (Not_RelSN_TRS (nfs,q,r,rw)) = (r = rw)"
   1.225 +| "satisfied (Infinite_DPP d) = (d = d)"
   1.226 +| "satisfied (Not_SN_FP_TRS t) = (t = t)"
   1.227 +
   1.228 +fun collect_assms :: "('tp \<Rightarrow> ('f,'l,'v) assm list) 
   1.229 +  \<Rightarrow> ('dpp \<Rightarrow> ('f,'l,'v) assm list)
   1.230 +  \<Rightarrow> ('fptp \<Rightarrow> ('f,'l,'v) assm list)
   1.231 +  \<Rightarrow> ('unk \<Rightarrow> ('f,'l,'v) assm list)
   1.232 +  \<Rightarrow> ('f,'l,'v,'tp,'dpp,'fptp,'unk) assm_proof \<Rightarrow> ('f,'l,'v) assm list" where
   1.233 +  "collect_assms tp dpp fptp unk (SN_assm_proof t prf) = tp prf"
   1.234 +| "collect_assms tp dpp fptp unk (SN_FP_assm_proof t prf) = fptp prf"
   1.235 +| "collect_assms tp dpp fptp unk (Finite_assm_proof d prf) = dpp prf"
   1.236 +| "collect_assms tp dpp fptp unk (Unknown_assm_proof p prf) = unk prf"
   1.237 +| "collect_assms _ _ _ _ _ = []"
   1.238 +
   1.239 +fun collect_neg_assms :: "('tp \<Rightarrow> ('f,'l,'v) assm list) 
   1.240 +  \<Rightarrow> ('dpp \<Rightarrow> ('f,'l,'v) assm list)
   1.241 +  \<Rightarrow> ('rtp \<Rightarrow> ('f,'l,'v) assm list)
   1.242 +  \<Rightarrow> ('fptp \<Rightarrow> ('f,'l,'v) assm list)
   1.243 +  \<Rightarrow> ('unk \<Rightarrow> ('f,'l,'v) assm list) 
   1.244 +  \<Rightarrow> ('f,'l,'v,'tp,'dpp,'rtp,'fptp,'unk) generic_assm_proof \<Rightarrow> ('f,'l,'v) assm list" where
   1.245 +  "collect_neg_assms tp dpp rtp fptp unk (Not_SN_assm_proof t prf) = tp prf"
   1.246 +| "collect_neg_assms tp dpp rtp fptp unk (Infinite_assm_proof d prf) = dpp prf"
   1.247 +| "collect_neg_assms tp dpp rtp fptp unk (Not_RelSN_assm_proof t prf) = rtp prf"
   1.248 +| "collect_neg_assms tp dpp rtp fptp unk (Not_SN_FP_assm_proof t prf) = fptp prf"
   1.249 +| "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf"
   1.250 +| "collect_neg_assms tp dpp rtp fptp unk _ = []"
   1.251 +
   1.252 +
   1.253 +
   1.254 +datatype_new ('f, 'l, 'v) dp_nontermination_proof =
   1.255 +  DP_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   1.256 +| DP_Nonloop "(('f,'l)lab, 'v)non_loop_prf"
   1.257 +| DP_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) dp_nontermination_proof"
   1.258 +| DP_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof"
   1.259 +| DP_Q_Reduction "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof"
   1.260 +| DP_Termination_Switch "('f,'l)lab join_info" "('f,'l,'v) dp_nontermination_proof"
   1.261 +| DP_Instantiation "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof"
   1.262 +| 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"
   1.263 +| DP_Narrowing "('f,'l,'v)ruleLL" pos "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof"
   1.264 +| DP_Assume_Infinite  "('f, 'l, 'v) dppLL" 
   1.265 +    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   1.266 +     ('f, 'l, 'v) dp_nontermination_proof, 
   1.267 +     ('f, 'l, 'v) reltrs_nontermination_proof, 
   1.268 +     ('f, 'l, 'v) fp_nontermination_proof,
   1.269 +     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   1.270 + and
   1.271 +('f,'l,'v) "trs_nontermination_proof" = 
   1.272 +  TRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   1.273 +| TRS_Not_Well_Formed
   1.274 +| TRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) trs_nontermination_proof"
   1.275 +| TRS_String_Reversal "('f,'l,'v) trs_nontermination_proof"
   1.276 +| TRS_DP_Trans "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof"
   1.277 +| TRS_Nonloop "(('f,'l)lab,'v) non_loop_prf"
   1.278 +| TRS_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) trs_nontermination_proof"
   1.279 +| TRS_Assume_Not_SN  "('f, 'l, 'v)qtrsLL" 
   1.280 +    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   1.281 +     ('f, 'l, 'v) dp_nontermination_proof, 
   1.282 +     ('f, 'l, 'v) reltrs_nontermination_proof, 
   1.283 +     ('f, 'l, 'v) fp_nontermination_proof,
   1.284 +     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   1.285 + and
   1.286 +('f,'l,'v)"reltrs_nontermination_proof" = 
   1.287 +  Rel_Loop "(('f,'l)lab,'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   1.288 +| Rel_Not_Well_Formed
   1.289 +| Rel_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) reltrs_nontermination_proof"
   1.290 +| Rel_R_Not_SN "('f,'l,'v) trs_nontermination_proof"
   1.291 +| Rel_TRS_Assume_Not_SN  "('f, 'l, 'v)qreltrsLL" 
   1.292 +    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   1.293 +     ('f, 'l, 'v) dp_nontermination_proof, 
   1.294 +     ('f, 'l, 'v) reltrs_nontermination_proof, 
   1.295 +     ('f, 'l, 'v) fp_nontermination_proof,
   1.296 +     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   1.297 + and
   1.298 + ('f, 'l, 'v) "fp_nontermination_proof" = 
   1.299 +  FPTRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   1.300 +| FPTRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) fp_nontermination_proof" 
   1.301 +| FPTRS_Assume_Not_SN  "('f, 'l, 'v)fptrsLL" 
   1.302 +    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   1.303 +     ('f, 'l, 'v) dp_nontermination_proof, 
   1.304 +     ('f, 'l, 'v) reltrs_nontermination_proof, 
   1.305 +     ('f, 'l, 'v) fp_nontermination_proof,
   1.306 +     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   1.307 + and
   1.308 + ('f, 'l, 'v) neg_unknown_proof =
   1.309 +  Assume_NT_Unknown unknown_info 
   1.310 +    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   1.311 +     ('f, 'l, 'v) dp_nontermination_proof, 
   1.312 +     ('f, 'l, 'v) reltrs_nontermination_proof, 
   1.313 +     ('f, 'l, 'v) fp_nontermination_proof,
   1.314 +     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   1.315 +
   1.316 +
   1.317 +datatype_new ('f, 'l, 'v) dp_termination_proof =
   1.318 +  P_is_Empty
   1.319 +| Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL"
   1.320 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   1.321 +| Redpair_Proc "('f,'l)lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL"  "('f, 'l, 'v) dp_termination_proof"
   1.322 +| Redpair_UR_Proc "('f, 'l) lab root_redtriple_impl + ('f, 'l) lab redtriple_impl"
   1.323 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" 
   1.324 +| Usable_Rules_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" 
   1.325 +| Dep_Graph_Proc "(('f, 'l, 'v) dp_termination_proof option \<times> ('f, 'l, 'v) trsLL) list"
   1.326 +| Mono_Redpair_Proc "('f, 'l) lab redtriple_impl"
   1.327 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" 
   1.328 +| Mono_Redpair_UR_Proc "('f, 'l) lab redtriple_impl"
   1.329 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   1.330 +| Size_Change_Subterm_Proc "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
   1.331 +| Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option"
   1.332 +    "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
   1.333 +| Uncurry_Proc "nat option" "(('f, 'l) lab, 'v) uncurry_info"
   1.334 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   1.335 +| Fcc_Proc "('f, 'l) lab" "(('f, 'l) lab, 'v) ctxt list"
   1.336 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   1.337 +| Split_Proc
   1.338 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" 
   1.339 +    "('f, 'l, 'v) dp_termination_proof" "('f, 'l, 'v) dp_termination_proof"
   1.340 +| Semlab_Proc
   1.341 +    "(('f, 'l) lab, 'v) sl_variant" "('f, 'l, 'v) trsLL"
   1.342 +    "(('f, 'l) lab, 'v) term list" "('f, 'l, 'v) trsLL"
   1.343 +    "('f, 'l, 'v) dp_termination_proof"
   1.344 +| Switch_Innermost_Proc "('f, 'l) lab join_info" "('f, 'l, 'v) dp_termination_proof"
   1.345 +| Rewriting_Proc
   1.346 +    "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL"
   1.347 +    "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) dp_termination_proof"
   1.348 +| Instantiation_Proc "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   1.349 +| Forward_Instantiation_Proc
   1.350 +    "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_termination_proof"
   1.351 +| Narrowing_Proc "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   1.352 +| Assume_Finite
   1.353 +    "('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"
   1.354 +| Unlab_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   1.355 +| Q_Reduction_Proc "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_termination_proof"
   1.356 +| Complex_Constant_Removal_Proc "(('f,'l)lab,'v)complex_constant_removal_prf" "('f, 'l, 'v) dp_termination_proof"
   1.357 +| General_Redpair_Proc
   1.358 +    "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL"
   1.359 +    "(('f, 'l) lab, 'v) cond_red_pair_prf" "('f, 'l, 'v) dp_termination_proof list" 
   1.360 +| To_Trs_Proc "('f, 'l, 'v) trs_termination_proof"
   1.361 +and ('f, 'l, 'v) trs_termination_proof =
   1.362 +  DP_Trans bool bool "(('f, 'l) lab, 'v) rules" "('f, 'l, 'v) dp_termination_proof"
   1.363 +| Rule_Removal "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v)trs_termination_proof"
   1.364 +| String_Reversal "('f, 'l, 'v) trs_termination_proof"
   1.365 +| Bounds "(('f, 'l) lab, 'v) bounds_info"
   1.366 +| Uncurry "(('f, 'l) lab, 'v) uncurry_info" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   1.367 +| Semlab
   1.368 +    "(('f, 'l) lab, 'v) sl_variant" "(('f, 'l) lab, 'v) term list"
   1.369 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   1.370 +| R_is_Empty
   1.371 +| Fcc "(('f, 'l) lab, 'v) ctxt list" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   1.372 +| Split "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" "('f, 'l, 'v) trs_termination_proof"
   1.373 +| Switch_Innermost "('f, 'l) lab join_info" "('f, 'l, 'v) trs_termination_proof" 
   1.374 +| Drop_Equality "('f, 'l, 'v) trs_termination_proof"
   1.375 +| Remove_Nonapplicable_Rules "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   1.376 +| 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"
   1.377 +and ('f, 'l, 'v) unknown_proof =
   1.378 +  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"
   1.379 +and ('f, 'l, 'v) fptrs_termination_proof =
   1.380 +  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"
   1.381 +
   1.382 +
   1.383 +end
     2.1 --- a/src/HOL/ROOT	Mon Jul 21 15:23:57 2014 +0200
     2.2 +++ b/src/HOL/ROOT	Mon Jul 21 18:04:08 2014 +0200
     2.3 @@ -734,6 +734,8 @@
     2.4      Misc_Datatype
     2.5      Misc_Primcorec
     2.6      Misc_Primrec
     2.7 +  theories [condition = ISABELLE_FULL_TEST]
     2.8 +    IsaFoR_Datatypes
     2.9  
    2.10  session "HOL-Word" (main) in Word = HOL +
    2.11    options [document_graph]