| DISP | j_act_cor_df | JActCor( < x:j_type:* > )== JActCor( < x > ) |
| ABS | j_act_cor | JActCor(x) ==
case x
of bool - > 
| int - > 
| Exception - > Atom
| Class(n) - > Void
| t[] - > 
|
| THM | j_act_cor_wf |  f:Atom   . x:Type. JActCor(x)   |
| ML | j_act_cor_eval | let j_act_cor_boolC =
SimpleMacroC `j_act_cor_bool`
 JActCor(boolean) ``type_cases bool_type j_act_cor``;;
let j_act_cor_intC =
SimpleMacroC `j_act_cor_int`
JActCor(int) ``type_cases int_type j_act_cor``;;
let j_act_cor_excC =
SimpleMacroC `j_act_cor_exc`
JActCor(Exception) Atom ``type_cases exc_type j_act_cor``;;
let j_act_cor_classC =
SimpleMacroC `j_act_cor_class`
JActCor(Class(n)) Void ``type_cases class_type j_act_cor``;;
let j_act_cor_arrayC =
SimpleMacroC `j_act_cor_array`
JActCor(t[]) ``type_cases array_type j_act_cor``;;
let j_act_corC =
FirstC [j_act_cor_boolC;
j_act_cor_intC;
j_act_cor_excC;
j_act_cor_classC;
j_act_cor_arrayC]
;;
add_AbReduce_conv `j_act_cor` j_act_corC
;; |
| DISP | j_eq_act_cor_df | ( < a:a:* > =ac < b:b:* > wrt < x:j_type:* > )== ( < a > =ac < b > )
( < a:a:* > =ac < b:b:* > )== ( < a > =ac < b > ) |
| ABS | j_eq_act_cor | (a =ac b) ==
case x
of bool - > a =b b
| int - > (a = b)
| Exception - > a =a b
| Class(n) - > tt
| t[] - > (a = b)
|
| ML | j_eq_act_cor_eval | let j_eq_act_cor_boolC =
SimpleMacroC `j_eq_act_cor_bool`
(a =ac b) a =b b ``type_cases bool_type j_eq_act_cor``;;
let j_eq_act_cor_intC =
SimpleMacroC `j_eq_act_cor_int`
(a =ac b) (a = b) ``type_cases int_type j_eq_act_cor``;;
let j_eq_act_cor_excC =
SimpleMacroC `j_eq_act_cor_exc`
(a =ac b) a =a b ``type_cases exc_type j_eq_act_cor``;;
let j_eq_act_cor_classC =
SimpleMacroC `j_eq_act_cor_class`
(a =ac b) tt ``type_cases class_type j_eq_act_cor``;;
let j_eq_act_cor_arrayC =
SimpleMacroC `j_eq_act_cor_array`
(a =ac b) (a = b) ``type_cases array_type j_eq_act_cor``;;
let j_eq_act_corC =
FirstC [j_eq_act_cor_boolC;
j_eq_act_cor_intC;
j_eq_act_cor_excC;
j_eq_act_cor_classC;
j_eq_act_cor_arrayC]
;;
add_AbReduce_conv `j_eq_act_cor` j_eq_act_corC
;; |
| THM | j_eq_act_cor_wf | f:Atom . x:Type. a,b:JActCor(x). (a =ac b) |
| THM | assert_of_j_eq_act_cor | f:Atom . x:Type. a,b:JActCor(x).  (a =ac b)   a = b |
| DISP | j_cor_df | JCor( < x:jtype:* > )== JCor( < x > ) |
| ABS | j_cor | JCor(x) == ?JActCor(x) |
| THM | j_cor_wf | f:Atom . x:Type. JCor(x) |
| THM | comb_for_j_cor_wf | ( f,x,z.JCor(x)) f:(Atom ) x:Type  True |
| ML | j_cor_eval | let j_cor_boolC =
SimpleMacroC `j_cor_bool`
JCor(boolean) ? ``type_cases bool_type j_act_cor j_cor``;;
let j_cor_intC =
SimpleMacroC `j_cor_int`
JCor(int) ? ``type_cases int_type j_act_cor j_cor``;;
let j_cor_excC =
SimpleMacroC `j_cor_exc`
JCor(Exception) ?Atom ``type_cases exc_type j_act_cor j_cor``;;
let j_cor_classC =
SimpleMacroC `j_cor_class`
JCor(Class(n)) ?Void ``type_cases class_type j_act_cor j_cor``;;
let j_cor_arrayC =
SimpleMacroC `j_cor_array`
JCor(t[]) ? ``type_cases array_type j_act_cor j_cor``;;
let j_corC =
FirstC [j_cor_boolC;
j_cor_intC;
j_cor_excC;
j_cor_classC;
j_cor_arrayC]
;;
add_AbReduce_conv `j_cor` j_corC
;; |
| ML | j_cor_hd | let JCorHD i = MoveDepHypsToConcl i THEN D i THENL [RenameVarUsingArg
`x` `a' i THEN Fold `j_ac` 0; D i THEN Thin i THEN Fold `it` 0 THEN Fo
ld `j_c` 0];; |
| DISP | j_c_df | Jc== Jc |
| ABS | j_c | Jc == inr  |
| THM | j_c_wf | f:Atom . x:Type. Jc JCor(x) |
| DISP | j_ac_df | Jac( < a:a:* > )== Jac( < a > ) |
| ABS | j_ac | Jac(a) == inl a |
| THM | j_ac_wf | f:Atom . x:Type. a:JActCor(x). Jac(a) JCor(x) |
| THM | comb_for_j_ac_wf | (f,x,a,z.Jac(a)) f:(Atom )
x:Type
a:JActCor(x)
True
JCor(x) |
| DISP | j_cor_cases_df | {[SOFT}{- > 0}case < x:jcor:* > {\\}of Jc - > < c:term:* > {\\} | Jac( < a:var >
) - > < ac:term:* > {\\}{ < -}{]}
== case < x > of Jc - > < c > | Jac( < a > ) - > < ac > |
| ABS | j_cor_cases | case x of Jc - > c | Jac(a) - > ac[a] ==
case x of inl(a) = > ac[a] | inr(i) = > c |
| ML | j_cor_cases_eval | let j_cor_cases_cC =
SimpleMacroC `j_cor_cases_c`
case Jc of Jc - > c | Jac(a) - > ac[a] c ``j_cor_cases j_c``;;
let j_cor_cases_acC =
SimpleMacroC `j_cor_cases_ac`
case Jac(a) of Jc - > c | Jac(a) - > ac[a] ac[a]
``j_cor_cases j_ac``;;
let j_cor_casesC =
FirstC [j_cor_cases_cC;
j_cor_cases_acC]
;;
add_AbReduce_conv `j_cor_cases` j_cor_casesC
;; |
| THM | j_cor_cases_wf | f:Atom . x:Type. T:. c:T. ac:JActCor(x) T. a:JCor(x).
case a of Jc - > c | Jac(a) - > ac[a] T |
| DISP | j_eq_cor_df | ( < a:jcor:* > =c < b:jcor:* > wrt < x:jtype:* > )== ( < a > =c < b > )
( < a:jcor:* > =c < b:jcor:* > )== ( < a > =c < b > ) |
| ABS | j_eq_cor | (a =c b) ==
case a
of Jc - > case b of Jc - > tt | Jac(u) - > ff
| Jac(ac) - > case b of Jc - > ff | Jac(bc) - > (ac =ac bc)
|
| THM | j_eq_cor_wf | f:Atom . x:Type. a,b:JCor(x). (a =c b) |
| THM | comb_for_j_eq_cor_wf | (f,x,a,b,z.(a =c b)) f:(Atom )
x:Type
a:JCor(x)
b:JCor(x)
True
|
| THM | assert_of_j_eq_cor | f:Atom . x:Type. a,b:JCor(x). (a =c b) a = b |
| THM | j_eq_cor_refl | f:Atom . x:Type. a:JCor(x). (a =c a) |
| THM | j_eq_cor_iff_eq | f:Atom . x:Type. a,b:JCor(x). (a =c b)  a = b |
| DISP | j_idx_df | JIdx( < x:jtype:* > ; < s:spec:* > )== JIdx( < x > )
JIdx( < x:x:* > )== JIdx( < x > ) |
| ABS | j_idx | JIdx(x) ==
case x
of bool - > Void
| int - > Void
| Exception - > Void
| Class(n) - > {a:Atom| isl(s n a)}
| t[] - >
|
| THM | j_idx_wf | f:Atom . s:Spec. x:Type. JIdx(x) |
| THM | comb_for_j_idx_wf | (f,s,x,z.JIdx(x)) f:(Atom ) s:Spec x:Type True |
| ML | j_idx_eval | let j_idx_boolC =
SimpleMacroC `j_idx_bool`
JIdx(boolean) Void ``type_cases bool_type j_idx``
;;
let j_idx_intC =
SimpleMacroC `j_idx_int`
JIdx(int) Void ``type_cases int_type j_idx``
;;
let j_idx_excC =
SimpleMacroC `j_idx_exc`
JIdx(Exception) Void ``type_cases exc_type j_idx``
;;
let j_idx_classC =
SimpleMacroC `j_idx_class`
JIdx(Class(n)) {a:Atom| isl(s n a)}
``type_cases class_type j_idx``
;;
let j_idx_arrayC =
SimpleMacroC `j_idx_array`
JIdx(t[]) ``type_cases array_type j_idx``
;;
let j_idxC =
FirstC [j_idx_boolC;
j_idx_intC;
j_idx_excC;
j_idx_classC;
j_idx_arrayC]
;;
add_AbReduce_conv `j_idx` j_idxC
;; |
| DISP | j_eq_idx_df | ( < i:idx:* > =i < j:idx:* > wrt < x:x:* > )== ( < i > =i < j > )
( < i:idx:* > =i < j:idx:* > )== ( < i > =i < j > ) |
| ABS | j_eq_idx | (i =i j) ==
case x
of bool - > tt
| int - > tt
| Exception - > tt
| Class(n) - > i =a j
| t[] - > (i = j)
|
| ML | j_eq_idx_eval | let j_eq_idx_boolC =
SimpleMacroC `j_eq_idx_bool`
(i =i j) tt ``type_cases bool_type j_eq_idx``;;
let j_eq_idx_intC =
SimpleMacroC `j_eq_idx_int`
(i =i j) tt ``type_cases int_type j_eq_idx``;;
let j_eq_idx_excC =
SimpleMacroC `j_eq_idx_exc`
(i =i j) tt ``type_cases exc_type j_eq_idx``;;
let j_eq_idx_classC =
SimpleMacroC `j_eq_idx_class`
(i =i j) i =a j ``type_cases class_type j_eq_idx``;;
let j_eq_idx_arrayC =
SimpleMacroC `j_eq_idx_array`
(i =i j) (i = j) ``type_cases array_type j_eq_idx``;;
let j_eq_idxC =
FirstC [j_eq_idx_boolC;
j_eq_idx_intC;
j_eq_idx_excC;
j_eq_idx_classC;
j_eq_idx_arrayC]
;;
add_AbReduce_conv `j_eq_idx` j_eq_idxC
;; |
| THM | j_eq_idx_wf | f:Atom . s:Spec. x:Type. i,j:JIdx(x). (i =i j) |
| THM | comb_for_j_eq_idx_wf | (f,s,x,i,j,z.(i =i j)) f:(Atom )
s:Spec
x:Type
i:JIdx(x)
j:JIdx(x)
True
|
| THM | assert_j_eq_idx | f:Atom . s:Spec. x:Type. i,j:JIdx(x). (i =i j) i = j |
| THM | j_eq_idx_refl | f:Atom . x:Type. s:Spec. i:JIdx(x). (i =i i) |
| THM | j_eq_idx_iff_eq | f:Atom . x:Type. s:Spec. i,j:JIdx(x). (i =i j) i = j |
| DISP | j_fld_df | Jfld( < x:type:* > . < i:idx:* > wrt < s:spec:* > )== Jfld( < x > . < i > )
Jfld( < x:type:* > . < i:idx:* > )== Jfld( < x > . < i > ) |
| ABS | j_fld | Jfld(x.i) ==
case x
of bool - > boolean
| int - > int
| Exception - > Exception
| Class(n) - > outl(s n i)
| t[] - > t
|
| ML | j_fld_eval | let j_fld_boolC =
SimpleMacroC `j_fld_bool`
Jfld(boolean.i) boolean ``type_cases bool_type j_fld``;;
let j_fld_intC =
SimpleMacroC `j_fld_int`
Jfld(int.i) int ``type_cases int_type j_fld``;;
let j_fld_excC =
SimpleMacroC `j_fld_exc`
Jfld(Exception.i) Exception ``type_cases exc_type j_fld``;;
let j_fld_classC =
SimpleMacroC `j_fld_class`
Jfld(Class(n).i) outl(s n i) ``type_cases class_type j_fld``;;
let j_fld_arrayC =
SimpleMacroC `j_fld_array`
Jfld(t[].i) t ``type_cases array_type j_fld``;;
let j_fldC =
FirstC [j_fld_boolC;
j_fld_intC;
j_fld_excC;
j_fld_classC;
j_fld_arrayC]
;;
add_AbReduce_conv `j_fld` j_fldC
;; |
| THM | j_fld_wf | f:Atom . s:Spec. x:Type. i:JIdx(x). Jfld(x.i) Type |
| DISP | j_sign_df | JSign( < f:f:* > ; < s:s:* > )== JSign( < f > ; < s > ) |
| ABS | j_sign | JSign(f;s) ==
< Type
, t.JCor(t)
, t.Jc
, t.JIdx(t)
, t,i.Jfld(t.i)
, t1,t2.(t1 =t t2)
, t1,c1,t2,c2.if (t1 =t t2) then (c1 =c c2) else ff fi
, t1,i1,t2,i2.if (t1 =t t2) then (i1 =i i2) else ff fi > |
| THM | j_sign_wf | f:Atom . s:Spec. JSign(f;s) Sign |
| THM | j_sign_reg | f:Atom . s:Spec. Reg(JSign(f;s)) |