From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 29 Jul 2003 14:59:48 +0000 (+0000)
Subject: Added method FalseInd
X-Git-Tag: LucaOK~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ef7c0b39d038ea5e64595f14b766683d7572833a;p=helm.git

Added method FalseInd
---

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 65d33f917..9a5ad74fd 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -345,6 +345,9 @@ and proof2pres term2pres p =
           let concl = (term2pres t) in 
           if conclude.Con.conclude_method = "BU_Conversion" then
             make_concl "that is equivalent to" concl
+          else if conclude.Con.conclude_method = "FalseInd" then
+           (* false ind is in charge to add the conclusion *)
+           falseind conclude
           else  
             let conclude_body = conclude_aux conclude in
             let ann_concl = 
@@ -425,6 +428,8 @@ and proof2pres term2pres p =
       exists conclude
     else if (conclude.Con.conclude_method = "AndInd") then
       andind conclude
+    else if (conclude.Con.conclude_method = "FalseInd") then
+      falseind conclude
     else if (conclude.Con.conclude_method = "Rewrite") then
       let justif = 
         (match (List.nth conclude.Con.conclude_args 6) with
@@ -447,21 +452,6 @@ and proof2pres term2pres p =
           P.Mtext([None,"mathcolor","Red"],"with");
           P.Mspace([None,"width","0.1cm"]);term2]))]);
           P.Mtr ([],[P.Mtd ([],P.indented justif)])]);
-(* OLD CODE   
-      let conclusion = 
-        (match conclude.Con.conclude_conclusion with 
-           None -> P.Mtext([],"NO Conclusion!!!")
-         | Some c -> term2pres c) in
-      P.Mtable ([None,"align","baseline 1";None,"equalrows","false";
-            None,"columnalign","left"],
-             [P.Mtr ([],[P.Mtd ([],P.Mrow([],[
-               P.Mtext([None,"mathcolor","Red"],"rewrite");
-               P.Mspace([None,"width","0.1cm"]);term1;
-               P.Mspace([None,"width","0.1cm"]);
-               P.Mtext([None,"mathcolor","Red"],"with");
-               P.Mspace([None,"width","0.1cm"]);term2]))]);
-              P.Mtr ([],[P.Mtd ([],P.indented justif)]);
-              P.Mtr ([],[P.Mtd ([],make_concl "we proved 2" conclusion)])]) *)
     else if conclude.Con.conclude_method = "Apply" then
       let pres_args = 
         make_args_for_apply term2pres conclude.Con.conclude_args in
@@ -469,21 +459,6 @@ and proof2pres term2pres p =
         P.Mtext([None,"mathcolor","Red"],"by")::
         P.Mspace([None,"width","0.1cm"])::
         P.Mo([],"(")::pres_args@[P.Mo([],")")])
-(* OLD CODE 
-      let by = 
-         P.Mrow([],
-           P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
-           P.Mo([],"(")::pres_args@[P.Mo([],")")]) in 
-      match conclude.Con.conclude_conclusion with
-        None -> P.Mrow([],[P.Mtext([],"QUA");by])
-      | Some t ->
-         let concl = (term2pres t) in
-         let ann_concl = make_concl "we proved 3" concl in
-         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
-            None,"columnalign","left"; 
-            Some "helm", "xref", conclude.Con.conclude_id],
-             [P.Mtr ([],[P.Mtd ([],by)]);
-              P.Mtr ([],[P.Mtd ([],ann_concl)])]) *)
     else 
       P.Mtable 
         ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
@@ -495,16 +470,6 @@ and proof2pres term2pres p =
                  ([None,"align","baseline 1"; None,"equalrows","false";
                    None,"columnalign","left"],
                   args2pres conclude.Con.conclude_args))))])]) 
-(* OLD CODE 
-     match conclude.Con.conclude_conclusion with
-       None -> body
-     | Some t ->
-         let concl = (term2pres t) in
-         let ann_concl = make_concl "we proved 4" concl in
-         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
-            None,"columnalign","left"],
-             [P.Mtr ([],[P.Mtd ([],body)]);
-              P.Mtr ([],[P.Mtd ([],ann_concl)])]) *)
 
   and args2pres l =
     let module P = Mpresentation in
@@ -655,6 +620,34 @@ and proof2pres term2pres p =
               [P.Mtr([],[P.Mtd([],presacontext)])])
        | _ -> assert false 
 
+     and falseind conclude =
+       let module P = Mpresentation in
+       let module Con = Content in
+       let proof_conclusion = 
+         (match conclude.Con.conclude_conclusion with
+            None -> P.Mtext([],"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 -> [P.Mtext([],"Contradiction, hence")]
+               | Some n -> 
+                  [P.Mi([],n);P.smallskip;P.Mtext([],"is contradictory, hence")])
+           | Con.Lemma lemma -> 
+               [P.Mi([],lemma.Con.lemma_name);P.smallskip;P.Mtext([],"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 module P = Mpresentation in
        let module Con = Content in