removing clone from function package and using the clean interface from Function_Relation instead
authorbulwahn
Mon Nov 22 10:42:01 2010 +0100 (2010-11-22)
changeset 406403fa1c2472568
parent 40639 f1f0e6adca0a
child 40641 5615cc557120
removing clone from function package and using the clean interface from Function_Relation instead
src/HOL/Tools/smallvalue_generators.ML
     1.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:41:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:42:01 2010 +0100
     1.3 @@ -134,36 +134,21 @@
     1.4    end
     1.5      
     1.6  val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
     1.7 -
     1.8 -fun gen_inst_state_tac ctxt rel st =
     1.9 -  case Term.add_vars (prop_of st) [] of
    1.10 -    [v as (_, T)] =>
    1.11 -      let
    1.12 -        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
    1.13 -        val rel' = cert rel
    1.14 -        val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st (*FIXME??*)
    1.15 -      in        
    1.16 -        PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
    1.17 -      end
    1.18 -  | _ => Seq.empty;
    1.19    
    1.20  fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    1.21    let
    1.22      val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
    1.23      val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
    1.24 -    fun my_relation_tac ctxt st =
    1.25 +    fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
    1.26 +      Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
    1.27 +    fun mk_termination_measure T =
    1.28        let
    1.29 -        val ((_ $ (_ $ rel)) :: tl) = prems_of st
    1.30 -        val domT = (HOLogic.dest_setT (fastype_of rel))
    1.31 -        fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
    1.32 -            Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
    1.33 -        val measure = mk_measure (mk_sumcases @{typ nat} mk_single_measure domT)
    1.34 +        val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
    1.35        in
    1.36 -        (Function_Common.apply_termination_rule ctxt 1
    1.37 -        THEN gen_inst_state_tac ctxt measure) st
    1.38 +        mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
    1.39        end
    1.40      fun termination_tac ctxt = 
    1.41 -      my_relation_tac ctxt
    1.42 +      Function_Relation.relation_tac ctxt mk_termination_measure 1
    1.43        THEN rtac @{thm wf_measure} 1
    1.44        THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
    1.45          (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},