| DISP | class_df |  ( < s:sign:* > @ < n:nam:* > )== @ < n >
@ < n:n:* > == @ < n > |
| ABS | class | @n ==
parec(C,j.{k:Nam| k = j} + k:Nam  C k Cor k C j + k:Nam
C k
i:Idx k
C (Fld k i)
C j @ n) |
| THM | class_wf |  s:Sign. n:Nam. @n   |
| DISP | nil_object_df |  ( < k:nam:* > )== ( < k > ) |
| ABS | nil_object | (k) == inl k |
| THM | nil_object_wf | s:Sign. n,k:Nam. k = n   (k) @n |
| DISP | cor_update_df | [core( < x:object:* > :@ < k:nam:* > ):= < t:cor:* > @ < y:object:* > ]
== [core( < x > :@ < k > ):= < t > @ < y > ] |
| ABS | cor_update | [core(x:@k):=t@y] == inr (inl < k, x, t, y > ) |
| THM | cor_update_wf | s:Sign. n,k:Nam. x:@k. t:Cor k. y:@n. [core(x:@k):=t@y] @n |
| DISP | ref_update_df | [( < x:object:* > :@ < k:nam:* > ). < i:i:* > := < z:object:* > @ < y:object:* > ]
== [( < x > :@ < k > ). < i > := < z > @ < y > ] |
| ABS | ref_update | [(x:@k).i:=z@y] == inr inr < k, x, i, z, y > |
| THM | ref_update_wf | s:Sign. n,k:Nam. x:@k. i:Idx k. z:@Fld k i. y:@n.
[(x:@k).i:=z@y] @n |
| DISP | object_cases_df | {[SOFT}{- > 0}case < o:object:* > {\\}
of ( < n:var > ) - > < base_case:base_case:* > {\\}
| [core( < x:var > :@ < k:var > ):= < t:var > @ < y:var > ] - >
< cor_case:cor_case:* > {\\}
| [( < u:var > :@ < m:var > ). < i:var > := < v:var > @ < w:var > ] - >
< ref_case:ref_case:* > {\\}
{ < -}{]})
== case < o >
of ( < n > ) - > < base_case >
| [core( < x > :@ < k > ):= < t > @ < y > ] - > < cor_case >
| [( < u > :@ < m > ). < i > := < v > @ < w > ] - > < ref_case >
) |
| ABS | object_cases | case o
of (n) - > base_case[n]
| [core(x:@k):=t@y] - > cor_case[k; x; t; y]
| [(u:@m).i:=v@w] - > ref_case[m; u; i; v; w]
) ==
case o
of inl(n) = > base_case[n]
| inr(cr) = > case cr
of inl(c) = > let < k,xty > = c
in
let < x,ty > = xty
in
let < t,y > = ty in cor_case[k; x; t; y]
| inr(r) = > let < m,uivw > = r
in
let < u,ivw > = uivw
in
let < i,vw > = ivw
in
let < v,w > = vw in ref_case[m; u; i; v; w] |
| THM | object_cases_wf | T:. s:Sign. n:Nam. o:@n. base_case:k:Nam   T.
cor_case:k:Nam @k Cor k @n T. ref_case:k:Nam
@k
i:Idx k
@Fld k i
@n
T.
case o
of (k) - > base_case[k]
| [core(x:@k):=t@y] - > cor_case[k;x;t;y]
| [(x:@k).i:=z@y] - > ref_case[k;x;i;z;y]
) T |
| ML | object_cases_eval | let object_cases_baseC =
SimpleMacroC `object_cases_base`
 case (k)
