// |Ded_Action.java|: Parent class for all deductions. /* Copyright (C) 2009 Hugh McGuire http://www.cis.gvsu.edu/~mcguire/ * Grand Valley State University, MI 49401-9403 */ /* This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. For a copy of the GNU General Public License, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth floor, Boston, MA 02110-1301, USA. Another option as of January 1, 2009 is to browse the following URL: http://www.gnu.org/copyleft/gpl.html */ import java.util.*; import javax.swing.JTable; import javax.swing.JFrame; import javax.swing.AbstractAction; import java.awt.Toolkit; import javax.swing.JOptionPane; import java.awt.event.ActionEvent; /** * Parent class for all deductions. * @author Hugh McGuire */ abstract class Ded_Action extends AbstractAction { // As I've told my students, |protected| is really as insecure/unprotected // as |public|. But I consider |final| material to be // like |static| constants provided by a class. protected final JTable table; private static boolean acting_vs_just_checking_applicability; // quiet Ded_Action(/*ProofBuilder GUI_given,*/ JTable table_given) { //GUI = GUI_given; table = table_given; } protected PB_TableModel table_model() { return (PB_TableModel) table.getModel(); } static boolean get_actingvsjustcheckingapplicability() { return acting_vs_just_checking_applicability; } /* When doing the updating |appears_applicable()| for all the items, * probably unify things by having each item have a method * |boolean consider(ActionEvent action_event, Deduction_Prep[] preps)| * which outside code can use instead of |appears_applicable()|, * passing |null| or something for the |ActionEvent|, * (there's an issue regarding |Resolve| distinguishing self vs. mult.rows; * although redundant when there really is an action, like * |appears_applicable()| having a parameter |String action_string| * would address this issue (can't do something like a |null| |source| * in |ActionEvent| because API documentation indicates that would * generate an |IllegalArgumentException|)) * and then here have something like the following: */ final public void actionPerformed(ActionEvent action_event) { int[] selected_rows_indexes = table.getSelectedRows(); Deduction_Prep[] preps = new Deduction_Prep[selected_rows_indexes.length]; for ( int i = 0; i < preps.length; i++ ) { if ( !table_model().get_entry(selected_rows_indexes[i]) .has_expr() ) { note_error( "You need to select rows containing only formulas,", "not narrative texts, to do a deduction." ); return; } preps[i] = new Deduction_Prep(table, i); } acting_vs_just_checking_applicability = true; table_model().set_addedrowindex_neg1(); try { consider(action_event.getActionCommand(), preps); } finally { acting_vs_just_checking_applicability = false; } // in C++ the following |if| could also contain this decl.+init. int added_row_index = table_model().get_addedrowindex(); if ( added_row_index >= 0 ) { // on my Mac with Java 1.5.0_06-112, // weird things happened when tried listening // for |TableModelEvent.INSERT| and doing // |setRowSelectionInterval()| then table.setRowSelectionInterval(added_row_index, added_row_index); /* // THE FOLLOWING HASN'T BEEN WORKING: table.scrollRectToVisible( table.getCellRect( added_row, table.convertColumnIndexToView( // may be wrong column; so what. prep.selected_column_id.ordinal() ), true ) ); */ //GUI.scroll_to_row_i(added_row); /* // THE FOLLOWING HASN'T BEEN WORKING: table_model().fireTableCellUpdated( formula_row_i_to_select, PB_TableModel.Column_ID.GOALS.ordinal() ); */ } } abstract boolean consider(String action_command, Deduction_Prep[] preps); boolean note_error(Object message) { if ( acting_vs_just_checking_applicability ) { Toolkit.getDefaultToolkit().beep(); JOptionPane.showMessageDialog( (JFrame) table.getTopLevelAncestor(), message, "Error", JOptionPane.ERROR_MESSAGE ); } return false; } boolean note_error(String message_line1, String message_line2, String message_line3, String message_line4, String message_line5 ) { String[] message = { message_line1, message_line2, message_line3, message_line4, message_line5 }; return note_error(message); } // I would appreciate being able to have default values for arguments // as in C++. boolean note_error(String message_line1, String message_line2) { return note_error(message_line1, message_line2, null, null); } boolean note_error(String message_line1, String message_line2, String message_line3 ) { return note_error( message_line1, message_line2, message_line3, null, null ); } boolean note_error(String message_line1, String message_line2, String message_line3, String message_line4 ) { return note_error( message_line1, message_line2, message_line3, message_line4, null ); } boolean note_sel_expr_rows_count(int sel_count_need) { if ( table.getSelectedRowCount() != sel_count_need ) return note_error( "This operation needs exactly " + sel_count_need + " row" + (sel_count_need == 1 ? "" : "s") + " to be selected." ); /* for ( int selected_row : table.getSelectedRows() ) if( !table_model().get_entry(selected_row).has_expr() ) return note_error( "To do this operation," + " you need to select" + (sel_count_need == 1 ? " a" : "") + " row" + (sel_count_need == 1 ? "" : "s") + " containing" + (sel_count_need == 1 ? " a" : "") + " formula" + (sel_count_need == 1 ? "" : "s") + "." ); */ return true; } // When I was considering writing a function like this, // I considered naming it "require_entire()". (;-) boolean note_sel_entire(Deduction_Prep prep) { return prep.subexpr == prep.expr ? true : note_error( "This operation needs to be applied to a row's entire formula;", "you have selected only a subexpression." ); } HashSet note_sel_unquant_vars(Deduction_Prep prep) { HashSet result = prep.expressionsmgmt.variables_unquantified(prep.subexpr); // really checking disjoint i.e. empty intersection if ( result.removeAll(prep.scoped_freeable_vars) || result.removeAll(prep.scoped_dependent_vars) ) { note_error( "For this operation, each of your selections should", "not contain any variable quantified outside the selection." ); // ? IS THIS MEANLY DENYING SELECTION OF REAL MATCH // INSIDE UNIVERSAL QUANTIFICATION WHICH WOULD BE ACCEPTED // BY THE RETRYING BELOW ? return null; } return result; } boolean note_parts_consistent(int row1, int row2) { return table_model().parts_consistent(row1, row2) ? true : note_error( /* "You selected two rows that were in separate (sub)parts." // are // conflicting // not combinable // incompatible */ "Those two rows that you selected are in separate" + " subparts of this proof." ); } HashMap standardize_variables_apart( HashSet vars0, Expression expr0 ) { // standardizing variables apart // using "g####" variables as with |(gensym)| in old LISP (;-) int g_index = 0; // to really copy old LISP, |static| HashMap g_vars0 = new HashMap(); // |g_vars0| used for changing variables back // from "g####" to their originals for ( String v : vars0 ) { String g_; do g_ = "g" + ++g_index; while ( table_model().get_expressionsmgmt().is_id_being_used(g_) ) ; table_model().get_expressionsmgmt().add_variable_id(g_); expr0.replace_throughout_scope(v, g_); g_vars0.put(g_, v); } return g_vars0; } boolean conclude_two_row_ded( Deduction_Prep prep0, Deduction_Prep prep1, boolean do_simplify, HashMap g_vars, LinkedList unifier, String narrative_base_flowing_with_preceding_row, String narrative_base_independent ) { // assert unifier != null : "unifier != null"; //prep0.expr.simplify(); Expression result = //delay_full_simplify && prep0.selected_column_id == PB_TableModel.Column_ID.SUPPS ? prep1.selected_column_id == PB_TableModel.Column_ID.SUPPS ? new Expression( prep0.expressionsmgmt.new_Symbol( Symbol.Specifier.OR ), prep0.expr.ensure_group(), prep1.expr.ensure_group() ) : new Expression( prep0.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), new Expression( prep0.expressionsmgmt.new_Symbol( prep0.expressionsmgmt.get_lognegsymspec() ), prep0.expr.ensure_group() ), prep1.expr.ensure_group() ) : prep1.selected_column_id == PB_TableModel.Column_ID.GOALS ? new Expression( prep0.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), prep0.expr.ensure_group(), prep1.expr.ensure_group() ) : new Expression( prep0.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), prep0.expr.ensure_group(), new Expression( prep1.expressionsmgmt.new_Symbol( prep1.expressionsmgmt.get_lognegsymspec() ), prep1.expr.ensure_group() ) ); boolean exprs_imps = prep0.expr.op_spec_equals(Symbol.Specifier.IMPLIES) && prep0.expr.op_spec_equals(Symbol.Specifier.IMPLIES); if ( do_simplify ) prep0.expressionsmgmt.simplify(result, true); // facilitate "Law of the Syllogism" used by Grimaldi if ( exprs_imps && result.op_spec_equals(Symbol.Specifier.OR) ) if ( result.get_argument1().ungroup() .op_spec_equals(Symbol.Specifier.NOT) ) result.this_structure_replace( prep1.expressionsmgmt.new_Symbol(Symbol.Specifier.IMPLIES), result.get_argument1().ungroup().get_argument1(), result.get_argument2() ); else if ( result.get_argument2().ungroup() .op_spec_equals(Symbol.Specifier.NOT) ) result.this_structure_replace( prep1.expressionsmgmt.new_Symbol(Symbol.Specifier.IMPLIES), result.get_argument1(), result.get_argument2().ungroup().get_argument1() ); for ( Map.Entry g_v : g_vars.entrySet() ) { String g_ = g_v.getKey(); result.replace_throughout_scope(g_, g_v.getValue()); prep0.expressionsmgmt.expunge_variable_id(g_); } PB_TableModel.Column_ID result_column_id = prep0.selected_column_id == PB_TableModel.Column_ID.SUPPS && prep1.selected_column_id == PB_TableModel.Column_ID.SUPPS ? PB_TableModel.Column_ID.SUPPS : PB_TableModel.Column_ID.GOALS; if ( result.op_spec_equals( result_column_id == PB_TableModel.Column_ID.SUPPS ? Symbol.Specifier.TRUE : Symbol.Specifier.FALSE ) ) return note_error("The result here was inconsequential."); if ( narrative_base_flowing_with_preceding_row == null ) narrative_base_flowing_with_preceding_row = table_model().REDUCES_BY_ + (prep0.selected_row < prep1.selected_row ? prep0.ref_num_name : prep1.ref_num_name ); if ( !unifier.isEmpty() ) { StringBuilder unifier_report_base = new StringBuilder("with " + Symbol.START_CODE_IN_COMMENTARY); do { Expressions_Mgmt.Variable_Binding_to_Expression binding = unifier.remove(); String variable_mapped = g_vars.get(binding.variable); unifier_report_base.append( (variable_mapped != null ? variable_mapped : binding.variable ) + " := " + binding.expression.gen_text(-1) + (unifier.isEmpty() ? Character.toString(Symbol.END_CODE_IN_COMMENTARY) : ", ") ); } while ( !unifier.isEmpty() ); narrative_base_flowing_with_preceding_row += (narrative_base_flowing_with_preceding_row.charAt(0) != ' ' ? "\n" : " " ) + unifier_report_base; narrative_base_independent += "\n" + unifier_report_base; } narrative_base_independent += "\nyields:"; if ( narrative_base_flowing_with_preceding_row.charAt(0) != ' ' ) narrative_base_flowing_with_preceding_row += "\nyields:"; table_model().add( prep0.selected_rows, result_column_id, narrative_base_flowing_with_preceding_row, narrative_base_independent, result ); return true; } boolean conclude_two_row_ded( Deduction_Prep prep0, Deduction_Prep prep1, HashMap g_vars, LinkedList unifier, String narrative_base_flowing_with_preceding_row, String narrative_base_independent ) { return conclude_two_row_ded( prep0, prep1, true, g_vars, unifier, narrative_base_flowing_with_preceding_row, narrative_base_independent ); } // At first I tried leaving the nested classes here non-static. // That caused problems! static class Suppose_Negation extends Ded_Action { Suppose_Negation(/*ProofBuilder GUI_given,*/ JTable table_given) { super(/*GUI_given,*/ table_given); } //public void actionPerformed(ActionEvent action_event) { boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(action_event.getActionCommand()) : "appears_applicable(action_event.getActionCommand())"; */ if ( !note_sel_expr_rows_count(1) ) return false; Deduction_Prep prep = new Deduction_Prep(table); /* if ( selected_row != table.getRowCount() - 1 ) return note_error( (JFrame) table.getTopLevelAncestor(), "This operation needs to be applied to the last row." ); */ if ( prep.selected_column_id != PB_TableModel.Column_ID.GOALS ) return note_error( "This operation is applicable only to a goal formula." ); if ( table_model().get_transformationgoal_relationship( prep.selected_row ) != null ) return note_error( "That operation would interfere" + " with the sequence of transformations", "which you're in the middle of." ); if ( !note_sel_entire(prep) ) return false; // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; table_model().note_supp_neg(prep.selected_row); Expression result = new Expression( prep.expressionsmgmt.new_Symbol( prep.expressionsmgmt.get_lognegsymspec() ), prep.expr.ensure_group() ); //result.simplify(); String narrative_base = "Attempting a proof by contradiction," + "\nsuppose the negation of "; table_model().add( prep.selected_rows, PB_TableModel.Column_ID.SUPPS, narrative_base + "that formula:", narrative_base + "formula " + prep.ref_num_name, result ); return true; } } static class Split extends Ded_Action { Split(/*ProofBuilder GUI_given,*/ JTable table_given) { super(/*GUI_given,*/ table_given); } static String word(int n) { switch ( n ) { case 0: return "zero"; case 1: return "one"; case 2: return "two"; case 3: return "three"; case 4: return "four"; case 5: return "five"; case 6: return "six"; case 7: return "seven"; case 8: return "eight"; case 9: return "nine"; default: return Integer.toString(n); } } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(action_event.getActionCommand()) : "appears_applicable(action_event.getActionCommand())"; */ if ( !note_sel_expr_rows_count(1) ) return false; Deduction_Prep prep = new Deduction_Prep(table); if ( table_model().get_transformationgoal_relationship( prep.selected_row ) != null ) return note_error( "Splitting that expression into multiple ones" + " would confuse the sequence of transformations." ); if ( !note_sel_entire(prep) ) return false; if ( !(prep.expr.op_spec_equals(Symbol.Specifier.AND) || prep.expr.op_spec_equals(Symbol.Specifier.OR) || prep.selected_column_id == PB_TableModel.Column_ID.GOALS && (prep.expr.op_spec_equals( Symbol.Specifier.IMPLIES ) || prep.expr.op_spec_equals( Symbol.Specifier.TURNSTILE ) ) ) ) return note_error( "This operation is applicable only to a row" + " containing a formula that is ", "a conjunction (i.e. \"something " + Symbol.AND_UNICODE + " something\"" + " a.k.a. \"something AND something\"),", "or a disjunction (with \"" + Symbol.OR_UNICODE + "\" a.k.a. \"OR\"),", "or an implication (with \"" + prep.expressionsmgmt .get_spec_String(Symbol.Specifier.IMPLIES) + "\" a.k.a. \"IMPLIES\") if it's a goal." ); // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; int formula_row_i_to_select = -1; if ( prep.expr.get_operator().get_specifier() .equals( prep.selected_column_id == PB_TableModel.Column_ID.GOALS ? Symbol.Specifier.AND : Symbol.Specifier.OR ) ) { HashSet free_variables = prep.expressionsmgmt.variables_unquantified(prep.expr); if ( !free_variables.isEmpty() ) return note_error( "Sorry, this operation isn't appropriate" + " for a formula with" + (free_variables.size() == 1 ? " a" : "") + " free variable" + (free_variables.size() > 1 ? "s" : "") + '.' // otherwise splitting such a goal could prove // e.g. (Ex)[x = 3 /\ x = 5] // and splitting such a supposition could have // (Ax)[x < x + 2 \/ x = -1] with one // case being x = -1 with x free from which // would have (Ax)[x = -1] in that case ); table_model().add_subparts( prep.selected_row, prep.selected_column_id, "We'll handle" /* + (prep.selected_row < table_model() .end_part_seg_rows(prep.selected_row) ? " formula " + prep.ref_num_name : " that formula" ) */ + " formula " + prep.ref_num_name + "'s components" // elements + "\nin separate subparts of this proof" + ", as follows:", prep.expr.multiary_op_args() ); // return table_model().get_addedrowindex() >= 0; } else if ( prep.selected_column_id == PB_TableModel.Column_ID.GOALS ) if ( prep.expr.op_spec_equals(Symbol.Specifier.IMPLIES) || prep.expr.op_spec_equals(Symbol.Specifier.TURNSTILE) ) { LinkedList consequents = prep.expr.get_argument2().multiary_op_args( Symbol.Specifier.OR ); //formula_row_i_to_select = table_model().add_elements( consequents, PB_TableModel.Column_ID.GOALS, "and we'll work on proving " + (consequents.size() > 1 ? "a" : "the") + " consequent:", null, prep.selected_rows ); table_model().remember_added_row(); // Probably should also handle auto-sub-split consequent // that is another implication. LinkedList antecedents = prep.expr.get_argument1().multiary_op_args( prep.expr.op_spec_equals( Symbol.Specifier.TURNSTILE ) ? Symbol.Specifier.COMMA : Symbol.Specifier.AND ); String narrative_base = "We'll assume that formula's antecedent" + (antecedents.size() > 1 ? "s" : "") + ':'; table_model().add_elements( antecedents, PB_TableModel.Column_ID.SUPPS, narrative_base, "Consider formula " + prep.ref_num_name + ".\n" + narrative_base, prep.selected_rows, true ); //formula_row_i_to_select += 2*antecedents.size(); table_model().set_addedrowindex_to_remembered(); } else { assert prep.expr.op_spec_equals(Symbol.Specifier.OR) : "prep.expr.op_spec_equals(Symbol.Specifier.OR)"; LinkedList elements = prep.expr.multiary_op_args(); String narrative_base = "That formula can be separated into " + word(elements.size()) + "\nalternative goals; first:"; table_model().add_elements( elements, PB_TableModel.Column_ID.GOALS, narrative_base, "Consider formula " + prep.ref_num_name + ".\n" + narrative_base, prep.selected_rows ); } else if ( prep.expr.op_spec_equals(Symbol.Specifier.AND) ) { LinkedList elements = prep.expr.multiary_op_args(); String narrative_base = "That formula can be separated into " + word(elements.size()) + "\nalternative suppositions/derivations; first:"; table_model().add_elements( elements, PB_TableModel.Column_ID.SUPPS, narrative_base, "Consider formula " + prep.ref_num_name + ".\n" + narrative_base, prep.selected_rows ); } return true; } } // Eliminate_Quantifier // Remove_Quantifier // Dequantify static class Dequantify extends Ded_Action { Dequantify(/*ProofBuilder GUI_given,*/ JTable table_given) { super(/*GUI_given,*/ table_given); } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(event.getActionCommand()) : "appears_applicable(event.getActionCommand())"; */ if ( !note_sel_expr_rows_count(1) ) return false; Deduction_Prep prep = new Deduction_Prep(table); if ( table_model().get_transformationgoal_relationship( prep.selected_row ) != null ) return note_error( "That operation would interfere" + " with the sequence of transformations", "which you're in the middle of." ); if ( prep.polarity == 0 ) return note_error( "What you selected appears to be within the scope" + " of a \"" + prep.expressionsmgmt .get_spec_String(Symbol.Specifier.EQUIV) + "\" operator.", "You need to apply Rewriting to that operator", "before you can remove a quantifier in its scope." ); //assert(quantifier.is_quantifier()); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.QUANT_SEP) ) { prep.quant = prep.subexpr; prep.parent = prep.subexpr; prep.subexpr = prep.subexpr.get_argument1(); // then one of the following |if|s should fire: } if ( prep.subexpr.is_group() && prep.subexpr.get_operator().get_text().equals("(") ) { prep.parent = prep.subexpr; prep.subexpr = prep.subexpr.get_argument1(); // then the following |if| should fire: } if ( prep.subexpr.get_operator().is_quantifier() ) { // subexpr == quantifier prep.parent = prep.subexpr; prep.subexpr = prep.subexpr.get_argument1(); } if ( prep.quant == null ) return note_error( "This operation needs to be applied to a variable" + " inside a quantifier." ); Expression quantifier = prep.quant.get_argument1().ungroup(); if ( prep.subexpr.get_operator().is_relation() || prep.parent != null && prep.parent.get_operator().is_relation() ) return note_error( "It would clarify matters if you would first apply the" + " canonical equivalence", "to expand the relativized quantification" + " at your selection into", "a more basic quantification plus a" + (quantifier .op_spec_equals(Symbol.Specifier.FORALL) ? "n implication." : " conjunction." ), "(To be able to do that, select the quantifier" + " plus the quantified formula.)" ); // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; if ( quantifier.op_spec_equals(Symbol.Specifier.FORALL) && prep.selected_column_id == PB_TableModel.Column_ID.SUPPS ) { Toolkit.getDefaultToolkit().beep(); String[] message = { "You generally don't need to remove quantifiers", "that are universal (i.e. \"" + Symbol.FORALL_UNICODE + "\", \"forall\") from suppositions/derivations.", "Proceed anyway?" }; if ( JOptionPane.showConfirmDialog( (JFrame) table.getTopLevelAncestor(), message, "Remove quantifier from supposition/derivation?", JOptionPane.YES_NO_OPTION ) == JOptionPane.NO_OPTION ) return false; } boolean freeing_vs_skolemizing = quantifier.op_spec_equals(Symbol.Specifier.FORALL) ^ (prep.polarity > 0); String rplcmnt_str = null; if ( freeing_vs_skolemizing ) { if ( !prep.scoped_dependent_vars.isEmpty() ) return note_error( "For soundness, you're supposed to remove", "quantifier(s) for " + prep.scoped_dependent_vars + " before what you've selected here." ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.COMMA) ) { HashSet vars = prep.expressionsmgmt .variables_unquantified(prep.subexpr); vars.retainAll(prep.scoped_freeable_vars); if ( vars.size() > 1 ) return note_error( "Multiple variables would need to be renamed,", "and that's inconvenient " + "for this program to handle;", "try selecting one of these variables at a time" + " for quantifier removal." ); } } else { if ( !prep.subexpr.op_spec_equals(Symbol.Specifier.IDENTIFIER) ) return prep.parent == quantifier ? note_error( "It's difficult to remove quantifiers" + " for all those selected variables at once.", "Try selecting one of them at a time" + " for quantifier removal." ) : note_error( "This operation needs to be applied to a variable" + " inside a quantifier;", "what you have selected is something else." ); String v = prep.subexpr.get_operator().get_text(); String r; Stack r_vars = new Stack(); r_vars.addAll( prep.expressionsmgmt.variables_unquantified(prep.expr) ); r_vars.addAll(prep.scoped_freeable_vars); if ( r_vars.isEmpty() ) r = "a"; else r = "f"; if ( Character.isUpperCase(v.charAt(0)) ) r = r.toUpperCase(); while ( prep.expressionsmgmt.is_id_being_used(r) || Symbol.is_reserved(r) ) r = Character.toString((char) (r.charAt(0) + 1)); /* r = (String) JOptionPane.showInputDialog( (JFrame) table.getTopLevelAncestor(), "Enter an identifier not already being used in this" + " proof for replacing the selected variable:", "Enter an identifier", JOptionPane.QUESTION_MESSAGE, null, null, r ); */ r = JOptionPane.showInputDialog( "Enter an identifier not already being used in this" + " proof for replacing the selected variable:", r ); if ( r == null ) return false; if ( r.equals("") ) return note_error("What you entered was \"" + r + "\"."); if ( Symbol.is_reserved(r) ) return note_error("That symbol already means something here."); if ( prep.expressionsmgmt.is_id_being_used(r) ) return note_error("That identifier is already being used."); if ( !Character.isUnicodeIdentifierStart(r.charAt(0)) ) return note_error( "What you entered" + " isn't a valid alphanumeric identifier." ); for ( char r_ch : r.toCharArray() ) if ( !(Character.isUnicodeIdentifierPart(r_ch) // kludge until properly handle subscripts || r_ch == Symbol.SUBSCRIPT_1_UNICODE || r_ch == Symbol.SUBSCRIPT_2_UNICODE || r_ch == Symbol.SUBSCRIPT_3_UNICODE ) ) return note_error( "What you entered" + " isn't a valid alphanumeric identifier." ); prep.expressionsmgmt.add_skolem_id(r); rplcmnt_str = r; Expression arg = null; if ( !r_vars.isEmpty() ) { rplcmnt_str += '(' + (r_vars.size() == 1 ? r_vars.peek() : "...") + ')'; Expression args = new Expression(r_vars.pop()); while ( !r_vars.empty() ) args = new Expression( prep.expressionsmgmt .new_Symbol(Symbol.Specifier.COMMA), new Expression(r_vars.pop()), args ); arg = args.ensure_group(); // depending on that preferring parenthesizing } prep.quant.get_argument2() .replace_throughout_scope(v, new Expression(r, arg)); } boolean multiple_variables = quantifier.get_argument1() .op_spec_equals(Symbol.Specifier.COMMA); if ( prep.parent == quantifier ) prep.quant.this_structure_replace(prep.quant.get_argument2()); else prep.parent.this_structure_replace( prep.subexpr == prep.parent.get_argument2() ? prep.parent.get_argument1() : prep.parent.get_argument2() ); String narrative_base = prep.expr == prep.quant ? prep.selected_column_id == PB_TableModel.Column_ID.GOALS ? quantifier .op_spec_equals(Symbol.Specifier.FORALL) ? "Well, let an arbitrary value \"" + rplcmnt_str + "\" be given;" + "\nthen we should prove the following:" : "Removing that variable quantification" + "\nclarifies that to prove that formula," + "\nit will suffice to find " + (multiple_variables ? "values for the variables." : "a value for the variable." ) : quantifier .op_spec_equals(Symbol.Specifier.FORALL) ? "Removing that variable quantification" // clarifies that with that supposition/derivation, // we can assign + "\nclarifies that we can assign" + "\nany value" + (multiple_variables ? "s to those variables." : " to that variable." ) : "That formula indicates there exists" + "\nsome value say \"" + rplcmnt_str + "\" satisfying that" + "\nquantified " + (prep.quant == prep.expr ? "" : "(sub)" ) + "formula, i.e.:" : "Removing the selected variable quantification there" + "\nreduces that to the following:"; table_model().add( prep.selected_rows, prep.selected_column_id, // " = by quantifier-removal" narrative_base, "Consider formula " + prep.ref_num_name + ".\n" + narrative_base, prep.expr ); return true; } } static class Induct extends Ded_Action { Induct(/*ProofBuilder GUI_given,*/ JTable table_given) { super(/*GUI_given,*/ table_given); } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(event.getActionCommand()) : "appears_applicable(event.getActionCommand())"; */ if ( !note_sel_expr_rows_count(1) ) return false; Deduction_Prep prep = new Deduction_Prep(table); if ( prep.selected_column_id != PB_TableModel.Column_ID.GOALS ) return note_error( "This operation is applicable only to a goal formula." ); if ( table_model().get_transformationgoal_relationship( prep.selected_row ) != null ) return note_error( "That operation would interfere" + " with the sequence of transformations", "which you're in the middle of." ); if ( !note_sel_entire(prep) ) return false; if ( !prep.expr.op_spec_equals(Symbol.Specifier.QUANT_SEP) ) return note_error( "This operation is applicable only to" + " a universal quantification." ); Expression quantifier = prep.expr.get_argument1().ungroup(); if ( quantifier == null || !quantifier.op_spec_equals(Symbol.Specifier.FORALL) ) return note_error( "This operation is applicable only to" + " a universal quantification." ); // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; Expression restriction = (Expression) quantifier.get_argument1().clone(), // |clone()| here so can munge in there later var = null, goal = prep.expr.get_argument2().ungroup(); Symbol implies; if ( !restriction.op_spec_equals(Symbol.Specifier.GEQ) && !restriction .op_spec_equals(Symbol.Specifier.GREATER_THAN) && !restriction.op_spec_equals(Symbol.Specifier.IS_IN) && goal.op_spec_equals(Symbol.Specifier.IMPLIES) ) { var = restriction; restriction = goal.get_argument1().ungroup(); implies = goal.get_operator(); goal = goal.get_argument2().ungroup(); } else implies = prep.expressionsmgmt.new_Symbol(Symbol.Specifier.IMPLIES); Expression restricted_var = null, base_num = null, pre_base_num = null; switch ( restriction.get_operator().get_specifier() ) { case GEQ: restricted_var = restriction.get_argument1().ungroup(); base_num = restriction.get_argument2().ungroup(); break; case GREATER_THAN: restricted_var = restriction.get_argument1().ungroup(); pre_base_num = restriction.get_argument2().ungroup(); break; case LEQ: base_num = restriction.get_argument1().ungroup(); restricted_var = restriction.get_argument2().ungroup(); break; case LESS_THAN: pre_base_num = restriction.get_argument1().ungroup(); restricted_var = restriction.get_argument2().ungroup(); break; case IS_IN: restricted_var = restriction.get_argument1().ungroup(); if ( restriction.get_argument2().ungroup() .op_spec_equals(Symbol.Specifier.N_NUMBERS) ) base_num = new Expression( prep.expressionsmgmt.get_startNat1() ? 1 : 0 ); break; default: restriction = null; } if ( pre_base_num != null && pre_base_num.op_spec_equals(Symbol.Specifier.INT) ) base_num = new Expression(pre_base_num.get_val() + 1); if ( var == null ) var = restricted_var; else if ( !var.equivalent_form(restricted_var) ) // restriction == null; // but then would need additional // condition in next clause // or something base_num = null; if ( !(base_num != null && base_num.op_spec_equals(Symbol.Specifier.INT) && prep.expressionsmgmt.is_variable(var) ) ) restriction = null; if ( restriction == null ) return note_error( "Since induction applies to integers" + " starting at some point," + " you're supposed to indicate", "such a starting point" + " by having" + " an appropriate restriction, e.g. \"(" + prep.expressionsmgmt .get_spec_String(Symbol.Specifier.FORALL) + 'v' + Symbol.GEQ_UNICODE + "0)[P(v)]\".", // "", // doesn't work for blank line "(By the way, if you're going to restart your proof now," + " note that you may be able", "to avoid some retyping" + " if you copy your theorem here" + " to the system clipboard.)" ); String stepwise_option = "Stepwise induction"; String strong_option = "Strong induction"; // Complete // String cancel_option = "Cancel"; String[] options = { stepwise_option, strong_option /*, cancel_option */ }; String[] message = { "Do you want to invoke the typical stepwise induction,", "or strong induction a.k.a. complete induction?" }; String opt = (String) JOptionPane.showInputDialog( (JFrame) table.getTopLevelAncestor(), message, "Choose induction flavor", JOptionPane.QUESTION_MESSAGE, null, options, options[0] ); if ( opt == /* cancel_option */ null ) return false; String v = var.get_operator().get_text(); // FUTURE options: // stepwise: * prev: v, next: v+1 // * prev: v-1, next: v // strong: * prev: =l /\ u <= next_num' quantifier.get_argument1().this_structure_replace(var); Expression prev_hyp = goal; Expression next = new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.PLUS), var, new Expression(1) ).parenthesize(); Expression next_goal = (Expression) goal.clone(); next_goal.replace_throughout_scope(v, next); // People might generally not use |restriction| for stepwise proofs, // but such is technically necessary: // e.g. to prove (Ax>=4)[x^2 <= 2^x], without using the restriction // one would need to prove [n^2 <= 2^n] ==> [(n+1)^2 <= 2^(n+1)] // which is false for n = 2, // by constrast with the situation when the restriction is included: // [n^2 <= 2^n] /\ n >= 4 ==> [(n+1)^2 <= 2^(n+1)]; // even for proofs involving summations, to split off an (n+1) term, // one technically needs to ensure that (n+1) > STARTING_VALUE. // I plan to enable eliding/hiding of unused rows, // so people who avoid using the restriction // will still be able to have 'pretty' proofs. // OK here I think I will elide restrictions of the form n e N Symbol and = prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND); Expression result; if ( opt == stepwise_option ) { Expression base = (Expression) goal.clone(); base.replace_throughout_scope(v, base_num); prep.expr.get_argument2().this_structure_replace( new Expression( implies, restriction.op_spec_equals( Symbol.Specifier.IS_IN ) ? prev_hyp : new Expression( and, prev_hyp, restriction // |restriction_next| // (in strong, below) // would include // duplication of // base case ), next_goal) .ensure_group() ); result = new Expression(and, base, prep.expr); } else { // opt == strong_option String u = null; HashSet vars = prep.expressionsmgmt.variables_unquantified(prep.expr); if ( v.length() == 1 ) { char v_char = v.charAt(0); if ( 'b' <= v_char && v_char <= 'z' ) { u = Character.toString((char) (v_char - 1)); if ( vars.contains(u) ) u = null; } } if ( u == null ) { u = v; do u += "_small"; while ( vars.contains(u) ); } prep.expressionsmgmt.add_variable_id(u); Expression uar = new Expression(u); // "uar":"var"::"u"::"v" (;-) Expression restriction_next = (Expression) restriction.clone(); restriction_next.replace_throughout_scope(v, next); Expression restriction_prev = (Expression) restriction.clone(); restriction_prev.replace_throughout_scope(v, uar); prev_hyp.replace_throughout_scope(v, uar); Expression quantifier_prev = (Expression) prep.expr.get_argument1().clone(); quantifier_prev.replace_throughout_scope(v, uar); result = new Expression( prep.expr.get_operator(), prep.expr.get_argument1(), new Expression( implies, new Expression( and, new Expression( prep.expr.get_operator(), // QUANT_SEP quantifier_prev, new Expression( implies, new Expression( and, restriction_prev, new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.LEQ ), uar, var ) ), prev_hyp ).bracket() ), restriction_next ), next_goal ).bracket() ); } String narrative_base = //PB_TableModel.REDUCES_BY_ "Well, invoking " + (opt == stepwise_option ? "stepwise" : "strong" ) + " induction, we should prove the following:"; table_model().add( prep.selected_rows, PB_TableModel.Column_ID.GOALS, narrative_base, "Consider formula " + prep.ref_num_name + ".\n" + narrative_base, result ); return true; } } // for a while I tried having // this resolution action handle the // equivalence rule also // Resolve [more standard name in literature, Manna & Waldinger] // Match // Combine/Join/Merge/Integrate/Unite/Unify/Amalgamate // Consolidate/Coalesce/Compound/Put together/Add/Meld/Blend // Fuse/Flux/Melt into one/interfuse/interblend/Synthesize // Syncretize/Syndicate/Pair/Partner // mix/admix/commix/immix/intermix/commingle/immingle // intermingle/hash/hybridize/crossbreed/cross/interbreed // miscegenate/conjugate/splice/clinch // interconnect/interjoin/interdigitate/bind/splice/bundle static class Resolve extends Ded_Action { final static String RESOLVE_SELF_CMD = "Invoke bivalence for a proposition"; final static String RESOLVE_2ROWS_CMD = "Apply one formula to another matching one"; Resolve(/*ProofBuilder GUI_given,*/ JTable table_given) { super(/*GUI_given,*/ table_given); } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(event.getActionCommand()) : "appears_applicable(event.getActionCommand())"; */ boolean self = action_command == RESOLVE_SELF_CMD; if ( !note_sel_expr_rows_count(self ? 1 : 2) ) return false; Deduction_Prep prep0 = new Deduction_Prep(table, 0); /* P |- (P /\ Q) <--> Q : split, transform (P /\ Q), resolve P if ( table_model().get_transformationgoal_relationship( prep0.selected_row ) != null ) return note_error( "That operation would interfere" + " with the sequence of transformations", "which you're in the middle of." ); */ if ( self ) { if ( prep0.selected_id == null ) return note_error( "This operation is applicable only to a selection that is", "a simple propositional variable." ); // Consider skipping this error // to enable a decision procedure by Manna & Waldinger if ( !prep0.selected_id_occurs_both_polarities ) return note_error( /* "Due to conditions of logic, it won't", "be useful for you to try to use", "those two selected formulas together.", */ "For this operation, one of your selections needs to be", "inside an even number of explicit or implicit negations,", "and another selection inside an odd number", "(or a selection can be inside an equivalence).", "(Suppositions/derivations start with one implicit negation.)" ); } Deduction_Prep prep1 = new Deduction_Prep(table, self ? 0 : 1); /* P |- (P /\ Q) <--> Q : split, transform (P /\ Q), resolve P if ( table_model().get_transformationgoal_relationship( prep1.selected_row ) != null ) return note_error( "That operation would interfere" + " with the sequence of transformations", "which you're in the middle of." ); */ if ( self && prep0.polarity != 0 ) // REALLY SHOULD FIND AN OPPOSITE-POLARITY OCCURRENCE // kludge: prep1.polarity *= -1; if ( !note_parts_consistent(prep0.selected_row, prep1.selected_row)) return false; if ( !prep0.selection_boolean() || !prep1.selection_boolean() ) return note_error( "For this operation, each of your selections", "needs to be an expression that would be true or false,", "not a domain value " + "(such as a numerical value or an object)." ); // Note below won't try using internals of axiom // for both selections. if ( prep1.seems_axiomatic() && !prep0.seems_axiomatic() || prep1.selected_column_id == PB_TableModel.Column_ID.SUPPS && prep0.selected_column_id == PB_TableModel.Column_ID.GOALS /* || prep1.selected_column_id == prep0.selected_column_id && prep1.polarity < 0 && prep0.polarity > 0 */ || prep0.selected_column_id == PB_TableModel.Column_ID.GOALS && prep1.selected_column_id == PB_TableModel.Column_ID.GOALS && prep1.polarity < 0 && prep0.polarity > 0 || prep0.selected_column_id == PB_TableModel.Column_ID.SUPPS && prep1.selected_column_id == PB_TableModel.Column_ID.SUPPS && prep1.polarity > 0 && prep0.polarity < 0 ) { // switch |prep0|, |prep1|: Deduction_Prep prep_hold = prep0; prep0 = prep1; prep1 = prep_hold; } // facilitate using material inside a universally quantified // supposition/derivation --- avoiding requiring removing the quantifier: if ( !prep0.try_expr_suq_free() ) prep1.try_expr_suq_free(); HashSet vars0 = note_sel_unquant_vars(prep0); if ( vars0 == null || note_sel_unquant_vars(prep1) == null ) return false; // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; Expression expr0 = (Expression) prep0.expr.clone(), subexpr0 = expr0.get_subexpr(prep0.start, prep0.limit), expr1 = (Expression) prep1.expr.clone(), subexpr1 = expr1.get_subexpr(prep1.start, prep1.limit); HashMap g_vars0 = standardize_variables_apart(vars0, expr0); LinkedList unifier = prep1.expressionsmgmt .unify(subexpr0, subexpr1, expr0, expr1); if ( unifier == null && prep0.subexpr.op_spec_equals( prep0.expressionsmgmt.get_lognegsymspec() ) ) { vars0 = note_sel_unquant_vars(prep0); expr0 = (Expression) prep0.expr.clone(); subexpr0 = expr0.get_subexpr(prep0.start, prep0.limit).get_argument1(); expr1 = (Expression) prep1.expr.clone(); subexpr1 = expr1.get_subexpr(prep1.start, prep1.limit); g_vars0 = standardize_variables_apart(vars0, expr0); if ( (unifier = prep1.expressionsmgmt .unify(subexpr0, subexpr1, expr0, expr1) ) != null ) prep0.polarity *= -1; } if ( unifier == null && prep1.subexpr.op_spec_equals( prep1.expressionsmgmt.get_lognegsymspec() ) ) { vars0 = note_sel_unquant_vars(prep0); expr0 = (Expression) prep0.expr.clone(); subexpr0 = expr0.get_subexpr(prep0.start, prep0.limit); expr1 = (Expression) prep1.expr.clone(); subexpr1 = expr1.get_subexpr(prep1.start, prep1.limit).get_argument1(); g_vars0 = standardize_variables_apart(vars0, expr0); if ( (unifier = prep1.expressionsmgmt .unify(subexpr0, subexpr1, expr0, expr1) ) != null ) prep1.polarity *= -1; } if ( unifier == null && prep0.subexpr.op_spec_equals(Symbol.Specifier.IMPLIES) ) { vars0 = note_sel_unquant_vars(prep0); expr0 = (Expression) prep0.expr.clone(); subexpr0 = // trying arg#2 first because that might be more useful // when goal-directed expr0.get_subexpr(prep0.start, prep0.limit).get_argument2(); expr1 = (Expression) prep1.expr.clone(); subexpr1 = expr1.get_subexpr(prep1.start, prep1.limit); g_vars0 = standardize_variables_apart(vars0, expr0); unifier = prep1.expressionsmgmt .unify(subexpr0, subexpr1, expr0, expr1); if ( unifier == null ) { vars0 = note_sel_unquant_vars(prep0); expr0 = (Expression) prep0.expr.clone(); subexpr0 = expr0.get_subexpr(prep0.start, prep0.limit) .get_argument1(); expr1 = (Expression) prep1.expr.clone(); subexpr1 = expr1.get_subexpr(prep1.start, prep1.limit); g_vars0 = standardize_variables_apart(vars0, expr0); if ( (unifier = prep1.expressionsmgmt .unify(subexpr0, subexpr1, expr0, expr1) ) != null ) prep0.polarity *= -1; } } if ( unifier == null && prep1.subexpr.op_spec_equals(Symbol.Specifier.IMPLIES) ) { vars0 = note_sel_unquant_vars(prep0); expr0 = (Expression) prep0.expr.clone(); subexpr0 = expr0.get_subexpr(prep0.start, prep0.limit); expr1 = (Expression) prep1.expr.clone(); subexpr1 = // trying arg#2 first because that might be more useful // when goal-directed expr1.get_subexpr(prep1.start, prep1.limit).get_argument2(); g_vars0 = standardize_variables_apart(vars0, expr0); unifier = prep1.expressionsmgmt .unify(subexpr0, subexpr1, expr0, expr1); if ( unifier == null ) { vars0 = note_sel_unquant_vars(prep0); expr0 = (Expression) prep0.expr.clone(); subexpr0 = expr0.get_subexpr(prep0.start, prep0.limit); expr1 = (Expression) prep1.expr.clone(); subexpr1 = expr1.get_subexpr(prep1.start, prep1.limit).get_argument1(); g_vars0 = standardize_variables_apart(vars0, expr0); if ( (unifier = prep1.expressionsmgmt .unify(subexpr0, subexpr1, expr0, expr1) ) != null ) prep1.polarity *= -1; } } if ( unifier == null ) return note_error("Your two selections don't match."); // Consider skipping this error when |self| // to enable a decision procedure by Manna & Waldinger if ( prep0.polarity * prep1.polarity > 0 ) return note_error( /* "Due to conditions of logic, it won't", "be useful for you to try to use", "those two selected formulas together.", */ "For this operation, one of your selections needs to be", "inside an even number of explicit or implicit negations,", "and another selection inside an odd number", "(or a selection can be inside an equivalence).", "(Suppositions/derivations start with one implicit negation.)" ); if ( prep0.parent != null && prep0.parent.op_spec_equals(Symbol.Specifier.EQUIV) || prep1.parent != null && prep1.parent.op_spec_equals(Symbol.Specifier.EQUIV) ) { Toolkit.getDefaultToolkit().beep(); String[] message = { "Sometimes, applying bivalence to one side of an equivalence" + " would yield useless junk;", "instead, really using the equivalence" + " might yield a more useful result.", /* Do you */ "Want to go ahead and do this applying bivalence anyway?" }; // Consider making "No" the default. if ( JOptionPane.showConfirmDialog( (JFrame) table.getTopLevelAncestor(), message, "Apply bivalence instead of really using equivalence?", JOptionPane.YES_NO_OPTION ) == JOptionPane.NO_OPTION ) return false; } // proceeding prep0.expr = expr0; prep0.subexpr = subexpr0; prep1.expr = expr1; prep1.subexpr = subexpr1; prep0.entry.try_select( prep0.subexpr.get_begin(), prep0.subexpr.get_limit() ); prep1.entry.try_select( prep1.subexpr.get_begin(), prep1.subexpr.get_limit() ); // considering swapping |prep0|,|prep1| which may be // deviating from Manna & Waldinger so things will look better // e.g. with suppositions |Q --> R| and |P \/ Q|, want result // |P \/ R| rather than |R \/ P| if ( !self // probably doesn't matter && prep0.selected_column_id == prep1.selected_column_id && prep0.subexpr.get_limit() <= prep0.expr.get_operator().get_begin() && prep1.subexpr.get_begin() >= prep1.expr.get_operator().get_limit() ) { Deduction_Prep hold = prep0; prep0 = prep1; prep1 = hold; } if ( prep0.selected_id != null ) { prep0.expr .replace_throughout_scope( prep0.selected_id, prep0.expressionsmgmt.new_Symbol( prep0.polarity <= prep1.polarity ? Symbol.Specifier.FALSE : Symbol.Specifier.TRUE ) ); prep1.expr .replace_throughout_scope( prep0.selected_id, prep0.expressionsmgmt.new_Symbol( prep0.polarity <= prep1.polarity ? Symbol.Specifier.TRUE : Symbol.Specifier.FALSE ) ); } else { prep0.subexpr.this_structure_replace( prep0.expressionsmgmt.new_Symbol( prep0.polarity <= prep1.polarity ? Symbol.Specifier.FALSE : Symbol.Specifier.TRUE ) ); prep1.subexpr.this_structure_replace( prep1.expressionsmgmt.new_Symbol( prep0.polarity <= prep1.polarity ? Symbol.Specifier.TRUE : Symbol.Specifier.FALSE ) ); } //prep0.expr.simplify(); String narrative_base_self = "hecking the alternatives" + "\n\tof \"" + prep1.expressionsmgmt.get_spec_String(Symbol.Specifier.FALSE) + "\"/\"" + prep1.expressionsmgmt.get_spec_String(Symbol.Specifier.TRUE) + "\" for \"" + prep0.selected_id + '\"'; String narrative_base_2rows_independent = "Applying formula " + prep0.ref_num_name + " to formula " + prep1.ref_num_name; /* + "\nyields:"; */ return conclude_two_row_ded( prep0, prep1, !self, g_vars0, unifier, self ? table_model().REDUCES_BY_ + 'c' + narrative_base_self : /*table_model().hilbert_style ? narrative_base_2rows_independent :*/ null, self ? 'C' + narrative_base_self + "/nin formula " + prep0.ref_num_name + " yields:" : narrative_base_2rows_independent ); } } static class Conjoin extends Ded_Action { Conjoin(/*ProofBuilder GUI_given,*/ JTable table_given) { super(/*GUI_given,*/ table_given); } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(event.getActionCommand()) : "appears_applicable(event.getActionCommand())"; */ if ( !note_sel_expr_rows_count(2) ) return false; Deduction_Prep prep0 = new Deduction_Prep(table, 0); if ( !note_sel_entire(prep0) ) return false; Deduction_Prep prep1 = new Deduction_Prep(table, 1); if ( !note_sel_entire(prep1) ) return false; if ( !note_parts_consistent(prep0.selected_row, prep1.selected_row)) return false; if ( prep0.selected_column_id != PB_TableModel.Column_ID.SUPPS || prep1.selected_column_id != PB_TableModel.Column_ID.SUPPS ) return note_error( "This operation is applicable" + " only to two suppositions/derivations." ); // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; HashSet vars0_1 = prep0.expressionsmgmt.variables_unquantified(prep0.subexpr); vars0_1.remove( prep1.expressionsmgmt.variables_unquantified(prep1.subexpr) ); // standardizing variables apart // using "g####" variables as with |(gensym)| in old LISP (;-) int g_index = 0; // to really copy old LISP, |static| for ( String v : vars0_1 ) { String g_; do g_ = "g" + ++g_index; while ( prep0.expressionsmgmt.is_id_being_used(g_) ); prep0.expressionsmgmt.add_variable_id(g_); prep0.expr.replace_throughout_scope(v, g_); } Expression result = new Expression( prep0.expressionsmgmt .new_Symbol(Symbol.Specifier.AND), prep0.expr.ensure_group(), prep1.expr.ensure_group() ); /* result.simplify(); if ( result.op_spec_equals(Symbol.Specifier.TRUE) ) return note_error("The result here was inconsequential."); */ String narrative_flowing_with_preceding_row = table_model().REDUCES_BY_ + "conjoining with " + prep0.ref_num_name; String narrative_independent = "Conjoining " + prep0.ref_num_name + " with " + prep1.ref_num_name + " yields:"; table_model().add( prep0.selected_rows, PB_TableModel.Column_ID.SUPPS, narrative_flowing_with_preceding_row, narrative_independent, result ); return true; } } // Substitute_Using_Equiv_or_Comparison // Substitute_Using_Equation_or_C // Change_According_to_Reln_or_Equiv static class Apply_Equation_Equivalence_or_Comparison extends Ded_Action { final static String APPLY_EQ_CMD = "Apply equation or equivalence"; final static String APPLY_CMP_CMD = "Apply comparison (\"<\", \"" + Symbol.LEQ_UNICODE + "\", \">\", or \"" + Symbol.GEQ_UNICODE + "\")"; Apply_Equation_Equivalence_or_Comparison( //ProofBuilder GUI_given, JTable table_given ) { super(/*GUI_given,*/ table_given); } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(event.getActionCommand()) : "appears_applicable(event.getActionCommand())"; */ if ( action_command == APPLY_EQ_CMD && table.getSelectedRowCount() == 1 ) { Canonical_Eqs canonical_eqs = new Canonical_Eqs(table); if ( get_actingvsjustcheckingapplicability() && canonical_eqs.get_consideration() ) canonical_eqs.setVisible(true); return canonical_eqs.get_consideration(); } if ( table.getSelectedRowCount() != 2 ) return note_error( "This operation needs exactly 1 or 2 rows" + " to be selected." ); Deduction_Prep prep0 = new Deduction_Prep(table, 0); Deduction_Prep prep1 = new Deduction_Prep(table, 1); if ( !note_parts_consistent(prep0.selected_row, prep1.selected_row)) return false; /* if ( !prep0.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) && !prep1.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) ) */ // facilitate using material inside a universally quantified // supposition/derivation // --- avoiding requiring removing the quantifier: if ( !prep0.try_expr_suq_free() ) prep1.try_expr_suq_free(); /* See below for prep_reln_arg2.try_expr_suq_free(); */ int selected_arg = 0; if ( !prep0.subexpr.get_operator().is_basic_transitive_comparator() && !prep1.subexpr.get_operator().is_basic_transitive_comparator() ) if ( prep0.parent != null && prep0.parent.get_operator().is_basic_transitive_comparator() ) { selected_arg = prep0.subexpr == prep0.parent.get_argument1().ungroup() ? 1 : 2; prep0.subexpr = prep0.parent; } else if ( prep1.parent != null && prep1.parent.get_operator() .is_basic_transitive_comparator() ) { selected_arg = prep1.subexpr == prep1.parent.get_argument1().ungroup() ? 1 : 2; prep1.subexpr = prep1.parent; } // then more than half of the following work is unnecessary; // but why muss the code? Deduction_Prep prep_reln_arg1, prep_replacee_arg1, prep_reln_arg2, prep_replacee_arg2; if ( prep0.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) || !prep1.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) && Symbol.is_transitive_numeric_comparator( prep0.subexpr.get_operator().get_specifier() ) ) { prep_reln_arg1 = prep0; prep_reln_arg2 = new Deduction_Prep(table, 0); /* See below for prep_reln_arg2.try_expr_suq_free(); */ prep_replacee_arg1 = prep1; prep_replacee_arg2 = new Deduction_Prep(table, 1); } else if ( prep1.subexpr.get_operator() .is_basic_transitive_comparator() ) { prep_reln_arg1 = prep1; prep_reln_arg2 = new Deduction_Prep(table, 1); /* See below for prep_reln_arg2.try_expr_suq_free(); */ prep_replacee_arg1 = prep0; prep_replacee_arg2 = new Deduction_Prep(table, 0); } else return note_error( "For this operation, one of your selections" + " needs to be an equation, an equivalence, or a comparison", "(and your other selection needs to match one" + " of the sides of the equation or equivalence or comparison)." ); /* if ( !prep_reln_arg2.subexpr .op_spec_equals(Symbol.Specifier.EQUALS) ) */ prep_reln_arg2.try_expr_suq_free(); if ( !prep_reln_arg2 .subexpr.equivalent_form(prep_reln_arg1.subexpr) ) prep_reln_arg2.subexpr = prep_reln_arg2.parent; if ( (prep_reln_arg1.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) || prep_reln_arg1.subexpr .op_spec_equals(Symbol.Specifier.EQUALS) ) ^ action_command == APPLY_EQ_CMD ) return note_error( "For this operation, one of your selections needs to be " + (action_command == APPLY_EQ_CMD ? "an equation or an equivalence." : "a comparison." ) ); // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; HashSet vars_reln = note_sel_unquant_vars(prep_reln_arg1); if ( vars_reln == null //|| note_sel_unquant_vars(prep_replacee_arg1) == null ) return false; /* HashSet replacee_bound_vars = prep_replacee_arg1.scoped_dependent_vars.clone(); prep_replacee_arg1.scoped_freeable_vars) prep_replacee_arg1.expressionsmgmt.variables_unquantified( prep_replacee_arg1.subexpr ); */ // standardizing variables apart // using "g####" variables as with |(gensym)| in old LISP (;-) int g_index = 0; // to really copy old LISP, |static| HashMap g_vars_reln = new HashMap(); // for returning "g####" variables to their originals for ( String v : vars_reln ) { String g_; do g_ = "g" + ++g_index; while ( prep_reln_arg1.expressionsmgmt.is_id_being_used(g_) ); prep_reln_arg1.expressionsmgmt.add_variable_id(g_); prep_reln_arg1.expr.replace_throughout_scope(v, g_); prep_reln_arg2.expr.replace_throughout_scope(v, g_); g_vars_reln.put(g_, v); } LinkedList unifier_arg1 = selected_arg == 2 ? null : prep_reln_arg1.expressionsmgmt .unify(prep_reln_arg1.subexpr.get_argument1(), prep_replacee_arg1.subexpr, prep_reln_arg1.expr, prep_replacee_arg1.expr, prep_replacee_arg1.scoped_dependent_vars // SOUNDNESS MAY ACTUALLY REQUIRE // ADDING |scoped_freeable_vars| ALSO ); LinkedList unifier_arg2 = selected_arg == 1 ? null : prep_reln_arg2.expressionsmgmt .unify(prep_reln_arg2.subexpr.get_argument2(), prep_replacee_arg2.subexpr, prep_reln_arg2.expr, prep_replacee_arg2.expr, prep_replacee_arg2.scoped_dependent_vars // SOUNDNESS MAY ACTUALLY REQUIRE // ADDING |scoped_freeable_vars| ALSO ); String word_for_relation = prep_reln_arg1.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) ? "equivalence" : prep_reln_arg1.subexpr.op_spec_equals(Symbol.Specifier.EQUALS) ? "equation" : "comparison"; if ( unifier_arg1 == null && unifier_arg2 == null ) return note_error( selected_arg != 0 // (safely) ? "Your two selections don't properly match." : "Neither side of the " + word_for_relation + " that you selected" // (safely) + " properly matches the other expression that you selected." ); if ( prep_reln_arg1.polarity > 0 ) return note_error( /* "Due to conditions of logic, it won't", "be useful for you to try to use", "those two selected formulas together.", */ "For this operation, the selected " + word_for_relation + " needs to be", "inside an odd number of explicit or implicit negations", "(or the selected " + word_for_relation + " can be " + "inside an equivalence).", "(Suppositions/derivations start with one implicit negation.)" ); if ( !(prep_reln_arg1.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) || prep_reln_arg1.subexpr .op_spec_equals(Symbol.Specifier.EQUALS) ) && prep_replacee_arg1.polarity == 0 ) return note_error( "The term you selected appears to be within the scope" + " of a \"" + prep_reln_arg1.expressionsmgmt .get_spec_String(Symbol.Specifier.EQUIV) + "\" operator.", "You need to use the Rewriting Deduction" + " to expand away that operator", "before you can apply a comparison to a term in its scope." ); // I don't know why I had this commenting-out: // if ( /* unifier_arg1 != null && */ // short-circuit if ( unifier_arg1 != null && // short-circuit !Symbol.basic_transitive_comparator_applicable_to( prep_reln_arg1.subexpr.get_operator().get_specifier(), prep_replacee_arg1.relationship, prep_replacee_arg1.polarity ) ) unifier_arg1 = null; // I don't know why I had this commenting-out: // if ( /* unifier_arg2 != null && */ // short-circuit if ( unifier_arg2 != null && // short-circuit !Symbol.basic_transitive_comparator_applicable_to( Symbol.reverse_numeric_comparator( prep_reln_arg2.subexpr.get_operator() .get_specifier() ), prep_replacee_arg2.relationship, prep_replacee_arg2.polarity ) ) unifier_arg2 = null; if ( unifier_arg1 == null && unifier_arg2 == null ) return note_error( "It's not clear" + " that it's legitimate to apply that comparison", "to that term." + " If appropriate, try other, less restricted deductions", "(such as \"Apply one formula to another matching one\")." ); if ( unifier_arg1 != null && unifier_arg2 != null // happens with e.g. commutativity (equation): // (Ax,y)[x*y = y*x] && !prep_replacee_arg1.expr.equivalent_form( prep_replacee_arg2.expr ) ) { String arg1_option = "match left-hand side, yield right-hand side"; String arg2_option = "match right-hand side, yield left-hand side"; String cancel_option = "Cancel"; String[] options = { arg1_option, arg2_option, cancel_option }; String[] message = { "Um, did you want to match the " + word_for_relation + "'s", "left-hand side to the other expression," + " yielding the " + word_for_relation + "'s right-hand side;", "or did you want to match the " + word_for_relation + "'s", "right-hand side to the expression," + " yielding the " + word_for_relation + "'s left-hand side?" }; String opt = (String) JOptionPane.showInputDialog( (JFrame) table.getTopLevelAncestor(), message, "Choose side(s)", // (;-) JOptionPane.QUESTION_MESSAGE, null, options, options[0] ); if ( opt == arg1_option ) unifier_arg2 = null; else if ( opt == arg2_option ) unifier_arg1 = null; else return false; } // proceeding LinkedList unifier; Deduction_Prep prep_reln, prep_replacee; Symbol.Specifier relationship_applying; Expression rplcmnt; if ( unifier_arg1 != null ) { unifier = unifier_arg1; prep_reln = prep_reln_arg1; relationship_applying = prep_reln.subexpr.get_operator().get_specifier(); prep_replacee = prep_replacee_arg1; rplcmnt = prep_reln.subexpr.get_argument2(); } else { unifier = unifier_arg2; prep_reln = prep_reln_arg2; relationship_applying = Symbol.reverse_numeric_comparator( prep_reln.subexpr.get_operator().get_specifier() ); prep_replacee = prep_replacee_arg2; rplcmnt = prep_reln.subexpr.get_argument1(); } // in case did |try_expr_suq_free()|: prep_reln.entry.try_select( prep_reln.subexpr.get_begin(), prep_reln.subexpr.get_limit() ); prep_replacee.entry.try_select( prep_replacee.subexpr.get_begin(), prep_replacee.subexpr.get_limit() ); if ( relationship_applying != Symbol.Specifier.EQUALS && relationship_applying != Symbol.Specifier.EQUIV ) prep_replacee.subexpr .this_structure_replace(rplcmnt.ensure_group()); else prep_replacee.expr.replace_throughout_ungrp( (Expression) prep_replacee.subexpr.clone(), // |clone()| to preserve: // replacing changes! rplcmnt.ensure_group() ); String acknowledgement_support = ""; if ( relationship_applying != Symbol.Specifier.EQUALS && relationship_applying != Symbol.Specifier.EQUIV && prep_replacee.relationship_support != null ) { prep_replacee.relationship_support .remove(prep_reln.selected_row); if ( !prep_replacee.relationship_support.isEmpty() ) { acknowledgement_support = "\n\tand also establishing factors' nonnegativity via"; String separator = " "; for ( int supporting_row_index : prep_replacee.relationship_support ) { Object comment = table_model().getValueAt( supporting_row_index, PB_TableModel.Column_ID.COMMENTS.ordinal() ); acknowledgement_support += separator + ((String) table_model().getValueAt( supporting_row_index, PB_TableModel .Column_ID .REF_NUMS.ordinal() ) ) .trim() + (comment != null ? " " + comment : ""); separator = ", "; } } } String narrative_base_flowing_with_preceding_row = (prep_reln.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) || prep_reln.subexpr .op_spec_equals(Symbol.Specifier.EQUALS) ? table_model().EQUIV_BY_ : table_model().REDUCES_BY_ ) + prep_reln.ref_num_name + acknowledgement_support; Symbol.Specifier transformationgoal_relationship = table_model().get_transformationgoal_relationship( prep_replacee.selected_row ); if ( !(transformationgoal_relationship == Symbol.Specifier.EQUIV || prep_replacee.expr.get_operator().spec_yields_boolean() || prep_replacee.expr == prep_replacee.subexpr && relationship_applying == Symbol.Specifier.EQUIV // catching e.g. "P" when not transforming ) ) narrative_base_flowing_with_preceding_row = table_model().SPACES_AT_FRONT_OF_EQUALS_ETC_BY_ + table_model().get_expressionsmgmt() .get_spec_String(relationship_applying) + table_model().SPACES_BY_ + prep_reln.ref_num_name + acknowledgement_support; String narrative_base_independent = "Applying the " + (prep_reln.subexpr != prep_reln.expr ? "selected " : "" ) + word_for_relation + " in formula " + prep_reln.ref_num_name + "\nto" + (prep_replacee.subexpr != prep_replacee.expr ? " the selection in" : "" ) + " formula " + prep_replacee.ref_num_name + acknowledgement_support; /* + "\nyields:"; */ prep_reln.subexpr.this_structure_replace( prep_reln.expressionsmgmt.new_Symbol(Symbol.Specifier.FALSE) ); //prep_reln.expr.simplify(); /* if ( prep_replacee.transformationgoal_relationship != null && prep_replacee.transformationgoal_relationship != Symbol.Specifier.EQUIV ) */ if ( prep_replacee.expr.ungroup().get_operator().spec_yields_domainval() ) // doing transformation { prep_reln.expressionsmgmt.simplify(prep_reln.expr); /* System.err.println("prep_reln.expr.ungroup():\n" + prep_reln.expr.ungroup().debug_info()); */ if ( !prep_reln.expr.ungroup() .op_spec_equals( prep_reln.selected_column_id == PB_TableModel.Column_ID.SUPPS ? Symbol.Specifier.FALSE : Symbol.Specifier.TRUE ) ) return note_error( "To use that " + word_for_relation + " there, you would first need to clear", "material such as preconditions attached to it." ); } if ( relationship_applying == Symbol.Specifier.LESS_THAN || relationship_applying == Symbol.Specifier.GREATER_THAN ) table_model() .note_achieving_strict_step_for_transforming( prep_replacee.selected_row ); if ( prep_replacee.relation != null && prep_replacee.polarity == Deduction_Prep.SOUTH_POLARITY ) { Symbol.Specifier replacee_reln_spec = prep_replacee.relation.get_operator().get_specifier(); if ( Symbol.comparator_is_strong(relationship_applying) // != ^ Symbol.comparator_is_strong(replacee_reln_spec) ) { replacee_reln_spec = prep_replacee.polarity < 0 ? Symbol.comparator_strengthen( prep_replacee.relation .get_operator().get_specifier() ) : Symbol.comparator_weaken( prep_replacee.relation .get_operator().get_specifier() ); if ( prep_replacee.relation.get_operator().get_specifier() != replacee_reln_spec ) prep_replacee.relation.this_structure_replace( prep_replacee.expressionsmgmt .new_Symbol(replacee_reln_spec), prep_replacee.relation.get_argument1(), prep_replacee.relation.get_argument2() ); } } return conclude_two_row_ded( prep_reln, prep_replacee, g_vars_reln, unifier, prep_reln.selected_row < prep_replacee.selected_row ? narrative_base_flowing_with_preceding_row : "Applying that " + word_for_relation + " to formula " + prep_replacee.ref_num_name, /* + "\nyields:", */ narrative_base_independent ); } } // useful if deleted simplification of a row static class Try_Simplify extends Ded_Action { Try_Simplify(/*ProofBuilder GUI_given,*/ JTable table_given) { super(/*GUI_given,*/ table_given); } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(event.getActionCommand()) : "appears_applicable(event.getActionCommand())"; */ if ( !note_sel_expr_rows_count(1) ) return false; Deduction_Prep prep = new Deduction_Prep(table); if ( !note_sel_entire(prep) ) return false; /* // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; */ if ( !prep.expressionsmgmt.simplify(prep.expr) || prep.entry.expr_equiv_form(prep.expr) ) return note_error( "Actually, no simplifications are known to be applicable" + " to that formula." ); // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; table_model().add( prep.selected_rows, prep.selected_column_id, /* "That formula can be simplified" + "\nto the following:", */ table_model().EQUIV_BY_ + "simplifying", // "simplification(s)" "Simplifying " + prep.ref_num_name + " yields:", prep.expr ); return true; } } static class Transform extends Ded_Action { Transform(/*ProofBuilder GUI_given,*/ JTable table_given) { super(/*GUI_given,*/ table_given); } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(event.getActionCommand()) : "appears_applicable(event.getActionCommand())"; */ if ( !note_sel_expr_rows_count(1) ) return false; Deduction_Prep prep = new Deduction_Prep(table); if ( prep.selected_column_id != PB_TableModel.Column_ID.GOALS ) return note_error( "This operation is applicable only to a goal formula." ); if ( table_model().get_transformationgoal_relationship( prep.selected_row ) != null ) return note_error( "That operation would interfere" + " with the sequence of transformations", "which you're in the middle of." ); if ( !note_sel_entire(prep) ) return false; if ( !prep.expr.get_operator().is_basic_transitive_comparator() ) return note_error( "This operation is applicable only to an equation" + " or an equivalence (a.k.a. a biimplication)", "or a comparison (\"" + Symbol.LEQ_UNICODE + "\" or \"<\" or \"" + Symbol.GEQ_UNICODE + "\" or \">\")." ); // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; String lhs_option = "work on left-hand side"; String rhs_option = "work on right-hand side"; // String cancel_option = "Cancel"; String[] options = { lhs_option, rhs_option /*, cancel_option */ }; String[] message = { "Do you want to transform the left-hand side" + " to the right-hand side,", "or do you want to transform the right-hand side" + " to the left-hand side?" }; String opt = (String) JOptionPane.showInputDialog( (JFrame) table.getTopLevelAncestor(), message, "Choose side to transform", // "Choose sides" (;-) JOptionPane.QUESTION_MESSAGE, null, options, options[0] ); if ( opt == /* cancel_option */ null ) return false; String narrative1, narrative2; if ( opt == lhs_option ) { narrative1 = "We'll work on transforming the left-hand side of "; narrative2 = "\nto the right-hand side as follows:"; } else { narrative1 = "We'll work on transforming the right-hand side of "; narrative2 = "\nto the left-hand side as follows:"; } LinkedList exprs_buf = new LinkedList(); exprs_buf.add( opt == lhs_option ? prep.expr.get_argument1().ungroup() : prep.expr.get_argument2().ungroup() ); /* table_model().add( prep.selected_rows, PB_TableModel.Column_ID.GOALS, narrative1 + "that" + narrative2, narrative1 + "formula " + prep.ref_num_name + narrative2, opt == lhs_option ? prep.expr.get_argument1().ungroup() : prep.expr.get_argument2().ungroup() ); */ table_model().add_subparts( prep.selected_row, PB_TableModel.Column_ID.GOALS, narrative1 + "formula " + prep.ref_num_name + narrative2, exprs_buf ); if ( table_model().get_addedrowindex() < 0 ) return false; table_model() .note_transformation_goal( table_model().get_addedrowindex(), prep.selected_row, opt == rhs_option ? Symbol.reverse_numeric_comparator( prep.subexpr.get_operator().get_specifier() ) : prep.subexpr.get_operator().get_specifier(), (opt == rhs_option ? prep.expr.get_argument1() : prep.expr.get_argument2() ) .ungroup() ); return true; } } static class Rewrite_Using_Basic_Algebra_Or_Such extends Ded_Action { private User_Entry_Dialog user_entry_dialog; Rewrite_Using_Basic_Algebra_Or_Such( //ProofBuilder GUI_given, JTable table_given, User_Entry_Dialog user_entry_dialog_given ) { super(/*GUI_given,*/ table_given); user_entry_dialog = user_entry_dialog_given; } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see error messages if any. */ if ( !note_sel_expr_rows_count(1) ) return false; Deduction_Prep prep = preps[0]; /* if ( !prep.subexpr.ungroup().get_operator().spec_yields_domainval() ) { // spec_arithmetic // spec_algebraic return note_error( "This operation is applicable only to arithmetic expressions." ); } */ // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; Expression rplcmnt = user_entry_dialog.obtain_smply_eq_rplcmnt( prep.subexpr, prep.subexpr_text ); if ( rplcmnt == null ) return false; prep.subexpr.this_structure_replace(rplcmnt); String narrative_base_flowing_with_preceding_row = (table_model().get_transformationgoal_relationship( prep.selected_row ) == Symbol.Specifier.EQUIV || prep.expr.get_operator().spec_yields_boolean() ? table_model().EQUIV_BY_ : table_model().EQUALS_BY_ ) + "basic algebra/arithmetic"; String narrative_base_independent = "Applying basic algebra" + " to" + (prep.subexpr != prep.expr ? " the selection in" : "") + " formula " + prep.ref_num_name + " yields:"; table_model().add( prep.selected_rows, prep.selected_column_id, // " = by quantifier-removal" narrative_base_flowing_with_preceding_row, narrative_base_independent + "formula " + prep.ref_num_name + " yields:", prep.expr ); return true; } } static class Instantiate_Variable extends Ded_Action { private User_Entry_Dialog user_entry_dialog; Instantiate_Variable( //ProofBuilder GUI_given, JTable table_given, User_Entry_Dialog user_entry_dialog_given ) { super(/*GUI_given,*/ table_given); user_entry_dialog = user_entry_dialog_given; } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(event.getActionCommand()) : "appears_applicable(event.getActionCommand())"; */ if ( !note_sel_expr_rows_count(1) ) return false; Deduction_Prep prep = new Deduction_Prep(table); if ( table_model().get_transformationgoal_relationship( prep.selected_row ) != null ) return note_error( "That operation would interfere" + " with the sequence of transformations", "which you're in the middle of." ); if ( !prep.expressionsmgmt.is_variable(prep.subexpr) && !prep.subexpr.op_spec_equals(Symbol.Specifier.QUANT_SEP) && !prep.subexpr.op_spec_equals(Symbol.Specifier.FORALL) && !prep.subexpr.op_spec_equals(Symbol.Specifier.EXISTS) ) return note_error( "To apply this operation, you need to select a variable", "(or a quantifier)." ); //assert(quantifier.is_quantifier()); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.QUANT_SEP) ) { prep.quant = prep.subexpr; prep.parent = prep.subexpr; prep.subexpr = prep.subexpr.get_argument1(); // then one of the following |if|s should fire: } if ( prep.subexpr.is_group() && prep.subexpr.get_operator().get_text().equals("(") ) { prep.parent = prep.subexpr; //prep.subexpr = prep.subexpr.get_argument1(); prep.subexpr = prep.subexpr.ungroup(); // then the following |if| should fire: } if ( prep.subexpr.get_operator().is_quantifier() ) { // subexpr == quantifier prep.parent = prep.subexpr; prep.subexpr = prep.subexpr.get_argument1(); } prep.subexpr_text = prep.entry.get_text().substring( prep.subexpr.get_begin(), prep.subexpr.get_limit() ); LinkedList var_exprs = prep.subexpr.multiary_op_args(Symbol.Specifier.COMMA); if ( prep.quant != null ) { Expression quantifier = prep.quant.get_argument1().ungroup(); if ( prep.subexpr.get_operator().is_relation() || prep.parent != null && prep.parent.get_operator().is_relation() ) return note_error( "It would clarify matters if you would first apply the" + " canonical equivalence", "to expand the relativized quantification" + " at your selection into", "a more basic quantification plus a" + (quantifier .op_spec_equals(Symbol.Specifier.FORALL) ? "n implication." : " conjunction." ), "(To be able to do that, select the quantifier" + " plus the quantified formula.)" ); /* // FUTURE allow constant terms plus uses of |scoped_dep_vars| if ( !prep.scoped_dependent_vars.isEmpty() ) { Toolkit.getDefaultToolkit().beep(); String[] message = { "The surrounding quantifiers of " + prep.scoped_dependent_vars + " may interfere with this operation.", "Want to proceed to try to assign a value to \"" + prep.subexpr_text + "\"anyway?" }; if ( JOptionPane.showConfirmDialog( (JFrame) table.getTopLevelAncestor(), message, "Remove quantifier from supposition/derivation?" , JOptionPane.YES_NO_OPTION ) == JOptionPane.NO_OPTION ) return false; } */ if ( prep.polarity == 0 ) return note_error( "What you selected appears to be within the scope" + " of a \"" + prep.expressionsmgmt .get_spec_String(Symbol.Specifier.EQUIV) + "\" operator.", "You need to use the Rewriting Deduction" + " to expand away that operator", "before you can assign a value to a quantified variable" + " in its scope." ); if ( !(quantifier.op_spec_equals(Symbol.Specifier.FORALL) ^ (prep.polarity > 0) ) ) return note_error( "This operation isn't applicable to a \"" + quantifier.get_operator().get_text() + "\" inside", (prep.polarity > 0 ? "zero or an even" : "an odd") + " number of" + (prep.selected_column_id == PB_TableModel.Column_ID.SUPPS ? " explicit or implicit" : "" ) + " negations.", prep.selected_column_id == PB_TableModel.Column_ID.SUPPS ? "(Suppositions/derivations" + " start with one implicit negation.)" : "" ); } // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; // proceeding // just in case ... prep.entry.try_select( prep.subexpr.get_begin(), prep.subexpr.get_limit() ); LinkedList rplc_exprs = user_entry_dialog .get_appropriate_terms_to_assign_to( prep.subexpr_text, prep.scoped_dependent_vars ); if ( rplc_exprs == null ) return false; // assert rplc_exprs.size() == var_exprs.size() ListIterator var_exprs_it = var_exprs.listIterator(), rplc_exprs_it = rplc_exprs.listIterator(); while ( var_exprs_it.hasNext() ) (prep.quant != null ? prep.quant.get_argument2() : prep.expr ) .replace_throughout_scope( var_exprs_it.next().get_operator().get_text(), rplc_exprs_it.next().ensure_group() ); // As appropriate, elide the replaced variable from quantifier: //prep.expr.simplify(true); if ( prep.quant != null ) if ( prep.expressionsmgmt .variables_unquantified( prep.quant.get_argument1().ungroup() .get_argument1() ) .size() == rplc_exprs.size() ) // just the variables instantiated prep.quant .this_structure_replace(prep.quant.get_argument2()); else for ( Expression var_expr : var_exprs ) prep.quant.get_argument1().ungroup().get_argument1() .this_structure_replace( prep.quant.get_argument1().ungroup() .get_argument1() .var_seq_remove( var_expr.get_operator().get_text() ) ); String narrative_base = "Assigning \"" + prep.subexpr_text + " := " + user_entry_dialog.get_entered_text() + "\" in "; table_model().add( prep.selected_rows, prep.selected_column_id, // " = by quantifier-removal" narrative_base + "that formula yields:", narrative_base + "formula " + prep.ref_num_name + " yields:", prep.expr ); return true; } } // Add_Quantifier // Quantify static class Existentially_Quantify extends Ded_Action { Existentially_Quantify(/*ProofBuilder GUI_given,*/ JTable table_given) { super(/*GUI_given,*/ table_given); } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(event.getActionCommand()) : "appears_applicable(event.getActionCommand())"; */ if ( !note_sel_expr_rows_count(1) ) return false; Deduction_Prep prep = new Deduction_Prep(table); if ( prep.selected_column_id != PB_TableModel.Column_ID.SUPPS ) return note_error( "This operation is applicable only to a supposition/derivation." ); if ( !prep.expressionsmgmt.constant_or_dep_term( prep.subexpr, new LinkedList() ) ) return note_error( "To apply this deduction," + " you need to select a constant term." ); // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; //String c = prep.subexpr.get_operator().get_text(); String v = Character.isUpperCase(prep.subexpr_text.charAt(0)) ? "X" : "x"; if ( prep.expr.occurs(v) ) { // "y" v = Character.toString((char) (v.charAt(0) + 1)); if ( prep.expr.occurs(v) ) // "z" v = Character.toString((char) (v.charAt(0) + 1)); } while ( prep.expr.occurs(v) || Symbol.is_reserved(v) ) v = Character.toString((char) (v.charAt(0) - 1)); /* v = (String) JOptionPane.showInputDialog( (JFrame) table.getTopLevelAncestor(), "Enter a variable not already being used in that formula" + " for replacing the constant term you selected:", "Enter a variable", JOptionPane.QUESTION_MESSAGE, null, null, v ); */ v = JOptionPane.showInputDialog( "Enter a variable not already being used in that formula" + " for replacing the selected constant term:", v ); if ( v == null ) return false; if ( v.equals("") ) return note_error("What you entered was \"" + v + "\"."); if ( Symbol.is_reserved(v) ) return note_error("That symbol already means something here."); if ( prep.expr.occurs(v) ) return note_error( "That identifier is already being used in that formula." ); if ( !Character.isUnicodeIdentifierStart(v.charAt(0)) ) return note_error( "What you entered" + " isn't a valid alphanumeric identifier." ); for ( char v_ch : v.toCharArray() ) if ( !Character.isUnicodeIdentifierPart(v_ch) ) return note_error( "What you entered" + " isn't a valid alphanumeric identifier." ); if ( !prep.expressionsmgmt.is_variable_id(v) ) { if ( prep.expressionsmgmt.is_id_being_used(v) ) return note_error( "You can't use that identifier for a variable" + " because it's already being used", "for a nonvariable in this proof." ); prep.expressionsmgmt.add_variable_id(v); } prep.expr.replace_throughout_ungrp( (Expression) prep.subexpr.clone(), // |clone()| to // preserve: // replacing changes! v ); String narrative_base = "Since \"" + prep.subexpr_text + "\" satisfies that formula," + "\nwe can say some value satisfies it, i.e.:"; table_model().add( prep.selected_rows, prep.selected_column_id, // " = by quantifier-removal" narrative_base, "Consider formula " + prep.ref_num_name + ".\n" + narrative_base, new Expression( prep.expressionsmgmt .new_Symbol(Symbol.Specifier.QUANT_SEP), new Expression( prep.expressionsmgmt .new_Symbol(Symbol.Specifier.EXISTS), new Expression(v) ) //.parenthesize(), .ensure_group(), prep.expr.bracket() ) ); return true; } } // Add_Quantifier // Quantify static class Universally_Quantify extends Ded_Action { Universally_Quantify(/*ProofBuilder GUI_given,*/ JTable table_given) { super(/*GUI_given,*/ table_given); } boolean consider(String action_command, Deduction_Prep[] preps) { /* I think it's educational for users to try the deduction * and see the error message. assert appears_applicable(event.getActionCommand()) : "appears_applicable(event.getActionCommand())"; */ if ( !note_sel_expr_rows_count(1) ) return false; Deduction_Prep prep = new Deduction_Prep(table); if ( prep.selected_column_id != PB_TableModel.Column_ID.SUPPS ) return note_error( "This operation is applicable only to a supposition/derivation." ); // conclude checking basic apparent applicability: if ( !get_actingvsjustcheckingapplicability() ) return true; String s = prep.subexpr.get_operator().get_text(); if ( (!prep.expressionsmgmt.is_variable(prep.subexpr) || prep.scoped_freeable_vars.contains(s) || prep.scoped_dependent_vars.contains(s) ) && (!prep.expressionsmgmt.constant_or_dep_term( prep.subexpr, new LinkedList() ) || prep.subexpr.get_argument1() != null || prep.subexpr.get_argument2() != null // just // in // case || prep.expressionsmgmt.is_skolem_id(s) ) ) return note_error( "To apply this deduction, you need to select either" + " a variable that is free,", "or a constant about which we made no assumptions", "(such as satisfying an existential quantification)." ); String v; if ( prep.expressionsmgmt.is_variable(prep.subexpr) ) v = s; else { v = Character.isUpperCase(s.charAt(0)) ? "X" : "x"; if ( prep.expr.occurs(v) ) { // "y" v = Character.toString((char) (v.charAt(0) + 1)); if ( prep.expr.occurs(v) ) // "z" v = Character.toString((char) (v.charAt(0) + 1)); } while ( prep.expr.occurs(v) || Symbol.is_reserved(v) ) v = Character.toString((char) (v.charAt(0) - 1)); /* v = (String) JOptionPane.showInputDialog( (JFrame) table.getTopLevelAncestor(), "Enter a variable not already being used in that" + " formula for replacing the constant you selected:", "Enter a variable", JOptionPane.QUESTION_MESSAGE, null, null, v ); */ v = JOptionPane.showInputDialog( "Enter a variable not already being used in that" + " formula for replacing the selected constant:", v ); if ( v == null ) return false; if ( v.equals("") ) return note_error("What you entered was \"" + v + "\"."); if ( Symbol.is_reserved(v) ) return note_error("That symbol already means something here."); if ( prep.expr.occurs(v) ) return note_error( "That identifier is already being used in that formula." ); if ( !Character.isUnicodeIdentifierStart(v.charAt(0)) ) return note_error( "What you entered" + " isn't a valid alphanumeric identifier." ); for ( char v_ch : v.toCharArray() ) if ( !Character.isUnicodeIdentifierPart(v_ch) ) return note_error( "What you entered" + " isn't a valid alphanumeric identifier." ); if ( !prep.expressionsmgmt.is_variable_id(v) ) { if ( prep.expressionsmgmt.is_id_being_used(v) ) return note_error( "You can't use that identifier for a variable" + " because it's already being used", "for a nonvariable in this proof." ); prep.expressionsmgmt.add_variable_id(v); } prep.expr.replace_throughout_scope(prep.subexpr_text, v); } String narrative_base = "Since \"" + prep.subexpr_text + "\" represents an arbitrary value," + "\nwe can say that formula is true for all values; i.e.:"; table_model().add( prep.selected_rows, prep.selected_column_id, // " = by quantifier-removal" narrative_base, "Consider formula " + prep.ref_num_name + ".\n" + narrative_base, new Expression( prep.expressionsmgmt .new_Symbol(Symbol.Specifier.QUANT_SEP), new Expression( prep.expressionsmgmt .new_Symbol(Symbol.Specifier.FORALL), new Expression(v) ) //.parenthesize(), .ensure_group(), prep.expr.bracket() ) ); return true; } } }