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