src/HOLCF/Ssum.thy
author huffman
Fri, 11 Mar 2005 23:58:31 +0100
changeset 15606 95617b30514b
parent 15600 a59f07556a8d
child 16060 833be7f71ecd
permissions -rw-r--r--
simplified some definitions, many proofs are much shorter
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$
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     3
    Author:     Franz Regensburger
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     5
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     6
Strict sum with typedef
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
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     9
header {* The type of strict sums *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    10
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    11
theory Ssum
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    12
imports Cprod
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
    13
begin
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    14
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    15
subsection {* Definition of strict sum type *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    16
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    17
typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    18
        "{p::'a * 'b. fst p = UU | snd p = UU}"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    19
by auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    20
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    21
syntax (xsymbols)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    22
  "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    23
syntax (HTML output)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    24
  "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    25
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    26
consts
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    27
  Isinl         :: "'a => ('a ++ 'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    28
  Isinr         :: "'b => ('a ++ 'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    29
  Iwhen         :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    30
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    31
defs   -- {*defining the abstract constants*}
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    32
  Isinl_def:     "Isinl(a) == Abs_Ssum(a,UU)"
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    33
  Isinr_def:     "Isinr(b) == Abs_Ssum(UU,b)"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    34
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    35
  Iwhen_def:     "Iwhen(f)(g)(s) == case Rep_Ssum s of (a,b) =>
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    36
                         if a ~= UU then f$a else
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    37
                         if b ~= UU then g$b else UU"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    38
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    39
lemma inj_on_Abs_Ssum: "inj_on Abs_Ssum Ssum"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    40
apply (rule inj_on_inverseI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    41
apply (erule Abs_Ssum_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    42
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    43
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    44
text {* Strictness of @{term Isinl}, @{term Isinr} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    45
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    46
lemma strict_IsinlIsinr: "Isinl(UU) = Isinr(UU)"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    47
by (simp add: Isinl_def Isinr_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    48
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    49
text {* distinctness of @{term Isinl}, @{term Isinr} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    50
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    51
lemma noteq_IsinlIsinr: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    52
        "Isinl(a)=Isinr(b) ==> a=UU & b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    53
apply (unfold Isinl_def Isinr_def)
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    54
apply (simp add: Abs_Ssum_inject Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    55
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    56
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    57
text {* injectivity of @{term Isinl}, @{term Isinr} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    58
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    59
lemma inject_Isinl: "Isinl(a1)=Isinl(a2)==> a1=a2"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    60
by (simp add: Isinl_def Abs_Ssum_inject Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    61
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    62
lemma inject_Isinr: "Isinr(b1)=Isinr(b2) ==> b1=b2"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    63
by (simp add: Isinr_def Abs_Ssum_inject Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    64
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    65
declare inject_Isinl [dest!] inject_Isinr [dest!]
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    66
declare noteq_IsinlIsinr [dest!]
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    67
declare noteq_IsinlIsinr [OF sym, dest!]
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    68
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    69
lemma inject_Isinl_rev: "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    70
by blast
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    71
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    72
lemma inject_Isinr_rev: "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    73
by blast
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    74
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    75
text {* Exhaustion of the strict sum @{typ "'a ++ 'b"} *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    76
text {* choice of the bottom representation is arbitrary *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    77
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    78
lemma Exh_Ssum: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    79
        "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    80
apply (unfold Isinl_def Isinr_def)
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    81
apply (rule_tac x=z in Abs_Ssum_cases)
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    82
apply (auto simp add: Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    83
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    84
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    85
text {* elimination rules for the strict sum @{typ "'a ++ 'b"} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    86
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    87
lemma IssumE:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    88
        "[|p=Isinl(UU) ==> Q ; 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    89
        !!x.[|p=Isinl(x); x~=UU |] ==> Q; 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    90
        !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    91
by (rule Exh_Ssum [THEN disjE]) auto
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    92
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    93
lemma IssumE2:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    94
"[| !!x. [| p = Isinl(x) |] ==> Q;   !!y. [| p = Isinr(y) |] ==> Q |] ==>Q"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    95
by (rule_tac p=p in IssumE) auto
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    96
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    97
text {* rewrites for @{term Iwhen} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    98
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
    99
lemma Iwhen1: "Iwhen f g (Isinl UU) = UU"
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   100
apply (unfold Iwhen_def Isinl_def)
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   101
apply (simp add: Abs_Ssum_inverse Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   102
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   103
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   104
lemma Iwhen2: "x~=UU ==> Iwhen f g (Isinl x) = f$x"
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   105
apply (unfold Iwhen_def Isinl_def)
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   106
apply (simp add: Abs_Ssum_inverse Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   107
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   108
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   109
lemma Iwhen3: "y~=UU ==> Iwhen f g (Isinr y) = g$y"
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   110
apply (unfold Iwhen_def Isinr_def)
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   111
apply (simp add: Abs_Ssum_inverse Ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   112
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   113
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   114
text {* instantiate the simplifier *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   115
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   116
lemmas Ssum0_ss = strict_IsinlIsinr[symmetric] Iwhen1 Iwhen2 Iwhen3
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   117
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   118
declare Ssum0_ss [simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   119
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   120
subsection {* Ordering for type @{typ "'a ++ 'b"} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   121
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   122
instance "++"::(pcpo, pcpo) sq_ord ..
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   123
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   124
defs (overloaded)
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   125
  less_ssum_def: "(op <<) == (%s1 s2. Rep_Ssum s1 << Rep_Ssum s2)"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   126
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   127
lemma less_ssum1a: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   128
"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   129
by (simp add: Isinl_def less_ssum_def Abs_Ssum_inverse Ssum_def inst_cprod_po)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   130
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   131
lemma less_ssum1b: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   132
"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   133
by (simp add: Isinr_def less_ssum_def Abs_Ssum_inverse Ssum_def inst_cprod_po)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   134
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   135
lemma less_ssum1c: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   136
"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   137
by (simp add: Isinr_def Isinl_def less_ssum_def Abs_Ssum_inverse Ssum_def inst_cprod_po eq_UU_iff)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   138
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   139
lemma less_ssum1d: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   140
"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   141
by (simp add: Isinr_def Isinl_def less_ssum_def Abs_Ssum_inverse Ssum_def inst_cprod_po eq_UU_iff)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   142
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   143
text {* optimize lemmas about @{term less_ssum} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   144
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   145
lemma less_ssum2a: "(Isinl x) << (Isinl y) = (x << y)"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   146
by (simp only: less_ssum1a)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   147
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   148
lemma less_ssum2b: "(Isinr x) << (Isinr y) = (x << y)"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   149
by (simp only: less_ssum1b)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   150
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   151
lemma less_ssum2c: "(Isinl x) << (Isinr y) = (x = UU)"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   152
by (simp only: less_ssum1c)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   153
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   154
lemma less_ssum2d: "(Isinr x) << (Isinl y) = (x = UU)"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   155
by (simp only: less_ssum1d)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   156
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   157
subsection {* Type @{typ "'a ++ 'b"} is a partial order *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   158
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   159
lemma refl_less_ssum: "(p::'a++'b) << p"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   160
by (unfold less_ssum_def, rule refl_less)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   161
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   162
lemma antisym_less_ssum: "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   163
apply (unfold less_ssum_def)
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   164
apply (subst Rep_Ssum_inject [symmetric])
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   165
by (rule antisym_less)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   166
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   167
lemma trans_less_ssum: "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   168
by (unfold less_ssum_def, rule trans_less)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   169
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   170
instance "++" :: (pcpo, pcpo) po
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   171
by intro_classes
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   172
  (assumption | rule refl_less_ssum antisym_less_ssum trans_less_ssum)+
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   173
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   174
text {* for compatibility with old HOLCF-Version *}
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   175
lemmas inst_ssum_po = less_ssum_def [THEN meta_eq_to_obj_eq]
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   176
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   177
subsection {* Type @{typ "'a ++ 'b"} is pointed *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   178
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   179
lemma minimal_ssum: "Isinl UU << s"
15606
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   180
apply (simp add: less_ssum_def Isinl_def Abs_Ssum_inverse Ssum_def)
95617b30514b simplified some definitions, many proofs are much shorter
huffman
parents: 15600
diff changeset
   181
apply (simp add: inst_cprod_pcpo [symmetric])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   182
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   183
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   184
lemmas UU_ssum_def = minimal_ssum [THEN minimal2UU, symmetric, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   185
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   186
lemma least_ssum: "? x::'a++'b.!y. x<<y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   187
apply (rule_tac x = "Isinl UU" in exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   188
apply (rule minimal_ssum [THEN allI])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   189
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   190
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   191
subsection {* Monotonicity of @{term Isinl}, @{term Isinr}, @{term Iwhen} *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   192
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   193
text {* @{term Isinl} and @{term Isinr} are monotone *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   194
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   195
lemma monofun_Isinl: "monofun(Isinl)"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   196
by (simp add: monofun less_ssum2a)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   197
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   198
lemma monofun_Isinr: "monofun(Isinr)"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   199
by (simp add: monofun less_ssum2b)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   200
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   201
text {* @{term Iwhen} is monotone in all arguments *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   202
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   203
lemma monofun_Iwhen1: "monofun(Iwhen)"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   204
apply (rule monofunI [rule_format])
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   205
apply (rule less_fun [THEN iffD2, rule_format])
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   206
apply (rule less_fun [THEN iffD2, rule_format])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   207
apply (rule_tac p = "xb" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   208
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   209
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   210
apply (erule monofun_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   211
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   212
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   213
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   214
lemma monofun_Iwhen2: "monofun(Iwhen(f))"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   215
apply (rule monofunI [rule_format])
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   216
apply (rule less_fun [THEN iffD2, rule_format])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   217
apply (rule_tac p = "xa" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   218
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   219
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   220
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   221
apply (erule monofun_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   222
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   223
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   224
lemma monofun_Iwhen3: "monofun(Iwhen(f)(g))"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   225
apply (rule monofunI [rule_format])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   226
apply (rule_tac p = "x" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   227
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   228
apply (rule_tac p = "y" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   229
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   230
apply (rule_tac P = "xa=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   231
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   232
apply (rule UU_I)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   233
apply (rule less_ssum2a [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   234
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   235
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   236
apply (rule monofun_cfun_arg)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   237
apply (erule less_ssum2a [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   238
apply (simp del: Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   239
apply (rule_tac s = "UU" and t = "xa" in subst)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   240
apply (erule less_ssum2c [THEN iffD1, symmetric])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   241
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   242
apply (rule_tac p = "y" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   243
apply simp
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   244
apply (simp only: less_ssum2d)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   245
apply (simp only: less_ssum2d)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   246
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   247
apply (rule monofun_cfun_arg)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   248
apply (erule less_ssum2b [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   249
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   250
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   251
text {* some kind of exhaustion rules for chains in @{typ "'a ++ 'b"} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   252
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   253
lemma ssum_lemma1: "[|~(!i.? x. Y(i::nat)=Isinl(x))|] ==> (? i.! x. Y(i)~=Isinl(x))"
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   254
by fast
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   255
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   256
lemma ssum_lemma2: "[|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))|]   
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   257
      ==> (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   258
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   259
apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   260
apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   261
apply (erule notE, assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   262
apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   263
apply (erule notE, assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   264
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   265
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   266
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   267
lemma ssum_lemma3: "[|chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|]  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   268
      ==> (!i.? y. Y(i)=Isinr(y))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   269
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   270
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   271
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   272
apply (rule_tac p = "Y (ia) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   273
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   274
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   275
apply (rule_tac [2] strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   276
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   277
apply (erule_tac [2] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   278
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   279
apply (rule_tac m = "i" and n = "ia" in nat_less_cases)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   280
prefer 2 apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   281
apply (rule exI, rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   282
apply (erule_tac P = "x=UU" in notE)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   283
apply (rule less_ssum2d [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   284
apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   285
apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   286
apply (erule chain_mono)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   287
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   288
apply (erule_tac P = "xa=UU" in notE)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   289
apply (rule less_ssum2c [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   290
apply (erule_tac s = "Y (i) " and t = "Isinr (x) ::'a++'b" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   291
apply (erule_tac s = "Y (ia) " and t = "Isinl (xa) ::'a++'b" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   292
apply (erule chain_mono)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   293
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   294
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   295
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   296
lemma ssum_lemma4: "chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   297
apply (rule case_split_thm)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   298
apply (erule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   299
apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   300
apply (erule ssum_lemma3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   301
apply (rule ssum_lemma2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   302
apply (erule ssum_lemma1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   303
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   304
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   305
text {* restricted surjectivity of @{term Isinl} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   306
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   307
lemma ssum_lemma5: "z=Isinl(x)==> Isinl((Iwhen (LAM x. x) (LAM y. UU))(z)) = z"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   308
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   309
apply (case_tac "x=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   310
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   311
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   312
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   313
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   314
text {* restricted surjectivity of @{term Isinr} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   315
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   316
lemma ssum_lemma6: "z=Isinr(x)==> Isinr((Iwhen (LAM y. UU) (LAM x. x))(z)) = z"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   317
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   318
apply (case_tac "x=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   319
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   320
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   321
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   322
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   323
text {* technical lemmas *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   324
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   325
lemma ssum_lemma7: "[|Isinl(x) << z; x~=UU|] ==> ? y. z=Isinl(y) & y~=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   326
apply (rule_tac p = "z" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   327
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   328
apply (erule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   329
apply (rule antisym_less)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   330
apply (erule less_ssum2a [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   331
apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   332
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   333
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   334
apply (rule notE)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   335
apply (erule_tac [2] less_ssum2c [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   336
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   337
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   338
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   339
lemma ssum_lemma8: "[|Isinr(x) << z; x~=UU|] ==> ? y. z=Isinr(y) & y~=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   340
apply (rule_tac p = "z" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   341
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   342
apply (erule notE)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   343
apply (erule less_ssum2d [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   344
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   345
apply (rule notE)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   346
apply (erule_tac [2] less_ssum2d [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   347
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   348
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   349
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   350
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   351
subsection {* Type @{typ "'a ++ 'b"} is a cpo in three steps *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   352
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   353
lemma lub_ssum1a: "[|chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   354
      range(Y) <<| Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   355
apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   356
apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   357
apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   358
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   359
apply (rule_tac t = "Y (i) " in ssum_lemma5 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   360
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   361
apply (rule monofun_Isinl [THEN monofunE, THEN spec, THEN spec, THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   362
apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   363
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   364
apply (rule_tac p = "u" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   365
apply (rule_tac t = "u" in ssum_lemma5 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   366
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   367
apply (rule monofun_Isinl [THEN monofunE, THEN spec, THEN spec, THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   368
apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   369
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   370
apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   371
apply simp
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   372
apply (rule less_ssum2c [THEN iffD2])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   373
apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   374
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   375
apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   376
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   377
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   378
apply (erule notE)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   379
apply (rule less_ssum2c [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   380
apply (rule_tac t = "Isinl (x) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   381
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   382
apply (erule ub_rangeD)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   383
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   384
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   385
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   386
lemma lub_ssum1b: "[|chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   387
      range(Y) <<| Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   388
apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   389
apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   390
apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   391
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   392
apply (rule_tac t = "Y (i) " in ssum_lemma6 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   393
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   394
apply (rule monofun_Isinr [THEN monofunE, THEN spec, THEN spec, THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   395
apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   396
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   397
apply (rule_tac p = "u" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   398
apply simp
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   399
apply (rule less_ssum2d [THEN iffD2])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   400
apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   401
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   402
apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   403
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   404
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   405
apply (erule notE)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   406
apply (rule less_ssum2d [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   407
apply (rule_tac t = "Isinr (y) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   408
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   409
apply (erule ub_rangeD)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   410
apply (rule_tac t = "u" in ssum_lemma6 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   411
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   412
apply (rule monofun_Isinr [THEN monofunE, THEN spec, THEN spec, THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   413
apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   414
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   415
apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   416
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   417
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   418
lemmas thelub_ssum1a = lub_ssum1a [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   419
(*
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   420
[| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   421
 lub (range ?Y1) = Isinl
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   422
 (lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i))))
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   423
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   424
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   425
lemmas thelub_ssum1b = lub_ssum1b [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   426
(*
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   427
[| chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   428
 lub (range ?Y1) = Isinr
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   429
 (lub (range (%i. Iwhen (LAM y. UU) (LAM x. x) (?Y1 i))))
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   430
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   431
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   432
lemma cpo_ssum: "chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   433
apply (rule ssum_lemma4 [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   434
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   435
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   436
apply (erule lub_ssum1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   437
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   438
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   439
apply (erule lub_ssum1b)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   440
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   441
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   442
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   443
instance "++" :: (pcpo, pcpo) cpo
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   444
by intro_classes (rule cpo_ssum)
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   445
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   446
instance "++" :: (pcpo, pcpo) pcpo
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   447
by intro_classes (rule least_ssum)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   448
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   449
text {* for compatibility with old HOLCF-Version *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   450
lemma inst_ssum_pcpo: "UU = Isinl UU"
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   451
apply (simp add: UU_def UU_ssum_def)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   452
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   453
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   454
declare inst_ssum_pcpo [symmetric, simp]
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   455
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   456
subsection {* Continuous versions of constants *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   457
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   458
consts  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   459
        sinl    :: "'a -> ('a++'b)" 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   460
        sinr    :: "'b -> ('a++'b)" 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   461
        sscase  :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   462
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   463
defs
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   464
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   465
sinl_def:        "sinl   == (LAM x. Isinl(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   466
sinr_def:        "sinr   == (LAM x. Isinr(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   467
sscase_def:      "sscase   == (LAM f g s. Iwhen(f)(g)(s))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   468
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   469
translations
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   470
"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   471
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   472
text {* continuity for @{term Isinl} and @{term Isinr} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   473
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   474
lemma contlub_Isinl: "contlub(Isinl)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   475
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   476
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   477
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   478
apply (rule_tac [2] thelub_ssum1a [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   479
apply (rule_tac [3] allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   480
apply (rule_tac [3] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   481
apply (rule_tac [3] refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   482
apply (erule_tac [2] monofun_Isinl [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   483
apply (case_tac "lub (range (Y))=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   484
apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   485
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   486
apply (rule_tac f = "Isinl" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   487
apply (rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   488
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   489
apply (rule_tac s = "UU" and t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   490
apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   491
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   492
apply (rule Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   493
apply (rule_tac f = "Isinl" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   494
apply (rule lub_equal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   495
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   496
apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   497
apply (erule monofun_Isinl [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   498
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   499
apply (case_tac "Y (k) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   500
apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   501
apply (rule Iwhen1[symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   502
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   503
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   504
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   505
lemma contlub_Isinr: "contlub(Isinr)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   506
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   507
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   508
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   509
apply (rule_tac [2] thelub_ssum1b [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   510
apply (rule_tac [3] allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   511
apply (rule_tac [3] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   512
apply (rule_tac [3] refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   513
apply (erule_tac [2] monofun_Isinr [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   514
apply (case_tac "lub (range (Y))=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   515
apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   516
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   517
apply (rule arg_cong, rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   518
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   519
apply (rule_tac s = "UU" and t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   520
apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   521
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   522
apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   523
apply (rule Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   524
apply (rule arg_cong, rule lub_equal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   525
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   526
apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   527
apply (erule monofun_Isinr [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   528
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   529
apply (case_tac "Y (k) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   530
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   531
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   532
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   533
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   534
lemma cont_Isinl [iff]: "cont(Isinl)"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   535
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   536
apply (rule monofun_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   537
apply (rule contlub_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   538
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   539
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   540
lemma cont_Isinr [iff]: "cont(Isinr)"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   541
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   542
apply (rule monofun_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   543
apply (rule contlub_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   544
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   545
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   546
text {* continuity for @{term Iwhen} in the first two arguments *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   547
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   548
lemma contlub_Iwhen1: "contlub(Iwhen)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   549
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   550
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   551
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   552
apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   553
apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   554
apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   555
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   556
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   557
apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   558
apply (rule_tac [2] ch2ch_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   559
apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   560
apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   561
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   562
apply (rule_tac p = "xa" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   563
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   564
apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   565
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   566
apply (erule contlub_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   567
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   568
apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   569
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   570
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   571
lemma contlub_Iwhen2: "contlub(Iwhen(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   572
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   573
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   574
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   575
apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   576
apply (erule_tac [2] monofun_Iwhen2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   577
apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   578
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   579
apply (rule_tac p = "x" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   580
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   581
apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   582
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   583
apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   584
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   585
apply (erule contlub_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   586
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   587
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   588
text {* continuity for @{term Iwhen} in its third argument *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   589
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   590
text {* first 5 ugly lemmas *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   591
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   592
lemma ssum_lemma9: "[| chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   593
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   594
apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   595
apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   596
apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   597
apply (rule_tac P = "y=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   598
apply assumption
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   599
apply (rule less_ssum2d [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   600
apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   601
apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   602
apply (erule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   603
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   604
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   605
lemma ssum_lemma10: "[| chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   606
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   607
apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   608
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   609
apply (erule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   610
apply (rule strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   611
apply (erule_tac [2] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   612
apply (rule_tac P = "xa=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   613
apply assumption
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   614
apply (rule less_ssum2c [THEN iffD1])
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   615
apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   616
apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   617
apply (erule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   618
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   619
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   620
lemma ssum_lemma11: "[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   621
    Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   622
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   623
apply (rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   624
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   625
apply (rule_tac s = "Isinl (UU) " and t = "Y (i) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   626
apply (rule inst_ssum_pcpo [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   627
apply (rule chain_UU_I [THEN spec, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   628
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   629
apply (erule inst_ssum_pcpo [THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   630
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   631
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   632
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   633
lemma ssum_lemma12: "[| chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   634
    Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   635
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   636
apply (rule_tac t = "x" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   637
apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   638
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   639
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   640
apply (rule thelub_ssum1a [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   641
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   642
apply (erule ssum_lemma9)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   643
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   644
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   645
apply (rule contlub_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   646
apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   647
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   648
apply (rule lub_equal2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   649
apply (rule chain_mono2 [THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   650
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   651
apply (rule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   652
apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   653
apply (erule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   654
apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   655
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   656
apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   657
apply (erule notnotD)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   658
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   659
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   660
apply (rule ssum_lemma9 [THEN spec, THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   661
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   662
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   663
apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   664
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   665
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   666
apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   667
apply (rule Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   668
apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   669
apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   670
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   671
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   672
apply (subst Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   673
apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   674
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   675
apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   676
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   677
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   678
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   679
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   680
lemma ssum_lemma13: "[| chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   681
    Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   682
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   683
apply (rule_tac t = "x" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   684
apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   685
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   686
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   687
apply (rule thelub_ssum1b [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   688
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   689
apply (erule ssum_lemma10)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   690
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   691
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   692
apply (rule contlub_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   693
apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   694
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   695
apply (rule lub_equal2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   696
apply (rule chain_mono2 [THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   697
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   698
apply (rule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   699
apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   700
apply (erule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   701
apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   702
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   703
apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   704
apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   705
apply (erule notnotD)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   706
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   707
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   708
apply (rule ssum_lemma10 [THEN spec, THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   709
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   710
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   711
apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   712
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   713
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   714
apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   715
apply (rule Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   716
apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   717
apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   718
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   719
apply (subst Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   720
apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   721
apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   722
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   723
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   724
apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   725
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   726
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   727
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   728
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   729
lemma contlub_Iwhen3: "contlub(Iwhen(f)(g))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   730
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   731
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   732
apply (rule_tac p = "lub (range (Y))" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   733
apply (erule ssum_lemma11)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   734
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   735
apply (erule ssum_lemma12)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   736
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   737
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   738
apply (erule ssum_lemma13)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   739
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   740
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   741
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   742
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   743
lemma cont_Iwhen1: "cont(Iwhen)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   744
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   745
apply (rule monofun_Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   746
apply (rule contlub_Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   747
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   748
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   749
lemma cont_Iwhen2: "cont(Iwhen(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   750
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   751
apply (rule monofun_Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   752
apply (rule contlub_Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   753
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   754
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   755
lemma cont_Iwhen3: "cont(Iwhen(f)(g))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   756
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   757
apply (rule monofun_Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   758
apply (rule contlub_Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   759
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   760
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   761
text {* continuous versions of lemmas for @{typ "'a ++ 'b"} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   762
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   763
lemma strict_sinl [simp]: "sinl$UU =UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   764
apply (unfold sinl_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   765
apply (simp add: cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   766
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   767
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   768
lemma strict_sinr [simp]: "sinr$UU=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   769
apply (unfold sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   770
apply (simp add: cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   771
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   772
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   773
lemma noteq_sinlsinr: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   774
        "sinl$a=sinr$b ==> a=UU & b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   775
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   776
apply (auto dest!: noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   777
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   778
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   779
lemma inject_sinl: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   780
        "sinl$a1=sinl$a2==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   781
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   782
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   783
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   784
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   785
lemma inject_sinr: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   786
        "sinr$a1=sinr$a2==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   787
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   788
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   789
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   790
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   791
declare inject_sinl [dest!] inject_sinr [dest!]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   792
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   793
lemma defined_sinl [simp]: "x~=UU ==> sinl$x ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   794
apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   795
apply (rule inject_sinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   796
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   797
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   798
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   799
lemma defined_sinr [simp]: "x~=UU ==> sinr$x ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   800
apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   801
apply (rule inject_sinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   802
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   803
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   804
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   805
lemma Exh_Ssum1: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   806
        "z=UU | (? a. z=sinl$a & a~=UU) | (? b. z=sinr$b & b~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   807
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   808
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   809
apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   810
apply (rule Exh_Ssum)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   811
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   812
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   813
lemma ssumE:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   814
assumes major: "p=UU ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   815
assumes prem2: "!!x.[|p=sinl$x; x~=UU |] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   816
assumes prem3: "!!y.[|p=sinr$y; y~=UU |] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   817
shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   818
apply (rule major [THEN IssumE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   819
apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   820
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   821
apply (rule prem2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   822
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   823
apply (simp add: sinl_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   824
apply (rule prem3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   825
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   826
apply (simp add: sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   827
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   828
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   829
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   830
lemma ssumE2:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   831
assumes preml: "!!x.[|p=sinl$x|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   832
assumes premr: "!!y.[|p=sinr$y|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   833
shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   834
apply (rule IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   835
apply (rule preml)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   836
apply (rule_tac [2] premr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   837
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   838
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   839
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   840
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   841
lemmas ssum_conts = cont_lemmas1 cont_Iwhen1 cont_Iwhen2
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   842
                cont_Iwhen3 cont2cont_CF1L
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   843
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   844
lemma sscase1 [simp]: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   845
        "sscase$f$g$UU = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   846
apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   847
apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   848
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   849
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   850
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   851
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   852
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   853
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   854
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   855
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   856
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   857
lemma sscase2 [simp]: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   858
        "x~=UU==> sscase$f$g$(sinl$x) = f$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   859
apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   860
apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   861
apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   862
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   863
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   864
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   865
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   866
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   867
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   868
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   869
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   870
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   871
lemma sscase3 [simp]: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   872
        "x~=UU==> sscase$f$g$(sinr$x) = g$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   873
apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   874
apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   875
apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   876
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   877
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   878
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   879
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   880
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   881
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   882
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   883
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   884
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   885
lemma less_ssum4a: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   886
        "(sinl$x << sinl$y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   887
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   888
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   889
apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   890
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   891
apply (rule cont_Isinl)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   892
apply (rule less_ssum2a)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   893
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   894
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   895
lemma less_ssum4b: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   896
        "(sinr$x << sinr$y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   897
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   898
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   899
apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   900
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   901
apply (rule cont_Isinr)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   902
apply (rule less_ssum2b)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   903
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   904
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   905
lemma less_ssum4c: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   906
        "(sinl$x << sinr$y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   907
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   908
apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   909
apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   910
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   911
apply (rule cont_Isinl)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   912
apply (rule less_ssum2c)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   913
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   914
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   915
lemma less_ssum4d: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   916
        "(sinr$x << sinl$y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   917
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   918
apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   919
apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   920
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   921
apply (rule cont_Isinr)
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
   922
apply (rule less_ssum2d)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   923
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   924
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   925
lemma ssum_chainE: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   926
        "chain(Y) ==> (!i.? x.(Y i)=sinl$x)|(!i.? y.(Y i)=sinr$y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   927
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   928
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   929
apply (erule ssum_lemma4)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   930
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   931
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   932
lemma thelub_ssum2a: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   933
"[| chain(Y); !i.? x. Y(i) = sinl$x |] ==>  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   934
    lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   935
apply (unfold sinl_def sinr_def sscase_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   936
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   937
apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   938
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   939
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   940
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   941
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   942
apply (subst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   943
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   944
apply (rule thelub_ssum1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   945
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   946
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   947
apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   948
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   949
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   950
apply (erule box_equals)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   951
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   952
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   953
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   954
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   955
lemma thelub_ssum2b: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   956
"[| chain(Y); !i.? x. Y(i) = sinr$x |] ==>  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   957
    lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   958
apply (unfold sinl_def sinr_def sscase_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   959
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   960
apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   961
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   962
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   963
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   964
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   965
apply (subst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   966
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   967
apply (rule thelub_ssum1b)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   968
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   969
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   970
apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   971
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   972
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   973
apply (erule box_equals)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   974
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   975
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   976
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   977
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   978
lemma thelub_ssum2a_rev: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   979
        "[| chain(Y); lub(range(Y)) = sinl$x|] ==> !i.? x. Y(i)=sinl$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   980
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   981
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   982
apply (erule ssum_lemma9)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   983
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   984
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   985
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   986
lemma thelub_ssum2b_rev: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   987
     "[| chain(Y); lub(range(Y)) = sinr$x|] ==> !i.? x. Y(i)=sinr$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   988
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   989
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   990
apply (erule ssum_lemma10)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   991
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   992
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   993
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   994
lemma thelub_ssum3: "chain(Y) ==>  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   995
    lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i)))) 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   996
  | lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   997
apply (rule ssum_chainE [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   998
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   999
apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1000
apply (erule thelub_ssum2a)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1001
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1002
apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1003
apply (erule thelub_ssum2b)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1004
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1005
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1006
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1007
lemma sscase4: "sscase$sinl$sinr$z=z"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1008
apply (rule_tac p = "z" in ssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1009
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1010
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1011
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
  1012
text {* install simplifier for Ssum *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1013
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1014
lemmas Ssum_rews = strict_sinl strict_sinr defined_sinl defined_sinr
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1015
                sscase1 sscase2 sscase3
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1016
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
  1017
text {* for backward compatibility *}
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
  1018
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
  1019
lemmas less_ssum3a = less_ssum2a
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
  1020
lemmas less_ssum3b = less_ssum2b
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
  1021
lemmas less_ssum3c = less_ssum2c
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
  1022
lemmas less_ssum3d = less_ssum2d
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
  1023
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1024
end