clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Benchmarks/Datatype_Benchmark/Brackin.thy Sat Feb 13 12:13:10 2016 +0100
@@ -0,0 +1,41 @@
+(* Title: Benchmarks/Datatype_Benchmark/Brackin.thy
+
+A couple of datatypes from Steve Brackin's work.
+*)
+
+theory Brackin imports Main begin
+
+datatype T =
+ X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
+ X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
+ X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
+ X32 | X33 | X34
+
+datatype ('a, 'b, 'c) TY1 =
+ NoF
+ | Fk 'a "('a, 'b, 'c) TY2"
+and ('a, 'b, 'c) TY2 =
+ Ta bool
+ | Td bool
+ | Tf "('a, 'b, 'c) TY1"
+ | Tk bool
+ | Tp bool
+ | App 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
+ | Pair "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
+and ('a, 'b, 'c) TY3 =
+ NoS
+ | Fresh "('a, 'b, 'c) TY2"
+ | Trustworthy 'a
+ | PrivateKey 'a 'b 'c
+ | PublicKey 'a 'b 'c
+ | Conveyed 'a "('a, 'b, 'c) TY2"
+ | Possesses 'a "('a, 'b, 'c) TY2"
+ | Received 'a "('a, 'b, 'c) TY2"
+ | Recognizes 'a "('a, 'b, 'c) TY2"
+ | NeverMalFromSelf 'a 'b "('a, 'b, 'c) TY2"
+ | Sends 'a "('a, 'b, 'c) TY2" 'b
+ | SharedSecret 'a "('a, 'b, 'c) TY2" 'b
+ | Believes 'a "('a, 'b, 'c) TY3"
+ | And "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Benchmarks/Datatype_Benchmark/IsaFoR.thy Sat Feb 13 12:13:10 2016 +0100
@@ -0,0 +1,380 @@
+(* Title: Benchmarks/Datatype_Benchmark/IsaFoR.thy
+ Author: Rene Thiemann, UIBK
+ Copyright 2014
+
+Benchmark consisting of datatypes defined in IsaFoR.
+*)
+
+section {* Benchmark Consisting of Datatypes Defined in IsaFoR *}
+
+theory IsaFoR
+imports Real
+begin
+
+datatype (discs_sels) ('f, 'l) lab =
+ Lab "('f, 'l) lab" 'l
+ | FunLab "('f, 'l) lab" "('f, 'l) lab list"
+ | UnLab 'f
+ | Sharp "('f, 'l) lab"
+
+datatype (discs_sels) 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
+
+datatype (discs_sels) ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
+datatype (discs_sels) ('f, 'v) ctxt =
+ Hole ("\<box>")
+ | More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
+
+type_synonym ('f, 'v) rule = "('f, 'v) term \<times> ('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 (discs_sels) pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
+
+type_synonym ('f, 'v) prseq = "(pos \<times> ('f, 'v) rule \<times> bool \<times> ('f, 'v) term) list"
+type_synonym ('f, 'v) rseq = "(pos \<times> ('f, 'v) rule \<times> ('f, 'v) term) list"
+
+type_synonym ('f, 'l, 'v) rseqL = "((('f, 'l) lab, 'v) rule \<times> (('f, 'l) lab, 'v) rseq) list"
+type_synonym ('f, 'l, 'v) dppLL =
+ "bool \<times> bool \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL \<times>
+ ('f, 'l, 'v) termsLL \<times>
+ ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL"
+
+type_synonym ('f, 'l, 'v) qreltrsLL =
+ "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL"
+
+type_synonym ('f, 'l, 'v) qtrsLL =
+ "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL"
+
+datatype (discs_sels) location = H | A | B | R
+
+type_synonym ('f, 'v) forb_pattern = "('f, 'v) ctxt \<times> ('f, 'v) term \<times> 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 \<times> ('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 \<times> nat \<Rightarrow> ('a \<times> 'a list)"
+type_synonym ('f, 'a) lpoly_interL = "(('f \<times> nat) \<times> ('a \<times> 'a list)) list"
+
+type_synonym 'v monom = "('v \<times> nat) list"
+type_synonym ('v, 'a) poly = "('v monom \<times> 'a) list"
+type_synonym ('f, 'a) poly_inter_list = "(('f \<times> nat) \<times> (nat, 'a) poly) list"
+type_synonym 'a vec = "'a list"
+type_synonym 'a mat = "'a vec list"
+
+datatype (discs_sels) arctic = MinInfty | Num_arc int
+datatype (discs_sels) 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
+datatype (discs_sels) order_tag = Lex | Mul
+
+type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag)) list"
+
+datatype (discs_sels) af_entry =
+ Collapse nat
+ | AFList "nat list"
+
+type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry) list"
+type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option))) list \<times> nat"
+
+datatype (discs_sels) '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 (discs_sels) list_order_type = MS_Ext | Max_Ext | Min_Ext | Dms_Ext
+type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list"
+
+datatype (discs_sels) 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
+
+type_synonym 'f sig_map_list = "(('f \<times> nat) \<times> 'f list) list"
+type_synonym ('f, 'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f, 'v) rules \<times> ('f, 'v) rules"
+
+datatype (discs_sels) arithFun =
+ Arg nat
+ | Const nat
+ | Sum "arithFun list"
+ | Max "arithFun list"
+ | Min "arithFun list"
+ | Prod "arithFun list"
+ | IfEqual arithFun arithFun arithFun arithFun
+
+datatype (discs_sels) 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
+datatype (discs_sels) ('f, 'v) sl_variant =
+ Rootlab "('f \<times> nat) option"
+ | Finitelab "'f sl_inter"
+ | QuasiFinitelab "'f sl_inter" 'v
+
+type_synonym ('f, 'v) crit_pair_joins = "(('f, 'v) term \<times> ('f, 'v) rseq \<times> ('f, 'v) term \<times> ('f, 'v) rseq) list"
+
+datatype (discs_sels) '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 (discs_sels) ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
+ "('f, 'v) term"
+ "(('f, 'v) rule \<times> ('f, 'v) rule) list"
+
+datatype (discs_sels) ('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 \<times> ('f, 'w) term) list"
+type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL"
+
+datatype (discs_sels) ('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 \<times> (('f, 'v) term \<times> 'v list) list \<times> ('f, 'v) cond_constraint \<times> ('f, 'v) cond_constraint_prf) list"
+
+datatype (discs_sels) ('f, 'v) cond_red_pair_prf =
+ Cond_Red_Pair_Prf
+ 'f "(('f, 'v) cond_constraint \<times> ('f, 'v) rules \<times> ('f, 'v) cond_constraint_prf) list" nat nat
+
+datatype (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
+datatype (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \<times> 'q) list"
+datatype (discs_sels) 'q ta_relation =
+ Decision_Proc
+ | Id_Relation
+ | Some_Relation "('q \<times> 'q) list"
+
+datatype (discs_sels) boundstype = Roof | Match
+datatype (discs_sels) ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
+
+datatype (discs_sels) ('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 (discs_sels) pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
+
+datatype (discs_sels) ('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 \<times> ('f, 'v) rseq" pat_rule_pos 'v
+ | Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat
+
+datatype (discs_sels) ('f, 'v) non_loop_prf =
+ Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos
+
+datatype (discs_sels) ('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 (discs_sels) ('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 (discs_sels) ('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 \<Rightarrow> bool" where
+ "satisfied (SN_TRS t) = (t = t)"
+| "satisfied (SN_FP_TRS t) = (t \<noteq> t)"
+| "satisfied (Finite_DPP d) = (d \<noteq> 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 \<Rightarrow> ('f, 'l, 'v) assm list)
+ \<Rightarrow> ('dpp \<Rightarrow> ('f, 'l, 'v) assm list)
+ \<Rightarrow> ('fptp \<Rightarrow> ('f, 'l, 'v) assm list)
+ \<Rightarrow> ('unk \<Rightarrow> ('f, 'l, 'v) assm list)
+ \<Rightarrow> ('f, 'l, 'v, 'tp, 'dpp, 'fptp, 'unk) assm_proof \<Rightarrow> ('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 \<Rightarrow> ('f, 'l, 'v) assm list)
+ \<Rightarrow> ('dpp \<Rightarrow> ('f, 'l, 'v) assm list)
+ \<Rightarrow> ('rtp \<Rightarrow> ('f, 'l, 'v) assm list)
+ \<Rightarrow> ('fptp \<Rightarrow> ('f, 'l, 'v) assm list)
+ \<Rightarrow> ('unk \<Rightarrow> ('f, 'l, 'v) assm list)
+ \<Rightarrow> ('f, 'l, 'v, 'tp, 'dpp, 'rtp, 'fptp, 'unk) generic_assm_proof \<Rightarrow> ('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 (discs_sels) ('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 (discs_sels) ('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 \<times> ('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 \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
+ | Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option"
+ "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy Sat Feb 13 12:13:10 2016 +0100
@@ -0,0 +1,471 @@
+(* Title: Benchmarks/Datatype_Benchmark/Misc_N2M.thy
+ Author: Dmitriy Traytel, TU Muenchen
+ Copyright 2014
+
+Miscellaneous tests for the nested-to-mutual reduction.
+*)
+
+section \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close>
+
+theory Misc_N2M
+imports "~~/src/HOL/Library/BNF_Axiomatization"
+begin
+
+declare [[typedef_overloaded]]
+
+
+locale misc
+begin
+
+datatype 'a li = Ni | Co 'a "'a li"
+datatype 'a tr = Tr "'a \<Rightarrow> 'a tr li"
+
+primrec (nonexhaustive)
+ f_tl :: "'a \<Rightarrow> 'a tr li \<Rightarrow> nat" and
+ f_t :: "'a \<Rightarrow> 'a tr \<Rightarrow> nat"
+where
+ "f_tl _ Ni = 0" |
+ "f_t a (Tr ts) = 1 + f_tl a (ts a)"
+
+datatype ('a, 'b) l = N | C 'a 'b "('a, 'b) l"
+datatype ('a, 'b) t = T "(('a, 'b) t, 'a) l" "(('a, 'b) t, 'b) l"
+
+primrec (nonexhaustive)
+ f_tl2 :: "(('a, 'a) t, 'a) l \<Rightarrow> nat" and
+ f_t2 :: "('a, 'a) t \<Rightarrow> nat"
+where
+ "f_tl2 N = 0" |
+ "f_t2 (T ts us) = f_tl2 ts + f_tl2 us"
+
+primrec (nonexhaustive)
+ g_tla :: "(('a, 'b) t, 'a) l \<Rightarrow> nat" and
+ g_tlb :: "(('a, 'b) t, 'b) l \<Rightarrow> nat" and
+ g_t :: "('a, 'b) t \<Rightarrow> nat"
+where
+ "g_tla N = 0" |
+ "g_tlb N = 1" |
+ "g_t (T ts us) = g_tla ts + g_tlb us"
+
+
+datatype
+ 'a l1 = N1 | C1 'a "'a l1"
+
+datatype
+ ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" "(nat \<times> ('a, 'b) t1) l1" and
+ ('a, 'b) t2 = T2 "('a, 'b) t1"
+
+primrec
+ h1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
+ h1_natl1 :: "(nat \<times> (nat, 'a) t1) l1 \<Rightarrow> nat" and
+ h1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
+where
+ "h1_tl1 N1 = 0" |
+ "h1_tl1 (C1 t ts) = h1_t1 t + h1_tl1 ts" |
+ "h1_natl1 N1 = Suc 0" |
+ "h1_natl1 (C1 n ts) = fst n + h1_natl1 ts" |
+ "h1_t1 (T1 n _ ts _) = n + h1_tl1 ts"
+
+end
+
+
+bnf_axiomatization ('a, 'b) M0 [wits: "('a, 'b) M0"]
+bnf_axiomatization ('a, 'b) N0 [wits: "('a, 'b) N0"]
+bnf_axiomatization ('a, 'b) K0 [wits: "('a, 'b) K0"]
+bnf_axiomatization ('a, 'b) L0 [wits: "('a, 'b) L0"]
+bnf_axiomatization ('a, 'b, 'c) G0 [wits: "('a, 'b, 'c) G0"]
+
+locale (*co*)mplicated
+begin
+
+datatype 'a M = CM "('a, 'a M) M0"
+datatype 'a N = CN "('a N, 'a) N0"
+datatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0"
+ and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
+datatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0"
+
+primrec
+ fG :: "'a G \<Rightarrow> 'a G"
+and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K"
+and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L"
+and fM :: "'a G M \<Rightarrow> 'a G M" where
+ "fG (CG x) = CG (map_G0 id fK (map_L fM fG) x)"
+| "fK (CK y) = CK (map_K0 fG fL y)"
+| "fL (CL z) = CL (map_L0 (map_N fG) fK z)"
+| "fM (CM w) = CM (map_M0 fG fM w)"
+thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps
+
+end
+
+locale complicated
+begin
+
+codatatype 'a M = CM "('a, 'a M) M0"
+codatatype 'a N = CN "('a N, 'a) N0"
+codatatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0"
+ and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
+codatatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0"
+
+primcorec
+ fG :: "'a G \<Rightarrow> 'a G"
+and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K"
+and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L"
+and fM :: "'a G M \<Rightarrow> 'a G M" where
+ "fG x = CG (map_G0 id fK (map_L fM fG) (un_CG x))"
+| "fK y = CK (map_K0 fG fL (un_CK y))"
+| "fL z = CL (map_L0 (map_N fG) fK (un_CL z))"
+| "fM w = CM (map_M0 fG fM (un_CM w))"
+thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps
+
+end
+
+datatype ('a, 'b) F1 = F1 'a 'b
+datatype F2 = F2 "((unit, nat) F1, F2) F1" | F2'
+datatype 'a kk1 = K1 'a | K2 "'a kk2" and 'a kk2 = K3 "'a kk1"
+datatype 'a ll1 = L1 'a | L2 "'a ll2 kk2" and 'a ll2 = L3 "'a ll1"
+
+datatype_compat F1
+datatype_compat F2
+datatype_compat kk1 kk2
+datatype_compat ll1 ll2
+
+
+subsection \<open>Deep Nesting\<close>
+
+datatype 'a tree = Empty | Node 'a "'a tree list"
+datatype_compat tree
+
+datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
+datatype_compat ttree
+
+datatype 'a tttree = TEmpty | TNode 'a "'a tttree list ttree list tree"
+datatype_compat tttree
+(*
+datatype 'a ttttree = TEmpty | TNode 'a "'a ttttree list tttree list ttree list tree"
+datatype_compat ttttree
+*)
+
+datatype ('a,'b)complex =
+ C1 nat "'a ttree"
+| C2 "('a,'b)complex list tree tree" 'b "('a,'b)complex" "('a,'b)complex2 ttree list"
+and ('a,'b)complex2 = D1 "('a,'b)complex ttree"
+datatype_compat complex complex2
+
+datatype 'a F = F1 'a | F2 "'a F"
+datatype 'a G = G1 'a | G2 "'a G F"
+datatype H = H1 | H2 "H G"
+
+datatype_compat F
+datatype_compat G
+datatype_compat H
+
+
+subsection \<open>Primrec cache\<close>
+
+datatype 'a l = N | C 'a "'a l"
+datatype ('a, 'b) t = T 'a 'b "('a, 'b) t l"
+
+context linorder
+begin
+
+(* slow *)
+primrec
+ f1_tl :: "(nat, 'a) t l \<Rightarrow> nat" and
+ f1_t :: "(nat, 'a) t \<Rightarrow> nat"
+where
+ "f1_tl N = 0" |
+ "f1_tl (C t ts) = f1_t t + f1_tl ts" |
+ "f1_t (T n _ ts) = n + f1_tl ts"
+
+(* should be fast *)
+primrec
+ f2_t :: "(nat, 'b) t \<Rightarrow> nat" and
+ f2_tl :: "(nat, 'b) t l \<Rightarrow> nat"
+where
+ "f2_tl N = 0" |
+ "f2_tl (C t ts) = f2_t t + f2_tl ts" |
+ "f2_t (T n _ ts) = n + f2_tl ts"
+
+end
+
+(* should be fast *)
+primrec
+ g1_t :: "('a, int) t \<Rightarrow> nat" and
+ g1_tl :: "('a, int) t l \<Rightarrow> nat"
+where
+ "g1_t (T _ _ ts) = g1_tl ts" |
+ "g1_tl N = 0" |
+ "g1_tl (C _ ts) = g1_tl ts"
+
+(* should be fast *)
+primrec
+ g2_t :: "(int, int) t \<Rightarrow> nat" and
+ g2_tl :: "(int, int) t l \<Rightarrow> nat"
+where
+ "g2_t (T _ _ ts) = g2_tl ts" |
+ "g2_tl N = 0" |
+ "g2_tl (C _ ts) = g2_tl ts"
+
+
+datatype
+ 'a l1 = N1 | C1 'a "'a l2" and
+ 'a l2 = N2 | C2 'a "'a l1"
+
+primrec
+ sum_l1 :: "'a::{zero,plus} l1 \<Rightarrow> 'a" and
+ sum_l2 :: "'a::{zero,plus} l2 \<Rightarrow> 'a"
+where
+ "sum_l1 N1 = 0" |
+ "sum_l1 (C1 n ns) = n + sum_l2 ns" |
+ "sum_l2 N2 = 0" |
+ "sum_l2 (C2 n ns) = n + sum_l1 ns"
+
+datatype
+ ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" and
+ ('a, 'b) t2 = T2 "('a, 'b) t1"
+
+(* slow *)
+primrec
+ h1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
+ h1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
+ h1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
+where
+ "h1_tl1 N1 = 0" |
+ "h1_tl1 (C1 t ts) = h1_t1 t + h1_tl2 ts" |
+ "h1_tl2 N2 = 0" |
+ "h1_tl2 (C2 t ts) = h1_t1 t + h1_tl1 ts" |
+ "h1_t1 (T1 n _ ts) = n + h1_tl1 ts"
+
+(* should be fast *)
+primrec
+ h2_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
+ h2_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
+ h2_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
+where
+ "h2_tl1 N1 = 0" |
+ "h2_tl1 (C1 t ts) = h2_t1 t + h2_tl2 ts" |
+ "h2_tl2 N2 = 0" |
+ "h2_tl2 (C2 t ts) = h2_t1 t + h2_tl1 ts" |
+ "h2_t1 (T1 n _ ts) = n + h2_tl1 ts"
+
+(* should be fast *)
+primrec
+ h3_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
+ h3_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
+ h3_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
+where
+ "h3_tl1 N1 = 0" |
+ "h3_tl1 (C1 t ts) = h3_t1 t + h3_tl2 ts" |
+ "h3_tl2 N2 = 0" |
+ "h3_tl2 (C2 t ts) = h3_t1 t + h3_tl1 ts" |
+ "h3_t1 (T1 n _ ts) = n + h3_tl1 ts"
+
+(* should be fast *)
+primrec
+ i1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
+ i1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
+ i1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" and
+ i1_t2 :: "(nat, 'a) t2 \<Rightarrow> nat"
+where
+ "i1_tl1 N1 = 0" |
+ "i1_tl1 (C1 t ts) = i1_t1 t + i1_tl2 ts" |
+ "i1_tl2 N2 = 0" |
+ "i1_tl2 (C2 t ts) = i1_t1 t + i1_tl1 ts" |
+ "i1_t1 (T1 n _ ts) = n + i1_tl1 ts" |
+ "i1_t2 (T2 t) = i1_t1 t"
+
+(* should be fast *)
+primrec
+ j1_t2 :: "(nat, 'a) t2 \<Rightarrow> nat" and
+ j1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" and
+ j1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
+ j1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat"
+where
+ "j1_tl1 N1 = 0" |
+ "j1_tl1 (C1 t ts) = j1_t1 t + j1_tl2 ts" |
+ "j1_tl2 N2 = 0" |
+ "j1_tl2 (C2 t ts) = j1_t1 t + j1_tl1 ts" |
+ "j1_t1 (T1 n _ ts) = n + j1_tl1 ts" |
+ "j1_t2 (T2 t) = j1_t1 t"
+
+
+datatype 'a l3 = N3 | C3 'a "'a l3"
+datatype 'a l4 = N4 | C4 'a "'a l4"
+datatype ('a, 'b) t3 = T3 'a 'b "('a, 'b) t3 l3" "('a, 'b) t3 l4"
+
+(* slow *)
+primrec
+ k1_tl3 :: "(nat, 'a) t3 l3 \<Rightarrow> nat" and
+ k1_tl4 :: "(nat, 'a) t3 l4 \<Rightarrow> nat" and
+ k1_t3 :: "(nat, 'a) t3 \<Rightarrow> nat"
+where
+ "k1_tl3 N3 = 0" |
+ "k1_tl3 (C3 t ts) = k1_t3 t + k1_tl3 ts" |
+ "k1_tl4 N4 = 0" |
+ "k1_tl4 (C4 t ts) = k1_t3 t + k1_tl4 ts" |
+ "k1_t3 (T3 n _ ts us) = n + k1_tl3 ts + k1_tl4 us"
+
+(* should be fast *)
+primrec
+ k2_tl4 :: "(nat, int) t3 l4 \<Rightarrow> nat" and
+ k2_tl3 :: "(nat, int) t3 l3 \<Rightarrow> nat" and
+ k2_t3 :: "(nat, int) t3 \<Rightarrow> nat"
+where
+ "k2_tl4 N4 = 0" |
+ "k2_tl4 (C4 t ts) = k2_t3 t + k2_tl4 ts" |
+ "k2_tl3 N3 = 0" |
+ "k2_tl3 (C3 t ts) = k2_t3 t + k2_tl3 ts" |
+ "k2_t3 (T3 n _ ts us) = n + k2_tl3 ts + k2_tl4 us"
+
+
+datatype ('a, 'b) l5 = N5 | C5 'a 'b "('a, 'b) l5"
+datatype ('a, 'b) l6 = N6 | C6 'a 'b "('a, 'b) l6"
+datatype ('a, 'b, 'c) t4 = T4 'a 'b "(('a, 'b, 'c) t4, 'b) l5" "(('a, 'b, 'c) t4, 'c) l6"
+
+(* slow *)
+primrec
+ l1_tl5 :: "((nat, 'a, 'b) t4, 'a) l5 \<Rightarrow> nat" and
+ l1_tl6 :: "((nat, 'a, 'b) t4, 'b) l6 \<Rightarrow> nat" and
+ l1_t4 :: "(nat, 'a, 'b) t4 \<Rightarrow> nat"
+where
+ "l1_tl5 N5 = 0" |
+ "l1_tl5 (C5 t _ ts) = l1_t4 t + l1_tl5 ts" |
+ "l1_tl6 N6 = 0" |
+ "l1_tl6 (C6 t _ ts) = l1_t4 t + l1_tl6 ts" |
+ "l1_t4 (T4 n _ ts us) = n + l1_tl5 ts + l1_tl6 us"
+
+
+subsection \<open>Primcorec Cache\<close>
+
+codatatype 'a col = N | C 'a "'a col"
+codatatype ('a, 'b) cot = T 'a 'b "('a, 'b) cot col"
+
+context linorder
+begin
+
+(* slow *)
+primcorec
+ f1_cotcol :: "nat \<Rightarrow> (nat, 'a) cot col" and
+ f1_cot :: "nat \<Rightarrow> (nat, 'a) cot"
+where
+ "n = 0 \<Longrightarrow> f1_cotcol n = N" |
+ "_ \<Longrightarrow> f1_cotcol n = C (f1_cot n) (f1_cotcol n)" |
+ "f1_cot n = T n undefined (f1_cotcol n)"
+
+(* should be fast *)
+primcorec
+ f2_cotcol :: "nat \<Rightarrow> (nat, 'b) cot col" and
+ f2_cot :: "nat \<Rightarrow> (nat, 'b) cot"
+where
+ "n = 0 \<Longrightarrow> f2_cotcol n = N" |
+ "_ \<Longrightarrow> f2_cotcol n = C (f2_cot n) (f2_cotcol n)" |
+ "f2_cot n = T n undefined (f2_cotcol n)"
+
+end
+
+(* should be fast *)
+primcorec
+ g1_cot :: "int \<Rightarrow> (int, 'a) cot" and
+ g1_cotcol :: "int \<Rightarrow> (int, 'a) cot col"
+where
+ "g1_cot n = T n undefined (g1_cotcol n)" |
+ "n = 0 \<Longrightarrow> g1_cotcol n = N" |
+ "_ \<Longrightarrow> g1_cotcol n = C (g1_cot n) (g1_cotcol n)"
+
+(* should be fast *)
+primcorec
+ g2_cot :: "int \<Rightarrow> (int, int) cot" and
+ g2_cotcol :: "int \<Rightarrow> (int, int) cot col"
+where
+ "g2_cot n = T n undefined (g2_cotcol n)" |
+ "n = 0 \<Longrightarrow> g2_cotcol n = N" |
+ "_ \<Longrightarrow> g2_cotcol n = C (g2_cot n) (g2_cotcol n)"
+
+
+codatatype
+ 'a col1 = N1 | C1 'a "'a col2" and
+ 'a col2 = N2 | C2 'a "'a col1"
+
+codatatype
+ ('a, 'b) cot1 = T1 'a 'b "('a, 'b) cot1 col1" and
+ ('a, 'b) cot2 = T2 "('a, 'b) cot1"
+
+(* slow *)
+primcorec
+ h1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
+ h1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
+ h1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
+where
+ "h1_cotcol1 n = C1 (h1_cot1 n) (h1_cotcol2 n)" |
+ "h1_cotcol2 n = C2 (h1_cot1 n) (h1_cotcol1 n)" |
+ "h1_cot1 n = T1 n undefined (h1_cotcol1 n)"
+
+(* should be fast *)
+primcorec
+ h2_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
+ h2_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
+ h2_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
+where
+ "h2_cotcol1 n = C1 (h2_cot1 n) (h2_cotcol2 n)" |
+ "h2_cotcol2 n = C2 (h2_cot1 n) (h2_cotcol1 n)" |
+ "h2_cot1 n = T1 n undefined (h2_cotcol1 n)"
+
+(* should be fast *)
+primcorec
+ h3_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
+ h3_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
+ h3_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
+where
+ "h3_cotcol1 n = C1 (h3_cot1 n) (h3_cotcol2 n)" |
+ "h3_cotcol2 n = C2 (h3_cot1 n) (h3_cotcol1 n)" |
+ "h3_cot1 n = T1 n undefined (h3_cotcol1 n)"
+
+(* should be fast *)
+primcorec
+ i1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
+ i1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
+ i1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" and
+ i1_cot2 :: "nat \<Rightarrow> (nat, 'a) cot2"
+where
+ "i1_cotcol1 n = C1 (i1_cot1 n) (i1_cotcol2 n)" |
+ "i1_cotcol2 n = C2 (i1_cot1 n) (i1_cotcol1 n)" |
+ "i1_cot1 n = T1 n undefined (i1_cotcol1 n)" |
+ "i1_cot2 n = T2 (i1_cot1 n)"
+
+(* should be fast *)
+primcorec
+ j1_cot2 :: "nat \<Rightarrow> (nat, 'a) cot2" and
+ j1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" and
+ j1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
+ j1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2"
+where
+ "j1_cotcol1 n = C1 (j1_cot1 n) (j1_cotcol2 n)" |
+ "j1_cotcol2 n = C2 (j1_cot1 n) (j1_cotcol1 n)" |
+ "j1_cot1 n = T1 n undefined (j1_cotcol1 n)" |
+ "j1_cot2 n = T2 (j1_cot1 n)"
+
+
+codatatype 'a col3 = N3 | C3 'a "'a col3"
+codatatype 'a col4 = N4 | C4 'a "'a col4"
+codatatype ('a, 'b) cot3 = T3 'a 'b "('a, 'b) cot3 col3" "('a, 'b) cot3 col4"
+
+(* slow *)
+primcorec
+ k1_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and
+ k1_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and
+ k1_cot3 :: "nat \<Rightarrow> (nat, 'a) cot3"
+where
+ "k1_cotcol3 n = C3 (k1_cot3 n) (k1_cotcol3 n)" |
+ "k1_cotcol4 n = C4 (k1_cot3 n) (k1_cotcol4 n)" |
+ "k1_cot3 n = T3 n undefined (k1_cotcol3 n) (k1_cotcol4 n)"
+
+(* should be fast *)
+primcorec
+ k2_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and
+ k2_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and
+ k2_cot3 :: "nat \<Rightarrow> (nat, 'a) cot3"
+where
+ "k2_cotcol4 n = C4 (k2_cot3 n) (k2_cotcol4 n)" |
+ "k2_cotcol3 n = C3 (k2_cot3 n) (k2_cotcol3 n)" |
+ "k2_cot3 n = T3 n undefined (k2_cotcol3 n) (k2_cotcol4 n)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy Sat Feb 13 12:13:10 2016 +0100
@@ -0,0 +1,27 @@
+theory Find_Unused_Assms_Examples
+imports Complex_Main
+begin
+
+section {* Arithmetics *}
+
+declare [[quickcheck_finite_types = false]]
+
+find_unused_assms Divides
+find_unused_assms GCD
+find_unused_assms Real
+
+section {* Set Theory *}
+
+declare [[quickcheck_finite_types = true]]
+
+find_unused_assms Fun
+find_unused_assms Relation
+find_unused_assms Set
+find_unused_assms Wellfounded
+
+section {* Datatypes *}
+
+find_unused_assms List
+find_unused_assms Map
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Sat Feb 13 12:13:10 2016 +0100
@@ -0,0 +1,196 @@
+theory Needham_Schroeder_Base
+imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
+begin
+
+datatype agent = Alice | Bob | Spy
+
+definition agents :: "agent set"
+where
+ "agents = {Spy, Alice, Bob}"
+
+definition bad :: "agent set"
+where
+ "bad = {Spy}"
+
+datatype key = pubEK agent | priEK agent
+
+fun invKey
+where
+ "invKey (pubEK A) = priEK A"
+| "invKey (priEK A) = pubEK A"
+
+datatype
+ msg = Agent agent
+ | Key key
+ | Nonce nat
+ | MPair msg msg
+ | Crypt key msg
+
+syntax
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+translations
+ "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+ "\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
+
+inductive_set
+ parts :: "msg set => msg set"
+ for H :: "msg set"
+ where
+ Inj [intro]: "X \<in> H ==> X \<in> parts H"
+ | Fst: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> X \<in> parts H"
+ | Snd: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> Y \<in> parts H"
+ | Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
+
+inductive_set
+ analz :: "msg set => msg set"
+ for H :: "msg set"
+ where
+ Inj [intro,simp] : "X \<in> H ==> X \<in> analz H"
+ | Fst: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H"
+ | Snd: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H"
+ | Decrypt [dest]:
+ "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
+
+inductive_set
+ synth :: "msg set => msg set"
+ for H :: "msg set"
+ where
+ Inj [intro]: "X \<in> H ==> X \<in> synth H"
+ | Agent [intro]: "Agent agt \<in> synth H"
+ | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
+ | Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
+
+primrec initState
+where
+ initState_Alice:
+ "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)"
+| initState_Bob:
+ "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)"
+| initState_Spy:
+ "initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
+
+datatype
+ event = Says agent agent msg
+ | Gets agent msg
+ | Notes agent msg
+
+
+primrec knows :: "agent => event list => msg set"
+where
+ knows_Nil: "knows A [] = initState A"
+| knows_Cons:
+ "knows A (ev # evs) =
+ (if A = Spy then
+ (case ev of
+ Says A' B X => insert X (knows Spy evs)
+ | Gets A' X => knows Spy evs
+ | Notes A' X =>
+ if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
+ else
+ (case ev of
+ Says A' B X =>
+ if A'=A then insert X (knows A evs) else knows A evs
+ | Gets A' X =>
+ if A'=A then insert X (knows A evs) else knows A evs
+ | Notes A' X =>
+ if A'=A then insert X (knows A evs) else knows A evs))"
+
+abbreviation (input)
+ spies :: "event list => msg set" where
+ "spies == knows Spy"
+
+primrec used :: "event list => msg set"
+where
+ used_Nil: "used [] = \<Union>(parts ` initState ` agents)"
+| used_Cons: "used (ev # evs) =
+ (case ev of
+ Says A B X => parts {X} \<union> used evs
+ | Gets A X => used evs
+ | Notes A X => parts {X} \<union> used evs)"
+
+subsection {* Preparations for sets *}
+
+fun find_first :: "('a => 'b option) => 'a list => 'b option"
+where
+ "find_first f [] = None"
+| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
+
+consts cps_of_set :: "'a set => ('a => term list option) => term list option"
+
+lemma
+ [code]: "cps_of_set (set xs) f = find_first f xs"
+sorry
+
+consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
+consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
+
+lemma
+ [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
+sorry
+
+consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
+ => 'b list => 'a Quickcheck_Exhaustive.three_valued"
+
+lemma [code]:
+ "find_first' f [] = Quickcheck_Exhaustive.No_value"
+ "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
+sorry
+
+lemma
+ [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
+sorry
+
+setup {*
+let
+ val Fun = Predicate_Compile_Aux.Fun
+ val Input = Predicate_Compile_Aux.Input
+ val Output = Predicate_Compile_Aux.Output
+ val Bool = Predicate_Compile_Aux.Bool
+ val oi = Fun (Output, Fun (Input, Bool))
+ val ii = Fun (Input, Fun (Input, Bool))
+ fun of_set compfuns (Type ("fun", [T, _])) =
+ case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
+ Type ("Quickcheck_Exhaustive.three_valued", _) =>
+ Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
+ | Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T)
+ | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
+ fun member compfuns (U as Type ("fun", [T, _])) =
+ (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
+ (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0))))
+
+in
+ Core_Data.force_modes_and_compilations @{const_name Set.member}
+ [(oi, (of_set, false)), (ii, (member, false))]
+end
+*}
+
+subsection {* Derived equations for analz, parts and synth *}
+
+lemma [code]:
+ "analz H = (let
+ H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
+ in if H' = H then H else analz H')"
+sorry
+
+lemma [code]:
+ "parts H = (let
+ H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
+ in if H' = H then H else parts H')"
+sorry
+
+definition synth' :: "msg set => msg => bool"
+where
+ "synth' H m = (m : synth H)"
+
+lemmas [code_pred_intro] = synth.intros[folded synth'_def]
+
+code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
+declare ListMem_iff[symmetric, code_pred_inline]
+declare [[quickcheck_timing]]
+
+setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
+declare [[quickcheck_full_support = false]]
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy Sat Feb 13 12:13:10 2016 +0100
@@ -0,0 +1,100 @@
+theory Needham_Schroeder_Guided_Attacker_Example
+imports Needham_Schroeder_Base
+begin
+
+inductive_set ns_public :: "event list set"
+ where
+ (*Initial trace is empty*)
+ Nil: "[] \<in> ns_public"
+
+ | Fake_NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1) \<rbrakk>
+ \<Longrightarrow> Says Spy B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ # evs1 \<in> ns_public"
+ | Fake_NS2: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1); Nonce NB \<in> analz (spies evs1) \<rbrakk>
+ \<Longrightarrow> Says Spy A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+ # evs1 \<in> ns_public"
+
+ (*Alice initiates a protocol run, sending a nonce to Bob*)
+ | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ # evs1 \<in> ns_public"
+ (*Bob responds to Alice's message with a further nonce*)
+ | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
+ Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+ # evs2 \<in> ns_public"
+
+ (*Alice proves her existence by sending NB back to Bob.*)
+ | NS3: "\<lbrakk>evs3 \<in> ns_public;
+ Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
+
+declare ListMem_iff[symmetric, code_pred_inline]
+
+lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
+
+code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
+thm ns_publicp.equation
+
+code_pred [generator_cps] ns_publicp .
+thm ns_publicp.generator_cps_equation
+
+
+lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
+quickcheck[smart_exhaustive, depth = 5, timeout = 100, expect = counterexample]
+(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
+oops
+
+lemma
+ "\<lbrakk>ns_publicp evs\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
+ \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
+ \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
+(*quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = counterexample]
+quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
+oops
+
+section {* Proving the counterexample trace for validation *}
+
+lemma
+ assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
+ assumes "evs =
+ [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
+ Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>),
+ Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>),
+ Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>)]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
+ shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
+proof -
+ from assms show "A \<noteq> Spy" by auto
+ from assms show "B \<noteq> Spy" by auto
+ have "[] : ns_public" by (rule Nil)
+ then have first_step: "[?e0] : ns_public"
+ proof (rule NS1)
+ show "Nonce 0 ~: used []" by eval
+ qed
+ then have "[?e1, ?e0] : ns_public"
+ proof (rule Fake_NS1)
+ show "Nonce 0 : analz (knows Spy [?e0])" by eval
+ qed
+ then have "[?e2, ?e1, ?e0] : ns_public"
+ proof (rule NS2)
+ show "Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e1, ?e0]" by simp
+ show " Nonce 1 ~: used [?e1, ?e0]" by eval
+ qed
+ then show "evs : ns_public"
+ unfolding assms
+ proof (rule NS3)
+ show " Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e2, ?e1, ?e0]" by simp
+ show "Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>)
+ : set [?e2, ?e1, ?e0]" by simp
+ qed
+ from assms show "Nonce NB : analz (knows Spy evs)"
+ apply simp
+ apply (rule analz.intros(4))
+ apply (rule analz.intros(1))
+ apply (auto simp add: bad_def)
+ done
+qed
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy Sat Feb 13 12:13:10 2016 +0100
@@ -0,0 +1,47 @@
+theory Needham_Schroeder_No_Attacker_Example
+imports Needham_Schroeder_Base
+begin
+
+inductive_set ns_public :: "event list set"
+ where
+ (*Initial trace is empty*)
+ Nil: "[] \<in> ns_public"
+ (*Alice initiates a protocol run, sending a nonce to Bob*)
+ | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ # evs1 \<in> ns_public"
+ (*Bob responds to Alice's message with a further nonce*)
+ | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
+ Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+ # evs2 \<in> ns_public"
+
+ (*Alice proves her existence by sending NB back to Bob.*)
+ | NS3: "\<lbrakk>evs3 \<in> ns_public;
+ Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
+
+code_pred [skip_proof] ns_publicp .
+thm ns_publicp.equation
+
+code_pred [generator_cps] ns_publicp .
+thm ns_publicp.generator_cps_equation
+
+lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
+(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose]
+quickcheck[exhaustive, size = 8, timeout = 3600, verbose]
+quickcheck[narrowing, size = 7, timeout = 3600, verbose]*)
+quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample]
+oops
+
+lemma
+ "\<lbrakk>ns_publicp evs\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
+ \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
+ \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
+quickcheck[smart_exhaustive, depth = 6, timeout = 30]
+quickcheck[narrowing, size = 6, timeout = 30, verbose]
+oops
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy Sat Feb 13 12:13:10 2016 +0100
@@ -0,0 +1,96 @@
+theory Needham_Schroeder_Unguided_Attacker_Example
+imports Needham_Schroeder_Base
+begin
+
+inductive_set ns_public :: "event list set"
+ where
+ (*Initial trace is empty*)
+ Nil: "[] \<in> ns_public"
+
+ | Fake: "\<lbrakk>evs1 \<in> ns_public; X \<in> synth (analz (spies evs1)) \<rbrakk>
+ \<Longrightarrow> Says Spy A X # evs1 \<in> ns_public"
+
+ (*Alice initiates a protocol run, sending a nonce to Bob*)
+ | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ # evs1 \<in> ns_public"
+ (*Bob responds to Alice's message with a further nonce*)
+ | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
+ Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+ # evs2 \<in> ns_public"
+
+ (*Alice proves her existence by sending NB back to Bob.*)
+ | NS3: "\<lbrakk>evs3 \<in> ns_public;
+ Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
+
+declare ListMem_iff[symmetric, code_pred_inline]
+
+lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
+
+code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
+thm ns_publicp.equation
+
+code_pred [generator_cps] ns_publicp .
+thm ns_publicp.generator_cps_equation
+
+
+lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
+quickcheck[smart_exhaustive, depth = 5, timeout = 200, expect = counterexample]
+(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
+oops
+
+lemma
+ "\<lbrakk>ns_publicp evs\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
+ \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
+ \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
+quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample]
+(*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
+oops
+
+section {* Proving the counterexample trace for validation *}
+
+lemma
+ assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
+ assumes "evs =
+ [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
+ Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>),
+ Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>),
+ Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>)]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
+ shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
+proof -
+ from assms show "A \<noteq> Spy" by auto
+ from assms show "B \<noteq> Spy" by auto
+ have "[] : ns_public" by (rule Nil)
+ then have first_step: "[?e0] : ns_public"
+ proof (rule NS1)
+ show "Nonce 0 ~: used []" by eval
+ qed
+ then have "[?e1, ?e0] : ns_public"
+ proof (rule Fake)
+ show "Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace> : synth (analz (knows Spy [?e0]))"
+ by (intro synth.intros(2,3,4,1)) eval+
+ qed
+ then have "[?e2, ?e1, ?e0] : ns_public"
+ proof (rule NS2)
+ show "Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e1, ?e0]" by simp
+ show " Nonce 1 ~: used [?e1, ?e0]" by eval
+ qed
+ then show "evs : ns_public"
+ unfolding assms
+ proof (rule NS3)
+ show " Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e2, ?e1, ?e0]" by simp
+ show "Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>) : set [?e2, ?e1, ?e0]" by simp
+ qed
+ from assms show "Nonce NB : analz (knows Spy evs)"
+ apply simp
+ apply (rule analz.intros(4))
+ apply (rule analz.intros(1))
+ apply (auto simp add: bad_def)
+ done
+qed
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Benchmarks/ROOT Sat Feb 13 12:13:10 2016 +0100
@@ -0,0 +1,26 @@
+chapter HOL
+
+session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
+ description {*
+ Big (co)datatypes.
+ *}
+ options [document = false]
+ theories
+ Brackin
+ IsaFoR
+ Misc_N2M
+
+session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
+ theories [quick_and_dirty]
+ Find_Unused_Assms_Examples
+ Needham_Schroeder_No_Attacker_Example
+ Needham_Schroeder_Guided_Attacker_Example
+ Needham_Schroeder_Unguided_Attacker_Example
+
+session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
+ description {*
+ Big records.
+ *}
+ options [document = false]
+ theories
+ Record_Benchmark
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy Sat Feb 13 12:13:10 2016 +0100
@@ -0,0 +1,427 @@
+(* Title: Benchmarks/Record_Benchmark/Record_Benchmark.thy
+ Author: Norbert Schirmer, DFKI
+*)
+
+section {* Benchmark for large record *}
+
+theory Record_Benchmark
+imports Main
+begin
+
+declare [[record_timing]]
+
+record many_A =
+A000::nat
+A001::nat
+A002::nat
+A003::nat
+A004::nat
+A005::nat
+A006::nat
+A007::nat
+A008::nat
+A009::nat
+A010::nat
+A011::nat
+A012::nat
+A013::nat
+A014::nat
+A015::nat
+A016::nat
+A017::nat
+A018::nat
+A019::nat
+A020::nat
+A021::nat
+A022::nat
+A023::nat
+A024::nat
+A025::nat
+A026::nat
+A027::nat
+A028::nat
+A029::nat
+A030::nat
+A031::nat
+A032::nat
+A033::nat
+A034::nat
+A035::nat
+A036::nat
+A037::nat
+A038::nat
+A039::nat
+A040::nat
+A041::nat
+A042::nat
+A043::nat
+A044::nat
+A045::nat
+A046::nat
+A047::nat
+A048::nat
+A049::nat
+A050::nat
+A051::nat
+A052::nat
+A053::nat
+A054::nat
+A055::nat
+A056::nat
+A057::nat
+A058::nat
+A059::nat
+A060::nat
+A061::nat
+A062::nat
+A063::nat
+A064::nat
+A065::nat
+A066::nat
+A067::nat
+A068::nat
+A069::nat
+A070::nat
+A071::nat
+A072::nat
+A073::nat
+A074::nat
+A075::nat
+A076::nat
+A077::nat
+A078::nat
+A079::nat
+A080::nat
+A081::nat
+A082::nat
+A083::nat
+A084::nat
+A085::nat
+A086::nat
+A087::nat
+A088::nat
+A089::nat
+A090::nat
+A091::nat
+A092::nat
+A093::nat
+A094::nat
+A095::nat
+A096::nat
+A097::nat
+A098::nat
+A099::nat
+A100::nat
+A101::nat
+A102::nat
+A103::nat
+A104::nat
+A105::nat
+A106::nat
+A107::nat
+A108::nat
+A109::nat
+A110::nat
+A111::nat
+A112::nat
+A113::nat
+A114::nat
+A115::nat
+A116::nat
+A117::nat
+A118::nat
+A119::nat
+A120::nat
+A121::nat
+A122::nat
+A123::nat
+A124::nat
+A125::nat
+A126::nat
+A127::nat
+A128::nat
+A129::nat
+A130::nat
+A131::nat
+A132::nat
+A133::nat
+A134::nat
+A135::nat
+A136::nat
+A137::nat
+A138::nat
+A139::nat
+A140::nat
+A141::nat
+A142::nat
+A143::nat
+A144::nat
+A145::nat
+A146::nat
+A147::nat
+A148::nat
+A149::nat
+A150::nat
+A151::nat
+A152::nat
+A153::nat
+A154::nat
+A155::nat
+A156::nat
+A157::nat
+A158::nat
+A159::nat
+A160::nat
+A161::nat
+A162::nat
+A163::nat
+A164::nat
+A165::nat
+A166::nat
+A167::nat
+A168::nat
+A169::nat
+A170::nat
+A171::nat
+A172::nat
+A173::nat
+A174::nat
+A175::nat
+A176::nat
+A177::nat
+A178::nat
+A179::nat
+A180::nat
+A181::nat
+A182::nat
+A183::nat
+A184::nat
+A185::nat
+A186::nat
+A187::nat
+A188::nat
+A189::nat
+A190::nat
+A191::nat
+A192::nat
+A193::nat
+A194::nat
+A195::nat
+A196::nat
+A197::nat
+A198::nat
+A199::nat
+A200::nat
+A201::nat
+A202::nat
+A203::nat
+A204::nat
+A205::nat
+A206::nat
+A207::nat
+A208::nat
+A209::nat
+A210::nat
+A211::nat
+A212::nat
+A213::nat
+A214::nat
+A215::nat
+A216::nat
+A217::nat
+A218::nat
+A219::nat
+A220::nat
+A221::nat
+A222::nat
+A223::nat
+A224::nat
+A225::nat
+A226::nat
+A227::nat
+A228::nat
+A229::nat
+A230::nat
+A231::nat
+A232::nat
+A233::nat
+A234::nat
+A235::nat
+A236::nat
+A237::nat
+A238::nat
+A239::nat
+A240::nat
+A241::nat
+A242::nat
+A243::nat
+A244::nat
+A245::nat
+A246::nat
+A247::nat
+A248::nat
+A249::nat
+A250::nat
+A251::nat
+A252::nat
+A253::nat
+A254::nat
+A255::nat
+A256::nat
+A257::nat
+A258::nat
+A259::nat
+A260::nat
+A261::nat
+A262::nat
+A263::nat
+A264::nat
+A265::nat
+A266::nat
+A267::nat
+A268::nat
+A269::nat
+A270::nat
+A271::nat
+A272::nat
+A273::nat
+A274::nat
+A275::nat
+A276::nat
+A277::nat
+A278::nat
+A279::nat
+A280::nat
+A281::nat
+A282::nat
+A283::nat
+A284::nat
+A285::nat
+A286::nat
+A287::nat
+A288::nat
+A289::nat
+A290::nat
+A291::nat
+A292::nat
+A293::nat
+A294::nat
+A295::nat
+A296::nat
+A297::nat
+A298::nat
+A299::nat
+
+record many_B = many_A +
+B000::nat
+B001::nat
+B002::nat
+B003::nat
+B004::nat
+B005::nat
+B006::nat
+B007::nat
+B008::nat
+B009::nat
+B010::nat
+B011::nat
+B012::nat
+B013::nat
+B014::nat
+B015::nat
+B016::nat
+B017::nat
+B018::nat
+B019::nat
+B020::nat
+B021::nat
+B022::nat
+B023::nat
+B024::nat
+B025::nat
+B026::nat
+B027::nat
+B028::nat
+B029::nat
+B030::nat
+
+lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
+ by simp
+
+lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
+ by simp
+
+lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
+ by simp
+
+lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
+ apply (tactic {* simp_tac
+ (put_simpset HOL_basic_ss @{context} addsimprocs [Record.upd_simproc]) 1*})
+ done
+
+lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
+ apply (tactic {* simp_tac
+ (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply simp
+ done
+
+lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
+ apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+ apply simp
+ done
+
+lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* simp_tac
+ (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply simp
+ done
+
+lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+ apply simp
+ done
+
+lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* simp_tac
+ (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply auto
+ done
+
+lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+ apply auto
+ done
+
+lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+ apply auto
+ done
+
+lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+ apply auto
+ done
+
+
+notepad
+begin
+ fix P r
+ assume "P (A155 r)"
+ then have "\<exists>x. P x"
+ apply -
+ apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+ apply auto
+ done
+end
+
+
+lemma "\<exists>r. A155 r = x"
+ apply (tactic {*simp_tac
+ (put_simpset HOL_basic_ss @{context} addsimprocs [Record.ex_sel_eq_simproc]) 1*})
+ done
+
+print_record many_A
+
+print_record many_B
+
+end
\ No newline at end of file
--- a/src/HOL/Datatype_Examples/Brackin.thy Sat Feb 13 11:50:01 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(* Title: HOL/Datatype_Examples/Brackin.thy
-
-A couple of datatypes from Steve Brackin's work.
-*)
-
-theory Brackin imports Main begin
-
-datatype T =
- X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
- X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
- X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
- X32 | X33 | X34
-
-datatype ('a, 'b, 'c) TY1 =
- NoF
- | Fk 'a "('a, 'b, 'c) TY2"
-and ('a, 'b, 'c) TY2 =
- Ta bool
- | Td bool
- | Tf "('a, 'b, 'c) TY1"
- | Tk bool
- | Tp bool
- | App 'a "('a, 'b, 'c) TY1" "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY3"
- | Pair "('a, 'b, 'c) TY2" "('a, 'b, 'c) TY2"
-and ('a, 'b, 'c) TY3 =
- NoS
- | Fresh "('a, 'b, 'c) TY2"
- | Trustworthy 'a
- | PrivateKey 'a 'b 'c
- | PublicKey 'a 'b 'c
- | Conveyed 'a "('a, 'b, 'c) TY2"
- | Possesses 'a "('a, 'b, 'c) TY2"
- | Received 'a "('a, 'b, 'c) TY2"
- | Recognizes 'a "('a, 'b, 'c) TY2"
- | NeverMalFromSelf 'a 'b "('a, 'b, 'c) TY2"
- | Sends 'a "('a, 'b, 'c) TY2" 'b
- | SharedSecret 'a "('a, 'b, 'c) TY2" 'b
- | Believes 'a "('a, 'b, 'c) TY3"
- | And "('a, 'b, 'c) TY3" "('a, 'b, 'c) TY3"
-
-end
--- a/src/HOL/Datatype_Examples/IsaFoR.thy Sat Feb 13 11:50:01 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,380 +0,0 @@
-(* Title: HOL/Datatype_Examples/IsaFoR.thy
- Author: Rene Thiemann, UIBK
- Copyright 2014
-
-Benchmark consisting of datatypes defined in IsaFoR.
-*)
-
-section {* Benchmark Consisting of Datatypes Defined in IsaFoR *}
-
-theory IsaFoR
-imports Real
-begin
-
-datatype (discs_sels) ('f, 'l) lab =
- Lab "('f, 'l) lab" 'l
- | FunLab "('f, 'l) lab" "('f, 'l) lab list"
- | UnLab 'f
- | Sharp "('f, 'l) lab"
-
-datatype (discs_sels) 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
-
-datatype (discs_sels) ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
-datatype (discs_sels) ('f, 'v) ctxt =
- Hole ("\<box>")
- | More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
-
-type_synonym ('f, 'v) rule = "('f, 'v) term \<times> ('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 (discs_sels) pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
-
-type_synonym ('f, 'v) prseq = "(pos \<times> ('f, 'v) rule \<times> bool \<times> ('f, 'v) term) list"
-type_synonym ('f, 'v) rseq = "(pos \<times> ('f, 'v) rule \<times> ('f, 'v) term) list"
-
-type_synonym ('f, 'l, 'v) rseqL = "((('f, 'l) lab, 'v) rule \<times> (('f, 'l) lab, 'v) rseq) list"
-type_synonym ('f, 'l, 'v) dppLL =
- "bool \<times> bool \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL \<times>
- ('f, 'l, 'v) termsLL \<times>
- ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL"
-
-type_synonym ('f, 'l, 'v) qreltrsLL =
- "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL"
-
-type_synonym ('f, 'l, 'v) qtrsLL =
- "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL"
-
-datatype (discs_sels) location = H | A | B | R
-
-type_synonym ('f, 'v) forb_pattern = "('f, 'v) ctxt \<times> ('f, 'v) term \<times> 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 \<times> ('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 \<times> nat \<Rightarrow> ('a \<times> 'a list)"
-type_synonym ('f, 'a) lpoly_interL = "(('f \<times> nat) \<times> ('a \<times> 'a list)) list"
-
-type_synonym 'v monom = "('v \<times> nat) list"
-type_synonym ('v, 'a) poly = "('v monom \<times> 'a) list"
-type_synonym ('f, 'a) poly_inter_list = "(('f \<times> nat) \<times> (nat, 'a) poly) list"
-type_synonym 'a vec = "'a list"
-type_synonym 'a mat = "'a vec list"
-
-datatype (discs_sels) arctic = MinInfty | Num_arc int
-datatype (discs_sels) 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
-datatype (discs_sels) order_tag = Lex | Mul
-
-type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag)) list"
-
-datatype (discs_sels) af_entry =
- Collapse nat
- | AFList "nat list"
-
-type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry) list"
-type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option))) list \<times> nat"
-
-datatype (discs_sels) '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 (discs_sels) list_order_type = MS_Ext | Max_Ext | Min_Ext | Dms_Ext
-type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list"
-
-datatype (discs_sels) 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
-
-type_synonym 'f sig_map_list = "(('f \<times> nat) \<times> 'f list) list"
-type_synonym ('f, 'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f, 'v) rules \<times> ('f, 'v) rules"
-
-datatype (discs_sels) arithFun =
- Arg nat
- | Const nat
- | Sum "arithFun list"
- | Max "arithFun list"
- | Min "arithFun list"
- | Prod "arithFun list"
- | IfEqual arithFun arithFun arithFun arithFun
-
-datatype (discs_sels) 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
-datatype (discs_sels) ('f, 'v) sl_variant =
- Rootlab "('f \<times> nat) option"
- | Finitelab "'f sl_inter"
- | QuasiFinitelab "'f sl_inter" 'v
-
-type_synonym ('f, 'v) crit_pair_joins = "(('f, 'v) term \<times> ('f, 'v) rseq \<times> ('f, 'v) term \<times> ('f, 'v) rseq) list"
-
-datatype (discs_sels) '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 (discs_sels) ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
- "('f, 'v) term"
- "(('f, 'v) rule \<times> ('f, 'v) rule) list"
-
-datatype (discs_sels) ('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 \<times> ('f, 'w) term) list"
-type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL"
-
-datatype (discs_sels) ('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 \<times> (('f, 'v) term \<times> 'v list) list \<times> ('f, 'v) cond_constraint \<times> ('f, 'v) cond_constraint_prf) list"
-
-datatype (discs_sels) ('f, 'v) cond_red_pair_prf =
- Cond_Red_Pair_Prf
- 'f "(('f, 'v) cond_constraint \<times> ('f, 'v) rules \<times> ('f, 'v) cond_constraint_prf) list" nat nat
-
-datatype (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
-datatype (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \<times> 'q) list"
-datatype (discs_sels) 'q ta_relation =
- Decision_Proc
- | Id_Relation
- | Some_Relation "('q \<times> 'q) list"
-
-datatype (discs_sels) boundstype = Roof | Match
-datatype (discs_sels) ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
-
-datatype (discs_sels) ('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 (discs_sels) pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
-
-datatype (discs_sels) ('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 \<times> ('f, 'v) rseq" pat_rule_pos 'v
- | Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat
-
-datatype (discs_sels) ('f, 'v) non_loop_prf =
- Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos
-
-datatype (discs_sels) ('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 (discs_sels) ('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 (discs_sels) ('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 \<Rightarrow> bool" where
- "satisfied (SN_TRS t) = (t = t)"
-| "satisfied (SN_FP_TRS t) = (t \<noteq> t)"
-| "satisfied (Finite_DPP d) = (d \<noteq> 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 \<Rightarrow> ('f, 'l, 'v) assm list)
- \<Rightarrow> ('dpp \<Rightarrow> ('f, 'l, 'v) assm list)
- \<Rightarrow> ('fptp \<Rightarrow> ('f, 'l, 'v) assm list)
- \<Rightarrow> ('unk \<Rightarrow> ('f, 'l, 'v) assm list)
- \<Rightarrow> ('f, 'l, 'v, 'tp, 'dpp, 'fptp, 'unk) assm_proof \<Rightarrow> ('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 \<Rightarrow> ('f, 'l, 'v) assm list)
- \<Rightarrow> ('dpp \<Rightarrow> ('f, 'l, 'v) assm list)
- \<Rightarrow> ('rtp \<Rightarrow> ('f, 'l, 'v) assm list)
- \<Rightarrow> ('fptp \<Rightarrow> ('f, 'l, 'v) assm list)
- \<Rightarrow> ('unk \<Rightarrow> ('f, 'l, 'v) assm list)
- \<Rightarrow> ('f, 'l, 'v, 'tp, 'dpp, 'rtp, 'fptp, 'unk) generic_assm_proof \<Rightarrow> ('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 (discs_sels) ('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 (discs_sels) ('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 \<times> ('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 \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
- | Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option"
- "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> 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
--- a/src/HOL/Datatype_Examples/Misc_N2M.thy Sat Feb 13 11:50:01 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,471 +0,0 @@
-(* Title: HOL/Datatype_Examples/Misc_N2M.thy
- Author: Dmitriy Traytel, TU Muenchen
- Copyright 2014
-
-Miscellaneous tests for the nested-to-mutual reduction.
-*)
-
-section \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close>
-
-theory Misc_N2M
-imports "~~/src/HOL/Library/BNF_Axiomatization"
-begin
-
-declare [[typedef_overloaded]]
-
-
-locale misc
-begin
-
-datatype 'a li = Ni | Co 'a "'a li"
-datatype 'a tr = Tr "'a \<Rightarrow> 'a tr li"
-
-primrec (nonexhaustive)
- f_tl :: "'a \<Rightarrow> 'a tr li \<Rightarrow> nat" and
- f_t :: "'a \<Rightarrow> 'a tr \<Rightarrow> nat"
-where
- "f_tl _ Ni = 0" |
- "f_t a (Tr ts) = 1 + f_tl a (ts a)"
-
-datatype ('a, 'b) l = N | C 'a 'b "('a, 'b) l"
-datatype ('a, 'b) t = T "(('a, 'b) t, 'a) l" "(('a, 'b) t, 'b) l"
-
-primrec (nonexhaustive)
- f_tl2 :: "(('a, 'a) t, 'a) l \<Rightarrow> nat" and
- f_t2 :: "('a, 'a) t \<Rightarrow> nat"
-where
- "f_tl2 N = 0" |
- "f_t2 (T ts us) = f_tl2 ts + f_tl2 us"
-
-primrec (nonexhaustive)
- g_tla :: "(('a, 'b) t, 'a) l \<Rightarrow> nat" and
- g_tlb :: "(('a, 'b) t, 'b) l \<Rightarrow> nat" and
- g_t :: "('a, 'b) t \<Rightarrow> nat"
-where
- "g_tla N = 0" |
- "g_tlb N = 1" |
- "g_t (T ts us) = g_tla ts + g_tlb us"
-
-
-datatype
- 'a l1 = N1 | C1 'a "'a l1"
-
-datatype
- ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" "(nat \<times> ('a, 'b) t1) l1" and
- ('a, 'b) t2 = T2 "('a, 'b) t1"
-
-primrec
- h1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
- h1_natl1 :: "(nat \<times> (nat, 'a) t1) l1 \<Rightarrow> nat" and
- h1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
-where
- "h1_tl1 N1 = 0" |
- "h1_tl1 (C1 t ts) = h1_t1 t + h1_tl1 ts" |
- "h1_natl1 N1 = Suc 0" |
- "h1_natl1 (C1 n ts) = fst n + h1_natl1 ts" |
- "h1_t1 (T1 n _ ts _) = n + h1_tl1 ts"
-
-end
-
-
-bnf_axiomatization ('a, 'b) M0 [wits: "('a, 'b) M0"]
-bnf_axiomatization ('a, 'b) N0 [wits: "('a, 'b) N0"]
-bnf_axiomatization ('a, 'b) K0 [wits: "('a, 'b) K0"]
-bnf_axiomatization ('a, 'b) L0 [wits: "('a, 'b) L0"]
-bnf_axiomatization ('a, 'b, 'c) G0 [wits: "('a, 'b, 'c) G0"]
-
-locale (*co*)mplicated
-begin
-
-datatype 'a M = CM "('a, 'a M) M0"
-datatype 'a N = CN "('a N, 'a) N0"
-datatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0"
- and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
-datatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0"
-
-primrec
- fG :: "'a G \<Rightarrow> 'a G"
-and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K"
-and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L"
-and fM :: "'a G M \<Rightarrow> 'a G M" where
- "fG (CG x) = CG (map_G0 id fK (map_L fM fG) x)"
-| "fK (CK y) = CK (map_K0 fG fL y)"
-| "fL (CL z) = CL (map_L0 (map_N fG) fK z)"
-| "fM (CM w) = CM (map_M0 fG fM w)"
-thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps
-
-end
-
-locale complicated
-begin
-
-codatatype 'a M = CM "('a, 'a M) M0"
-codatatype 'a N = CN "('a N, 'a) N0"
-codatatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0"
- and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
-codatatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0"
-
-primcorec
- fG :: "'a G \<Rightarrow> 'a G"
-and fK :: "('a G, 'a G N) K \<Rightarrow> ('a G, 'a G N) K"
-and fL :: "('a G, 'a G N) L \<Rightarrow> ('a G, 'a G N) L"
-and fM :: "'a G M \<Rightarrow> 'a G M" where
- "fG x = CG (map_G0 id fK (map_L fM fG) (un_CG x))"
-| "fK y = CK (map_K0 fG fL (un_CK y))"
-| "fL z = CL (map_L0 (map_N fG) fK (un_CL z))"
-| "fM w = CM (map_M0 fG fM (un_CM w))"
-thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps
-
-end
-
-datatype ('a, 'b) F1 = F1 'a 'b
-datatype F2 = F2 "((unit, nat) F1, F2) F1" | F2'
-datatype 'a kk1 = K1 'a | K2 "'a kk2" and 'a kk2 = K3 "'a kk1"
-datatype 'a ll1 = L1 'a | L2 "'a ll2 kk2" and 'a ll2 = L3 "'a ll1"
-
-datatype_compat F1
-datatype_compat F2
-datatype_compat kk1 kk2
-datatype_compat ll1 ll2
-
-
-subsection \<open>Deep Nesting\<close>
-
-datatype 'a tree = Empty | Node 'a "'a tree list"
-datatype_compat tree
-
-datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
-datatype_compat ttree
-
-datatype 'a tttree = TEmpty | TNode 'a "'a tttree list ttree list tree"
-datatype_compat tttree
-(*
-datatype 'a ttttree = TEmpty | TNode 'a "'a ttttree list tttree list ttree list tree"
-datatype_compat ttttree
-*)
-
-datatype ('a,'b)complex =
- C1 nat "'a ttree"
-| C2 "('a,'b)complex list tree tree" 'b "('a,'b)complex" "('a,'b)complex2 ttree list"
-and ('a,'b)complex2 = D1 "('a,'b)complex ttree"
-datatype_compat complex complex2
-
-datatype 'a F = F1 'a | F2 "'a F"
-datatype 'a G = G1 'a | G2 "'a G F"
-datatype H = H1 | H2 "H G"
-
-datatype_compat F
-datatype_compat G
-datatype_compat H
-
-
-subsection \<open>Primrec cache\<close>
-
-datatype 'a l = N | C 'a "'a l"
-datatype ('a, 'b) t = T 'a 'b "('a, 'b) t l"
-
-context linorder
-begin
-
-(* slow *)
-primrec
- f1_tl :: "(nat, 'a) t l \<Rightarrow> nat" and
- f1_t :: "(nat, 'a) t \<Rightarrow> nat"
-where
- "f1_tl N = 0" |
- "f1_tl (C t ts) = f1_t t + f1_tl ts" |
- "f1_t (T n _ ts) = n + f1_tl ts"
-
-(* should be fast *)
-primrec
- f2_t :: "(nat, 'b) t \<Rightarrow> nat" and
- f2_tl :: "(nat, 'b) t l \<Rightarrow> nat"
-where
- "f2_tl N = 0" |
- "f2_tl (C t ts) = f2_t t + f2_tl ts" |
- "f2_t (T n _ ts) = n + f2_tl ts"
-
-end
-
-(* should be fast *)
-primrec
- g1_t :: "('a, int) t \<Rightarrow> nat" and
- g1_tl :: "('a, int) t l \<Rightarrow> nat"
-where
- "g1_t (T _ _ ts) = g1_tl ts" |
- "g1_tl N = 0" |
- "g1_tl (C _ ts) = g1_tl ts"
-
-(* should be fast *)
-primrec
- g2_t :: "(int, int) t \<Rightarrow> nat" and
- g2_tl :: "(int, int) t l \<Rightarrow> nat"
-where
- "g2_t (T _ _ ts) = g2_tl ts" |
- "g2_tl N = 0" |
- "g2_tl (C _ ts) = g2_tl ts"
-
-
-datatype
- 'a l1 = N1 | C1 'a "'a l2" and
- 'a l2 = N2 | C2 'a "'a l1"
-
-primrec
- sum_l1 :: "'a::{zero,plus} l1 \<Rightarrow> 'a" and
- sum_l2 :: "'a::{zero,plus} l2 \<Rightarrow> 'a"
-where
- "sum_l1 N1 = 0" |
- "sum_l1 (C1 n ns) = n + sum_l2 ns" |
- "sum_l2 N2 = 0" |
- "sum_l2 (C2 n ns) = n + sum_l1 ns"
-
-datatype
- ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" and
- ('a, 'b) t2 = T2 "('a, 'b) t1"
-
-(* slow *)
-primrec
- h1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
- h1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
- h1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
-where
- "h1_tl1 N1 = 0" |
- "h1_tl1 (C1 t ts) = h1_t1 t + h1_tl2 ts" |
- "h1_tl2 N2 = 0" |
- "h1_tl2 (C2 t ts) = h1_t1 t + h1_tl1 ts" |
- "h1_t1 (T1 n _ ts) = n + h1_tl1 ts"
-
-(* should be fast *)
-primrec
- h2_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
- h2_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
- h2_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
-where
- "h2_tl1 N1 = 0" |
- "h2_tl1 (C1 t ts) = h2_t1 t + h2_tl2 ts" |
- "h2_tl2 N2 = 0" |
- "h2_tl2 (C2 t ts) = h2_t1 t + h2_tl1 ts" |
- "h2_t1 (T1 n _ ts) = n + h2_tl1 ts"
-
-(* should be fast *)
-primrec
- h3_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
- h3_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
- h3_t1 :: "(nat, 'a) t1 \<Rightarrow> nat"
-where
- "h3_tl1 N1 = 0" |
- "h3_tl1 (C1 t ts) = h3_t1 t + h3_tl2 ts" |
- "h3_tl2 N2 = 0" |
- "h3_tl2 (C2 t ts) = h3_t1 t + h3_tl1 ts" |
- "h3_t1 (T1 n _ ts) = n + h3_tl1 ts"
-
-(* should be fast *)
-primrec
- i1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat" and
- i1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
- i1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" and
- i1_t2 :: "(nat, 'a) t2 \<Rightarrow> nat"
-where
- "i1_tl1 N1 = 0" |
- "i1_tl1 (C1 t ts) = i1_t1 t + i1_tl2 ts" |
- "i1_tl2 N2 = 0" |
- "i1_tl2 (C2 t ts) = i1_t1 t + i1_tl1 ts" |
- "i1_t1 (T1 n _ ts) = n + i1_tl1 ts" |
- "i1_t2 (T2 t) = i1_t1 t"
-
-(* should be fast *)
-primrec
- j1_t2 :: "(nat, 'a) t2 \<Rightarrow> nat" and
- j1_t1 :: "(nat, 'a) t1 \<Rightarrow> nat" and
- j1_tl1 :: "(nat, 'a) t1 l1 \<Rightarrow> nat" and
- j1_tl2 :: "(nat, 'a) t1 l2 \<Rightarrow> nat"
-where
- "j1_tl1 N1 = 0" |
- "j1_tl1 (C1 t ts) = j1_t1 t + j1_tl2 ts" |
- "j1_tl2 N2 = 0" |
- "j1_tl2 (C2 t ts) = j1_t1 t + j1_tl1 ts" |
- "j1_t1 (T1 n _ ts) = n + j1_tl1 ts" |
- "j1_t2 (T2 t) = j1_t1 t"
-
-
-datatype 'a l3 = N3 | C3 'a "'a l3"
-datatype 'a l4 = N4 | C4 'a "'a l4"
-datatype ('a, 'b) t3 = T3 'a 'b "('a, 'b) t3 l3" "('a, 'b) t3 l4"
-
-(* slow *)
-primrec
- k1_tl3 :: "(nat, 'a) t3 l3 \<Rightarrow> nat" and
- k1_tl4 :: "(nat, 'a) t3 l4 \<Rightarrow> nat" and
- k1_t3 :: "(nat, 'a) t3 \<Rightarrow> nat"
-where
- "k1_tl3 N3 = 0" |
- "k1_tl3 (C3 t ts) = k1_t3 t + k1_tl3 ts" |
- "k1_tl4 N4 = 0" |
- "k1_tl4 (C4 t ts) = k1_t3 t + k1_tl4 ts" |
- "k1_t3 (T3 n _ ts us) = n + k1_tl3 ts + k1_tl4 us"
-
-(* should be fast *)
-primrec
- k2_tl4 :: "(nat, int) t3 l4 \<Rightarrow> nat" and
- k2_tl3 :: "(nat, int) t3 l3 \<Rightarrow> nat" and
- k2_t3 :: "(nat, int) t3 \<Rightarrow> nat"
-where
- "k2_tl4 N4 = 0" |
- "k2_tl4 (C4 t ts) = k2_t3 t + k2_tl4 ts" |
- "k2_tl3 N3 = 0" |
- "k2_tl3 (C3 t ts) = k2_t3 t + k2_tl3 ts" |
- "k2_t3 (T3 n _ ts us) = n + k2_tl3 ts + k2_tl4 us"
-
-
-datatype ('a, 'b) l5 = N5 | C5 'a 'b "('a, 'b) l5"
-datatype ('a, 'b) l6 = N6 | C6 'a 'b "('a, 'b) l6"
-datatype ('a, 'b, 'c) t4 = T4 'a 'b "(('a, 'b, 'c) t4, 'b) l5" "(('a, 'b, 'c) t4, 'c) l6"
-
-(* slow *)
-primrec
- l1_tl5 :: "((nat, 'a, 'b) t4, 'a) l5 \<Rightarrow> nat" and
- l1_tl6 :: "((nat, 'a, 'b) t4, 'b) l6 \<Rightarrow> nat" and
- l1_t4 :: "(nat, 'a, 'b) t4 \<Rightarrow> nat"
-where
- "l1_tl5 N5 = 0" |
- "l1_tl5 (C5 t _ ts) = l1_t4 t + l1_tl5 ts" |
- "l1_tl6 N6 = 0" |
- "l1_tl6 (C6 t _ ts) = l1_t4 t + l1_tl6 ts" |
- "l1_t4 (T4 n _ ts us) = n + l1_tl5 ts + l1_tl6 us"
-
-
-subsection \<open>Primcorec Cache\<close>
-
-codatatype 'a col = N | C 'a "'a col"
-codatatype ('a, 'b) cot = T 'a 'b "('a, 'b) cot col"
-
-context linorder
-begin
-
-(* slow *)
-primcorec
- f1_cotcol :: "nat \<Rightarrow> (nat, 'a) cot col" and
- f1_cot :: "nat \<Rightarrow> (nat, 'a) cot"
-where
- "n = 0 \<Longrightarrow> f1_cotcol n = N" |
- "_ \<Longrightarrow> f1_cotcol n = C (f1_cot n) (f1_cotcol n)" |
- "f1_cot n = T n undefined (f1_cotcol n)"
-
-(* should be fast *)
-primcorec
- f2_cotcol :: "nat \<Rightarrow> (nat, 'b) cot col" and
- f2_cot :: "nat \<Rightarrow> (nat, 'b) cot"
-where
- "n = 0 \<Longrightarrow> f2_cotcol n = N" |
- "_ \<Longrightarrow> f2_cotcol n = C (f2_cot n) (f2_cotcol n)" |
- "f2_cot n = T n undefined (f2_cotcol n)"
-
-end
-
-(* should be fast *)
-primcorec
- g1_cot :: "int \<Rightarrow> (int, 'a) cot" and
- g1_cotcol :: "int \<Rightarrow> (int, 'a) cot col"
-where
- "g1_cot n = T n undefined (g1_cotcol n)" |
- "n = 0 \<Longrightarrow> g1_cotcol n = N" |
- "_ \<Longrightarrow> g1_cotcol n = C (g1_cot n) (g1_cotcol n)"
-
-(* should be fast *)
-primcorec
- g2_cot :: "int \<Rightarrow> (int, int) cot" and
- g2_cotcol :: "int \<Rightarrow> (int, int) cot col"
-where
- "g2_cot n = T n undefined (g2_cotcol n)" |
- "n = 0 \<Longrightarrow> g2_cotcol n = N" |
- "_ \<Longrightarrow> g2_cotcol n = C (g2_cot n) (g2_cotcol n)"
-
-
-codatatype
- 'a col1 = N1 | C1 'a "'a col2" and
- 'a col2 = N2 | C2 'a "'a col1"
-
-codatatype
- ('a, 'b) cot1 = T1 'a 'b "('a, 'b) cot1 col1" and
- ('a, 'b) cot2 = T2 "('a, 'b) cot1"
-
-(* slow *)
-primcorec
- h1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
- h1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
- h1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
-where
- "h1_cotcol1 n = C1 (h1_cot1 n) (h1_cotcol2 n)" |
- "h1_cotcol2 n = C2 (h1_cot1 n) (h1_cotcol1 n)" |
- "h1_cot1 n = T1 n undefined (h1_cotcol1 n)"
-
-(* should be fast *)
-primcorec
- h2_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
- h2_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
- h2_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
-where
- "h2_cotcol1 n = C1 (h2_cot1 n) (h2_cotcol2 n)" |
- "h2_cotcol2 n = C2 (h2_cot1 n) (h2_cotcol1 n)" |
- "h2_cot1 n = T1 n undefined (h2_cotcol1 n)"
-
-(* should be fast *)
-primcorec
- h3_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
- h3_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
- h3_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1"
-where
- "h3_cotcol1 n = C1 (h3_cot1 n) (h3_cotcol2 n)" |
- "h3_cotcol2 n = C2 (h3_cot1 n) (h3_cotcol1 n)" |
- "h3_cot1 n = T1 n undefined (h3_cotcol1 n)"
-
-(* should be fast *)
-primcorec
- i1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2" and
- i1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
- i1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" and
- i1_cot2 :: "nat \<Rightarrow> (nat, 'a) cot2"
-where
- "i1_cotcol1 n = C1 (i1_cot1 n) (i1_cotcol2 n)" |
- "i1_cotcol2 n = C2 (i1_cot1 n) (i1_cotcol1 n)" |
- "i1_cot1 n = T1 n undefined (i1_cotcol1 n)" |
- "i1_cot2 n = T2 (i1_cot1 n)"
-
-(* should be fast *)
-primcorec
- j1_cot2 :: "nat \<Rightarrow> (nat, 'a) cot2" and
- j1_cot1 :: "nat \<Rightarrow> (nat, 'a) cot1" and
- j1_cotcol1 :: "nat \<Rightarrow> (nat, 'a) cot1 col1" and
- j1_cotcol2 :: "nat \<Rightarrow> (nat, 'a) cot1 col2"
-where
- "j1_cotcol1 n = C1 (j1_cot1 n) (j1_cotcol2 n)" |
- "j1_cotcol2 n = C2 (j1_cot1 n) (j1_cotcol1 n)" |
- "j1_cot1 n = T1 n undefined (j1_cotcol1 n)" |
- "j1_cot2 n = T2 (j1_cot1 n)"
-
-
-codatatype 'a col3 = N3 | C3 'a "'a col3"
-codatatype 'a col4 = N4 | C4 'a "'a col4"
-codatatype ('a, 'b) cot3 = T3 'a 'b "('a, 'b) cot3 col3" "('a, 'b) cot3 col4"
-
-(* slow *)
-primcorec
- k1_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and
- k1_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and
- k1_cot3 :: "nat \<Rightarrow> (nat, 'a) cot3"
-where
- "k1_cotcol3 n = C3 (k1_cot3 n) (k1_cotcol3 n)" |
- "k1_cotcol4 n = C4 (k1_cot3 n) (k1_cotcol4 n)" |
- "k1_cot3 n = T3 n undefined (k1_cotcol3 n) (k1_cotcol4 n)"
-
-(* should be fast *)
-primcorec
- k2_cotcol4 :: "nat \<Rightarrow> (nat, 'a) cot3 col4" and
- k2_cotcol3 :: "nat \<Rightarrow> (nat, 'a) cot3 col3" and
- k2_cot3 :: "nat \<Rightarrow> (nat, 'a) cot3"
-where
- "k2_cotcol4 n = C4 (k2_cot3 n) (k2_cotcol4 n)" |
- "k2_cotcol3 n = C3 (k2_cot3 n) (k2_cotcol3 n)" |
- "k2_cot3 n = T3 n undefined (k2_cotcol3 n) (k2_cotcol4 n)"
-
-end
--- a/src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy Sat Feb 13 11:50:01 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-theory Find_Unused_Assms_Examples
-imports Complex_Main
-begin
-
-section {* Arithmetics *}
-
-declare [[quickcheck_finite_types = false]]
-
-find_unused_assms Divides
-find_unused_assms GCD
-find_unused_assms Real
-
-section {* Set Theory *}
-
-declare [[quickcheck_finite_types = true]]
-
-find_unused_assms Fun
-find_unused_assms Relation
-find_unused_assms Set
-find_unused_assms Wellfounded
-
-section {* Datatypes *}
-
-find_unused_assms List
-find_unused_assms Map
-
-end
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Sat Feb 13 11:50:01 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,196 +0,0 @@
-theory Needham_Schroeder_Base
-imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
-begin
-
-datatype agent = Alice | Bob | Spy
-
-definition agents :: "agent set"
-where
- "agents = {Spy, Alice, Bob}"
-
-definition bad :: "agent set"
-where
- "bad = {Spy}"
-
-datatype key = pubEK agent | priEK agent
-
-fun invKey
-where
- "invKey (pubEK A) = priEK A"
-| "invKey (priEK A) = pubEK A"
-
-datatype
- msg = Agent agent
- | Key key
- | Nonce nat
- | MPair msg msg
- | Crypt key msg
-
-syntax
- "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
-translations
- "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
- "\<lbrace>x, y\<rbrace>" == "CONST MPair x y"
-
-inductive_set
- parts :: "msg set => msg set"
- for H :: "msg set"
- where
- Inj [intro]: "X \<in> H ==> X \<in> parts H"
- | Fst: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> X \<in> parts H"
- | Snd: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> Y \<in> parts H"
- | Body: "Crypt K X \<in> parts H ==> X \<in> parts H"
-
-inductive_set
- analz :: "msg set => msg set"
- for H :: "msg set"
- where
- Inj [intro,simp] : "X \<in> H ==> X \<in> analz H"
- | Fst: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H"
- | Snd: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H"
- | Decrypt [dest]:
- "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
-
-inductive_set
- synth :: "msg set => msg set"
- for H :: "msg set"
- where
- Inj [intro]: "X \<in> H ==> X \<in> synth H"
- | Agent [intro]: "Agent agt \<in> synth H"
- | MPair [intro]: "[|X \<in> synth H; Y \<in> synth H|] ==> \<lbrace>X,Y\<rbrace> \<in> synth H"
- | Crypt [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Crypt K X \<in> synth H"
-
-primrec initState
-where
- initState_Alice:
- "initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)"
-| initState_Bob:
- "initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)"
-| initState_Spy:
- "initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
-
-datatype
- event = Says agent agent msg
- | Gets agent msg
- | Notes agent msg
-
-
-primrec knows :: "agent => event list => msg set"
-where
- knows_Nil: "knows A [] = initState A"
-| knows_Cons:
- "knows A (ev # evs) =
- (if A = Spy then
- (case ev of
- Says A' B X => insert X (knows Spy evs)
- | Gets A' X => knows Spy evs
- | Notes A' X =>
- if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
- else
- (case ev of
- Says A' B X =>
- if A'=A then insert X (knows A evs) else knows A evs
- | Gets A' X =>
- if A'=A then insert X (knows A evs) else knows A evs
- | Notes A' X =>
- if A'=A then insert X (knows A evs) else knows A evs))"
-
-abbreviation (input)
- spies :: "event list => msg set" where
- "spies == knows Spy"
-
-primrec used :: "event list => msg set"
-where
- used_Nil: "used [] = \<Union>(parts ` initState ` agents)"
-| used_Cons: "used (ev # evs) =
- (case ev of
- Says A B X => parts {X} \<union> used evs
- | Gets A X => used evs
- | Notes A X => parts {X} \<union> used evs)"
-
-subsection {* Preparations for sets *}
-
-fun find_first :: "('a => 'b option) => 'a list => 'b option"
-where
- "find_first f [] = None"
-| "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)"
-
-consts cps_of_set :: "'a set => ('a => term list option) => term list option"
-
-lemma
- [code]: "cps_of_set (set xs) f = find_first f xs"
-sorry
-
-consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option"
-consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
-
-lemma
- [code]: "pos_cps_of_set (set xs) f i = find_first f xs"
-sorry
-
-consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
- => 'b list => 'a Quickcheck_Exhaustive.three_valued"
-
-lemma [code]:
- "find_first' f [] = Quickcheck_Exhaustive.No_value"
- "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
-sorry
-
-lemma
- [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
-sorry
-
-setup {*
-let
- val Fun = Predicate_Compile_Aux.Fun
- val Input = Predicate_Compile_Aux.Input
- val Output = Predicate_Compile_Aux.Output
- val Bool = Predicate_Compile_Aux.Bool
- val oi = Fun (Output, Fun (Input, Bool))
- val ii = Fun (Input, Fun (Input, Bool))
- fun of_set compfuns (Type ("fun", [T, _])) =
- case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of
- Type ("Quickcheck_Exhaustive.three_valued", _) =>
- Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
- | Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T --> Predicate_Compile_Aux.mk_monadT compfuns T)
- | _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T --> (Predicate_Compile_Aux.mk_monadT compfuns T))
- fun member compfuns (U as Type ("fun", [T, _])) =
- (absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns
- (Const (@{const_name "Set.member"}, T --> HOLogic.mk_setT T --> @{typ bool}) $ Bound 1 $ Bound 0))))
-
-in
- Core_Data.force_modes_and_compilations @{const_name Set.member}
- [(oi, (of_set, false)), (ii, (member, false))]
-end
-*}
-
-subsection {* Derived equations for analz, parts and synth *}
-
-lemma [code]:
- "analz H = (let
- H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
- in if H' = H then H else analz H')"
-sorry
-
-lemma [code]:
- "parts H = (let
- H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
- in if H' = H then H else parts H')"
-sorry
-
-definition synth' :: "msg set => msg => bool"
-where
- "synth' H m = (m : synth H)"
-
-lemmas [code_pred_intro] = synth.intros[folded synth'_def]
-
-code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+
-
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
-declare ListMem_iff[symmetric, code_pred_inline]
-declare [[quickcheck_timing]]
-
-setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
-declare [[quickcheck_full_support = false]]
-
-end
\ No newline at end of file
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy Sat Feb 13 11:50:01 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-theory Needham_Schroeder_Guided_Attacker_Example
-imports Needham_Schroeder_Base
-begin
-
-inductive_set ns_public :: "event list set"
- where
- (*Initial trace is empty*)
- Nil: "[] \<in> ns_public"
-
- | Fake_NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1) \<rbrakk>
- \<Longrightarrow> Says Spy B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
- # evs1 \<in> ns_public"
- | Fake_NS2: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1); Nonce NB \<in> analz (spies evs1) \<rbrakk>
- \<Longrightarrow> Says Spy A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
- # evs1 \<in> ns_public"
-
- (*Alice initiates a protocol run, sending a nonce to Bob*)
- | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
- # evs1 \<in> ns_public"
- (*Bob responds to Alice's message with a further nonce*)
- | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
- Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
- # evs2 \<in> ns_public"
-
- (*Alice proves her existence by sending NB back to Bob.*)
- | NS3: "\<lbrakk>evs3 \<in> ns_public;
- Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
- Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
-
-declare ListMem_iff[symmetric, code_pred_inline]
-
-lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
-
-code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
-thm ns_publicp.equation
-
-code_pred [generator_cps] ns_publicp .
-thm ns_publicp.generator_cps_equation
-
-
-lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
-quickcheck[smart_exhaustive, depth = 5, timeout = 100, expect = counterexample]
-(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
-oops
-
-lemma
- "\<lbrakk>ns_publicp evs\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
- \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
- \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
-(*quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = counterexample]
-quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
-oops
-
-section {* Proving the counterexample trace for validation *}
-
-lemma
- assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
- assumes "evs =
- [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
- Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>),
- Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>),
- Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>)]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
- shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
-proof -
- from assms show "A \<noteq> Spy" by auto
- from assms show "B \<noteq> Spy" by auto
- have "[] : ns_public" by (rule Nil)
- then have first_step: "[?e0] : ns_public"
- proof (rule NS1)
- show "Nonce 0 ~: used []" by eval
- qed
- then have "[?e1, ?e0] : ns_public"
- proof (rule Fake_NS1)
- show "Nonce 0 : analz (knows Spy [?e0])" by eval
- qed
- then have "[?e2, ?e1, ?e0] : ns_public"
- proof (rule NS2)
- show "Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e1, ?e0]" by simp
- show " Nonce 1 ~: used [?e1, ?e0]" by eval
- qed
- then show "evs : ns_public"
- unfolding assms
- proof (rule NS3)
- show " Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e2, ?e1, ?e0]" by simp
- show "Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>)
- : set [?e2, ?e1, ?e0]" by simp
- qed
- from assms show "Nonce NB : analz (knows Spy evs)"
- apply simp
- apply (rule analz.intros(4))
- apply (rule analz.intros(1))
- apply (auto simp add: bad_def)
- done
-qed
-
-end
\ No newline at end of file
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy Sat Feb 13 11:50:01 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-theory Needham_Schroeder_No_Attacker_Example
-imports Needham_Schroeder_Base
-begin
-
-inductive_set ns_public :: "event list set"
- where
- (*Initial trace is empty*)
- Nil: "[] \<in> ns_public"
- (*Alice initiates a protocol run, sending a nonce to Bob*)
- | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
- # evs1 \<in> ns_public"
- (*Bob responds to Alice's message with a further nonce*)
- | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
- Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
- # evs2 \<in> ns_public"
-
- (*Alice proves her existence by sending NB back to Bob.*)
- | NS3: "\<lbrakk>evs3 \<in> ns_public;
- Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
- Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
-
-code_pred [skip_proof] ns_publicp .
-thm ns_publicp.equation
-
-code_pred [generator_cps] ns_publicp .
-thm ns_publicp.generator_cps_equation
-
-lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
-(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose]
-quickcheck[exhaustive, size = 8, timeout = 3600, verbose]
-quickcheck[narrowing, size = 7, timeout = 3600, verbose]*)
-quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample]
-oops
-
-lemma
- "\<lbrakk>ns_publicp evs\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
- \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
- \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
-quickcheck[smart_exhaustive, depth = 6, timeout = 30]
-quickcheck[narrowing, size = 6, timeout = 30, verbose]
-oops
-
-end
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy Sat Feb 13 11:50:01 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-theory Needham_Schroeder_Unguided_Attacker_Example
-imports Needham_Schroeder_Base
-begin
-
-inductive_set ns_public :: "event list set"
- where
- (*Initial trace is empty*)
- Nil: "[] \<in> ns_public"
-
- | Fake: "\<lbrakk>evs1 \<in> ns_public; X \<in> synth (analz (spies evs1)) \<rbrakk>
- \<Longrightarrow> Says Spy A X # evs1 \<in> ns_public"
-
- (*Alice initiates a protocol run, sending a nonce to Bob*)
- | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
- # evs1 \<in> ns_public"
- (*Bob responds to Alice's message with a further nonce*)
- | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
- Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
- # evs2 \<in> ns_public"
-
- (*Alice proves her existence by sending NB back to Bob.*)
- | NS3: "\<lbrakk>evs3 \<in> ns_public;
- Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
- Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
- \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
-
-declare ListMem_iff[symmetric, code_pred_inline]
-
-lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
-
-code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
-thm ns_publicp.equation
-
-code_pred [generator_cps] ns_publicp .
-thm ns_publicp.generator_cps_equation
-
-
-lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
-quickcheck[smart_exhaustive, depth = 5, timeout = 200, expect = counterexample]
-(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
-oops
-
-lemma
- "\<lbrakk>ns_publicp evs\<rbrakk>
- \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
- \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B
- \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
-quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample]
-(*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
-oops
-
-section {* Proving the counterexample trace for validation *}
-
-lemma
- assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
- assumes "evs =
- [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
- Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>),
- Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>),
- Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>)]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
- shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
-proof -
- from assms show "A \<noteq> Spy" by auto
- from assms show "B \<noteq> Spy" by auto
- have "[] : ns_public" by (rule Nil)
- then have first_step: "[?e0] : ns_public"
- proof (rule NS1)
- show "Nonce 0 ~: used []" by eval
- qed
- then have "[?e1, ?e0] : ns_public"
- proof (rule Fake)
- show "Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace> : synth (analz (knows Spy [?e0]))"
- by (intro synth.intros(2,3,4,1)) eval+
- qed
- then have "[?e2, ?e1, ?e0] : ns_public"
- proof (rule NS2)
- show "Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e1, ?e0]" by simp
- show " Nonce 1 ~: used [?e1, ?e0]" by eval
- qed
- then show "evs : ns_public"
- unfolding assms
- proof (rule NS3)
- show " Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e2, ?e1, ?e0]" by simp
- show "Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>) : set [?e2, ?e1, ?e0]" by simp
- qed
- from assms show "Nonce NB : analz (knows Spy evs)"
- apply simp
- apply (rule analz.intros(4))
- apply (rule analz.intros(1))
- apply (auto simp add: bad_def)
- done
-qed
-
-end
\ No newline at end of file
--- a/src/HOL/ROOT Sat Feb 13 11:50:01 2016 +0100
+++ b/src/HOL/ROOT Sat Feb 13 12:13:10 2016 +0100
@@ -788,7 +788,7 @@
session "HOL-Datatype_Examples" in Datatype_Examples = HOL +
description {*
- (Co)datatype Examples, including large ones from John Harrison.
+ (Co)datatype Examples.
*}
options [document = false]
theories
@@ -807,10 +807,6 @@
Misc_Datatype
Misc_Primcorec
Misc_Primrec
- theories [condition = ISABELLE_FULL_TEST]
- Brackin
- IsaFoR
- Misc_N2M
session "HOL-Word" (main) in Word = HOL +
theories Word
@@ -964,13 +960,6 @@
Hotel_Example
Quickcheck_Narrowing_Examples
-session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
- theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
- Find_Unused_Assms_Examples
- Needham_Schroeder_No_Attacker_Example
- Needham_Schroeder_Guided_Attacker_Example
- Needham_Schroeder_Unguided_Attacker_Example
-
session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
description {*
Author: Cezary Kaliszyk and Christian Urban
@@ -1139,12 +1128,3 @@
theories
TrivEx
TrivEx2
-
-session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
- description {*
- Some benchmark on large record.
- *}
- options [document = false]
- theories [condition = ISABELLE_FULL_TEST]
- Record_Benchmark
-
--- a/src/HOL/Record_Benchmark/Record_Benchmark.thy Sat Feb 13 11:50:01 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,427 +0,0 @@
-(* Title: HOL/Record_Benchmark/Record_Benchmark.thy
- Author: Norbert Schirmer, DFKI
-*)
-
-section {* Benchmark for large record *}
-
-theory Record_Benchmark
-imports Main
-begin
-
-declare [[record_timing]]
-
-record many_A =
-A000::nat
-A001::nat
-A002::nat
-A003::nat
-A004::nat
-A005::nat
-A006::nat
-A007::nat
-A008::nat
-A009::nat
-A010::nat
-A011::nat
-A012::nat
-A013::nat
-A014::nat
-A015::nat
-A016::nat
-A017::nat
-A018::nat
-A019::nat
-A020::nat
-A021::nat
-A022::nat
-A023::nat
-A024::nat
-A025::nat
-A026::nat
-A027::nat
-A028::nat
-A029::nat
-A030::nat
-A031::nat
-A032::nat
-A033::nat
-A034::nat
-A035::nat
-A036::nat
-A037::nat
-A038::nat
-A039::nat
-A040::nat
-A041::nat
-A042::nat
-A043::nat
-A044::nat
-A045::nat
-A046::nat
-A047::nat
-A048::nat
-A049::nat
-A050::nat
-A051::nat
-A052::nat
-A053::nat
-A054::nat
-A055::nat
-A056::nat
-A057::nat
-A058::nat
-A059::nat
-A060::nat
-A061::nat
-A062::nat
-A063::nat
-A064::nat
-A065::nat
-A066::nat
-A067::nat
-A068::nat
-A069::nat
-A070::nat
-A071::nat
-A072::nat
-A073::nat
-A074::nat
-A075::nat
-A076::nat
-A077::nat
-A078::nat
-A079::nat
-A080::nat
-A081::nat
-A082::nat
-A083::nat
-A084::nat
-A085::nat
-A086::nat
-A087::nat
-A088::nat
-A089::nat
-A090::nat
-A091::nat
-A092::nat
-A093::nat
-A094::nat
-A095::nat
-A096::nat
-A097::nat
-A098::nat
-A099::nat
-A100::nat
-A101::nat
-A102::nat
-A103::nat
-A104::nat
-A105::nat
-A106::nat
-A107::nat
-A108::nat
-A109::nat
-A110::nat
-A111::nat
-A112::nat
-A113::nat
-A114::nat
-A115::nat
-A116::nat
-A117::nat
-A118::nat
-A119::nat
-A120::nat
-A121::nat
-A122::nat
-A123::nat
-A124::nat
-A125::nat
-A126::nat
-A127::nat
-A128::nat
-A129::nat
-A130::nat
-A131::nat
-A132::nat
-A133::nat
-A134::nat
-A135::nat
-A136::nat
-A137::nat
-A138::nat
-A139::nat
-A140::nat
-A141::nat
-A142::nat
-A143::nat
-A144::nat
-A145::nat
-A146::nat
-A147::nat
-A148::nat
-A149::nat
-A150::nat
-A151::nat
-A152::nat
-A153::nat
-A154::nat
-A155::nat
-A156::nat
-A157::nat
-A158::nat
-A159::nat
-A160::nat
-A161::nat
-A162::nat
-A163::nat
-A164::nat
-A165::nat
-A166::nat
-A167::nat
-A168::nat
-A169::nat
-A170::nat
-A171::nat
-A172::nat
-A173::nat
-A174::nat
-A175::nat
-A176::nat
-A177::nat
-A178::nat
-A179::nat
-A180::nat
-A181::nat
-A182::nat
-A183::nat
-A184::nat
-A185::nat
-A186::nat
-A187::nat
-A188::nat
-A189::nat
-A190::nat
-A191::nat
-A192::nat
-A193::nat
-A194::nat
-A195::nat
-A196::nat
-A197::nat
-A198::nat
-A199::nat
-A200::nat
-A201::nat
-A202::nat
-A203::nat
-A204::nat
-A205::nat
-A206::nat
-A207::nat
-A208::nat
-A209::nat
-A210::nat
-A211::nat
-A212::nat
-A213::nat
-A214::nat
-A215::nat
-A216::nat
-A217::nat
-A218::nat
-A219::nat
-A220::nat
-A221::nat
-A222::nat
-A223::nat
-A224::nat
-A225::nat
-A226::nat
-A227::nat
-A228::nat
-A229::nat
-A230::nat
-A231::nat
-A232::nat
-A233::nat
-A234::nat
-A235::nat
-A236::nat
-A237::nat
-A238::nat
-A239::nat
-A240::nat
-A241::nat
-A242::nat
-A243::nat
-A244::nat
-A245::nat
-A246::nat
-A247::nat
-A248::nat
-A249::nat
-A250::nat
-A251::nat
-A252::nat
-A253::nat
-A254::nat
-A255::nat
-A256::nat
-A257::nat
-A258::nat
-A259::nat
-A260::nat
-A261::nat
-A262::nat
-A263::nat
-A264::nat
-A265::nat
-A266::nat
-A267::nat
-A268::nat
-A269::nat
-A270::nat
-A271::nat
-A272::nat
-A273::nat
-A274::nat
-A275::nat
-A276::nat
-A277::nat
-A278::nat
-A279::nat
-A280::nat
-A281::nat
-A282::nat
-A283::nat
-A284::nat
-A285::nat
-A286::nat
-A287::nat
-A288::nat
-A289::nat
-A290::nat
-A291::nat
-A292::nat
-A293::nat
-A294::nat
-A295::nat
-A296::nat
-A297::nat
-A298::nat
-A299::nat
-
-record many_B = many_A +
-B000::nat
-B001::nat
-B002::nat
-B003::nat
-B004::nat
-B005::nat
-B006::nat
-B007::nat
-B008::nat
-B009::nat
-B010::nat
-B011::nat
-B012::nat
-B013::nat
-B014::nat
-B015::nat
-B016::nat
-B017::nat
-B018::nat
-B019::nat
-B020::nat
-B021::nat
-B022::nat
-B023::nat
-B024::nat
-B025::nat
-B026::nat
-B027::nat
-B028::nat
-B029::nat
-B030::nat
-
-lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
- by simp
-
-lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
- by simp
-
-lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
- by simp
-
-lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
- apply (tactic {* simp_tac
- (put_simpset HOL_basic_ss @{context} addsimprocs [Record.upd_simproc]) 1*})
- done
-
-lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
- apply (tactic {* simp_tac
- (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*})
- apply simp
- done
-
-lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
- apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
- apply simp
- done
-
-lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
- apply (tactic {* simp_tac
- (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*})
- apply simp
- done
-
-lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
- apply simp
- done
-
-lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* simp_tac
- (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*})
- apply auto
- done
-
-lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
- apply auto
- done
-
-lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
- apply auto
- done
-
-lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
- apply auto
- done
-
-
-notepad
-begin
- fix P r
- assume "P (A155 r)"
- then have "\<exists>x. P x"
- apply -
- apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
- apply auto
- done
-end
-
-
-lemma "\<exists>r. A155 r = x"
- apply (tactic {*simp_tac
- (put_simpset HOL_basic_ss @{context} addsimprocs [Record.ex_sel_eq_simproc]) 1*})
- done
-
-print_record many_A
-
-print_record many_B
-
-end
\ No newline at end of file