Added buttons for new tactics Injection and Discriminate

diff --git a/helm/gTopLevel/esempi/decompose.cic b/helm/gTopLevel/esempi/decompose.cic
index f03d410a3242197acf54b2793789fc41d0d3e4c3..1a06fcba380e7e0be9ccdc4914a766bdfa42fac3 100644 (file)
--- 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 c1dc822b68761242022f9df50932748ebe0952ca..bdf78b28fa1c32a5b88b0cf246b0a07a084cfedd 100644 (file)
--- 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 d7e71177d5c524904548e6bb3a70d7a0d90ebde5..96f306cdf4c8f0b97ce036d17a6d9a2873fee2a2 100644 (file)
--- 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 d527e4fafa28956d83ed5745384d354ffa2a7b05..313991cedd21f41679e270d759f67c0356302d2d 100644 (file)
--- 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 577bdd7053828ecf39adb8249bcff80e99da78f8..1d7eae9a59d9dda14b097c67be747a231e82d941 100644 (file)
--- 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 29a6f2d7945b26ba449225858c0f18178a621f73..c75dc437fe00f5eba77b6b7ec70ef8bb0acc9fda 100644 (file)
--- 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