of (k) - > base_case[k]
| [core(x:@k):=t@y] - > cor_case[k; x; t; y]
| [(x:@k).i:=z@y] - > ref_case[k; x; i; z; y]
) base_case[k] ``object_cases nil_object``
;;
let object_cases_corC =
SimpleMacroC `object_cases_cor`
case [core(x:@k):=t@y]
of (k) - > base_case[k]
| [core(x:@k):=t@y] - > cor_case[k; x; t; y]
| [(x:@k).i:=z@y] - > ref_case[k; x; i; z; y]
) cor_case[k; x; t; y] ``object_cases cor_update``
;;
let object_cases_refC =
SimpleMacroC `object_cases_ref`
case [(x:@k).i:=z@y]
of (k) - > base_case[k]
| [core(x:@k):=t@y] - > cor_case[k; x; t; y]
| [(x:@k).i:=z@y] - > ref_case[k; x; i; z; y]
) ref_case[k; x; i; z; y] ``object_cases ref_update``
;;
let object_casesC =
FirstC [object_cases_baseC;
object_cases_corC;
object_cases_refC]
;;
add_AbReduce_conv `object_cases` object_casesC
;;
|
| ML | fix_varname | let RenameVarUsingArg argname default i p =
let v = get_var_arg argname p
? maybe_new_var default (declared_vars p)
in
RenameVar v i p
;; |
| THM | class_ind_tp | s:Sign. P:n:Nam @n  .
(n,k:Nam. k = n P[n;(k)])
(n,k:Nam. x:@k. t:Cor k. y:@n.
P[k;x] P[n;y] P[n;[core(x:@k):=t@y]])
(n,k:Nam. x:@k. i:Idx k. z:@Fld k i. y:@n.
P[k;x] P[Fld k i;z] P[n;y] P[n;[(x:@k).i:=z@y]])
{n:Nam. o:@n. P[n;o]} |
| ML | class_ind_tac | let ClassInd i j p = ByAnalogyWith1 `class_ind_tp`
[`hr_n`, int_to_arg i;
`hr_o`, int_to_arg j] p
;;
let ClassIndG i j = FoldTop `guard` 0 THEN
ClassInd i j THENM
UnfoldTop `guard` 0
;; |
| DISP | nam_df | nam( < o:object:* > )== nam( < o > ) |
| ML | nam_ml | nam(o)
==r case o
of (k) - > k
| [core(x:@k):=t@y] - > nam(y)
| [(x:@k).i:=z@y] - > nam(y)
) |
| THM | nam_wf | s:Sign. n:Nam. o:@n. nam(o) Nam |
| THM | nam_sound | s:Sign. n:Nam. o:@n. nam(o) = n |
| THM | nam_sound_mem | s:Sign. n:Nam. x:@n. x @nam(x) |
| DISP | eq_obj_df | ( < o1:object:* > = < o2:object:* > wrt < s:sign:* > )== ( < o1 > = < o2 > )
( < o1:object:* > = < o2:object:* > )== ( < o1 > = < o2 > ) |
| ML | eq_obj_ml |
(o1=o2)
==r case o1
of (k1) - > case o2
of (k2) - > (k1 = k2)
| [core(x2:@k2):=t2@y2] - > ff
| [(x2:@k2).i2:=z2@y2] - > ff
)
| [core(x1:@k1):=t1@y1] - > case o2
of (k2) - > ff
| [core(x2:@k2):=t2@y2] - > (k1
= k2)
  (x1=x2)
