tuned whitespace;
authorwenzelm
Thu Feb 20 19:32:20 2014 +0100 (2014-02-20)
changeset 5562795c8ef02f04b
parent 55626 0e2b7f04c944
child 55628 8103021024c1
tuned whitespace;
src/Tools/coherent.ML
src/Tools/cong_tac.ML
src/Tools/intuitionistic.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/Tools/coherent.ML	Thu Feb 20 18:23:32 2014 +0100
     1.2 +++ b/src/Tools/coherent.ML	Thu Feb 20 19:32:20 2014 +0100
     1.3 @@ -91,80 +91,82 @@
     1.4    let
     1.5      val vs = fold Term.add_vars (maps snd cs) [];
     1.6      fun insts [] inst = Seq.single inst
     1.7 -      | insts ((ixn, T) :: vs') inst = Seq.maps
     1.8 -          (fn t => insts vs' (((ixn, T), t) :: inst))
     1.9 -          (Seq.of_list (case Typtab.lookup dom T of
    1.10 -             NONE => error ("Unknown domain: " ^
    1.11 -               Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
    1.12 -               commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
    1.13 -           | SOME ts => ts))
    1.14 -  in Seq.map (fn inst =>
    1.15 -    (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
    1.16 -      (insts vs [])
    1.17 +      | insts ((ixn, T) :: vs') inst =
    1.18 +          Seq.maps (fn t => insts vs' (((ixn, T), t) :: inst))
    1.19 +            (Seq.of_list
    1.20 +              (case Typtab.lookup dom T of
    1.21 +                NONE =>
    1.22 +                  error ("Unknown domain: " ^
    1.23 +                    Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
    1.24 +                    commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
    1.25 +              | SOME ts => ts))
    1.26 +  in
    1.27 +    Seq.map (fn inst =>
    1.28 +      (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
    1.29 +        (insts vs [])
    1.30    end;
    1.31  
    1.32  (* Check whether disjunction is valid in given state *)
    1.33  fun is_valid_disj ctxt facts [] = false
    1.34    | is_valid_disj ctxt facts ((Ts, ts) :: ds) =
    1.35 -      let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts
    1.36 -      in case Seq.pull (valid_conj ctxt facts empty_env
    1.37 -        (map (fn t => subst_bounds (rev vs, t)) ts)) of
    1.38 +      let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts in
    1.39 +        (case Seq.pull (valid_conj ctxt facts empty_env
    1.40 +            (map (fn t => subst_bounds (rev vs, t)) ts)) of
    1.41            SOME _ => true
    1.42 -        | NONE => is_valid_disj ctxt facts ds
    1.43 +        | NONE => is_valid_disj ctxt facts ds)
    1.44        end;
    1.45  
    1.46  val show_facts = Unsynchronized.ref false;
    1.47  
    1.48 -fun string_of_facts ctxt s facts = space_implode "\n"
    1.49 -  (s :: map (Syntax.string_of_term ctxt)
    1.50 -     (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
    1.51 +fun string_of_facts ctxt s facts =
    1.52 +  space_implode "\n"
    1.53 +    (s :: map (Syntax.string_of_term ctxt)
    1.54 +      (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
    1.55  
    1.56  fun print_facts ctxt facts =
    1.57    if !show_facts then message (fn () => string_of_facts ctxt "Facts:" facts)
    1.58    else ();
    1.59  
    1.60  fun valid ctxt rules goal dom facts nfacts nparams =
    1.61 -  let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
    1.62 -    valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
    1.63 -      let val cs' = map (fn (Ts, ts) =>
    1.64 -        (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
    1.65 -      in
    1.66 -        inst_extra_vars ctxt dom cs' |>
    1.67 -          Seq.map_filter (fn (inst, cs'') =>
    1.68 -            if is_valid_disj ctxt facts cs'' then NONE
    1.69 -            else SOME (th, env, inst, is, cs''))
    1.70 -      end))
    1.71 +  let
    1.72 +    val seq =
    1.73 +      Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
    1.74 +        valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
    1.75 +          let val cs' = map (fn (Ts, ts) =>
    1.76 +            (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
    1.77 +          in
    1.78 +            inst_extra_vars ctxt dom cs' |>
    1.79 +              Seq.map_filter (fn (inst, cs'') =>
    1.80 +                if is_valid_disj ctxt facts cs'' then NONE
    1.81 +                else SOME (th, env, inst, is, cs''))
    1.82 +          end));
    1.83    in
    1.84 -    case Seq.pull seq of
    1.85 +    (case Seq.pull seq of
    1.86        NONE => (tracing (string_of_facts ctxt "Countermodel found:" facts); NONE)
    1.87      | SOME ((th, env, inst, is, cs), _) =>
    1.88          if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, []))
    1.89          else
    1.90            (case valid_cases ctxt rules goal dom facts nfacts nparams cs of
    1.91 -             NONE => NONE
    1.92 -           | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs)))
    1.93 +            NONE => NONE
    1.94 +          | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs))))
    1.95    end
    1.96  
    1.97  and valid_cases ctxt rules goal dom facts nfacts nparams [] = SOME []
    1.98    | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
    1.99        let
   1.100          val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
   1.101 -        val params = map_index (fn (i, T) =>
   1.102 -          Free ("par" ^ string_of_int (nparams + i), T)) Ts;
   1.103 -        val ts' = map_index (fn (i, t) =>
   1.104 -          (subst_bounds (rev params, t), nfacts + i)) ts;
   1.105 -        val dom' = fold (fn (T, p) =>
   1.106 -          Typtab.map_default (T, []) (fn ps => ps @ [p]))
   1.107 -            (Ts ~~ params) dom;
   1.108 -        val facts' = fold (fn (t, i) => Net.insert_term op =
   1.109 -          (t, (t, i))) ts' facts
   1.110 +        val params = map_index (fn (i, T) => Free ("par" ^ string_of_int (nparams + i), T)) Ts;
   1.111 +        val ts' = map_index (fn (i, t) => (subst_bounds (rev params, t), nfacts + i)) ts;
   1.112 +        val dom' =
   1.113 +          fold (fn (T, p) => Typtab.map_default (T, []) (fn ps => ps @ [p])) (Ts ~~ params) dom;
   1.114 +        val facts' = fold (fn (t, i) => Net.insert_term op = (t, (t, i))) ts' facts;
   1.115        in
   1.116 -        case valid ctxt rules goal dom' facts'
   1.117 -          (nfacts + length ts) (nparams + length Ts) of
   1.118 +        (case valid ctxt rules goal dom' facts' (nfacts + length ts) (nparams + length Ts) of
   1.119            NONE => NONE
   1.120 -        | SOME prf => (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
   1.121 -            NONE => NONE
   1.122 -          | SOME prfs => SOME ((params, prf) :: prfs))
   1.123 +        | SOME prf =>
   1.124 +            (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
   1.125 +              NONE => NONE
   1.126 +            | SOME prfs => SOME ((params, prf) :: prfs)))
   1.127        end;
   1.128  
   1.129  
   1.130 @@ -172,37 +174,41 @@
   1.131  
   1.132  fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
   1.133    let
   1.134 -    val _ = message (fn () => space_implode "\n"
   1.135 -      ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
   1.136 -    val th' = Drule.implies_elim_list
   1.137 -      (Thm.instantiate
   1.138 -         (map (fn (ixn, (S, T)) =>
   1.139 -            (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
   1.140 -               (Vartab.dest tye),
   1.141 -          map (fn (ixn, (T, t)) =>
   1.142 -            (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
   1.143 -             Thm.cterm_of thy t)) (Vartab.dest env) @
   1.144 -          map (fn (ixnT, t) =>
   1.145 -            (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
   1.146 -      (map (nth asms) is);
   1.147 -    val (_, cases) = dest_elim (prop_of th')
   1.148 +    val _ =
   1.149 +      message (fn () => space_implode "\n"
   1.150 +        ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
   1.151 +    val th' =
   1.152 +      Drule.implies_elim_list
   1.153 +        (Thm.instantiate
   1.154 +           (map (fn (ixn, (S, T)) =>
   1.155 +              (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
   1.156 +                 (Vartab.dest tye),
   1.157 +            map (fn (ixn, (T, t)) =>
   1.158 +              (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
   1.159 +               Thm.cterm_of thy t)) (Vartab.dest env) @
   1.160 +            map (fn (ixnT, t) =>
   1.161 +              (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
   1.162 +        (map (nth asms) is);
   1.163 +    val (_, cases) = dest_elim (prop_of th');
   1.164    in
   1.165 -    case (cases, prfs) of
   1.166 +    (case (cases, prfs) of
   1.167        ([([], [_])], []) => th'
   1.168      | ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf
   1.169 -    | _ => Drule.implies_elim_list
   1.170 -        (Thm.instantiate (Thm.match
   1.171 -           (Drule.strip_imp_concl (cprop_of th'), goal)) th')
   1.172 -        (map (thm_of_case_prf thy goal asms) (prfs ~~ cases))
   1.173 +    | _ =>
   1.174 +        Drule.implies_elim_list
   1.175 +          (Thm.instantiate (Thm.match
   1.176 +             (Drule.strip_imp_concl (cprop_of th'), goal)) th')
   1.177 +          (map (thm_of_case_prf thy goal asms) (prfs ~~ cases)))
   1.178    end
   1.179  
   1.180  and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) =
   1.181    let
   1.182      val cparams = map (cterm_of thy) params;
   1.183 -    val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms'
   1.184 +    val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms';
   1.185    in
   1.186 -    Drule.forall_intr_list cparams (Drule.implies_intr_list asms''
   1.187 -      (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf))
   1.188 +    Drule.forall_intr_list cparams
   1.189 +      (Drule.implies_intr_list asms''
   1.190 +        (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf))
   1.191    end;
   1.192  
   1.193  
   1.194 @@ -211,15 +217,16 @@
   1.195  fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
   1.196    rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN
   1.197    SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
   1.198 -    let val xs = map (term_of o #2) params @
   1.199 -      map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
   1.200 -        (rev (Variable.dest_fixes ctxt''))  (* FIXME !? *)
   1.201 +    let
   1.202 +      val xs =
   1.203 +        map (term_of o #2) params @
   1.204 +        map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
   1.205 +          (rev (Variable.dest_fixes ctxt''))  (* FIXME !? *)
   1.206      in
   1.207 -      case valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
   1.208 +      (case valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
   1.209             (mk_dom xs) Net.empty 0 0 of
   1.210 -         NONE => no_tac
   1.211 -       | SOME prf =>
   1.212 -           rtac (thm_of_cl_prf (Proof_Context.theory_of ctxt'') concl [] prf) 1
   1.213 +        NONE => no_tac
   1.214 +      | SOME prf => rtac (thm_of_cl_prf (Proof_Context.theory_of ctxt'') concl [] prf) 1)
   1.215      end) ctxt' 1) ctxt;
   1.216  
   1.217  val setup = Method.setup @{binding coherent}
     2.1 --- a/src/Tools/cong_tac.ML	Thu Feb 20 18:23:32 2014 +0100
     2.2 +++ b/src/Tools/cong_tac.ML	Thu Feb 20 19:32:20 2014 +0100
     2.3 @@ -21,14 +21,15 @@
     2.4        _ $ (_ $ (f $ x) $ (g $ y)) =>
     2.5          let
     2.6            val cong' = Thm.lift_rule cgoal cong;
     2.7 -          val _ $ (_ $ (f' $ x') $ (g' $ y')) =
     2.8 -            Logic.strip_assums_concl (Thm.prop_of cong');
     2.9 +          val _ $ (_ $ (f' $ x') $ (g' $ y')) = Logic.strip_assums_concl (Thm.prop_of cong');
    2.10            val ps = Logic.strip_params (Thm.concl_of cong');
    2.11 -          val insts = [(f', f), (g', g), (x', x), (y', y)]
    2.12 +          val insts =
    2.13 +            [(f', f), (g', g), (x', x), (y', y)]
    2.14              |> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
    2.15          in
    2.16 -          fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
    2.17 -            handle THM _ => no_tac st
    2.18 +          fn st =>
    2.19 +            compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
    2.20 +              handle THM _ => no_tac st
    2.21          end
    2.22      | _ => no_tac)
    2.23    end);
     3.1 --- a/src/Tools/intuitionistic.ML	Thu Feb 20 18:23:32 2014 +0100
     3.2 +++ b/src/Tools/intuitionistic.ML	Thu Feb 20 19:32:20 2014 +0100
     3.3 @@ -42,17 +42,20 @@
     3.4    REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
     3.5    REMDUPS (unsafe_step_tac ctxt) i;
     3.6  
     3.7 -fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else
     3.8 -  let
     3.9 -    val ps = Logic.strip_assums_hyp g;
    3.10 -    val c = Logic.strip_assums_concl g;
    3.11 -  in
    3.12 -    if member (fn ((ps1, c1), (ps2, c2)) =>
    3.13 -        c1 aconv c2 andalso
    3.14 -        length ps1 = length ps2 andalso
    3.15 -        eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
    3.16 -    else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
    3.17 -  end);
    3.18 +fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) =>
    3.19 +  if d > lim then no_tac
    3.20 +  else
    3.21 +    let
    3.22 +      val ps = Logic.strip_assums_hyp g;
    3.23 +      val c = Logic.strip_assums_concl g;
    3.24 +    in
    3.25 +      if member (fn ((ps1, c1), (ps2, c2)) =>
    3.26 +          c1 aconv c2 andalso
    3.27 +          length ps1 = length ps2 andalso
    3.28 +          eq_set (op aconv) (ps1, ps2)) gs (ps, c)
    3.29 +      then no_tac
    3.30 +      else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
    3.31 +    end);
    3.32  
    3.33  in
    3.34  
     4.1 --- a/src/Tools/quickcheck.ML	Thu Feb 20 18:23:32 2014 +0100
     4.2 +++ b/src/Tools/quickcheck.ML	Thu Feb 20 19:32:20 2014 +0100
     4.3 @@ -83,11 +83,11 @@
     4.4  structure Quickcheck : QUICKCHECK =
     4.5  struct
     4.6  
     4.7 -val quickcheckN = "quickcheck"
     4.8 +val quickcheckN = "quickcheck";
     4.9  
    4.10 -val genuineN = "genuine"
    4.11 -val noneN = "none"
    4.12 -val unknownN = "unknown"
    4.13 +val genuineN = "genuine";
    4.14 +val noneN = "none";
    4.15 +val unknownN = "unknown";
    4.16  
    4.17  
    4.18  (* preferences *)
    4.19 @@ -103,58 +103,63 @@
    4.20  (* quickcheck report *)
    4.21  
    4.22  datatype report = Report of
    4.23 -  { iterations : int, raised_match_errors : int,
    4.24 -    satisfied_assms : int list, positive_concl_tests : int }
    4.25 + {iterations : int,
    4.26 +  raised_match_errors : int,
    4.27 +  satisfied_assms : int list,
    4.28 +  positive_concl_tests : int};
    4.29  
    4.30  
    4.31  (* Quickcheck Result *)
    4.32  
    4.33  datatype result = Result of
    4.34 -  { counterexample : (bool * (string * term) list) option, evaluation_terms : (term * term) list option,
    4.35 -    timings : (string * int) list, reports : (int * report) list}
    4.36 + {counterexample : (bool * (string * term) list) option,
    4.37 +  evaluation_terms : (term * term) list option,
    4.38 +  timings : (string * int) list,
    4.39 +  reports : (int * report) list};
    4.40  
    4.41  val empty_result =
    4.42 -  Result {counterexample = NONE, evaluation_terms = NONE, timings = [], reports = []}
    4.43 +  Result {counterexample = NONE, evaluation_terms = NONE, timings = [], reports = []};
    4.44  
    4.45 -fun counterexample_of (Result r) = #counterexample r
    4.46 +fun counterexample_of (Result r) = #counterexample r;
    4.47  
    4.48 -fun found_counterexample (Result r) = is_some (#counterexample r)
    4.49 +fun found_counterexample (Result r) = is_some (#counterexample r);
    4.50  
    4.51 -fun response_of (Result r) = case (#counterexample r, #evaluation_terms r) of
    4.52 +fun response_of (Result r) =
    4.53 +  (case (#counterexample r, #evaluation_terms r) of
    4.54      (SOME ts, SOME evals) => SOME (ts, evals)
    4.55 -  | (NONE, NONE) => NONE
    4.56 +  | (NONE, NONE) => NONE);
    4.57  
    4.58 -fun timings_of (Result r) = #timings r
    4.59 +fun timings_of (Result r) = #timings r;
    4.60  
    4.61  fun set_response names eval_terms (SOME (genuine, ts)) (Result r) =
    4.62 -  let
    4.63 -    val (ts1, ts2) = chop (length names) ts
    4.64 -    val (eval_terms', _) = chop (length ts2) eval_terms
    4.65 -  in
    4.66 -    Result {counterexample = SOME (genuine, (names ~~ ts1)),
    4.67 -      evaluation_terms = SOME (eval_terms' ~~ ts2),
    4.68 -      timings = #timings r, reports = #reports r}
    4.69 -  end
    4.70 -  | set_response _ _ NONE result = result
    4.71 +      let
    4.72 +        val (ts1, ts2) = chop (length names) ts
    4.73 +        val (eval_terms', _) = chop (length ts2) eval_terms
    4.74 +      in
    4.75 +        Result {counterexample = SOME (genuine, (names ~~ ts1)),
    4.76 +          evaluation_terms = SOME (eval_terms' ~~ ts2),
    4.77 +          timings = #timings r, reports = #reports r}
    4.78 +      end
    4.79 +  | set_response _ _ NONE result = result;
    4.80  
    4.81  
    4.82  fun cons_timing timing (Result r) =
    4.83    Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
    4.84 -    timings = cons timing (#timings r), reports = #reports r}
    4.85 +    timings = cons timing (#timings r), reports = #reports r};
    4.86  
    4.87  fun cons_report size (SOME report) (Result r) =
    4.88 -  Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
    4.89 -    timings = #timings r, reports = cons (size, report) (#reports r)}
    4.90 -  | cons_report _ NONE result = result
    4.91 +      Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
    4.92 +        timings = #timings r, reports = cons (size, report) (#reports r)}
    4.93 +  | cons_report _ NONE result = result;
    4.94  
    4.95  fun add_timing timing result_ref =
    4.96 -  Unsynchronized.change result_ref (cons_timing timing)
    4.97 +  Unsynchronized.change result_ref (cons_timing timing);
    4.98  
    4.99  fun add_report size report result_ref =
   4.100 -  Unsynchronized.change result_ref (cons_report size report)
   4.101 +  Unsynchronized.change result_ref (cons_report size report);
   4.102  
   4.103  fun add_response names eval_terms response result_ref =
   4.104 -  Unsynchronized.change result_ref (set_response names eval_terms response)
   4.105 +  Unsynchronized.change result_ref (set_response names eval_terms response);
   4.106  
   4.107  
   4.108  (* expectation *)
   4.109 @@ -162,33 +167,33 @@
   4.110  datatype expectation = No_Expectation | No_Counterexample | Counterexample;
   4.111  
   4.112  fun merge_expectation (expect1, expect2) =
   4.113 -  if expect1 = expect2 then expect1 else No_Expectation
   4.114 +  if expect1 = expect2 then expect1 else No_Expectation;
   4.115  
   4.116  (*quickcheck configuration -- default parameters, test generators*)
   4.117 -val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "")
   4.118 -val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10)
   4.119 -val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100)
   4.120 -val depth = Attrib.setup_config_int @{binding quickcheck_depth} (K 10)
   4.121 +val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "");
   4.122 +val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10);
   4.123 +val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100);
   4.124 +val depth = Attrib.setup_config_int @{binding quickcheck_depth} (K 10);
   4.125  
   4.126 -val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
   4.127 -val locale = Attrib.setup_config_string @{binding quickcheck_locale} (K "interpret expand")
   4.128 -val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
   4.129 -val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
   4.130 -val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
   4.131 +val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false);
   4.132 +val locale = Attrib.setup_config_string @{binding quickcheck_locale} (K "interpret expand");
   4.133 +val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true);
   4.134 +val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false);
   4.135 +val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0);
   4.136  
   4.137 -val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
   4.138 -val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false)
   4.139 +val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false);
   4.140 +val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false);
   4.141  
   4.142 -val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
   4.143 -val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
   4.144 -val tag = Attrib.setup_config_string @{binding quickcheck_tag} (K "")
   4.145 +val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false);
   4.146 +val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false);
   4.147 +val tag = Attrib.setup_config_string @{binding quickcheck_tag} (K "");
   4.148  
   4.149 -val use_subtype = Attrib.setup_config_bool @{binding quickcheck_use_subtype} (K false)
   4.150 +val use_subtype = Attrib.setup_config_bool @{binding quickcheck_use_subtype} (K false);
   4.151  
   4.152  val allow_function_inversion =
   4.153 -  Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false)
   4.154 -val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true)
   4.155 -val finite_type_size = Attrib.setup_config_int @{binding quickcheck_finite_type_size} (K 3)
   4.156 +  Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false);
   4.157 +val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true);
   4.158 +val finite_type_size = Attrib.setup_config_int @{binding quickcheck_finite_type_size} (K 3);
   4.159  
   4.160  datatype test_params = Test_Params of
   4.161    {default_type: typ list, expect : expectation};
   4.162 @@ -213,13 +218,14 @@
   4.163  structure Data = Generic_Data
   4.164  (
   4.165    type T =
   4.166 -    ((string * (bool Config.T * tester)) list
   4.167 -      * ((string * (Proof.context -> term list -> (int -> term list option) list)) list
   4.168 -      * ((string * (Proof.context -> term list -> (int -> bool) list)) list)))
   4.169 -      * test_params;
   4.170 +    ((string * (bool Config.T * tester)) list *
   4.171 +      ((string * (Proof.context -> term list -> (int -> term list option) list)) list *
   4.172 +      ((string * (Proof.context -> term list -> (int -> bool) list)) list))) *
   4.173 +      test_params;
   4.174    val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
   4.175    val extend = I;
   4.176 -  fun merge (((testers1, (batch_generators1, batch_validators1)), params1),
   4.177 +  fun merge
   4.178 +   (((testers1, (batch_generators1, batch_validators1)), params1),
   4.179      ((testers2, (batch_generators2, batch_validators2)), params2)) : T =
   4.180      ((AList.merge (op =) (K true) (testers1, testers2),
   4.181        (AList.merge (op =) (K true) (batch_generators1, batch_generators2),
   4.182 @@ -229,11 +235,11 @@
   4.183  
   4.184  val test_params_of = snd o Data.get o Context.Proof;
   4.185  
   4.186 -val default_type = fst o dest_test_params o test_params_of
   4.187 +val default_type = fst o dest_test_params o test_params_of;
   4.188  
   4.189 -val expect = snd o dest_test_params o test_params_of
   4.190 +val expect = snd o dest_test_params o test_params_of;
   4.191  
   4.192 -val map_test_params = Data.map o apsnd o map_test_params'
   4.193 +val map_test_params = Data.map o apsnd o map_test_params';
   4.194  
   4.195  val add_tester = Data.map o apfst o apfst o AList.update (op =);
   4.196  
   4.197 @@ -243,15 +249,15 @@
   4.198  
   4.199  fun active_testers ctxt =
   4.200    let
   4.201 -    val testers = (map snd o fst o fst o Data.get o Context.Proof) ctxt
   4.202 +    val testers = map snd (fst (fst (Data.get (Context.Proof ctxt))));
   4.203    in
   4.204      map snd (filter (fn (active, _) => Config.get ctxt active) testers)
   4.205 -  end
   4.206 +  end;
   4.207  
   4.208  fun set_active_testers [] gen_ctxt = gen_ctxt
   4.209    | set_active_testers testers gen_ctxt =
   4.210        let
   4.211 -        val registered_testers = (fst o fst o Data.get) gen_ctxt
   4.212 +        val registered_testers = fst (fst (Data.get gen_ctxt));
   4.213        in
   4.214          fold (fn (name, (config, _)) => Config.put_generic config (member (op =) testers name))
   4.215            registered_testers gen_ctxt
   4.216 @@ -281,9 +287,9 @@
   4.217    end;
   4.218  
   4.219  val mk_batch_tester =
   4.220 -  gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt));
   4.221 +  gen_mk_tester (AList.lookup (op =) o fst o snd o fst o Data.get o Context.Proof);
   4.222  val mk_batch_validator =
   4.223 -  gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt));
   4.224 +  gen_mk_tester (AList.lookup (op =) o snd o snd o fst o Data.get o Context.Proof);
   4.225  
   4.226  
   4.227  (* testing propositions *)
   4.228 @@ -293,11 +299,10 @@
   4.229  
   4.230  fun limit timeout (limit_time, is_interactive) f exc () =
   4.231    if limit_time then
   4.232 -      TimeLimit.timeLimit timeout f ()
   4.233 -    handle TimeLimit.TimeOut =>
   4.234 -      if is_interactive then exc () else raise TimeLimit.TimeOut
   4.235 -  else
   4.236 -    f ();
   4.237 +    TimeLimit.timeLimit timeout f ()
   4.238 +      handle TimeLimit.TimeOut =>
   4.239 +        if is_interactive then exc () else raise TimeLimit.TimeOut
   4.240 +  else f ();
   4.241  
   4.242  fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s;
   4.243  
   4.244 @@ -309,11 +314,13 @@
   4.245    (case active_testers ctxt of
   4.246      [] => error "No active testers for quickcheck"
   4.247    | testers =>
   4.248 -    limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
   4.249 -      (fn () => Par_List.get_some (fn tester =>
   4.250 -        tester ctxt (length testers > 1) insts goals |>
   4.251 -        (fn result => if exists found_counterexample result then SOME result else NONE)) testers)
   4.252 -      (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ());
   4.253 +      limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
   4.254 +        (fn () =>
   4.255 +          Par_List.get_some (fn tester =>
   4.256 +            tester ctxt (length testers > 1) insts goals |>
   4.257 +            (fn result => if exists found_counterexample result then SOME result else NONE))
   4.258 +          testers)
   4.259 +        (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ());
   4.260  
   4.261  fun all_axioms_of ctxt t =
   4.262    let
   4.263 @@ -341,7 +348,8 @@
   4.264      val cs = space_explode " " s;
   4.265    in
   4.266      if forall (fn c => c = "expand" orelse c = "interpret") cs then cs
   4.267 -    else (warning ("Invalid quickcheck_locale setting: falling back to the default setting.");
   4.268 +    else
   4.269 +     (warning ("Invalid quickcheck_locale setting: falling back to the default setting.");
   4.270        ["interpret", "expand"])
   4.271    end;
   4.272  
   4.273 @@ -370,18 +378,19 @@
   4.274        (case fst (Locale.specification_of thy locale) of
   4.275          NONE => []
   4.276        | SOME t => the_default [] (all_axioms_of lthy t));
   4.277 -   val config = locale_config_of (Config.get lthy locale);
   4.278 -   val goals =
   4.279 -    (case some_locale of
   4.280 -      NONE => [(proto_goal, eval_terms)]
   4.281 -    | SOME locale =>
   4.282 -        fold (fn c =>
   4.283 -          if c = "expand" then cons (Logic.list_implies (axioms_of locale, proto_goal), eval_terms)
   4.284 -          else if c = "interpret" then
   4.285 -            append (map (fn (_, phi) =>
   4.286 -                (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
   4.287 -              (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale))
   4.288 -          else I) config []);
   4.289 +    val config = locale_config_of (Config.get lthy locale);
   4.290 +    val goals =
   4.291 +      (case some_locale of
   4.292 +        NONE => [(proto_goal, eval_terms)]
   4.293 +      | SOME locale =>
   4.294 +          fold (fn c =>
   4.295 +            if c = "expand" then
   4.296 +              cons (Logic.list_implies (axioms_of locale, proto_goal), eval_terms)
   4.297 +            else if c = "interpret" then
   4.298 +              append (map (fn (_, phi) =>
   4.299 +                  (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
   4.300 +                (Locale.registrations_of (Context.Theory thy) (* FIXME !? *) locale))
   4.301 +            else I) config []);
   4.302      val _ =
   4.303        verbose_message lthy
   4.304          (Pretty.string_of
   4.305 @@ -396,39 +405,39 @@
   4.306  fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck";
   4.307  
   4.308  fun pretty_counterex ctxt auto NONE =
   4.309 -    Pretty.str (tool_name auto ^ " found no counterexample." ^ Config.get ctxt tag)
   4.310 +      Pretty.str (tool_name auto ^ " found no counterexample." ^ Config.get ctxt tag)
   4.311    | pretty_counterex ctxt auto (SOME ((genuine, cex), eval_terms)) =
   4.312        (Pretty.text_fold o Pretty.fbreaks)
   4.313 -        (Pretty.str (tool_name auto ^ " found a " ^
   4.314 +       (Pretty.str (tool_name auto ^ " found a " ^
   4.315           (if genuine then "counterexample:"
   4.316            else "potentially spurious counterexample due to underspecified functions:") ^
   4.317 -         Config.get ctxt tag) ::
   4.318 -         Pretty.str "" ::
   4.319 -         map (fn (s, t) =>
   4.320 +        Config.get ctxt tag) ::
   4.321 +        Pretty.str "" ::
   4.322 +        map (fn (s, t) =>
   4.323            Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex) @
   4.324 -         (if null eval_terms then []
   4.325 -          else
   4.326 -           Pretty.str "" :: Pretty.str "Evaluated terms:" ::
   4.327 -           map (fn (t, u) =>
   4.328 -            Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
   4.329 -             Syntax.pretty_term ctxt u]) (rev eval_terms)));
   4.330 +        (if null eval_terms then []
   4.331 +         else
   4.332 +          Pretty.str "" :: Pretty.str "Evaluated terms:" ::
   4.333 +            map (fn (t, u) =>
   4.334 +              Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
   4.335 +                Syntax.pretty_term ctxt u]) (rev eval_terms)));
   4.336  
   4.337  
   4.338  (* Isar commands *)
   4.339  
   4.340  fun read_nat s =
   4.341 -  (case (Library.read_int o Symbol.explode) s of
   4.342 +  (case Library.read_int (Symbol.explode s) of
   4.343      (k, []) =>
   4.344        if k >= 0 then k
   4.345        else error ("Not a natural number: " ^ s)
   4.346 -  | (_, _ :: _) => error ("Not a natural number: " ^ s));
   4.347 +  | _ => error ("Not a natural number: " ^ s));
   4.348  
   4.349  fun read_bool "false" = false
   4.350    | read_bool "true" = true
   4.351    | read_bool s = error ("Not a Boolean value: " ^ s);
   4.352  
   4.353  fun read_real s =
   4.354 -  (case (Real.fromString s) of
   4.355 +  (case Real.fromString s of
   4.356      SOME s => s
   4.357    | NONE => error ("Not a real number: " ^ s));
   4.358  
   4.359 @@ -437,36 +446,42 @@
   4.360    | read_expectation "counterexample" = Counterexample
   4.361    | read_expectation s = error ("Not an expectation value: " ^ s);
   4.362  
   4.363 -fun valid_tester_name genctxt name = AList.defined (op =) (fst (fst (Data.get genctxt))) name;
   4.364 +fun valid_tester_name genctxt name =
   4.365 +  AList.defined (op =) (fst (fst (Data.get genctxt))) name;
   4.366  
   4.367  fun parse_tester name (testers, genctxt) =
   4.368    if valid_tester_name genctxt name then
   4.369      (insert (op =) name testers, genctxt)
   4.370 -  else
   4.371 -    error ("Unknown tester: " ^ name);
   4.372 +  else error ("Unknown tester: " ^ name);
   4.373  
   4.374  fun parse_test_param ("tester", args) = fold parse_tester args
   4.375    | parse_test_param ("size", [arg]) = apsnd (Config.put_generic size (read_nat arg))
   4.376    | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg))
   4.377    | parse_test_param ("depth", [arg]) = apsnd (Config.put_generic depth (read_nat arg))
   4.378 -  | parse_test_param ("default_type", arg) = (fn (testers, gen_ctxt) =>
   4.379 -    (testers, map_test_params
   4.380 -      ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt))
   4.381 +  | parse_test_param ("default_type", arg) =
   4.382 +      (fn (testers, gen_ctxt) =>
   4.383 +        (testers, map_test_params
   4.384 +          (apfst (K (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg))) gen_ctxt))
   4.385    | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
   4.386 -  | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg)))
   4.387 +  | parse_test_param ("expect", [arg]) = apsnd (map_test_params (apsnd (K (read_expectation arg))))
   4.388    | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
   4.389 -  | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg))
   4.390 -  | parse_test_param ("abort_potential", [arg]) = apsnd (Config.put_generic abort_potential (read_bool arg))
   4.391 +  | parse_test_param ("genuine_only", [arg]) =
   4.392 +      apsnd (Config.put_generic genuine_only (read_bool arg))
   4.393 +  | parse_test_param ("abort_potential", [arg]) =
   4.394 +      apsnd (Config.put_generic abort_potential (read_bool arg))
   4.395    | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
   4.396    | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
   4.397    | parse_test_param ("tag", [arg]) = apsnd (Config.put_generic tag arg)
   4.398 -  | parse_test_param ("use_subtype", [arg]) = apsnd (Config.put_generic use_subtype (read_bool arg))
   4.399 -  | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
   4.400 -  | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
   4.401 +  | parse_test_param ("use_subtype", [arg]) =
   4.402 +      apsnd (Config.put_generic use_subtype (read_bool arg))
   4.403 +  | parse_test_param ("timeout", [arg]) =
   4.404 +      apsnd (Config.put_generic timeout (read_real arg))
   4.405 +  | parse_test_param ("finite_types", [arg]) =
   4.406 +      apsnd (Config.put_generic finite_types (read_bool arg))
   4.407    | parse_test_param ("allow_function_inversion", [arg]) =
   4.408        apsnd (Config.put_generic allow_function_inversion (read_bool arg))
   4.409    | parse_test_param ("finite_type_size", [arg]) =
   4.410 -    apsnd (Config.put_generic finite_type_size (read_nat arg))
   4.411 +      apsnd (Config.put_generic finite_type_size (read_nat arg))
   4.412    | parse_test_param (name, _) =
   4.413        (fn (testers, genctxt) =>
   4.414          if valid_tester_name genctxt name then
   4.415 @@ -487,8 +502,9 @@
   4.416          ((insts, eval_terms),
   4.417            proof_map_result (fn gen_ctxt => parse_test_param (name, arg) (testers, gen_ctxt)) ctxt)));
   4.418  
   4.419 -fun quickcheck_params_cmd args = Context.theory_map
   4.420 -  (fn gen_ctxt => uncurry set_active_testers (fold parse_test_param args ([], gen_ctxt)));
   4.421 +fun quickcheck_params_cmd args =
   4.422 +  Context.theory_map
   4.423 +    (fn gen_ctxt => uncurry set_active_testers (fold parse_test_param args ([], gen_ctxt)));
   4.424  
   4.425  fun check_expectation state results =
   4.426    if is_some results andalso expect (Proof.context_of state) = No_Counterexample then
   4.427 @@ -502,8 +518,10 @@
   4.428    |> Proof.map_context_result (fn ctxt =>
   4.429      apsnd (fn (testers, ctxt) => Context.proof_map (set_active_testers testers) ctxt)
   4.430        (fold parse_test_param_inst args (([], []), ([], ctxt))))
   4.431 -  |> (fn ((insts, eval_terms), state') => test_goal (true, true) (insts, eval_terms) i state'
   4.432 -      |> tap (check_expectation state') |> rpair state');
   4.433 +  |> (fn ((insts, eval_terms), state') =>
   4.434 +      test_goal (true, true) (insts, eval_terms) i state'
   4.435 +      |> tap (check_expectation state')
   4.436 +      |> rpair state');
   4.437  
   4.438  fun quickcheck args i state =
   4.439    Option.map (the o get_first counterexample_of) (fst (gen_quickcheck args i state));