author wenzelm Fri, 16 Nov 2001 22:10:27 +0100 changeset 12228 9e5d3c96111a parent 12227 c654c2c03f1d child 12229 bfba0eb5124b
converted;
 src/ZF/ex/CoUnit.ML file | annotate | diff | comparison | revisions src/ZF/ex/CoUnit.thy file | annotate | diff | comparison | revisions
```--- a/src/ZF/ex/CoUnit.ML	Fri Nov 16 22:09:44 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-(*  Title:      ZF/ex/CoUnit.ML
-    ID:         \$Id\$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Trivial codatatype definitions, one of which goes wrong!
-
-See discussion in
-  L C Paulson.  A Concrete Final Coalgebra Theorem for ZF Set Theory.
-  Report 334,  Cambridge University Computer Laboratory.  1994.
-*)
-
-(*USELESS because folding on Con(?xa) == ?xa fails*)
-val ConE = counit.mk_cases "Con(x) \\<in> counit";
-
-(*Proving freeness results*)
-val Con_iff = counit.mk_free "Con(x)=Con(y) <-> x=y";
-
-(*Should be a singleton, not everything!*)
-Goal "counit = quniv(0)";
-by (rtac (counit.dom_subset RS equalityI) 1);
-by (rtac subsetI 1);
-by (etac counit.coinduct 1);
-by (rtac subset_refl 1);
-by (rewrite_goals_tac counit.con_defs);
-by (Fast_tac 1);
-qed "counit_eq_univ";
-
-
-(*A similar example, but the constructor is non-degenerate and it works!
-  The resulting set is a singleton.
-*)
-
-val Con2E = counit2.mk_cases "Con2(x,y) \\<in> counit2";
-
-(*Proving freeness results*)
-val Con2_iff = counit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";
-
-Goalw counit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))";
-by (rtac bnd_monoI 1);
-by (REPEAT (ares_tac [subset_refl, QPair_subset_univ, QPair_mono] 1));
-qed "Con2_bnd_mono";
-
-Goal "lfp(univ(0), %x. Con2(x,x)) \\<in> counit2";
-by (rtac (singletonI RS counit2.coinduct) 1);
-by (rtac (qunivI RS singleton_subsetI) 1);
-by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);
-by (fast_tac (claset() addSIs [Con2_bnd_mono RS lfp_unfold]) 1);
-qed "lfp_Con2_in_counit2";
-
-(*Lemma for proving finality.  Borrowed from ex/llist_eq.ML!*)
-Goal "Ord(i) ==> \\<forall>x y. x \\<in> counit2 & y \\<in> counit2 --> x Int Vset(i) \\<subseteq> y";
-by (etac trans_induct 1);
-by (safe_tac subset_cs);
-by (etac counit2.elim 1);
-by (etac counit2.elim 1);
-by (rewrite_goals_tac counit2.con_defs);
-by (fast_tac (subset_cs
-	      addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
-qed "counit2_Int_Vset_subset_lemma";
-
-val counit2_Int_Vset_subset = standard
-        (counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);
-
-Goal "[| x \\<in> counit2;  y \\<in> counit2 |] ==> x=y";
-by (rtac equalityI 1);
-by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1));
-qed "counit2_implies_equal";
-
-Goal "counit2 = {lfp(univ(0), %x. Con2(x,x))}";
-by (rtac equalityI 1);
-by (rtac (lfp_Con2_in_counit2 RS singleton_subsetI) 2);
-by (rtac subsetI 1);
-by (dtac (lfp_Con2_in_counit2 RS counit2_implies_equal) 1);
-by (etac subst 1);
-by (rtac singletonI 1);
-qed "counit2_eq_univ";```
```--- a/src/ZF/ex/CoUnit.thy	Fri Nov 16 22:09:44 2001 +0100
+++ b/src/ZF/ex/CoUnit.thy	Fri Nov 16 22:10:27 2001 +0100
@@ -2,33 +2,102 @@
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-
-Trivial codatatype definitions, one of which goes wrong!
-
-See discussion in
-  L C Paulson.  A Concrete Final Coalgebra Theorem for ZF Set Theory.
-  Report 334,  Cambridge University Computer Laboratory.  1994.
*)

-CoUnit = Main +
+header {* Trivial codatatype definitions, one of which goes wrong! *}
+
+theory CoUnit = Main:

-(*This degenerate definition does not work well because the one constructor's
-  definition is trivial!  The same thing occurs with Aczel's Special Final
-  Coalgebra Theorem
-*)
+text {*
+  See discussion in: L C Paulson.  A Concrete Final Coalgebra Theorem
+  for ZF Set Theory.  Report 334, Cambridge University Computer
+  Laboratory.  1994.
+
+  \bigskip
+
+  This degenerate definition does not work well because the one
+  constructor's definition is trivial!  The same thing occurs with
+  Aczel's Special Final Coalgebra Theorem.
+*}
+
consts
counit :: i
codatatype
-  "counit" = Con ("x \\<in> counit")
+  "counit" = Con ("x \<in> counit")
+
+inductive_cases ConE: "Con(x) \<in> counit"
+  -- {* USELESS because folding on @{term "Con(xa) == xa"} fails. *}
+
+lemma Con_iff: "Con(x) = Con(y) <-> x = y"
+  -- {* Proving freeness results. *}
+  by (auto elim!: counit.free_elims)
+
+lemma counit_eq_univ: "counit = quniv(0)"
+  -- {* Should be a singleton, not everything! *}
+  apply (rule counit.dom_subset [THEN equalityI])
+  apply (rule subsetI)
+  apply (erule counit.coinduct)
+   apply (rule subset_refl)
+  apply (unfold counit.con_defs)
+  apply fast
+  done

-(*A similar example, but the constructor is non-degenerate and it works!
-  The resulting set is a singleton.
-*)
+text {*
+  \medskip A similar example, but the constructor is non-degenerate
+  and it works!  The resulting set is a singleton.
+*}

consts
counit2 :: i
codatatype
-  "counit2" = Con2 ("x \\<in> counit2", "y \\<in> counit2")
+  "counit2" = Con2 ("x \<in> counit2", "y \<in> counit2")
+
+
+inductive_cases Con2E: "Con2(x, y) \<in> counit2"
+
+lemma Con2_iff: "Con2(x, y) = Con2(x', y') <-> x = x' & y = y'"
+  -- {* Proving freeness results. *}
+  by (fast elim!: counit2.free_elims)
+
+lemma Con2_bnd_mono: "bnd_mono(univ(0), %x. Con2(x, x))"
+  apply (unfold counit2.con_defs)
+  apply (rule bnd_monoI)
+   apply (assumption | rule subset_refl QPair_subset_univ QPair_mono)+
+  done
+
+lemma lfp_Con2_in_counit2: "lfp(univ(0), %x. Con2(x,x)) \<in> counit2"
+  apply (rule singletonI [THEN counit2.coinduct])
+  apply (rule qunivI [THEN singleton_subsetI])
+  apply (rule subset_trans [OF lfp_subset empty_subsetI [THEN univ_mono]])
+  apply (fast intro!: Con2_bnd_mono [THEN lfp_unfold])
+  done
+
+lemma counit2_Int_Vset_subset [rule_format]:
+  "Ord(i) ==> \<forall>x y. x \<in> counit2 --> y \<in> counit2 --> x Int Vset(i) \<subseteq> y"
+  -- {* Lemma for proving finality. *}
+  apply (erule trans_induct)
+  apply (tactic "safe_tac subset_cs")
+  apply (erule counit2.cases)
+  apply (erule counit2.cases)
+  apply (unfold counit2.con_defs)
+  apply (tactic {* fast_tac (subset_cs
+    addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
+    addSEs [Ord_in_Ord, Pair_inject]) 1 *})
+  done
+
+lemma counit2_implies_equal: "[| x \<in> counit2;  y \<in> counit2 |] ==> x = y"
+  apply (rule equalityI)
+  apply (assumption | rule conjI counit2_Int_Vset_subset [THEN Int_Vset_subset])+
+  done
+
+lemma counit2_eq_univ: "counit2 = {lfp(univ(0), %x. Con2(x,x))}"
+  apply (rule equalityI)
+   apply (rule_tac [2] lfp_Con2_in_counit2 [THEN singleton_subsetI])
+  apply (rule subsetI)
+  apply (drule lfp_Con2_in_counit2 [THEN counit2_implies_equal])
+  apply (erule subst)
+  apply (rule singletonI)
+  done

end```