DISP	j_class_name_df	JClassName( < f:f:* > )== JClassName( < f > )
ABS	j_class_name	JClassName(f) == {a:Atom| (f a)}
THM	j_class_name_wf	f:Atom . JClassName(f)
DISP	type_df	Type( < f:f:* > )== Type Type== Type
ABS	type	Type == rec(T.Unit + Unit + Unit + JClassName(f) + T)
THM	type_wf	f:Atom . Type
DISP	bool_type_df	boolean== boolean
ABS	bool_type	boolean == inl
THM	bool_type_wf	f:Atom . boolean Type
DISP	int_type_df	int== int
ABS	int_type	int == inr (inl )
THM	int_type_wf	f:Atom . int Type
DISP	exc_type_df	Exception== Exception
ABS	exc_type	Exception == inr inr (inl )
THM	exc_type_wf	f:Atom . Exception Type
DISP	class_type_df	Class( < n:n:* > )== Class( < n > )
ABS	class_type	Class(n) == inr inr inr (inl n )
THM	class_type_wf	f:Atom . n:JClassName(f). Class(n) Type
THM	comb_for_class_type_wf	(f,n,z.Class(n)) f:(Atom ) n:JClassName(f) True Type
DISP	array_type_df	< t:j_type:* > []== < t > []
ABS	array_type	t[] == inr inr inr inr t
THM	array_type_wf	f:Atom . t:Type. t[] Type
THM	comb_for_array_type_wf	(f,t,z.t[]) f:(Atom ) t:Type True Type
ML	type_hd	let TypeHD i = MoveDepHypsToConcl i THEN D i THEN Fold `type` i THEN D (-2) THEN D (-2) THENL [Fold `it` 0 THEN Fold `bool_type` 0 THEN Thin (-1) THEN Thin (-1); D (-2) THEN Fold `it` 0 THEN Fold `int_type` 0 T HEN Thin (-1) THEN Thin (-1); D (-2) THEN D (-2)] THENL [Id; Id; D (-2 ) THEN Fold `it` 0 THEN Fold `exc_type` 0 THEN Thin (-1) THEN Thin (-1 ); Fold `class_type` (-1) THEN Fold `class_type` 0 THEN RenameVarUsing Arg `x` `n' (-2); Fold `array_type` (-1) THEN Fold `array_type` 0 THEN RenameVarUsingArg `y` `t' (-2)];;
DISP	type_cases_df	{[SOFT}{- > 0}case < x:j_type:* > {\\}of bool - > < b:term:* > {\\} | int - > < z:term:* > {\\} | Exception - > < e:term:* > {\\} | Class( < n:var > ) - > < c:term:* > {\\} | < t:var > [] - > < a:term:* > {\\}{ < -}{]} == case < x > of bool - > < b > | int - > < z > | Exception - > < e > | Class( < n > ) - > < c > | < t > [] - > < a >
ABS	type_cases	case x of bool - > b | int - > z | Exception - > e | Class(n) - > c[n] | t[] - > a[t] == case x of inl(x1) = > b | inr(x2) = > case x2 of inl(x3) = > z | inr(x4) = > case x4 of inl(x5) = > e | inr(x6) = > case x6 of inl(n) = > c[n] | inr(t) = > a[t]
ML	type_cases_eval	let type_cases_boolC = SimpleMacroC `type_cases_bool` case boolean of bool - > b | int - > z | Exception - > e | Class(n) - > c[n] | t[] - > a[t] b ``type_cases bool_type`` ;; let type_cases_intC = SimpleMacroC `type_cases_int` case int of bool - > b | int - > z | Exception - > e | Class(n) - > c[n] | t[] - > a[t] z ``type_cases int_type`` ;; let type_cases_excC = SimpleMacroC `type_cases_exc` case Exception of bool - > b | int - > z | Exception - > e | Class(n) - > c[n] | t[] - > a[t] e ``type_cases exc_type`` ;; let type_cases_classC = SimpleMacroC `type_cases_class` case Class(k) of bool - > b | int - > z | Exception - > e | Class(n) - > c[n] | t[] - > a[t] c[k] ``type_cases class_type`` ;; let type_cases_arrayC = SimpleMacroC `type_cases_array` case s[] of bool - > b | int - > z | Exception - > e | Class(n) - > c[n] | t[] - > a[t] a[s] ``type_cases array_type`` ;; let type_casesC = FirstC [type_cases_boolC; type_cases_intC; type_cases_excC; type_cases_classC; type_cases_arrayC] ;; add_AbReduce_conv `type_cases` type_casesC ;;
THM	type_cases_wf	f:Atom . T:. x:Type. b,z,e:T. c:JClassName(f) T. a:Type T. case x of bool - > b | int - > z | Exception - > e | Class(n) - > c[n] | t[] - > a[t] T
ML	type_ind	let TypeInd i = AbRecTypeInd i THENM (D (-1) THEN D (-1) THENL [Fold ` it` 0 THEN Fold `bool_type` 0 THEN Thin (-1) THEN Thin (-1) THEN Thin  (-1); D (-1) THEN Fold `it` 0 THEN Fold `int_type` 0 THEN Thin (-1) TH EN Thin (-1) THEN Thin (-1); D (-1) THEN D (-1)] THENL [Id; Id; Fold ` it` 0 THEN Fold `exc_type` 0 THEN Thin (-1) THEN Thin (-1) THEN Thin ( -1) ; Fold `class_type` 0 THEN Thin (-2) THEN Thin (-2); Fold `array_ type` 0 THEN (\p. (With (mvt (var_of_hyp (-1) p)) (D (-2))) p) THENM D (-2) THENM Thin (-2) THENM Thin (-3)]);;
DISP	eq_type_df	( < x:j_type:* > =t < y:j_type:* > )== ( < x > =t < y > )
ML	eq_type_ml	(x =t y) ==r case x of bool - > case y of bool - > tt | int - > ff | Exception - > ff | Class(n) - > ff | t[] - > ff | int - > case y of bool - > ff | int - > tt | Exception - > ff | Class(n) - > ff | t[] - > ff | Exception - > case y of bool - > ff | int - > ff | Exception - > tt | Class(n) - > ff | t[] - > ff | Class(n) - > case y of bool - > ff | int - > ff | Exception - > ff | Class(m) - > n =a m | t[] - > ff | t[] - > case y of bool - > ff | int - > ff | Exception - > ff | Class(n) - > ff | s[] - > (t =t s)
THM	eq_type_wf	f:Atom . x,y:Type. (x =t y)
ML	eq_type_eval	let eq_type_int_intC = MacroC `eq_type_int_intV` (RecUnfoldC `eq_type` ANDTHENC AbRedexC ANDTHENC AbRedexC) (int =t int) IdC tt ;; let eq_typeC = FirstC [eq_type_int_intC;] ;; add_AbReduce_conv `eq_type` eq_typeC ;;
THM	comb_for_eq_type_wf	(f,x,y,z.(x =t y)) f:(Atom ) x:Type y:Type True
THM	assert_of_eq_type	f:Atom . x,y:Type. (x =t y) x = y
THM	eq_type_refl	f:Atom . x:Type. (x =t x)
THM	eq_type_iff_eq	f:Atom . x,y:Type. (x =t y) x = y
DISP	spec_df	Spec( < f:f:* > )== Spec Spec== Spec
ABS	spec	Spec == JClassName(f) Atom ?Type
ML	spec_soft	add_soft_abs ``spec``;;

the other theories