src/Provers/classical.ML
 changeset 1524 524879632d88 parent 1231 91d2c1bb5803 child 1587 e7d8a4957bac
equal inserted replaced
1523:7513fbe502fb 1524:524879632d88
`    88 `
`    88 `
`    89 local open Data in`
`    89 local open Data in`
`    90 `
`    90 `
`    91 (** Useful tactics for classical reasoning **)`
`    91 (** Useful tactics for classical reasoning **)`
`    92 `
`    92 `
`    93 val imp_elim = make_elim mp;`
`    93 val imp_elim = (*cannot use bind_thm within a structure!*)`
`       `
`    94   store_thm ("imp_elim", make_elim mp);`
`    94 `
`    95 `
`    95 (*Solve goal that assumes both P and ~P. *)`
`    96 (*Solve goal that assumes both P and ~P. *)`
`    96 val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;`
`    97 val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;`
`    97 `
`    98 `
`    98 (*Finds P-->Q and P in the assumptions, replaces implication by Q.`
`    99 (*Finds P-->Q and P in the assumptions, replaces implication by Q.`
`   100 fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;`
`   101 fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;`
`   101 `
`   102 `
`   102 (*Like mp_tac but instantiates no variables*)`
`   103 (*Like mp_tac but instantiates no variables*)`
`   103 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;`
`   104 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;`
`   104 `
`   105 `
`   105 val swap = rule_by_tactic (etac thin_rl 1) (not_elim RS classical);`
`   106 val swap =`
`       `
`   107   store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical));`
`   106 `
`   108 `
`   107 (*Creates rules to eliminate ~A, from rules to introduce A*)`
`   109 (*Creates rules to eliminate ~A, from rules to introduce A*)`
`   108 fun swapify intrs = intrs RLN (2, [swap]);`
`   110 fun swapify intrs = intrs RLN (2, [swap]);`
`   109 `
`   111 `
`   110 (*Uses introduction rules in the normal way, or on negated assumptions,`
`   112 (*Uses introduction rules in the normal way, or on negated assumptions,`