smallvalue_generator are defined quick via oracle or sound via function package
authorbulwahn
Fri Dec 03 08:40:46 2010 +0100 (2010-12-03)
changeset 409018fdfa9c4e7ed
parent 40900 1d5f76d79856
child 40902 7c652e4a924a
smallvalue_generator are defined quick via oracle or sound via function package
src/HOL/Tools/smallvalue_generators.ML
     1.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:46 2010 +0100
     1.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:46 2010 +0100
     1.3 @@ -16,6 +16,10 @@
     1.4  structure Smallvalue_Generators : SMALLVALUE_GENERATORS =
     1.5  struct
     1.6  
     1.7 +(* static options *)
     1.8 +
     1.9 +val define_foundationally = false
    1.10 +
    1.11  (** general term functions **)
    1.12  
    1.13  fun mk_measure f =
    1.14 @@ -36,6 +40,8 @@
    1.15    end
    1.16    | mk_sumcases _ f T = f T
    1.17  
    1.18 +fun mk_undefined T = Const(@{const_name undefined}, T)
    1.19 +  
    1.20  
    1.21  (** abstract syntax **)
    1.22  
    1.23 @@ -70,11 +76,8 @@
    1.24  fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    1.25    --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
    1.26   
    1.27 -fun mk_equations thy descr vs tycos (names, auxnames) (Ts, Us) =
    1.28 +fun mk_equations thy descr vs tycos smalls (Ts, Us) =
    1.29    let
    1.30 -    val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
    1.31 -    val smalls = map2 (fn name => fn T => Free (name, full_smallT T))
    1.32 -      smallsN (Ts @ Us)
    1.33      fun mk_small_call T =
    1.34        let
    1.35          val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)        
    1.36 @@ -119,44 +122,77 @@
    1.37      val lhss = map2 (fn t => fn T => t $ test_function T $ size) smalls (Ts @ Us);
    1.38      val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
    1.39    in
    1.40 -    (Ts @ Us ~~ (smallsN ~~ eqs))
    1.41 +    eqs
    1.42 +  end
    1.43 +
    1.44 +(* foundational definition with the function package *)
    1.45 +
    1.46 +val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
    1.47 +
    1.48 +fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
    1.49 +    Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
    1.50 +
    1.51 +fun mk_termination_measure T =
    1.52 +  let
    1.53 +    val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
    1.54 +  in
    1.55 +    mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
    1.56    end
    1.57 -    
    1.58 -val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
    1.59 -  
    1.60 +
    1.61 +fun termination_tac ctxt = 
    1.62 +  Function_Relation.relation_tac ctxt mk_termination_measure 1
    1.63 +  THEN rtac @{thm wf_measure} 1
    1.64 +  THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
    1.65 +    (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
    1.66 +     @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
    1.67 +
    1.68 +fun pat_completeness_auto ctxt =
    1.69 +  Pat_Completeness.pat_completeness_tac ctxt 1
    1.70 +  THEN auto_tac (clasimpset_of ctxt)    
    1.71 +
    1.72 +
    1.73 +(* creating the instances *)
    1.74 +
    1.75  fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    1.76    let
    1.77      val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
    1.78 -    val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
    1.79 -    fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
    1.80 -      Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
    1.81 -    fun mk_termination_measure T =
    1.82 -      let
    1.83 -        val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
    1.84 -      in
    1.85 -        mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
    1.86 -      end
    1.87 -    fun termination_tac ctxt = 
    1.88 -      Function_Relation.relation_tac ctxt mk_termination_measure 1
    1.89 -      THEN rtac @{thm wf_measure} 1
    1.90 -      THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
    1.91 -        (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
    1.92 -         @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
    1.93 -    fun pat_completeness_auto ctxt =
    1.94 -      Pat_Completeness.pat_completeness_tac ctxt 1
    1.95 -      THEN auto_tac (clasimpset_of ctxt)
    1.96 -  in 
    1.97 +    val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
    1.98 +  in
    1.99      thy
   1.100      |> Class.instantiation (tycos, vs, @{sort full_small})
   1.101 -    |> Function.add_function
   1.102 -      (map (fn (T, (name, _)) =>
   1.103 -          Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T))) eqs)
   1.104 -        (map (pair (apfst Binding.conceal Attrib.empty_binding) o snd o snd) eqs)
   1.105 -        Function_Common.default_config pat_completeness_auto
   1.106 -    |> snd
   1.107 -    |> Local_Theory.restore
   1.108 -    |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
   1.109 -    |> snd
   1.110 +    |> (if define_foundationally then
   1.111 +      let
   1.112 +        val smalls = map2 (fn name => fn T => Free (name, full_smallT T)) smallsN (Ts @ Us)
   1.113 +        val eqs = mk_equations thy descr vs tycos smalls (Ts, Us)
   1.114 +      in
   1.115 +        Function.add_function
   1.116 +          (map (fn (name, T) =>
   1.117 +              Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T)))
   1.118 +                (smallsN ~~ (Ts @ Us)))
   1.119 +            (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs)
   1.120 +          Function_Common.default_config pat_completeness_auto
   1.121 +        #> snd
   1.122 +        #> Local_Theory.restore
   1.123 +        #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
   1.124 +        #> snd
   1.125 +      end
   1.126 +    else
   1.127 +      fold_map (fn (name, T) => Local_Theory.define
   1.128 +          ((Binding.conceal (Binding.name name), NoSyn),
   1.129 +            (apfst Binding.conceal Attrib.empty_binding, mk_undefined (full_smallT T)))
   1.130 +        #> apfst fst) (smallsN ~~ (Ts @ Us))
   1.131 +      #> (fn (smalls, lthy) =>
   1.132 +        let
   1.133 +          val eqs_t = mk_equations thy descr vs tycos smalls (Ts, Us)
   1.134 +          val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
   1.135 +            (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
   1.136 +        in
   1.137 +          fold (fn (name, eq) => Local_Theory.note
   1.138 +          ((Binding.conceal (Binding.qualify true prfx
   1.139 +             (Binding.qualify true name (Binding.name "simps"))),
   1.140 +             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
   1.141 +               [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (smallsN ~~ eqs) lthy
   1.142 +        end))
   1.143      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   1.144    end handle FUNCTION_TYPE =>
   1.145      (Datatype_Aux.message config