tuned line length;
authorwenzelm
Mon Jul 15 20:36:27 2013 +0200 (2013-07-15)
changeset 52666391913d17d15
parent 52665 5f817bad850a
child 52667 d2b12523186d
tuned line length;
src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
src/HOL/Predicate_Compile_Examples/Examples.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
src/HOL/Predicate_Compile_Examples/List_Examples.thy
src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Mon Jul 15 20:13:30 2013 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Mon Jul 15 20:36:27 2013 +0200
     1.3 @@ -19,7 +19,10 @@
     1.4  declare size_list_def[symmetric, code_pred_inline]
     1.5  
     1.6  
     1.7 -setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
     1.8 +setup {*
     1.9 +  Context.theory_map
    1.10 +    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
    1.11 +*}
    1.12  
    1.13  datatype alphabet = a | b
    1.14  
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Mon Jul 15 20:13:30 2013 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Mon Jul 15 20:36:27 2013 +0200
     2.3 @@ -29,7 +29,8 @@
     2.4                           (s1 @ rhs @ s2) = rsl \<and>
     2.5                           (rule lhs rhs) \<in> fst g }"
     2.6  
     2.7 -definition derivesp :: "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
     2.8 +definition derivesp ::
     2.9 +  "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
    2.10  where
    2.11    "derivesp g = (\<lambda> lhs rhs. (lhs, rhs) \<in> derives (Collect (fst g), snd g))"
    2.12   
    2.13 @@ -252,7 +253,8 @@
    2.14  where
    2.15    irconst: "eval_var (IrConst i) conf (IntVal i)"
    2.16  | objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
    2.17 -| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
    2.18 +| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow>
    2.19 +    eval_var (Add l r) conf (IntVal (vl+vr))"
    2.20  
    2.21  
    2.22  code_pred eval_var .
     3.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Mon Jul 15 20:13:30 2013 +0200
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Mon Jul 15 20:36:27 2013 +0200
     3.3 @@ -31,7 +31,9 @@
     3.4  
     3.5  lemma [code_pred_def]:
     3.6    "cardsp [] g k = False"
     3.7 -  "cardsp (e # s) g k = (let C = cardsp s g in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
     3.8 +  "cardsp (e # s) g k =
     3.9 +    (let C = cardsp s g
    3.10 +     in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
    3.11  unfolding cardsp_def [abs_def] cards.simps by (auto simp add: Let_def split: event.split)
    3.12  
    3.13  definition
    3.14 @@ -79,7 +81,10 @@
    3.15  
    3.16  values 40 "{s. hotel s}"
    3.17  
    3.18 -setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
    3.19 +setup {*
    3.20 +  Context.theory_map
    3.21 +    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
    3.22 +*}
    3.23  
    3.24  lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
    3.25  quickcheck[tester = prolog, iterations = 1, expect = counterexample]
     4.1 --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Mon Jul 15 20:13:30 2013 +0200
     4.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Mon Jul 15 20:36:27 2013 +0200
     4.3 @@ -79,7 +79,10 @@
     4.4  
     4.5  section {* Manual setup to find counterexample *}
     4.6  
     4.7 -setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
     4.8 +setup {*
     4.9 +  Context.theory_map
    4.10 +    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
    4.11 +*}
    4.12  
    4.13  setup {* Code_Prolog.map_code_options (K 
    4.14    { ensure_groundness = true,
     5.1 --- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Mon Jul 15 20:13:30 2013 +0200
     5.2 +++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Mon Jul 15 20:36:27 2013 +0200
     5.3 @@ -5,7 +5,10 @@
     5.4    "~~/src/HOL/Library/Code_Prolog"
     5.5  begin
     5.6  
     5.7 -setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
     5.8 +setup {*
     5.9 +  Context.theory_map
    5.10 +    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
    5.11 +*}
    5.12  
    5.13  setup {* Code_Prolog.map_code_options (K 
    5.14    {ensure_groundness = true,
     6.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Mon Jul 15 20:13:30 2013 +0200
     6.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Mon Jul 15 20:36:27 2013 +0200
     6.3 @@ -85,7 +85,8 @@
     6.4   
     6.5  fun prop_regex :: "Nat * Nat * RE * RE * Sym list \<Rightarrow> bool"
     6.6  where
     6.7 -  "prop_regex (n, (k, (p, (q, s)))) = ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"
     6.8 +  "prop_regex (n, (k, (p, (q, s)))) =
     6.9 +    ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"
    6.10  
    6.11  
    6.12  
    6.13 @@ -97,7 +98,10 @@
    6.14  oops
    6.15  
    6.16  
    6.17 -setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
    6.18 +setup {*
    6.19 +  Context.theory_map
    6.20 +    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
    6.21 +*}
    6.22  
    6.23  setup {* Code_Prolog.map_code_options (K 
    6.24    {ensure_groundness = true,