--- a/src/FOL/IFOL.thy Wed Sep 12 17:26:05 2012 +0200
+++ b/src/FOL/IFOL.thy Wed Sep 12 22:00:29 2012 +0200
@@ -13,7 +13,6 @@
ML_file "~~/src/Provers/hypsubst.ML"
ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
ML_file "~~/src/Tools/IsaPlanner/isand.ML"
-ML_file "~~/src/Tools/IsaPlanner/rw_tools.ML"
ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
ML_file "~~/src/Tools/eqsubst.ML"
ML_file "~~/src/Provers/quantifier1.ML"
--- a/src/HOL/HOL.thy Wed Sep 12 17:26:05 2012 +0200
+++ b/src/HOL/HOL.thy Wed Sep 12 22:00:29 2012 +0200
@@ -18,7 +18,6 @@
ML_file "~~/src/Tools/solve_direct.ML"
ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
ML_file "~~/src/Tools/IsaPlanner/isand.ML"
-ML_file "~~/src/Tools/IsaPlanner/rw_tools.ML"
ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
ML_file "~~/src/Provers/hypsubst.ML"
ML_file "~~/src/Provers/splitter.ML"
--- a/src/Tools/IsaPlanner/isand.ML Wed Sep 12 17:26:05 2012 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Wed Sep 12 22:00:29 2012 +0200
@@ -8,7 +8,7 @@
instead, we work with newly introduced frees, and hide the
"all"'s, exporting results from theorems proved with the frees, to
solve the all cases of the previous goal. This allows resolution
-to do proof search normally.
+to do proof search normally.
Note: A nice idea: allow exporting to solve any subgoal, thus
allowing the interleaving of proof, or provide a structure for the
@@ -23,113 +23,35 @@
signature ISA_ND =
sig
-
- (* export data *)
- datatype export = export of
- {gth: Thm.thm, (* initial goal theorem *)
- sgid: int, (* subgoal id which has been fixed etc *)
- fixes: Thm.cterm list, (* frees *)
- assumes: Thm.cterm list} (* assumptions *)
- val fixes_of_exp : export -> Thm.cterm list
- val export_back : export -> Thm.thm -> Thm.thm Seq.seq
- val export_solution : export -> Thm.thm -> Thm.thm
- val export_solutions : export list * Thm.thm -> Thm.thm
-
(* inserting meta level params for frees in the conditions *)
- val allify_conditions :
- (Term.term -> Thm.cterm) ->
- (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
- val allify_conditions' :
- (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
- val assume_allified :
- theory -> (string * Term.sort) list * (string * Term.typ) list
- -> Term.term -> (Thm.cterm * Thm.thm)
+ val allify_conditions : (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
(* meta level fixed params (i.e. !! vars) *)
- val fix_alls_in_term : Term.term -> Term.term * Term.term list
- val fix_alls_term : int -> Term.term -> Term.term * Term.term list
- val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list
- val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list
- val fix_alls : int -> Thm.thm -> Thm.thm * export
+ val fix_alls_term : int -> term -> term * term list
- (* meta variables in types and terms *)
- val fix_tvars_to_tfrees_in_terms
- : string list (* avoid these names *)
- -> Term.term list ->
- (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *)
- val fix_vars_to_frees_in_terms
- : string list (* avoid these names *)
- -> Term.term list ->
- (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *)
- val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm
- val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm
- val fix_vars_and_tvars :
- Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm
- val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm
- val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm
- val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm
- val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm
- val unfix_frees_and_tfrees :
- (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm
+ val unfix_frees : cterm list -> thm -> thm
(* assumptions/subgoals *)
- val assume_prems :
- int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list
- val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
- val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export
- val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list
- val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list
-
- (* abstracts cterms (vars) to locally meta-all bounds *)
- val prepare_goal_export : string list * Thm.cterm list -> Thm.thm
- -> int * Thm.thm
- val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq
- val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
+ val fixed_subgoal_thms : thm -> thm list * (thm list -> thm)
end
-
-structure IsaND
-: ISA_ND
-= struct
-
-(* Solve *some* subgoal of "th" directly by "sol" *)
-(* Note: this is probably what Markus ment to do upon export of a
-"show" but maybe he used RS/rtac instead, which would wrongly lead to
-failing if there are premices to the shown goal.
-
-given:
-sol : Thm.thm = [| Ai... |] ==> Ci
-th : Thm.thm =
- [| ... [| Ai... |] ==> Ci ... |] ==> G
-results in:
- [| ... [| Ai-1... |] ==> Ci-1
- [| Ai+1... |] ==> Ci+1 ...
- |] ==> G
-i.e. solves some subgoal of th that is identical to sol.
-*)
-fun solve_with sol th =
- let fun solvei 0 = Seq.empty
- | solvei i =
- Seq.append (Thm.bicompose false (false,sol,0) i th) (solvei (i - 1))
- in
- solvei (Thm.nprems_of th)
- end;
-
+structure IsaND : ISA_ND =
+struct
(* Given ctertmify function, (string,type) pairs capturing the free
vars that need to be allified in the assumption, and a theorem with
assumptions possibly containing the free vars, then we give back the
-assumptions allified as hidden hyps.
+assumptions allified as hidden hyps.
-Given: x
-th: A vs ==> B vs
+Given: x
+th: A vs ==> B vs
Results in: "B vs" [!!x. A x]
*)
-fun allify_conditions ctermify Ts th =
- let
+fun allify_conditions ctermify Ts th =
+ let
val premts = Thm.prems_of th;
-
- fun allify_prem_var (vt as (n,ty),t) =
+
+ fun allify_prem_var (vt as (n,ty),t) =
(Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
fun allify_prem Ts p = List.foldr allify_prem_var p Ts
@@ -137,308 +59,64 @@
val cTs = map (ctermify o Free) Ts
val cterm_asms = map (ctermify o allify_prem Ts) premts
val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
- in
+ in
(Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
end;
-fun allify_conditions' Ts th =
- allify_conditions (Thm.cterm_of (Thm.theory_of_thm th)) Ts th;
-
-(* allify types *)
-fun allify_typ ts ty =
- let
- fun trec (x as (TFree (s,srt))) =
- (case Library.find_first (fn (s2,srt2) => s = s2) ts
- of NONE => x
- | SOME (s2,_) => TVar ((s,0),srt))
- (* Maybe add in check here for bad sorts?
- if srt = srt2 then TVar ((s,0),srt)
- else raise ("thaw_typ", ts, ty) *)
- | trec (Type (s,typs)) = Type (s, map trec typs)
- | trec (v as TVar _) = v;
- in trec ty end;
-
-(* implicit types and term *)
-fun allify_term_typs ty = Term.map_types (allify_typ ty);
-
-(* allified version of term, given frees to allify over. Note that we
-only allify over the types on the given allified cterm, we can't do
-this for the theorem as we are not allowed type-vars in the hyp. *)
-(* FIXME: make the allified term keep the same conclusion as it
-started with, rather than a strictly more general version (ie use
-instantiate with initial params we abstracted from, rather than
-forall_elim_vars. *)
-fun assume_allified sgn (tyvs,vs) t =
- let
- fun allify_var (vt as (n,ty),t) =
- (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
- fun allify Ts p = List.foldr allify_var p Ts
-
- val ctermify = Thm.cterm_of sgn;
- val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs
- val allified_term = t |> allify vs;
- val ct = ctermify allified_term;
- val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term);
- in (typ_allified_ct,
- Thm.forall_elim_vars 0 (Thm.assume ct)) end;
-
-
-(* change type-vars to fresh type frees *)
-fun fix_tvars_to_tfrees_in_terms names ts =
- let
- val tfree_names = map fst (List.foldr Misc_Legacy.add_term_tfrees [] ts);
- val tvars = List.foldr Misc_Legacy.add_term_tvars [] ts;
- val (names',renamings) =
- List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) =>
- let val n2 = singleton (Name.variant_list Ns) n in
- (n2::Ns, (tv, (n2,s))::Rs)
- end) (tfree_names @ names,[]) tvars;
- in renamings end;
-fun fix_tvars_to_tfrees th =
- let
- val sign = Thm.theory_of_thm th;
- val ctypify = Thm.ctyp_of sign;
- val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
- val renamings = fix_tvars_to_tfrees_in_terms
- [] ((Thm.prop_of th) :: tpairs);
- val crenamings =
- map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f)))
- renamings;
- val fixedfrees = map snd crenamings;
- in (fixedfrees, Thm.instantiate (crenamings, []) th) end;
-
-
-(* change type-free's to type-vars in th, skipping the ones in "ns" *)
-fun unfix_tfrees ns th =
- let
- val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
- val skiptfrees = subtract (op =) varfiytfrees (Misc_Legacy.add_term_tfrees (Thm.prop_of th,[]));
- in #2 (Thm.varifyT_global' skiptfrees th) end;
-
-(* change schematic/meta vars to fresh free vars, avoiding name clashes
- with "names" *)
-fun fix_vars_to_frees_in_terms names ts =
- let
- val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars [] ts);
- val Ns = List.foldr Misc_Legacy.add_term_names names ts;
- val (_,renamings) =
- Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) =>
- let val n2 = singleton (Name.variant_list Ns) n in
- (n2 :: Ns, (v, (n2,ty)) :: Rs)
- end) ((Ns,[]), vars);
- in renamings end;
-fun fix_vars_to_frees th =
- let
- val ctermify = Thm.cterm_of (Thm.theory_of_thm th)
- val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
- val renamings = fix_vars_to_frees_in_terms
- [] ([Thm.prop_of th] @ tpairs);
- val crenamings =
- map (fn (v,f) => (ctermify (Var v), ctermify (Free f)))
- renamings;
- val fixedfrees = map snd crenamings;
- in (fixedfrees, Thm.instantiate ([], crenamings) th) end;
-
-fun fix_tvars_upto_idx ix th =
- let
- val sgn = Thm.theory_of_thm th;
- val ctypify = Thm.ctyp_of sgn
- val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
- val prop = (Thm.prop_of th);
- val tvars = List.foldr Misc_Legacy.add_term_tvars [] (prop :: tpairs);
- val ctyfixes =
- map_filter
- (fn (v as ((s,i),ty)) =>
- if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
- else NONE) tvars;
- in Thm.instantiate (ctyfixes, []) th end;
-fun fix_vars_upto_idx ix th =
- let
- val sgn = Thm.theory_of_thm th;
- val ctermify = Thm.cterm_of sgn
- val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
- val prop = (Thm.prop_of th);
- val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars
- [] (prop :: tpairs));
- val cfixes =
- map_filter
- (fn (v as ((s,i),ty)) =>
- if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
- else NONE) vars;
- in Thm.instantiate ([], cfixes) th end;
-
-
(* make free vars into schematic vars with index zero *)
- fun unfix_frees frees =
+fun unfix_frees frees =
fold (K (Thm.forall_elim_var 0)) frees
o Drule.forall_intr_list frees;
-(* fix term and type variables *)
-fun fix_vars_and_tvars th =
- let val (tvars, th') = fix_tvars_to_tfrees th
- val (vars, th'') = fix_vars_to_frees th'
- in ((vars, tvars), th'') end;
-
-(* implicit Thm.thm argument *)
-(* assumes: vars may contain fixed versions of the frees *)
-(* THINK: what if vs already has types varified? *)
-fun unfix_frees_and_tfrees (vs,tvs) =
- (unfix_tfrees tvs o unfix_frees vs);
-
(* datatype to capture an exported result, ie a fix or assume. *)
-datatype export =
+datatype export =
export of {fixes : Thm.cterm list, (* fixed vars *)
assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
sgid : int,
gth : Thm.thm}; (* subgoal/goalthm *)
-fun fixes_of_exp (export rep) = #fixes rep;
-
-(* export the result of the new goal thm, ie if we reduced teh
-subgoal, then we get a new reduced subtgoal with the old
-all-quantified variables *)
-local
-
-(* allify puts in a meta level univ quantifier for a free variavble *)
-fun allify_term (v, t) =
- let val vt = #t (Thm.rep_cterm v)
- val (n,ty) = Term.dest_Free vt
- in (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
-
-fun allify_for_sg_term ctermify vs t =
- let val t_alls = List.foldr allify_term t vs;
- val ct_alls = ctermify t_alls;
- in
- (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
- end;
-(* lookup type of a free var name from a list *)
-fun lookupfree vs vn =
- case Library.find_first (fn (n,ty) => n = vn) vs of
- NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term")
- | SOME x => x;
-in
-fun export_back (export {fixes = vs, assumes = hprems,
- sgid = i, gth = gth}) newth =
- let
- val sgn = Thm.theory_of_thm newth;
- val ctermify = Thm.cterm_of sgn;
-
- val sgs = prems_of newth;
- val (sgallcts, sgthms) =
- Library.split_list (map (allify_for_sg_term ctermify vs) sgs);
- val minimal_newth =
- (Library.foldl (fn ( newth', sgthm) =>
- Drule.compose_single (sgthm, 1, newth'))
- (newth, sgthms));
- val allified_newth =
- minimal_newth
- |> Drule.implies_intr_list hprems
- |> Drule.forall_intr_list vs
-
- val newth' = Drule.implies_intr_list sgallcts allified_newth
- in
- Thm.bicompose false (false, newth', (length sgallcts)) i gth
- end;
-
-(*
-Given "vs" : names of free variables to abstract over,
-Given cterms : premices to abstract over (P1... Pn) in terms of vs,
-Given a thm of the form:
-P1 vs; ...; Pn vs ==> Goal(C vs)
-
-Gives back:
-(n, length of given cterms which have been allified
- [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm
-*)
-(* note: C may contain further premices etc
-Note that cterms is the assumed facts, ie prems of "P1" that are
-reintroduced in allified form.
-*)
-fun prepare_goal_export (vs, cterms) th =
- let
- val sgn = Thm.theory_of_thm th;
- val ctermify = Thm.cterm_of sgn;
-
- val allfrees = map Term.dest_Free (Misc_Legacy.term_frees (Thm.prop_of th))
- val cfrees = map (ctermify o Free o lookupfree allfrees) vs
-
- val sgs = prems_of th;
- val (sgallcts, sgthms) =
- Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs);
-
- val minimal_th =
- Goal.conclude (Library.foldl (fn ( th', sgthm) =>
- Drule.compose_single (sgthm, 1, th'))
- (th, sgthms));
-
- val allified_th =
- minimal_th
- |> Drule.implies_intr_list cterms
- |> Drule.forall_intr_list cfrees
-
- val th' = Drule.implies_intr_list sgallcts allified_th
- in
- ((length sgallcts), th')
- end;
-
-end;
-
-
(* exporting function that takes a solution to the fixed/assumed goal,
and uses this to solve the subgoal in the main theorem *)
fun export_solution (export {fixes = cfvs, assumes = hcprems,
- sgid = i, gth = gth}) solth =
- let
- val solth' =
+ sgid = i, gth = gth}) solth =
+ let
+ val solth' =
solth |> Drule.implies_intr_list hcprems
|> Drule.forall_intr_list cfvs
in Drule.compose_single (solth', i, gth) end;
-fun export_solutions (xs,th) = List.foldr (uncurry export_solution) th xs;
-
(* fix parameters of a subgoal "i", as free variables, and create an
exporting function that will use the result of this proved goal to
-show the goal in the original theorem.
+show the goal in the original theorem.
Note, an advantage of this over Isar is that it supports instantiation
of unkowns in the earlier theorem, ie we can do instantiation of meta
-vars!
+vars!
-avoids constant, free and vars names.
+avoids constant, free and vars names.
loosely corresponds to:
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
-Result:
- ("(As ==> SGi x') ==> (As ==> SGi x')" : thm,
- expf :
- ("As ==> SGi x'" : thm) ->
+Result:
+ ("(As ==> SGi x') ==> (As ==> SGi x')" : thm,
+ expf :
+ ("As ==> SGi x'" : thm) ->
("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
*)
-fun fix_alls_in_term alledt =
+fun fix_alls_term i t =
let
- val t = Term.strip_all_body alledt;
- val alls = rev (Term.strip_all_vars alledt);
- val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
- val names = Misc_Legacy.add_term_names (t,varnames);
- val fvs = map Free
- (Name.variant_list names (map fst alls)
- ~~ (map snd alls));
- in ((subst_bounds (fvs,t)), fvs) end;
-
-fun fix_alls_term i t =
- let
val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
val names = Misc_Legacy.add_term_names (t,varnames);
val gt = Logic.get_goal t i;
val body = Term.strip_all_body gt;
val alls = rev (Term.strip_all_vars gt);
- val fvs = map Free
+ val fvs = map Free
(Name.variant_list names (map fst alls)
~~ (map snd alls));
in ((subst_bounds (fvs,body)), fvs) end;
-fun fix_alls_cterm i th =
+fun fix_alls_cterm i th =
let
val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
@@ -448,20 +126,20 @@
(ct_body, cfvs)
end;
-fun fix_alls' i =
+fun fix_alls' i =
(apfst Thm.trivial) o (fix_alls_cterm i);
-(* hide other goals *)
+(* hide other goals *)
(* note the export goal is rotated by (i - 1) and will have to be
unrotated to get backto the originial position(s) *)
-fun hide_other_goals th =
+fun hide_other_goals th =
let
(* tl beacuse fst sg is the goal we are interested in *)
val cprems = tl (Drule.cprems_of th)
val aprems = map Thm.assume cprems
in
- (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems,
+ (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems,
cprems)
end;
@@ -470,104 +148,36 @@
namely the subgoal that we were trying to solve. *)
(* loosely corresponds to:
Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
-Result:
- ("(As ==> SGi x') ==> SGi x'" : thm,
- expf :
- ("SGi x'" : thm) ->
+Result:
+ ("(As ==> SGi x') ==> SGi x'" : thm,
+ expf :
+ ("SGi x'" : thm) ->
("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
*)
-fun fix_alls i th =
- let
+fun fix_alls i th =
+ let
val (fixed_gth, fixedvars) = fix_alls' i th
val (sml_gth, othergoals) = hide_other_goals fixed_gth
in
- (sml_gth, export {fixes = fixedvars,
- assumes = othergoals,
+ (sml_gth, export {fixes = fixedvars,
+ assumes = othergoals,
sgid = i, gth = th})
end;
-(* assume the premises of subgoal "i", this gives back a list of
-assumed theorems that are the premices of subgoal i, it also gives
-back a new goal thm and an exporter, the new goalthm is as the old
-one, but without the premices, and the exporter will use a proof of
-the new goalthm, possibly using the assumed premices, to shoe the
-orginial goal.
-
-Note: Dealing with meta vars, need to meta-level-all them in the
-shyps, which we can later instantiate with a specific value.... ?
-think about this... maybe need to introduce some new fixed vars and
-then remove them again at the end... like I do with rw_inst.
-
-loosely corresponds to:
-Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm
-Result:
-(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions
- "SGi ==> SGi" : thm, -- new goal
- "SGi" ["A0" ... "An"] : thm -> -- export function
- ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
-*)
-fun assume_prems i th =
- let
- val t = (prop_of th);
- val gt = Logic.get_goal t i;
- val _ = case Term.strip_all_vars gt of [] => ()
- | _ => error "assume_prems: goal has params"
- val body = gt;
- val prems = Logic.strip_imp_prems body;
- val concl = Logic.strip_imp_concl body;
-
- val sgn = Thm.theory_of_thm th;
- val ctermify = Thm.cterm_of sgn;
- val cprems = map ctermify prems;
- val aprems = map Thm.assume cprems;
- val gthi = Thm.trivial (ctermify concl);
-
- (* fun explortf thi =
- Drule.compose (Drule.implies_intr_list cprems thi,
- i, th) *)
- in
- (aprems, gthi, cprems)
- end;
-
-
-(* first fix the variables, then assume the assumptions *)
-(* loosely corresponds to:
-Given
- "[| SG0; ...
- !! xs. [| A0 xs; ... An xs |] ==> SGi xs;
- ... SGm |] ==> G" : thm
-Result:
-(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions
- "SGi xs' ==> SGi xs'" : thm, -- new goal
- "SGi xs'" ["A0 xs'" ... "An xs'"] : thm -> -- export function
- ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
-*)
-
-(* Note: the fix_alls actually pulls through all the assumptions which
-means that the second export is not needed. *)
-fun fixes_and_assumes i th =
- let
- val (fixgth, exp1) = fix_alls i th
- val (assumps, goalth, _) = assume_prems 1 fixgth
- in
- (assumps, goalth, exp1)
- end;
-
-
(* Fixme: allow different order of subgoals given to expf *)
(* make each subgoal into a separate thm that needs to be proved *)
(* loosely corresponds to:
-Given
+Given
"[| SG0; ... SGm |] ==> G" : thm
-Result:
+Result:
(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
["SG0", ..., "SGm"] : thm list -> -- export function
"G" : thm)
*)
-fun subgoal_thms th =
- let
- val t = (prop_of th);
+fun subgoal_thms th =
+ let
+ val t = (prop_of th);
val prems = Logic.strip_imp_prems t;
@@ -576,58 +186,37 @@
val aprems = map (Thm.trivial o ctermify) prems;
- fun explortf premths =
+ fun explortf premths =
Drule.implies_elim_list th premths
in
(aprems, explortf)
end;
-(* make all the premices of a theorem hidden, and provide an unhide
-function, that will bring them back out at a later point. This is
-useful if you want to get back these premices, after having used the
-theorem with the premices hidden *)
-(* loosely corresponds to:
-Given "As ==> G" : thm
-Result: ("G [As]" : thm,
- "G [As]" : thm -> "As ==> G" : thm
-*)
-fun hide_prems th =
- let
- val cprems = Drule.cprems_of th;
- val aprems = map Thm.assume cprems;
- (* val unhidef = Drule.implies_intr_list cprems; *)
- in
- (Drule.implies_elim_list th aprems, cprems)
- end;
-
-
-
-
(* Fixme: allow different order of subgoals in exportf *)
(* as above, but also fix all parameters in all subgoals, and uses
fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
subgoals. *)
(* loosely corresponds to:
-Given
- "[| !! x0s. A0s x0s ==> SG0 x0s;
+Given
+ "[| !! x0s. A0s x0s ==> SG0 x0s;
...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
-Result:
-(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'",
+Result:
+(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'",
... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function
"G" : thm)
*)
(* requires being given solutions! *)
-fun fixed_subgoal_thms th =
- let
+fun fixed_subgoal_thms th =
+ let
val (subgoals, expf) = subgoal_thms th;
(* fun export_sg (th, exp) = exp th; *)
- fun export_sgs expfs solthms =
+ fun export_sgs expfs solthms =
expf (map2 (curry (op |>)) solthms expfs);
(* expf (map export_sg (ths ~~ expfs)); *)
- in
- apsnd export_sgs (Library.split_list (map (apsnd export_solution o
+ in
+ apsnd export_sgs (Library.split_list (map (apsnd export_solution o
fix_alls 1) subgoals))
end;
--- a/src/Tools/IsaPlanner/rw_inst.ML Wed Sep 12 17:26:05 2012 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Wed Sep 12 22:00:29 2012 +0200
@@ -3,61 +3,34 @@
Rewriting using a conditional meta-equality theorem which supports
schematic variable instantiation.
-*)
+*)
signature RW_INST =
sig
+ val beta_eta_contract : thm -> thm
+
(* Rewrite: give it instantiation infromation, a rule, and the
target thm, and it will return the rewritten target thm *)
val rw :
- ((Term.indexname * (Term.sort * Term.typ)) list * (* type var instantiations *)
- (Term.indexname * (Term.typ * Term.term)) list) (* schematic var instantiations *)
- * (string * Term.typ) list (* Fake named bounds + types *)
- * (string * Term.typ) list (* names of bound + types *)
- * Term.term -> (* outer term for instantiation *)
- Thm.thm -> (* rule with indexies lifted *)
- Thm.thm -> (* target thm *)
- Thm.thm (* rewritten theorem possibly
- with additional premises for
- rule conditions *)
-
- (* used tools *)
- val mk_abstractedrule :
- (string * Term.typ) list (* faked outer bound *)
- -> (string * Term.typ) list (* hopeful name of outer bounds *)
- -> Thm.thm -> Thm.cterm list * Thm.thm
- val mk_fixtvar_tyinsts :
- (Term.indexname * (Term.sort * Term.typ)) list ->
- Term.term list -> ((string * int) * (Term.sort * Term.typ)) list
- * (string * Term.sort) list
- val mk_renamings :
- Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
- val new_tfree :
- ((string * int) * Term.sort) *
- (((string * int) * (Term.sort * Term.typ)) list * string list) ->
- ((string * int) * (Term.sort * Term.typ)) list * string list
- val cross_inst : (Term.indexname * (Term.typ * Term.term)) list
- -> (Term.indexname *(Term.typ * Term.term)) list
- val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list
- -> (Term.indexname * (Term.sort * Term.typ)) list
-
- val beta_contract : Thm.thm -> Thm.thm
- val beta_eta_contract : Thm.thm -> Thm.thm
-
+ ((indexname * (sort * typ)) list * (* type var instantiations *)
+ (indexname * (typ * term)) list) (* schematic var instantiations *)
+ * (string * typ) list (* Fake named bounds + types *)
+ * (string * typ) list (* names of bound + types *)
+ * term -> (* outer term for instantiation *)
+ thm -> (* rule with indexies lifted *)
+ thm -> (* target thm *)
+ thm (* rewritten theorem possibly
+ with additional premises for
+ rule conditions *)
end;
-structure RWInst
-: RW_INST
-= struct
+structure RWInst : RW_INST =
+struct
-(* beta contract the theorem *)
-fun beta_contract thm =
- Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
-
(* beta-eta contract the theorem *)
-fun beta_eta_contract thm =
+fun beta_eta_contract thm =
let
val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
@@ -79,7 +52,7 @@
creates an abstracted version of the theorem, with local bound vars as
lambda-params:
-Ts:
+Ts:
("x", ty)
rule::
@@ -91,19 +64,18 @@
note: assumes rule is instantiated
*)
(* Note, we take abstraction in the order of last abstraction first *)
-fun mk_abstractedrule TsFake Ts rule =
- let
+fun mk_abstractedrule TsFake Ts rule =
+ let
val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
- (* now we change the names of temporary free vars that represent
+ (* now we change the names of temporary free vars that represent
bound vars with binders outside the redex *)
- val prop = Thm.prop_of rule;
val names = usednames_of_thm rule;
- val (fromnames,tonames,names2,Ts') =
- Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
+ val (fromnames,tonames,_,Ts') =
+ Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
let val n2 = singleton (Name.variant_list names) n in
(ctermify (Free(faken,ty)) :: rnf,
- ctermify (Free(n2,ty)) :: rnt,
+ ctermify (Free(n2,ty)) :: rnt,
n2 :: names,
(n2,ty) :: Ts'')
end)
@@ -113,14 +85,14 @@
with introduced vars from bounds outside in redex *)
val rule' = rule |> Drule.forall_intr_list fromnames
|> Drule.forall_elim_list tonames;
-
+
(* make unconditional rule and prems *)
- val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts')
+ val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts')
rule';
(* using these names create lambda-abstracted version of the rule *)
val abstractions = rev (Ts' ~~ tonames);
- val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) =>
+ val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) =>
Thm.abstract_rule n ct th)
(uncond_rule, abstractions);
in (cprems, abstract_rule) end;
@@ -131,21 +103,21 @@
variables *)
(* make fixed unique free variable instantiations for non-ground vars *)
(* Create a table of vars to be renamed after instantiation - ie
- other uninstantiated vars in the hyps of the rule
+ other uninstantiated vars in the hyps of the rule
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
-fun mk_renamings tgt rule_inst =
+fun mk_renamings tgt rule_inst =
let
val rule_conds = Thm.prems_of rule_inst
val names = List.foldr Misc_Legacy.add_term_names [] (tgt :: rule_conds);
- val (conds_tyvs,cond_vs) =
- Library.foldl (fn ((tyvs, vs), t) =>
+ val (_, cond_vs) =
+ Library.foldl (fn ((tyvs, vs), t) =>
(union (op =) (Misc_Legacy.term_tvars t) tyvs,
union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs))
(([],[]), rule_conds);
- val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
+ val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
val vars_to_fix = union (op =) termvars cond_vs;
- val (renamings, names2) =
- List.foldr (fn (((n,i),ty), (vs, names')) =>
+ val (renamings, _) =
+ List.foldr (fn (((n,i),ty), (vs, names')) =>
let val n' = singleton (Name.variant_list names') n in
((((n,i),ty), Free (n', ty)) :: vs, n'::names')
end)
@@ -158,17 +130,17 @@
in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
-(* make instantiations to fix type variables that are not
+(* make instantiations to fix type variables that are not
already instantiated (in ignore_ixs) from the list of terms. *)
-fun mk_fixtvar_tyinsts ignore_insts ts =
- let
+fun mk_fixtvar_tyinsts ignore_insts ts =
+ let
val ignore_ixs = map fst ignore_insts;
- val (tvars, tfrees) =
- List.foldr (fn (t, (varixs, tfrees)) =>
+ val (tvars, tfrees) =
+ List.foldr (fn (t, (varixs, tfrees)) =>
(Misc_Legacy.add_term_tvars (t,varixs),
Misc_Legacy.add_term_tfrees (t,tfrees)))
([],[]) ts;
- val unfixed_tvars =
+ val unfixed_tvars =
filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
in (fixtyinsts, tfrees) end;
@@ -177,27 +149,27 @@
(* cross-instantiate the instantiations - ie for each instantiation
replace all occurances in other instantiations - no loops are possible
and thus only one-parsing of the instantiations is necessary. *)
-fun cross_inst insts =
- let
- fun instL (ix, (ty,t)) =
- map (fn (ix2,(ty2,t2)) =>
+fun cross_inst insts =
+ let
+ fun instL (ix, (ty,t)) =
+ map (fn (ix2,(ty2,t2)) =>
(ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
fun cross_instL ([], l) = rev l
- | cross_instL ((ix, t) :: insts, l) =
+ | cross_instL ((ix, t) :: insts, l) =
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
in cross_instL (insts, []) end;
(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
-fun cross_inst_typs insts =
- let
- fun instL (ix, (srt,ty)) =
- map (fn (ix2,(srt2,ty2)) =>
+fun cross_inst_typs insts =
+ let
+ fun instL (ix, (srt,ty)) =
+ map (fn (ix2,(srt2,ty2)) =>
(ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
fun cross_instL ([], l) = rev l
- | cross_instL ((ix, t) :: insts, l) =
+ | cross_instL ((ix, t) :: insts, l) =
cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
in cross_instL (insts, []) end;
@@ -212,42 +184,40 @@
first abstraction first. FakeTs has abstractions using the fake name
- ie the name distinct from all other abstractions. *)
-fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
- let
+fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
+ let
(* general signature info *)
val target_sign = (Thm.theory_of_thm target_thm);
val ctermify = Thm.cterm_of target_sign;
val ctypeify = Thm.ctyp_of target_sign;
(* fix all non-instantiated tvars *)
- val (fixtyinsts, othertfrees) =
+ val (fixtyinsts, othertfrees) =
mk_fixtvar_tyinsts nonfixed_typinsts
[Thm.prop_of rule, Thm.prop_of target_thm];
- val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
- fixtyinsts;
val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
(* certified instantiations for types *)
- val ctyp_insts =
- map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty))
+ val ctyp_insts =
+ map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty))
typinsts;
(* type instantiated versions *)
val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule;
- val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
+ val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts;
(* type instanitated outer term *)
val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
- val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
+ val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
FakeTs;
- val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
+ val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
Ts;
(* type-instantiate the var instantiations *)
- val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) =>
- (ix, (Term.typ_subst_TVars term_typ_inst ty,
+ val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) =>
+ (ix, (Term.typ_subst_TVars term_typ_inst ty,
Term.subst_TVars term_typ_inst t))
:: insts_tyinst)
[] unprepinsts;
@@ -256,36 +226,36 @@
val insts_tyinst_inst = cross_inst insts_tyinst;
(* create certms of instantiations *)
- val cinsts_tyinst =
- map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)),
+ val cinsts_tyinst =
+ map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)),
ctermify t)) insts_tyinst_inst;
(* The instantiated rule *)
val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
(* Create a table of vars to be renamed after instantiation - ie
- other uninstantiated vars in the hyps the *instantiated* rule
+ other uninstantiated vars in the hyps the *instantiated* rule
ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
- val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst)
+ val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst)
rule_inst;
- val cterm_renamings =
+ val cterm_renamings =
map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
(* Create the specific version of the rule for this target application *)
- val outerterm_inst =
- outerterm_tyinst
+ val outerterm_inst =
+ outerterm_tyinst
|> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
|> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
val couter_inst = Thm.reflexive (ctermify outerterm_inst);
- val (cprems, abstract_rule_inst) =
+ val (cprems, abstract_rule_inst) =
rule_inst |> Thm.instantiate ([], cterm_renamings)
|> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
- val specific_tgt_rule =
+ val specific_tgt_rule =
beta_eta_contract
(Thm.combination couter_inst abstract_rule_inst);
(* create an instantiated version of the target thm *)
- val tgt_th_inst =
+ val tgt_th_inst =
tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
|> Thm.instantiate ([], cterm_renamings);
@@ -302,4 +272,4 @@
end;
-end; (* struct *)
+end;
--- a/src/Tools/IsaPlanner/rw_tools.ML Wed Sep 12 17:26:05 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,179 +0,0 @@
-(* Title: Tools/IsaPlanner/rw_tools.ML
- Author: Lucas Dixon, University of Edinburgh
-
-Term related tools used for rewriting.
-*)
-
-signature RWTOOLS =
-sig
-end;
-
-structure RWTools
-= struct
-
-(* fake free variable names for locally bound variables - these work
-as placeholders. *)
-
-(* don't use dest_fake.. - we should instead be working with numbers
-and a list... else we rely on naming conventions which can break, or
-be violated - in contrast list locations are correct by
-construction/definition. *)
-(*
-fun dest_fake_bound_name n =
- case (raw_explode n) of (* FIXME Symbol.explode (?) *)
- (":" :: realchars) => implode realchars
- | _ => n; *)
-fun is_fake_bound_name n = (hd (raw_explode n) = ":"); (* FIXME Symbol.explode (?) *)
-fun mk_fake_bound_name n = ":b_" ^ n;
-
-
-
-(* fake free variable names for local meta variables - these work
-as placeholders. *)
-fun dest_fake_fix_name n =
- case (raw_explode n) of (* FIXME Symbol.explode (?) *)
- ("@" :: realchars) => implode realchars
- | _ => n;
-fun is_fake_fix_name n = (hd (raw_explode n) = "@"); (* FIXME Symbol.explode (?) *)
-fun mk_fake_fix_name n = "@" ^ n;
-
-
-
-(* fake free variable names for meta level bound variables *)
-fun dest_fake_all_name n =
- case (raw_explode n) of (* FIXME Symbol.explode (?) *)
- ("+" :: realchars) => implode realchars
- | _ => n;
-fun is_fake_all_name n = (hd (raw_explode n) = "+"); (* FIXME Symbol.explode (?) *)
-fun mk_fake_all_name n = "+" ^ n;
-
-
-
-
-(* Ys and Ts not used, Ns are real names of faked local bounds, the
-idea is that this will be mapped to free variables thus if a free
-variable is a faked local bound then we change it to being a meta
-variable so that it can later be instantiated *)
-(* FIXME: rename this - avoid the word fix! *)
-(* note we are not really "fix"'ing the free, more like making it variable! *)
-(* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) =
- if n mem Ns then Var((n,0),ty) else Free (n,ty);
-*)
-
-(* make a var into a fixed free (ie prefixed with "@") *)
-fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty);
-
-
-(* mk_frees_bound: string list -> Term.term -> Term.term *)
-(* This function changes free variables to being represented as bound
-variables if the free's variable name is in the given list. The debruijn
-index is simply the position in the list *)
-(* THINKABOUT: danger of an existing free variable with the same name: fix
-this so that name conflict are avoided automatically! In the meantime,
-don't have free variables named starting with a ":" *)
-fun bounds_of_fakefrees Ys (a $ b) =
- (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b)
- | bounds_of_fakefrees Ys (Abs(n,ty,t)) =
- Abs(n,ty, bounds_of_fakefrees (n::Ys) t)
- | bounds_of_fakefrees Ys (Free (n,ty)) =
- let fun try_mk_bound_of_free (i,[]) = Free (n,ty)
- | try_mk_bound_of_free (i,(y::ys)) =
- if n = y then Bound i else try_mk_bound_of_free (i+1,ys)
- in try_mk_bound_of_free (0,Ys) end
- | bounds_of_fakefrees Ys t = t;
-
-
-(* map a function f onto each free variables *)
-fun map_to_frees f Ys (a $ b) =
- (map_to_frees f Ys a) $ (map_to_frees f Ys b)
- | map_to_frees f Ys (Abs(n,ty,t)) =
- Abs(n,ty, map_to_frees f ((n,ty)::Ys) t)
- | map_to_frees f Ys (Free a) =
- f Ys a
- | map_to_frees f Ys t = t;
-
-
-(* map a function f onto each meta variable *)
-fun map_to_vars f Ys (a $ b) =
- (map_to_vars f Ys a) $ (map_to_vars f Ys b)
- | map_to_vars f Ys (Abs(n,ty,t)) =
- Abs(n,ty, map_to_vars f ((n,ty)::Ys) t)
- | map_to_vars f Ys (Var a) =
- f Ys a
- | map_to_vars f Ys t = t;
-
-(* map a function f onto each free variables *)
-fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) =
- let val (n2,ty2) = f (n,ty)
- in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end
- | map_to_alls f x = x;
-
-(* map a function f to each type variable in a term *)
-(* implicit arg: term *)
-fun map_to_term_tvars f =
- Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x); (* FIXME map_atyps !? *)
-
-
-
-(* what if a param desn't occur in the concl? think about! Note: This
-simply fixes meta level univ bound vars as Frees. At the end, we will
-change them back to schematic vars that will then unify
-appropriactely, ie with unfake_vars *)
-fun fake_concl_of_goal gt i =
- let
- val prems = Logic.strip_imp_prems gt
- val sgt = nth prems (i - 1)
-
- val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt)
- val tparams = Term.strip_all_vars sgt
-
- val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty))
- tparams
- in
- Term.subst_bounds (rev fakefrees,tbody)
- end;
-
-(* what if a param desn't occur in the concl? think about! Note: This
-simply fixes meta level univ bound vars as Frees. At the end, we will
-change them back to schematic vars that will then unify
-appropriactely, ie with unfake_vars *)
-fun fake_goal gt i =
- let
- val prems = Logic.strip_imp_prems gt
- val sgt = nth prems (i - 1)
-
- val tbody = Term.strip_all_body sgt
- val tparams = Term.strip_all_vars sgt
-
- val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty))
- tparams
- in
- Term.subst_bounds (rev fakefrees,tbody)
- end;
-
-
-(* hand written - for some reason the Isabelle version in drule is broken!
-Example? something to do with Bin Yangs examples?
- *)
-fun rename_term_bvars ns (Abs(s,ty,t)) =
- let val s2opt = Library.find_first (fn (x,y) => s = x) ns
- in case s2opt of
- NONE => (Abs(s,ty,rename_term_bvars ns t))
- | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end
- | rename_term_bvars ns (a$b) =
- (rename_term_bvars ns a) $ (rename_term_bvars ns b)
- | rename_term_bvars _ x = x;
-
-fun rename_thm_bvars ns th =
- let val t = Thm.prop_of th
- in Thm.rename_boundvars t (rename_term_bvars ns t) th end;
-
-(* Finish this to show how it breaks! (raises the exception):
-
-exception rename_thm_bvars_exp of ((string * string) list * Thm.thm)
-
- Drule.rename_bvars ns th
- handle TERM _ => raise rename_thm_bvars_exp (ns, th);
-*)
-
-end;
--- a/src/Tools/eqsubst.ML Wed Sep 12 17:26:05 2012 +0200
+++ b/src/Tools/eqsubst.ML Wed Sep 12 22:00:29 2012 +0200
@@ -19,99 +19,47 @@
* int (* maxidx *)
* Zipper.T (* focusterm to search under *)
- exception eqsubst_occL_exp of
- string * int list * thm list * int * thm
-
- (* low level substitution functions *)
- val apply_subst_in_asm :
- int ->
- thm ->
- thm ->
- (cterm list * int * 'a * thm) * match -> thm Seq.seq
- val apply_subst_in_concl :
- int ->
- thm ->
- cterm list * thm ->
- thm -> match -> thm Seq.seq
+ datatype 'a skipseq = SkipMore of int | SkipSeq of 'a Seq.seq Seq.seq
- (* matching/unification within zippers *)
- val clean_match_z :
- theory -> term -> Zipper.T -> match option
- val clean_unify_z :
- theory -> int -> term -> Zipper.T -> match Seq.seq
-
- (* skipping things in seq seq's *)
-
- (* skipping non-empty sub-sequences but when we reach the end
- of the seq, remembering how much we have left to skip. *)
- datatype 'a skipseq = SkipMore of int
- | SkipSeq of 'a Seq.seq Seq.seq;
-
- val skip_first_asm_occs_search :
- ('a -> 'b -> 'c Seq.seq Seq.seq) ->
- 'a -> int -> 'b -> 'c skipseq
- val skip_first_occs_search :
- int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
- val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
+ val skip_first_asm_occs_search :
+ ('a -> 'b -> 'c Seq.seq Seq.seq) ->
+ 'a -> int -> 'b -> 'c skipseq
+ val skip_first_occs_search :
+ int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
+ val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
- (* tactics *)
- val eqsubst_asm_tac :
- Proof.context ->
- int list -> thm list -> int -> tactic
- val eqsubst_asm_tac' :
- Proof.context ->
- (searchinfo -> int -> term -> match skipseq) ->
- int -> thm -> int -> tactic
- val eqsubst_tac :
- Proof.context ->
- int list -> (* list of occurences to rewrite, use [0] for any *)
- thm list -> int -> tactic
- val eqsubst_tac' :
- Proof.context -> (* proof context *)
- (searchinfo -> term -> match Seq.seq) (* search function *)
- -> thm (* equation theorem to rewrite with *)
- -> int (* subgoal number in goal theorem *)
- -> thm (* goal theorem *)
- -> thm Seq.seq (* rewritten goal theorem *)
-
-
- val fakefree_badbounds :
- (string * typ) list ->
- term ->
- (string * typ) list * (string * typ) list * term
+ (* tactics *)
+ val eqsubst_asm_tac :
+ Proof.context ->
+ int list -> thm list -> int -> tactic
+ val eqsubst_asm_tac' :
+ Proof.context ->
+ (searchinfo -> int -> term -> match skipseq) ->
+ int -> thm -> int -> tactic
+ val eqsubst_tac :
+ Proof.context ->
+ int list -> (* list of occurences to rewrite, use [0] for any *)
+ thm list -> int -> tactic
+ val eqsubst_tac' :
+ Proof.context -> (* proof context *)
+ (searchinfo -> term -> match Seq.seq) (* search function *)
+ -> thm (* equation theorem to rewrite with *)
+ -> int (* subgoal number in goal theorem *)
+ -> thm (* goal theorem *)
+ -> thm Seq.seq (* rewritten goal theorem *)
- val mk_foo_match :
- (term -> term) ->
- ('a * typ) list -> term -> term
+ (* search for substitutions *)
+ val valid_match_start : Zipper.T -> bool
+ val search_lr_all : Zipper.T -> Zipper.T Seq.seq
+ val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
+ val searchf_lr_unify_all :
+ searchinfo -> term -> match Seq.seq Seq.seq
+ val searchf_lr_unify_valid :
+ searchinfo -> term -> match Seq.seq Seq.seq
+ val searchf_bt_unify_valid :
+ searchinfo -> term -> match Seq.seq Seq.seq
- (* preparing substitution *)
- val prep_meta_eq : Proof.context -> thm -> thm list
- val prep_concl_subst :
- int -> thm -> (cterm list * thm) * searchinfo
- val prep_subst_in_asm :
- int -> thm -> int ->
- (cterm list * int * int * thm) * searchinfo
- val prep_subst_in_asms :
- int -> thm ->
- ((cterm list * int * int * thm) * searchinfo) list
- val prep_zipper_match :
- Zipper.T -> term * ((string * typ) list * (string * typ) list * term)
-
- (* search for substitutions *)
- val valid_match_start : Zipper.T -> bool
- val search_lr_all : Zipper.T -> Zipper.T Seq.seq
- val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
- val searchf_lr_unify_all :
- searchinfo -> term -> match Seq.seq Seq.seq
- val searchf_lr_unify_valid :
- searchinfo -> term -> match Seq.seq Seq.seq
- val searchf_bt_unify_valid :
- searchinfo -> term -> match Seq.seq Seq.seq
-
- (* Isar level hooks *)
- val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method
- val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method
- val setup : theory -> theory
+ val setup : theory -> theory
end;
@@ -142,25 +90,25 @@
datatype 'a skipseq = SkipMore of int
| SkipSeq of 'a Seq.seq Seq.seq;
(* given a seqseq, skip the first m non-empty seq's, note deficit *)
-fun skipto_skipseq m s =
- let
- fun skip_occs n sq =
- case Seq.pull sq of
+fun skipto_skipseq m s =
+ let
+ fun skip_occs n sq =
+ case Seq.pull sq of
NONE => SkipMore n
- | SOME (h,t) =>
+ | SOME (h,t) =>
(case Seq.pull h of NONE => skip_occs n t
| SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
else skip_occs (n - 1) t)
in (skip_occs m s) end;
-(* note: outerterm is the taget with the match replaced by a bound
- variable : ie: "P lhs" beocmes "%x. P x"
+(* note: outerterm is the taget with the match replaced by a bound
+ variable : ie: "P lhs" beocmes "%x. P x"
insts is the types of instantiations of vars in lhs
and typinsts is the type instantiations of types in the lhs
- Note: Final rule is the rule lifted into the ontext of the
+ Note: Final rule is the rule lifted into the ontext of the
taget thm. *)
-fun mk_foo_match mkuptermfunc Ts t =
- let
+fun mk_foo_match mkuptermfunc Ts t =
+ let
val ty = Term.type_of t
val bigtype = (rev (map snd Ts)) ---> ty
fun mk_foo 0 t = t
@@ -172,12 +120,13 @@
(* T is outer bound vars, n is number of locally bound vars *)
(* THINK: is order of Ts correct...? or reversed? *)
-fun fakefree_badbounds Ts t =
- let val (FakeTs,Ts,newnames) =
- List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
+fun mk_fake_bound_name n = ":b_" ^ n;
+fun fakefree_badbounds Ts t =
+ let val (FakeTs,Ts,newnames) =
+ List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
let val newname = singleton (Name.variant_list usednames) n
- in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
- (newname,ty)::Ts,
+ in ((mk_fake_bound_name newname,ty)::FakeTs,
+ (newname,ty)::Ts,
newname::usednames) end)
([],[],[])
Ts
@@ -187,9 +136,9 @@
abstraction. In this function we additionally construct the
abstraction environment, and an outer context term (with the focus
abstracted out) for use in rewriting with RWInst.rw *)
-fun prep_zipper_match z =
- let
- val t = Zipper.trm z
+fun prep_zipper_match z =
+ let
+ val t = Zipper.trm z
val c = Zipper.ctxt z
val Ts = Zipper.C.nty_ctxt c
val (FakeTs', Ts', t') = fakefree_badbounds Ts t
@@ -198,12 +147,7 @@
(t', (FakeTs', Ts', absterm))
end;
-(* Matching and Unification with exception handled *)
-fun clean_match thy (a as (pat, t)) =
- let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
- in SOME (Vartab.dest tyenv, Vartab.dest tenv)
- end handle Pattern.MATCH => NONE;
-
+(* Unification with exception handled *)
(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
fun clean_unify thry ix (a as (pat, tgt)) =
let
@@ -242,41 +186,18 @@
| NONE => Seq.empty
end;
-(* Matching and Unification for zippers *)
+(* Unification for zippers *)
(* Note: Ts is a modified version of the original names of the outer
bound variables. New names have been introduced to make sure they are
unique w.r.t all names in the term and each other. usednames' is
oldnames + new names. *)
-fun clean_match_z thy pat z =
- let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
- case clean_match thy (pat, t) of
- NONE => NONE
- | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
(* ix = max var index *)
-fun clean_unify_z sgn ix pat z =
+fun clean_unify_z sgn ix pat z =
let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
- Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
+ Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
(clean_unify sgn ix (t, pat)) end;
-(* FOR DEBUGGING...
-type trace_subst_errT = int (* subgoal *)
- * thm (* thm with all goals *)
- * (cterm list (* certified free var placeholders for vars *)
- * thm) (* trivial thm of goal concl *)
- (* possible matches/unifiers *)
- * thm (* rule *)
- * (((indexname * typ) list (* type instantiations *)
- * (indexname * term) list ) (* term instantiations *)
- * (string * typ) list (* Type abs env *)
- * term) (* outer term *);
-
-val trace_subst_err = (Unsynchronized.ref NONE : trace_subst_errT option Unsynchronized.ref);
-val trace_subst_search = Unsynchronized.ref false;
-exception trace_subst_exp of trace_subst_errT;
-*)
-
-
fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
| bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
| bot_left_leaf_of x = x;
@@ -284,8 +205,8 @@
(* Avoid considering replacing terms which have a var at the head as
they always succeed trivially, and uninterestingly. *)
fun valid_match_start z =
- (case bot_left_leaf_of (Zipper.trm z) of
- Var _ => false
+ (case bot_left_leaf_of (Zipper.trm z) of
+ Var _ => false
| _ => true);
(* search from top, left to right, then down *)
@@ -293,12 +214,12 @@
(* search from top, left to right, then down *)
fun search_lr_valid validf =
- let
- fun sf_valid_td_lr z =
+ let
+ fun sf_valid_td_lr z =
let val here = if validf z then [Zipper.Here z] else [] in
- case Zipper.trm z
- of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)]
- @ here
+ case Zipper.trm z
+ of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)]
+ @ here
@ [Zipper.LookIn (Zipper.move_down_right z)]
| Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
| _ => here
@@ -308,11 +229,11 @@
(* search from bottom to top, left to right *)
fun search_bt_valid validf =
- let
- fun sf_valid_td_lr z =
+ let
+ fun sf_valid_td_lr z =
let val here = if validf z then [Zipper.Here z] else [] in
- case Zipper.trm z
- of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z),
+ case Zipper.trm z
+ of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z),
Zipper.LookIn (Zipper.move_down_right z)] @ here
| Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
| _ => here
@@ -320,7 +241,7 @@
in Zipper.lzy_search sf_valid_td_lr end;
fun searchf_unify_gen f (sgn, maxidx, z) lhs =
- Seq.map (clean_unify_z sgn maxidx lhs)
+ Seq.map (clean_unify_z sgn maxidx lhs)
(Zipper.limit_apply f z);
(* search all unifications *)
@@ -328,7 +249,7 @@
searchf_unify_gen search_lr_all;
(* search only for 'valid' unifiers (non abs subterms and non vars) *)
-val searchf_lr_unify_valid =
+val searchf_lr_unify_valid =
searchf_unify_gen (search_lr_valid valid_match_start);
val searchf_bt_unify_valid =
@@ -390,8 +311,6 @@
the given theorems*)
-exception eqsubst_occL_exp of
- string * (int list) * (thm list) * int * thm;
fun skip_first_occs_search occ srchf sinfo lhs =
case (skipto_skipseq occ (srchf sinfo lhs)) of
SkipMore _ => Seq.empty
@@ -408,8 +327,8 @@
let val thmseq = (Seq.of_list thms)
fun apply_occ occ th =
thmseq |> Seq.maps
- (fn r => eqsubst_tac'
- ctxt
+ (fn r => eqsubst_tac'
+ ctxt
(skip_first_occs_search
occ searchf_lr_unify_valid) r
(i + ((Thm.nprems_of th) - nprems))
@@ -419,8 +338,7 @@
in
Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
end
- end
- handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
+ end;
(* inthms are the given arguments in Isar, and treated as eqstep with
@@ -534,8 +452,7 @@
Seq.map distinct_subgoals
(Seq.EVERY (map apply_occ sortedoccs) th)
end
- end
- handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
+ end;
(* inthms are the given arguments in Isar, and treated as eqstep with
the first one, then the second etc *)