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