% @(#)$Id: WithUnassigned.proof,v 1.2 1997/02/13 00:21:26 leavens Exp $ set script WithUnassigned set log WithUnassigned %%% Proof Obligations for trait WithUnassigned execute WithUnassigned_Axioms %% Implications declare variables tval: T .. % main trait: WithUnassigned set name WithUnassignedTheorem prove (injectTVal(extractTVal(injectTVal(tval)))) = (injectTVal(tval)) .. [] conjecture qed %% Conversions freeze WithUnassigned %% converts isUnassigned, extractTVal exempting extractTVal(unassigned) thaw WithUnassigned declare operators extractTVal': WithUnassigned[T] -> T , isUnassigned': WithUnassigned[T] -> Bool .. % subtrait 0: WithUnassigned (isUnassigned': WithUnassigned[T] -> Bool for % isUnassigned: WithUnassigned[T] -> Bool, extractTVal': WithUnassigned[T] % -> T for extractTVal: WithUnassigned[T] -> T) set name WithUnassigned assert sort WithUnassigned[T] partitioned by isUnassigned', extractTVal' ;(extractTVal'(injectTVal(tval))) = (tval) ;(~ isUnassigned'(injectTVal(tval))) ;(isUnassigned'(unassigned)) .. declare variables _x1_: WithUnassigned[T] .. set name exemptions assert extractTVal(unassigned) = extractTVal'(unassigned) .. set name conversionChecks prove (isUnassigned(_x1_)) = (isUnassigned'(_x1_)) by ind <> basis subgoal [] basis subgoal <> basis subgoal [] basis subgoal [] conjecture qed prove (extractTVal(_x1_)) = (extractTVal'(_x1_)) by ind <> basis subgoal [] basis subgoal <> basis subgoal [] basis subgoal [] conjecture qed