src/ZF/ex/CoUnit.thy
author wenzelm
Thu, 07 Apr 2016 20:51:52 +0200
changeset 62908 d7009a515733
parent 61798 27f3c10b0b50
child 65449 c82e63b11b8b
permissions -rw-r--r--
clarified mode of ROOT.ML files;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35762
af3ff2ba4c54 removed old CVS Ids;
wenzelm
parents: 24893
diff changeset
     1
(*  Title:      ZF/ex/CoUnit.thy
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
     3
    Copyright   1994  University of Cambridge
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
     4
*)
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
     5
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
     6
section \<open>Trivial codatatype definitions, one of which goes wrong!\<close>
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 12228
diff changeset
     8
theory CoUnit imports Main begin
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
     9
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    10
text \<open>
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    11
  See discussion in: L C Paulson.  A Concrete Final Coalgebra Theorem
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    12
  for ZF Set Theory.  Report 334, Cambridge University Computer
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    13
  Laboratory.  1994.
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    14
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    15
  \bigskip
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    16
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    17
  This degenerate definition does not work well because the one
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    18
  constructor's definition is trivial!  The same thing occurs with
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    19
  Aczel's Special Final Coalgebra Theorem.
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    20
\<close>
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    21
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    22
consts
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 810
diff changeset
    23
  counit :: i
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    24
codatatype
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    25
  "counit" = Con ("x \<in> counit")
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    26
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    27
inductive_cases ConE: "Con(x) \<in> counit"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    28
  \<comment> \<open>USELESS because folding on @{term "Con(xa) == xa"} fails.\<close>
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    29
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 42793
diff changeset
    30
lemma Con_iff: "Con(x) = Con(y) \<longleftrightarrow> x = y"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    31
  \<comment> \<open>Proving freeness results.\<close>
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    32
  by (auto elim!: counit.free_elims)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    33
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    34
lemma counit_eq_univ: "counit = quniv(0)"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    35
  \<comment> \<open>Should be a singleton, not everything!\<close>
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    36
  apply (rule counit.dom_subset [THEN equalityI])
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    37
  apply (rule subsetI)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    38
  apply (erule counit.coinduct)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    39
   apply (rule subset_refl)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    40
  apply (unfold counit.con_defs)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    41
  apply fast
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    42
  done
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    43
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    44
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    45
text \<open>
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    46
  \medskip A similar example, but the constructor is non-degenerate
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    47
  and it works!  The resulting set is a singleton.
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    48
\<close>
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    49
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    50
consts
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 810
diff changeset
    51
  counit2 :: i
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
    52
codatatype
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    53
  "counit2" = Con2 ("x \<in> counit2", "y \<in> counit2")
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    54
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    55
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    56
inductive_cases Con2E: "Con2(x, y) \<in> counit2"
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    57
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 42793
diff changeset
    58
lemma Con2_iff: "Con2(x, y) = Con2(x', y') \<longleftrightarrow> x = x' & y = y'"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    59
  \<comment> \<open>Proving freeness results.\<close>
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    60
  by (fast elim!: counit2.free_elims)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    61
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    62
lemma Con2_bnd_mono: "bnd_mono(univ(0), %x. Con2(x, x))"
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    63
  apply (unfold counit2.con_defs)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    64
  apply (rule bnd_monoI)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    65
   apply (assumption | rule subset_refl QPair_subset_univ QPair_mono)+
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    66
  done
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    67
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    68
lemma lfp_Con2_in_counit2: "lfp(univ(0), %x. Con2(x,x)) \<in> counit2"
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    69
  apply (rule singletonI [THEN counit2.coinduct])
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    70
  apply (rule qunivI [THEN singleton_subsetI])
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    71
  apply (rule subset_trans [OF lfp_subset empty_subsetI [THEN univ_mono]])
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    72
  apply (fast intro!: Con2_bnd_mono [THEN lfp_unfold])
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    73
  done
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    74
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    75
lemma counit2_Int_Vset_subset [rule_format]:
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 42793
diff changeset
    76
  "Ord(i) ==> \<forall>x y. x \<in> counit2 \<longrightarrow> y \<in> counit2 \<longrightarrow> x \<inter> Vset(i) \<subseteq> y"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    77
  \<comment> \<open>Lemma for proving finality.\<close>
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    78
  apply (erule trans_induct)
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 35762
diff changeset
    79
  apply (tactic "safe_tac (put_claset subset_cs @{context})")
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    80
  apply (erule counit2.cases)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    81
  apply (erule counit2.cases)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    82
  apply (unfold counit2.con_defs)
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    83
  apply (tactic \<open>fast_tac (put_claset subset_cs @{context}
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    84
    addSIs [@{thm QPair_Int_Vset_subset_UN} RS @{thm subset_trans}, @{thm QPair_mono}]
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    85
    addSEs [@{thm Ord_in_Ord}, @{thm Pair_inject}]) 1\<close>)
12228
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    86
  done
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    87
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    88
lemma counit2_implies_equal: "[| x \<in> counit2;  y \<in> counit2 |] ==> x = y"
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    89
  apply (rule equalityI)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    90
  apply (assumption | rule conjI counit2_Int_Vset_subset [THEN Int_Vset_subset])+
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    91
  done
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    92
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    93
lemma counit2_eq_univ: "counit2 = {lfp(univ(0), %x. Con2(x,x))}"
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    94
  apply (rule equalityI)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    95
   apply (rule_tac [2] lfp_Con2_in_counit2 [THEN singleton_subsetI])
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    96
  apply (rule subsetI)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    97
  apply (drule lfp_Con2_in_counit2 [THEN counit2_implies_equal])
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    98
  apply (erule subst)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
    99
  apply (rule singletonI)
9e5d3c96111a converted;
wenzelm
parents: 11354
diff changeset
   100
  done
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
   101
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents:
diff changeset
   102
end