Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <199507102203.AA114043820@bobcat.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: RE: [Q] manipulating assumptions
Date: Mon, 10 Jul 1995 16:03:40 -0600
From: Phil Windley <windley@cs.byu.edu>


Recently rahard@ee.umanitoba.ca asked about manipulating assumptions.  

Below are 8 different ways of solving the goal.  The first 6 do not
manipulate the assumption list in the sense that the question asked, but do
solve the goal.  The last two manipulate the assumption list using
ASSUM_LIST.  

Its interesting to note that the last two examples are not shorter than the
first 5 and are in many cases considerably more complex.  Obviously this
won't always be the case, but the direct approach is not always the best.  

The following URL contains a brief tutorial on managing assumptions.  

http://lal.cs.byu.edu:80/lal/holtut/lesson-4/lesson-4.html

Comments, as always, are welcome...

--phil--


_____________________________________________________________________

let my_goal = 
"!inp out.
  (?p1 p2.
    (p1 = T) /\
    (~inp ==> (p1 = out)) /\
    (inp ==> (p2 = out)) /\
    (p2 = F)) ==>
  (out = ~inp)";;


% take 0: using FIRST_ASSUM %

g my_goal;;

% put in canonical form %
e(
REWRITE_TAC []
);;

e(
REPEAT STRIP_TAC
);;


% for the implications %
e(
ASM_CASES_TAC "inp:bool"
THEN RES_TAC
THEN ASM_REWRITE_TAC []  % this solves the case where inp is true %
);;

% use the first equality in reverse to substitute in goal %
e(
FIRST_ASSUM (SUBST1_TAC o GSYM)
);;

% accept it %
e(
FIRST_ASSUM MATCH_ACCEPT_TAC
);;


% take 1: propositional form, part I %

g my_goal;;


e(
REPEAT STRIP_TAC
);;

% put it all back without existential and universal quantification %
e(
POP_ASSUM_LIST (MAP_EVERY MP_TAC)
);;

e(
BOOL_CASES_TAC "p1:bool"
THEN REWRITE_TAC []
);;


e(
BOOL_CASES_TAC "p2:bool"
THEN REWRITE_TAC []
);;


e(
BOOL_CASES_TAC "out:bool"
THEN REWRITE_TAC []
);;


% take 2: propositional form, part II %

g my_goal;;


e(
REPEAT STRIP_TAC
);;

% put it all back without existential and universal quantification %
e(
POP_ASSUM_LIST (MAP_EVERY MP_TAC)
);;

load_library `taut`;;

e(
TAUT_TAC
);;

% take 3: propositional form, part III %

g my_goal;;


% just get rid of the existential quantification and put it right back %
e(
REPEAT (STRIP_GOAL_THEN (STRIP_THM_THEN MP_TAC))
);;

e(
TAUT_TAC
);;


% take 4: unwind %

unlink `foo.th`;new_theory `foo`;;

load_library `unwind`;;

% presumably, your goal is an already slightly expanded form that 
  started off as definitions: %

let foo = new_definition
   (`foo`,
    "foo inp out = 
      (?p1 p2.
	(p1 = T) /\
	(~inp ==> (p1 = out)) /\
	(inp ==> (p2 = out)) /\
	(p2 = F))"
    );;

% unwind can get rid of those pesky existentially quantified lines: %

let foo_expanded = EXPAND_AUTO_RIGHT_RULE [] foo;;


g "! inp out . foo inp out ==> (out = ~inp)";;

e(
REWRITE_TAC [foo_expanded]
THEN TAUT_TAC
);;


% take 5: don't use plain old STRIP_TAC---premanipulate the assumptions %


g my_goal;;

e(
REWRITE_TAC []
);;

e(
REPEAT GEN_TAC
);;

% reverse the equalities as you put them on the assumption list %
e(
STRIP_GOAL_THEN (STRIP_ASSUME_TAC o GSYM)
);;

% get rid of some implications %
e(
ASM_CASES_TAC "inp:bool"
THEN RES_TAC
);;

% this now solves both subgoals %
e(
ASM_REWRITE_TAC []
);;
 

% take 6: bald faced grab the numbers and mangle 'em %

g my_goal;;

e(
REWRITE_TAC []
THEN REPEAT STRIP_TAC
);;

e(
ASSUM_LIST (\thl . 
   STRIP_ASSUME_TAC (REWRITE_RULE [el 1 thl] (el 2 thl))
   THEN STRIP_ASSUME_TAC (REWRITE_RULE [el 4 thl] (el 3 thl)) 
   )
);;

e(
EQ_TAC
);;

e(
ASSUM_LIST (STRIP_ASSUME_TAC o (REWRITE_RULE []) o CONTRAPOS o (el 2))
);;


e(
ASM_REWRITE_TAC []
);;


% take 7: applying a little more finesse (and a *lot* more thought) %

g my_goal;;


e(
REWRITE_TAC []
THEN REPEAT STRIP_TAC
);;


e(
EQ_TAC
);;


let imp_filter = filter (is_imp o concl) and
    not_imp_filter = filter (\x . $not ((is_imp o concl) x));;

e(
ASSUM_LIST (\thl . 
   MAP_EVERY STRIP_ASSUME_TAC 
    (map ((REWRITE_RULE (not_imp_filter thl)) o CONTRAPOS) (imp_filter thl)))
);;

e(
ASSUM_LIST (\thl . 
   MAP_EVERY STRIP_ASSUME_TAC 
    (map (REWRITE_RULE (not_imp_filter thl)) (imp_filter thl)))
);;