src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
changeset 39800 17e29ddd538e
parent 39463 7ce0ed8dc4d6
child 40301 bf39a257b3d3
equal deleted inserted replaced
39799:fdbea66eae4b 39800:17e29ddd538e
    56 
    56 
    57 declare filter_b_def[symmetric, code_pred_inline]
    57 declare filter_b_def[symmetric, code_pred_inline]
    58 
    58 
    59 setup {* Code_Prolog.map_code_options (K
    59 setup {* Code_Prolog.map_code_options (K
    60   {ensure_groundness = true,
    60   {ensure_groundness = true,
       
    61   limit_globally = NONE,
    61   limited_types = [],
    62   limited_types = [],
    62   limited_predicates = [(["s1", "a1", "b1"], 2)],
    63   limited_predicates = [(["s1", "a1", "b1"], 2)],
    63   replacing = [(("s1", "limited_s1"), "quickcheck")],
    64   replacing = [(("s1", "limited_s1"), "quickcheck")],
    64   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    65   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    65 
    66 
    79 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
    80 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
    80 
    81 
    81 
    82 
    82 setup {* Code_Prolog.map_code_options (K
    83 setup {* Code_Prolog.map_code_options (K
    83   {ensure_groundness = true,
    84   {ensure_groundness = true,
       
    85   limit_globally = NONE,
    84   limited_types = [],
    86   limited_types = [],
    85   limited_predicates = [(["s2", "a2", "b2"], 3)],
    87   limited_predicates = [(["s2", "a2", "b2"], 3)],
    86   replacing = [(("s2", "limited_s2"), "quickcheck")],
    88   replacing = [(("s2", "limited_s2"), "quickcheck")],
    87   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    89   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
    88 
    90 
   101 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
   103 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
   102 
   104 
   103 
   105 
   104 setup {* Code_Prolog.map_code_options (K
   106 setup {* Code_Prolog.map_code_options (K
   105   {ensure_groundness = true,
   107   {ensure_groundness = true,
       
   108   limit_globally = NONE,
   106   limited_types = [],
   109   limited_types = [],
   107   limited_predicates = [(["s3", "a3", "b3"], 6)],
   110   limited_predicates = [(["s3", "a3", "b3"], 6)],
   108   replacing = [(("s3", "limited_s3"), "quickcheck")],
   111   replacing = [(("s3", "limited_s3"), "quickcheck")],
   109   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
   112   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
   110 
   113 
   115 
   118 
   116 
   119 
   117 (*
   120 (*
   118 setup {* Code_Prolog.map_code_options (K
   121 setup {* Code_Prolog.map_code_options (K
   119   {ensure_groundness = true,
   122   {ensure_groundness = true,
       
   123   limit_globally = NONE,
   120   limited_types = [],
   124   limited_types = [],
   121   limited_predicates = [],
   125   limited_predicates = [],
   122   replacing = [],
   126   replacing = [],
   123   manual_reorder = [],
   127   manual_reorder = [],
   124   timeout = Time.fromSeconds 10,
   128   timeout = Time.fromSeconds 10,
   141 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   145 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   142 
   146 
   143 
   147 
   144 setup {* Code_Prolog.map_code_options (K
   148 setup {* Code_Prolog.map_code_options (K
   145   {ensure_groundness = true,
   149   {ensure_groundness = true,
       
   150   limit_globally = NONE,
   146   limited_types = [],
   151   limited_types = [],
   147   limited_predicates = [(["s4", "a4", "b4"], 6)],
   152   limited_predicates = [(["s4", "a4", "b4"], 6)],
   148   replacing = [(("s4", "limited_s4"), "quickcheck")],
   153   replacing = [(("s4", "limited_s4"), "quickcheck")],
   149   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
   154   manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
   150 
   155