adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet
authorbulwahn
Mon Mar 29 17:30:56 2010 +0200 (2010-03-29)
changeset 36040fcd7bea01a93
parent 36039 affb6e1041e1
child 36041 8b25e3b217bc
adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Mon Mar 29 17:30:55 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Mon Mar 29 17:30:56 2010 +0200
     1.3 @@ -788,7 +788,7 @@
     1.4  definition
     1.5    "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
     1.6  
     1.7 -code_pred [inductify] case_f .
     1.8 +code_pred [inductify, skip_proof] case_f .
     1.9  thm case_fP.equation
    1.10  thm case_fP.intros
    1.11  
    1.12 @@ -910,11 +910,11 @@
    1.13  declare list.size(3,4)[code_pred_def]
    1.14  (*code_pred [inductify, show_steps, show_intermediate_results] length .*)
    1.15  setup {* Predicate_Compile_Data.ignore_consts [@{const_name Orderings.top_class.top}] *}
    1.16 -code_pred [inductify] lex .
    1.17 +code_pred [inductify, skip_proof] lex .
    1.18  thm lex.equation
    1.19  thm lex_def
    1.20  declare lenlex_conv[code_pred_def]
    1.21 -code_pred [inductify] lenlex .
    1.22 +code_pred [inductify, skip_proof] lenlex .
    1.23  thm lenlex.equation
    1.24  
    1.25  code_pred [random_dseq inductify] lenlex .
    1.26 @@ -1037,7 +1037,7 @@
    1.27  *)
    1.28  (*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
    1.29  
    1.30 -code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat .
    1.31 +code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
    1.32  thm concatP.equation
    1.33  
    1.34  values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
    1.35 @@ -1068,31 +1068,31 @@
    1.36  values "{x. tlP [1, 2, (3::nat)] x}"
    1.37  values "{x. tlP [1, 2, (3::int)] [3]}"
    1.38  
    1.39 -code_pred [inductify] last .
    1.40 +code_pred [inductify, skip_proof] last .
    1.41  thm lastP.equation
    1.42  
    1.43 -code_pred [inductify] butlast .
    1.44 +code_pred [inductify, skip_proof] butlast .
    1.45  thm butlastP.equation
    1.46  
    1.47 -code_pred [inductify] take .
    1.48 +code_pred [inductify, skip_proof] take .
    1.49  thm takeP.equation
    1.50  
    1.51 -code_pred [inductify] drop .
    1.52 +code_pred [inductify, skip_proof] drop .
    1.53  thm dropP.equation
    1.54 -code_pred [inductify] zip .
    1.55 +code_pred [inductify, skip_proof] zip .
    1.56  thm zipP.equation
    1.57  
    1.58 -code_pred [inductify] upt .
    1.59 -code_pred [inductify] remdups .
    1.60 +code_pred [inductify, skip_proof] upt .
    1.61 +code_pred [inductify, skip_proof] remdups .
    1.62  thm remdupsP.equation
    1.63  code_pred [dseq inductify] remdups .
    1.64  values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
    1.65  
    1.66 -code_pred [inductify] remove1 .
    1.67 +code_pred [inductify, skip_proof] remove1 .
    1.68  thm remove1P.equation
    1.69  values "{xs. remove1P 1 xs [2, (3::int)]}"
    1.70  
    1.71 -code_pred [inductify] removeAll .
    1.72 +code_pred [inductify, skip_proof] removeAll .
    1.73  thm removeAllP.equation
    1.74  code_pred [dseq inductify] removeAll .
    1.75  
    1.76 @@ -1100,17 +1100,17 @@
    1.77  
    1.78  code_pred [inductify] distinct .
    1.79  thm distinct.equation
    1.80 -code_pred [inductify] replicate .
    1.81 +code_pred [inductify, skip_proof] replicate .
    1.82  thm replicateP.equation
    1.83  values 5 "{(n, xs). replicateP n (0::int) xs}"
    1.84  
    1.85 -code_pred [inductify] splice .
    1.86 +code_pred [inductify, skip_proof] splice .
    1.87  thm splice.simps
    1.88  thm spliceP.equation
    1.89  
    1.90  values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
    1.91  
    1.92 -code_pred [inductify] List.rev .
    1.93 +code_pred [inductify, skip_proof] List.rev .
    1.94  code_pred [inductify] map .
    1.95  code_pred [inductify] foldr .
    1.96  code_pred [inductify] foldl .
    1.97 @@ -1159,7 +1159,7 @@
    1.98  | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
    1.99  | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
   1.100  
   1.101 -code_pred [inductify] S\<^isub>3p .
   1.102 +code_pred [inductify, skip_proof] S\<^isub>3p .
   1.103  thm S\<^isub>3p.equation
   1.104  
   1.105  values 10 "{x. S\<^isub>3p x}"
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Mon Mar 29 17:30:55 2010 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Mon Mar 29 17:30:56 2010 +0200
     2.3 @@ -108,7 +108,7 @@
     2.4  | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
     2.5  | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
     2.6  
     2.7 -code_pred [inductify] S\<^isub>3 .
     2.8 +code_pred [inductify, skip_proof] S\<^isub>3 .
     2.9  thm S\<^isub>3.equation
    2.10  (*
    2.11  values 10 "{x. S\<^isub>3 x}"
     3.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Mar 29 17:30:55 2010 +0200
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Mar 29 17:30:56 2010 +0200
     3.3 @@ -218,7 +218,7 @@
     3.4      \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
     3.5  | T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
     3.6  
     3.7 -code_pred [inductify] typing .
     3.8 +code_pred [inductify, skip_proof] typing .
     3.9  
    3.10  thm typing.equation
    3.11