tuning
authorblanchet
Thu Jul 24 00:24:00 2014 +0200 (2014-07-24)
changeset 57634efc00b9b8680
parent 57633 4ff8c090d580
child 57635 97adb86619a4
tuning
src/HOL/BNF_Examples/Compat.thy
src/HOL/BNF_Examples/IsaFoR_Datatypes.thy
src/HOL/BNF_Examples/Koenig.thy
src/HOL/BNF_Examples/Stream_Processor.thy
     1.1 --- a/src/HOL/BNF_Examples/Compat.thy	Thu Jul 24 00:24:00 2014 +0200
     1.2 +++ b/src/HOL/BNF_Examples/Compat.thy	Thu Jul 24 00:24:00 2014 +0200
     1.3 @@ -1,3 +1,12 @@
     1.4 +(*  Title:      HOL/BNF_Examples/Compat.thy
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +    Copyright   2014
     1.7 +
     1.8 +Tests for compatibility with the old datatype package.
     1.9 +*)
    1.10 +
    1.11 +header {* Tests for Compatibility with the Old Datatype Package *}
    1.12 +
    1.13  theory Compat
    1.14  imports Main
    1.15  begin
     2.1 --- a/src/HOL/BNF_Examples/IsaFoR_Datatypes.thy	Thu Jul 24 00:24:00 2014 +0200
     2.2 +++ b/src/HOL/BNF_Examples/IsaFoR_Datatypes.thy	Thu Jul 24 00:24:00 2014 +0200
     2.3 @@ -1,37 +1,39 @@
     2.4  (*  Title:      HOL/BNF_Examples/IsaFoR_Datatypes.thy
     2.5 -    Author:     René Thiemann
     2.6 +    Author:     Rene Thiemann, UIBK
     2.7      Copyright   2014
     2.8  
     2.9 -Benchmark of datatypes defined in IsaFoR
    2.10 +Benchmark consisting of datatypes defined in IsaFoR.
    2.11  *)
    2.12  
    2.13 +header {* Benchmark Consisting of Datatypes Defined in IsaFoR *}
    2.14 +
    2.15  theory IsaFoR_Datatypes
    2.16 -imports
    2.17 -  Real
    2.18 +imports Real
    2.19  begin
    2.20  
    2.21  datatype_new ('f, 'l) lab =
    2.22 -  Lab "('f, 'l) lab" 'l
    2.23 -| FunLab "('f, 'l) lab" "('f, 'l) lab list"
    2.24 -| UnLab 'f
    2.25 -| Sharp "('f, 'l) lab"
    2.26 +    Lab "('f, 'l) lab" 'l
    2.27 +  | FunLab "('f, 'l) lab" "('f, 'l) lab list"
    2.28 +  | UnLab 'f
    2.29 +  | Sharp "('f, 'l) lab"
    2.30  
    2.31  datatype_new 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
    2.32  
    2.33  datatype_new ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
    2.34  datatype_new ('f, 'v) ctxt =
    2.35 -  Hole ("\<box>")
    2.36 -| More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
    2.37 -
    2.38 +    Hole ("\<box>")
    2.39 +  | More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
    2.40  
    2.41  type_synonym ('f, 'v) rule = "('f, 'v) term \<times> ('f, 'v) term"
    2.42  type_synonym ('f, 'v) trs  = "('f, 'v) rule set"
    2.43  
    2.44 -type_synonym ('f, 'v) rules = "('f,'v) rule list"
    2.45 +type_synonym ('f, 'v) rules = "('f, 'v) rule list"
    2.46  type_synonym ('f, 'l, 'v) ruleLL  = "(('f, 'l) lab, 'v) rule"
    2.47  type_synonym ('f, 'l, 'v) trsLL   = "(('f, 'l) lab, 'v) rules"
    2.48  type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list"
    2.49 +
    2.50  datatype_new pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
    2.51 +
    2.52  type_synonym  ('f, 'v) prseq = "(pos \<times> ('f, 'v) rule \<times> bool \<times> ('f, 'v) term) list"
    2.53  type_synonym  ('f, 'v) rseq = "(pos \<times> ('f, 'v) rule \<times> ('f, 'v) term) list"
    2.54  
    2.55 @@ -49,43 +51,45 @@
    2.56  
    2.57  datatype_new location = H | A | B | R
    2.58  
    2.59 -type_synonym ('f,'v)forb_pattern = "('f,'v)ctxt \<times> ('f,'v)term \<times> location"
    2.60 -type_synonym ('f,'v)forb_patterns = "('f,'v)forb_pattern set"
    2.61 +type_synonym ('f, 'v) forb_pattern = "('f, 'v) ctxt \<times> ('f, 'v) term \<times> location"
    2.62 +type_synonym ('f, 'v) forb_patterns = "('f, 'v) forb_pattern set"
    2.63  
    2.64  type_synonym ('f, 'l, 'v) fptrsLL =
    2.65 -  "(('f, 'l)lab, 'v) forb_pattern list \<times> ('f, 'l, 'v) trsLL"
    2.66 +  "(('f, 'l) lab, 'v) forb_pattern list \<times> ('f, 'l, 'v) trsLL"
    2.67  
    2.68  type_synonym ('f, 'l, 'v) prob = "('f, 'l, 'v) qreltrsLL + ('f, 'l, 'v) dppLL"
    2.69  
    2.70  type_synonym ('f, 'a) lpoly_inter = "'f \<times> nat \<Rightarrow> ('a \<times> 'a list)"
    2.71  type_synonym ('f, 'a) lpoly_interL = "(('f \<times> nat) \<times> ('a \<times> 'a list)) list"
    2.72  
    2.73 -type_synonym 'v monom = "('v \<times> nat)list" 
    2.74 -type_synonym ('v,'a)poly = "('v monom \<times> 'a)list"
    2.75 -type_synonym ('f,'a)poly_inter_list = "(('f \<times> nat) \<times> (nat,'a)poly)list"
    2.76 +type_synonym 'v monom = "('v \<times> nat) list"
    2.77 +type_synonym ('v, 'a) poly = "('v monom \<times> 'a) list"
    2.78 +type_synonym ('f, 'a) poly_inter_list = "(('f \<times> nat) \<times> (nat, 'a) poly) list"
    2.79  type_synonym 'a vec = "'a list"
    2.80 -type_synonym 'a mat = "'a vec list" 
    2.81 -
    2.82 +type_synonym 'a mat = "'a vec list"
    2.83  
    2.84  datatype_new arctic = MinInfty | Num_arc int
    2.85  datatype_new 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
    2.86  datatype_new order_tag = Lex | Mul
    2.87  
    2.88 -type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag))list"
    2.89 -datatype_new af_entry = Collapse nat | AFList "nat list"
    2.90 -type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry)list"
    2.91 -type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option)))list \<times> nat"
    2.92 +type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag)) list"
    2.93 +
    2.94 +datatype_new af_entry =
    2.95 +    Collapse nat
    2.96 +  | AFList "nat list"
    2.97  
    2.98 +type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry) list"
    2.99 +type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option))) list \<times> nat"
   2.100  
   2.101 -datatype_new 'f redtriple_impl = 
   2.102 -    Int_carrier "('f, int) lpoly_interL" 
   2.103 -  | Int_nl_carrier "('f, int) poly_inter_list" 
   2.104 +datatype_new 'f redtriple_impl =
   2.105 +    Int_carrier "('f, int) lpoly_interL"
   2.106 +  | Int_nl_carrier "('f, int) poly_inter_list"
   2.107    | Rat_carrier "('f, rat) lpoly_interL"
   2.108    | Rat_nl_carrier rat "('f, rat) poly_inter_list"
   2.109    | Real_carrier "('f, real) lpoly_interL"
   2.110    | Real_nl_carrier real "('f, real) poly_inter_list"
   2.111 -  | Arctic_carrier "('f, arctic) lpoly_interL" 
   2.112 -  | Arctic_rat_carrier "('f, rat arctic_delta) lpoly_interL" 
   2.113 +  | Arctic_carrier "('f, arctic) lpoly_interL"
   2.114 +  | Arctic_rat_carrier "('f, rat arctic_delta) lpoly_interL"
   2.115    | Int_mat_carrier nat nat "('f, int mat) lpoly_interL"
   2.116    | Rat_mat_carrier nat nat "('f, rat mat) lpoly_interL"
   2.117    | Real_mat_carrier nat nat "('f, real mat) lpoly_interL"
   2.118 @@ -94,151 +98,155 @@
   2.119    | RPO "'f status_prec_repr" "'f afs_list"
   2.120    | KBO "'f prec_weight_repr" "'f afs_list"
   2.121  
   2.122 -datatype_new list_order_type = MS_Ext | Max_Ext | Min_Ext  | Dms_Ext 
   2.123 +datatype_new list_order_type = MS_Ext | Max_Ext | Min_Ext  | Dms_Ext
   2.124  type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list"
   2.125  
   2.126  datatype_new 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
   2.127  
   2.128  type_synonym 'f sig_map_list = "(('f \<times> nat) \<times> 'f list) list"
   2.129 -type_synonym ('f,'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f,'v)rules \<times> ('f,'v)rules"
   2.130 +type_synonym ('f, 'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f, 'v) rules \<times> ('f, 'v) rules"
   2.131  
   2.132  datatype_new arithFun =
   2.133 -  Arg nat
   2.134 -| Const nat
   2.135 -| Sum "arithFun list"
   2.136 -| Max "arithFun list"
   2.137 -| Min "arithFun list"
   2.138 -| Prod "arithFun list"
   2.139 -| IfEqual arithFun arithFun arithFun arithFun
   2.140 +    Arg nat
   2.141 +  | Const nat
   2.142 +  | Sum "arithFun list"
   2.143 +  | Max "arithFun list"
   2.144 +  | Min "arithFun list"
   2.145 +  | Prod "arithFun list"
   2.146 +  | IfEqual arithFun arithFun arithFun arithFun
   2.147  
   2.148  datatype_new 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
   2.149 -datatype_new ('f,'v)sl_variant = Rootlab "('f \<times> nat) option" | Finitelab "'f sl_inter" | QuasiFinitelab "'f sl_inter" 'v
   2.150 +datatype_new ('f, 'v) sl_variant =
   2.151 +    Rootlab "('f \<times> nat) option"
   2.152 +  | Finitelab "'f sl_inter"
   2.153 +  | QuasiFinitelab "'f sl_inter" 'v
   2.154  
   2.155 -type_synonym ('f,'v)crit_pair_joins = "(('f,'v)term \<times> ('f,'v)rseq \<times> ('f,'v)term \<times> ('f,'v)rseq)list"
   2.156 -datatype_new 'f join_info = Guided "('f,string)crit_pair_joins" | Join_NF | Join_BFS nat
   2.157 +type_synonym ('f, 'v) crit_pair_joins = "(('f, 'v) term \<times> ('f, 'v) rseq \<times> ('f, 'v) term \<times> ('f, 'v) rseq) list"
   2.158 +
   2.159 +datatype_new 'f join_info = Guided "('f, string) crit_pair_joins" | Join_NF | Join_BFS nat
   2.160  
   2.161  type_synonym unknown_info = string
   2.162  
   2.163  type_synonym dummy_prf = unit
   2.164  
   2.165 -
   2.166 -datatype_new ('f,'v)complex_constant_removal_prf = Complex_Constant_Removal_Proof 
   2.167 -  "('f,'v)term" 
   2.168 -  "(('f,'v)rule \<times> ('f,'v)rule) list" 
   2.169 +datatype_new ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
   2.170 +  "('f, 'v) term"
   2.171 +  "(('f, 'v) rule \<times> ('f, 'v) rule) list"
   2.172  
   2.173 -datatype_new ('f,'v)cond_constraint 
   2.174 -  = CC_cond bool "('f,'v)rule" 
   2.175 -  | CC_rewr "('f,'v)term" "('f,'v)term"
   2.176 -  | CC_impl "('f,'v)cond_constraint list" "('f,'v)cond_constraint"
   2.177 -  | CC_all 'v "('f,'v)cond_constraint"
   2.178 +datatype_new ('f, 'v) cond_constraint =
   2.179 +    CC_cond bool "('f, 'v) rule"
   2.180 +  | CC_rewr "('f, 'v) term" "('f, 'v) term"
   2.181 +  | CC_impl "('f, 'v) cond_constraint list" "('f, 'v) cond_constraint"
   2.182 +  | CC_all 'v "('f, 'v) cond_constraint"
   2.183  
   2.184  type_synonym ('f, 'v, 'w) gsubstL = "('v \<times> ('f, 'w) term) list"
   2.185  type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL"
   2.186  
   2.187 -datatype_new ('f,'v)cond_constraint_prf = 
   2.188 -  Final 
   2.189 -| Delete_Condition "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   2.190 -| Different_Constructor "('f,'v)cond_constraint"
   2.191 -| Same_Constructor "('f,'v)cond_constraint" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   2.192 -| Variable_Equation 'v "('f,'v)term" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   2.193 -| Funarg_Into_Var "('f,'v)cond_constraint" nat 'v "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   2.194 -| Simplify_Condition "('f,'v)cond_constraint" "('f,'v)substL" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   2.195 -| 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"
   2.196 +datatype_new ('f, 'v) cond_constraint_prf =
   2.197 +    Final
   2.198 +  | Delete_Condition "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   2.199 +  | Different_Constructor "('f, 'v) cond_constraint"
   2.200 +  | Same_Constructor "('f, 'v) cond_constraint" "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   2.201 +  | Variable_Equation 'v "('f, 'v) term" "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   2.202 +  | Funarg_Into_Var "('f, 'v) cond_constraint" nat 'v "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   2.203 +  | Simplify_Condition "('f, 'v) cond_constraint" "('f, 'v) substL" "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   2.204 +  | 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"
   2.205  
   2.206 +datatype_new ('f, 'v) cond_red_pair_prf =
   2.207 +  Cond_Red_Pair_Prf
   2.208 +    'f "(('f, 'v) cond_constraint \<times> ('f, 'v) rules \<times> ('f, 'v) cond_constraint_prf) list" nat nat
   2.209  
   2.210 -datatype_new ('f,'v)cond_red_pair_prf = Cond_Red_Pair_Prf 
   2.211 -  'f 
   2.212 -  "(('f,'v)cond_constraint \<times> ('f,'v)rules \<times> ('f,'v)cond_constraint_prf) list"
   2.213 -  nat 
   2.214 -  nat 
   2.215 -
   2.216 -datatype_new ('q,'f)ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
   2.217 -datatype_new ('q,'f)tree_automaton = Tree_Automaton "'q list" "('q,'f)ta_rule list" "('q \<times> 'q)list"
   2.218 -datatype_new 'q ta_relation = Decision_Proc | Id_Relation | Some_Relation "('q \<times> 'q) list"
   2.219 +datatype_new ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
   2.220 +datatype_new ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \<times> 'q) list"
   2.221 +datatype_new 'q ta_relation =
   2.222 +    Decision_Proc
   2.223 +  | Id_Relation
   2.224 +  | Some_Relation "('q \<times> 'q) list"
   2.225  
   2.226  datatype_new boundstype = Roof | Match
   2.227 -datatype_new ('f,'q)bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
   2.228 +datatype_new ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
   2.229  
   2.230  datatype_new ('f, 'v) pat_eqv_prf =
   2.231 -  Pat_Dom_Renaming "('f, 'v) substL"
   2.232 -| Pat_Irrelevant "('f, 'v) substL" "('f, 'v) substL"
   2.233 -| Pat_Simplify "('f, 'v) substL" "('f, 'v) substL"
   2.234 +    Pat_Dom_Renaming "('f, 'v) substL"
   2.235 +  | Pat_Irrelevant "('f, 'v) substL" "('f, 'v) substL"
   2.236 +  | Pat_Simplify "('f, 'v) substL" "('f, 'v) substL"
   2.237  
   2.238  datatype_new pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
   2.239  
   2.240 -datatype_new ('f, 'v) pat_rule_prf = 
   2.241 -  Pat_OrigRule "('f, 'v) rule" bool
   2.242 -| Pat_InitPump "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL"
   2.243 -| Pat_InitPumpCtxt "('f, 'v) pat_rule_prf" "('f, 'v) substL" pos 'v
   2.244 -| Pat_Equiv "('f, 'v) pat_rule_prf" bool "('f, 'v) pat_eqv_prf"
   2.245 -| Pat_Narrow "('f, 'v) pat_rule_prf" "('f, 'v) pat_rule_prf" pos
   2.246 -| Pat_Inst "('f, 'v) pat_rule_prf" "('f, 'v) substL" pat_rule_pos
   2.247 -| Pat_Rewr "('f, 'v) pat_rule_prf" "('f, 'v) term \<times> ('f, 'v) rseq" pat_rule_pos 'v 
   2.248 -| Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat
   2.249 +datatype_new ('f, 'v) pat_rule_prf =
   2.250 +    Pat_OrigRule "('f, 'v) rule" bool
   2.251 +  | Pat_InitPump "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL"
   2.252 +  | Pat_InitPumpCtxt "('f, 'v) pat_rule_prf" "('f, 'v) substL" pos 'v
   2.253 +  | Pat_Equiv "('f, 'v) pat_rule_prf" bool "('f, 'v) pat_eqv_prf"
   2.254 +  | Pat_Narrow "('f, 'v) pat_rule_prf" "('f, 'v) pat_rule_prf" pos
   2.255 +  | Pat_Inst "('f, 'v) pat_rule_prf" "('f, 'v) substL" pat_rule_pos
   2.256 +  | Pat_Rewr "('f, 'v) pat_rule_prf" "('f, 'v) term \<times> ('f, 'v) rseq" pat_rule_pos 'v
   2.257 +  | Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat
   2.258  
   2.259  datatype_new ('f, 'v) non_loop_prf =
   2.260 -  Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos
   2.261 -
   2.262 +    Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos
   2.263  
   2.264 -datatype_new ('f, 'l, 'v) problem = 
   2.265 -  SN_TRS "('f,'l,'v)qreltrsLL"
   2.266 -| SN_FP_TRS "('f,'l,'v)fptrsLL" 
   2.267 -| Finite_DPP "('f,'l,'v) dppLL"
   2.268 -| Unknown_Problem unknown_info
   2.269 -| Not_SN_TRS "('f,'l,'v)qtrsLL" 
   2.270 -| Not_RelSN_TRS "('f,'l,'v)qreltrsLL" 
   2.271 -| Infinite_DPP "('f,'l,'v) dppLL"
   2.272 -| Not_SN_FP_TRS "('f,'l,'v)fptrsLL" 
   2.273 +datatype_new ('f, 'l, 'v) problem =
   2.274 +    SN_TRS "('f, 'l, 'v) qreltrsLL"
   2.275 +  | SN_FP_TRS "('f, 'l, 'v) fptrsLL"
   2.276 +  | Finite_DPP "('f, 'l, 'v) dppLL"
   2.277 +  | Unknown_Problem unknown_info
   2.278 +  | Not_SN_TRS "('f, 'l, 'v) qtrsLL"
   2.279 +  | Not_RelSN_TRS "('f, 'l, 'v) qreltrsLL"
   2.280 +  | Infinite_DPP "('f, 'l, 'v) dppLL"
   2.281 +  | Not_SN_FP_TRS "('f, 'l, 'v) fptrsLL"
   2.282 +
   2.283  declare [[bnf_timing]]
   2.284 -datatype_new ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof = 
   2.285 -  SN_assm_proof "('f,'l,'v)qreltrsLL" 'a
   2.286 -| Finite_assm_proof "('f,'l,'v)dppLL" 'b
   2.287 -| SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'c
   2.288 -| Not_SN_assm_proof "('f,'l,'v)qtrsLL" 'a
   2.289 -| Infinite_assm_proof "('f,'l,'v)dppLL" 'b
   2.290 -| Not_RelSN_assm_proof "('f,'l,'v)qreltrsLL" 'c
   2.291 -| Not_SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'd
   2.292 -| Unknown_assm_proof unknown_info 'e
   2.293  
   2.294 -type_synonym ('f,'l,'v,'a,'b,'c,'d)assm_proof = "('f,'l,'v,'a,'b,'c,dummy_prf,'d)generic_assm_proof"
   2.295 +datatype_new ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof =
   2.296 +    SN_assm_proof "('f, 'l, 'v) qreltrsLL" 'a
   2.297 +  | Finite_assm_proof "('f, 'l, 'v) dppLL" 'b
   2.298 +  | SN_FP_assm_proof "('f, 'l, 'v) fptrsLL" 'c
   2.299 +  | Not_SN_assm_proof "('f, 'l, 'v) qtrsLL" 'a
   2.300 +  | Infinite_assm_proof "('f, 'l, 'v) dppLL" 'b
   2.301 +  | Not_RelSN_assm_proof "('f, 'l, 'v) qreltrsLL" 'c
   2.302 +  | Not_SN_FP_assm_proof "('f, 'l, 'v) fptrsLL" 'd
   2.303 +  | Unknown_assm_proof unknown_info 'e
   2.304  
   2.305 -datatype_new ('f, 'l, 'v) assm = 
   2.306 -  SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" 
   2.307 -| SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL"
   2.308 -| Finite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL"
   2.309 -| Unknown_assm "('f,'l,'v)problem list" unknown_info
   2.310 -| Not_SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qtrsLL" 
   2.311 -| Not_RelSN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" 
   2.312 -| Not_SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL"
   2.313 -| Infinite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL"
   2.314 +type_synonym ('f, 'l, 'v, 'a, 'b, 'c, 'd) assm_proof = "('f, 'l, 'v, 'a, 'b, 'c, dummy_prf, 'd) generic_assm_proof"
   2.315  
   2.316 -fun satisfied :: "('f,'l,'v)problem \<Rightarrow> bool" where
   2.317 +datatype_new ('f, 'l, 'v) assm =
   2.318 +    SN_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) qreltrsLL"
   2.319 +  | SN_FP_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) fptrsLL"
   2.320 +  | Finite_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) dppLL"
   2.321 +  | Unknown_assm "('f, 'l, 'v) problem list" unknown_info
   2.322 +  | Not_SN_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) qtrsLL"
   2.323 +  | Not_RelSN_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) qreltrsLL"
   2.324 +  | Not_SN_FP_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) fptrsLL"
   2.325 +  | Infinite_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) dppLL"
   2.326 +
   2.327 +fun satisfied :: "('f, 'l, 'v) problem \<Rightarrow> bool" where
   2.328    "satisfied (SN_TRS t) = (t = t)"
   2.329  | "satisfied (SN_FP_TRS t) = (t \<noteq> t)"
   2.330  | "satisfied (Finite_DPP d) = (d \<noteq> d)"
   2.331  | "satisfied (Unknown_Problem s) = (s = ''foo'')"
   2.332 -| "satisfied (Not_SN_TRS (nfs,q,r)) = (length q = length r)"
   2.333 -| "satisfied (Not_RelSN_TRS (nfs,q,r,rw)) = (r = rw)"
   2.334 +| "satisfied (Not_SN_TRS (nfs, q, r)) = (length q = length r)"
   2.335 +| "satisfied (Not_RelSN_TRS (nfs, q, r, rw)) = (r = rw)"
   2.336  | "satisfied (Infinite_DPP d) = (d = d)"
   2.337  | "satisfied (Not_SN_FP_TRS t) = (t = t)"
   2.338  
   2.339 -fun collect_assms :: "('tp \<Rightarrow> ('f,'l,'v) assm list) 
   2.340 -  \<Rightarrow> ('dpp \<Rightarrow> ('f,'l,'v) assm list)
   2.341 -  \<Rightarrow> ('fptp \<Rightarrow> ('f,'l,'v) assm list)
   2.342 -  \<Rightarrow> ('unk \<Rightarrow> ('f,'l,'v) assm list)
   2.343 -  \<Rightarrow> ('f,'l,'v,'tp,'dpp,'fptp,'unk) assm_proof \<Rightarrow> ('f,'l,'v) assm list" where
   2.344 +fun collect_assms :: "('tp \<Rightarrow> ('f, 'l, 'v) assm list)
   2.345 +  \<Rightarrow> ('dpp \<Rightarrow> ('f, 'l, 'v) assm list)
   2.346 +  \<Rightarrow> ('fptp \<Rightarrow> ('f, 'l, 'v) assm list)
   2.347 +  \<Rightarrow> ('unk \<Rightarrow> ('f, 'l, 'v) assm list)
   2.348 +  \<Rightarrow> ('f, 'l, 'v, 'tp, 'dpp, 'fptp, 'unk) assm_proof \<Rightarrow> ('f, 'l, 'v) assm list" where
   2.349    "collect_assms tp dpp fptp unk (SN_assm_proof t prf) = tp prf"
   2.350  | "collect_assms tp dpp fptp unk (SN_FP_assm_proof t prf) = fptp prf"
   2.351  | "collect_assms tp dpp fptp unk (Finite_assm_proof d prf) = dpp prf"
   2.352  | "collect_assms tp dpp fptp unk (Unknown_assm_proof p prf) = unk prf"
   2.353  | "collect_assms _ _ _ _ _ = []"
   2.354  
   2.355 -fun collect_neg_assms :: "('tp \<Rightarrow> ('f,'l,'v) assm list) 
   2.356 -  \<Rightarrow> ('dpp \<Rightarrow> ('f,'l,'v) assm list)
   2.357 -  \<Rightarrow> ('rtp \<Rightarrow> ('f,'l,'v) assm list)
   2.358 -  \<Rightarrow> ('fptp \<Rightarrow> ('f,'l,'v) assm list)
   2.359 -  \<Rightarrow> ('unk \<Rightarrow> ('f,'l,'v) assm list) 
   2.360 -  \<Rightarrow> ('f,'l,'v,'tp,'dpp,'rtp,'fptp,'unk) generic_assm_proof \<Rightarrow> ('f,'l,'v) assm list" where
   2.361 +fun collect_neg_assms :: "('tp \<Rightarrow> ('f, 'l, 'v) assm list)
   2.362 +  \<Rightarrow> ('dpp \<Rightarrow> ('f, 'l, 'v) assm list)
   2.363 +  \<Rightarrow> ('rtp \<Rightarrow> ('f, 'l, 'v) assm list)
   2.364 +  \<Rightarrow> ('fptp \<Rightarrow> ('f, 'l, 'v) assm list)
   2.365 +  \<Rightarrow> ('unk \<Rightarrow> ('f, 'l, 'v) assm list)
   2.366 +  \<Rightarrow> ('f, 'l, 'v, 'tp, 'dpp, 'rtp, 'fptp, 'unk) generic_assm_proof \<Rightarrow> ('f, 'l, 'v) assm list" where
   2.367    "collect_neg_assms tp dpp rtp fptp unk (Not_SN_assm_proof t prf) = tp prf"
   2.368  | "collect_neg_assms tp dpp rtp fptp unk (Infinite_assm_proof d prf) = dpp prf"
   2.369  | "collect_neg_assms tp dpp rtp fptp unk (Not_RelSN_assm_proof t prf) = rtp prf"
   2.370 @@ -246,135 +254,127 @@
   2.371  | "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf"
   2.372  | "collect_neg_assms tp dpp rtp fptp unk _ = []"
   2.373  
   2.374 -
   2.375 -
   2.376  datatype_new ('f, 'l, 'v) dp_nontermination_proof =
   2.377 -  DP_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   2.378 -| DP_Nonloop "(('f,'l)lab, 'v)non_loop_prf"
   2.379 -| DP_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) dp_nontermination_proof"
   2.380 -| DP_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof"
   2.381 -| DP_Q_Reduction "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof"
   2.382 -| DP_Termination_Switch "('f,'l)lab join_info" "('f,'l,'v) dp_nontermination_proof"
   2.383 -| DP_Instantiation "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof"
   2.384 -| 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"
   2.385 -| DP_Narrowing "('f,'l,'v)ruleLL" pos "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof"
   2.386 -| DP_Assume_Infinite  "('f, 'l, 'v) dppLL" 
   2.387 -    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   2.388 -     ('f, 'l, 'v) dp_nontermination_proof, 
   2.389 -     ('f, 'l, 'v) reltrs_nontermination_proof, 
   2.390 -     ('f, 'l, 'v) fp_nontermination_proof,
   2.391 -     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   2.392 - and
   2.393 -('f,'l,'v) "trs_nontermination_proof" = 
   2.394 -  TRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   2.395 -| TRS_Not_Well_Formed
   2.396 -| TRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) trs_nontermination_proof"
   2.397 -| TRS_String_Reversal "('f,'l,'v) trs_nontermination_proof"
   2.398 -| TRS_DP_Trans "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof"
   2.399 -| TRS_Nonloop "(('f,'l)lab,'v) non_loop_prf"
   2.400 -| TRS_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) trs_nontermination_proof"
   2.401 -| TRS_Assume_Not_SN  "('f, 'l, 'v)qtrsLL" 
   2.402 -    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   2.403 -     ('f, 'l, 'v) dp_nontermination_proof, 
   2.404 -     ('f, 'l, 'v) reltrs_nontermination_proof, 
   2.405 -     ('f, 'l, 'v) fp_nontermination_proof,
   2.406 -     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   2.407 - and
   2.408 -('f,'l,'v)"reltrs_nontermination_proof" = 
   2.409 -  Rel_Loop "(('f,'l)lab,'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   2.410 -| Rel_Not_Well_Formed
   2.411 -| Rel_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) reltrs_nontermination_proof"
   2.412 -| Rel_R_Not_SN "('f,'l,'v) trs_nontermination_proof"
   2.413 -| Rel_TRS_Assume_Not_SN  "('f, 'l, 'v)qreltrsLL" 
   2.414 -    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   2.415 -     ('f, 'l, 'v) dp_nontermination_proof, 
   2.416 -     ('f, 'l, 'v) reltrs_nontermination_proof, 
   2.417 -     ('f, 'l, 'v) fp_nontermination_proof,
   2.418 -     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   2.419 - and
   2.420 - ('f, 'l, 'v) "fp_nontermination_proof" = 
   2.421 -  FPTRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   2.422 -| FPTRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) fp_nontermination_proof" 
   2.423 -| FPTRS_Assume_Not_SN  "('f, 'l, 'v)fptrsLL" 
   2.424 -    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   2.425 -     ('f, 'l, 'v) dp_nontermination_proof, 
   2.426 -     ('f, 'l, 'v) reltrs_nontermination_proof, 
   2.427 -     ('f, 'l, 'v) fp_nontermination_proof,
   2.428 -     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   2.429 - and
   2.430 - ('f, 'l, 'v) neg_unknown_proof =
   2.431 -  Assume_NT_Unknown unknown_info 
   2.432 -    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   2.433 -     ('f, 'l, 'v) dp_nontermination_proof, 
   2.434 -     ('f, 'l, 'v) reltrs_nontermination_proof, 
   2.435 -     ('f, 'l, 'v) fp_nontermination_proof,
   2.436 -     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   2.437 -
   2.438 +    DP_Loop "(('f, 'l) lab, 'v) term" "(('f, 'l) lab, 'v) prseq" "(('f, 'l) lab, 'v) substL" "(('f, 'l) lab, 'v) ctxt"
   2.439 +  | DP_Nonloop "(('f, 'l) lab, 'v) non_loop_prf"
   2.440 +  | DP_Rule_Removal "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_nontermination_proof"
   2.441 +  | DP_Q_Increase "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_nontermination_proof"
   2.442 +  | DP_Q_Reduction "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_nontermination_proof"
   2.443 +  | DP_Termination_Switch "('f, 'l) lab join_info" "('f, 'l, 'v) dp_nontermination_proof"
   2.444 +  | DP_Instantiation "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_nontermination_proof"
   2.445 +  | 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"
   2.446 +  | DP_Narrowing "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_nontermination_proof"
   2.447 +  | DP_Assume_Infinite  "('f, 'l, 'v) dppLL"
   2.448 +      "('f, 'l, 'v, ('f, 'l, 'v) trs_nontermination_proof,
   2.449 +       ('f, 'l, 'v) dp_nontermination_proof,
   2.450 +       ('f, 'l, 'v) reltrs_nontermination_proof,
   2.451 +       ('f, 'l, 'v) fp_nontermination_proof,
   2.452 +       ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   2.453 +and ('f, 'l, 'v) "trs_nontermination_proof" =
   2.454 +    TRS_Loop "(('f, 'l) lab, 'v) term" "(('f, 'l) lab, 'v) rseq" "(('f, 'l) lab, 'v) substL" "(('f, 'l) lab, 'v) ctxt"
   2.455 +  | TRS_Not_Well_Formed
   2.456 +  | TRS_Rule_Removal "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_nontermination_proof"
   2.457 +  | TRS_String_Reversal "('f, 'l, 'v) trs_nontermination_proof"
   2.458 +  | TRS_DP_Trans "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_nontermination_proof"
   2.459 +  | TRS_Nonloop "(('f, 'l) lab, 'v) non_loop_prf"
   2.460 +  | TRS_Q_Increase "('f, 'l, 'v) termsLL" "('f, 'l, 'v) trs_nontermination_proof"
   2.461 +  | TRS_Assume_Not_SN  "('f, 'l, 'v) qtrsLL"
   2.462 +      "('f, 'l, 'v, ('f, 'l, 'v) trs_nontermination_proof,
   2.463 +       ('f, 'l, 'v) dp_nontermination_proof,
   2.464 +       ('f, 'l, 'v) reltrs_nontermination_proof,
   2.465 +       ('f, 'l, 'v) fp_nontermination_proof,
   2.466 +       ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   2.467 +and ('f, 'l, 'v)"reltrs_nontermination_proof" =
   2.468 +    Rel_Loop "(('f, 'l) lab, 'v) term" "(('f, 'l) lab, 'v) prseq" "(('f, 'l) lab, 'v) substL" "(('f, 'l) lab, 'v) ctxt"
   2.469 +  | Rel_Not_Well_Formed
   2.470 +  | Rel_Rule_Removal "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) reltrs_nontermination_proof"
   2.471 +  | Rel_R_Not_SN "('f, 'l, 'v) trs_nontermination_proof"
   2.472 +  | Rel_TRS_Assume_Not_SN  "('f, 'l, 'v) qreltrsLL"
   2.473 +      "('f, 'l, 'v, ('f, 'l, 'v) trs_nontermination_proof,
   2.474 +       ('f, 'l, 'v) dp_nontermination_proof,
   2.475 +       ('f, 'l, 'v) reltrs_nontermination_proof,
   2.476 +       ('f, 'l, 'v) fp_nontermination_proof,
   2.477 +       ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   2.478 +and ('f, 'l, 'v) "fp_nontermination_proof" =
   2.479 +    FPTRS_Loop "(('f, 'l) lab, 'v) term" "(('f, 'l) lab, 'v) rseq" "(('f, 'l) lab, 'v) substL" "(('f, 'l) lab, 'v) ctxt"
   2.480 +  | FPTRS_Rule_Removal "('f, 'l, 'v) trsLL" "('f, 'l, 'v) fp_nontermination_proof"
   2.481 +  | FPTRS_Assume_Not_SN  "('f, 'l, 'v) fptrsLL"
   2.482 +      "('f, 'l, 'v, ('f, 'l, 'v) trs_nontermination_proof,
   2.483 +       ('f, 'l, 'v) dp_nontermination_proof,
   2.484 +       ('f, 'l, 'v) reltrs_nontermination_proof,
   2.485 +       ('f, 'l, 'v) fp_nontermination_proof,
   2.486 +       ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   2.487 +and ('f, 'l, 'v) neg_unknown_proof =
   2.488 +    Assume_NT_Unknown unknown_info
   2.489 +      "('f, 'l, 'v, ('f, 'l, 'v) trs_nontermination_proof,
   2.490 +       ('f, 'l, 'v) dp_nontermination_proof,
   2.491 +       ('f, 'l, 'v) reltrs_nontermination_proof,
   2.492 +       ('f, 'l, 'v) fp_nontermination_proof,
   2.493 +       ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   2.494  
   2.495  datatype_new ('f, 'l, 'v) dp_termination_proof =
   2.496 -  P_is_Empty
   2.497 -| Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL"
   2.498 -    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.499 -| Redpair_Proc "('f,'l)lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL"  "('f, 'l, 'v) dp_termination_proof"
   2.500 -| Redpair_UR_Proc "('f, 'l) lab root_redtriple_impl + ('f, 'l) lab redtriple_impl"
   2.501 -    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" 
   2.502 -| Usable_Rules_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" 
   2.503 -| Dep_Graph_Proc "(('f, 'l, 'v) dp_termination_proof option \<times> ('f, 'l, 'v) trsLL) list"
   2.504 -| Mono_Redpair_Proc "('f, 'l) lab redtriple_impl"
   2.505 -    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" 
   2.506 -| Mono_Redpair_UR_Proc "('f, 'l) lab redtriple_impl"
   2.507 -    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.508 -| Size_Change_Subterm_Proc "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
   2.509 -| Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option"
   2.510 -    "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
   2.511 -| Uncurry_Proc "nat option" "(('f, 'l) lab, 'v) uncurry_info"
   2.512 -    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.513 -| Fcc_Proc "('f, 'l) lab" "(('f, 'l) lab, 'v) ctxt list"
   2.514 -    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.515 -| Split_Proc
   2.516 -    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" 
   2.517 -    "('f, 'l, 'v) dp_termination_proof" "('f, 'l, 'v) dp_termination_proof"
   2.518 -| Semlab_Proc
   2.519 -    "(('f, 'l) lab, 'v) sl_variant" "('f, 'l, 'v) trsLL"
   2.520 -    "(('f, 'l) lab, 'v) term list" "('f, 'l, 'v) trsLL"
   2.521 -    "('f, 'l, 'v) dp_termination_proof"
   2.522 -| Switch_Innermost_Proc "('f, 'l) lab join_info" "('f, 'l, 'v) dp_termination_proof"
   2.523 -| Rewriting_Proc
   2.524 -    "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL"
   2.525 -    "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) dp_termination_proof"
   2.526 -| Instantiation_Proc "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.527 -| Forward_Instantiation_Proc
   2.528 -    "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_termination_proof"
   2.529 -| Narrowing_Proc "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.530 -| Assume_Finite
   2.531 -    "('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"
   2.532 -| Unlab_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.533 -| Q_Reduction_Proc "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_termination_proof"
   2.534 -| Complex_Constant_Removal_Proc "(('f,'l)lab,'v)complex_constant_removal_prf" "('f, 'l, 'v) dp_termination_proof"
   2.535 -| General_Redpair_Proc
   2.536 -    "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL"
   2.537 -    "(('f, 'l) lab, 'v) cond_red_pair_prf" "('f, 'l, 'v) dp_termination_proof list" 
   2.538 -| To_Trs_Proc "('f, 'l, 'v) trs_termination_proof"
   2.539 +    P_is_Empty
   2.540 +  | Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL"
   2.541 +      "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.542 +  | Redpair_Proc "('f, 'l) lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL"  "('f, 'l, 'v) dp_termination_proof"
   2.543 +  | Redpair_UR_Proc "('f, 'l) lab root_redtriple_impl + ('f, 'l) lab redtriple_impl"
   2.544 +      "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.545 +  | Usable_Rules_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.546 +  | Dep_Graph_Proc "(('f, 'l, 'v) dp_termination_proof option \<times> ('f, 'l, 'v) trsLL) list"
   2.547 +  | Mono_Redpair_Proc "('f, 'l) lab redtriple_impl"
   2.548 +      "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.549 +  | Mono_Redpair_UR_Proc "('f, 'l) lab redtriple_impl"
   2.550 +      "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.551 +  | Size_Change_Subterm_Proc "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
   2.552 +  | Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option"
   2.553 +      "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
   2.554 +  | Uncurry_Proc "nat option" "(('f, 'l) lab, 'v) uncurry_info"
   2.555 +      "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.556 +  | Fcc_Proc "('f, 'l) lab" "(('f, 'l) lab, 'v) ctxt list"
   2.557 +      "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.558 +  | Split_Proc
   2.559 +      "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL"
   2.560 +      "('f, 'l, 'v) dp_termination_proof" "('f, 'l, 'v) dp_termination_proof"
   2.561 +  | Semlab_Proc
   2.562 +      "(('f, 'l) lab, 'v) sl_variant" "('f, 'l, 'v) trsLL"
   2.563 +      "(('f, 'l) lab, 'v) term list" "('f, 'l, 'v) trsLL"
   2.564 +      "('f, 'l, 'v) dp_termination_proof"
   2.565 +  | Switch_Innermost_Proc "('f, 'l) lab join_info" "('f, 'l, 'v) dp_termination_proof"
   2.566 +  | Rewriting_Proc
   2.567 +      "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL"
   2.568 +      "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) dp_termination_proof"
   2.569 +  | Instantiation_Proc "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.570 +  | Forward_Instantiation_Proc
   2.571 +      "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_termination_proof"
   2.572 +  | Narrowing_Proc "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.573 +  | Assume_Finite
   2.574 +      "('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"
   2.575 +  | Unlab_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   2.576 +  | Q_Reduction_Proc "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_termination_proof"
   2.577 +  | Complex_Constant_Removal_Proc "(('f, 'l) lab, 'v) complex_constant_removal_prf" "('f, 'l, 'v) dp_termination_proof"
   2.578 +  | General_Redpair_Proc
   2.579 +      "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL"
   2.580 +      "(('f, 'l) lab, 'v) cond_red_pair_prf" "('f, 'l, 'v) dp_termination_proof list"
   2.581 +  | To_Trs_Proc "('f, 'l, 'v) trs_termination_proof"
   2.582  and ('f, 'l, 'v) trs_termination_proof =
   2.583 -  DP_Trans bool bool "(('f, 'l) lab, 'v) rules" "('f, 'l, 'v) dp_termination_proof"
   2.584 -| Rule_Removal "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v)trs_termination_proof"
   2.585 -| String_Reversal "('f, 'l, 'v) trs_termination_proof"
   2.586 -| Bounds "(('f, 'l) lab, 'v) bounds_info"
   2.587 -| Uncurry "(('f, 'l) lab, 'v) uncurry_info" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   2.588 -| Semlab
   2.589 -    "(('f, 'l) lab, 'v) sl_variant" "(('f, 'l) lab, 'v) term list"
   2.590 -    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   2.591 -| R_is_Empty
   2.592 -| Fcc "(('f, 'l) lab, 'v) ctxt list" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   2.593 -| Split "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" "('f, 'l, 'v) trs_termination_proof"
   2.594 -| Switch_Innermost "('f, 'l) lab join_info" "('f, 'l, 'v) trs_termination_proof" 
   2.595 -| Drop_Equality "('f, 'l, 'v) trs_termination_proof"
   2.596 -| Remove_Nonapplicable_Rules "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   2.597 -| 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"
   2.598 +    DP_Trans bool bool "(('f, 'l) lab, 'v) rules" "('f, 'l, 'v) dp_termination_proof"
   2.599 +  | Rule_Removal "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   2.600 +  | String_Reversal "('f, 'l, 'v) trs_termination_proof"
   2.601 +  | Bounds "(('f, 'l) lab, 'v) bounds_info"
   2.602 +  | Uncurry "(('f, 'l) lab, 'v) uncurry_info" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   2.603 +  | Semlab
   2.604 +      "(('f, 'l) lab, 'v) sl_variant" "(('f, 'l) lab, 'v) term list"
   2.605 +      "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   2.606 +  | R_is_Empty
   2.607 +  | Fcc "(('f, 'l) lab, 'v) ctxt list" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   2.608 +  | Split "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" "('f, 'l, 'v) trs_termination_proof"
   2.609 +  | Switch_Innermost "('f, 'l) lab join_info" "('f, 'l, 'v) trs_termination_proof"
   2.610 +  | Drop_Equality "('f, 'l, 'v) trs_termination_proof"
   2.611 +  | Remove_Nonapplicable_Rules "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   2.612 +  | 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"
   2.613  and ('f, 'l, 'v) unknown_proof =
   2.614 -  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"
   2.615 +    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"
   2.616  and ('f, 'l, 'v) fptrs_termination_proof =
   2.617 -  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"
   2.618 -
   2.619 +    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"
   2.620  
   2.621  end
     3.1 --- a/src/HOL/BNF_Examples/Koenig.thy	Thu Jul 24 00:24:00 2014 +0200
     3.2 +++ b/src/HOL/BNF_Examples/Koenig.thy	Thu Jul 24 00:24:00 2014 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  Koenig's lemma.
     3.5  *)
     3.6  
     3.7 -header {* Koenig's lemma *}
     3.8 +header {* Koenig's Lemma *}
     3.9  
    3.10  theory Koenig
    3.11  imports TreeFI Stream
     4.1 --- a/src/HOL/BNF_Examples/Stream_Processor.thy	Thu Jul 24 00:24:00 2014 +0200
     4.2 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Thu Jul 24 00:24:00 2014 +0200
     4.3 @@ -3,10 +3,10 @@
     4.4      Author:     Andrei Popescu, TU Muenchen
     4.5      Copyright   2014
     4.6  
     4.7 -Stream processors---a syntactic representation of continuous functions on streams
     4.8 +Stream processors---a syntactic representation of continuous functions on streams.
     4.9  *)
    4.10  
    4.11 -header {* Stream Processors *}
    4.12 +header {* Stream Processors---A Syntactic Representation of Continuous Functions on Streams *}
    4.13  
    4.14  theory Stream_Processor
    4.15  imports Stream "~~/src/HOL/Library/BNF_Axiomatization"