src/HOLCF/Ssum.thy
author huffman
Fri, 04 Mar 2005 23:12:36 +0100
changeset 15576 efb95d0d01f7
child 15577 e16da3068ad6
permissions -rw-r--r--
converted to new-style theories, and combined numbered files
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/Ssum0.thy
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
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    11
theory Ssum = Cfun:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    12
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    13
constdefs
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    14
  Sinl_Rep      :: "['a,'a,'b,bool]=>bool"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    15
 "Sinl_Rep == (%a.%x y p. (a~=UU --> x=a & p))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    16
  Sinr_Rep      :: "['b,'a,'b,bool]=>bool"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    17
 "Sinr_Rep == (%b.%x y p.(b~=UU --> y=b & ~p))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    18
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    19
typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    20
	"{f.(? a. f=Sinl_Rep(a::'a))|(? b. f=Sinr_Rep(b::'b))}"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    21
by auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    22
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    23
syntax (xsymbols)
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
syntax (HTML output)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    26
  "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    27
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    28
consts
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    29
  Isinl         :: "'a => ('a ++ 'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    30
  Isinr         :: "'b => ('a ++ 'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    31
  Iwhen         :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    32
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    33
defs   (*defining the abstract constants*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    34
  Isinl_def:     "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    35
  Isinr_def:     "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    36
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    37
  Iwhen_def:     "Iwhen(f)(g)(s) == @z.
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    38
                                    (s=Isinl(UU) --> z=UU)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    39
                        &(!a. a~=UU & s=Isinl(a) --> z=f$a)  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    40
                        &(!b. b~=UU & s=Isinr(b) --> z=g$b)"  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    41
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    42
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    43
(* A non-emptyness result for Sssum                                         *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    44
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    45
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    46
lemma SsumIl: "Sinl_Rep(a):Ssum"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    47
apply (unfold Ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    48
apply blast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    49
done
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 SsumIr: "Sinr_Rep(a):Ssum"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    52
apply (unfold Ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    53
apply blast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    54
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    55
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    56
lemma inj_on_Abs_Ssum: "inj_on Abs_Ssum Ssum"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    57
apply (rule inj_on_inverseI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    58
apply (erule Abs_Ssum_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    59
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    60
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
(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr                        *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    63
(* ------------------------------------------------------------------------ *)
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
lemma strict_SinlSinr_Rep: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    66
 "Sinl_Rep(UU) = Sinr_Rep(UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    67
apply (unfold Sinr_Rep_def Sinl_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    68
apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    69
apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    70
apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    71
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    72
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    73
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    74
lemma strict_IsinlIsinr: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    75
 "Isinl(UU) = Isinr(UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    76
apply (unfold Isinl_def Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    77
apply (rule strict_SinlSinr_Rep [THEN arg_cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    78
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    79
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    80
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    81
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    82
(* distinctness of  Sinl_Rep, Sinr_Rep and Isinl, Isinr                     *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    83
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    84
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    85
lemma noteq_SinlSinr_Rep: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    86
        "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    87
apply (unfold Sinl_Rep_def Sinr_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    88
apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    89
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    90
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    91
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    92
lemma noteq_IsinlIsinr: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    93
        "Isinl(a)=Isinr(b) ==> a=UU & b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    94
apply (unfold Isinl_def Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    95
apply (rule noteq_SinlSinr_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    96
apply (erule inj_on_Abs_Ssum [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    97
apply (rule SsumIl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    98
apply (rule SsumIr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    99
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   100
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   101
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   102
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   103
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   104
(* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr                       *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   105
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   106
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   107
lemma inject_Sinl_Rep1: "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   108
apply (unfold Sinl_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   109
apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   110
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   111
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   112
lemma inject_Sinr_Rep1: "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   113
apply (unfold Sinr_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   114
apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   115
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   116
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   117
lemma inject_Sinl_Rep2: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   118
"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   119
apply (unfold Sinl_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   120
apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   121
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   122
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   123
lemma inject_Sinr_Rep2: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   124
"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   125
apply (unfold Sinr_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   126
apply (blast dest!: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   127
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   128
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   129
lemma inject_Sinl_Rep: "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   130
apply (case_tac "a1=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   131
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   132
apply (rule inject_Sinl_Rep1 [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   133
apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   134
apply (case_tac "a2=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   135
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   136
apply (drule inject_Sinl_Rep1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   137
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   138
apply (erule inject_Sinl_Rep2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   139
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   140
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   141
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   142
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   143
lemma inject_Sinr_Rep: "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   144
apply (case_tac "b1=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   145
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   146
apply (rule inject_Sinr_Rep1 [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   147
apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   148
apply (case_tac "b2=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   149
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   150
apply (drule inject_Sinr_Rep1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   151
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   152
apply (erule inject_Sinr_Rep2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   153
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   154
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   155
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   156
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   157
lemma inject_Isinl: "Isinl(a1)=Isinl(a2)==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   158
apply (unfold Isinl_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   159
apply (rule inject_Sinl_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   160
apply (erule inj_on_Abs_Ssum [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   161
apply (rule SsumIl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   162
apply (rule SsumIl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   163
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   164
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   165
lemma inject_Isinr: "Isinr(b1)=Isinr(b2) ==> b1=b2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   166
apply (unfold Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   167
apply (rule inject_Sinr_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   168
apply (erule inj_on_Abs_Ssum [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   169
apply (rule SsumIr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   170
apply (rule SsumIr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   171
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   172
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   173
declare inject_Isinl [dest!] inject_Isinr [dest!]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   174
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   175
lemma inject_Isinl_rev: "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   176
apply blast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   177
done
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 inject_Isinr_rev: "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   180
apply blast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   181
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   182
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
(* Exhaustion of the strict sum ++                                          *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   185
(* choice of the bottom representation is arbitrary                         *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   186
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   187
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   188
lemma Exh_Ssum: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   189
        "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
   190
apply (unfold Isinl_def Isinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   191
apply (rule Rep_Ssum[unfolded Ssum_def, THEN CollectE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   192
apply (erule disjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   193
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   194
apply (case_tac "z= Abs_Ssum (Sinl_Rep (UU))")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   195
apply (erule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   196
apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   197
apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   198
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   199
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   200
apply (rule Rep_Ssum_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   201
apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   202
apply (rule_tac Q = "Sinl_Rep (a) =Sinl_Rep (UU) " in contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   203
apply (erule_tac [2] arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   204
apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   205
apply (rule Rep_Ssum_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   206
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   207
apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   208
apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   209
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   210
apply (case_tac "z= Abs_Ssum (Sinl_Rep (UU))")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   211
apply (erule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   212
apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   213
apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   214
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   215
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   216
apply (rule Rep_Ssum_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   217
apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   218
apply (rule_tac Q = "Sinr_Rep (b) =Sinl_Rep (UU) " in contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   219
prefer 2 apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   220
apply (rule strict_SinlSinr_Rep [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   221
apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   222
apply (rule Rep_Ssum_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   223
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   224
apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   225
apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   226
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   227
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   228
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   229
(* elimination rules for the strict sum ++                                  *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   230
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   231
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   232
lemma IssumE:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   233
        "[|p=Isinl(UU) ==> Q ; 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   234
        !!x.[|p=Isinl(x); x~=UU |] ==> Q; 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   235
        !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   236
apply (rule Exh_Ssum [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   237
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   238
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   239
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   240
lemma IssumE2:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   241
"[| !!x. [| p = Isinl(x) |] ==> Q;   !!y. [| p = Isinr(y) |] ==> Q |] ==>Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   242
apply (rule IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   243
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   244
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   245
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   246
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   247
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   248
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   249
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   250
(* rewrites for Iwhen                                                       *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   251
(* ------------------------------------------------------------------------ *)
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 Iwhen1: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   254
        "Iwhen f g (Isinl UU) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   255
apply (unfold Iwhen_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   256
apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   257
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   258
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   259
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   260
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   261
apply (rule_tac P = "a=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   262
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   263
apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   264
apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   265
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   266
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   267
apply (rule_tac P = "b=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   268
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   269
apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   270
apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   271
apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   272
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   273
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   274
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   275
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   276
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   277
lemma Iwhen2: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   278
        "x~=UU ==> Iwhen f g (Isinl x) = f$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   279
apply (unfold Iwhen_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   280
apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   281
prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   282
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   283
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   284
apply (rule_tac P = "x=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   285
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   286
apply (rule inject_Isinl)
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 (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   289
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   290
apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   291
apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   292
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   293
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   294
apply (rule_tac P = "Isinl (x) = Isinr (b) " in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   295
prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   296
apply (rule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   297
apply (erule_tac [2] noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   298
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   299
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   300
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   301
lemma Iwhen3: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   302
        "y~=UU ==> Iwhen f g (Isinr y) = g$y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   303
apply (unfold Iwhen_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   304
apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   305
prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   306
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   307
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   308
apply (rule_tac P = "y=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   309
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   310
apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   311
apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   312
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   313
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   314
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   315
apply (rule_tac P = "Isinr (y) = Isinl (a) " in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   316
prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   317
apply (rule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   318
apply (erule_tac [2] sym [THEN noteq_IsinlIsinr])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   319
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   320
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   321
apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   322
apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   323
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   324
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   325
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   326
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   327
(* instantiate the simplifier                                               *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   328
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   329
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   330
lemmas Ssum0_ss = strict_IsinlIsinr[symmetric] Iwhen1 Iwhen2 Iwhen3
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   331
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   332
declare Ssum0_ss [simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   333
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   334
(* Partial ordering for the strict sum ++ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   335
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   336
instance "++"::(pcpo,pcpo)sq_ord ..
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   337
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   338
defs (overloaded)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   339
  less_ssum_def: "(op <<) == (%s1 s2.@z.
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   340
         (! u x. s1=Isinl u & s2=Isinl x --> z = u << x)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   341
        &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   342
        &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU))
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   343
        &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   344
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   345
lemma less_ssum1a: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   346
"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   347
apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   348
apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   349
apply (drule_tac [2] conjunct1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   350
apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   351
apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   352
apply (erule_tac [2] mp)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   353
prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   354
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   355
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   356
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   357
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   358
apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   359
apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   360
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   361
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   362
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   363
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   364
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   365
apply (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   366
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   367
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   368
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   369
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   370
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   371
apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   372
apply (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   373
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   374
apply (rule eq_UU_iff[symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   375
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   376
apply (erule conjE)
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 (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   379
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   380
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   381
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   382
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   383
lemma less_ssum1b: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   384
"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   385
apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   386
apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   387
apply (drule_tac [2] conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   388
apply (drule_tac [2] conjunct1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   389
apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   390
apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   391
apply (erule_tac [2] mp)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   392
prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   393
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   394
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   395
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   396
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   397
apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   398
apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   399
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   400
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   401
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   402
apply (erule conjE)
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 (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   405
apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   406
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   407
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   408
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   409
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   410
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   411
apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   412
apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   413
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   414
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   415
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   416
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   417
apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   418
apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   419
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   420
apply (rule eq_UU_iff[symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   421
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   422
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
lemma less_ssum1c: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   425
"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   426
apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   427
apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   428
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   429
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   430
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   431
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   432
apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   433
apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   434
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   435
apply (rule eq_UU_iff)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   436
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   437
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   438
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   439
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   440
apply (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   441
apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   442
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   443
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   444
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   445
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   446
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   447
apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   448
apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   449
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   450
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   451
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   452
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   453
apply (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   454
apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   455
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   456
apply (drule conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   457
apply (drule conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   458
apply (drule conjunct1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   459
apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   460
apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   461
apply (erule mp)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   462
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   463
done
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
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   466
lemma less_ssum1d: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   467
"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   468
apply (unfold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   469
apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   470
apply (drule_tac [2] conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   471
apply (drule_tac [2] conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   472
apply (drule_tac [2] conjunct2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   473
apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   474
apply (drule_tac [2] spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   475
apply (erule_tac [2] mp)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   476
prefer 2 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   477
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   478
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   479
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   480
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   481
apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   482
apply (drule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   483
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   484
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   485
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   486
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   487
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   488
apply (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   489
apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   490
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   491
apply (rule eq_UU_iff)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   492
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   493
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   494
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   495
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   496
apply (drule noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   497
apply (drule noteq_IsinlIsinr[OF sym])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   498
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   499
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   500
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   501
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   502
apply (drule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   503
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   504
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   505
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   506
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   507
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   508
(* optimize lemmas about less_ssum                                          *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   509
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   510
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   511
lemma less_ssum2a: "(Isinl x) << (Isinl y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   512
apply (rule less_ssum1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   513
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   514
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   515
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   516
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   517
lemma less_ssum2b: "(Isinr x) << (Isinr y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   518
apply (rule less_ssum1b)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   519
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   520
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   521
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   522
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   523
lemma less_ssum2c: "(Isinl x) << (Isinr y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   524
apply (rule less_ssum1c)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   525
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   526
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   527
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   528
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   529
lemma less_ssum2d: "(Isinr x) << (Isinl y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   530
apply (rule less_ssum1d)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   531
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   532
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   533
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   534
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   535
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   536
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   537
(* less_ssum is a partial order on ++                                     *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   538
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   539
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   540
lemma refl_less_ssum: "(p::'a++'b) << p"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   541
apply (rule_tac p = "p" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   542
apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   543
apply (rule less_ssum2a [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   544
apply (rule refl_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   545
apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   546
apply (rule less_ssum2b [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   547
apply (rule refl_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   548
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   549
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   550
lemma antisym_less_ssum: "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   551
apply (rule_tac p = "p1" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   552
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   553
apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   554
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   555
apply (rule_tac f = "Isinl" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   556
apply (rule antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   557
apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   558
apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   559
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   560
apply (erule less_ssum2d [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   561
apply (erule less_ssum2c [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   562
apply (rule strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   563
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   564
apply (rule_tac p = "p2" in IssumE2)
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 less_ssum2c [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   567
apply (erule less_ssum2d [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   568
apply (rule strict_IsinlIsinr [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   569
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   570
apply (rule_tac f = "Isinr" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   571
apply (rule antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   572
apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   573
apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   574
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   575
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   576
lemma trans_less_ssum: "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   577
apply (rule_tac p = "p1" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   578
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   579
apply (rule_tac p = "p3" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   580
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   581
apply (rule less_ssum2a [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   582
apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   583
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   584
apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   585
apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   586
apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   587
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   588
apply (erule less_ssum2c [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   589
apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   590
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   591
apply (rule less_ssum2c [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   592
apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   593
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   594
apply (rule UU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   595
apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   596
apply (erule less_ssum2a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   597
apply (rule antisym_less_inverse [THEN conjunct1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   598
apply (erule less_ssum2c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   599
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   600
apply (erule less_ssum2c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   601
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   602
apply (rule_tac p = "p3" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   603
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   604
apply (rule less_ssum2d [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   605
apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   606
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   607
apply (erule less_ssum2d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   608
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   609
apply (rule UU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   610
apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   611
apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   612
apply (rule antisym_less_inverse [THEN conjunct1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   613
apply (erule less_ssum2d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   614
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   615
apply (rule less_ssum2b [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   616
apply (rule_tac p = "p2" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   617
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   618
apply (erule less_ssum2d [THEN iffD1, THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   619
apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   620
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   621
apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   622
apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   623
apply (erule less_ssum2b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   624
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   625
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   626
(* Class Instance ++::(pcpo,pcpo)po *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   627
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   628
instance "++"::(pcpo,pcpo)po
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   629
apply (intro_classes)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   630
apply (rule refl_less_ssum)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   631
apply (rule antisym_less_ssum, assumption+)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   632
apply (rule trans_less_ssum, assumption+)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   633
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   634
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   635
(* for compatibility with old HOLCF-Version *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   636
lemma inst_ssum_po: "(op <<)=(%s1 s2.@z.
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   637
         (! u x. s1=Isinl u & s2=Isinl x --> z = u << x)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   638
        &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   639
        &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU))
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   640
        &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   641
apply (fold less_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   642
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   643
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   644
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   645
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   646
(* access to less_ssum in class po                                          *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   647
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   648
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   649
lemma less_ssum3a: "Isinl x << Isinl y = x << y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   650
apply (simp (no_asm) add: less_ssum2a)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   651
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   652
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   653
lemma less_ssum3b: "Isinr x << Isinr y = x << y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   654
apply (simp (no_asm) add: less_ssum2b)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   655
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   656
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   657
lemma less_ssum3c: "Isinl x << Isinr y = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   658
apply (simp (no_asm) add: less_ssum2c)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   659
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   660
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   661
lemma less_ssum3d: "Isinr x << Isinl y = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   662
apply (simp (no_asm) add: less_ssum2d)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   663
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   664
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   665
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   666
(* type ssum ++ is pointed                                                  *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   667
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   668
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   669
lemma minimal_ssum: "Isinl UU << s"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   670
apply (rule_tac p = "s" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   671
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   672
apply (rule less_ssum3a [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   673
apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   674
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   675
apply (subst strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   676
apply (rule less_ssum3b [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   677
apply (rule minimal)
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
lemmas UU_ssum_def = minimal_ssum [THEN minimal2UU, symmetric, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   681
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   682
lemma least_ssum: "? x::'a++'b.!y. x<<y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   683
apply (rule_tac x = "Isinl UU" in exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   684
apply (rule minimal_ssum [THEN allI])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   685
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   686
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   687
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   688
(* Isinl, Isinr are monotone                                                *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   689
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   690
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   691
lemma monofun_Isinl: "monofun(Isinl)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   692
apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   693
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   694
apply (erule less_ssum3a [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   695
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   696
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   697
lemma monofun_Isinr: "monofun(Isinr)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   698
apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   699
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   700
apply (erule less_ssum3b [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   701
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   702
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   703
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   704
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   705
(* Iwhen is monotone in all arguments                                       *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   706
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   707
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   708
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   709
lemma monofun_Iwhen1: "monofun(Iwhen)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   710
apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   711
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   712
apply (rule less_fun [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   713
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   714
apply (rule less_fun [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   715
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   716
apply (rule_tac p = "xb" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   717
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   718
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   719
apply (erule monofun_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   720
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   721
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   722
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   723
lemma monofun_Iwhen2: "monofun(Iwhen(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   724
apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   725
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   726
apply (rule less_fun [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   727
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   728
apply (rule_tac p = "xa" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   729
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   730
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   731
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   732
apply (erule monofun_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   733
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   734
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   735
lemma monofun_Iwhen3: "monofun(Iwhen(f)(g))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   736
apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   737
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   738
apply (rule_tac p = "x" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   739
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   740
apply (rule_tac p = "y" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   741
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   742
apply (rule_tac P = "xa=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   743
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   744
apply (rule UU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   745
apply (rule less_ssum3a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   746
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   747
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   748
apply (rule monofun_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   749
apply (erule less_ssum3a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   750
apply (simp del: Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   751
apply (rule_tac s = "UU" and t = "xa" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   752
apply (erule less_ssum3c [THEN iffD1, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   753
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   754
apply (rule_tac p = "y" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   755
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   756
apply (simp only: less_ssum3d)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   757
apply (simp only: less_ssum3d)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   758
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   759
apply (rule monofun_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   760
apply (erule less_ssum3b [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   761
done
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
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   764
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   765
(* some kind of exhaustion rules for chains in 'a ++ 'b                     *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   766
(* ------------------------------------------------------------------------ *)
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 ssum_lemma1: "[|~(!i.? x. Y(i::nat)=Isinl(x))|] ==> (? i.! x. Y(i)~=Isinl(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   769
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   770
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   771
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   772
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
   773
      ==> (? 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
   774
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   775
apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   776
apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   777
apply (erule notE, assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   778
apply (drule spec)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   779
apply (erule notE, assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   780
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   781
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   782
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   783
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   784
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
   785
      ==> (!i.? y. Y(i)=Isinr(y))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   786
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   787
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   788
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   789
apply (rule_tac p = "Y (ia) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   790
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   791
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   792
apply (rule_tac [2] strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   793
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   794
apply (erule_tac [2] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   795
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   796
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
   797
prefer 2 apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   798
apply (rule exI, rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   799
apply (erule_tac P = "x=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   800
apply (rule less_ssum3d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   801
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
   802
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
   803
apply (erule chain_mono)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   804
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   805
apply (erule_tac P = "xa=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   806
apply (rule less_ssum3c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   807
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
   808
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
   809
apply (erule chain_mono)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   810
apply assumption
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 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
   814
apply (rule case_split_thm)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   815
apply (erule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   816
apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   817
apply (erule ssum_lemma3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   818
apply (rule ssum_lemma2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   819
apply (erule ssum_lemma1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   820
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   821
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   822
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   823
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   824
(* restricted surjectivity of Isinl                                         *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   825
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   826
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   827
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
   828
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   829
apply (case_tac "x=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   830
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   831
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   832
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   833
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   834
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   835
(* restricted surjectivity of Isinr                                         *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   836
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   837
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   838
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
   839
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   840
apply (case_tac "x=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   841
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   842
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   843
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   844
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   845
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   846
(* technical lemmas                                                         *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   847
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   848
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   849
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
   850
apply (rule_tac p = "z" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   851
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   852
apply (erule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   853
apply (rule antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   854
apply (erule less_ssum3a [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   855
apply (rule minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   856
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   857
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   858
apply (rule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   859
apply (erule_tac [2] less_ssum3c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   860
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   861
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   862
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   863
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
   864
apply (rule_tac p = "z" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   865
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   866
apply (erule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   867
apply (erule less_ssum3d [THEN iffD1])
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
apply (rule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   870
apply (erule_tac [2] less_ssum3d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   871
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   872
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   873
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   874
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   875
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   876
(* the type 'a ++ 'b is a cpo in three steps                                *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   877
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   878
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   879
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
   880
      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
   881
apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   882
apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   883
apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   884
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   885
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
   886
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   887
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
   888
apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   889
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   890
apply (rule_tac p = "u" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   891
apply (rule_tac t = "u" in ssum_lemma5 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   892
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   893
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
   894
apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   895
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   896
apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   897
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   898
apply (rule less_ssum3c [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   899
apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   900
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   901
apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   902
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   903
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   904
apply (erule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   905
apply (rule less_ssum3c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   906
apply (rule_tac t = "Isinl (x) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   907
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   908
apply (erule ub_rangeD)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   909
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   910
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   911
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   912
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   913
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
   914
      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
   915
apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   916
apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   917
apply (erule allE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   918
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   919
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
   920
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   921
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
   922
apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   923
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   924
apply (rule_tac p = "u" in IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   925
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   926
apply (rule less_ssum3d [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   927
apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   928
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   929
apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   930
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   931
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   932
apply (erule notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   933
apply (rule less_ssum3d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   934
apply (rule_tac t = "Isinr (y) " in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   935
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   936
apply (erule ub_rangeD)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   937
apply (rule_tac t = "u" in ssum_lemma6 [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   938
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   939
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
   940
apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   941
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   942
apply (erule monofun_Iwhen3 [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   943
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   944
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   945
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   946
lemmas thelub_ssum1a = lub_ssum1a [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   947
(*
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   948
[| chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   949
 lub (range ?Y1) = Isinl
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   950
 (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
   951
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   952
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   953
lemmas thelub_ssum1b = lub_ssum1b [THEN thelubI, standard]
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
[| chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   956
 lub (range ?Y1) = Isinr
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   957
 (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
   958
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   959
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   960
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
   961
apply (rule ssum_lemma4 [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   962
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   963
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   964
apply (erule lub_ssum1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   965
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   966
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   967
apply (erule lub_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
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   970
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   971
(* Class instance of  ++ for class pcpo *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   972
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   973
instance "++" :: (pcpo,pcpo)pcpo
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   974
apply (intro_classes)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   975
apply (erule cpo_ssum)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   976
apply (rule least_ssum)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   977
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   978
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   979
consts  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   980
        sinl    :: "'a -> ('a++'b)" 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   981
        sinr    :: "'b -> ('a++'b)" 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   982
        sscase  :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   983
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   984
defs
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
sinl_def:        "sinl   == (LAM x. Isinl(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   987
sinr_def:        "sinr   == (LAM x. Isinr(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   988
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
   989
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   990
translations
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   991
"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
   992
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   993
(* for compatibility with old HOLCF-Version *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   994
lemma inst_ssum_pcpo: "UU = Isinl UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   995
apply (simp add: UU_def UU_ssum_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   996
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   997
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   998
declare inst_ssum_pcpo [symmetric, simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   999
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1000
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1001
(* continuity for Isinl and Isinr                                           *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1002
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1003
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1004
lemma contlub_Isinl: "contlub(Isinl)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1005
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1006
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1007
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1008
apply (rule_tac [2] thelub_ssum1a [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1009
apply (rule_tac [3] allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1010
apply (rule_tac [3] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1011
apply (rule_tac [3] refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1012
apply (erule_tac [2] monofun_Isinl [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1013
apply (case_tac "lub (range (Y))=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1014
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
  1015
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1016
apply (rule_tac f = "Isinl" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1017
apply (rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1018
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1019
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
  1020
apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1021
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1022
apply (rule Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1023
apply (rule_tac f = "Isinl" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1024
apply (rule lub_equal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1025
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1026
apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1027
apply (erule monofun_Isinl [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1028
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1029
apply (case_tac "Y (k) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1030
apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1031
apply (rule Iwhen1[symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1032
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1033
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1034
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1035
lemma contlub_Isinr: "contlub(Isinr)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1036
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1037
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1038
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1039
apply (rule_tac [2] thelub_ssum1b [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1040
apply (rule_tac [3] allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1041
apply (rule_tac [3] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1042
apply (rule_tac [3] refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1043
apply (erule_tac [2] monofun_Isinr [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1044
apply (case_tac "lub (range (Y))=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1045
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
  1046
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1047
apply (rule arg_cong, rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1048
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1049
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
  1050
apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1051
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1052
apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1053
apply (rule Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1054
apply (rule arg_cong, rule lub_equal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1055
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1056
apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1057
apply (erule monofun_Isinr [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1058
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1059
apply (case_tac "Y (k) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1060
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1061
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1062
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1063
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1064
lemma cont_Isinl: "cont(Isinl)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1065
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1066
apply (rule monofun_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1067
apply (rule contlub_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1068
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1069
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1070
lemma cont_Isinr: "cont(Isinr)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1071
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1072
apply (rule monofun_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1073
apply (rule contlub_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1074
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1075
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1076
declare cont_Isinl [iff] cont_Isinr [iff]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1077
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1078
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1079
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1080
(* continuity for Iwhen in the firts two arguments                          *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1081
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1082
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1083
lemma contlub_Iwhen1: "contlub(Iwhen)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1084
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1085
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1086
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1087
apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1088
apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1089
apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1090
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1091
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1092
apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1093
apply (rule_tac [2] ch2ch_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1094
apply (erule_tac [2] monofun_Iwhen1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1095
apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1096
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1097
apply (rule_tac p = "xa" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1098
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1099
apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1100
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1101
apply (erule contlub_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1102
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1103
apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1104
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1105
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1106
lemma contlub_Iwhen2: "contlub(Iwhen(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1107
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1108
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1109
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1110
apply (rule_tac [2] thelub_fun [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1111
apply (erule_tac [2] monofun_Iwhen2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1112
apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1113
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1114
apply (rule_tac p = "x" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1115
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1116
apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1117
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1118
apply (rule lub_const [THEN thelubI, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1119
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1120
apply (erule contlub_cfun_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1121
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1122
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1123
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1124
(* continuity for Iwhen in its third argument                               *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1125
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1126
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1127
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1128
(* first 5 ugly lemmas                                                      *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1129
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1130
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1131
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
  1132
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1133
apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1134
apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1135
apply (erule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1136
apply (rule_tac P = "y=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1137
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1138
apply (rule less_ssum3d [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1139
apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1140
apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1141
apply (erule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1142
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1143
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1144
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1145
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
  1146
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1147
apply (rule_tac p = "Y (i) " in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1148
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1149
apply (erule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1150
apply (rule strict_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1151
apply (erule_tac [2] exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1152
apply (rule_tac P = "xa=UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1153
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1154
apply (rule less_ssum3c [THEN iffD1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1155
apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1156
apply (erule subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1157
apply (erule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1158
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1159
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1160
lemma ssum_lemma11: "[| chain(Y); lub(range(Y)) = Isinl(UU) |] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1161
    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
  1162
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1163
apply (rule chain_UU_I_inverse [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1164
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1165
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
  1166
apply (rule inst_ssum_pcpo [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1167
apply (rule chain_UU_I [THEN spec, symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1168
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1169
apply (erule inst_ssum_pcpo [THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1170
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1171
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1172
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1173
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
  1174
    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
  1175
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1176
apply (rule_tac t = "x" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1177
apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1178
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1179
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1180
apply (rule thelub_ssum1a [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1181
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1182
apply (erule ssum_lemma9)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1183
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1184
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1185
apply (rule contlub_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1186
apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1187
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1188
apply (rule lub_equal2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1189
apply (rule chain_mono2 [THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1190
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1191
apply (rule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1192
apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1193
apply (erule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1194
apply (rule inject_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1195
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1196
apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1197
apply (erule notnotD)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1198
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1199
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1200
apply (rule ssum_lemma9 [THEN spec, THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1201
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1202
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1203
apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1204
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1205
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1206
apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1207
apply (rule Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1208
apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1209
apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1210
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1211
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1212
apply (subst Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1213
apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1214
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1215
apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1216
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1217
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1218
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1219
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1220
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1221
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
  1222
    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
  1223
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1224
apply (rule_tac t = "x" in subst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1225
apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1226
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1227
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1228
apply (rule thelub_ssum1b [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1229
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1230
apply (erule ssum_lemma10)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1231
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1232
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1233
apply (rule contlub_cfun_arg)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1234
apply (rule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1235
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1236
apply (rule lub_equal2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1237
apply (rule chain_mono2 [THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1238
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1239
apply (rule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1240
apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1241
apply (erule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1242
apply (rule inject_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1243
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1244
apply (erule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1245
apply (rule strict_IsinlIsinr [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1246
apply (erule notnotD)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1247
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1248
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1249
apply (rule ssum_lemma10 [THEN spec, THEN exE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1250
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1251
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1252
apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1253
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1254
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1255
apply (rule cfun_arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1256
apply (rule Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1257
apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1258
apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1259
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1260
apply (subst Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1261
apply force
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1262
apply (rule_tac t = "Y (i) " in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1263
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1264
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1265
apply (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1266
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1267
apply (erule monofun_Iwhen3 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1268
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1269
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1270
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1271
lemma contlub_Iwhen3: "contlub(Iwhen(f)(g))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1272
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1273
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1274
apply (rule_tac p = "lub (range (Y))" in IssumE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1275
apply (erule ssum_lemma11)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1276
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1277
apply (erule ssum_lemma12)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1278
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1279
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1280
apply (erule ssum_lemma13)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1281
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1282
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1283
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1284
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1285
lemma cont_Iwhen1: "cont(Iwhen)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1286
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1287
apply (rule monofun_Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1288
apply (rule contlub_Iwhen1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1289
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1290
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1291
lemma cont_Iwhen2: "cont(Iwhen(f))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1292
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1293
apply (rule monofun_Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1294
apply (rule contlub_Iwhen2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1295
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1296
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1297
lemma cont_Iwhen3: "cont(Iwhen(f)(g))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1298
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1299
apply (rule monofun_Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1300
apply (rule contlub_Iwhen3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1301
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1302
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1303
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1304
(* continuous versions of lemmas for 'a ++ 'b                               *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1305
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1306
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1307
lemma strict_sinl [simp]: "sinl$UU =UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1308
apply (unfold sinl_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1309
apply (simp add: cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1310
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1311
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1312
lemma strict_sinr [simp]: "sinr$UU=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1313
apply (unfold sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1314
apply (simp add: cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1315
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1316
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1317
lemma noteq_sinlsinr: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1318
        "sinl$a=sinr$b ==> a=UU & b=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1319
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1320
apply (auto dest!: noteq_IsinlIsinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1321
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1322
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1323
lemma inject_sinl: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1324
        "sinl$a1=sinl$a2==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1325
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1326
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1327
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1328
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1329
lemma inject_sinr: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1330
        "sinr$a1=sinr$a2==> a1=a2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1331
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1332
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1333
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1334
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1335
declare inject_sinl [dest!] inject_sinr [dest!]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1336
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1337
lemma defined_sinl [simp]: "x~=UU ==> sinl$x ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1338
apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1339
apply (rule inject_sinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1340
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1341
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1342
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1343
lemma defined_sinr [simp]: "x~=UU ==> sinr$x ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1344
apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1345
apply (rule inject_sinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1346
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1347
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1348
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1349
lemma Exh_Ssum1: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1350
        "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
  1351
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1352
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1353
apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1354
apply (rule Exh_Ssum)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1355
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1356
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1357
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1358
lemma ssumE:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1359
assumes major: "p=UU ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1360
assumes prem2: "!!x.[|p=sinl$x; x~=UU |] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1361
assumes prem3: "!!y.[|p=sinr$y; y~=UU |] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1362
shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1363
apply (rule major [THEN IssumE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1364
apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1365
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1366
apply (rule prem2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1367
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1368
apply (simp add: sinl_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1369
apply (rule prem3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1370
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1371
apply (simp add: sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1372
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1373
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1374
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1375
lemma ssumE2:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1376
assumes preml: "!!x.[|p=sinl$x|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1377
assumes premr: "!!y.[|p=sinr$y|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1378
shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1379
apply (rule IssumE2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1380
apply (rule preml)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1381
apply (rule_tac [2] premr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1382
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1383
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1384
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1385
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1386
lemmas ssum_conts = cont_lemmas1 cont_Iwhen1 cont_Iwhen2
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1387
                cont_Iwhen3 cont2cont_CF1L
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1388
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1389
lemma sscase1 [simp]: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1390
        "sscase$f$g$UU = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1391
apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1392
apply (subst inst_ssum_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1393
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1394
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1395
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1396
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1397
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1398
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1399
apply (simp only: Ssum0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1400
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1401
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1402
lemma sscase2 [simp]: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1403
        "x~=UU==> sscase$f$g$(sinl$x) = f$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1404
apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1405
apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1406
apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1407
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1408
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1409
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1410
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1411
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1412
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1413
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1414
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1415
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1416
lemma sscase3 [simp]: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1417
        "x~=UU==> sscase$f$g$(sinr$x) = g$x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1418
apply (unfold sscase_def sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1419
apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1420
apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1421
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1422
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1423
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1424
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1425
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1426
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1427
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1428
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1429
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1430
lemma less_ssum4a: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1431
        "(sinl$x << sinl$y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1432
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1433
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1434
apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1435
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1436
apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1437
apply (rule less_ssum3a)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1438
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1439
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1440
lemma less_ssum4b: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1441
        "(sinr$x << sinr$y) = (x << y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1442
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1443
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1444
apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1445
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1446
apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1447
apply (rule less_ssum3b)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1448
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1449
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1450
lemma less_ssum4c: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1451
        "(sinl$x << sinr$y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1452
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1453
apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1454
apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1455
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1456
apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1457
apply (rule less_ssum3c)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1458
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1459
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1460
lemma less_ssum4d: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1461
        "(sinr$x << sinl$y) = (x = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1462
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1463
apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1464
apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1465
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1466
apply (rule cont_Isinr)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1467
apply (rule less_ssum3d)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1468
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1469
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1470
lemma ssum_chainE: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1471
        "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
  1472
apply (unfold sinl_def sinr_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1473
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1474
apply (erule ssum_lemma4)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1475
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1476
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1477
lemma thelub_ssum2a: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1478
"[| chain(Y); !i.? x. Y(i) = sinl$x |] ==>  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1479
    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
  1480
apply (unfold sinl_def sinr_def sscase_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1481
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1482
apply (rule cont_Isinl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1483
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1484
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1485
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1486
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1487
apply (subst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1488
apply (intro ssum_conts)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1489
apply (rule thelub_ssum1a)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1490
apply assumption