src/HOLCF/Ssum.thy
author wenzelm
Sun, 21 Oct 2007 14:21:48 +0200
changeset 25131 2c8caac48ade
parent 19440 b2877e230b07
child 25740 de65baf89106
permissions -rw-r--r--
modernized specifications ('definition', 'abbreviation', 'notation');
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
17817
405fb812e738 add names to infix declarations
huffman
parents: 16921
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
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
    30
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
    31
  sinl :: "'a \<rightarrow> ('a ++ 'b)" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
    32
  "sinl = (\<Lambda> a. Abs_Ssum <a, \<bottom>>)"
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    33
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
    34
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
    35
  sinr :: "'b \<rightarrow> ('a ++ 'b)" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
    36
  "sinr = (\<Lambda> b. Abs_Ssum <\<bottom>, b>)"
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    37
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    38
subsection {* Properties of @{term sinl} and @{term sinr} *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    39
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    40
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
    41
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
    42
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    43
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
    44
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
    45
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    46
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
    47
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
    48
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    49
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
    50
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
    51
17837
2922be3544f8 added compactness lemmas; cleaned up
huffman
parents: 17817
diff changeset
    52
lemma compact_sinl [simp]: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
2922be3544f8 added compactness lemmas; cleaned up
huffman
parents: 17817
diff changeset
    53
by (rule compact_Ssum, simp add: Rep_Ssum_sinl)
2922be3544f8 added compactness lemmas; cleaned up
huffman
parents: 17817
diff changeset
    54
2922be3544f8 added compactness lemmas; cleaned up
huffman
parents: 17817
diff changeset
    55
lemma compact_sinr [simp]: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"
2922be3544f8 added compactness lemmas; cleaned up
huffman
parents: 17817
diff changeset
    56
by (rule compact_Ssum, simp add: Rep_Ssum_sinr)
2922be3544f8 added compactness lemmas; cleaned up
huffman
parents: 17817
diff changeset
    57
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    58
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
    59
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
    60
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    61
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
    62
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
    63
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
    64
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
    65
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
    66
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
    67
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
    68
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
    69
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
    70
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
    71
by (rule sinl_eq [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    72
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
    73
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
    74
by (rule sinr_eq [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    75
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
    76
lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
17837
2922be3544f8 added compactness lemmas; cleaned up
huffman
parents: 17817
diff changeset
    77
by (cut_tac sinl_eq [of "x" "\<bottom>"], simp)
15576
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 sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
17837
2922be3544f8 added compactness lemmas; cleaned up
huffman
parents: 17817
diff changeset
    80
by (cut_tac sinr_eq [of "x" "\<bottom>"], simp)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    81
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
    82
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
    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
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
    85
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
    86
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
    87
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    88
subsection {* Case analysis *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    89
16921
16094ed8ac6b renamed Exh_Ssum1 to Exh_Ssum; cleaned up
huffman
parents: 16823
diff changeset
    90
lemma Exh_Ssum: 
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    91
  "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
    92
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
    93
apply (rule_tac p=y in cprodE)
16921
16094ed8ac6b renamed Exh_Ssum1 to Exh_Ssum; cleaned up
huffman
parents: 16823
diff changeset
    94
apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum)
16094ed8ac6b renamed Exh_Ssum1 to Exh_Ssum; cleaned up
huffman
parents: 16823
diff changeset
    95
apply (simp add: Abs_Ssum_inject Ssum_def)
16094ed8ac6b renamed Exh_Ssum1 to Exh_Ssum; cleaned up
huffman
parents: 16823
diff changeset
    96
apply (auto simp add: cpair_strict Abs_Ssum_strict)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    97
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    98
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    99
lemma ssumE:
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   100
  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   101
   \<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
   102
   \<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
   103
by (cut_tac z=p in Exh_Ssum, auto)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   104
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   105
lemma ssumE2:
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   106
  "\<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
   107
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
   108
apply (simp only: sinl_strict [symmetric])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   109
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   110
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   111
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   112
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   113
subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
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 sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
18078
20e5a6440790 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents: 17837
diff changeset
   116
by (simp add: less_Ssum_def Rep_Ssum_sinl)
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 sinr_less [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
18078
20e5a6440790 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents: 17837
diff changeset
   119
by (simp add: less_Ssum_def Rep_Ssum_sinr)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   120
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
   121
lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
19440
b2877e230b07 add lemma less_UU_iff as default simp rule
huffman
parents: 18078
diff changeset
   122
by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr)
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
   123
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 sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
19440
b2877e230b07 add lemma less_UU_iff as default simp rule
huffman
parents: 18078
diff changeset
   125
by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   126
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
   127
lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
19440
b2877e230b07 add lemma less_UU_iff as default simp rule
huffman
parents: 18078
diff changeset
   128
by (subst po_eq_conv, 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
   129
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
   130
lemma sinr_eq_sinl [simp]: "(sinr\<cdot>x = sinl\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
19440
b2877e230b07 add lemma less_UU_iff as default simp rule
huffman
parents: 18078
diff changeset
   131
by (subst po_eq_conv, simp)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   132
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   133
subsection {* Chains of strict sums *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   134
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   135
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
   136
apply (rule_tac p=p in ssumE)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   137
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
   138
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
   139
apply simp
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   140
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   141
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   142
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
   143
apply (rule_tac p=p in ssumE)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   144
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
   145
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
   146
apply simp
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   147
done
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   148
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   149
lemma ssum_chain_lemma:
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   150
"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
   151
             (\<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
   152
 apply (rule_tac p="lub (range Y)" in ssumE2)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   153
  apply (rule disjI1)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   154
  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
   155
  apply (rule conjI)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   156
   apply (rule chain_monofun)
16742
d1641dba61e5 use theorem ch2ch_cont
huffman
parents: 16699
diff changeset
   157
   apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   158
  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
   159
  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
   160
  apply (simp add: Rep_Ssum_sinl)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   161
 apply (rule disjI2)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   162
 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
   163
 apply (rule conjI)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   164
  apply (rule chain_monofun)
16742
d1641dba61e5 use theorem ch2ch_cont
huffman
parents: 16699
diff changeset
   165
  apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   166
 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
   167
 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
   168
 apply (simp add: Rep_Ssum_sinr)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   169
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   170
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   171
subsection {* Definitions of constants *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   172
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
   173
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
   174
  Iwhen :: "['a \<rightarrow> 'c, 'b \<rightarrow> 'c, 'a ++ 'b] \<Rightarrow> 'c" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
   175
  "Iwhen = (\<lambda>f g s.
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   176
    if cfst\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then f\<cdot>(cfst\<cdot>(Rep_Ssum s)) else
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
   177
    if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>)"
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   178
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   179
text {* rewrites for @{term Iwhen} *}
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 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
   182
by (simp add: Iwhen_def Rep_Ssum_strict)
16060
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 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
   185
by (simp add: Iwhen_def Rep_Ssum_sinl)
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 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
   188
by (simp add: Iwhen_def Rep_Ssum_sinr)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   189
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   190
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
   191
by (simp add: strictify_conv_if)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   192
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   193
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
   194
by (simp add: strictify_conv_if)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   195
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   196
subsection {* Continuity of @{term Iwhen} *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   197
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   198
text {* @{term Iwhen} is continuous in all arguments *}
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_Iwhen1: "cont (\<lambda>f. 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_Iwhen2: "cont (\<lambda>g. Iwhen f g s)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   204
by (rule_tac p=s in ssumE, simp_all)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   205
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   206
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
   207
apply (rule contI)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   208
apply (drule ssum_chain_lemma, safe)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   209
apply (simp add: contlub_cfun_arg [symmetric])
16823
13f3768a6f14 simplified proof of cont_Iwhen3
huffman
parents: 16752
diff changeset
   210
apply (simp add: Iwhen4 cont_cfun_arg)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   211
apply (simp add: contlub_cfun_arg [symmetric])
16823
13f3768a6f14 simplified proof of cont_Iwhen3
huffman
parents: 16752
diff changeset
   212
apply (simp add: Iwhen5 cont_cfun_arg)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   213
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   214
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   215
subsection {* Continuous versions of constants *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   216
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
   217
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
   218
  sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
   219
  "sscase = (\<Lambda> f g s. Iwhen f g s)"
16060
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
translations
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
   222
  "case s of CONST sinl\<cdot>x \<Rightarrow> t1 | CONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
18078
20e5a6440790 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents: 17837
diff changeset
   223
20e5a6440790 change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents: 17837
diff changeset
   224
translations
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
   225
  "\<Lambda>(CONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 19440
diff changeset
   226
  "\<Lambda>(CONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   227
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   228
text {* continuous versions of lemmas for @{term sscase} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   229
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   230
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
   231
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
   232
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   233
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
   234
by (simp add: beta_sscase)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   235
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   236
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
   237
by (simp add: beta_sscase)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   238
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   239
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
   240
by (simp add: beta_sscase)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   241
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   242
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
   243
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
   244
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   245
end