src/HOLCF/Ssum.thy
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16211 faa9691da2bc
child 16316 17db5df51a35
permissions -rw-r--r--
New theory with lemmas for the fixrec package
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
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    11
imports Cprod TypedefPcpo
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
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    18
typedef (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>}"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    20
by (rule_tac x="<\<bottom>,\<bottom>>" in exI, 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
subsection {* Class instances *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    28
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    29
instance "++" :: (pcpo, pcpo) sq_ord ..
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    30
defs (overloaded)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    31
  less_ssum_def: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_Ssum x \<sqsubseteq> Rep_Ssum y"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    32
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    33
lemma adm_Ssum: "adm (\<lambda>x. x \<in> Ssum)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    34
by (simp add: Ssum_def cont_fst cont_snd)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    35
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    36
lemma UU_Ssum: "\<bottom> \<in> Ssum"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    37
by (simp add: Ssum_def inst_cprod_pcpo2)
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
instance "++" :: (pcpo, pcpo) po
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    40
by (rule typedef_po [OF type_definition_Ssum less_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
instance "++" :: (pcpo, pcpo) cpo
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    43
by (rule typedef_cpo [OF type_definition_Ssum less_ssum_def adm_Ssum])
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
instance "++" :: (pcpo, pcpo) pcpo
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    46
by (rule typedef_pcpo_UU [OF type_definition_Ssum less_ssum_def UU_Ssum])
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
lemmas cont_Rep_Ssum =
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    49
  typedef_cont_Rep [OF type_definition_Ssum less_ssum_def adm_Ssum]
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    50
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    51
lemmas cont_Abs_Ssum = 
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    52
  typedef_cont_Abs [OF type_definition_Ssum less_ssum_def adm_Ssum]
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    53
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    54
lemmas Rep_Ssum_strict =
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    55
  typedef_Rep_strict [OF type_definition_Ssum less_ssum_def UU_Ssum]
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    56
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    57
lemmas Abs_Ssum_strict =
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    58
  typedef_Abs_strict [OF type_definition_Ssum less_ssum_def UU_Ssum]
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    59
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    60
lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>"
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    61
by (simp add: Abs_Ssum_strict inst_cprod_pcpo2 [symmetric])
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    62
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    63
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    64
subsection {* Definitions of constructors *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    65
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    66
constdefs
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    67
  sinl :: "'a \<rightarrow> ('a ++ 'b)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    68
  "sinl \<equiv> \<Lambda> a. Abs_Ssum <a, \<bottom>>"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    69
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    70
  sinr :: "'b \<rightarrow> ('a ++ 'b)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    71
  "sinr \<equiv> \<Lambda> b. Abs_Ssum <\<bottom>, b>"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    72
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    73
subsection {* Properties of @{term sinl} and @{term sinr} *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    74
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    75
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
    76
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
    77
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    78
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
    79
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
    80
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    81
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
    82
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
    83
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    84
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
    85
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
    86
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    87
lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    88
by (simp add: sinl_Abs_Ssum UU_Abs_Ssum)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    89
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    90
lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    91
by (simp add: sinr_Abs_Ssum UU_Abs_Ssum)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    92
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    93
lemma noteq_sinlsinr: "sinl\<cdot>a = sinr\<cdot>b \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    94
apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum)
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    95
apply (simp add: Abs_Ssum_inject Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    96
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    97
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
    98
lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y"
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
    99
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
   100
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
   101
lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y"
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   102
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
   103
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   104
lemma sinl_eq: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   105
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
   106
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   107
lemma sinr_eq: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   108
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
   109
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
   110
lemma sinl_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   111
apply (erule contrapos_nn)
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
   112
apply (rule sinl_inject)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   113
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   114
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   115
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
   116
lemma sinr_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   117
apply (erule contrapos_nn)
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16083
diff changeset
   118
apply (rule sinr_inject)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   119
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   120
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   121
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   122
subsection {* Case analysis *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   123
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   124
lemma Exh_Ssum1: 
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   125
  "z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   126
apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum UU_Abs_Ssum)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   127
apply (rule_tac x=z in Abs_Ssum_cases)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   128
apply (rule_tac p=y in cprodE)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   129
apply (auto simp add: Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   130
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   131
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   132
lemma ssumE:
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   133
  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   134
   \<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
   135
   \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   136
by (cut_tac z=p in Exh_Ssum1, auto)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   137
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   138
lemma ssumE2:
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   139
  "\<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
   140
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
   141
apply (simp only: sinl_strict [symmetric])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   142
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   143
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   144
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   145
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   146
subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   147
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   148
lemma less_ssum4a: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   149
by (simp add: less_ssum_def Rep_Ssum_sinl cpair_less)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   150
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   151
lemma less_ssum4b: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   152
by (simp add: less_ssum_def Rep_Ssum_sinr cpair_less)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   153
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   154
lemma less_ssum4c: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   155
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
   156
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   157
lemma less_ssum4d: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   158
by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   159
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   160
subsection {* Chains of strict sums *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   161
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   162
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
   163
apply (rule_tac p=p in ssumE)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   164
apply (rule_tac x="\<bottom>" in exI, simp)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   165
apply (simp add: less_ssum4a sinl_eq)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   166
apply (simp add: less_ssum4d)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   167
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   168
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   169
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
   170
apply (rule_tac p=p in ssumE)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   171
apply (rule_tac x="\<bottom>" in exI, simp)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   172
apply (simp add: less_ssum4c)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   173
apply (simp add: less_ssum4b sinr_eq)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   174
done
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
lemma ssum_chain_lemma:
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   177
"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
   178
             (\<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
   179
 apply (rule_tac p="lub (range Y)" in ssumE2)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   180
  apply (rule disjI1)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   181
  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
   182
  apply (rule conjI)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   183
   apply (rule chain_monofun)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   184
   apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun])
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   185
  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
   186
  apply (drule less_sinlD, clarify)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   187
  apply (simp add: sinl_eq Rep_Ssum_sinl)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   188
 apply (rule disjI2)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   189
 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
   190
 apply (rule conjI)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   191
  apply (rule chain_monofun)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   192
  apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun])
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   193
 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
   194
 apply (drule less_sinrD, clarify)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   195
 apply (simp add: sinr_eq Rep_Ssum_sinr)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   196
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   197
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   198
subsection {* Definitions of constants *}
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
constdefs
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   201
  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
   202
  "Iwhen \<equiv> \<lambda>f g s.
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   203
    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
   204
    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
   205
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   206
text {* rewrites for @{term Iwhen} *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   207
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   208
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
   209
by (simp add: Iwhen_def Rep_Ssum_strict)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   210
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   211
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
   212
by (simp add: Iwhen_def Rep_Ssum_sinl)
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
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
   215
by (simp add: Iwhen_def Rep_Ssum_sinr)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   216
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   217
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
   218
by (simp add: strictify_conv_if)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   219
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   220
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
   221
by (simp add: strictify_conv_if)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   222
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   223
subsection {* Continuity of @{term Iwhen} *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   224
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   225
text {* @{term Iwhen} is continuous in all arguments *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   226
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   227
lemma cont_Iwhen1: "cont (\<lambda>f. Iwhen f g s)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   228
by (rule_tac p=s in ssumE, simp_all)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   229
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   230
lemma cont_Iwhen2: "cont (\<lambda>g. Iwhen f g s)"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   231
by (rule_tac p=s in ssumE, simp_all)
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 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
   234
apply (rule contI)
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   235
apply (drule ssum_chain_lemma, safe)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   236
apply (simp add: contlub_cfun_arg [symmetric])
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   237
apply (simp add: Iwhen4)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   238
apply (simp add: contlub_cfun_arg)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   239
apply (simp add: thelubE chain_monofun)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   240
apply (simp add: contlub_cfun_arg [symmetric])
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   241
apply (simp add: Iwhen5)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   242
apply (simp add: contlub_cfun_arg)
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   243
apply (simp add: thelubE chain_monofun)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   244
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   245
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   246
subsection {* Continuous versions of constants *}
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   247
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   248
constdefs
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   249
  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
   250
  "sscase \<equiv> \<Lambda> f g s. Iwhen f g s"
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   251
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   252
translations
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   253
"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
   254
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   255
text {* continuous versions of lemmas for @{term sscase} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   256
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   257
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
   258
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
   259
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   260
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
   261
by (simp add: beta_sscase)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   262
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   263
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
   264
by (simp add: beta_sscase)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   265
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   266
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
   267
by (simp add: beta_sscase)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   268
16060
833be7f71ecd Simplified version of strict sum theory, using TypedefPcpo
huffman
parents: 15606
diff changeset
   269
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
   270
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
   271
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   272
end