(* gen.ML *)
fun xl () = OS.Process.system ("xlock -remote -mode random") ;
fun lo _ = Isar.loop () ;
fun printnl str = print (str ^ "\n") ;
(* don't know how to undo this but sometimes handy
install_pp (make_pp ["term"] Goals.pprint_term);
*)
(* fmap : ('a -> 'b) list -> 'a -> 'b list
apply list of functions to one argument *)
fun fmap fs x = map (fn f => f x) fs ;
(* General Isabelle stuff *)
print_depth 20 ;
fun load _ = () ; (* found in Moscow ML code *)
fun beep () = TextIO.print (chr 7) ;
(* Goal *)
val [Goal_def, triv_goal, rev_triv_goal] =
map thm ["Goal_def", "triv_goal", "rev_triv_goal"] ;
(* thmt : string -> xstring -> thm
like thm, but to get a theorem in a given theory context *)
fun thmt tstr str =
let val cont = the_context () ;
val _ = context (theory tstr) ;
val th = thm str ;
val _ = context cont ;
in th end ;
(* theory *)
val rthy = ref "" ;
fun upd_th tname = (rthy := tname ; update_thy tname) ;
fun use_th tname = (rthy := tname ; use_thy tname) ;
fun upd() = update_thy (!rthy) ;
fun us() = use_thy (!rthy) ;
(* for cterms *)
val funct' = fst o Thm.dest_comb ;
val arg' = snd o Thm.dest_comb ;
(* funargs' : cterm -> cterm * cterm list *)
fun funargs' t =
let
fun peel t args =
let val (f, a) = Thm.dest_comb t ; in peel f (a :: args) end
handle _ => (t, args)
in peel t [] end ;
fun argn' n t =
let val (f, args) = funargs' t in Library.nth_elem (n-1, args) end ;
val left' = arg' o funct' ; val right' = arg' ;
(* for terms *)
(* want to make single-letter ones obsolete *)
fun f (a $ b) = a ; fun a (a $ b) = b ;
fun l (a $ b $ c) = b ; fun r (a $ b $ c) = c ;
(* funargs : term -> term * term list *)
fun funargs t =
let
fun peel t args =
let val (f $ a) = t ; in peel f (a :: args) end
handle Bind => (t, args)
in peel t [] end ;
fun dest_fa' (f $ arg) args = dest_fa' f (arg :: args)
| dest_fa' f args = (f, args) ;
(* dest_fa : term -> term * term list - same as funargs *)
fun dest_fa f = dest_fa' f [] ;
(* mk_fa : term -> term list -> term *)
fun mk_fa f (arg :: args) = mk_fa (f $ arg) args
| mk_fa f [] = f ;
fun funct (a $ b) = a ; fun arg (a $ b) = b ;
fun left (a $ b $ c) = b ; fun right (a $ b $ c) = c ;
val exr = ref Match ;
fun keep_exn e = (exr := e ; print_exn e) ;
fun incr sg = sg + 1 ;
fun decr sg = sg - 1 ;
fun incr_by n sg = sg + n ;
fun decr_by n sg = sg - n ;
(* printing hierarchy of subterms, for use when simply printing the
term is too long, but you want to see the innards of a term *)
fun indent () = TextIO.print " " ;
fun indentn i = funpow i indent () ;
(* prinh : int -> term -> unit *)
fun prinh i t = (indentn i ; prin t ;
let val (f, a) = funargs t ;
in case (a, t) of ([], Abs (x, _, body)) => prinh (i+1) body
| ([], _) => ()
| _ => app (prinh (i+1)) (f :: a) end) ;
fun nth (xs, i) = Library.nth_elem (i, xs) ; (* for Isabelle98 *)
(* will recalculate the path of a file to be used according to
the path of the file "calling" it ; note this causes confusion
if the file used has an exception *)
val files_used = ref ([] : (string * string) list) ;
val std_use = use ;
val file_stack = ref ["notset"] ;
(* gets that part of string upto and including last "/" *)
fun path_of_str str =
let val re = rev (explode str)
fun ffs (rp as "/" :: wd) = rp
| ffs (ch :: wd) = ffs wd
| ffs [] = []
in implode (rev (ffs re)) end ;
fun is_rel file = not (hd (explode file) = "/") ;
fun locfile file =
if is_rel file then path_of_str (hd (!file_stack)) ^ file else file ;
fun useact file =
(files_used := (file, hd (!file_stack)) :: !files_used ;
file_stack := file :: !file_stack ;
std_use file handle ex =>
(files_used := tl (!files_used) ; file_stack := ["notset"] ; raise ex) ;
file_stack := tl (!file_stack)) ;
fun use file = useact (locfile file) ;
fun uses file =
let val lf = locfile file
in if exists (fn (f, _) => f = lf) (!files_used) then () else useact lf end ;
(* tacthm : tactic -> thm -> thm
like rule_by_tactic, but doesn't freeze variables *)
fun tacthm tf state =
case Seq.pull (tf state) of SOME(x,_) => x
| NONE => raise THM ("tacthm", 0, [state]) ;
val tacsthm = tacthm o EVERY ;
(* fwd : tactic -> thm -> thm
uses tactics do do forward proof, as though on an
assumption of a subgoal, eg in meta_std for HOL *)
fun fwd tac th =
let val tt = rule_by_tactic tac (make_elim th)
in tacthm (TRYALL atac) tt end ;
val op RS = Drule.RS ; (* because gets set differently elsewhere *)
val op MRS = Drule.MRS ; (* because gets set differently elsewhere *)
val op RSN = Drule.RSN ; (* because gets set differently elsewhere *)
val rtac = Tactic.rtac ; (* because gets set differently elsewhere *)
(* to unify premises *)
fun up th = tacthm (TRYALL atac) (th RS cut_rl);
val cut2 = tacthm (etac thin_rl 2) (cut_rl RS cut_rl);
val revcut2 = tacthm (etac thin_rl 2) (revcut_rl RSN (2, revcut_rl));
(*
val tacthm = fn : tactic -> thm -> thm
val up = fn : thm -> thm - unify premises
val cut2 = "[| [| PROP ?psi; PROP ?psi1 |] ==> PROP ?theta;
PROP ?psi1; PROP ?psi |] ==> PROP ?theta" : thm
val revcut2 =
"[| PROP ?V; PROP ?V1; [| PROP ?V; PROP ?V1 |] ==> PROP ?W |] ==> PROP ?W"
: thm
*)
val thin_same = prove_goal ProtoPure.thy
"PROP P ==> PROP P ==> PROP P" (fn prems => [ resolve_tac prems 1]) ;
(* to duplicate an assumption in a subgoal, use etac dup_rl *)
val dup_rl = tacthm (ftac asm_rl 2) revcut_rl ;
(* to use one subgoal in proving another, use use_sg_tac, then atac *)
val use_sg_tac = PRIMITIVE (fn th => th RS cut_rl) ;
val meta_iffI = prove_goal ProtoPure.thy
"[| PROP P ==> PROP Q; PROP Q ==> PROP P |] ==> PROP P == PROP Q"
(fn [prem1,prem2] => [rtac (equal_intr prem1 prem2) 1]);
val meta_cong = prove_goal ProtoPure.thy
"[| P == Q; R == S |] ==> P (R) == Q (S)"
(fn [prem1,prem2] => [ rewtac prem1, rewtac prem2, rtac reflexive_thm 1 ]) ;
(* mii : thm -> thm -> thm, takes P ==> Q and Q ==> P to P == Q,
like equal_intr, but also does necessary resolution *)
fun mii ded1 ded2 = tacthm (atac 1 THEN atac 1) ([ded1, ded2] MRS meta_iffI) ;
val meta_iffD2 = prove_goal ProtoPure.thy
"[| PROP P==PROP Q; PROP Q |] ==> PROP P"
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
val meta_iffD1 = symmetric_thm RS meta_iffD2;
val meta_iffDs = [meta_iffD1, meta_iffD2] ;
fun md1 th = th RS meta_iffD1;
fun md2 th = th RS meta_iffD2;
val trans3 = transitive_thm RS transitive_thm ;
val trans4 = transitive_thm RS trans3 ;
(* apply_unify : theory -> term -> term -> term
apply term t to u, unifying variable terms and types *)
fun apply_unify thy t u =
let val [ct, cu] = map (cterm_of thy) [t, u] ;
(* standard o added Tue Jul 9 10:13:36 EST 2013 *)
val [rt, ru] = map (standard o reflexive) [ct, cu] ;
val rtu = [rt, ru] MRS meta_cong ;
val Const ("==", ty) $ ctu $ ctu' = prop_of rtu ;
in ctu end ;
(* bind_st_thm : string * string * thm -> unit
like bind_thm, but also gives statement of theorem (ie you can choose
the variable names; won't work if premises are themselves meta-level
implications); also will prove, in simple cases, a weaker theorem *)
fun bind_st_thm (name, stmt, thm) =
qed_goal name (theory_of_thm thm) stmt
(fn prems => [rtac (prems MRS thm) 1]) ;
(* thm_vars : thm -> string list, get vars of thm, should have zero indices *)
fun thm_vars th =
let val tvs = (term_vars o #prop o rep_thm) th ;
val vns = map (fn Var ((n, 0), ty) => n) tvs ;
in vns end ;
(* rtac_all : thm list -> tactic
resolves theorems, one-by-one, against the then first subgoal *)
fun rtac_all [] = all_tac
| rtac_all (p :: ps) = rtac p 1 THEN rtac_all ps ;
(* TRY', REPEAT' : ('a -> tactic) -> 'a -> tactic
just like THEN' etc *)
fun TRY' tacf i = TRY (tacf i) ;
fun REPEAT' tacf i = REPEAT (tacf i) ;
(* to try a tactic on any goal, and return sequence of all successes *)
fun ANYGOAL' tac 0 st = no_tac st
| ANYGOAL' tac n st = (tac n APPEND ANYGOAL' tac (n-1)) st ;
fun ANYGOAL tac st = ANYGOAL' tac (nprems_of st) st ;
(* LASTGOAL : apply tactic to the highest-numbered goal *)
fun LASTGOAL tac st = tac (nprems_of st) st ;
(* TRYE : tactic -> tactic
variant of TRY which handles errors *)
fun TRYE tac state = tac state handle _ => all_tac state ;
(* THENR : int -> int -> (int -> tactic) -> tactic
like ALLGOALS but with a limited range of subgoals,
THENR m n tf does tf j for j = n downto m;
note - doing them in downwards order means it doesn't matter that
each tf j may change subgoal j into several, or none *)
fun THENR m n tf =
if n = m then tf m
else if n < m then all_tac
else tf n THEN THENR m (n-1) tf ;
infix 1 THENEXP THENRG ;
(* THENRG : (int -> tactic) * (int -> int -> tactic) -> int -> tactic
sequencing tactics, where the second one has two integer arguments,
which denote the range of subgoals resulting from the first tactic *)
fun (tacf1 THENRG tacf2) sg state =
let fun tac2 newstate =
tacf2 sg (nprems_of newstate - nprems_of state + sg) newstate
in (tacf1 sg THEN tac2) state end ;
(* THENEXP : (int -> tactic) * (int -> tactic) -> int -> tactic
composition of tactic functions tacf1,tacf2, where
tacf1,tacf2 : int -> tactic,
and the integer argument is a subgoal number;
if tacf1 sg replaces subgoal sg by a number of subgoals,
tacf2 is then applied to each of those subgoals *)
fun (tacf1 THENEXP tacf2) sg state =
let fun tac2 newstate =
(THENR sg (nprems_of newstate - nprems_of state + sg) tacf2) newstate
in (tacf1 sg THEN tac2) state end ;
val op THENEXP = op THEN_ALL_NEW ;
(* resThen : 'a Seq.seq -> ('a -> 'b Seq.seq) -> 'b Seq.seq
like tactical THEN, except res is result of applying first tactic *)
fun resThen res tac2 = Seq.flat (Seq.map tac2 res) ;
(* resThenExp : thm Seq.seq -> (int -> tactic) -> (int -> tactic)
like THENEXP where res is result of first tactic *)
fun resThenExp res tacf2 sg state =
let val nafter = nprems_of state - sg
fun tac2 newstate = (THENR sg (nprems_of newstate - nafter) tacf2) newstate
in resThen res tac2 end ;
fun (tacf1 THENEXP tacf2) sg state =
resThenExp (tacf1 sg state) tacf2 sg state ;
(* REPEXP : (int -> tactic) -> int -> tactic
repeats a tactic on a given subgoal and all resulting subgoals;
note the inefficiency of recalculating tacf sg state in the first version *)
fun REPEXP tacf sg state =
case Seq.pull (tacf sg state) of NONE => Seq.single state
| _ => (tacf THENEXP REPEXP tacf) sg state ;
fun REPEXP tacf sg state =
case Seq.pull (tacf sg state) of NONE => Seq.single state
| SOME res => resThenExp (Seq.cons res) (REPEXP tacf) sg state ;
(* REPINC, REPINC1 : int -> (int -> tactic) -> int -> tactic
repeats a tactic on a subgoal number which gets incremented each time,
REPINC1 must succeed once *)
fun REPINC1 inc tacf sg state =
(tacf sg THEN REPINC inc tacf (sg + inc)) state
and REPINC inc tacf sg state = TRY (REPINC1 inc tacf sg) state ;
(* REP_DET_EXP : (int -> tactic) -> int -> tactic
tacf: int -> tactic, and isg a subgoal,
repeats trying tacf on isg and all subgoals resulting;
deterministic, ie only uses first result of each tactic application *)
fun REP_DET_EXP tacf isg state =
let
val nabove = nprems_of state - isg
fun reptac sg st =
if sg + nabove > nprems_of st then st
else
case Seq.pull (tacf sg st) of
NONE => reptac (sg+1) st
| SOME (nst, _) => reptac sg nst
in Seq.single (reptac isg state) end ;
(* 94-7: structure is Sequence, not Seq *)
fun SOMEGOALRG tf l h = FIRST (map tf (h downto l)) ;
(* TEST : (thm -> bool) -> tactic
tactic succeeds (with same state) if state satisfies p *)
fun TEST p st = if p st then all_tac st else no_tac st ;
(* CAN_TAC : tactic -> thm -> bool
test on state, whether tactic succeeds or not *)
fun CAN_TAC tac st = Option.isSome (Seq.pull (tac st)) ;
(* CAN : tactic -> tactic
the tactic which succeeds (with same state) if tac succeeds *)
fun CAN tac st = TEST (CAN_TAC tac) st ;
(* MUSTFAIL : tactic -> tactic
MUSTFAIL' : ('a -> tactic) -> 'a -> tactic
tactic succeeds (with same state) iff tac fails *)
fun MUSTFAIL tac st =
case Seq.pull (tac st) of NONE => all_tac st
| SOME _ => no_tac st ;
fun MUSTFAIL' tf i = MUSTFAIL (tf i) ;
(* UNIQUE : tactic -> tactic
tactic must succeed with a unique solution *)
fun UNIQUE tac st =
case Seq.pull (tac st) of NONE => Seq.empty
| SOME (nst, nseq) =>
case Seq.pull nseq of NONE => Seq.cons (nst, nseq)
| SOME _ => Seq.empty ;
(* MSSG : (int -> tactic) -> int -> tactic
(MustSolveSubGoal) makes tactic fail unless it solves subgoal *)
fun MSSG tf = tf THEN_ALL_NEW (fn i => no_tac) ;
(* nosg_tac, sg_tac : int -> tactic
succeeds iff given sg does NOT / does exist *)
fun nosg_tac sg st = if nprems_of st >= sg then Seq.empty else Seq.single st ;
fun sg_tac sg st = if nprems_of st >= sg then Seq.single st else Seq.empty ;
(* WHILE : tactic list -> tactic
WHILE' : ('a -> tactic) list -> 'a -> tactic
do tactics in list, until one fails;
tactic fails if first one fails *)
fun WHILE [] = all_tac
| WHILE (tac :: tacs) = tac THEN TRY (WHILE tacs) ;
fun WHILE' tacs i = WHILE (fmap tacs i) ;
(* LAST : (int -> tactic) -> tactic, applies tac to last goal *)
fun LAST tac st = let val sg = nprems_of st in tac sg st end ;
(* mkps : thm -> unit, make new proof state from theorem *)
fun mkps th = by (PRIMITIVE (fn _ => th)) ;
(* apply2sgs : (term -> bool) -> (int -> tactic) -> tactic
apply given subgoal-tactic to those subgoals satisfying cond
(couldn't we use SUBGOAL for this ?? *)
fun apply2sgs cond sgtac state =
let val prems = prems_of state
(* doprems : int -> term list -> tactic
apply sgtac to given list of subgoals, which start from number n;
attack subgoals in descending order (to avoid problems
with changing numbering of subgoals) *)
fun doprems n (p :: ps) =
if cond p then doprems (n+1) ps THEN sgtac n
else doprems (n+1) ps
| doprems _ [] = all_tac
in doprems 1 prems state end ;
infix 0 RSL ;
(* RSL : thm * thm -> thm
resolves th1 with last premise of th2 *)
fun (th1 RSL th2) = th1 RSN (nprems_of th2, th2) ;
(* mkass : thm -> thm, turns premises of thm (no Vars) into assumptions *)
fun mkass frozen =
let
val cps = cprems_of frozen ;
val cas = map assume cps ;
val ie = implies_elim_list frozen cas ;
in ie end ;
(* reop : (thm list -> thm list) -> thm -> thm
reorder premises in theorem *)
fun reop reof thm =
let
val (frozen, thaw) = freeze_thaw thm ;
val ct = cprop_of frozen ;
val cps = cprems_of frozen ;
val cas = map assume cps ;
val ie = implies_elim_list frozen cas ;
val ih' = implies_intr_list (reof cps) ie ;
in varifyT (thaw ih') end ;
(* rdp : thm -> thm
rdpn : thm -> thm
removes duplicated premises in theorem, rdp does standard first (why ??) *)
fun rdpn th =
let
val (frozen, thaw) = freeze_thaw th ;
val cps = cprems_of frozen ;
val cas = map assume cps ;
val ie = implies_elim_list frozen cas ;
val ih = implies_intr_hyps ie ;
in thaw ih end ;
val rdp = rdpn o standard ;
(* alternative to the above, remove duplicate premises
in a theorem whose premises have no assumptions *)
val rdp_tac = EVERY [use_sg_tac,
(ANYGOAL atac THEN ANYGOAL atac), TRYALL atac, TRYALL (etac thin_rl) ] ;
fun rem_dup_prems th =
let val (fth, thaw) = freeze_thaw th ;
val rth = tacthm (REPEAT rdp_tac) fth ;
in thaw rth end ;
(*
fun ti0 inp =
case BasisLibrary.Int.fromString inp of SOME i => i
| NONE => 0 ;
fun ti1 inp =
case BasisLibrary.Int.fromString inp of NONE => 0
| SOME i => i ;
fun ti2 inp =
(case BasisLibrary.Int.fromString inp of NONE => false
| _ => true) ;
ti2 "akl" ; (* result true *)
ti1 "1" ; (* result 1 *)
ti1 "akl" ; (* crashes *)
*)
(* query_tac : int -> tactic -> tactic
require input before performing tactic *)
fun query_tac lim tac st =
let val _ = Display.print_goals lim st ;
val inp = (old_inputLine TextIO.stdIn)
in if hd (explode inp) = "q" then no_tac st
else tac st end ;
(* step_aux : ('a -> Tactical.tactic) -> 'a list -> 'a list
to go through a proof step by step, returning rest of list *)
fun step_aux f (tacs as tac::tacl) =
let val inp = (old_inputLine TextIO.stdIn)
in if hd (explode inp) = "q" then tac :: tacl
else (case Int.fromString inp of
NONE => (by (f tac) ; step_aux f tacl)
| SOME i => (byev (map f (Library.take (i, tacs))) ;
step_aux f (Library.drop (i, tacs))))
handle e => (tac :: tacl) end
| step_aux _ [] = [] ;
(* step : tactic list -> tactic list
stepl : tactic list list -> tactic list list
step' : ('a -> tactic) list -> 'a -> ('a -> tactic) list
stepl' : ('a -> tactic) list list -> 'a -> ('a -> tactic) list list
*)
val step = step_aux Library.I ;
val stepl = step_aux EVERY ;
fun step' tacfs n = step_aux (fn tf => tf n) tacfs ;
fun stepl' tacfss n = step_aux (fn tfs => EVERY' tfs n) tacfss ;
(* abbreviations *)
fun tby tac = timeap by tac ;
fun b1 tacf = by (tacf 1) ;
fun b2 tacf = by (tacf 2) ;
fun b3 tacf = by (tacf 3) ;
fun bn n tacf = by (tacf n) ;
fun bag tacf = by (ALLGOALS tacf) ;
fun bta tacf = by (TRYALL tacf) ;
fun tbag tacf = tby (ALLGOALS tacf) ;
fun byfn f = byev (f (premises())) ;
fun byall [] = []
| byall (tac :: tacs) = (by tac ; byall tacs) handle _ => tac :: tacs ;
fun byall' tacfs n = byall (fmap tacfs n) ;
fun byev' tacfs n = byev (fmap tacfs n) ;
fun safe () = by Safe_tac ;
(* EVERYL : tactic list list -> tactic
EVERYL' : ('a -> tactic) list list -> 'a -> tactic *)
fun EVERYL tss = EVERY (map EVERY tss) ;
fun EVERYL' tss = EVERY' (map EVERY' tss) ;
fun byalll [] = []
| byalll (tac :: tacs) = (byev tac ; byalll tacs) handle _ => tac :: tacs ;
fun byalll' tacfs n = byalll (fmap tacfs n) ;
(* stepf : (thm list -> tactic list) -> tactic list
as step, but use the same function argument as prove_goal
ie, when using "goal" command, to step through a proof given
in the form required by "prove_goal" command *)
fun stepf f = step (f (premises())) ;
(* inst_tac : (string * string) list -> tactic
to instantiate unknowns in proof state,
note - leave out the index, as this is very changeable *)
fun inst_tac insts state =
Seq.single (read_instantiate insts (zero_var_indexes state)) ;
(* prems_only : (int -> tactic) -> (thm -> tactic) -> tactic
make tactics, such as simplification, affect only the premises of a subgoal
*)
fun prems_only tacfp tacf st =
let
val sg1 = nth (cprems_of st, 0) ;
val sg1p = Drule.strip_imp_prems sg1 ;
val ap = map assume sg1p ;
val ctP = read_cterm (sign_of (the_context())) ("P", propT) ;
val thP = trivial ctP ;
val thseq = EVERY [(cut_facts_tac ap 1), tacfp 1] thP ;
val (_, thawP) = freeze_thaw (standard thP) ;
val th' = thawP (Seq.hd thseq) ;
val th = implies_intr_hyps th' ;
in tacf th st end ;
(* chop_tac : int -> tactic -> tactic
chop_tac' : int -> ('a -> tactic) -> ('a -> tactic)
discards first n result states *)
fun chop_tac n tac state = snd (Seq.chop (n, tac state)) ;
fun chop_tac' n tacf a state = snd (Seq.chop (n, tacf a state)) ;
(* chop_last : tactic -> tactic
discards all but last result states, avoiding recomputation *)
fun chop_last tac state =
let open Seq
fun last (seq, tl) =
case pull tl of NONE => seq | SOME (a, s) => last (tl, s) ;
val ts = tac state ;
in last (ts, ts) end ;
(* where you want to augment set of premises using forward_tac repeatedly,
but can't use REPEAT because same premise will get acted on *)
(* chops_tac : tactic -> tactic
repeat tactic n times, chopped n-1, ..., 0 times *)
fun chops_tac 0 tac = all_tac
| chops_tac n tac =
let val n1 = n-1 in chop_tac n1 tac THEN chops_tac n1 tac end ;
(* chops_auto : tactic -> tactic
repeat tactic n times, n given by trying tactic once *)
fun chops_auto tac state =
let val n = length (Seq.list_of (tac state)) ;
in chops_tac n tac state end ;
(* rep_forw_tac : thm list -> int -> tactic
does forward_tac repeatedly (on original premises) *)
fun rep_forw_tac ths = chops_auto o (forward_tac ths) ;
(* apply tacf to top subgoal *)
fun bt tacf =
let fun tac st =
let val n = nprems_of st ; in tacf n st end ;
in by (tac) end ;
(** finding the theorems we want **)
(* tc : xstring list -> (string list * thm) list
tct : xstring list -> theory list -> (string list * thm) list
tcs : xstring list -> string list -> (string list * thm) list
tcta : xstring list -> theory -> (string list * thm) list
like thms_containing, but tct limited to given theories;
tcta limited to theory and ancestors;
tcs like tct, but specifies theories as strings,
they all sort on size of theorem, and remove duplicates,
all use thms_containing, so results within theory of current proof *)
(* rd : ('a list * thm) list -> ('a list * thm) list
remove consecutive duplicate thms, listing all names for a given thm *)
fun rd ((s1, th1) :: (s2, th2) :: sths) =
if eq_thm (th1, th2) then rd ((s1 @ s2, th1) :: sths)
else (s1, th1) :: rd ((s2, th2) :: sths)
| rd sths = sths ;
(* sst : ('a * thm) list -> ('a list * thm) list
list theorems in order of size *)
fun sst thl =
let fun mks (s, th) = ((s, th), (prop_of th)) ;
val thsl = map mks thl ;
fun comp ((_, s1), (_, s2)) = Term.term_ord (s1, s2) ;
val ss = Library.sort comp thsl ;
val res = map (fn ((s, th), _) => ([s], th)) ss ;
in res end ;
(* match_name : string -> string -> bool
inmn : string list -> string -> bool
subsetmn : string list -> string list -> bool
equality, membership, subset, all modified to allow matching of
names partly qualified to various extent;
in arguments fq = fully qualified, pq = partly qualified, eg
match_name "y.z" "x.y.z" = true ;
inmn ["x.y.z", "a.b"] "y.z" = true ;
subsetmn ["z", "a.b"] ["x.y.z", "a.b"] = true ;
*)
fun match_name pqual fqual =
let fun rparts name = rev (String.fields (equal #".") name) ;
in Library.prefix (Library.pairself rparts (pqual, fqual)) end ;
fun inmn fqs pq = List.exists (match_name pq) fqs ;
fun subsetmn pqs fqs = List.all (inmn fqs) pqs ;
(* test whether part of theorem matches pattern given,
seems to need exact match of type classes *)
fun pmatch pat th =
let val thy = the_context () ;
val tsig = Sign.tsig_of (sign_of thy) ;
in Pattern.matches_subterm thy (pat, prop_of th) end ;
(* cmatch : term -> term -> bool
really simple matching of pattern to term *)
fun cmatch (pf $ pa) (tf $ ta) = cmatch pf tf andalso cmatch pa ta
| cmatch (Const (pn, _)) (Const (tn, _)) = pn = tn
| cmatch (Free _) _ = true
| cmatch (Var _) _ = true
| cmatch (Abs (_, _, pt)) (Abs (_, _, tt)) = cmatch pt tt
| cmatch (Bound pn) (Bound tn) = pn = tn
| cmatch _ _ = false ;
(* cppmatch, cpmatch : term -> term -> bool
cppmatch tries to match a proper subterm of arg2
cpmatch tries to match a subterm of arg2 *)
fun cppmatch pat (f $ a) = cpmatch pat f orelse cpmatch pat a
| cppmatch pat (Abs (_, _, b)) = cpmatch pat b
| cppmatch pat _ = false
and cpmatch pat tm = cmatch pat tm orelse cppmatch pat tm ;
(* film, filpm : term -> ('a * thm) list -> ('a * thm) list
filrpm : string -> ('a * thm) list -> ('a * thm) list
test whether theorem, any part of theorem, matches pattern,
eg filpm pat (tc strs), filrpm text (tc strs) *)
fun filpm pat = filter (fn (_, th) => cpmatch pat (prop_of th)) ;
fun film pat = filter (fn (_, th) =>
cmatch pat (prop_of th) orelse
cmatch pat (HOLogic.dest_Trueprop (prop_of th))
handle _ => false) ; (* HOL only *)
fun filrpm text = filpm (read text) ;
(* thcc : string list -> thm -> bool
test whether theorem actually contains given list of constants *)
fun thcc consts th = subsetmn consts (Term.term_consts (prop_of th)) ;
fun size_ok (_, th) = size_of_thm th < 1000 ;
fun tc' consts = filter (thcc consts o snd) (thms_containing consts) ;
val tc = rd o sst o filter size_ok o tc' ;
fun tct' consts thys =
let val tc_consts = tc' consts ;
fun n_of_thy thy = map fst (PureThy.thms_of thy) ;
val names_thys = List.concat (map n_of_thy thys) ;
fun inthy name = name mem names_thys ;
fun oneInThy nl = exists inthy nl ;
val nInThy = filter (inthy o fst) tc_consts ;
in nInThy end ;
val tct = let open Library in (rd o sst) oo tct' end ;
fun tcs consts thynames = tct consts (map theory thynames) ;
fun tcta strs thy = tct strs (thy :: ancestors_of thy) ;
(* eg
val ts = tct([ "op +", "op -"])([ Ring_and_Field_thy]) ;
val fts = filpm (read "(a = b) = (c = d)") ts ;
val fts = film (read "(a + b) = (c + d)") ts ;
*)
(* spf : unit -> unit -> proof
save proof as a function, to save printing it out *)
fun spf () =
let val pf' = save_proof () ;
fun pf () = pf' ;
in pf end ;
(* rpf : (unit -> proof) -> unit
restore proof from a function *)
fun rpf pf = (restore_proof (pf ()) ; pr()) ;
fun pup _ = push_proof () ;
fun pop _ = pop_proof () ;
fun b1 tacf = by (tacf 1) ;
fun b2 tacf = by (tacf 2) ;
fun bn n tacf = by (tacf n) ;
fun bag tacf = by (ALLGOALS tacf) ;
fun byfn f = byev (f (premises())) ;
fun byall [] = []
| byall (tac :: tacs) = (by tac ; byall tacs) handle _ => tac :: tacs ;
val tt = theory_of_thm ;
val sgt = sign_of_thm ;
(* getall : thm list -> thm list
getall [] gets all the states of a proof *)
fun getall sts =
let val st = topthm () ;
in let val _ = chop() ;
in getall (st :: sts) end
handle ERROR => st :: sts end ;
fun thy_prove thy str = prove_goal thy str (fn _ => [CLASIMPSET auto_tac]) ;
fun thy_prove_fs thy str = prove_goal thy str
(fn _ => [CLASET Classical.safe_tac, (TRYALL (CLASET' fast_tac)),
(ALLGOALS (SIMPSET' simp_tac))]) ;
(* to test whether a theorem belongs to current theory *)
fun curthy th = eq_thy (the_context (), theory_of_thm th) ;
fun plb str = TextIO.print (legacy_bindings (theory str)) ;
fun ulb str = (use_legacy_bindings (theory str)) ;
val cthy = ref "" ;
fun ub str = (cthy := str ; reset trace_simp ;
update_thy str handle _ => () ; beep ()) ;
fun ubp _ = ub (!cthy) ;
fun uall _ = ub "all" ;
(* apply tactic to frozen state, then thaw,
doesn't do types properly *)
fun freeze_tac tac state =
let val (fth, thaw) = freeze_thaw state ;
in Seq.map thaw (tac fth) end ;
(* assume we want all free types turned back to variables *)
fun freeze_vty_tac tac state =
let val (fth, thaw) = freeze_thaw state ;
in Seq.map (Thm.varifyT o thaw) (tac fth) end ;
(* where tactic used repeatedly fails, to store point of failure *)
val goal_ref = ref asm_rl ;
fun store tac state = (goal_ref := state ; tac state) ;
fun store_on_fail tac = (tac ORELSE store no_tac) ;
(* looking at theories, signatures, etc *)
(* type classes, sorts, etc *)
fun expass (k, ds) = List.map (fn d => (k, d)) ds ;
fun expall kdss = List.concat (map expass kdss) ;
(* tycl : theory -> string list * string list
information re type classes *)
(*
fun tycl thy =
let val {sign, ...} = Theory.rep_theory thy ;
val {tsig, ...} = Sign.rep_sg sign ;
val {classrel, arities, ...} = Type.rep_tsig tsig ;
val cls = Symtab.dest classrel ;
val ars = Symtab.dest arities ;
val scls = List.map Sorts.str_of_classrel (expall cls) ;
fun mar (t, (c, sl)) = (t, sl, [c]) ;
val sars = List.map (Sign.string_of_arity thy o mar) (expall ars) ;
in (scls, sars) end ;
*)
(*
val (scls, sars) = tycl thy ;
*)
(* mk_dummyT : term -> term
change a term to have dummy types, so it will be shorter when printed *)
fun mk_dummyT (Const (str, _)) = Const (str, dummyT)
| mk_dummyT (Free (str, _)) = Free (str, dummyT)
| mk_dummyT (Var (ixn, _)) = Var (ixn, dummyT)
| mk_dummyT (t $ u) = mk_dummyT t $ mk_dummyT u
| mk_dummyT (Abs (str, _, t)) = (Abs (str, dummyT, mk_dummyT t))
| mk_dummyT (Bound i) = Bound i ;
(* print theory or parts of it *)
fun pfthy thy =
let
val ptl as [ names, name_prefix,
classes, default, witness, syntactic, logical, arities,
consts, abbrevs, constraints, axioms, oracles, definitions ] =
Display.pretty_full_theory thy ;
in { all = ptl, names = names, name_prefix = name_prefix,
classes = classes, default = default, witness = witness,
syntactic = syntactic, logical = logical, arities = arities,
consts = consts, abbrevs = abbrevs, constraints = constraints,
axioms = axioms, oracles = oracles, definitions = definitions }
end ;
functor Pfthy (val thy : theory) = struct
val ptl as [ names, theory_data, proof_data, name_prefix,
classes, default, witness, syntactic, logical, arities,
consts, constraints, axioms, oracles ] =
Display.pretty_full_theory thy ;
end ;
(*several object-logics declare theories that hide basis library structures*)
structure BasisLibrary =
struct
structure List = List;
structure Option = Option;
structure Bool = Bool;
structure String = String;
structure Int = Int;
structure Real = Real;
end;
(*
structure Pthy = Pfthy (val thy = the_context ()) ;
open Pthy ;
val pt = Pretty.chunks ptl ;
TextIO.print (Pretty.output pt) ; (* same as Pretty.string_of ? *)
TextIO.print (Pretty.output classes) ; (* same as Pretty.string_of ? *)
TextIO.print (Pretty.output arities) ; (* same as Pretty.string_of ? *)
fun prt n = TextIO.print (Pretty.output (List.nth (ptl, n))) ;
*)