From: Michele Galatà <??>
Date: Tue, 4 Feb 2003 17:51:55 +0000 (+0000)
Subject: Added buttons for new tactics Injection and Discriminate
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e974eb6799c994efdee15aa47a34909360dc0aec

Added buttons for new tactics Injection and Discriminate
---

diff --git a/helm/gTopLevel/esempi/decompose.cic b/helm/gTopLevel/esempi/decompose.cic
index f03d410a3..1a06fcba3 100644
--- a/helm/gTopLevel/esempi/decompose.cic
+++ b/helm/gTopLevel/esempi/decompose.cic
@@ -1,5 +1,8 @@
-!A:Prop.!B:Prop.!C:Prop.(and (or A C) (and (or A B) (or B C))) -> True
+!A:Prop.!B:Prop.!C:Prop.(and (sumbool A False) (and (or True B) (or B False))) -> True
 
 !A:Prop.!B:Prop.!C:Prop.(and (sumbool A C) (and (or A B) !D:Prop.(or B D))) -> True
 
 !A:Prop.!B:Prop.!C:Prop.(and (and A C) (and (and A B) (and B C))) -> True
+
+(and True True) -> True
+(and True False) -> True
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index c1dc822b6..bdf78b28f 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2538,6 +2538,12 @@ object(self)
    let replaceb =
     GButton.button ~label:"Replace"
      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+   let injectionb =
+    GButton.button ~label:"Injection"
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+   let discriminateb =
+    GButton.button ~label:"Discriminate"
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
 (* Zack: spostare in una toolbar
    let generalizeb =
     GButton.button ~label:"Generalize"
@@ -2587,6 +2593,8 @@ object(self)
    ignore(introsb#connect#clicked InvokeTactics'.intros) ;
    ignore(decomposeb#connect#clicked InvokeTactics'.decompose) ;
    ignore(searchpatternb#connect#clicked searchPattern) ;
+   ignore(injectionb#connect#clicked InvokeTactics'.injection) ;
+   ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ;
 (* Zack: spostare in una toolbar
    ignore(whdb#connect#clicked whd) ;
    ignore(reduceb#connect#clicked reduce) ;
diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index d7e71177d..96f306cdf 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -409,6 +409,8 @@ module Make(C:Callbacks) =
   let left = call_tactic ProofEngine.left
   let right = call_tactic ProofEngine.right
   let assumption = call_tactic ProofEngine.assumption
+  let injection = call_tactic_with_input ProofEngine.injection
+  let discriminate = call_tactic_with_input ProofEngine.discriminate
   let generalize =
    call_tactic_with_goal_inputs
     (ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)
diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index d527e4faf..313991ced 100644
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -99,6 +99,8 @@ module Make (C : Callbacks) :
    val absurd : unit -> unit
    val contradiction : unit -> unit
    val decompose : unit -> unit
+   val injection : unit -> unit
+   val discriminate : unit -> unit
    val whd_in_scratch : unit -> unit
    val reduce_in_scratch : unit -> unit
    val simpl_in_scratch : unit -> unit
diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 577bdd705..1d7eae9a5 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -238,10 +238,10 @@ let contradiction () = apply_tactic NegationTactics.contradiction_tac
 let decompose ~uris_choice_callback term =
  apply_tactic (EliminationTactics.decompose_tac ~uris_choice_callback term)
 
-(*
-let decide_equality () = apply_tactic VariousTactics.decide_equality_tac
-let compare term1 term2 = apply_tactic (VariousTactics.compare_tac ~term1 ~term2)
-*)
+let injection term = apply_tactic (DiscriminateTactics.injection_tac ~term)
+let discriminate term = apply_tactic (DiscriminateTactics.discriminate_tac ~term)
+let decide_equality () = apply_tactic DiscriminateTactics.decide_equality_tac
+let compare term = apply_tactic (DiscriminateTactics.compare_tac ~term)
 
 (*
 let prova_tatticali () = apply_tactic Tacticals.prova_tac
diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index 29a6f2d79..c75dc437f 100644
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -92,10 +92,11 @@ val decompose :
    (UriManager.uri * int * (UriManager.uri * Cic.term) list) list) ->
  Cic.term -> unit
 
-(*
+val injection : Cic.term -> unit
+val discriminate : Cic.term -> unit
 val decide_equality : unit -> unit
-val compare : Cic.term -> Cic.term -> unit
-*)
+val compare : Cic.term -> unit
+
 
 (*
 val prova_tatticali : unit -> unit