Module exactEval:condExpr
Builds on exactEval:host
expr ::= ...
| condExpr(expr, expr, expr) /*condExpr(C, T, F): C ? T : F*/
fresh_name "X" Names X
------------------------------------------------ [Proj-ConditionalExpr]
Names |{expr}- condExpr(C, T, F) ~~>
stmtExpr(
seq(declare(intTy, X, num(0)),
ifThenElse(C,
assign(X, T),
assign(X, F))),
name(X))
vars C V1
vars T V2
vars F V3
V1 ++ V2 = V4
V4 ++ V3 = V
------------------------ [V-ConditionalExpr]
vars condExpr(C, T, F) V
exprNames Ctx C CN
exprNames Ctx T TN
exprNames Ctx F FN
CN ++ TN = N1
N1 ++ FN = N
--------------------------------- [EN-ConditionalExpr]
exprNames Ctx condExpr(C, T, F) N
typeOf FT ET C boolTy
typeOf FT ET T Ty
typeOf FT ET F Ty
--------------------------------- [T-ConditionalExpr]
typeOf FT ET condExpr(C, T, F) Ty
evalExpr FE EE C trueVal EE1 O1
evalExpr FE EE1 T V EE2 O2
O1 ++ O2 = O
---------------------------------------- [E-ConditionalExpr-True]
evalExpr FE EE condExpr(C, T, F) V EE2 O
evalExpr FE EE C falseVal EE1 O1
evalExpr FE EE1 F V EE2 O2
O1 ++ O2 = O
---------------------------------------- [E-ConditionalExpr-False]
evalExpr FE EE condExpr(C, T, F) V EE2 O
Click on a command or tactic to see a detailed view of its use.
Module exactEval:condExpr. /******************************************************************** Basic Projection Constraints ********************************************************************/ Prove_Constraint exactEval:host:proj_expr_unique. [Show Proof] Prove_Constraint exactEval:host:proj_expr_is. [Show Proof] Prove_Constraint exactEval:host:proj_expr_other. [Show Proof] Prove_Constraint exactEval:host:proj_stmt_unique. Prove_Constraint exactEval:host:proj_stmt_is. Prove_Constraint exactEval:host:proj_stmt_other. Prove_Constraint exactEval:host:proj_fun_unique. Prove_Constraint exactEval:host:proj_fun_is. Prove_Constraint exactEval:host:proj_param_unique. Prove_Constraint exactEval:host:proj_param_is. Prove_Constraint exactEval:host:proj_program_unique. Prove_Constraint exactEval:host:proj_program_is. Prove_Constraint exactEval:host:proj_typ_unique. Prove_Constraint exactEval:host:proj_typ_is. /******************************************************************** Decidable Equality ********************************************************************/ Add_Proj_Rel exactEval:host:is_expr, exactEval:host:is_args, exactEval:host:is_recFieldExprs, exactEval:host:is_stmt. Prove_Ext_Ind exactEval:host:is_expr, exactEval:host:is_args, exactEval:host:is_recFieldExprs, exactEval:host:is_stmt. [Show Proof] Prove exactEval:host:is_args_nilArgs_or_consArgs. Prove exactEval:host:is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs. /******************************************************************** Variables ********************************************************************/ Prove exactEval:host:vars_unique. [Show Proof] Prove exactEval:host:vars_is. [Show Proof] Prove exactEval:host:vars_exist, exactEval:host:varsArgs_exist, exactEval:host:varsRecFields_exist. [Show Proof] /******************************************************************** Statement Names ********************************************************************/ Prove exactEval:host:stmtNames_is, exactEval:host:stmtNames_isCtx, exactEval:host:exprNames_is. [Show Proof] Prove exactEval:host:stmtNames_unique, exactEval:host:exprNames_unique. [Show Proof] Prove exactEval:host:stmtNames_keep_older. Prove exactEval:host:stmtNames_exists, exactEval:host:exprNames_exists, exactEval:host:argsNames_exists, exactEval:host:recFieldNames_exists. [Show Proof] Prove exactEval:host:stmtNames_not_in_ctx, exactEval:host:exprNames_not_in_ctx. [Show Proof] Prove exactEval:host:stmtNames_relatedCtxs, exactEval:host:stmtNames_relatedCtxs_ctx_fwd, exactEval:host:stmtNames_relatedCtxs_ctx_back, exactEval:host:exprNames_relatedCtxs. [Show Proof] Prove exactEval:host:stmtNames_increaseCtxs, exactEval:host:stmtNames_increaseCtxs_ctxs, exactEval:host:exprNames_increaseCtxs. [Show Proof] Prove_Constraint exactEval:host:proj_exprNames. [Show Proof] Prove_Constraint exactEval:host:proj_stmtNames. Prove_Constraint exactEval:host:proj_stmtNames_names_forward. Prove_Constraint exactEval:host:proj_stmtNames_names_backward. /******************************************************************** Typing ********************************************************************/ Prove exactEval:host:typeOf_isTy, exactEval:host:stmtOK_isCtx. [Show Proof] Prove exactEval:host:stmtOK_keep_scopes. Prove exactEval:host:stmtOK_older_scopes_same. Prove exactEval:host:stmtOK_first_scope_lookup_same. Prove exactEval:host:typeOf_unique, exactEval:host:stmtOK_unique. [Show Proof] Prove exactEval:host:paramTy_is. Prove exactEval:host:getFunInfo_is. Prove exactEval:host:paramTy_exists. Prove exactEval:host:getFunInfo_exists. /******************************************************************** Evaluation ********************************************************************/ Prove exactEval:host:evalExpr_isCtx, exactEval:host:evalExpr_isValue, exactEval:host:evalStmt_isCtx, exactEval:host:evalArgs_isCtx, exactEval:host:evalArgs_isValue, exactEval:host:evalRecFields_isCtx, exactEval:host:evalRecFields_isValue. [Show Proof] Prove exactEval:host:evalExpr_isOutput, exactEval:host:evalStmt_isOutput, exactEval:host:evalArgs_isOutput, exactEval:host:evalRecFields_isOutput. [Show Proof] Prove exactEval:host:paramName_is. Prove exactEval:host:getFunEvalInfo_is. Prove exactEval:host:evalProgram_isOutput. Prove exactEval:host:evalExpr_names_same, exactEval:host:evalStmt_names_same, exactEval:host:evalArgs_names_same, exactEval:host:evalRecFields_names_same. [Show Proof] Prove exactEval:host:evalExpr_newNameScopes, exactEval:host:evalExpr_newNameScopes_output, exactEval:host:evalExpr_newNameScopes_ctx, exactEval:host:evalStmt_newNameScopes_output, exactEval:host:evalStmt_newNameScopes, exactEval:host:evalArgs_newNameScopes, exactEval:host:evalArgs_newNameScopes_output, exactEval:host:evalArgs_newNameScopes_ctx, exactEval:host:evalRecFields_newNameScopes, exactEval:host:evalRecFields_newNameScopes_output, exactEval:host:evalRecFields_newNameScopes_ctx. [Show Proof] Add_Ext_Size exactEval:host:evalExpr, exactEval:host:evalArgs, exactEval:host:evalRecFields, exactEval:host:evalStmt. Add_Proj_Rel exactEval:host:evalExpr, exactEval:host:evalArgs, exactEval:host:evalRecFields, exactEval:host:evalStmt. Prove exactEval:host:evalExpr_newNameScopes_exists_ES, exactEval:host:evalStmt_newNameScopes_exists_ES, exactEval:host:evalArgs_newNameScopes_exists_ES, exactEval:host:evalRecFields_newNameScopes_exists_ES. [Show Proof] Prove exactEval:host:evalExpr_ctx_names, exactEval:host:evalStmt_ctx_names, exactEval:host:evalArgs_ctx_names, exactEval:host:evalRecFields_ctx_names. [Show Proof] Prove exactEval:host:evalExpr_newNameScopes_exists_back, exactEval:host:evalStmt_newNameScopes_exists_back, exactEval:host:evalArgs_newNameScopes_exists_back, exactEval:host:evalRecFields_newNameScopes_exists_back. [Show Proof] Theorem append_values_total : forall LA LB, is_list is_value LA -> exists L, LA ++ LB = L. [Show Proof] Prove exactEval:host:evalExpr_scopes_same, exactEval:host:evalExpr_scopes_same_ctx, exactEval:host:evalStmt_scopes_same, exactEval:host:evalStmt_scopes_same_ctx, exactEval:host:evalArgs_scopes_same, exactEval:host:evalArgs_scopes_same_ctx, exactEval:host:evalRecFields_scopes_same, exactEval:host:evalRecFields_scopes_same_ctx. [Show Proof] Prove exactEval:host:evalExpr_scopes_same_exists, exactEval:host:evalStmt_scopes_same_exists, exactEval:host:evalArgs_scopes_same_exists, exactEval:host:evalRecFields_scopes_same_exists. [Show Proof] Prove_Constraint exactEval:host:proj_evalExpr_forward. [Show Proof] Prove_Constraint exactEval:host:proj_evalExpr_backward. [Show Proof] Prove_Constraint exactEval:host:proj_evalStmt_forward. Prove_Constraint exactEval:host:proj_evalStmt_backward. Prove_Ext_Ind exactEval:host:evalExpr, exactEval:host:evalArgs, exactEval:host:evalRecFields, exactEval:host:evalStmt. [Show Proof] Prove exactEval:host:paramName_unique. Prove_Constraint exactEval:host:proj_paramName_forward. Prove_Constraint exactEval:host:proj_paramName_back. Prove exactEval:host:getFunEvalInfo_unique. Prove_Constraint exactEval:host:proj_getFunEvalInfo_forward. Prove_Constraint exactEval:host:proj_getFunEvalInfo_back. Prove exactEval:host:evalProgram_unique. Prove_Constraint exactEval:host:proj_evalProgram_forward. Prove_Constraint exactEval:host:proj_evalProgram_back. Prove exactEval:host:evalExpr_typePres_ctx, exactEval:host:evalExpr_typePres, exactEval:host:evalStmt_typePres, exactEval:host:evalArgs_typePres_Ctx, exactEval:host:evalArgs_typePres, exactEval:host:evalRecFields_typePres_Ctx, exactEval:host:evalRecFields_typePres. [Show Proof] Prove exactEval:host:paramTy_paramName_same. Prove exactEval:host:funOK_getFunEvalInfo_related. Prove exactEval:host:evalExpr_output_forms, exactEval:host:evalStmt_output_forms, exactEval:host:evalArgs_output_forms, exactEval:host:evalRecFields_output_forms. [Show Proof] Prove exactEval:host:evalProgram_output_forms. Prove exactEval:host:paramName_exists. Prove exactEval:host:getFunEvalInfo_exists.