Theory Pratt_Certificate_Code

(*
  File:     Pratt_Certificate_Code.thy
  Author:   Manuel Eberl, TU München

  Efficient checking of Pratt certificates using the code generator.
  Evaluation on some big examples.
*)
theory Pratt_Certificate_Code
imports
  Pratt_Certificate
  "HOL-Library.Code_Target_Numeral"
begin

subsection ‹Code generation for Pratt certificates›

text ‹
  The following one-time setup is required to set up code generation for the certificate
  checking. Other theories importing this theories do not have to do this again.
›

setup ‹
  Context.theory_map (Pratt.setup_valid_cert_code_conv
    (@{computation_check
        terms: Trueprop valid_pratt_tree "0::nat" "1::nat" "2::nat" "3::nat" "4::nat"
        datatypes: "pratt_tree list" "nat × nat × pratt_tree list" nat}))
›

text ‹
  We can now evaluate the efficiency of the procedure on some examples.
›

lemma "prime (131059 :: nat)"
  by (pratt (code))

lemma "prime (100000007 :: nat)"
  by (pratt (code))

lemma "prime (8504276003 :: nat)"
  by (pratt (code))

lemma "prime (52759926861157 :: nat)"
  by (pratt (code))

lemma "prime (39070009756439177203 :: nat)"
  by (pratt (code)
        ‹{39070009756439177203, 2, 
           {2, {3, 2, {2}}, {197, 2, {2, {7, 3, {2, {3, 2, {2}}}}}}, 
            {11018051256751037, 2, {2, {19, 2, {2, {3, 2, {2}}}}, 
              {1249, 7, {2, {3, 2, {2}}, {13, 2, {2, {3, 2, {2}}}}}}, 
              {116072344789, 2, {2, {3, 2, {2}}, 
                {3067, 2, {2, {3, 2, {2}}, {7, 3, {2, {3, 2, {2}}}}, 
                  {73, 5, {2, {3, 2, {2}}}}}}, 
                {3153797, 2, {2, {788449, 11, 
                   {2, {3, 2, {2}}, {43, 3, 
                     {2, {3, 2, {2}}, {7, 3, {2, {3, 2, {2}}}}}}, 
                    {191, 19, {2, {5, 2, {2}}, {19, 2, {2, {3, 2, {2}}}}}}}}}}}}}}}}›)

lemma "prime (933491553728809239092563013853810654040043466297416456476877 :: nat)"
  by (pratt (code)
        ‹{933491553728809239092563013853810654040043466297416456476877, 
             2, {2, {38463351105299604725411, 6, 
               {2, {5, 2, {2}}, {13, 2, {2, {3, 2, {2}}}}, 
                {295871931579227728657, 5, 
                 {2, {3, 2, {2}}, {26041, 13, 
                   {2, {3, 2, {2}}, {5, 2, {2}}, {7, 3, {2, {3, 2, {2}}}}, 
                    {31, 3, {2, {3, 2, {2}}, {5, 2, {2}}}}}}, 
                  {29009, 3, {2, {7, 3, {2, {3, 2, {2}}}}, 
                    {37, 2, {2, {3, 2, {2}}}}}}, 
                  {39133, 5, {2, {3, 2, {2}}, 
                    {1087, 3, {2, {3, 2, {2}}, 
                      {181, 2, {2, {3, 2, {2}}, {5, 2, {2}}}}}}}}, 
                  {208511, 7, {2, {5, 2, {2}}, {29, 2, {2, {7, 3, {2, {3, 2, {2}}}}}}, 
                    {719, 11, {2, {359, 7, 
                       {2, {179, 2, {2, {89, 3, {2, {11, 2, {2, {5, 2, {2}}}}}}}}}}}}}}
                   }}}}, {6067409149902371339956289140415169329, 3, 
               {2, {11, 2, {2, {5, 2, {2}}}}, 
                {103, 5, {2, {3, 2, {2}}, {17, 3, {2}}}}, 
                {7955023343, 7, {2, {7, 3, {2, {3, 2, {2}}}}, 
                  {79, 3, {2, {3, 2, {2}}, {13, 2, {2, {3, 2, {2}}}}}}, 
                  {1451, 2, {2, {5, 2, {2}}, {29, 2, {2, {7, 3, {2, {3, 2, {2}}}}}}}}, 
                  {4957, 2, {2, {3, 2, {2}}, {7, 3, {2, {3, 2, {2}}}}, 
                    {59, 2, {2, {29, 2, {2, {7, 3, {2, {3, 2, {2}}}}}}}}}}}}, 
                {8108847767, 5, {2, {4054423883, 2, 
                   {2, {2027211941, 2, {2, {5, 2, {2}}, {13, 2, {2, {3, 2, {2}}}}, 
                      {29, 2, {2, {7, 3, {2, {3, 2, {2}}}}}}, 
                      {268861, 6, {2, {3, 2, {2}}, {5, 2, {2}}, 
                        {4481, 3, {2, {5, 2, {2}}, {7, 3, {2, {3, 2, {2}}}}}}}}}}}}}}, 
                {5188630976471, 13, {2, {5, 2, {2}}, 
                  {518863097647, 5, {2, {3, 2, {2}}, 
                    {67, 2, {2, {3, 2, {2}}, {11, 2, {2, {5, 2, {2}}}}}}, 
                    {17881, 7, {2, {3, 2, {2}}, {5, 2, {2}}, 
                      {149, 2, {2, {37, 2, {2, {3, 2, {2}}}}}}}}, 
                    {24061, 10, {2, {3, 2, {2}}, {5, 2, {2}}, 
                      {401, 3, {2, {5, 2, {2}}}}}}}}}}}}}}
›)

end