don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
authorhuffman
Mon Mar 08 13:58:00 2010 -0800 (2010-03-08)
changeset 35661ede27eb8e94b
parent 35660 8169419cd824
child 35662 44d7aafdddb9
don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/ex/Domain_ex.thy
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 12:43:44 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 13:58:00 2010 -0800
     1.3 @@ -231,6 +231,7 @@
     1.4  
     1.5    val {take_0_thms, take_Suc_thms, chain_take_thms, ...} = take_info;
     1.6    val {lub_take_thms, finite_defs, reach_thms, ...} = take_info;
     1.7 +  val {take_induct_thms, ...} = take_info;
     1.8  
     1.9    fun one_con p (con, args) =
    1.10      let
    1.11 @@ -282,7 +283,7 @@
    1.12    in
    1.13      val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
    1.14      val is_emptys = map warn n__eqs;
    1.15 -    val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
    1.16 +    val is_finite = #is_finite take_info;
    1.17      val _ = if is_finite
    1.18              then message ("Proving finiteness rule for domain "^comp_dnam^" ...")
    1.19              else ();
    1.20 @@ -326,70 +327,27 @@
    1.21  
    1.22    val global_ctxt = ProofContext.init thy;
    1.23  
    1.24 -  val _ = trace " Proving finites, ind...";
    1.25 -  val (finites, ind) =
    1.26 +  val _ = trace " Proving ind...";
    1.27 +  val ind =
    1.28    (
    1.29      if is_finite
    1.30      then (* finite case *)
    1.31        let
    1.32 -        val decisive_lemma =
    1.33 -          let
    1.34 -            val iso_locale_thms =
    1.35 -                map2 (fn x => fn y => @{thm iso.intro} OF [x, y])
    1.36 -                axs_abs_iso axs_rep_iso;
    1.37 -            val decisive_abs_rep_thms =
    1.38 -                map (fn x => @{thm decisive_abs_rep} OF [x])
    1.39 -                iso_locale_thms;
    1.40 -            val n = Free ("n", @{typ nat});
    1.41 -            fun mk_decisive t = %%: @{const_name decisive} $ t;
    1.42 -            fun f dn = mk_decisive (dc_take dn $ n);
    1.43 -            val goal = mk_trp (foldr1 mk_conj (map f dnames));
    1.44 -            val rules0 = @{thm decisive_bottom} :: take_0_thms;
    1.45 -            val rules1 =
    1.46 -                take_Suc_thms @ decisive_abs_rep_thms
    1.47 -                @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map};
    1.48 -            val tacs = [
    1.49 -                rtac @{thm nat.induct} 1,
    1.50 -                simp_tac (HOL_ss addsimps rules0) 1,
    1.51 -                asm_simp_tac (HOL_ss addsimps rules1) 1];
    1.52 -          in pg [] goal (K tacs) end;
    1.53 -        fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
    1.54 -        fun one_finite (dn, decisive_thm) =
    1.55 +        fun concf n dn = %:(P_name n) $ %:(x_name n);
    1.56 +        fun tacf {prems, context} =
    1.57            let
    1.58 -            val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
    1.59 -            val tacs = [
    1.60 -                rtac @{thm lub_ID_finite} 1,
    1.61 -                resolve_tac chain_take_thms 1,
    1.62 -                resolve_tac lub_take_thms 1,
    1.63 -                rtac decisive_thm 1];
    1.64 -          in pg finite_defs goal (K tacs) end;
    1.65 -
    1.66 -        val _ = trace " Proving finites";
    1.67 -        val finites = map one_finite (dnames ~~ atomize global_ctxt decisive_lemma);
    1.68 -        val _ = trace " Proving ind";
    1.69 -        val ind =
    1.70 -          let
    1.71 -            fun concf n dn = %:(P_name n) $ %:(x_name n);
    1.72 -            fun tacf {prems, context} =
    1.73 -              let
    1.74 -                fun finite_tacs (finite, fin_ind) = [
    1.75 -                  rtac(rewrite_rule finite_defs finite RS exE)1,
    1.76 -                  etac subst 1,
    1.77 -                  rtac fin_ind 1,
    1.78 -                  ind_prems_tac prems];
    1.79 -              in
    1.80 -                TRY (safe_tac HOL_cs) ::
    1.81 -                maps finite_tacs (finites ~~ atomize global_ctxt finite_ind)
    1.82 -              end;
    1.83 -          in pg'' thy [] (ind_term concf) tacf end;
    1.84 -      in (finites, ind) end (* let *)
    1.85 +            fun finite_tacs (take_induct, fin_ind) = [
    1.86 +                rtac take_induct 1,
    1.87 +                rtac fin_ind 1,
    1.88 +                ind_prems_tac prems];
    1.89 +          in
    1.90 +            TRY (safe_tac HOL_cs) ::
    1.91 +            maps finite_tacs (take_induct_thms ~~ atomize global_ctxt finite_ind)
    1.92 +          end;
    1.93 +      in pg'' thy [] (ind_term concf) tacf end
    1.94  
    1.95      else (* infinite case *)
    1.96        let
    1.97 -        fun one_finite n dn =
    1.98 -          read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
    1.99 -        val finites = mapn one_finite 1 dnames;
   1.100 -
   1.101          val goal =
   1.102            let
   1.103              fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
   1.104 @@ -420,12 +378,12 @@
   1.105            handle ERROR _ =>
   1.106              (warning "Cannot prove infinite induction rule"; TrueI)
   1.107                    );
   1.108 -      in (finites, ind) end
   1.109 +      in ind end
   1.110    )
   1.111        handle THM _ =>
   1.112 -             (warning "Induction proofs failed (THM raised)."; ([], TrueI))
   1.113 +             (warning "Induction proofs failed (THM raised)."; TrueI)
   1.114             | ERROR _ =>
   1.115 -             (warning "Cannot prove induction rule"; ([], TrueI));
   1.116 +             (warning "Cannot prove induction rule"; TrueI);
   1.117  
   1.118  val case_ns =
   1.119    let
   1.120 @@ -445,7 +403,6 @@
   1.121  
   1.122  in thy |> Sign.add_path comp_dnam
   1.123         |> snd o PureThy.add_thmss [
   1.124 -           ((Binding.name "finites"    , finites     ), []),
   1.125             ((Binding.name "finite_ind" , [finite_ind]), []),
   1.126             ((Binding.name "ind"        , [ind]       ), [])]
   1.127         |> (if induct_failed then I
     2.1 --- a/src/HOLCF/ex/Domain_ex.thy	Mon Mar 08 12:43:44 2010 -0800
     2.2 +++ b/src/HOLCF/ex/Domain_ex.thy	Mon Mar 08 13:58:00 2010 -0800
     2.3 @@ -107,7 +107,7 @@
     2.4  
     2.5  subsection {* Generated constants and theorems *}
     2.6  
     2.7 -domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (lazy right :: "'a tree")
     2.8 +domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
     2.9  
    2.10  lemmas tree_abs_defined_iff =
    2.11    iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
    2.12 @@ -174,7 +174,7 @@
    2.13  text {* Rules about finiteness predicate *}
    2.14  term tree_finite
    2.15  thm tree.finite_def
    2.16 -thm tree.finites
    2.17 +thm tree.finite (* only generated for flat datatypes *)
    2.18  
    2.19  text {* Rules about bisimulation predicate *}
    2.20  term tree_bisim
    2.21 @@ -196,14 +196,6 @@
    2.22    -- {* Inner syntax error at "= UU" *}
    2.23  *)
    2.24  
    2.25 -text {*
    2.26 -  I don't know what is going on here.  The failed proof has to do with
    2.27 -  the finiteness predicate.
    2.28 -*}
    2.29 -
    2.30 -domain foo = Foo (lazy "bar") and bar = Bar
    2.31 -  -- "Cannot prove induction rule"
    2.32 -
    2.33  text {* Declaring class constraints on the LHS is currently broken. *}
    2.34  (*
    2.35  domain ('a::cpo) box = Box (lazy 'a)