src/HOLCF/Sprod.thy
author huffman
Fri, 04 Mar 2005 23:23:47 +0100
changeset 15577 e16da3068ad6
parent 15576 efb95d0d01f7
child 15591 50c3384ca6c4
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/Sprod0.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 product 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 products *}
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 Sprod
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
  Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    17
 "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a  & y=b ))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    18
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    19
typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    20
by auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    21
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    22
syntax (xsymbols)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    23
  "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    24
syntax (HTML output)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    25
  "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    26
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    27
subsection {* @{term Ispair}, @{term Isfst}, and @{term Issnd} *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    28
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    29
consts
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    30
  Ispair        :: "['a,'b] => ('a ** 'b)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    31
  Isfst         :: "('a ** 'b) => 'a"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    32
  Issnd         :: "('a ** 'b) => 'b"  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    33
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    34
defs
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    35
   (*defining the abstract constants*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    36
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    37
  Ispair_def:    "Ispair a b == Abs_Sprod(Spair_Rep a 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
  Isfst_def:     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    40
                &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    41
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    42
  Issnd_def:     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    43
                &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    44
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    45
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    46
(* A non-emptyness result for Sprod                                         *)
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
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    49
lemma SprodI: "(Spair_Rep a b):Sprod"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    50
apply (unfold Sprod_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    51
apply (rule CollectI, rule exI, rule exI, rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    52
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    53
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    54
lemma inj_on_Abs_Sprod: "inj_on Abs_Sprod Sprod"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    55
apply (rule inj_on_inverseI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    56
apply (erule Abs_Sprod_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    57
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    58
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    59
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    60
(* Strictness and definedness of Spair_Rep                                  *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    61
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    62
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    63
lemma strict_Spair_Rep: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    64
 "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    65
apply (unfold Spair_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    66
apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    67
apply (rule ext)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    68
apply (rule iffI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    69
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    70
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    71
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    72
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    73
lemma defined_Spair_Rep_rev: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    74
 "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    75
apply (unfold Spair_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    76
apply (case_tac "a=UU|b=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    77
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    78
apply (fast dest: fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    79
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    80
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    81
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    82
(* injectivity of Spair_Rep and Ispair                                      *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    83
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    84
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    85
lemma inject_Spair_Rep: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    86
"[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    87
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    88
apply (unfold Spair_Rep_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    89
apply (drule fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    90
apply (drule fun_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    91
apply (erule iffD1 [THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    92
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    93
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    94
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    95
lemma inject_Ispair: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    96
        "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    97
apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    98
apply (erule inject_Spair_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    99
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   100
apply (erule inj_on_Abs_Sprod [THEN inj_onD])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   101
apply (rule SprodI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   102
apply (rule SprodI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   103
done
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
(* strictness and definedness of Ispair                                     *)
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 strict_Ispair: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   110
 "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   111
apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   112
apply (erule strict_Spair_Rep [THEN arg_cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   113
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   114
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   115
lemma strict_Ispair1: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   116
        "Ispair UU b  = Ispair UU UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   117
apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   118
apply (rule strict_Spair_Rep [THEN arg_cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   119
apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   120
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   121
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   122
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   123
lemma strict_Ispair2: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   124
        "Ispair a UU = Ispair UU UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   125
apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   126
apply (rule strict_Spair_Rep [THEN arg_cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   127
apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   128
apply (rule refl)
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 strict_Ispair_rev: "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   132
apply (rule de_Morgan_disj [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   133
apply (erule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   134
apply (erule strict_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   135
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   136
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   137
lemma defined_Ispair_rev: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   138
        "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   139
apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   140
apply (rule defined_Spair_Rep_rev)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   141
apply (rule inj_on_Abs_Sprod [THEN inj_onD])
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
apply (rule SprodI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   144
apply (rule SprodI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   145
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   146
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   147
lemma defined_Ispair: "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   148
apply (rule contrapos_nn)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   149
apply (erule_tac [2] defined_Ispair_rev)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   150
apply (rule de_Morgan_disj [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   151
apply (erule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   152
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   153
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   154
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   155
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   156
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   157
(* Exhaustion of the strict product **                                      *)
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
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   160
lemma Exh_Sprod:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   161
        "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   162
apply (unfold Ispair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   163
apply (rule Rep_Sprod[unfolded Sprod_def, THEN CollectE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   164
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   165
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   166
apply (rule excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   167
apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   168
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   169
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   170
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   171
apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   172
apply (erule arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   173
apply (rule de_Morgan_disj [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   174
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   175
apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   176
apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   177
apply (rule_tac f = "Abs_Sprod" in arg_cong)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   178
apply (erule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   179
apply (erule strict_Spair_Rep)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   180
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   181
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   182
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   183
(* general elimination rule for strict product                              *)
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
lemma IsprodE:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   187
assumes prem1: "p=Ispair UU UU ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   188
assumes prem2: "!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   189
shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   190
apply (rule Exh_Sprod [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   191
apply (erule prem1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   192
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   193
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   194
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   195
apply (erule conjE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   196
apply (erule prem2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   197
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   198
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   199
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   200
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   201
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   202
(* some results about the selectors Isfst, Issnd                            *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   203
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   204
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   205
lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   206
apply (unfold Isfst_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   207
apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   208
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   209
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   210
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   211
apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   212
apply (rule not_sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   213
apply (rule defined_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   214
apply (fast+)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   215
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   216
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   217
lemma strict_Isfst1 [simp]: "Isfst(Ispair UU y) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   218
apply (subst strict_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   219
apply (rule strict_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   220
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   221
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   222
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   223
lemma strict_Isfst2 [simp]: "Isfst(Ispair x UU) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   224
apply (subst strict_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   225
apply (rule strict_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   226
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   227
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   228
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   229
lemma strict_Issnd: "p=Ispair UU UU ==>Issnd p=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   230
apply (unfold Issnd_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   231
apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   232
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   233
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   234
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   235
apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   236
apply (rule not_sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   237
apply (rule defined_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   238
apply (fast+)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   239
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   240
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   241
lemma strict_Issnd1 [simp]: "Issnd(Ispair UU y) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   242
apply (subst strict_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   243
apply (rule strict_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   244
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   245
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   246
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   247
lemma strict_Issnd2 [simp]: "Issnd(Ispair x UU) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   248
apply (subst strict_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   249
apply (rule strict_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   250
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   251
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   252
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   253
lemma Isfst: "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   254
apply (unfold Isfst_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   255
apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   256
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   257
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   258
apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   259
apply (erule defined_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   260
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   261
apply assumption
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 inject_Ispair [THEN conjunct1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   264
prefer 3 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   265
apply (fast+)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   266
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   267
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   268
lemma Issnd: "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   269
apply (unfold Issnd_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   270
apply (rule some_equality)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   271
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   272
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   273
apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   274
apply (erule defined_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   275
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   276
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   277
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   278
apply (rule inject_Ispair [THEN conjunct2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   279
prefer 3 apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   280
apply (fast+)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   281
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   282
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   283
lemma Isfst2: "y~=UU ==>Isfst(Ispair x y)=x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   284
apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   285
apply (erule Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   286
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   287
apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   288
apply (rule strict_Isfst1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   289
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   290
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   291
lemma Issnd2: "~x=UU ==>Issnd(Ispair x y)=y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   292
apply (rule_tac Q = "y=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   293
apply (erule Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   294
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   295
apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   296
apply (rule strict_Issnd2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   297
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   298
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   299
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   300
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   301
(* instantiate the simplifier                                               *)
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
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   304
lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   305
                 Isfst2 Issnd2
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   306
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   307
declare Isfst2 [simp] Issnd2 [simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   308
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   309
lemma defined_IsfstIssnd: "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   310
apply (rule_tac p = "p" in IsprodE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   311
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   312
apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   313
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   314
apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   315
apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   316
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   317
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   318
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   319
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   320
(* Surjective pairing: equivalent to Exh_Sprod                              *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   321
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   322
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   323
lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   324
apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   325
apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   326
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   327
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   328
apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   329
done
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
lemma Sel_injective_Sprod: "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   332
apply (subgoal_tac "Ispair (Isfst x) (Issnd x) =Ispair (Isfst y) (Issnd y) ")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   333
apply (simp (no_asm_use) add: surjective_pairing_Sprod[symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   334
apply simp
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   335
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   336
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   337
subsection {* The strict product is a partial order *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   338
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   339
instance "**"::(sq_ord,sq_ord)sq_ord ..
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   340
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   341
defs (overloaded)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   342
  less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   343
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   344
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   345
(* less_sprod is a partial order on Sprod                                   *)
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
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   348
lemma refl_less_sprod: "(p::'a ** 'b) << p"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   349
apply (unfold less_sprod_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   350
apply (fast intro: refl_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   351
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   352
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   353
lemma antisym_less_sprod: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   354
        "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   355
apply (unfold less_sprod_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   356
apply (rule Sel_injective_Sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   357
apply (fast intro: antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   358
apply (fast intro: antisym_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   359
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   360
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   361
lemma trans_less_sprod: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   362
        "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   363
apply (unfold less_sprod_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   364
apply (blast intro: trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   365
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   366
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   367
instance "**"::(pcpo,pcpo)po
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   368
by intro_classes
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   369
  (assumption | rule refl_less_sprod antisym_less_sprod trans_less_sprod)+
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   370
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   371
(* for compatibility with old HOLCF-Version *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   372
lemma inst_sprod_po: "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   373
apply (fold less_sprod_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   374
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   375
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   376
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   377
subsection {* The strict product is pointed *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   378
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   379
(* type sprod is pointed                                                    *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   380
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   381
(*
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   382
lemma minimal_sprod: "Ispair UU UU << p"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   383
apply (simp add: inst_sprod_po minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   384
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   385
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   386
lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   387
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   388
lemma least_sprod: "? x::'a**'b.!y. x<<y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   389
apply (rule_tac x = "Ispair UU UU" in exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   390
apply (rule minimal_sprod [THEN allI])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   391
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   392
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   393
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   394
(* Ispair is monotone in both arguments                                     *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   395
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   396
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   397
lemma monofun_Ispair1: "monofun(Ispair)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   398
apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   399
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   400
apply (rule less_fun [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   401
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   402
apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   403
apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   404
apply (frule notUU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   405
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   406
apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   407
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   408
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   409
lemma monofun_Ispair2: "monofun(Ispair(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   410
apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   411
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   412
apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   413
apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   414
apply (frule notUU_I)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   415
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   416
apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   417
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   418
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   419
lemma monofun_Ispair: "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   420
apply (rule trans_less)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   421
apply (rule monofun_Ispair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   422
prefer 2 apply (rule monofun_Ispair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   423
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   424
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   425
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   426
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   427
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   428
(* Isfst and Issnd are monotone                                             *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   429
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   430
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   431
lemma monofun_Isfst: "monofun(Isfst)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   432
apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   433
apply (simp add: inst_sprod_po)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   434
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   435
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   436
lemma monofun_Issnd: "monofun(Issnd)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   437
apply (unfold monofun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   438
apply (simp add: inst_sprod_po)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   439
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   440
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   441
subsection {* The strict product is a cpo *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   442
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   443
(* the type 'a ** 'b is a cpo                                               *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   444
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   445
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   446
lemma lub_sprod: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   447
"[|chain(S)|] ==> range(S) <<|  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   448
  Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   449
apply (rule is_lubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   450
apply (rule ub_rangeI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   451
apply (rule_tac t = "S (i) " in surjective_pairing_Sprod [THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   452
apply (rule monofun_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   453
apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   454
apply (erule monofun_Isfst [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   455
apply (rule is_ub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   456
apply (erule monofun_Issnd [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   457
apply (rule_tac t = "u" in surjective_pairing_Sprod [THEN ssubst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   458
apply (rule monofun_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   459
apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   460
apply (erule monofun_Isfst [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   461
apply (erule monofun_Isfst [THEN ub2ub_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   462
apply (rule is_lub_thelub)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   463
apply (erule monofun_Issnd [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   464
apply (erule monofun_Issnd [THEN ub2ub_monofun])
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
lemmas thelub_sprod = lub_sprod [THEN thelubI, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   468
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   469
lemma cpo_sprod: "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   470
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   471
apply (erule lub_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   472
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   473
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   474
instance "**" :: (pcpo, pcpo) cpo
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   475
by intro_classes (rule cpo_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   476
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   477
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   478
subsection {* The strict product is a pcpo *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   479
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   480
lemma minimal_sprod: "Ispair UU UU << p"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   481
apply (simp add: inst_sprod_po minimal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   482
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   483
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   484
lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   485
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   486
lemma least_sprod: "? x::'a**'b.!y. x<<y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   487
apply (rule_tac x = "Ispair UU UU" in exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   488
apply (rule minimal_sprod [THEN allI])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   489
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   490
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   491
instance "**" :: (pcpo, pcpo) pcpo
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   492
by intro_classes (rule least_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   493
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   494
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   495
subsection {* Other constants *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   496
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   497
consts  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   498
  spair		:: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   499
  sfst		:: "('a**'b)->'a"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   500
  ssnd		:: "('a**'b)->'b"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   501
  ssplit	:: "('a->'b->'c)->('a**'b)->'c"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   502
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   503
syntax  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   504
  "@stuple"	:: "['a, args] => 'a ** 'b"	("(1'(:_,/ _:'))")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   505
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   506
translations
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   507
        "(:x, y, z:)"   == "(:x, (:y, z:):)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   508
        "(:x, y:)"      == "spair$x$y"
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
defs
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   511
spair_def:       "spair  == (LAM x y. Ispair x y)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   512
sfst_def:        "sfst   == (LAM p. Isfst p)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   513
ssnd_def:        "ssnd   == (LAM p. Issnd p)"     
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   514
ssplit_def:      "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   515
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   516
(* for compatibility with old HOLCF-Version *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   517
lemma inst_sprod_pcpo: "UU = Ispair UU UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   518
apply (simp add: UU_def UU_sprod_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   519
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   520
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   521
declare inst_sprod_pcpo [symmetric, simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   522
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   523
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   524
(* continuity of Ispair, Isfst, Issnd                                       *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   525
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   526
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   527
lemma sprod3_lemma1: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   528
"[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   529
  Ispair (lub(range Y)) x = 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   530
  Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   531
         (lub(range(%i. Issnd(Ispair(Y i) x))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   532
apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   533
apply (rule lub_equal)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   534
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   535
apply (rule monofun_Isfst [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   536
apply (rule ch2ch_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   537
apply (rule monofun_Ispair1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   538
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   539
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   540
apply (simp (no_asm_simp))
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   541
apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   542
apply (drule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   543
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   544
apply (rule lub_chain_maxelem)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   545
apply (erule Issnd2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   546
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   547
apply (rename_tac "j")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   548
apply (case_tac "Y (j) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   549
apply auto
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 sprod3_lemma2: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   553
"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   554
    Ispair (lub(range Y)) x = 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   555
    Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   556
           (lub(range(%i. Issnd(Ispair(Y i) x))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   557
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
   558
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   559
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   560
apply (rule strict_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   561
apply (rule strict_Ispair [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   562
apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   563
apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   564
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   565
apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   566
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   567
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   568
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   569
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   570
lemma sprod3_lemma3: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   571
"[| chain(Y); x = UU |] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   572
           Ispair (lub(range Y)) x = 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   573
           Ispair (lub(range(%i. Isfst(Ispair (Y i) x)))) 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   574
                  (lub(range(%i. Issnd(Ispair (Y i) x))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   575
apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   576
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   577
apply (rule strict_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   578
apply (rule strict_Ispair [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   579
apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   580
apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   581
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   582
apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   583
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   584
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   585
lemma contlub_Ispair1: "contlub(Ispair)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   586
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   587
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   588
apply (rule expand_fun_eq [THEN iffD2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   589
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   590
apply (subst lub_fun [THEN thelubI])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   591
apply (erule monofun_Ispair1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   592
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   593
apply (rule_tac [2] thelub_sprod [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   594
apply (rule_tac [2] ch2ch_fun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   595
apply (erule_tac [2] monofun_Ispair1 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   596
apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   597
apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   598
apply (erule sprod3_lemma1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   599
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   600
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   601
apply (erule sprod3_lemma2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   602
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   603
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   604
apply (erule sprod3_lemma3)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   605
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   606
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   607
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   608
lemma sprod3_lemma4: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   609
"[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   610
          Ispair x (lub(range Y)) = 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   611
          Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   612
                 (lub(range(%i. Issnd (Ispair x (Y i)))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   613
apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   614
apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   615
apply (drule chain_UU_I_inverse2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   616
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   617
apply (rule lub_chain_maxelem)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   618
apply (erule Isfst2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   619
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   620
apply (rename_tac "j")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   621
apply (case_tac "Y (j) =UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   622
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   623
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   624
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   625
lemma sprod3_lemma5: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   626
"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   627
          Ispair x (lub(range Y)) = 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   628
          Ispair (lub(range(%i. Isfst(Ispair x (Y i))))) 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   629
                 (lub(range(%i. Issnd(Ispair x (Y i)))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   630
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
   631
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   632
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   633
apply (rule strict_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   634
apply (rule strict_Ispair [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   635
apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   636
apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   637
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   638
apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   639
apply (erule chain_UU_I [THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   640
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   641
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   642
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   643
lemma sprod3_lemma6: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   644
"[| chain(Y); x = UU |] ==> 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   645
          Ispair x (lub(range Y)) = 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   646
          Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   647
                 (lub(range(%i. Issnd (Ispair x (Y i)))))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   648
apply (rule_tac s = "UU" and t = "x" in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   649
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   650
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   651
apply (rule strict_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   652
apply (rule strict_Ispair [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   653
apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   654
apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   655
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   656
apply (simp add: Sprod0_ss)
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 contlub_Ispair2: "contlub(Ispair(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   660
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   661
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   662
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   663
apply (rule_tac [2] thelub_sprod [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   664
apply (erule_tac [2] monofun_Ispair2 [THEN ch2ch_monofun])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   665
apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   666
apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   667
apply (erule sprod3_lemma4)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   668
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   669
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   670
apply (erule sprod3_lemma5)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   671
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   672
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   673
apply (erule sprod3_lemma6)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   674
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   675
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   676
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   677
lemma cont_Ispair1: "cont(Ispair)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   678
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   679
apply (rule monofun_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   680
apply (rule contlub_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   681
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   682
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   683
lemma cont_Ispair2: "cont(Ispair(x))"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   684
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   685
apply (rule monofun_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   686
apply (rule contlub_Ispair2)
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
lemma contlub_Isfst: "contlub(Isfst)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   690
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   691
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   692
apply (subst lub_sprod [THEN thelubI])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   693
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   694
apply (rule_tac Q = "lub (range (%i. Issnd (Y (i))))=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   695
apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   696
apply (rule_tac s = "UU" and t = "lub (range (%i. Issnd (Y (i))))" in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   697
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   698
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   699
apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   700
apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   701
apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   702
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   703
apply (rule strict_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   704
apply (rule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   705
apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct2])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   706
apply (fast dest!: monofun_Issnd [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   707
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   708
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   709
lemma contlub_Issnd: "contlub(Issnd)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   710
apply (rule contlubI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   711
apply (intro strip)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   712
apply (subst lub_sprod [THEN thelubI])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   713
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   714
apply (rule_tac Q = "lub (range (%i. Isfst (Y (i))))=UU" in excluded_middle [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   715
apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   716
apply (rule_tac s = "UU" and t = "lub (range (%i. Isfst (Y (i))))" in ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   717
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   718
apply (simp add: Sprod0_ss)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   719
apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   720
apply (rule chain_UU_I_inverse)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   721
apply (rule allI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   722
apply (rule strict_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   723
apply (rule contrapos_np)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   724
apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct1])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   725
apply (fast dest!: monofun_Isfst [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   726
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   727
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   728
lemma cont_Isfst: "cont(Isfst)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   729
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   730
apply (rule monofun_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   731
apply (rule contlub_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   732
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   733
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   734
lemma cont_Issnd: "cont(Issnd)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   735
apply (rule monocontlub2cont)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   736
apply (rule monofun_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   737
apply (rule contlub_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   738
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   739
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   740
lemma spair_eq: "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   741
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   742
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   743
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   744
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   745
(* convert all lemmas to the continuous versions                            *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   746
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   747
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   748
lemma beta_cfun_sprod [simp]: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   749
        "(LAM x y. Ispair x y)$a$b = Ispair a b"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   750
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   751
apply (simp (no_asm) add: cont_Ispair2 cont_Ispair1 cont2cont_CF1L)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   752
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   753
apply (rule cont_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   754
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   755
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   756
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   757
lemma inject_spair: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   758
        "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   759
apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   760
apply (erule inject_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   761
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   762
apply (erule box_equals)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   763
apply (rule beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   764
apply (rule beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   765
done
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
lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   768
apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   769
apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   770
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   771
apply (rule beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   772
apply (rule sym)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   773
apply (rule inst_sprod_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   774
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   775
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   776
lemma strict_spair: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   777
        "(a=UU | b=UU) ==> (:a,b:)=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   778
apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   779
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   780
apply (rule beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   781
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   782
apply (rule_tac [2] inst_sprod_pcpo [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   783
apply (erule strict_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   784
done
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 strict_spair1: "(:UU,b:) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   787
apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   788
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   789
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   790
apply (rule_tac [2] inst_sprod_pcpo [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   791
apply (rule strict_Ispair1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   792
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   793
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   794
lemma strict_spair2: "(:a,UU:) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   795
apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   796
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   797
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   798
apply (rule_tac [2] inst_sprod_pcpo [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   799
apply (rule strict_Ispair2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   800
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   801
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   802
declare strict_spair1 [simp] strict_spair2 [simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   803
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   804
lemma strict_spair_rev: "(:x,y:)~=UU ==> ~x=UU & ~y=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   805
apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   806
apply (rule strict_Ispair_rev)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   807
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   808
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   809
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   810
lemma defined_spair_rev: "(:a,b:) = UU ==> (a = UU | b = UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   811
apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   812
apply (rule defined_Ispair_rev)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   813
apply auto
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   814
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   815
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   816
lemma defined_spair: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   817
        "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   818
apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   819
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   820
apply (subst inst_sprod_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   821
apply (erule defined_Ispair)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   822
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   823
done
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
lemma Exh_Sprod2:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   826
        "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   827
apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   828
apply (rule Exh_Sprod [THEN disjE])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   829
apply (rule disjI1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   830
apply (subst inst_sprod_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   831
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   832
apply (rule disjI2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   833
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   834
apply (erule exE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   835
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   836
apply (rule exI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   837
apply (rule conjI)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   838
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   839
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   840
apply fast
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   841
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   842
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   843
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   844
lemma sprodE:
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   845
assumes prem1: "p=UU ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   846
assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   847
shows "Q"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   848
apply (rule IsprodE)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   849
apply (rule prem1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   850
apply (subst inst_sprod_pcpo)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   851
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   852
apply (rule prem2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   853
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   854
prefer 2 apply (assumption)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   855
apply (unfold spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   856
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   857
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   858
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   859
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   860
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   861
lemma strict_sfst: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   862
        "p=UU==>sfst$p=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   863
apply (unfold sfst_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   864
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   865
apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   866
apply (rule strict_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   867
apply (rule inst_sprod_pcpo [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   868
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   869
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   870
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   871
lemma strict_sfst1: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   872
        "sfst$(:UU,y:) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   873
apply (unfold sfst_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   874
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   875
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   876
apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   877
apply (rule strict_Isfst1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   878
done
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
lemma strict_sfst2: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   881
        "sfst$(:x,UU:) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   882
apply (unfold sfst_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   883
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   884
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   885
apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   886
apply (rule strict_Isfst2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   887
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   888
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   889
lemma strict_ssnd: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   890
        "p=UU==>ssnd$p=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   891
apply (unfold ssnd_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   892
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   893
apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   894
apply (rule strict_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   895
apply (rule inst_sprod_pcpo [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   896
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   897
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   898
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   899
lemma strict_ssnd1: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   900
        "ssnd$(:UU,y:) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   901
apply (unfold ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   902
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   903
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   904
apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   905
apply (rule strict_Issnd1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   906
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   907
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   908
lemma strict_ssnd2: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   909
        "ssnd$(:x,UU:) = UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   910
apply (unfold ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   911
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   912
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   913
apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   914
apply (rule strict_Issnd2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   915
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   916
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   917
lemma sfst2: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   918
        "y~=UU ==>sfst$(:x,y:)=x"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   919
apply (unfold sfst_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   920
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   921
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   922
apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   923
apply (erule Isfst2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   924
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   925
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   926
lemma ssnd2: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   927
        "x~=UU ==>ssnd$(:x,y:)=y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   928
apply (unfold ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   929
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   930
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   931
apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   932
apply (erule Issnd2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   933
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   934
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   935
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   936
lemma defined_sfstssnd: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   937
        "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   938
apply (unfold sfst_def ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   939
apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   940
apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   941
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   942
apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   943
apply (rule defined_IsfstIssnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   944
apply (rule inst_sprod_pcpo [THEN subst])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   945
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   946
done
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
lemma surjective_pairing_Sprod2: "(:sfst$p , ssnd$p:) = p"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   949
apply (unfold sfst_def ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   950
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   951
apply (simplesubst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   952
apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   953
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   954
apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   955
apply (rule surjective_pairing_Sprod [symmetric])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   956
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   957
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   958
lemma lub_sprod2: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   959
"chain(S) ==> range(S) <<|  
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   960
               (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   961
apply (unfold sfst_def ssnd_def spair_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   962
apply (subst beta_cfun_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   963
apply (simplesubst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   964
apply (rule cont_Issnd)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   965
apply (subst beta_cfun [THEN ext])
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   966
apply (rule cont_Isfst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   967
apply (erule lub_sprod)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   968
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   969
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   970
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   971
lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard]
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
 "chain ?S1 ==>
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   974
 lub (range ?S1) =
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   975
 (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   976
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   977
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   978
lemma ssplit1: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   979
        "ssplit$f$UU=UU"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   980
apply (unfold ssplit_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   981
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   982
apply (simp (no_asm))
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   983
apply (subst strictify1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   984
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   985
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   986
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   987
lemma ssplit2: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   988
        "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   989
apply (unfold ssplit_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   990
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   991
apply (simp (no_asm))
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   992
apply (subst strictify2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   993
apply (rule defined_spair)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   994
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   995
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   996
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   997
apply (simp (no_asm))
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   998
apply (subst sfst2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
   999
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1000
apply (subst ssnd2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1001
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1002
apply (rule refl)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1003
done
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 ssplit3: 
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1007
  "ssplit$spair$z=z"
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1008
apply (unfold ssplit_def)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1009
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1010
apply (simp (no_asm))
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1011
apply (case_tac "z=UU")
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1012
apply (erule ssubst)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1013
apply (rule strictify1)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1014
apply (rule trans)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1015
apply (rule strictify2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1016
apply assumption
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1017
apply (subst beta_cfun)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1018
apply (simp (no_asm))
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1019
apply (rule surjective_pairing_Sprod2)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1020
done
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1021
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1022
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1023
(* install simplifier for Sprod                                             *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1024
(* ------------------------------------------------------------------------ *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1025
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1026
lemmas Sprod_rews = strict_sfst1 strict_sfst2
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1027
                strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1028
                ssplit1 ssplit2
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1029
declare Sprod_rews [simp]
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1030
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
  1031
end