author huffman Mon, 08 Mar 2010 13:58:00 -0800 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
```--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 12:43:44 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 13:58:00 2010 -0800
@@ -231,6 +231,7 @@

val {take_0_thms, take_Suc_thms, chain_take_thms, ...} = take_info;
val {lub_take_thms, finite_defs, reach_thms, ...} = take_info;
+  val {take_induct_thms, ...} = take_info;

fun one_con p (con, args) =
let
@@ -282,7 +283,7 @@
in
val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
val is_emptys = map warn n__eqs;
-    val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
+    val is_finite = #is_finite take_info;
val _ = if is_finite
then message ("Proving finiteness rule for domain "^comp_dnam^" ...")
else ();
@@ -326,70 +327,27 @@

val global_ctxt = ProofContext.init thy;

-  val _ = trace " Proving finites, ind...";
-  val (finites, ind) =
+  val _ = trace " Proving ind...";
+  val ind =
(
if is_finite
then (* finite case *)
let
-        val decisive_lemma =
-          let
-            val iso_locale_thms =
-                map2 (fn x => fn y => @{thm iso.intro} OF [x, y])
-                axs_abs_iso axs_rep_iso;
-            val decisive_abs_rep_thms =
-                map (fn x => @{thm decisive_abs_rep} OF [x])
-                iso_locale_thms;
-            val n = Free ("n", @{typ nat});
-            fun mk_decisive t = %%: @{const_name decisive} \$ t;
-            fun f dn = mk_decisive (dc_take dn \$ n);
-            val goal = mk_trp (foldr1 mk_conj (map f dnames));
-            val rules0 = @{thm decisive_bottom} :: take_0_thms;
-            val rules1 =
-                take_Suc_thms @ decisive_abs_rep_thms
-                @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map};
-            val tacs = [
-                rtac @{thm nat.induct} 1,
-                simp_tac (HOL_ss addsimps rules0) 1,
-                asm_simp_tac (HOL_ss addsimps rules1) 1];
-          in pg [] goal (K tacs) end;
-        fun take_enough dn = mk_ex ("n",dc_take dn \$ Bound 0 ` %:"x" === %:"x");
-        fun one_finite (dn, decisive_thm) =
+        fun concf n dn = %:(P_name n) \$ %:(x_name n);
+        fun tacf {prems, context} =
let
-            val goal = mk_trp (%%:(dn^"_finite") \$ %:"x");
-            val tacs = [
-                rtac @{thm lub_ID_finite} 1,
-                resolve_tac chain_take_thms 1,
-                resolve_tac lub_take_thms 1,
-                rtac decisive_thm 1];
-          in pg finite_defs goal (K tacs) end;
-
-        val _ = trace " Proving finites";
-        val finites = map one_finite (dnames ~~ atomize global_ctxt decisive_lemma);
-        val _ = trace " Proving ind";
-        val ind =
-          let
-            fun concf n dn = %:(P_name n) \$ %:(x_name n);
-            fun tacf {prems, context} =
-              let
-                fun finite_tacs (finite, fin_ind) = [
-                  rtac(rewrite_rule finite_defs finite RS exE)1,
-                  etac subst 1,
-                  rtac fin_ind 1,
-                  ind_prems_tac prems];
-              in
-                TRY (safe_tac HOL_cs) ::
-                maps finite_tacs (finites ~~ atomize global_ctxt finite_ind)
-              end;
-          in pg'' thy [] (ind_term concf) tacf end;
-      in (finites, ind) end (* let *)
+            fun finite_tacs (take_induct, fin_ind) = [
+                rtac take_induct 1,
+                rtac fin_ind 1,
+                ind_prems_tac prems];
+          in
+            TRY (safe_tac HOL_cs) ::
+            maps finite_tacs (take_induct_thms ~~ atomize global_ctxt finite_ind)
+          end;
+      in pg'' thy [] (ind_term concf) tacf end

else (* infinite case *)
let
-        fun one_finite n dn =
-          read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
-        val finites = mapn one_finite 1 dnames;
-
val goal =
let
@@ -420,12 +378,12 @@
handle ERROR _ =>
(warning "Cannot prove infinite induction rule"; TrueI)
);
-      in (finites, ind) end
+      in ind end
)
handle THM _ =>
-             (warning "Induction proofs failed (THM raised)."; ([], TrueI))
+             (warning "Induction proofs failed (THM raised)."; TrueI)
| ERROR _ =>
-             (warning "Cannot prove induction rule"; ([], TrueI));
+             (warning "Cannot prove induction rule"; TrueI);

val case_ns =
let
@@ -445,7 +403,6 @@

-           ((Binding.name "finites"    , finites     ), []),
((Binding.name "finite_ind" , [finite_ind]), []),
((Binding.name "ind"        , [ind]       ), [])]
|> (if induct_failed then I```
```--- a/src/HOLCF/ex/Domain_ex.thy	Mon Mar 08 12:43:44 2010 -0800
+++ b/src/HOLCF/ex/Domain_ex.thy	Mon Mar 08 13:58:00 2010 -0800
@@ -107,7 +107,7 @@

subsection {* Generated constants and theorems *}

-domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (lazy right :: "'a tree")
+domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")

lemmas tree_abs_defined_iff =
iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
@@ -174,7 +174,7 @@
text {* Rules about finiteness predicate *}
term tree_finite
thm tree.finite_def
-thm tree.finites
+thm tree.finite (* only generated for flat datatypes *)

text {* Rules about bisimulation predicate *}
term tree_bisim
@@ -196,14 +196,6 @@
-- {* Inner syntax error at "= UU" *}
*)

-text {*
-  I don't know what is going on here.  The failed proof has to do with
-  the finiteness predicate.
-*}
-
-domain foo = Foo (lazy "bar") and bar = Bar
-  -- "Cannot prove induction rule"
-
text {* Declaring class constraints on the LHS is currently broken. *}
(*
domain ('a::cpo) box = Box (lazy 'a)```