src/HOLCF/Ssum.thy
author huffman
Tue, 26 Jul 2005 18:28:11 +0200
changeset 16921 16094ed8ac6b
parent 16823 13f3768a6f14
child 17817 405fb812e738
permissions -rw-r--r--
renamed Exh_Ssum1 to Exh_Ssum; cleaned up
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15600
a59f07556a8d fixed filename in header
huffman
parents: 15593
diff changeset
     1
(*  Title:      HOLCF/Ssum.thy
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     2
    ID:         $Id$
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
     3
    Author:     Franz Regensburger and Brian Huffman
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     4
16070
4a83dd540b88 removed LICENCE note -- everything is subject to Isabelle licence as
wenzelm
parents: 16060
diff changeset
     5
Strict sum with typedef.
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     6
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     7
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     8
header {* The type of strict sums *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     9
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    10
theory Ssum
16699
24b494ff8f0f use new pcpodef package
huffman
parents: 16316
diff changeset
    11
imports Cprod
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    12
begin
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    13
16083
fca38c55c8fa added defaultsort declaration, moved cpair_less to Cprod.thy
huffman
parents: 16070
diff changeset
    14
defaultsort pcpo
fca38c55c8fa added defaultsort declaration, moved cpair_less to Cprod.thy
huffman
parents: 16070
diff changeset
    15
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    16
subsection {* Definition of strict sum type *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    17
16699
24b494ff8f0f use new pcpodef package
huffman
parents: 16316
diff changeset
    18
pcpodef (Ssum)  ('a, 'b) "++" (infixr 10) = 
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    19
        "{p::'a \<times> 'b. cfst\<cdot>p = \<bottom> \<or> csnd\<cdot>p = \<bottom>}"
16699
24b494ff8f0f use new pcpodef package
huffman
parents: 16316
diff changeset
    20
by simp
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    21
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    22
syntax (xsymbols)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    23
  "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    24
syntax (HTML output)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    25
  "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    26
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    27
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    28
subsection {* Definitions of constructors *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    29
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    30
constdefs
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    31
  sinl :: "'a \<rightarrow> ('a ++ 'b)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    32
  "sinl \<equiv> \<Lambda> a. Abs_Ssum <a, \<bottom>>"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    33
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    34
  sinr :: "'b \<rightarrow> ('a ++ 'b)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    35
  "sinr \<equiv> \<Lambda> b. Abs_Ssum <\<bottom>, b>"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    36
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    37
subsection {* Properties of @{term sinl} and @{term sinr} *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    38
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    39
lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum <a, \<bottom>>"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    40
by (unfold sinl_def, simp add: cont_Abs_Ssum Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    41
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    42
lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum <\<bottom>, b>"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    43
by (unfold sinr_def, simp add: cont_Abs_Ssum Ssum_def)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    44
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    45
lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = <a, \<bottom>>"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    46
by (unfold sinl_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    47
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    48
lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = <\<bottom>, b>"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    49
by (unfold sinr_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    50
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    51
lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    52
by (simp add: sinl_Abs_Ssum Abs_Ssum_strict cpair_strict)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    53
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    54
lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    55
by (simp add: sinr_Abs_Ssum Abs_Ssum_strict cpair_strict)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    56
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    57
lemma sinl_eq [simp]: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)"
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    58
by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    59
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    60
lemma sinr_eq [simp]: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)"
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    61
by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    62
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    63
lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y"
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    64
by (rule sinl_eq [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    65
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    66
lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y"
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    67
by (rule sinr_eq [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    68
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    69
lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    70
apply (rule sinl_strict [THEN subst])
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    71
apply (rule sinl_eq)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    72
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    73
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    74
lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    75
apply (rule sinr_strict [THEN subst])
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    76
apply (rule sinr_eq)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    77
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    78
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    79
lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    80
by simp
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    81
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    82
lemma sinr_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    83
by simp
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    84
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    85
subsection {* Case analysis *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    86
16921
16094ed8ac6b renamed Exh_Ssum1 to Exh_Ssum; cleaned up
huffman
parents: 16823
diff changeset
    87
lemma Exh_Ssum: 
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    88
  "z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)"
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    89
apply (rule_tac x=z in Abs_Ssum_induct)
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
    90
apply (rule_tac p=y in cprodE)
16921
16094ed8ac6b renamed Exh_Ssum1 to Exh_Ssum; cleaned up
huffman
parents: 16823
diff changeset
    91
apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum)
16094ed8ac6b renamed Exh_Ssum1 to Exh_Ssum; cleaned up
huffman
parents: 16823
diff changeset
    92
apply (simp add: Abs_Ssum_inject Ssum_def)
16094ed8ac6b renamed Exh_Ssum1 to Exh_Ssum; cleaned up
huffman
parents: 16823
diff changeset
    93
apply (auto simp add: cpair_strict Abs_Ssum_strict)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    94
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    95
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    96
lemma ssumE:
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    97
  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    98
   \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    99
   \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
16921
16094ed8ac6b renamed Exh_Ssum1 to Exh_Ssum; cleaned up
huffman
parents: 16823
diff changeset
   100
by (cut_tac z=p in Exh_Ssum, auto)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   101
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   102
lemma ssumE2:
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   103
  "\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   104
apply (rule_tac p=p in ssumE)
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
   105
apply (simp only: sinl_strict [symmetric])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   106
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   107
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   108
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   109
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   110
subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   111
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   112
lemma sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
16699
24b494ff8f0f use new pcpodef package
huffman
parents: 16316
diff changeset
   113
by (simp add: less_Ssum_def Rep_Ssum_sinl cpair_less)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   114
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   115
lemma sinr_less [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
16699
24b494ff8f0f use new pcpodef package
huffman
parents: 16316
diff changeset
   116
by (simp add: less_Ssum_def Rep_Ssum_sinr cpair_less)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   117
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   118
lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   119
by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   120
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   121
lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
16699
24b494ff8f0f use new pcpodef package
huffman
parents: 16316
diff changeset
   122
by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   123
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   124
lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   125
by (simp add: po_eq_conv)
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   126
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   127
lemma sinr_eq_sinl [simp]: "(sinr\<cdot>x = sinl\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   128
by (simp add: po_eq_conv)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   129
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   130
subsection {* Chains of strict sums *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   131
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   132
lemma less_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   133
apply (rule_tac p=p in ssumE)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   134
apply (rule_tac x="\<bottom>" in exI, simp)
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   135
apply simp
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   136
apply simp
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   137
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   138
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   139
lemma less_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   140
apply (rule_tac p=p in ssumE)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   141
apply (rule_tac x="\<bottom>" in exI, simp)
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   142
apply simp
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   143
apply simp
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   144
done
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   145
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   146
lemma ssum_chain_lemma:
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   147
"chain Y \<Longrightarrow> (\<exists>A. chain A \<and> Y = (\<lambda>i. sinl\<cdot>(A i))) \<or>
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   148
             (\<exists>B. chain B \<and> Y = (\<lambda>i. sinr\<cdot>(B i)))"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   149
 apply (rule_tac p="lub (range Y)" in ssumE2)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   150
  apply (rule disjI1)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   151
  apply (rule_tac x="\<lambda>i. cfst\<cdot>(Rep_Ssum (Y i))" in exI)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   152
  apply (rule conjI)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   153
   apply (rule chain_monofun)
16742
d1641dba61e5 use theorem ch2ch_cont
huffman
parents: 16699
diff changeset
   154
   apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   155
  apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   156
  apply (drule less_sinlD, clarify)
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   157
  apply (simp add: Rep_Ssum_sinl)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   158
 apply (rule disjI2)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   159
 apply (rule_tac x="\<lambda>i. csnd\<cdot>(Rep_Ssum (Y i))" in exI)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   160
 apply (rule conjI)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   161
  apply (rule chain_monofun)
16742
d1641dba61e5 use theorem ch2ch_cont
huffman
parents: 16699
diff changeset
   162
  apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   163
 apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   164
 apply (drule less_sinrD, clarify)
16752
270ec60cc9e8 added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
huffman
parents: 16742
diff changeset
   165
 apply (simp add: Rep_Ssum_sinr)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   166
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   167
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   168
subsection {* Definitions of constants *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   169
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   170
constdefs
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   171
  Iwhen :: "['a \<rightarrow> 'c, 'b \<rightarrow> 'c, 'a ++ 'b] \<Rightarrow> 'c"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   172
  "Iwhen \<equiv> \<lambda>f g s.
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   173
    if cfst\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then f\<cdot>(cfst\<cdot>(Rep_Ssum s)) else
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   174
    if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   175
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   176
text {* rewrites for @{term Iwhen} *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   177
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   178
lemma Iwhen1 [simp]: "Iwhen f g \<bottom> = \<bottom>"
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
   179
by (simp add: Iwhen_def Rep_Ssum_strict)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   180
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   181
lemma Iwhen2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinl\<cdot>x) = f\<cdot>x"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   182
by (simp add: Iwhen_def Rep_Ssum_sinl)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   183
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   184
lemma Iwhen3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinr\<cdot>y) = g\<cdot>y"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   185
by (simp add: Iwhen_def Rep_Ssum_sinr)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   186
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   187
lemma Iwhen4: "Iwhen f g (sinl\<cdot>x) = strictify\<cdot>f\<cdot>x"
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
   188
by (simp add: strictify_conv_if)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   189
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   190
lemma Iwhen5: "Iwhen f g (sinr\<cdot>y) = strictify\<cdot>g\<cdot>y"
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
   191
by (simp add: strictify_conv_if)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   192
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   193
subsection {* Continuity of @{term Iwhen} *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   194
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   195
text {* @{term Iwhen} is continuous in all arguments *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   196
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   197
lemma cont_Iwhen1: "cont (\<lambda>f. Iwhen f g s)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   198
by (rule_tac p=s in ssumE, simp_all)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   199
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   200
lemma cont_Iwhen2: "cont (\<lambda>g. Iwhen f g s)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   201
by (rule_tac p=s in ssumE, simp_all)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   202
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   203
lemma cont_Iwhen3: "cont (\<lambda>s. Iwhen f g s)"
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
   204
apply (rule contI)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   205
apply (drule ssum_chain_lemma, safe)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   206
apply (simp add: contlub_cfun_arg [symmetric])
16823
13f3768a6f14 simplified proof of cont_Iwhen3
huffman
parents: 16752
diff changeset
   207
apply (simp add: Iwhen4 cont_cfun_arg)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   208
apply (simp add: contlub_cfun_arg [symmetric])
16823
13f3768a6f14 simplified proof of cont_Iwhen3
huffman
parents: 16752
diff changeset
   209
apply (simp add: Iwhen5 cont_cfun_arg)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   210
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   211
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   212
subsection {* Continuous versions of constants *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   213
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   214
constdefs
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   215
  sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   216
  "sscase \<equiv> \<Lambda> f g s. Iwhen f g s"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   217
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   218
translations
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   219
"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   220
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   221
text {* continuous versions of lemmas for @{term sscase} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   222
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   223
lemma beta_sscase: "sscase\<cdot>f\<cdot>g\<cdot>s = Iwhen f g s"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   224
by (simp add: sscase_def cont_Iwhen1 cont_Iwhen2 cont_Iwhen3)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   225
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   226
lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   227
by (simp add: beta_sscase)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   228
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   229
lemma sscase2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = f\<cdot>x"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   230
by (simp add: beta_sscase)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   231
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   232
lemma sscase3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>y) = g\<cdot>y"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   233
by (simp add: beta_sscase)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   234
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   235
lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   236
by (rule_tac p=z in ssumE, simp_all)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   237
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   238
end