- P.Maction([None,"actiontype","toggle" ; None,"selection","1"],
- [P.indented (P.Mtext([None,"mathcolor","Red"],"Proof"));
- acontext2pres p.Con.proof_apply_context body true]) in
- P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
- None,"columnalign","left"],
- pattern::asubconcl::induction_hypothesis@
- [P.Mtr([],[P.Mtd([],presacontext)])])
- | _ -> assert false in
+ let acontext_id =
+ match p.Con.proof_apply_context with
+ [] -> p.Con.proof_conclude.Con.conclude_id
+ | {Con.proof_id = id}::_ -> id
+ in
+ B.Action([None,"type","toggle"],
+ [ B.indent (add_xref acontext_id (B.b_kw "Proof"));
+ acontext2pres p.Con.proof_apply_context body true]) in
+ B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext])
+ | _ -> assert false
+
+ and falseind conclude =
+ let proof_conclusion =
+ (match conclude.Con.conclude_conclusion with
+ None -> B.b_kw "No conclusion???"
+ | Some t -> term2pres t) in
+ let case_arg =
+ (match conclude.Con.conclude_args with
+ [Con.Aux(n);_;case_arg] -> case_arg
+ | _ -> assert false;
+ (*
+ List.map (ContentPp.parg 0) conclude.Con.conclude_args;
+ assert false *)) in
+ let arg =
+ (match case_arg with
+ Con.Aux n -> assert false
+ | Con.Premise prem ->
+ (match prem.Con.premise_binder with
+ None -> [B.b_kw "Contradiction, hence"]
+ | Some n ->
+ [ B.Object ([],P.Mi([],n)); B.skip;
+ B.b_kw "is contradictory, hence"])
+ | Con.Lemma lemma ->
+ [ B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip;
+ B.b_kw "is contradictory, hence" ]
+ | _ -> assert false) in
+ (* let body = proof2pres {proof with Con.proof_context = tl} in *)
+ make_row arg proof_conclusion
+
+ and andind conclude =
+ let proof_conclusion =
+ (match conclude.Con.conclude_conclusion with
+ None -> B.b_kw "No conclusion???"
+ | Some t -> term2pres t) in
+ let proof,case_arg =
+ (match conclude.Con.conclude_args with
+ [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
+ | _ -> assert false;
+ (*
+ List.map (ContentPp.parg 0) conclude.Con.conclude_args;
+ assert false *)) in
+ let arg =
+ (match case_arg with
+ Con.Aux n -> assert false
+ | Con.Premise prem ->
+ (match prem.Con.premise_binder with
+ None -> []
+ | Some n -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))])
+ | Con.Lemma lemma ->
+ [(B.b_kw "by");B.skip;
+ B.Object([], P.Mi([],lemma.Con.lemma_name))]
+ | _ -> assert false) in
+ match proof.Con.proof_context with
+ `Hypothesis hyp1::`Hypothesis hyp2::tl ->
+ let get_name hyp =
+ (match hyp.Con.dec_name with
+ None -> "_"
+ | Some s -> s) in
+ let preshyp1 =
+ B.H ([],
+ [B.Text([],"(");
+ B.Object ([], P.Mi([],get_name hyp1));
+ B.Text([],")");
+ B.skip;
+ term2pres hyp1.Con.dec_type]) in
+ let preshyp2 =
+ B.H ([],
+ [B.Text([],"(");
+ B.Object ([], P.Mi([],get_name hyp2));
+ B.Text([],")");
+ B.skip;
+ term2pres hyp2.Con.dec_type]) in
+ (* let body = proof2pres {proof with Con.proof_context = tl} in *)
+ let body = conclude2pres proof.Con.proof_conclude false true in
+ let presacontext =
+ acontext2pres proof.Con.proof_apply_context body false in
+ B.V
+ ([],
+ [B.H ([],arg@[B.skip; B.b_kw "we have"]);
+ preshyp1;
+ B.b_kw "and";
+ preshyp2;
+ presacontext]);
+ | _ -> assert false
+
+ and exists conclude =
+ let proof_conclusion =
+ (match conclude.Con.conclude_conclusion with
+ None -> B.b_kw "No conclusion???"
+ | Some t -> term2pres t) in
+ let proof =
+ (match conclude.Con.conclude_args with
+ [Con.Aux(n);_;Con.ArgProof proof;_] -> proof
+ | _ -> assert false;
+ (*
+ List.map (ContentPp.parg 0) conclude.Con.conclude_args;
+ assert false *)) in
+ match proof.Con.proof_context with
+ `Declaration decl::`Hypothesis hyp::tl
+ | `Hypothesis decl::`Hypothesis hyp::tl ->
+ let get_name decl =
+ (match decl.Con.dec_name with
+ None -> "_"
+ | Some s -> s) in
+ let presdecl =
+ B.H ([],
+ [(B.b_kw "let");
+ B.skip;
+ B.Object ([], P.Mi([],get_name decl));
+ B.Text([],":"); term2pres decl.Con.dec_type]) in
+ let suchthat =
+ B.H ([],
+ [(B.b_kw "such that");
+ B.skip;
+ B.Text([],"(");
+ B.Object ([], P.Mi([],get_name hyp));
+ B.Text([],")");
+ B.skip;
+ term2pres hyp.Con.dec_type]) in
+ (* let body = proof2pres {proof with Con.proof_context = tl} in *)
+ let body = conclude2pres proof.Con.proof_conclude false true in
+ let presacontext =
+ acontext2pres proof.Con.proof_apply_context body false in
+ B.V
+ ([],
+ [presdecl;
+ suchthat;
+ presacontext]);
+ | _ -> assert false
+
+ in
+ proof2pres p