module ThmTactics where
import Lookup
import Tactics
import Tacticals
import Kernel
import Tree
import Core_datatype
import DerivedRules
import Goals
import Vtslib
import Type_defs
import Parse
import X_interface
import Edlib
import Globals
import Tags -- partain
import Sub_Core1
import Sub_Core2
import Sub_Core3
import Sub_Core4
import Unparse
import Attributes
{-
rewrite_tac = Tactic "Rewrite" rewrite_input rewrite_subgoal
beta_tac = Tactic "Beta" beta_input beta_subgoal
eta_tac = Tactic "Eta" eta_input eta_subgoal
recurse_tac = Tactic "Recurse" recurse_input recurse_subgoal
-}
{-
create_name s i dc@(Symbol_dec t attL)
= case get_att Name_Style attL of
SOME _ -> (dc,i)
NONE -> (Symbol_dec t attL' , i+1)
where
nm = Name (s ++ nprimes i)
att = set_att Name_Style (Symbol_Name nm)
attL' = att : attL
create_name s i dc@(Axiom_dec t attL)
= case get_att Name_Style attL of
SOME _ -> (dc,i)
NONE -> (Axiom_dec t attL' , i+1)
where
nm = Name (s ++ nprimes i)
att = set_att Name_Style (Symbol_Name nm)
attL' = att : attL
-}
create_name s i (Decpair dc1 dc2 attL)
= (Decpair dc1' dc2' attL, i3)
where
(dc1',i2) = create_name s i dc1
(dc2',i3) = create_name s i2 dc2
create_name s i dc = (dc,i)
--nprimes i = take i ( repeat '\39' )
{-
(******************************************************************************)
(* complete_thm *)
(* *)
(* � *)
(* --------- Complete (�� *)
(* *)
(******************************************************************************)
-}
complete_tac = Tactic "Complete" complete_thm_input complete_thm
complete_thm gst sg lt (SOME [dv]) (ThmSpec itm)
= if not (is_valid_Thm th )
then Bad mesg
else if eq_trm th_itm itm
then Ok ([], complete_thm_valid th)
else Bad ("Derivation does not prove given goal\n" ++
"proves: " ++ unparse_trm sg ps th_itm )
where
ps = fetch_ps gst
th = parse_Thm sg ps dv
( TH_Err mesg ) = th
( th_itm , _ ) = internal_Thm th
complete_thm _ _ _ _ _ = Bad "Goal is not a theorem"
complete_thm_valid th []
= SOME (ThmDone th)
complete_thm_valid _ _ = NONE
complete_thm_input lt gst (ThmSpec tm)
= x_form True form /./
exp
where
exp NONE = reTurn NONE
exp ( SOME [OutText s]) = reTurn ( SOME [s] )
form = [InComment "Complete Theorem", InMultiText "Derivation" ""]
{-
(******************************************************************************)
(* gen_subgoal *)
(* *)
(* �.� *)
(* ------------ Gen *)
(* � �] � *)
(* *)
(******************************************************************************)
-}
gen_tac = OrdTactic "Gen" null_arg_fn gen_subgoal
gen_subgoal gst sg lt args (ThmSpec (Binder Forall dc tm _ _))
= Ok (subgoals, [lt,lt], rwL, gen_valid sg )
where
(dc',_) = create_name "xxx" 0 dc
subgoals = [DecSpec dc', ThmSpec tm]
rwL = [True, False]
-- ltL = [lt, extend_lookup_table true dc' lt]
gen_subgoal _ _ _ _ _
= Bad "Cannot apply tactic to given goal"
gen_valid sg dnL rwL
= case (dnL, rwL) of
([SOME (DecDone dc), SOME (ThmDone th)],_)
-> (rwL,[sg,extend dc sg],SOME (ThmDone (generalise th)))
([SOME (DecDone dc), NONE], [true,_])
-> ([True,True],[sg,extend dc sg],NONE)
_ -> (rwL,[sg,sg],NONE)
{-
(******************************************************************************)
(* disch_subgoal *)
(* *)
(* [��� *)
(* -------------- Dischage *)
(* � ��t *)
(******************************************************************************)
-}
disch_tac = OrdTactic "Disch" null_arg_fn disch_subgoal
disch_subgoal gst sg lt args (ThmSpec (Binder Imp dc tm _ _))
= Ok (subgoals, [lt,lt], rwL, disch_valid sg)
where
(dc',_) = create_name "hhh" 0 dc
subgoals = [DecSpec dc', ThmSpec tm]
rwL = [True, False]
disch_subgoal _ _ _ _ _
= Bad "Cannot apply 'Disch' to specified goal"
disch_valid sg dnL rwL
= case (dnL, rwL) of
([SOME (DecDone dc), SOME (ThmDone th)],_)
-> (rwL,[sg,extend dc sg],SOME (ThmDone (discharge th)))
([SOME (DecDone dc), NONE], [true,_])
-> ([True,True],[sg,extend dc sg],NONE)
_ -> (rwL,[sg,sg],NONE)
{-
(******************************************************************************)
(* conj_subgoal *)
(* *)
(* � � *)
(* ----- Conjunction *)
(* � � *)
(******************************************************************************)
-}
conj_tac = Tactic "Conjunction" null_arg_fn conj_subgoal
conj_subgoal gst sg lt args (ThmSpec (Binary' And tm1 tm2 _ _))
= Ok ([ThmSpec tm1, ThmSpec tm2], conj_valid)
conj_subgoal _ _ _ _ _
= Bad "cannot apply tactic to specified goal"
conj_valid [SOME (ThmDone th1), SOME (ThmDone th2)]
= SOME (ThmDone (conj th1 th2))
conj_valid _ = NONE
{-
(******************************************************************************)
(* disj_subgoal *)
(* *)
(* c *)
(* --------- Disjunction (�a�) give either � a� *)
(* a�, b� *)
(******************************************************************************)
-}
disj_tac = Tactic "Disjunction" disj_input disj_subgoal
disj_subgoal gst sg lt (SOME args) (ThmSpec tm)
= case args of
["Derivation", dv]
-> if is_valid_Thm th
then case internal_Thm th of
(Binary' Or tm1 tm2 _ _ , _)
-> Ok ([ThmSpec tm4, ThmSpec tm5],
disj_dv_valid th)
where
dc1 = Axiom_dec tm1 []
dc2 = Axiom_dec tm2 []
tm3 = shift_trm [] 1 tm
tm4 = Binder Imp dc1 tm3 [] []
tm5 = Binder Imp dc2 tm3 [] []
_ -> Bad "Goal is not a disjunction"
else Bad mesg
where
ps = fetch_ps gst
th = parse_Thm sg ps dv
( TH_Err mesg ) = th
["Specification",tm_rep]
-> parse_trm sg ps tm_rep |||
exp
where
exp tm6@(Binary' Or tm1 tm2 _ _)
= Ok ([ThmSpec tm4, ThmSpec tm5,
ThmSpec tm6], disj_tm_valid)
where
dc1 = Axiom_dec tm1 []
dc2 = Axiom_dec tm2 []
tm3 = shift_trm [] 1 tm
tm4 = Binder Imp dc1 tm3 [] []
tm5 = Binder Imp dc2 tm3 [] []
exp _ = Bad "Specification is not a disjunction"
ps = fetch_ps gst
_ -> Bad "No selection"
disj_subgoal _ _ _ _ _ = Bad "Cannot apply 'disjunction'"
disj_dv_valid th [SOME (ThmDone th1), SOME (ThmDone th2)]
= SOME (ThmDone (disj th th1 th2))
disj_dv_valid _ _ = NONE
disj_tm_valid [SOME (ThmDone th1), SOME (ThmDone th2), SOME (ThmDone th3)]
= SOME (ThmDone (disj th3 th1 th2))
disj_tm_valid _ = NONE
disj_input lt gst _
= x_form True form /./
exp
where
exp NONE = reTurn NONE
exp ( SOME [OutRadio s1,OutText s2] )
= reTurn ( SOME [s1,s2] )
form = [InComment "Disjunction",
InRadio "Argument Type" 0 ["Derivation","Specification"],
InMultiText "" ""]
{-
(******************************************************************************)
(* reflex_subgoal *)
(* *)
(* �� *)
(* ----- Reflex *)
(* *)
(******************************************************************************)
-}
reflex_tac = Tactic "Reflex" null_arg_fn reflex_subgoal
reflex_subgoal gst sg lt args (ThmSpec (Binary' Eq' tm1 tm2 _ _))
| eq_trm tm1 tm2 = Ok ([], reflex_valid (reflex (trm_to_Trm sg tm1)))
| otherwise = Bad "Terms not equal"
reflex_subgoal _ _ _ _ _
= Bad "cannot apply 'reflex' to specified goal"
reflex_valid th [] = SOME (ThmDone th)
reflex_valid _ _ = NONE
{-
{-
(******************************************************************************)
(* rewrite_subgoal *)
(* *)
(* P[a]i *)
(* ----- Rewrite (�a = b) supply either � a=b *)
(* P[b]i *)
(* *)
(******************************************************************************)
-}
rewrite_subgoal gst sg lt (SOME [index,spec,spec_type]) (ThmSpec tm)
= case spec_type of
"Derivation"
-> case internal_Thm th of
(Binary' Eq' tm2 tm3 _ _ ,_)
| eq_trm tm1 tm2
-> Ok ([ThmSpec tm4], rewrite_th_valid iL th)
where
tm4 = replace_trm tm tm3 iL
| otherwise
-> Bad "LHS does not match subgoal"
_ -> Bad "Theorem not an equality"
where
iL = parse_index index
(tm1,dcL) = select_trm tm iL
sg1 = foldl ext_Sg sg dcL
ps = fetch_ps gst
th = parse_Thm sg ps spec
"Specification"
-> case parse_trm sg spec of -- add ps to parse
th_tm@(Binary' Eq' tm2 tm3 _ _)
| eq_trm tm1 tm2
-> Ok ([ThmSpec tm4, ThmSpec th_tm],
rewrite_tm_valid iL)
where
tm4 = replace_trm tm tm3 iL
| otherwise
-> Bad "LHS does not match subgoal"
_ -> Bad "Term not an equality"
where
iL = parse_index index
(tm1,dcL) = select_trm tm iL
sg1 = foldl ext_sg (internal_Sgn sg) dcL
ps = fetch_ps gst
rewrite_th_valid iL th [SOME (ThmDone th1)]
= SOME (ThmDone (subterm_rw th1 (symmetry th) iL))
rewrite_tm_valid iL [SOME (ThmDone th1), SOME (ThmDone th2)]
= SOME (ThmDone (subterm_rw th1 (symmetry th2) iL))
rewrite_input gst lt (ThmSpec tm)
= error "rewrite_input not implemented"
{-
= x_form True form /./
exp
where
exp NONE -> reTurn NONE
exp ( SOME [OutSubterm s1,OutText s2,OutRadio s3] )
= reTurn ( SOME [s1,s2,s3] )
exp _ = return_err "Unexected arguments returned"
attL = get_attributes gst
(s,data) = unparse_trm_data ust1 tm
form = [InComment "Rewrite",
InSubterm s data,
InMultiText "Rewrite Theorem" "",
InRadio "Type of Input " 0 ["Derivation","Specification"]]
-}
parse_index inp
= case next_tk inp of
(SOME tk, inp1) -> read tk : parse_index inp1
(NONE, _) -> []
ext_Sg sg dc = extend (dec_to_Dec sg dc) sg
ext_sg sg dc = Extend dc sg []
-}
induction_tac= Tactic "Induction" null_arg_fn ind_subgoal
ind_subgoal gst sg lt args (ThmSpec (Binder Forall dc tm _ attL))
= Ok ( gL , ind_valid ind_thm pL )
where
tm1 = Binder Lambda dc tm [] attL
( Symbol_dec st attL ) = dc
(i,j,spec,dcL,parmL) = get_datatype_info (internal_Sgn sg) st
specL = map (trm_to_Trm sg) spec
ind_thm = foldl specialise (induction (constructor sg i j 0)) specL
(Binder _ dec tm2 _ _ , _) = internal_Thm ind_thm
(spec_thm,pL) = find_betas (subst_trm dec tm2 tm1)
gL = map ThmSpec (reduce_ind spec_thm) ++ [TrmSpec tm1]
ind_subgoal _ _ _ _ _
= Bad "Goal is not universally quantified"
reduce_ind (Binder Imp dc tm _ _)
= typ_of_dec dc : reduce_ind (shift_trm [] (-1) tm)
reduce_ind _ = []
ind_valid th pL dnL
= SOME (ThmDone (foldl mp th1 dnL1))
where
i = length dnL - 1
dnL1 = take i dnL
SOME (TrmDone tm) = head (drop i dnL)
th1 = rep_beta (specialise th tm) pL
mp th1 (SOME (ThmDone th2)) = modus_ponens th1 th2
axiom_tac = Tactic "Axiom" axiom_arg_fn axiom_subgoal
axiom_arg_fn gst lt (ThmSpec tm)
= x_form True form /./
exp
where
exp NONE = reTurn NONE
exp ( SOME [OutText s] ) = reTurn ( SOME [s] )
form = [InComment "Tactic: Axiom", InSingleText "Name Of Axiom" ""]
axiom_subgoal gst sg lt (SOME [name]) obj
= case lookup_name sg name of
SOME (Sym i j _ _)
-> if ( is_valid_Thm app_axiom )
then Ok ([], axiom_valid app_axiom )
else Bad ("Axiom: " ++ show i ++ " " ++ show j)
where
app_axiom = axiom sg i j
_ -> Bad ("No Such Axiom Name: " ++ name)
axiom_subgoal _ _ _ _ _
= Bad "Hmm: it's failed, no name supplied perhaps?"
axiom_valid th [] = SOME (ThmDone th)
axiom_valid _ _ = NONE
hyp_tac = Tactic "Hyp" null_arg_fn find_hyp
find_hyp gst sg lt NONE (ThmSpec tm)
= case filter (find_match tm) hyps of
[] -> Bad "Can't find match"
(th : _) -> Ok ([], axiom_valid th)
where
hyps = get_hyp_from_sgn sg (internal_Sgn sg) 0
find_hyp _ _ _ _ _
= Bad "goal is not a theorem specification"
get_hyp_from_sgn sg (Empty _) i = []
get_hyp_from_sgn sg (Extend dc isg _) i
= l ++ get_hyp_from_sgn sg isg (i + 1)
where
(_, l) = get_hyp_from_dec sg dc i 0
get_hyp_from_sgn sg _ i = []
get_hyp_from_dec sg (Axiom_dec _ _ ) i j = (j, [axiom sg i j])
get_hyp_from_dec sg (Def _ _ _) i j = (j, [axiom sg i j])
get_hyp_from_dec sg (Decpair dc1 dc2 _) i j
= (j'', l ++ l')
where
(j', l) = get_hyp_from_dec sg dc1 i (j+1)
(j'',l') = get_hyp_from_dec sg dc2 i (j' + 1)
get_hyp_from_dec _ _ _ j = (j, [])
find_match tm th
= eq_trm tm tm'
where
(tm',_) = internal_Thm th
{-
(******************************************************************************)
(* eq_subgoal *)
(* *)
(* a=b *)
(* --------- *)
(* a� b� *)
(******************************************************************************)
-}
eq_tac = Tactic "Eq" null_arg_fn eq_subgoal
eq_subgoal gst sg lt args (ThmSpec (Binary' Eq' itm1 itm2 _ _))
= if eq_trm ty1 ty2 && eq_trm ty1 (Constant Bool' [] [])
then Ok ([ThmSpec tm3, ThmSpec tm4],eq_valid gst lt sg tm1 tm2)
else Bad "Equality not on booleans"
where
dc1 = Axiom_dec itm1 []
dc2 = Axiom_dec itm2 []
tm3 = Binder Imp dc1 (shift_trm [] 1 itm2) [] []
tm4 = Binder Imp dc2 (shift_trm [] 1 itm1) [] []
tm1 = trm_to_Trm sg itm1
tm2 = trm_to_Trm sg itm2
(ty1,_,_) = internal_Trm (typ_of_Trm tm1)
(ty2,_,_) = internal_Trm (typ_of_Trm tm2)
eq_subgoal _ _ _ _ _ = Bad "Cannot apply tactic to given goal"
eq_valid gst lt sg tm1 tm2 [SOME (ThmDone th1), SOME (ThmDone th2)]
= SOME (ThmDone th6)
where
inp = "\186(\177a:bool.\177b:bool.(a\182b)\182(b\182a)\182(a=b))"
ps = fetch_ps gst
eq_th = parse_Thm sg ps inp
th3 = specialise eq_th tm1
th4 = specialise th3 tm2
th5 = modus_ponens th4 th1
th6 = modus_ponens th5 th2
eq_valid _ _ _ _ _ _ = NONE
{-
(******************************************************************************)
(* or_subgoal *)
(* *)
(* a �b *)
(* ------- *)
(* �a �b *)
(******************************************************************************)
-}
or_tac = Tactic "Or" null_arg_fn or_subgoal
or_subgoal gst sg lt NONE (ThmSpec (Binary' Or tm1 tm2 _ _))
= Ok ([ThmSpec tm3], or_valid gst lt sg tM1 tM2)
where
dc = Axiom_dec (Unary Not tm1 [] []) []
tm3 = Binder Imp dc (shift_trm [] 1 tm2) [] []
tM1 = trm_to_Trm sg tm1
tM2 = trm_to_Trm sg tm2
or_subgoal _ _ _ _ _ = Bad "Goal is not a disjunction"
or_valid gst lt sg tm1 tm2 [SOME (ThmDone th)]
= SOME (ThmDone th2)
where
inp = "\186(\177a:bool.\177b:bool.(\181a\182b)=(a\180b))"
ps = fetch_ps gst
or_th = parse_Thm sg ps inp
th1 = specialise (specialise or_th tm1) tm2
th2 = subterm_rw th th1 []
or_valid _ _ _ _ _ _ = NONE
{-
(******************************************************************************)
(* not_subgoal *)
(* *)
(* ��a *)
(* ------- *)
(* a *)
(******************************************************************************)
-}
not_tac = Tactic "Not" null_arg_fn not_subgoal
not_subgoal gst sg lt NONE (ThmSpec (Unary Not (Unary Not tm1 _ _) _ _))
= Ok ([ThmSpec tm1], not_valid gst lt sg tM1)
where
tM1 = trm_to_Trm sg tm1
not_subgoal _ _ _ _ _ = Bad "cannot apply 'Not' to given goal"
not_valid gst lt sg tm1 [SOME (ThmDone th)]
= SOME (ThmDone th2)
where
inp = "\186(\177a:bool.a=\181\181a)"
ps = fetch_ps gst
not_th = parse_Thm sg ps inp
th1 = specialise not_th tm1
th2 = subterm_rw th th1 []
not_valid _ _ _ _ _ = NONE
{-
(******************************************************************************)
(* lemma-subgoal *)
(* *)
(* a *)
(* ------------ b *)
(* b �a, b *)
(******************************************************************************)
-}
lemma_tac = Tactic "Lemma" lemma_input lemma_subgoal
lemma_subgoal gst sg lt (SOME [nm,spec]) (ThmSpec tm)
= parse_trm sg ps spec |||
exp
where
ps = fetch_ps gst
exp lemma = Ok ( [g1,g2], lemma_valid )
where
g1 = ThmSpec (Binder Imp dc tm' [] [])
where
rnm = Name nm
dc = Axiom_dec lemma [sym_nm rnm]
tm' = shift_trm [] 1 tm
g2 = ThmSpec lemma
lemma_subgoal _ _ _ _ _ = Bad "Goal is not a theorem specification"
lemma_valid [SOME (ThmDone th1), SOME (ThmDone th2)]
= SOME (ThmDone (modus_ponens th1 th2))
lemma_valid _ = NONE
lemma_input gst lt (ThmSpec tm)
= x_form True form /./
exp
where
exp NONE = reTurn NONE
exp ( SOME [OutText s1,OutText s2] )
= reTurn ( SOME [s1,s2] )
form = [InComment "Add lemma",
InSingleText "Name " "",
InMultiText "Lemma" ""]
{-
rw_input str gst lt (ThmSpec tm)
= error "re_input not implemented"
{-
= x_form True form /./
exp
where`
exp NONE = reTurn NONE
exp ( SOME [OutSubterm s] ) = reTurn ( SOME [s] )
exp _ = return_err "Unexected arguments returned"
attL = get_attributes gst
ust = get_default_us gst
val ust1 = U.set_defaults (U.set_lookup_table ust lt) attL
val (s,data) = unparse_trm_data ust1 tm
form = [InComment str, InSubterm s data]
-}
beta_subgoal gst sg lt (SOME [index]) (ThmSpec tm)
= Ok ( [ ThmSpec tm3 ] , beta_valid th iL )
where
iL = parse_index index
(App (Binder Lambda dc tm1 _ _) tm2 _ _ ,dcL)
= select_trm tm iL
tm3 = replace_trm tm (subst_trm dc tm1 tm2) iL
th = reflex (trm_to_Trm sg tm)
beta_valid th iL [SOME (ThmDone th')]
= SOME (ThmDone (subterm_rw th' (beta_rw th (0:iL)) []))
beta_valid _ _ _ = NONE
beta_input = rw_input "�ewrite"
{-
fun eta_subgoal gst sg lt (SOME [index]) (ThmSpec tm) =
let val iL = parse_index (strings_to_input [index])
val (Binder(Lambda,dc,App (tm1,Sym(0,0,_,_),_,_),_,_),dcL) =
select_trm tm iL
in if occurs 0 tm1
then fail "Not �educducable"
else
let val tm3 = replace_trm tm (shift_trm [] ~1 tm1) iL
val th = reflex (trm_to_Trm sg tm)
in ( [ ThmSpec tm3 ] , eta_valid th iL ) end
end
and eta_valid th iL [SOME (ThmDone th')] =
SOME (ThmDone (subterm_rw th' (eta_rw th (0::iL)) []))
val eta_input = rw_input "�ewrite"
-}
{-
fun recurse_subgoal gst sg lt (SOME [index]) (ThmSpec tm) =
let val iL = parse_index (strings_to_input [index])
val (App (Recurse _,_,_,_),dcL) = select_trm tm iL
val th = recurse_rw (reflex (trm_to_Trm sg tm)) (0::iL)
val (Binary' (Eq',tm3,_,_,_), _) = internal_Thm th
in ( [ ThmSpec tm3 ] , recurse_valid th ) end
and recurse_valid th [SOME (ThmDone th')] =
SOME (ThmDone (subterm_rw th' th []))
val recurse_input = rw_input "Recurse Rewrite"
-}
-}
taut_tac = Tactic "Taut" null_arg_fn taut_subgoal
taut_subgoal gst sg lt _ (ThmSpec tm)
= if is_valid_Thm th
then Ok ( [] , taut_valid th )
else Bad mesg
where
th = taut (trm_to_Trm sg tm)
( TH_Err mesg ) = th
taut_subgoal _ _ _ _ _ = Bad "goal is not a theorem specification"
taut_valid th [] = SOME (ThmDone th)
taut_valid _ _ = NONE
{-
(******************************************************************************)
(* exists_subgoal *)
(* *)
(* p *)
(* ------ ��.q *)
(* �.q� *)
(******************************************************************************)
-}
exists_elim_tac = Tactic "ExistsElim" exists_elim_input exists_elim_subgoal
exists_elim_subgoal gst sg lt (SOME [s1,"Derivation"]) (ThmSpec tm)
= parse_Thm_M sg ps s1 |||
exp
where
ps = fetch_ps gst
exp th = Ok ( [ ThmSpec tm''' ] , exists_elim_valid th )
where
(Binder Exists dc tm' _ _ ,_) = internal_Thm th
tm'' = Binder Imp (Axiom_dec tm' [])(shift_trm [] 2 tm) [] []
tm''' = Binder Forall dc tm'' [] []
exists_elim_subgoal gst sg lt (SOME [s1,"Specification"]) (ThmSpec tm)
= parse_trm sg ps s1 |||
exp
where
ps = fetch_ps gst
exp tm1@(Binder Exists dc tm' _ _)
= Ok ( [ ThmSpec tm''', ThmSpec tm1 ] , exists_elim_valid' )
where
tm'' = Binder Imp (Axiom_dec tm' []) (shift_trm [] 2 tm) [] []
tm''' = Binder Forall dc tm'' [] []
exp _ = Bad "term is not an existential"
exists_elim_subgoal _ _ _ _ _
= Bad "Invalid application of 'ExistsElim'"
exists_elim_valid th' [SOME (ThmDone th)]
= SOME (ThmDone (exists_elim th' th))
exists_elim_valid _ _ = NONE
exists_elim_valid' [SOME (ThmDone th1), SOME (ThmDone th2)]
= SOME (ThmDone (exists_elim th1 th2))
exists_elim_valid' _ = NONE
exists_elim_input gst lt (ThmSpec tm)
= x_form True form /./
exp
where
exp ( SOME [OutText s1,OutRadio s2] )
= reTurn ( SOME [s1,s2] )
exp _ = reTurn NONE
form = [InComment "Exists Elimination",
InMultiText "Existential Object" "",
InRadio "Type of Object" 0 ["Derivation","Specification"]]
strip split_tac auto_tac
= repeat_tac (snd (lift_tactic reflex_tac) `orelse`
snd (lift_tactic hyp_tac) `orelse`
-- snd (lift_tactic taut_tac) `orelse`
snd (lift_ordtactic gen_tac) `orelse`
snd (lift_ordtactic disch_tac) `orelse`
snd (lift_tactic conj_tac) `orelse`
snd (lift_tactic or_tac) `orelse`
snd (lift_tactic not_tac) `orelse`
snd (lift_tactic eq_tac) `orelse`
snd (lift_tactic auto_tac) ) -- `orelse`
-- snd (lift_ordtactic split_tac) )
triv auto_tac
= snd (lift_tactic reflex_tac) `orelse`
snd (lift_tactic hyp_tac) `orelse`
snd (lift_tactic auto_tac) `orelse`
snd (lift_tactic taut_tac) `orelse`
( \ trst -> reTurn trst )
|
