Lines Matching defs:proofs
499 val proofs = append_proofs [th_proof, unchanged_thm_proof, used_stack_thm_proof, spec_thm_proof]
501 (spec, spec_thm_name, th, th_name, proofs)
545 val (ir1_spec, ir1_spec_name, ir1_wf, ir1_wf_name, ir2_spec, ir2_spec_name, ir2_wf, ir2_wf_name, proofs) =
562 fun mk_sc_spec___pre ir1_spec ir1_spec_name ir1_wf ir1_wf_name ir2_spec ir2_spec_name ir2_wf ir2_wf_name proofs =
611 val proofs' = append_proofs [proofs, f_th_proof, sc_f_thm_proof, f_th_proof', well_formed_th_proof];
614 (f_th, f_th_name', well_formed_th, well_formed_th_name, sc_ir, proofs')
618 val (ir1_spec, ir1_name, ir2_spec, ir2_name, proofs) = (spec1, spec1_name, spec2, spec2_name, [])
629 fun mk_sc_spec ir1_spec ir1_name ir2_spec ir2_name proofs =
636 val proofs' = append_proofs [proofs, specL1_proof, specL2_proof];
637 val (ir_spec, ir_spec_name, ir_wf, ir_wf_name, sc_ir, proofs'') =
638 mk_sc_spec___pre (el 1 specL1) (el 1 specL1_name) (el 2 specL1) (el 2 specL1_name) (el 1 specL2) (el 1 specL2_name) (el 2 specL2) (el 2 specL2_name) proofs';
660 val proofs''' = append_proofs[proofs'', unchanged_th_proof, th_proof]
670 (th, th_name, proofs''')
774 fun mk_fc_spec (pre_spec, pre_spec_name, body_spec, body_spec_name, post_spec, post_spec_name, pre_th, pre_th_name, post_th, post_th_name, proofs, unchanged_list) =
785 val proofs' = append_proofs [proofs, preL_proof, bodyL_proof, postL_proof];
842 val proofs'' = append_proofs [proofs', body_PSPEC_proof];
844 val (ir_spec1, ir_spec1_name, ir_wf1, ir_wf1_name, _, proofs''') =
845 mk_sc_spec___pre (el 1 preL) (el 1 preL_name) (el 2 preL) (el 2 preL_name) (el 1 bodyL) (el 1 bodyL_name) (el 2 bodyL) (el 2 bodyL_name) proofs'';
847 val (ir_spec, ir_spec_name, ir_wf, ir_wf_name, sc_ir, proofs'''') =
848 mk_sc_spec___pre ir_spec1 ir_spec1_name ir_wf1 ir_wf1_name (el 1 postL) (el 1 postL_name) (el 2 postL) (el 2 postL_name) proofs''';
888 val proofs''''' = append_proofs [proofs'''', unchanged_th_proof, th_proof];
890 (th, th_name, proofs''''')
1022 fun mk_tr_spec cond body_spec body_name proofs =
1104 val proofs' = append_proofs[proofs, wf_th_proof, f_th_proof, well_formed_th_proof, unchanged_th_proof, th_proof]
1115 (th, th_name, proofs')
1152 val (ir1_spec, ir1_name, ir2_spec, ir2_name, proofs) = (spec1, spec1_name, spec2, spec2_name, proofs2);
1156 fun mk_cj_spec cond ir1_spec ir1_name ir2_spec ir2_name unchanged_list proofs =
1217 val proofs = append_proofs [proofs, f_th_proof, unchanged_th_proof, well_formed_th_proof, th_proof]
1227 (th, th_name, proofs)
1363 val proofs = [];
1368 fun fwd_reason (annotatedIR.BLK blk_ir) unchanged_list proofs =
1373 (spec, spec_thm_name, append_proofs [proofs, proofs_blk])
1376 | fwd_reason (annotatedIR.SC (ir1, ir2, info)) unchanged_list proofs =
1378 val (spec1, spec1_name, proofs1) = fwd_reason ir1 unchanged_list proofs;
1384 | fwd_reason (annotatedIR.TR (cond, body, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) unchanged_list proofs =
1385 let val (body_spec, body_name, proofs') = fwd_reason body unchanged_list proofs
1387 mk_tr_spec cond body_spec body_name proofs'
1389 | fwd_reason (annotatedIR.CJ (cond, ir1, ir2, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) unchanged_list proofs =
1391 val (spec1, spec1_name, proofs1) = fwd_reason ir1 unchanged_list proofs;
1396 | fwd_reason (annotatedIR.CALL (fname, pre_ir, body_ir, post_ir,info)) unchanged_list proofs =
1400 val (body_spec, body_spec_name, proofs') = fwd_reason body_ir f_unchanged_list proofs;
1404 val proofs'' = append_proofs [proofs', pre_proofs, post_proofs];
1406 mk_fc_spec (pre_spec, pre_spec_name, body_spec, body_spec_name, post_spec, post_spec_name, pre_th, pre_th_name, post_th, post_th_name, proofs'', unchanged_list)
1451 val (f_th_name, proofs) =
1470 val proofs' = append_proofs [proofs, thm_proof];
1472 (thm, thm_name, proofs')