COM	bar_primitives	The four basic primitives of the partial type library are: bar(T) the type containing elements of T and all divergent terms t in! T the assertion that t halts and t is in bar(T) T admissible the assertion that fixpoint induction may be performed over T T total the assertion that every element of T halts
DISP	bar	bar( < T:type:* > )== bar( < T > )
DISP	halt	Parens ::Prec(atomrel)::Index 0 :: {[SOFT} < e:term:L > {\\ }in! {- > 0} < T:type:L > { < -}{]} == < e > in! < T > Parens ::Prec(postop):: < e:term:E > halts== < e > halts
DISP	admiss	Parens ::Prec(postop):: < T:type:E > admissible== < T > admissible
DISP	total	Parens ::Prec(postop):: < T:Type:E > total== < T > total
COM	bar_com	We want to be able to form halting assertions t in! T whenever t is in bar(T). For this to be sound, T must not equate any convergent and divergent elements. We instead require the stronger condition that T contains only convergent elements. This seems to make things work out more nicely in practice.
RULE	barEquality	H bar(A) = bar(B) BY barEquality () H A = B H A total
RULE	barInclusion	H a = a' BY barInclusion level{i} H a = a' H bar(A) = bar(A)
RULE	bar_memberEquality	H a = a' BY bar_memberEquality level{i} z B C H a in! B a' in! C H, z:(a in! B) a = a' H bar(A)
COM	halt_com	We use a typed halting assertion t in! T rather than a simpler untyped halting condition for the following reason: For t in! T to be well-formed in a sequent, we need it to be functional over the hypotheses. With typed halting, we can simply require that t is in bar(T) and bar(T) is functional over the hypotheses. With untyped halting, we would have to show that t's halting behavior is functional over all the hypotheses, which would be impossible to ever prove.
RULE	haltEquality	H (a in! A) = (b in! B) BY haltEquality () H a = b H bar(A) = bar(B)
RULE	halt_axiomEquality	H Ax = Ax BY halt_axiomEquality () H a in! A
RULE	haltUniversal	H a in! A BY haltUniversal B H a in! B H a = a
RULE	termination	H a = b BY termination () H a in! A H a = b
RULE	member_termination	H a = a BY member_termination () H a in! A
COM	bottom_com	Introducing special rules for bottom are just for convenience. It would have been possible to prove the existence of a divergent term (say, the fixpoint of the flip function), which by bar_memberEquality would have been divergent in every bar type.
RULE	bottomEquality	H Y (x.x) = Y (x.x) BY bottomEquality level{i} H bar(A) = bar(A)
RULE	bottomDivergent	H Void BY bottomDivergent x A H Y (x.x) in! A
COM	total_com	Totality has to be primitive. If we tried to define it as T total iff x:bar(T). x in! T well-formedness would depend upon bar(T) being well-formed, which is only the case if T is total. This would make totality non-negatable.
RULE	totalEquality	H A total = B total BY totalEquality () H A = B
RULE	total_axiomEquality	H Ax = Ax BY total_axiomEquality () H A total
RULE	totality	H a in! A BY totality () H A total H a = a
COM	admiss_com	The admissibility assertion, T admissible, is true whenever fixpoint induction can be performed on T.
RULE	admissEquality	H A admissible = B admissible BY admissEquality () H A = B
RULE	admiss_axiomEquality	H Ax = Ax BY admiss_axiomEquality () H A admissible
COM	fixpoint_com	This is the critical rule to the theory of partial types, but semantically speaking it says nothing, since admissibility means that fixpoint induction may be performed. So this is just the elimination form for admissibility.
RULE	fixpoint_induction	H Y f = Y f BY fixpoint_induction () H f = f H A admissible
COM	totality_com	Most types are total. In particular, unions, products and functions are total since the intro forms are canonical and halt computation. This specifies that this is a lazy computation system. In an eager system computation would continue within product and union intros at least. Set and quotient types are total when their underlying types are.
RULE	voidTotal	H Void total BY voidTotal () No Subgoals
RULE	intTotal	H total BY intTotal () No Subgoals
RULE	atomTotal	H Atom total BY atomTotal () No Subgoals
RULE	equalityTotal	H (a1 = a2) total BY equalityTotal level{i} H (a1 = a2) = (a1 = a2)
RULE	unionTotal	H (A + B) total BY unionTotal level{i} H A + B = A + B
RULE	productTotal	H (x:A B) total BY productTotal level{i} H x:A B = x:A B
RULE	functionTotal	H (x:A B) total BY functionTotal level{i} H x:A B = x:A B
RULE	setTotal	H {x:A| B} total BY setTotal level{i} H A total H {x:A| B} = {x:A| B}
RULE	quotientTotal	H (x,y:A//B) total BY quotientTotal level{i} H A total H (x,y:A//B) = (x,y:A//B)
COM	admissibility_com	At present there are no rules showing admissibility for dependent products, sets or quotients, but we want some. The present situation is particularly unsatisfying since it makes it impossible to perform t he usual predicate fixpoint induction.
RULE	intAdmissible	H admissible BY intAdmissible () No Subgoals
RULE	atomAdmissible	H Atom admissible BY atomAdmissible () No Subgoals
RULE	equalityAdmissible	H (a1 = a2) admissible BY equalityAdmissible level{i} H (a1 = a2) = (a1 = a2)
RULE	unionAdmissible	H (A + B) admissible BY unionAdmissible () H A admissible H B admissible
RULE	functionAdmissible	H (x:A B) admissible BY functionAdmissible y H A admissible H, y:A B[y/x] admissible
RULE	prodAdmissible	H (A B) admissible BY prodAdmissible () H A admissible H B admissible
THM	total_wf	A:. A total
THM	bar_wf	A:. A total bar(A)
THM	halt_wf	A:. A total (a:bar(A). (a in! A) )
THM	admiss_wf	A:. A admissible
DISP	bottom_df	Bot== Bot
ABS	bottom	Bot == Y (x.x)
THM	bottom_wf	A:. A total Bot bar(A)
THM	bottom_diverge	A:. A total (Bot in! A)
COM	partial_term_com	For any strict n-place operator there will need to be n+2 partial term rules: 1) a rule for membership in the bar type op(t1, ..., tn) in bar(T) if for each i, ti in bar(Si) 2) a rule for halting op(t1, ..., tn) in! T if for each i, ti in! Si 3) n rules for inducement ti in! Si if op(t1, ..., tn) in! T None of these rules are derivable from the original typing rule op(t1, ..., tn) in T if for each i, ti in Si but the original typing rule is derivable from the halting rule and the totality and member_termination rules, so long as each Si is total. If op is nonstrict in position k, the kth subgoal of the halting rule would be dropped, as well as the kth inducement rule. At present, partial term rules are only in place for subtraction. They need to be put in for every operator.
RULE	subtract_barEquality	H m1 - n1 = m2 - n2 BY subtract_barEquality () H m1 = m2 H n1 = n2
RULE	subtractHalt	H (e1 - e2) halts BY subHalt () H e1 halts H e2 halts
RULE	subtractInduceLeft	H e1 halts BY subInduceLeft e2 H (e1 - e2) halts H e1 = e1
RULE	subtractInduceRight	H e2 halts BY subInduceRight e1 H (e1 - e2) halts
RULE	apply_barEquality	H f1 a1 = f2 a2 BY apply_barEquality x:A bar(B) H f1 = f2 H a1 = a2
RULE	applyInduceArg	H a in! A BY applyInduceArg (x:A B) f H f a in! B[a/x] H a = a
ML	ApplyInduceArg	let ApplyInduceArg B f = Refine `applyInduceArg` [mk_term_arg B; mk_term_arg f] THENL [Reduce 0; FoldTop `member` 0 THEN AddHiddenLabel `wf`];;
RULE	decide_barEquality	H case e1 of inl(x1) = > l1 | inr(y1) = > r1 = case e2 of inl(x2) = > l2 | inr(y2) = > r2 BY decide_barEquality z bar(T) bar(A + B) u v w H e1 = e2 H, u:A, w:(e1 = (inl u )) l1[u/x1] = l2[u/x2] H, v:B, w:(e1 = (inr v )) r1[v/y1] = r2[v/y2]
RULE	spread_barEquality	H let < x1,y1 > = e1 in t1 = let < x2,y2 > = e2 in t2 BY spread_barEquality z bar(T) bar(w:A B) u v a H e1 = e2 H, u:A, v:B[u/w], a:(e1 = < u, v > ) t1[u,v/x1,y1] = t2[u,v/x2,y2]
RULE	spreadInduce	H a in! A BY spreadInduce x y b B H let < x,y > = a in b in! B H a = a
ML	SpreadInduce	let SpreadInduce x y b B = Refine `spreadInduce` [mk_var_arg x; mk_var_arg y; mk_term_arg b; mk_term_arg B] THENL [Reduce 0; FoldTop `member` 0 THEN AddHiddenLabel `wf`] ;;
ML	bar_eq_tac	let EqCDBar p = let T,t,t' = dest_equal (concl p) in let opid = opid_of_term t in if not opid = opid_of_term t' then failwith `EqCDBar: outermost constructors do not match` else if opid_of_term T = `bar` then if opid = `decide` then let [(),a; [x],(); [y],()] = bterms_of_term t in let using_term = get_using_type p a in let z,over_term = get_over_pair t T in let new_var_args = mk_new_var_args [[x];[y];[]] p in Refine `decide_barEquality` (mk_bterm_arg [z] over_term . mk_term_arg (mk_std_term `bar` [[],using_term]) . new_var_args ) p else if opid = `spread` then let [(),a; [x;y],()] = bterms_of_term t in let using_term = get_using_type p a in let z,over_term = get_over_pair t T in let new_var_args = mk_new_var_args [[x];[y];[]] p in message (term_to_string using_term); Refine `spread_barEquality` (mk_bterm_arg [z] over_term . mk_term_arg using_term % (mk_std_term `bar` [[],using_t erm])% . new_var_args ) p else failwith `EqCDBar : unknown opid` else failwith `EqCDBar : not a bar type` ;; update_EqCD_additions `EqCDBar` EqCDBar;; let MemCDBar = Unfold `member` 0 THEN EqCDBar THEN Fold `member` 0 ;; let CDBar = EqCDBar ORELSE MemCDBar ;;
ML	auto_t	let AutoT = Auto THEN Try Termination THEN Auto;;
THM	bar_eq_lemma	T:. T total (x,y:bar(T). x = y x in! T x = y)
THM	bar_eq_lemma_rev	T:. T total (x,y:bar(T). x = y y in! T x = y)

the other theories