# HG changeset patch # User wenzelm # Date 1405969067 -7200 # Node ID 5c3484b90d5c11f136e04009aede5bfadcf54365 # Parent 5efff4075b63db8455d55b3816b143d57c258f14# Parent 3a1b1bda702f8a0bf5b14228f52f72b18f2bd910 merged diff -r 3a1b1bda702f -r 5c3484b90d5c Admin/isatest/settings/afp-poly --- a/Admin/isatest/settings/afp-poly Mon Jul 21 20:36:25 2014 +0200 +++ b/Admin/isatest/settings/afp-poly Mon Jul 21 20:57:47 2014 +0200 @@ -5,7 +5,7 @@ # to be retired: # JINJATHREADS_OPTIONS="-M 1 -q 0 -p 0" -# ISABELLE_GHC=/opt/local/bin/ghc +ISABELLE_GHC=ghc ISABELLE_HOME_USER=~/afp/isabelle-afp-poly diff -r 3a1b1bda702f -r 5c3484b90d5c Admin/isatest/settings/mac-poly-M2 --- a/Admin/isatest/settings/mac-poly-M2 Mon Jul 21 20:36:25 2014 +0200 +++ b/Admin/isatest/settings/mac-poly-M2 Mon Jul 21 20:57:47 2014 +0200 @@ -9,7 +9,7 @@ ML_HOME="/home/polyml/polyml-5.5.0/$ML_PLATFORM" ML_OPTIONS="-H 500" -#ISABELLE_GHC=/opt/local/bin/ghc +ISABELLE_GHC=ghc ISABELLE_HOME_USER=~/isabelle-mac-poly-M2 diff -r 3a1b1bda702f -r 5c3484b90d5c Admin/isatest/settings/mac-poly-M4 --- a/Admin/isatest/settings/mac-poly-M4 Mon Jul 21 20:36:25 2014 +0200 +++ b/Admin/isatest/settings/mac-poly-M4 Mon Jul 21 20:57:47 2014 +0200 @@ -8,7 +8,7 @@ ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="-H 500 --gcthreads 4" -#ISABELLE_GHC=/opt/local/bin/ghc +ISABELLE_GHC=ghc ISABELLE_HOME_USER=~/isabelle-mac-poly-M4 diff -r 3a1b1bda702f -r 5c3484b90d5c Admin/isatest/settings/mac-poly-M8 --- a/Admin/isatest/settings/mac-poly-M8 Mon Jul 21 20:36:25 2014 +0200 +++ b/Admin/isatest/settings/mac-poly-M8 Mon Jul 21 20:57:47 2014 +0200 @@ -8,7 +8,7 @@ ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="-H 500 --gcthreads 8" -#ISABELLE_GHC=/opt/local/bin/ghc +ISABELLE_GHC=ghc ISABELLE_HOME_USER=~/isabelle-mac-poly-M8 diff -r 3a1b1bda702f -r 5c3484b90d5c Admin/isatest/settings/mac-poly-M8-quick_and_dirty --- a/Admin/isatest/settings/mac-poly-M8-quick_and_dirty Mon Jul 21 20:36:25 2014 +0200 +++ b/Admin/isatest/settings/mac-poly-M8-quick_and_dirty Mon Jul 21 20:57:47 2014 +0200 @@ -8,7 +8,7 @@ ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="-H 1000 --gcthreads 8" -#ISABELLE_GHC=/opt/local/bin/ghc +ISABELLE_GHC=ghc ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-quick_and_dirty diff -r 3a1b1bda702f -r 5c3484b90d5c Admin/isatest/settings/mac-poly-M8-skip_proofs --- a/Admin/isatest/settings/mac-poly-M8-skip_proofs Mon Jul 21 20:36:25 2014 +0200 +++ b/Admin/isatest/settings/mac-poly-M8-skip_proofs Mon Jul 21 20:57:47 2014 +0200 @@ -8,7 +8,7 @@ ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="-H 1000 --gcthreads 8" -#ISABELLE_GHC=/opt/local/bin/ghc +ISABELLE_GHC=ghc ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-skip_proofs diff -r 3a1b1bda702f -r 5c3484b90d5c Admin/isatest/settings/mac-poly64-M2 --- a/Admin/isatest/settings/mac-poly64-M2 Mon Jul 21 20:36:25 2014 +0200 +++ b/Admin/isatest/settings/mac-poly64-M2 Mon Jul 21 20:57:47 2014 +0200 @@ -8,7 +8,7 @@ ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="-H 1000" -#ISABELLE_GHC=/opt/local/bin/ghc +ISABELLE_GHC=ghc ISABELLE_HOME_USER=~/isabelle-at-mac-poly64-M2 diff -r 3a1b1bda702f -r 5c3484b90d5c Admin/isatest/settings/mac-poly64-M4 --- a/Admin/isatest/settings/mac-poly64-M4 Mon Jul 21 20:36:25 2014 +0200 +++ b/Admin/isatest/settings/mac-poly64-M4 Mon Jul 21 20:57:47 2014 +0200 @@ -8,7 +8,7 @@ ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="-H 2000 --gcthreads 4" -#ISABELLE_GHC=/opt/local/bin/ghc +ISABELLE_GHC=ghc ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4 diff -r 3a1b1bda702f -r 5c3484b90d5c Admin/isatest/settings/mac-poly64-M8 --- a/Admin/isatest/settings/mac-poly64-M8 Mon Jul 21 20:36:25 2014 +0200 +++ b/Admin/isatest/settings/mac-poly64-M8 Mon Jul 21 20:57:47 2014 +0200 @@ -8,7 +8,7 @@ ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="-H 2000 --gcthreads 8" -#ISABELLE_GHC=/opt/local/bin/ghc +ISABELLE_GHC=ghc ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8 diff -r 3a1b1bda702f -r 5c3484b90d5c src/HOL/BNF_Examples/IsaFoR_Datatypes.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF_Examples/IsaFoR_Datatypes.thy Mon Jul 21 20:57:47 2014 +0200 @@ -0,0 +1,380 @@ +(* Title: HOL/BNF_Examples/IsaFoR_Datatypes.thy + Author: René Thiemann + Copyright 2014 + +Benchmark of datatypes defined in IsaFoR +*) + +theory IsaFoR_Datatypes +imports + Real +begin + +datatype_new ('f, 'l) lab = + Lab "('f, 'l) lab" 'l +| FunLab "('f, 'l) lab" "('f, 'l) lab list" +| UnLab 'f +| Sharp "('f, 'l) lab" + +datatype_new 'f projL = Projection "(('f \ nat) \ nat) list" + +datatype_new ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list" +datatype_new ('f, 'v) ctxt = + Hole ("\") +| More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list" + + +type_synonym ('f, 'v) rule = "('f, 'v) term \ ('f, 'v) term" +type_synonym ('f, 'v) trs = "('f, 'v) rule set" + +type_synonym ('f, 'v) rules = "('f,'v) rule list" +type_synonym ('f, 'l, 'v) ruleLL = "(('f, 'l) lab, 'v) rule" +type_synonym ('f, 'l, 'v) trsLL = "(('f, 'l) lab, 'v) rules" +type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list" +datatype_new pos = Empty ("\") | PCons "nat" "pos" (infixr "<#" 70) +type_synonym ('f, 'v) prseq = "(pos \ ('f, 'v) rule \ bool \ ('f, 'v) term) list" +type_synonym ('f, 'v) rseq = "(pos \ ('f, 'v) rule \ ('f, 'v) term) list" + +type_synonym ('f, 'l, 'v) rseqL = "((('f, 'l) lab, 'v) rule \ (('f, 'l) lab, 'v) rseq) list" +type_synonym ('f, 'l, 'v) dppLL = + "bool \ bool \ ('f, 'l, 'v) trsLL \ ('f, 'l, 'v) trsLL \ + ('f, 'l, 'v) termsLL \ + ('f, 'l, 'v) trsLL \ ('f, 'l, 'v) trsLL" + +type_synonym ('f, 'l, 'v) qreltrsLL = + "bool \ ('f, 'l, 'v) termsLL \ ('f, 'l, 'v) trsLL \ ('f, 'l, 'v) trsLL" + +type_synonym ('f, 'l, 'v) qtrsLL = + "bool \ ('f, 'l, 'v) termsLL \ ('f, 'l, 'v) trsLL" + +datatype_new location = H | A | B | R + +type_synonym ('f,'v)forb_pattern = "('f,'v)ctxt \ ('f,'v)term \ location" +type_synonym ('f,'v)forb_patterns = "('f,'v)forb_pattern set" + +type_synonym ('f, 'l, 'v) fptrsLL = + "(('f, 'l)lab, 'v) forb_pattern list \ ('f, 'l, 'v) trsLL" + +type_synonym ('f, 'l, 'v) prob = "('f, 'l, 'v) qreltrsLL + ('f, 'l, 'v) dppLL" + +type_synonym ('f, 'a) lpoly_inter = "'f \ nat \ ('a \ 'a list)" +type_synonym ('f, 'a) lpoly_interL = "(('f \ nat) \ ('a \ 'a list)) list" + +type_synonym 'v monom = "('v \ nat)list" +type_synonym ('v,'a)poly = "('v monom \ 'a)list" +type_synonym ('f,'a)poly_inter_list = "(('f \ nat) \ (nat,'a)poly)list" +type_synonym 'a vec = "'a list" +type_synonym 'a mat = "'a vec list" + + +datatype_new arctic = MinInfty | Num_arc int +datatype_new 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a +datatype_new order_tag = Lex | Mul + +type_synonym 'f status_prec_repr = "(('f \ nat) \ (nat \ order_tag))list" +datatype_new af_entry = Collapse nat | AFList "nat list" +type_synonym 'f afs_list = "(('f \ nat) \ af_entry)list" +type_synonym 'f prec_weight_repr = "(('f \ nat) \ (nat \ nat \ (nat list option)))list \ nat" + + +datatype_new 'f redtriple_impl = + Int_carrier "('f, int) lpoly_interL" + | Int_nl_carrier "('f, int) poly_inter_list" + | Rat_carrier "('f, rat) lpoly_interL" + | Rat_nl_carrier rat "('f, rat) poly_inter_list" + | Real_carrier "('f, real) lpoly_interL" + | Real_nl_carrier real "('f, real) poly_inter_list" + | Arctic_carrier "('f, arctic) lpoly_interL" + | Arctic_rat_carrier "('f, rat arctic_delta) lpoly_interL" + | Int_mat_carrier nat nat "('f, int mat) lpoly_interL" + | Rat_mat_carrier nat nat "('f, rat mat) lpoly_interL" + | Real_mat_carrier nat nat "('f, real mat) lpoly_interL" + | Arctic_mat_carrier nat "('f, arctic mat) lpoly_interL" + | Arctic_rat_mat_carrier nat "('f, rat arctic_delta mat) lpoly_interL" + | RPO "'f status_prec_repr" "'f afs_list" + | KBO "'f prec_weight_repr" "'f afs_list" + +datatype_new list_order_type = MS_Ext | Max_Ext | Min_Ext | Dms_Ext +type_synonym 'f scnp_af = "(('f \ nat) \ (nat \ nat) list) list" + +datatype_new 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl" + +type_synonym 'f sig_map_list = "(('f \ nat) \ 'f list) list" +type_synonym ('f,'v) uncurry_info = "'f \ 'f sig_map_list \ ('f,'v)rules \ ('f,'v)rules" + +datatype_new arithFun = + Arg nat +| Const nat +| Sum "arithFun list" +| Max "arithFun list" +| Min "arithFun list" +| Prod "arithFun list" +| IfEqual arithFun arithFun arithFun arithFun + +datatype_new 'f sl_inter = SL_Inter nat "(('f \ nat) \ arithFun) list" +datatype_new ('f,'v)sl_variant = Rootlab "('f \ nat) option" | Finitelab "'f sl_inter" | QuasiFinitelab "'f sl_inter" 'v + +type_synonym ('f,'v)crit_pair_joins = "(('f,'v)term \ ('f,'v)rseq \ ('f,'v)term \ ('f,'v)rseq)list" +datatype_new 'f join_info = Guided "('f,string)crit_pair_joins" | Join_NF | Join_BFS nat + +type_synonym unknown_info = string + +type_synonym dummy_prf = unit + + +datatype_new ('f,'v)complex_constant_removal_prf = Complex_Constant_Removal_Proof + "('f,'v)term" + "(('f,'v)rule \ ('f,'v)rule) list" + +datatype_new ('f,'v)cond_constraint + = CC_cond bool "('f,'v)rule" + | CC_rewr "('f,'v)term" "('f,'v)term" + | CC_impl "('f,'v)cond_constraint list" "('f,'v)cond_constraint" + | CC_all 'v "('f,'v)cond_constraint" + +type_synonym ('f, 'v, 'w) gsubstL = "('v \ ('f, 'w) term) list" +type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL" + +datatype_new ('f,'v)cond_constraint_prf = + Final +| Delete_Condition "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" +| Different_Constructor "('f,'v)cond_constraint" +| Same_Constructor "('f,'v)cond_constraint" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" +| Variable_Equation 'v "('f,'v)term" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" +| Funarg_Into_Var "('f,'v)cond_constraint" nat 'v "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" +| Simplify_Condition "('f,'v)cond_constraint" "('f,'v)substL" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" +| Induction "('f,'v)cond_constraint" "('f,'v)cond_constraint list" "(('f,'v)rule \ (('f,'v)term \ 'v list) list \ ('f,'v)cond_constraint \ ('f,'v)cond_constraint_prf) list" + + +datatype_new ('f,'v)cond_red_pair_prf = Cond_Red_Pair_Prf + 'f + "(('f,'v)cond_constraint \ ('f,'v)rules \ ('f,'v)cond_constraint_prf) list" + nat + nat + +datatype_new ('q,'f)ta_rule = TA_rule 'f "'q list" 'q ("_ _ \ _") +datatype_new ('q,'f)tree_automaton = Tree_Automaton "'q list" "('q,'f)ta_rule list" "('q \ 'q)list" +datatype_new 'q ta_relation = Decision_Proc | Id_Relation | Some_Relation "('q \ 'q) list" + +datatype_new boundstype = Roof | Match +datatype_new ('f,'q)bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \ nat) tree_automaton" "'q ta_relation" + +datatype_new ('f, 'v) pat_eqv_prf = + Pat_Dom_Renaming "('f, 'v) substL" +| Pat_Irrelevant "('f, 'v) substL" "('f, 'v) substL" +| Pat_Simplify "('f, 'v) substL" "('f, 'v) substL" + +datatype_new pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close + +datatype_new ('f, 'v) pat_rule_prf = + Pat_OrigRule "('f, 'v) rule" bool +| Pat_InitPump "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" +| Pat_InitPumpCtxt "('f, 'v) pat_rule_prf" "('f, 'v) substL" pos 'v +| Pat_Equiv "('f, 'v) pat_rule_prf" bool "('f, 'v) pat_eqv_prf" +| Pat_Narrow "('f, 'v) pat_rule_prf" "('f, 'v) pat_rule_prf" pos +| Pat_Inst "('f, 'v) pat_rule_prf" "('f, 'v) substL" pat_rule_pos +| Pat_Rewr "('f, 'v) pat_rule_prf" "('f, 'v) term \ ('f, 'v) rseq" pat_rule_pos 'v +| Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat + +datatype_new ('f, 'v) non_loop_prf = + Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos + + +datatype_new ('f, 'l, 'v) problem = + SN_TRS "('f,'l,'v)qreltrsLL" +| SN_FP_TRS "('f,'l,'v)fptrsLL" +| Finite_DPP "('f,'l,'v) dppLL" +| Unknown_Problem unknown_info +| Not_SN_TRS "('f,'l,'v)qtrsLL" +| Not_RelSN_TRS "('f,'l,'v)qreltrsLL" +| Infinite_DPP "('f,'l,'v) dppLL" +| Not_SN_FP_TRS "('f,'l,'v)fptrsLL" +declare [[bnf_timing]] +datatype_new ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof = + SN_assm_proof "('f,'l,'v)qreltrsLL" 'a +| Finite_assm_proof "('f,'l,'v)dppLL" 'b +| SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'c +| Not_SN_assm_proof "('f,'l,'v)qtrsLL" 'a +| Infinite_assm_proof "('f,'l,'v)dppLL" 'b +| Not_RelSN_assm_proof "('f,'l,'v)qreltrsLL" 'c +| Not_SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'd +| Unknown_assm_proof unknown_info 'e + +type_synonym ('f,'l,'v,'a,'b,'c,'d)assm_proof = "('f,'l,'v,'a,'b,'c,dummy_prf,'d)generic_assm_proof" + +datatype_new ('f, 'l, 'v) assm = + SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" +| SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL" +| Finite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL" +| Unknown_assm "('f,'l,'v)problem list" unknown_info +| Not_SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qtrsLL" +| Not_RelSN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" +| Not_SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL" +| Infinite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL" + +fun satisfied :: "('f,'l,'v)problem \ bool" where + "satisfied (SN_TRS t) = (t = t)" +| "satisfied (SN_FP_TRS t) = (t \ t)" +| "satisfied (Finite_DPP d) = (d \ d)" +| "satisfied (Unknown_Problem s) = (s = ''foo'')" +| "satisfied (Not_SN_TRS (nfs,q,r)) = (length q = length r)" +| "satisfied (Not_RelSN_TRS (nfs,q,r,rw)) = (r = rw)" +| "satisfied (Infinite_DPP d) = (d = d)" +| "satisfied (Not_SN_FP_TRS t) = (t = t)" + +fun collect_assms :: "('tp \ ('f,'l,'v) assm list) + \ ('dpp \ ('f,'l,'v) assm list) + \ ('fptp \ ('f,'l,'v) assm list) + \ ('unk \ ('f,'l,'v) assm list) + \ ('f,'l,'v,'tp,'dpp,'fptp,'unk) assm_proof \ ('f,'l,'v) assm list" where + "collect_assms tp dpp fptp unk (SN_assm_proof t prf) = tp prf" +| "collect_assms tp dpp fptp unk (SN_FP_assm_proof t prf) = fptp prf" +| "collect_assms tp dpp fptp unk (Finite_assm_proof d prf) = dpp prf" +| "collect_assms tp dpp fptp unk (Unknown_assm_proof p prf) = unk prf" +| "collect_assms _ _ _ _ _ = []" + +fun collect_neg_assms :: "('tp \ ('f,'l,'v) assm list) + \ ('dpp \ ('f,'l,'v) assm list) + \ ('rtp \ ('f,'l,'v) assm list) + \ ('fptp \ ('f,'l,'v) assm list) + \ ('unk \ ('f,'l,'v) assm list) + \ ('f,'l,'v,'tp,'dpp,'rtp,'fptp,'unk) generic_assm_proof \ ('f,'l,'v) assm list" where + "collect_neg_assms tp dpp rtp fptp unk (Not_SN_assm_proof t prf) = tp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Infinite_assm_proof d prf) = dpp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Not_RelSN_assm_proof t prf) = rtp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Not_SN_FP_assm_proof t prf) = fptp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf" +| "collect_neg_assms tp dpp rtp fptp unk _ = []" + + + +datatype_new ('f, 'l, 'v) dp_nontermination_proof = + DP_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" +| DP_Nonloop "(('f,'l)lab, 'v)non_loop_prf" +| DP_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) dp_nontermination_proof" +| DP_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof" +| DP_Q_Reduction "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof" +| DP_Termination_Switch "('f,'l)lab join_info" "('f,'l,'v) dp_nontermination_proof" +| DP_Instantiation "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof" +| 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" +| DP_Narrowing "('f,'l,'v)ruleLL" pos "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof" +| DP_Assume_Infinite "('f, 'l, 'v) dppLL" + "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, + ('f, 'l, 'v) dp_nontermination_proof, + ('f, 'l, 'v) reltrs_nontermination_proof, + ('f, 'l, 'v) fp_nontermination_proof, + ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" + and +('f,'l,'v) "trs_nontermination_proof" = + TRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" +| TRS_Not_Well_Formed +| TRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) trs_nontermination_proof" +| TRS_String_Reversal "('f,'l,'v) trs_nontermination_proof" +| TRS_DP_Trans "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof" +| TRS_Nonloop "(('f,'l)lab,'v) non_loop_prf" +| TRS_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) trs_nontermination_proof" +| TRS_Assume_Not_SN "('f, 'l, 'v)qtrsLL" + "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, + ('f, 'l, 'v) dp_nontermination_proof, + ('f, 'l, 'v) reltrs_nontermination_proof, + ('f, 'l, 'v) fp_nontermination_proof, + ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" + and +('f,'l,'v)"reltrs_nontermination_proof" = + Rel_Loop "(('f,'l)lab,'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" +| Rel_Not_Well_Formed +| Rel_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) reltrs_nontermination_proof" +| Rel_R_Not_SN "('f,'l,'v) trs_nontermination_proof" +| Rel_TRS_Assume_Not_SN "('f, 'l, 'v)qreltrsLL" + "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, + ('f, 'l, 'v) dp_nontermination_proof, + ('f, 'l, 'v) reltrs_nontermination_proof, + ('f, 'l, 'v) fp_nontermination_proof, + ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" + and + ('f, 'l, 'v) "fp_nontermination_proof" = + FPTRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" +| FPTRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) fp_nontermination_proof" +| FPTRS_Assume_Not_SN "('f, 'l, 'v)fptrsLL" + "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, + ('f, 'l, 'v) dp_nontermination_proof, + ('f, 'l, 'v) reltrs_nontermination_proof, + ('f, 'l, 'v) fp_nontermination_proof, + ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" + and + ('f, 'l, 'v) neg_unknown_proof = + Assume_NT_Unknown unknown_info + "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, + ('f, 'l, 'v) dp_nontermination_proof, + ('f, 'l, 'v) reltrs_nontermination_proof, + ('f, 'l, 'v) fp_nontermination_proof, + ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" + + +datatype_new ('f, 'l, 'v) dp_termination_proof = + P_is_Empty +| Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Redpair_Proc "('f,'l)lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Redpair_UR_Proc "('f, 'l) lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Usable_Rules_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Dep_Graph_Proc "(('f, 'l, 'v) dp_termination_proof option \ ('f, 'l, 'v) trsLL) list" +| Mono_Redpair_Proc "('f, 'l) lab redtriple_impl" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Mono_Redpair_UR_Proc "('f, 'l) lab redtriple_impl" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Size_Change_Subterm_Proc "((('f, 'l) lab, 'v) rule \ ((nat \ nat) list \ (nat \ nat) list)) list" +| Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option" + "((('f, 'l) lab, 'v) rule \ ((nat \ nat) list \ (nat \ nat) list)) list" +| Uncurry_Proc "nat option" "(('f, 'l) lab, 'v) uncurry_info" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Fcc_Proc "('f, 'l) lab" "(('f, 'l) lab, 'v) ctxt list" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Split_Proc + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" + "('f, 'l, 'v) dp_termination_proof" "('f, 'l, 'v) dp_termination_proof" +| Semlab_Proc + "(('f, 'l) lab, 'v) sl_variant" "('f, 'l, 'v) trsLL" + "(('f, 'l) lab, 'v) term list" "('f, 'l, 'v) trsLL" + "('f, 'l, 'v) dp_termination_proof" +| Switch_Innermost_Proc "('f, 'l) lab join_info" "('f, 'l, 'v) dp_termination_proof" +| Rewriting_Proc + "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" + "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) dp_termination_proof" +| Instantiation_Proc "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Forward_Instantiation_Proc + "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_termination_proof" +| Narrowing_Proc "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Assume_Finite + "('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" +| Unlab_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Q_Reduction_Proc "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_termination_proof" +| Complex_Constant_Removal_Proc "(('f,'l)lab,'v)complex_constant_removal_prf" "('f, 'l, 'v) dp_termination_proof" +| General_Redpair_Proc + "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" + "(('f, 'l) lab, 'v) cond_red_pair_prf" "('f, 'l, 'v) dp_termination_proof list" +| To_Trs_Proc "('f, 'l, 'v) trs_termination_proof" +and ('f, 'l, 'v) trs_termination_proof = + DP_Trans bool bool "(('f, 'l) lab, 'v) rules" "('f, 'l, 'v) dp_termination_proof" +| Rule_Removal "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v)trs_termination_proof" +| String_Reversal "('f, 'l, 'v) trs_termination_proof" +| Bounds "(('f, 'l) lab, 'v) bounds_info" +| Uncurry "(('f, 'l) lab, 'v) uncurry_info" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" +| Semlab + "(('f, 'l) lab, 'v) sl_variant" "(('f, 'l) lab, 'v) term list" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" +| R_is_Empty +| Fcc "(('f, 'l) lab, 'v) ctxt list" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" +| Split "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" "('f, 'l, 'v) trs_termination_proof" +| Switch_Innermost "('f, 'l) lab join_info" "('f, 'l, 'v) trs_termination_proof" +| Drop_Equality "('f, 'l, 'v) trs_termination_proof" +| Remove_Nonapplicable_Rules "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" +| 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" +and ('f, 'l, 'v) unknown_proof = + 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" +and ('f, 'l, 'v) fptrs_termination_proof = + 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" + + +end diff -r 3a1b1bda702f -r 5c3484b90d5c src/HOL/ROOT --- a/src/HOL/ROOT Mon Jul 21 20:36:25 2014 +0200 +++ b/src/HOL/ROOT Mon Jul 21 20:57:47 2014 +0200 @@ -734,6 +734,8 @@ Misc_Datatype Misc_Primcorec Misc_Primrec + theories [condition = ISABELLE_FULL_TEST] + IsaFoR_Datatypes session "HOL-Word" (main) in Word = HOL + options [document_graph]