fix proof script for take_apps so it works with indirect recursion
authorhuffman
Tue Mar 02 16:25:59 2010 -0800 (2010-03-02)
changeset 35523cc57f4a274a3
parent 35522 f9714c7c0837
child 35524 a2a59e92b02e
fix proof script for take_apps so it works with indirect recursion
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 16:07:48 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 16:25:59 2010 -0800
     1.3 @@ -176,8 +176,9 @@
     1.4  local
     1.5    fun dc_take dn = %%:(dn^"_take");
     1.6    val dnames = map (fst o fst) eqs;
     1.7 -  fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict");
     1.8 -  val axs_take_strict = map get_take_strict dnames;
     1.9 +  val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
    1.10 +  fun get_deflation_take dn = PureThy.get_thm thy (dn ^ ".deflation_take");
    1.11 +  val axs_deflation_take = map get_deflation_take dnames;
    1.12  
    1.13    fun one_take_app (con, args) =
    1.14      let
    1.15 @@ -191,7 +192,9 @@
    1.16        val rhs = con_app2 con one_rhs args;
    1.17        val goal = mk_trp (lhs === rhs);
    1.18        val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}];
    1.19 -      val rules2 = @{thms take_con_rules ID1} @ axs_take_strict;
    1.20 +      val rules2 =
    1.21 +          @{thms take_con_rules ID1 deflation_strict}
    1.22 +          @ deflation_thms @ axs_deflation_take;
    1.23        val tacs =
    1.24            [simp_tac (HOL_basic_ss addsimps rules) 1,
    1.25             asm_simp_tac (HOL_basic_ss addsimps rules2) 1];