# HG changeset patch # User wenzelm # Date 1455361990 -3600 # Node ID 705d4c4003ea2f81180aaf75403f84108619d79b # Parent 747fc3692fca9097350af4041cbecbed940790e4 clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default; diff -r 747fc3692fca -r 705d4c4003ea src/Benchmarks/Datatype_Benchmark/Brackin.thy --- /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 diff -r 747fc3692fca -r 705d4c4003ea src/Benchmarks/Datatype_Benchmark/IsaFoR.thy --- /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 \ nat) \ nat) list" + +datatype (discs_sels) ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list" +datatype (discs_sels) ('f, 'v) ctxt = + Hole ("\") + | More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list" + +type_synonym ('f, 'v) rule = "('f, 'v) term \ ('f, 'v) term" +type_synonym ('f, 'v) trs = "('f, 'v) rule set" + +type_synonym ('f, 'v) rules = "('f, 'v) rule list" +type_synonym ('f, 'l, 'v) ruleLL = "(('f, 'l) lab, 'v) rule" +type_synonym ('f, 'l, 'v) trsLL = "(('f, 'l) lab, 'v) rules" +type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list" + +datatype (discs_sels) pos = Empty ("\") | PCons "nat" "pos" (infixr "<#" 70) + +type_synonym ('f, 'v) prseq = "(pos \ ('f, 'v) rule \ bool \ ('f, 'v) term) list" +type_synonym ('f, 'v) rseq = "(pos \ ('f, 'v) rule \ ('f, 'v) term) list" + +type_synonym ('f, 'l, 'v) rseqL = "((('f, 'l) lab, 'v) rule \ (('f, 'l) lab, 'v) rseq) list" +type_synonym ('f, 'l, 'v) dppLL = + "bool \ bool \ ('f, 'l, 'v) trsLL \ ('f, 'l, 'v) trsLL \ + ('f, 'l, 'v) termsLL \ + ('f, 'l, 'v) trsLL \ ('f, 'l, 'v) trsLL" + +type_synonym ('f, 'l, 'v) qreltrsLL = + "bool \ ('f, 'l, 'v) termsLL \ ('f, 'l, 'v) trsLL \ ('f, 'l, 'v) trsLL" + +type_synonym ('f, 'l, 'v) qtrsLL = + "bool \ ('f, 'l, 'v) termsLL \ ('f, 'l, 'v) trsLL" + +datatype (discs_sels) location = H | A | B | R + +type_synonym ('f, 'v) forb_pattern = "('f, 'v) ctxt \ ('f, 'v) term \ location" +type_synonym ('f, 'v) forb_patterns = "('f, 'v) forb_pattern set" + +type_synonym ('f, 'l, 'v) fptrsLL = + "(('f, 'l) lab, 'v) forb_pattern list \ ('f, 'l, 'v) trsLL" + +type_synonym ('f, 'l, 'v) prob = "('f, 'l, 'v) qreltrsLL + ('f, 'l, 'v) dppLL" + +type_synonym ('f, 'a) lpoly_inter = "'f \ nat \ ('a \ 'a list)" +type_synonym ('f, 'a) lpoly_interL = "(('f \ nat) \ ('a \ 'a list)) list" + +type_synonym 'v monom = "('v \ nat) list" +type_synonym ('v, 'a) poly = "('v monom \ 'a) list" +type_synonym ('f, 'a) poly_inter_list = "(('f \ nat) \ (nat, 'a) poly) list" +type_synonym 'a vec = "'a list" +type_synonym 'a mat = "'a vec list" + +datatype (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 \ nat) \ (nat \ order_tag)) list" + +datatype (discs_sels) af_entry = + Collapse nat + | AFList "nat list" + +type_synonym 'f afs_list = "(('f \ nat) \ af_entry) list" +type_synonym 'f prec_weight_repr = "(('f \ nat) \ (nat \ nat \ (nat list option))) list \ nat" + +datatype (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 \ nat) \ (nat \ 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 \ nat) \ 'f list) list" +type_synonym ('f, 'v) uncurry_info = "'f \ 'f sig_map_list \ ('f, 'v) rules \ ('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 \ nat) \ arithFun) list" +datatype (discs_sels) ('f, 'v) sl_variant = + Rootlab "('f \ nat) option" + | Finitelab "'f sl_inter" + | QuasiFinitelab "'f sl_inter" 'v + +type_synonym ('f, 'v) crit_pair_joins = "(('f, 'v) term \ ('f, 'v) rseq \ ('f, 'v) term \ ('f, 'v) rseq) list" + +datatype (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 \ ('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 \ ('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 \ (('f, 'v) term \ 'v list) list \ ('f, 'v) cond_constraint \ ('f, 'v) cond_constraint_prf) list" + +datatype (discs_sels) ('f, 'v) cond_red_pair_prf = + Cond_Red_Pair_Prf + 'f "(('f, 'v) cond_constraint \ ('f, 'v) rules \ ('f, 'v) cond_constraint_prf) list" nat nat + +datatype (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \ _") +datatype (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \ 'q) list" +datatype (discs_sels) 'q ta_relation = + Decision_Proc + | Id_Relation + | Some_Relation "('q \ 'q) list" + +datatype (discs_sels) boundstype = Roof | Match +datatype (discs_sels) ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \ 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 \ ('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 \ bool" where + "satisfied (SN_TRS t) = (t = t)" +| "satisfied (SN_FP_TRS t) = (t \ t)" +| "satisfied (Finite_DPP d) = (d \ d)" +| "satisfied (Unknown_Problem s) = (s = ''foo'')" +| "satisfied (Not_SN_TRS (nfs, q, r)) = (length q = length r)" +| "satisfied (Not_RelSN_TRS (nfs, q, r, rw)) = (r = rw)" +| "satisfied (Infinite_DPP d) = (d = d)" +| "satisfied (Not_SN_FP_TRS t) = (t = t)" + +fun collect_assms :: "('tp \ ('f, 'l, 'v) assm list) + \ ('dpp \ ('f, 'l, 'v) assm list) + \ ('fptp \ ('f, 'l, 'v) assm list) + \ ('unk \ ('f, 'l, 'v) assm list) + \ ('f, 'l, 'v, 'tp, 'dpp, 'fptp, 'unk) assm_proof \ ('f, 'l, 'v) assm list" where + "collect_assms tp dpp fptp unk (SN_assm_proof t prf) = tp prf" +| "collect_assms tp dpp fptp unk (SN_FP_assm_proof t prf) = fptp prf" +| "collect_assms tp dpp fptp unk (Finite_assm_proof d prf) = dpp prf" +| "collect_assms tp dpp fptp unk (Unknown_assm_proof p prf) = unk prf" +| "collect_assms _ _ _ _ _ = []" + +fun collect_neg_assms :: "('tp \ ('f, 'l, 'v) assm list) + \ ('dpp \ ('f, 'l, 'v) assm list) + \ ('rtp \ ('f, 'l, 'v) assm list) + \ ('fptp \ ('f, 'l, 'v) assm list) + \ ('unk \ ('f, 'l, 'v) assm list) + \ ('f, 'l, 'v, 'tp, 'dpp, 'rtp, 'fptp, 'unk) generic_assm_proof \ ('f, 'l, 'v) assm list" where + "collect_neg_assms tp dpp rtp fptp unk (Not_SN_assm_proof t prf) = tp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Infinite_assm_proof d prf) = dpp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Not_RelSN_assm_proof t prf) = rtp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Not_SN_FP_assm_proof t prf) = fptp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf" +| "collect_neg_assms tp dpp rtp fptp unk _ = []" + +datatype (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 \ ('f, 'l, 'v) trsLL) list" + | Mono_Redpair_Proc "('f, 'l) lab redtriple_impl" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" + | Mono_Redpair_UR_Proc "('f, 'l) lab redtriple_impl" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" + | Size_Change_Subterm_Proc "((('f, 'l) lab, 'v) rule \ ((nat \ nat) list \ (nat \ nat) list)) list" + | Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option" + "((('f, 'l) lab, 'v) rule \ ((nat \ nat) list \ (nat \ nat) list)) list" + | Uncurry_Proc "nat option" "(('f, 'l) lab, 'v) uncurry_info" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" + | Fcc_Proc "('f, 'l) lab" "(('f, 'l) lab, 'v) ctxt list" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" + | Split_Proc + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" + "('f, 'l, 'v) dp_termination_proof" "('f, 'l, 'v) dp_termination_proof" + | Semlab_Proc + "(('f, 'l) lab, 'v) sl_variant" "('f, 'l, 'v) trsLL" + "(('f, 'l) lab, 'v) term list" "('f, 'l, 'v) trsLL" + "('f, 'l, 'v) dp_termination_proof" + | Switch_Innermost_Proc "('f, 'l) lab join_info" "('f, 'l, 'v) dp_termination_proof" + | Rewriting_Proc + "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" + "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) dp_termination_proof" + | Instantiation_Proc "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" + | Forward_Instantiation_Proc + "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_termination_proof" + | Narrowing_Proc "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" + | Assume_Finite + "('f, 'l, 'v) dppLL" "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list" + | Unlab_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" + | Q_Reduction_Proc "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_termination_proof" + | Complex_Constant_Removal_Proc "(('f, 'l) lab, 'v) complex_constant_removal_prf" "('f, 'l, 'v) dp_termination_proof" + | General_Redpair_Proc + "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" + "(('f, 'l) lab, 'v) cond_red_pair_prf" "('f, 'l, 'v) dp_termination_proof list" + | To_Trs_Proc "('f, 'l, 'v) trs_termination_proof" +and ('f, 'l, 'v) trs_termination_proof = + DP_Trans bool bool "(('f, 'l) lab, 'v) rules" "('f, 'l, 'v) dp_termination_proof" + | Rule_Removal "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" + | String_Reversal "('f, 'l, 'v) trs_termination_proof" + | Bounds "(('f, 'l) lab, 'v) bounds_info" + | Uncurry "(('f, 'l) lab, 'v) uncurry_info" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" + | Semlab + "(('f, 'l) lab, 'v) sl_variant" "(('f, 'l) lab, 'v) term list" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" + | R_is_Empty + | Fcc "(('f, 'l) lab, 'v) ctxt list" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" + | Split "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" "('f, 'l, 'v) trs_termination_proof" + | Switch_Innermost "('f, 'l) lab join_info" "('f, 'l, 'v) trs_termination_proof" + | Drop_Equality "('f, 'l, 'v) trs_termination_proof" + | Remove_Nonapplicable_Rules "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" + | Assume_SN "('f, 'l, 'v) qreltrsLL" "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list" +and ('f, 'l, 'v) unknown_proof = + Assume_Unknown unknown_info "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list" +and ('f, 'l, 'v) fptrs_termination_proof = + Assume_FP_SN "('f, 'l, 'v) fptrsLL" "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list" + +end diff -r 747fc3692fca -r 705d4c4003ea src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy --- /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 \Miscellaneous Tests for the Nested-to-Mutual Reduction\ + +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 \ 'a tr li" + +primrec (nonexhaustive) + f_tl :: "'a \ 'a tr li \ nat" and + f_t :: "'a \ 'a tr \ 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 \ nat" and + f_t2 :: "('a, 'a) t \ 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 \ nat" and + g_tlb :: "(('a, 'b) t, 'b) l \ nat" and + g_t :: "('a, 'b) t \ 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 \ ('a, 'b) t1) l1" and + ('a, 'b) t2 = T2 "('a, 'b) t1" + +primrec + h1_tl1 :: "(nat, 'a) t1 l1 \ nat" and + h1_natl1 :: "(nat \ (nat, 'a) t1) l1 \ nat" and + h1_t1 :: "(nat, 'a) t1 \ 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 \ 'a G" +and fK :: "('a G, 'a G N) K \ ('a G, 'a G N) K" +and fL :: "('a G, 'a G N) L \ ('a G, 'a G N) L" +and fM :: "'a G M \ '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 \ 'a G" +and fK :: "('a G, 'a G N) K \ ('a G, 'a G N) K" +and fL :: "('a G, 'a G N) L \ ('a G, 'a G N) L" +and fM :: "'a G M \ '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 \Deep Nesting\ + +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 \Primrec cache\ + +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 \ nat" and + f1_t :: "(nat, 'a) t \ 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 \ nat" and + f2_tl :: "(nat, 'b) t l \ 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 \ nat" and + g1_tl :: "('a, int) t l \ 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 \ nat" and + g2_tl :: "(int, int) t l \ 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 \ 'a" and + sum_l2 :: "'a::{zero,plus} l2 \ '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 \ nat" and + h1_tl2 :: "(nat, 'a) t1 l2 \ nat" and + h1_t1 :: "(nat, 'a) t1 \ 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 \ nat" and + h2_tl2 :: "(nat, 'a) t1 l2 \ nat" and + h2_t1 :: "(nat, 'a) t1 \ 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 \ nat" and + h3_tl1 :: "(nat, 'a) t1 l1 \ nat" and + h3_t1 :: "(nat, 'a) t1 \ 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 \ nat" and + i1_tl1 :: "(nat, 'a) t1 l1 \ nat" and + i1_t1 :: "(nat, 'a) t1 \ nat" and + i1_t2 :: "(nat, 'a) t2 \ 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 \ nat" and + j1_t1 :: "(nat, 'a) t1 \ nat" and + j1_tl1 :: "(nat, 'a) t1 l1 \ nat" and + j1_tl2 :: "(nat, 'a) t1 l2 \ 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 \ nat" and + k1_tl4 :: "(nat, 'a) t3 l4 \ nat" and + k1_t3 :: "(nat, 'a) t3 \ 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 \ nat" and + k2_tl3 :: "(nat, int) t3 l3 \ nat" and + k2_t3 :: "(nat, int) t3 \ 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 \ nat" and + l1_tl6 :: "((nat, 'a, 'b) t4, 'b) l6 \ nat" and + l1_t4 :: "(nat, 'a, 'b) t4 \ 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 \Primcorec Cache\ + +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 \ (nat, 'a) cot col" and + f1_cot :: "nat \ (nat, 'a) cot" +where + "n = 0 \ f1_cotcol n = N" | + "_ \ 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 \ (nat, 'b) cot col" and + f2_cot :: "nat \ (nat, 'b) cot" +where + "n = 0 \ f2_cotcol n = N" | + "_ \ 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 \ (int, 'a) cot" and + g1_cotcol :: "int \ (int, 'a) cot col" +where + "g1_cot n = T n undefined (g1_cotcol n)" | + "n = 0 \ g1_cotcol n = N" | + "_ \ g1_cotcol n = C (g1_cot n) (g1_cotcol n)" + +(* should be fast *) +primcorec + g2_cot :: "int \ (int, int) cot" and + g2_cotcol :: "int \ (int, int) cot col" +where + "g2_cot n = T n undefined (g2_cotcol n)" | + "n = 0 \ g2_cotcol n = N" | + "_ \ 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 \ (nat, 'a) cot1 col1" and + h1_cotcol2 :: "nat \ (nat, 'a) cot1 col2" and + h1_cot1 :: "nat \ (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 \ (nat, 'a) cot1 col1" and + h2_cotcol2 :: "nat \ (nat, 'a) cot1 col2" and + h2_cot1 :: "nat \ (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 \ (nat, 'a) cot1 col2" and + h3_cotcol1 :: "nat \ (nat, 'a) cot1 col1" and + h3_cot1 :: "nat \ (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 \ (nat, 'a) cot1 col2" and + i1_cotcol1 :: "nat \ (nat, 'a) cot1 col1" and + i1_cot1 :: "nat \ (nat, 'a) cot1" and + i1_cot2 :: "nat \ (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 \ (nat, 'a) cot2" and + j1_cot1 :: "nat \ (nat, 'a) cot1" and + j1_cotcol1 :: "nat \ (nat, 'a) cot1 col1" and + j1_cotcol2 :: "nat \ (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 \ (nat, 'a) cot3 col3" and + k1_cotcol4 :: "nat \ (nat, 'a) cot3 col4" and + k1_cot3 :: "nat \ (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 \ (nat, 'a) cot3 col4" and + k2_cotcol3 :: "nat \ (nat, 'a) cot3 col3" and + k2_cot3 :: "nat \ (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 diff -r 747fc3692fca -r 705d4c4003ea src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy --- /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 diff -r 747fc3692fca -r 705d4c4003ea src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy --- /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\_,/ _\)") +translations + "\x, y, z\" == "\x, \y, z\\" + "\x, y\" == "CONST MPair x y" + +inductive_set + parts :: "msg set => msg set" + for H :: "msg set" + where + Inj [intro]: "X \ H ==> X \ parts H" + | Fst: "\X,Y\ \ parts H ==> X \ parts H" + | Snd: "\X,Y\ \ parts H ==> Y \ parts H" + | Body: "Crypt K X \ parts H ==> X \ parts H" + +inductive_set + analz :: "msg set => msg set" + for H :: "msg set" + where + Inj [intro,simp] : "X \ H ==> X \ analz H" + | Fst: "\X,Y\ \ analz H ==> X \ analz H" + | Snd: "\X,Y\ \ analz H ==> Y \ analz H" + | Decrypt [dest]: + "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" + +inductive_set + synth :: "msg set => msg set" + for H :: "msg set" + where + Inj [intro]: "X \ H ==> X \ synth H" + | Agent [intro]: "Agent agt \ synth H" + | MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> \X,Y\ \ synth H" + | Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" + +primrec initState +where + initState_Alice: + "initState Alice = {Key (priEK Alice)} \ (Key ` pubEK ` agents)" +| initState_Bob: + "initState Bob = {Key (priEK Bob)} \ (Key ` pubEK ` agents)" +| initState_Spy: + "initState Spy = (Key ` priEK ` bad) \ (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' \ 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 [] = \(parts ` initState ` agents)" +| used_Cons: "used (ev # evs) = + (case ev of + Says A B X => parts {X} \ used evs + | Gets A X => used evs + | Notes A X => parts {X} \ 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 \ (\((%m. case m of \X, Y\ => {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 \ (\((%m. case m of \X, Y\ => {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 diff -r 747fc3692fca -r 705d4c4003ea src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy --- /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: "[] \ ns_public" + + | Fake_NS1: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1) \ + \ Says Spy B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + | Fake_NS2: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1); Nonce NB \ analz (spies evs1) \ + \ Says Spy A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs1 \ ns_public" + + (*Alice initiates a protocol run, sending a nonce to Bob*) + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + (*Bob responds to Alice's message with a further nonce*) + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs2 \ ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + | NS3: "\evs3 \ ns_public; + Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; + Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ + \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 + "\ns_publicp evs\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs + \ A \ Spy \ B \ Spy \ A \ B + \ Nonce NB \ 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) \Nonce 0, Nonce 1\), + Says Spy Bob (Crypt (pubEK Bob) \Nonce 0, Agent Alice\), + Says Alice Spy (Crypt (pubEK Spy) \Nonce 0, Agent Alice\)]" (is "_ = [?e3, ?e2, ?e1, ?e0]") + shows "A \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" +proof - + from assms show "A \ Spy" by auto + from assms show "B \ 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) \Nonce 0, Agent Alice\) \ 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) \Nonce 0, Agent Alice\) \ set [?e2, ?e1, ?e0]" by simp + show "Says Bob Alice (Crypt (pubEK Alice) \Nonce 0, Nonce 1\) + : 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 diff -r 747fc3692fca -r 705d4c4003ea src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy --- /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: "[] \ ns_public" + (*Alice initiates a protocol run, sending a nonce to Bob*) + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + (*Bob responds to Alice's message with a further nonce*) + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs2 \ ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + | NS3: "\evs3 \ ns_public; + Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; + Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ + \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 + "\ns_publicp evs\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs + \ A \ Spy \ B \ Spy \ A \ B + \ Nonce NB \ analz (spies evs)" +quickcheck[smart_exhaustive, depth = 6, timeout = 30] +quickcheck[narrowing, size = 6, timeout = 30, verbose] +oops + +end diff -r 747fc3692fca -r 705d4c4003ea src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy --- /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: "[] \ ns_public" + + | Fake: "\evs1 \ ns_public; X \ synth (analz (spies evs1)) \ + \ Says Spy A X # evs1 \ ns_public" + + (*Alice initiates a protocol run, sending a nonce to Bob*) + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + (*Bob responds to Alice's message with a further nonce*) + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) + # evs2 \ ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + | NS3: "\evs3 \ ns_public; + Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; + Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ + \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 + "\ns_publicp evs\ + \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs + \ A \ Spy \ B \ Spy \ A \ B + \ Nonce NB \ 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) \Nonce 0, Nonce 1\), + Says Spy Bob (Crypt (pubEK Bob) \Nonce 0, Agent Alice\), + Says Alice Spy (Crypt (pubEK Spy) \Nonce 0, Agent Alice\)]" (is "_ = [?e3, ?e2, ?e1, ?e0]") + shows "A \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" +proof - + from assms show "A \ Spy" by auto + from assms show "B \ 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) \Nonce 0, Agent Alice\ : 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) \Nonce 0, Agent Alice\) \ 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) \Nonce 0, Agent Alice\) \ set [?e2, ?e1, ?e0]" by simp + show "Says Bob Alice (Crypt (pubEK Alice) \Nonce 0, Nonce 1\) : 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 diff -r 747fc3692fca -r 705d4c4003ea src/Benchmarks/ROOT --- /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 diff -r 747fc3692fca -r 705d4c4003ea src/Benchmarks/Record_Benchmark/Record_Benchmark.thy --- /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\A255:=x\) = A155 r" + by simp + +lemma "A155 (r\A255:=x,A253:=y,A255:=z \) = A155 r" + by simp + +lemma "(r\A255:=x,A253:=y,A255:=z \) = r\A253:=y,A255:=z\" + by simp + +lemma "(r\A255:=x,A253:=y,A255:=z \) = r\A253:=y,A255:=z\" + apply (tactic {* simp_tac + (put_simpset HOL_basic_ss @{context} addsimprocs [Record.upd_simproc]) 1*}) + done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* simp_tac + (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*}) + apply simp + done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) + apply simp + done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* simp_tac + (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*}) + apply simp + done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) + apply simp + done + +lemma "\r. P (A155 r) \ (\x. P x)" + apply (tactic {* simp_tac + (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*}) + apply auto + done + +lemma "\r. P (A155 r) \ (\x. P x)" + apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) + apply auto + done + +lemma "P (A155 r) \ (\x. P x)" + apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) + apply auto + done + +lemma fixes r shows "P (A155 r) \ (\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 "\x. P x" + apply - + apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) + apply auto + done +end + + +lemma "\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 diff -r 747fc3692fca -r 705d4c4003ea src/HOL/Datatype_Examples/Brackin.thy --- 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 diff -r 747fc3692fca -r 705d4c4003ea src/HOL/Datatype_Examples/IsaFoR.thy --- 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 \ nat) \ nat) list" - -datatype (discs_sels) ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list" -datatype (discs_sels) ('f, 'v) ctxt = - Hole ("\") - | More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list" - -type_synonym ('f, 'v) rule = "('f, 'v) term \ ('f, 'v) term" -type_synonym ('f, 'v) trs = "('f, 'v) rule set" - -type_synonym ('f, 'v) rules = "('f, 'v) rule list" -type_synonym ('f, 'l, 'v) ruleLL = "(('f, 'l) lab, 'v) rule" -type_synonym ('f, 'l, 'v) trsLL = "(('f, 'l) lab, 'v) rules" -type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list" - -datatype (discs_sels) pos = Empty ("\") | PCons "nat" "pos" (infixr "<#" 70) - -type_synonym ('f, 'v) prseq = "(pos \ ('f, 'v) rule \ bool \ ('f, 'v) term) list" -type_synonym ('f, 'v) rseq = "(pos \ ('f, 'v) rule \ ('f, 'v) term) list" - -type_synonym ('f, 'l, 'v) rseqL = "((('f, 'l) lab, 'v) rule \ (('f, 'l) lab, 'v) rseq) list" -type_synonym ('f, 'l, 'v) dppLL = - "bool \ bool \ ('f, 'l, 'v) trsLL \ ('f, 'l, 'v) trsLL \ - ('f, 'l, 'v) termsLL \ - ('f, 'l, 'v) trsLL \ ('f, 'l, 'v) trsLL" - -type_synonym ('f, 'l, 'v) qreltrsLL = - "bool \ ('f, 'l, 'v) termsLL \ ('f, 'l, 'v) trsLL \ ('f, 'l, 'v) trsLL" - -type_synonym ('f, 'l, 'v) qtrsLL = - "bool \ ('f, 'l, 'v) termsLL \ ('f, 'l, 'v) trsLL" - -datatype (discs_sels) location = H | A | B | R - -type_synonym ('f, 'v) forb_pattern = "('f, 'v) ctxt \ ('f, 'v) term \ location" -type_synonym ('f, 'v) forb_patterns = "('f, 'v) forb_pattern set" - -type_synonym ('f, 'l, 'v) fptrsLL = - "(('f, 'l) lab, 'v) forb_pattern list \ ('f, 'l, 'v) trsLL" - -type_synonym ('f, 'l, 'v) prob = "('f, 'l, 'v) qreltrsLL + ('f, 'l, 'v) dppLL" - -type_synonym ('f, 'a) lpoly_inter = "'f \ nat \ ('a \ 'a list)" -type_synonym ('f, 'a) lpoly_interL = "(('f \ nat) \ ('a \ 'a list)) list" - -type_synonym 'v monom = "('v \ nat) list" -type_synonym ('v, 'a) poly = "('v monom \ 'a) list" -type_synonym ('f, 'a) poly_inter_list = "(('f \ nat) \ (nat, 'a) poly) list" -type_synonym 'a vec = "'a list" -type_synonym 'a mat = "'a vec list" - -datatype (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 \ nat) \ (nat \ order_tag)) list" - -datatype (discs_sels) af_entry = - Collapse nat - | AFList "nat list" - -type_synonym 'f afs_list = "(('f \ nat) \ af_entry) list" -type_synonym 'f prec_weight_repr = "(('f \ nat) \ (nat \ nat \ (nat list option))) list \ nat" - -datatype (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 \ nat) \ (nat \ 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 \ nat) \ 'f list) list" -type_synonym ('f, 'v) uncurry_info = "'f \ 'f sig_map_list \ ('f, 'v) rules \ ('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 \ nat) \ arithFun) list" -datatype (discs_sels) ('f, 'v) sl_variant = - Rootlab "('f \ nat) option" - | Finitelab "'f sl_inter" - | QuasiFinitelab "'f sl_inter" 'v - -type_synonym ('f, 'v) crit_pair_joins = "(('f, 'v) term \ ('f, 'v) rseq \ ('f, 'v) term \ ('f, 'v) rseq) list" - -datatype (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 \ ('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 \ ('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 \ (('f, 'v) term \ 'v list) list \ ('f, 'v) cond_constraint \ ('f, 'v) cond_constraint_prf) list" - -datatype (discs_sels) ('f, 'v) cond_red_pair_prf = - Cond_Red_Pair_Prf - 'f "(('f, 'v) cond_constraint \ ('f, 'v) rules \ ('f, 'v) cond_constraint_prf) list" nat nat - -datatype (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \ _") -datatype (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \ 'q) list" -datatype (discs_sels) 'q ta_relation = - Decision_Proc - | Id_Relation - | Some_Relation "('q \ 'q) list" - -datatype (discs_sels) boundstype = Roof | Match -datatype (discs_sels) ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \ 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 \ ('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 \ bool" where - "satisfied (SN_TRS t) = (t = t)" -| "satisfied (SN_FP_TRS t) = (t \ t)" -| "satisfied (Finite_DPP d) = (d \ d)" -| "satisfied (Unknown_Problem s) = (s = ''foo'')" -| "satisfied (Not_SN_TRS (nfs, q, r)) = (length q = length r)" -| "satisfied (Not_RelSN_TRS (nfs, q, r, rw)) = (r = rw)" -| "satisfied (Infinite_DPP d) = (d = d)" -| "satisfied (Not_SN_FP_TRS t) = (t = t)" - -fun collect_assms :: "('tp \ ('f, 'l, 'v) assm list) - \ ('dpp \ ('f, 'l, 'v) assm list) - \ ('fptp \ ('f, 'l, 'v) assm list) - \ ('unk \ ('f, 'l, 'v) assm list) - \ ('f, 'l, 'v, 'tp, 'dpp, 'fptp, 'unk) assm_proof \ ('f, 'l, 'v) assm list" where - "collect_assms tp dpp fptp unk (SN_assm_proof t prf) = tp prf" -| "collect_assms tp dpp fptp unk (SN_FP_assm_proof t prf) = fptp prf" -| "collect_assms tp dpp fptp unk (Finite_assm_proof d prf) = dpp prf" -| "collect_assms tp dpp fptp unk (Unknown_assm_proof p prf) = unk prf" -| "collect_assms _ _ _ _ _ = []" - -fun collect_neg_assms :: "('tp \ ('f, 'l, 'v) assm list) - \ ('dpp \ ('f, 'l, 'v) assm list) - \ ('rtp \ ('f, 'l, 'v) assm list) - \ ('fptp \ ('f, 'l, 'v) assm list) - \ ('unk \ ('f, 'l, 'v) assm list) - \ ('f, 'l, 'v, 'tp, 'dpp, 'rtp, 'fptp, 'unk) generic_assm_proof \ ('f, 'l, 'v) assm list" where - "collect_neg_assms tp dpp rtp fptp unk (Not_SN_assm_proof t prf) = tp prf" -| "collect_neg_assms tp dpp rtp fptp unk (Infinite_assm_proof d prf) = dpp prf" -| "collect_neg_assms tp dpp rtp fptp unk (Not_RelSN_assm_proof t prf) = rtp prf" -| "collect_neg_assms tp dpp rtp fptp unk (Not_SN_FP_assm_proof t prf) = fptp prf" -| "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf" -| "collect_neg_assms tp dpp rtp fptp unk _ = []" - -datatype (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 \ ('f, 'l, 'v) trsLL) list" - | Mono_Redpair_Proc "('f, 'l) lab redtriple_impl" - "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" - | Mono_Redpair_UR_Proc "('f, 'l) lab redtriple_impl" - "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" - | Size_Change_Subterm_Proc "((('f, 'l) lab, 'v) rule \ ((nat \ nat) list \ (nat \ nat) list)) list" - | Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option" - "((('f, 'l) lab, 'v) rule \ ((nat \ nat) list \ (nat \ nat) list)) list" - | Uncurry_Proc "nat option" "(('f, 'l) lab, 'v) uncurry_info" - "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" - | Fcc_Proc "('f, 'l) lab" "(('f, 'l) lab, 'v) ctxt list" - "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" - | Split_Proc - "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" - "('f, 'l, 'v) dp_termination_proof" "('f, 'l, 'v) dp_termination_proof" - | Semlab_Proc - "(('f, 'l) lab, 'v) sl_variant" "('f, 'l, 'v) trsLL" - "(('f, 'l) lab, 'v) term list" "('f, 'l, 'v) trsLL" - "('f, 'l, 'v) dp_termination_proof" - | Switch_Innermost_Proc "('f, 'l) lab join_info" "('f, 'l, 'v) dp_termination_proof" - | Rewriting_Proc - "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" - "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) dp_termination_proof" - | Instantiation_Proc "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" - | Forward_Instantiation_Proc - "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_termination_proof" - | Narrowing_Proc "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" - | Assume_Finite - "('f, 'l, 'v) dppLL" "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list" - | Unlab_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" - | Q_Reduction_Proc "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_termination_proof" - | Complex_Constant_Removal_Proc "(('f, 'l) lab, 'v) complex_constant_removal_prf" "('f, 'l, 'v) dp_termination_proof" - | General_Redpair_Proc - "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" - "(('f, 'l) lab, 'v) cond_red_pair_prf" "('f, 'l, 'v) dp_termination_proof list" - | To_Trs_Proc "('f, 'l, 'v) trs_termination_proof" -and ('f, 'l, 'v) trs_termination_proof = - DP_Trans bool bool "(('f, 'l) lab, 'v) rules" "('f, 'l, 'v) dp_termination_proof" - | Rule_Removal "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" - | String_Reversal "('f, 'l, 'v) trs_termination_proof" - | Bounds "(('f, 'l) lab, 'v) bounds_info" - | Uncurry "(('f, 'l) lab, 'v) uncurry_info" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" - | Semlab - "(('f, 'l) lab, 'v) sl_variant" "(('f, 'l) lab, 'v) term list" - "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" - | R_is_Empty - | Fcc "(('f, 'l) lab, 'v) ctxt list" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" - | Split "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" "('f, 'l, 'v) trs_termination_proof" - | Switch_Innermost "('f, 'l) lab join_info" "('f, 'l, 'v) trs_termination_proof" - | Drop_Equality "('f, 'l, 'v) trs_termination_proof" - | Remove_Nonapplicable_Rules "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" - | Assume_SN "('f, 'l, 'v) qreltrsLL" "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list" -and ('f, 'l, 'v) unknown_proof = - Assume_Unknown unknown_info "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list" -and ('f, 'l, 'v) fptrs_termination_proof = - Assume_FP_SN "('f, 'l, 'v) fptrsLL" "('f, 'l, 'v, ('f, 'l, 'v) trs_termination_proof, ('f, 'l, 'v) dp_termination_proof, ('f, 'l, 'v) fptrs_termination_proof, ('f, 'l, 'v) unknown_proof) assm_proof list" - -end diff -r 747fc3692fca -r 705d4c4003ea src/HOL/Datatype_Examples/Misc_N2M.thy --- 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 \Miscellaneous Tests for the Nested-to-Mutual Reduction\ - -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 \ 'a tr li" - -primrec (nonexhaustive) - f_tl :: "'a \ 'a tr li \ nat" and - f_t :: "'a \ 'a tr \ 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 \ nat" and - f_t2 :: "('a, 'a) t \ 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 \ nat" and - g_tlb :: "(('a, 'b) t, 'b) l \ nat" and - g_t :: "('a, 'b) t \ 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 \ ('a, 'b) t1) l1" and - ('a, 'b) t2 = T2 "('a, 'b) t1" - -primrec - h1_tl1 :: "(nat, 'a) t1 l1 \ nat" and - h1_natl1 :: "(nat \ (nat, 'a) t1) l1 \ nat" and - h1_t1 :: "(nat, 'a) t1 \ 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 \ 'a G" -and fK :: "('a G, 'a G N) K \ ('a G, 'a G N) K" -and fL :: "('a G, 'a G N) L \ ('a G, 'a G N) L" -and fM :: "'a G M \ '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 \ 'a G" -and fK :: "('a G, 'a G N) K \ ('a G, 'a G N) K" -and fL :: "('a G, 'a G N) L \ ('a G, 'a G N) L" -and fM :: "'a G M \ '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 \Deep Nesting\ - -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 \Primrec cache\ - -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 \ nat" and - f1_t :: "(nat, 'a) t \ 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 \ nat" and - f2_tl :: "(nat, 'b) t l \ 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 \ nat" and - g1_tl :: "('a, int) t l \ 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 \ nat" and - g2_tl :: "(int, int) t l \ 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 \ 'a" and - sum_l2 :: "'a::{zero,plus} l2 \ '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 \ nat" and - h1_tl2 :: "(nat, 'a) t1 l2 \ nat" and - h1_t1 :: "(nat, 'a) t1 \ 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 \ nat" and - h2_tl2 :: "(nat, 'a) t1 l2 \ nat" and - h2_t1 :: "(nat, 'a) t1 \ 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 \ nat" and - h3_tl1 :: "(nat, 'a) t1 l1 \ nat" and - h3_t1 :: "(nat, 'a) t1 \ 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 \ nat" and - i1_tl1 :: "(nat, 'a) t1 l1 \ nat" and - i1_t1 :: "(nat, 'a) t1 \ nat" and - i1_t2 :: "(nat, 'a) t2 \ 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 \ nat" and - j1_t1 :: "(nat, 'a) t1 \ nat" and - j1_tl1 :: "(nat, 'a) t1 l1 \ nat" and - j1_tl2 :: "(nat, 'a) t1 l2 \ 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 \ nat" and - k1_tl4 :: "(nat, 'a) t3 l4 \ nat" and - k1_t3 :: "(nat, 'a) t3 \ 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 \ nat" and - k2_tl3 :: "(nat, int) t3 l3 \ nat" and - k2_t3 :: "(nat, int) t3 \ 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 \ nat" and - l1_tl6 :: "((nat, 'a, 'b) t4, 'b) l6 \ nat" and - l1_t4 :: "(nat, 'a, 'b) t4 \ 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 \Primcorec Cache\ - -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 \ (nat, 'a) cot col" and - f1_cot :: "nat \ (nat, 'a) cot" -where - "n = 0 \ f1_cotcol n = N" | - "_ \ 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 \ (nat, 'b) cot col" and - f2_cot :: "nat \ (nat, 'b) cot" -where - "n = 0 \ f2_cotcol n = N" | - "_ \ 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 \ (int, 'a) cot" and - g1_cotcol :: "int \ (int, 'a) cot col" -where - "g1_cot n = T n undefined (g1_cotcol n)" | - "n = 0 \ g1_cotcol n = N" | - "_ \ g1_cotcol n = C (g1_cot n) (g1_cotcol n)" - -(* should be fast *) -primcorec - g2_cot :: "int \ (int, int) cot" and - g2_cotcol :: "int \ (int, int) cot col" -where - "g2_cot n = T n undefined (g2_cotcol n)" | - "n = 0 \ g2_cotcol n = N" | - "_ \ 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 \ (nat, 'a) cot1 col1" and - h1_cotcol2 :: "nat \ (nat, 'a) cot1 col2" and - h1_cot1 :: "nat \ (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 \ (nat, 'a) cot1 col1" and - h2_cotcol2 :: "nat \ (nat, 'a) cot1 col2" and - h2_cot1 :: "nat \ (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 \ (nat, 'a) cot1 col2" and - h3_cotcol1 :: "nat \ (nat, 'a) cot1 col1" and - h3_cot1 :: "nat \ (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 \ (nat, 'a) cot1 col2" and - i1_cotcol1 :: "nat \ (nat, 'a) cot1 col1" and - i1_cot1 :: "nat \ (nat, 'a) cot1" and - i1_cot2 :: "nat \ (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 \ (nat, 'a) cot2" and - j1_cot1 :: "nat \ (nat, 'a) cot1" and - j1_cotcol1 :: "nat \ (nat, 'a) cot1 col1" and - j1_cotcol2 :: "nat \ (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 \ (nat, 'a) cot3 col3" and - k1_cotcol4 :: "nat \ (nat, 'a) cot3 col4" and - k1_cot3 :: "nat \ (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 \ (nat, 'a) cot3 col4" and - k2_cotcol3 :: "nat \ (nat, 'a) cot3 col3" and - k2_cot3 :: "nat \ (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 diff -r 747fc3692fca -r 705d4c4003ea src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy --- 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 diff -r 747fc3692fca -r 705d4c4003ea src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy --- 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\_,/ _\)") -translations - "\x, y, z\" == "\x, \y, z\\" - "\x, y\" == "CONST MPair x y" - -inductive_set - parts :: "msg set => msg set" - for H :: "msg set" - where - Inj [intro]: "X \ H ==> X \ parts H" - | Fst: "\X,Y\ \ parts H ==> X \ parts H" - | Snd: "\X,Y\ \ parts H ==> Y \ parts H" - | Body: "Crypt K X \ parts H ==> X \ parts H" - -inductive_set - analz :: "msg set => msg set" - for H :: "msg set" - where - Inj [intro,simp] : "X \ H ==> X \ analz H" - | Fst: "\X,Y\ \ analz H ==> X \ analz H" - | Snd: "\X,Y\ \ analz H ==> Y \ analz H" - | Decrypt [dest]: - "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" - -inductive_set - synth :: "msg set => msg set" - for H :: "msg set" - where - Inj [intro]: "X \ H ==> X \ synth H" - | Agent [intro]: "Agent agt \ synth H" - | MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> \X,Y\ \ synth H" - | Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" - -primrec initState -where - initState_Alice: - "initState Alice = {Key (priEK Alice)} \ (Key ` pubEK ` agents)" -| initState_Bob: - "initState Bob = {Key (priEK Bob)} \ (Key ` pubEK ` agents)" -| initState_Spy: - "initState Spy = (Key ` priEK ` bad) \ (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' \ 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 [] = \(parts ` initState ` agents)" -| used_Cons: "used (ev # evs) = - (case ev of - Says A B X => parts {X} \ used evs - | Gets A X => used evs - | Notes A X => parts {X} \ 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 \ (\((%m. case m of \X, Y\ => {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 \ (\((%m. case m of \X, Y\ => {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 diff -r 747fc3692fca -r 705d4c4003ea src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy --- 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: "[] \ ns_public" - - | Fake_NS1: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1) \ - \ Says Spy B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - | Fake_NS2: "\evs1 \ ns_public; Nonce NA \ analz (spies evs1); Nonce NB \ analz (spies evs1) \ - \ Says Spy A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs1 \ ns_public" - - (*Alice initiates a protocol run, sending a nonce to Bob*) - | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ - \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - (*Bob responds to Alice's message with a further nonce*) - | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; - Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs2 \ ns_public" - - (*Alice proves her existence by sending NB back to Bob.*) - | NS3: "\evs3 \ ns_public; - Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; - Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ - \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 - "\ns_publicp evs\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs - \ A \ Spy \ B \ Spy \ A \ B - \ Nonce NB \ 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) \Nonce 0, Nonce 1\), - Says Spy Bob (Crypt (pubEK Bob) \Nonce 0, Agent Alice\), - Says Alice Spy (Crypt (pubEK Spy) \Nonce 0, Agent Alice\)]" (is "_ = [?e3, ?e2, ?e1, ?e0]") - shows "A \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" -proof - - from assms show "A \ Spy" by auto - from assms show "B \ 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) \Nonce 0, Agent Alice\) \ 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) \Nonce 0, Agent Alice\) \ set [?e2, ?e1, ?e0]" by simp - show "Says Bob Alice (Crypt (pubEK Alice) \Nonce 0, Nonce 1\) - : 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 diff -r 747fc3692fca -r 705d4c4003ea src/HOL/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy --- 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: "[] \ ns_public" - (*Alice initiates a protocol run, sending a nonce to Bob*) - | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ - \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - (*Bob responds to Alice's message with a further nonce*) - | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; - Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs2 \ ns_public" - - (*Alice proves her existence by sending NB back to Bob.*) - | NS3: "\evs3 \ ns_public; - Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; - Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ - \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 - "\ns_publicp evs\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs - \ A \ Spy \ B \ Spy \ A \ B - \ Nonce NB \ analz (spies evs)" -quickcheck[smart_exhaustive, depth = 6, timeout = 30] -quickcheck[narrowing, size = 6, timeout = 30, verbose] -oops - -end diff -r 747fc3692fca -r 705d4c4003ea src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy --- 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: "[] \ ns_public" - - | Fake: "\evs1 \ ns_public; X \ synth (analz (spies evs1)) \ - \ Says Spy A X # evs1 \ ns_public" - - (*Alice initiates a protocol run, sending a nonce to Bob*) - | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ - \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - (*Bob responds to Alice's message with a further nonce*) - | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; - Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) - # evs2 \ ns_public" - - (*Alice proves her existence by sending NB back to Bob.*) - | NS3: "\evs3 \ ns_public; - Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; - Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ - \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ 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 ==> \ (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 - "\ns_publicp evs\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) : set evs - \ A \ Spy \ B \ Spy \ A \ B - \ Nonce NB \ 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) \Nonce 0, Nonce 1\), - Says Spy Bob (Crypt (pubEK Bob) \Nonce 0, Agent Alice\), - Says Alice Spy (Crypt (pubEK Spy) \Nonce 0, Agent Alice\)]" (is "_ = [?e3, ?e2, ?e1, ?e0]") - shows "A \ Spy" "B \ Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" -proof - - from assms show "A \ Spy" by auto - from assms show "B \ 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) \Nonce 0, Agent Alice\ : 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) \Nonce 0, Agent Alice\) \ 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) \Nonce 0, Agent Alice\) \ set [?e2, ?e1, ?e0]" by simp - show "Says Bob Alice (Crypt (pubEK Alice) \Nonce 0, Nonce 1\) : 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 diff -r 747fc3692fca -r 705d4c4003ea src/HOL/ROOT --- 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 - diff -r 747fc3692fca -r 705d4c4003ea src/HOL/Record_Benchmark/Record_Benchmark.thy --- 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\A255:=x\) = A155 r" - by simp - -lemma "A155 (r\A255:=x,A253:=y,A255:=z \) = A155 r" - by simp - -lemma "(r\A255:=x,A253:=y,A255:=z \) = r\A253:=y,A255:=z\" - by simp - -lemma "(r\A255:=x,A253:=y,A255:=z \) = r\A253:=y,A255:=z\" - apply (tactic {* simp_tac - (put_simpset HOL_basic_ss @{context} addsimprocs [Record.upd_simproc]) 1*}) - done - -lemma "(\r. P (A155 r)) \ (\x. P x)" - apply (tactic {* simp_tac - (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*}) - apply simp - done - -lemma "(\r. P (A155 r)) \ (\x. P x)" - apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) - apply simp - done - -lemma "(\r. P (A155 r)) \ (\x. P x)" - apply (tactic {* simp_tac - (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*}) - apply simp - done - -lemma "(\r. P (A155 r)) \ (\x. P x)" - apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) - apply simp - done - -lemma "\r. P (A155 r) \ (\x. P x)" - apply (tactic {* simp_tac - (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*}) - apply auto - done - -lemma "\r. P (A155 r) \ (\x. P x)" - apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) - apply auto - done - -lemma "P (A155 r) \ (\x. P x)" - apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) - apply auto - done - -lemma fixes r shows "P (A155 r) \ (\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 "\x. P x" - apply - - apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*}) - apply auto - done -end - - -lemma "\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