author huffman Mon Mar 08 13:58:00 2010 -0800 (2010-03-08) changeset 35661 ede27eb8e94b parent 35660 8169419cd824 child 35662 44d7aafdddb9
don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
```     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.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)
```