(t1 = t2)
(y1=y2)
| [(x2:@k2).i2:=z2@y2] - > ff
)
| [(x1:@k1).i1:=z1@y1] - > case o2
of (k2) - > ff
| [core(x2:@k2):=t2@y2] - > ff
| [(x2:@k2).i2:=z2@y2] - > (k1 =
k2)
(x1=x2)
(i1 = i2)
(z1=z2)
(y1=y2)
)
) |
| THM | eq_obj_wf | s:Sign. n:Nam. x:@n. k:Nam. y:@k. (x=y)  |
| ML | eq_obj_eval | let eq_obj_nil_nilC = MacroC `eq_obj_nil_nilC`
(RecUnfoldC `eq_obj` ANDTHENC AbRedexC ANDTHENC AbRedexC)
((n1)=(n2)) IdC (n1 = n2)
;;
let eq_obj_nil_corC = MacroC `eq_obj_nil_corC`
(RecUnfoldC `eq_obj` ANDTHENC AbRedexC ANDTHENC AbRedexC)
((n1)=[core(x:@k):=t@y]) IdC ff
;;
let eq_obj_nil_refC = MacroC `eq_obj_nil_refC`
(RecUnfoldC `eq_obj` ANDTHENC AbRedexC ANDTHENC AbRedexC)
((n1)=[(x:@k).i:=z@y]) IdC ff
;;
let eq_obj_cor_nilC = MacroC `eq_obj_cor_nilC`
(RecUnfoldC `eq_obj` ANDTHENC AbRedexC ANDTHENC AbRedexC)
([core(x:@k):=t@y]=(n)) IdC ff
;;
let eq_obj_cor_corC = MacroC `eq_obj_cor_corC`
(RecUnfoldC `eq_obj` ANDTHENC AbRedexC ANDTHENC AbRedexC)
([core(x1:@k1):=t1@y1]=[core(x2:@k2):=t2@y2]) IdC
(k1 = k2) (x1=x2) (t1 = t2) (y1=y2)
;;
let eq_obj_cor_refC = MacroC `eq_obj_cor_refC`
(RecUnfoldC `eq_obj` ANDTHENC AbRedexC ANDTHENC AbRedexC)
([core(x1:@k1):=t1@y1]=[(x2:@k2).i:=z2@y2]) IdC ff
;;
let eq_obj_ref_nilC = MacroC `eq_obj_ref_nilC`
(RecUnfoldC `eq_obj` ANDTHENC AbRedexC ANDTHENC AbRedexC)
([(x:@k).i:=z@y]=(n)) IdC ff
;;
let eq_obj_ref_corC = MacroC `eq_obj_ref_corC`
(RecUnfoldC `eq_obj` ANDTHENC AbRedexC ANDTHENC AbRedexC)
([(x1:@k1).i1:=z1@y1]=[core(x2:@k2):=t2@y2]) IdC ff
;;
let eq_obj_ref_refC = MacroC `eq_obj_ref_refC`
(RecUnfoldC `eq_obj` ANDTHENC AbRedexC ANDTHENC AbRedexC)
([(x1:@k1).i1:=z1@y1]=[(x2:@k2).i2:=z2@y2]) IdC (k1 = k2)
(x1=x2)
(i1 = i2)
(z1=z2)
(y1=y2)
;;
let eq_objC =
FirstC [eq_obj_nil_nilC; eq_obj_nil_corC; eq_obj_nil_refC;
eq_obj_cor_nilC; eq_obj_cor_corC; eq_obj_cor_refC;
eq_obj_ref_nilC; eq_obj_ref_corC; eq_obj_ref_refC;]
;;
add_AbReduce_conv `eq_obj` eq_objC
;; |
| THM | eq_obj_imp_eq_nam | s:Sign. n:Nam. x:@n. k:Nam. y:@k. Reg(s)  (x=y) n = k |
| THM | par_type_lemma | T:. F:T . t,t':T. f:F[t]. t = t' f F[t'] |
| DISP | cor_df | cor( < o:obj:* > wrt < s:sign:* > )== cor( < o > )
cor( < o:obj:* > )== cor( < o > ) |
| ML | cor_ml | cor(o)
==r case o
of (n) - > cor n
| [core(x:@k):=t@y] - > if (x=y) then t else cor(y) fi
| [(x:@k).i:=z@y] - > cor(y)
) |
| THM | cor_wf | s:Sign. n:Nam. o:@n. Reg(s) cor(o) Cor n |
| DISP | ref_df | ( < o:obj:* > :( < s:sign:* > @ < n:nam:* > ). < i:idx:* > == < o > . < i >
< o:obj:* > . < i:idx:* > == < o > . < i > |
| ML | ref_ml | o.i
==r case o
of (k) - > (Fld k i)
| [core(x:@k):=t@y] - > [core(x:@k):=t@y.i]
| [(x:@k).j:=z@y] - > if (x=y) (j = i)
then [(x:@k).j:=z@z]
else [(x:@k).j:=z@y.i]
fi
) |
| THM | ref_wf | s:Sign. n:Nam. o:@n. i:Idx n. Reg(s) o.i @Fld n i |
| DISP | c_update_df | [cor( < x:object:* > ):= < t:cor:* > @ < y:object:* > ]== [cor( < x > ):= < t > @ < y > ] |
| ABS | c_update | [cor(x):=t@y] == [core(x:@nam(x)):=t@y] |
| THM | c_update_wf | s:Sign. n,k:Nam. x:@k. t:Cor k. y:@n. [cor(x):=t@y] @n |
| DISP | r_update_df | [ < x:object:* > . < i:idx:* > := < z:object:* > @ < y:object:* > ]
== [ < x > . < i > := < z > @ < y > ] |
| ABS | r_update | [x.i:=z@y] == [(x:@nam(x)).i:=z@y] |
| THM | r_update_wf | s:Sign. n,k:Nam. x:@k. i:Idx k. z:@Fld k i. y:@n.
[x.i:=z@y] @n |
| ML | nam_eval | let nam_of_nil_objectC =
MacroC `nam_of_nil_objectC`
(RecUnfoldC `nam` ANDTHENC AbRedexC)
nam((n)) IdC n
;;
let nam_of_cor_updateC =
MacroC `nam_of_cor_updateC`
(RecUnfoldC `nam` ANDTHENC AbRedexC)
nam([core(x:@k):=t@y]) IdC nam(y)
;;
let nam_of_ref_updateC =
MacroC `nam_of_ref_updateC`
(RecUnfoldC `nam` ANDTHENC AbRedexC)
nam([(x:@k).i:=z@y]) IdC nam(y)
;;
let nam_of_c_updateC =
MacroC `nam_of_c_updateC`
(UnfoldC `c_update` ANDTHENC
RecUnfoldC `nam`
ANDTHENC AbRedexC)
nam([cor(x):=t@y]) IdC nam(y)
;;
let nam_of_r_updateC =
MacroC `nam_of_r_updateC`
(UnfoldC `r_update` ANDTHENC
RecUnfoldC `nam`
ANDTHENC AbRedexC)
nam([x.i:=z@y]) IdC nam(y)
;;
let namC =
nam_of_nil_objectC ORELSEC
nam_of_cor_updateC ORELSEC
nam_of_c_updateC ORELSEC
nam_of_ref_updateC ORELSEC
nam_of_r_updateC
;;
add_AbReduce_conv `nam` namC;; |
| DISP | get_ref_df | get_ref( < o:o:* > ; < i:i:* > ; < s:s:* > )== get_ref( < o > ; < i > ; < s > ) |
| ABS | get_ref | get_ref(o;i;s) == o.i |
| THM | get_ref_wf | s:Sign. n:Nam. o:@n. i:Idx n.
Reg(s) get_ref(o;i;s) @Fld nam(o) i |
| THM | get_ref_wf_2 | s:Sign. n:Nam. o:@n. i:Idx n.
Reg(s) get_ref(o;i;s) @Fld n i |
| THM | comb_for_class_wf | ( s,n,z.@n) s:Sign n:Nam  True |