the type of proof in or2and_edge is now string.

Since we produce and-nodes only when we manage to prove the parental
or-node assuming and-node, we do not have to use the option type anymore.

Author: yutakang

Abduction/Abduction_Graph.ML

@@ -58,7 +58,6 @@ val grand_children                               : abduction_graph -> key -> key
 val all_gg_parents_are_proved                    : abduction_graph -> key -> bool;
 
 (* query on abduction_node for or2and_edge *)
-val ornode_proved_assmng_andnodes                : abduction_graph -> key -> bool;
 val or2and_edge_to_proof                         : abduction_graph -> key -> string;
 
 val is_worth_proving                             : Proof.context -> abduction_graph -> key -> bool;
@@ -289,10 +288,6 @@ fun orkeys_tobe_expanded_in (ctxt:Proof.context) (graph:abduction_graph): keys =
     result
   end;
 
-(* ornode_proved_assmng_andnodes *)
-fun ornode_proved_assmng_andnodes (graph:abduction_graph) (key:key) =
-    Abduction_Node.ornode_proved_assmng_andnodes (PGraph.get_node graph key);
-
 (* or2and_edge_to_proof *)
 fun or2and_edge_to_proof (graph:abduction_graph) (key:key) =
     Abduction_Node.or2and_edge_to_proof (PGraph.get_node graph key);

Abduction/Abduction_Node.ML

@@ -36,7 +36,6 @@ val lemma_name_of                                : abduction_node -> string;
 val is_worth_proving                             : Proof.context -> abduction_node -> bool;
 
 (* query on abduction_node for or2and_edge *)
-val ornode_proved_assmng_andnodes: abduction_node -> bool;
 val or2and_edge_to_proof         : abduction_node -> string;
 
 (* destructors of abduction_node *)
@@ -104,11 +103,6 @@ fun is_branch (Or_Node or_nd) = #is_branch or_nd
 fun is_final_goal (Or_Node or_nd) = #final_goal or_nd
   | is_final_goal  _              = error "is_final_goal. This is not Or_Node."
 
-(* ornode_proved_assmng_andnodes *)
-fun ornode_proved_assmng_andnodes (Or_To_And or2and_edge:abduction_node) =
-    #proof_of_ornode_assmng_andnodes or2and_edge |> is_some
-  | ornode_proved_assmng_andnodes _ = error "ornode_proved_assmng_andnodes";
-
 (* or2and_edge_to_proof *)
 fun or2and_edge_to_proof (Or_To_And or2and_edge:abduction_node) = Or2And_Edge.or2and_edge_to_proof or2and_edge
   | or2and_edge_to_proof _ = error "or2and_edge_to_proof failed. This is not or2and_edge."

Abduction/Or2And_Edge.ML

@@ -37,12 +37,9 @@ fun proof_is_from_tactic (Tactic _) = true
 (* or2and_edge *)
 type or2and_edge = {
   how_to_get_andnodes_from_ornode: how_to_get_andnodes_from_ornode,
-  proof_of_ornode_assmng_andnodes: string option}(*NONE: we cannot prove the or-node.*)
+  proof_of_ornode_assmng_andnodes: string}(*NONE: we cannot prove the or-node.*)
 
 (* or2and_edge_to_proof *)
-fun or2and_edge_to_proof ({proof_of_ornode_assmng_andnodes, ...}:or2and_edge) =
-  if   is_some proof_of_ornode_assmng_andnodes
-  then the proof_of_ornode_assmng_andnodes
-  else error "edge_to_final_proof failed. We do not know how to prove the or-node assuming the subgoals of the and-node.";
+fun or2and_edge_to_proof ({proof_of_ornode_assmng_andnodes, ...}:or2and_edge) = proof_of_ornode_assmng_andnodes;
 
 end;

Abduction/Seed_Of_Or2And_Edge.ML

@@ -23,10 +23,10 @@ val print_seed_of_or2and_edge: Proof.context -> seed_of_or2and_edge -> unit list
 val seed_is_from_tactic      : seed_of_or2and_edge -> bool;
 
 val apply_PSL_to_get_seeds_of_or2and_edges: Proof.state -> seeds_of_or2and_edge;
-val filter_out_bad_seeds_of_or2and_edge: term (*parental or-node*) -> Proof.state -> abduction_graph -> seeds_of_or2and_edge -> seeds_of_or2and_edge
-val conjectures_to_seeds_of_or2and_edge: (Proof.state (*default pst*) * Proof.state (*chained pst to proved the parental ornode*)) -> (string * term) list -> seeds_of_or2and_edge;
-val seed_has_counterexample            : Proof.state -> seed_of_or2and_edge -> bool;
-val seeds_to_updated_graph             : key -> seeds_of_or2and_edge -> Update_Abduction_Graph.update_abduction_graph;
+val filter_out_bad_seeds_of_or2and_edge   : term (*parental or-node*) -> Proof.state -> abduction_graph -> seeds_of_or2and_edge -> seeds_of_or2and_edge
+val conjectures_to_seeds_of_or2and_edge   : (Proof.state (*default pst*) * Proof.state (*chained pst to proved the parental ornode*)) -> (string * term) list -> seeds_of_or2and_edge;
+val seed_has_counterexample               : Proof.state -> seed_of_or2and_edge -> bool;
+val seeds_to_updated_graph                : key -> seeds_of_or2and_edge -> Update_Abduction_Graph.update_abduction_graph;
 
 end;
 
@@ -170,19 +170,16 @@ fun add_or2and_edge_and_connect_it_to_parental_ornode
      if proved_parent_or
      then
        let
-         val how_we_got_andnode    = Or2And_Edge.how_to_get_andnodes_from_ornode_of proof: string;
-         val script_to_prove_andnd = the script_opt_gen                                  : string;
-         val script_to_prove_ornd  = how_we_got_andnode ^ script_to_prove_andnd          : string;
+         val how_we_got_andnode    = Or2And_Edge.how_to_get_andnodes_from_ornode_of proof                        : string;
+         val script_to_prove_andnd = the script_opt_gen                                                          : string;
+         val script_to_prove_ornd  = how_we_got_andnode ^ script_to_prove_andnd                                  : string;
          val or2and_edge_val       = Abduction_Node.Or_To_And {
                                       how_to_get_andnodes_from_ornode = proof,
-                                      (*TODO: Should we really need to use the option type here?*)
-                                      proof_of_ornode_assmng_andnodes = SOME script_to_prove_ornd}               : abduction_node;
+                                      proof_of_ornode_assmng_andnodes = script_to_prove_ornd}                    : abduction_node;
          val or2and_edge_key      = ((O2A_E (serial())), [])                                                     : key;
          val thy                  = Proof.theory_of state                                                        : theory;
          val used_cnjctr_names    = Top_Down_Util.get_lemma_names_from_sh_output thy script_to_prove_andnd       : strings;
-
          val used_name_term_pairs = filter (fn (name, _) => member (op =) used_cnjctr_names name) name_term_pairs: (string * term) list;
-
          val relevant_name_term_pairs = if   Or2And_Edge.how_to_get_andnodes_from_ornode_of proof = "" (*if this is the result of tactic application*)
                                         then used_name_term_pairs
                                         else name_term_pairs;