--- a/src/HOL/Tools/function_package/context_tree.ML Mon Jul 16 21:17:12 2007 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML Mon Jul 16 21:22:43 2007 +0200
@@ -9,19 +9,19 @@
signature FUNDEF_CTXTREE =
sig
+ type depgraph
type ctx_tree
(* FIXME: This interface is a mess and needs to be cleaned up! *)
val cong_deps : thm -> int IntGraph.T
val add_congs : thm list
- val mk_tree: (thm * FundefCommon.depgraph) list ->
- (string * typ) -> term -> Proof.context -> term -> FundefCommon.ctx_tree
+ val mk_tree: (thm * depgraph) list ->
+ (string * typ) -> term -> Proof.context -> term -> ctx_tree
- val inst_tree: theory -> term -> term -> FundefCommon.ctx_tree
- -> FundefCommon.ctx_tree
+ val inst_tree: theory -> term -> term -> ctx_tree -> ctx_tree
- val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list
+ val add_context_varnames : ctx_tree -> string list -> string list
val export_term : (string * typ) list * term list -> term -> term
val export_thm : theory -> (string * typ) list * term list -> thm -> thm
@@ -33,9 +33,9 @@
(((string * typ) list * thm list) * thm) list ->
(((string * typ) list * thm list) * thm) list * 'b ->
(((string * typ) list * thm list) * thm) list * 'b)
- -> FundefCommon.ctx_tree -> 'b -> 'b
+ -> ctx_tree -> 'b -> 'b
- val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> FundefCommon.ctx_tree -> thm * (thm * thm) list
+ val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> ctx_tree -> thm * (thm * thm) list
end
structure FundefCtxTree : FUNDEF_CTXTREE =
@@ -44,6 +44,13 @@
open FundefCommon
open FundefLib
+type depgraph = int IntGraph.T
+
+datatype ctx_tree
+ = Leaf of term
+ | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
+ | RCall of (term * ctx_tree)
+
(* Maps "Trueprop A = B" to "A" *)
val rhs_of = snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
@@ -160,7 +167,7 @@
fun import_thm thy (fixes, athms) =
fold (forall_elim o cterm_of thy o Free) fixes
- #> fold implies_elim_swp athms
+ #> fold (flip implies_elim) athms
fun assume_in_ctxt thy (fixes, athms) prop =
let
--- a/src/HOL/Tools/function_package/fundef_common.ML Mon Jul 16 21:17:12 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Jul 16 21:22:43 2007 +0200
@@ -26,14 +26,6 @@
val rel_name = suffix "_rel"
val dom_name = suffix "_dom"
-type depgraph = int IntGraph.T
-
-datatype ctx_tree
- = Leaf of term
- | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
- | RCall of (term * ctx_tree)
-
-
datatype fundef_result =
FundefResult of
@@ -58,6 +50,7 @@
{
defname : string,
+ (* contains no logical entities: invariant under morphisms *)
add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
fs : term list,
@@ -73,7 +66,7 @@
val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
val name = Morphism.name phi
in
- FundefCtxData { add_simps = add_simps (* contains no logical entities *),
+ FundefCtxData { add_simps = add_simps,
fs = map term fs, R = term R, psimps = fact psimps,
pinducts = fact pinducts, termination = thm termination,
defname = name defname }
@@ -154,7 +147,6 @@
FundefData.map (fold (fn f => NetRules.insert (f, data)) fs)
#> store_termination_rule termination
-
(* Configuration management *)
datatype fundef_opt
= Sequential
@@ -186,6 +178,10 @@
fun target_of (FundefConfig {target, ...}) = target
+val default_config = FundefConfig { sequential=false, default="%x. arbitrary",
+ target=NONE, domintros=false, tailrec=false }
+
+
(* Common operations on equations *)
fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
@@ -248,7 +244,7 @@
val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
- val _ = forall (FundefLib.forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs
+ val _ = forall (not o Term.exists_subterm (fn Free (n, _) => n mem fnames | _ => false)) gs
orelse error (input_error "Recursive Calls not allowed in premises")
in
fqgar
@@ -265,14 +261,23 @@
type fixes = ((string * typ) * mixfix) list
type 'a spec = ((bstring * Attrib.src list) * 'a list) list
-type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec -> (term list * (thm list -> thm spec))
+type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec
+ -> (term list * (thm list -> thm spec) * (thm list -> thm list list))
+
+val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
fun empty_preproc check _ _ ctxt fixes spec =
let
val (nas,tss) = split_list spec
val _ = check ctxt fixes (flat tss)
+ val ts = flat tss
+ val fnames = map (fst o fst) fixes
+ val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
+
+ fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
+ |> map (map snd)
in
- (flat tss, curry op ~~ nas o Library.unflat tss)
+ (ts, curry op ~~ nas o Library.unflat tss, sort)
end
structure Preprocessor = GenericDataFun
@@ -313,44 +318,11 @@
val flags_statements = statements_ow
>> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
-
- fun basic_apply_flags ((config, fixes), (flags, statements)) = ((config, fixes), statements)
in
fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements)
-
end
-
-
-
-val default_config = FundefConfig { sequential=false, default="%x. arbitrary",
- target=NONE, domintros=false, tailrec=false }
-
-
end
end
-(* Common Abbreviations *)
-
-structure FundefAbbrev =
-struct
-
-fun implies_elim_swp x y = implies_elim y x
-
-(* HOL abbreviations *)
-val boolT = HOLogic.boolT
-val mk_prod = HOLogic.mk_prod
-val mk_eq = HOLogic.mk_eq
-val eq_const = HOLogic.eq_const
-val Trueprop = HOLogic.mk_Trueprop
-val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
-
-fun free_to_var (Free (v,T)) = Var ((v,0),T)
- | free_to_var _ = raise Match
-
-fun var_to_free (Var ((v,_),T)) = Free (v,T)
- | var_to_free _ = raise Match
-
-
-end
--- a/src/HOL/Tools/function_package/fundef_core.ML Mon Jul 16 21:17:12 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML Mon Jul 16 21:22:43 2007 +0200
@@ -24,10 +24,11 @@
structure FundefCore : FUNDEF_CORE =
struct
+val boolT = HOLogic.boolT
+val mk_eq = HOLogic.mk_eq
open FundefLib
open FundefCommon
-open FundefAbbrev
datatype globals =
Globals of {
@@ -85,7 +86,7 @@
qglr : ((string * typ) list * term list * term * term),
cdata : clause_context,
- tree: ctx_tree,
+ tree: FundefCtxTree.ctx_tree,
lGI: thm,
RCs: rec_call_info list
}
@@ -125,8 +126,8 @@
let
val shift = incr_boundvars (length qs')
in
- (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
- $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
+ (implies $ HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs')
+ $ HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
|> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
|> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
|> curry abstract_over fvar
@@ -140,12 +141,12 @@
fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
let
fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
- Trueprop Pbool
- |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
+ HOLogic.mk_Trueprop Pbool
+ |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
|> fold_rev (curry Logic.mk_implies) gs
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
in
- Trueprop Pbool
+ HOLogic.mk_Trueprop Pbool
|> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
|> mk_forall_rename ("x", x)
|> mk_forall_rename ("P", Pbool)
@@ -168,7 +169,7 @@
val cqs = map (cterm_of thy) qs
val ags = map (assume o cterm_of thy) gs
- val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
+ val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
in
ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
cqs = cqs, ags = ags, case_hyp = case_hyp }
@@ -203,18 +204,18 @@
val lGI = GIntro_thm
|> forall_elim (cert f)
|> fold forall_elim cqs
- |> fold implies_elim_swp ags
+ |> fold (flip implies_elim) ags
fun mk_call_info (rcfix, rcassm, rcarg) RI =
let
val llRI = RI
|> fold forall_elim cqs
|> fold (forall_elim o cert o Free) rcfix
- |> fold implies_elim_swp ags
- |> fold implies_elim_swp rcassm
+ |> fold (flip implies_elim) ags
+ |> fold (flip implies_elim) rcassm
val h_assum =
- Trueprop (G $ rcarg $ (h $ rcarg))
+ HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|> fold_rev (mk_forall o Free) rcfix
|> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
@@ -263,16 +264,16 @@
val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
- val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
+ val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
in if j < i then
let
val compat = lookup_compat_thm j i cts
in
compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
|> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
- |> fold implies_elim_swp agsj
- |> fold implies_elim_swp agsi
- |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
+ |> fold (flip implies_elim) agsj
+ |> fold (flip implies_elim) agsi
+ |> flip implies_elim ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
end
else
let
@@ -280,9 +281,9 @@
in
compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
|> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
- |> fold implies_elim_swp agsi
- |> fold implies_elim_swp agsj
- |> implies_elim_swp (assume lhsi_eq_lhsj)
+ |> fold (flip implies_elim) agsi
+ |> fold (flip implies_elim) agsj
+ |> flip implies_elim (assume lhsi_eq_lhsj)
|> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
end
end
@@ -330,11 +331,11 @@
val RLj_import =
RLj |> fold forall_elim cqsj'
- |> fold implies_elim_swp agsj'
- |> fold implies_elim_swp Ghsj'
+ |> fold (flip implies_elim) agsj'
+ |> fold (flip implies_elim) Ghsj'
- val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
- val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
+ val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
+ val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
in
(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
|> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
@@ -364,7 +365,7 @@
val existence = fold (curry op COMP o prep_RC) RCs lGI
val P = cterm_of thy (mk_eq (y, rhsC))
- val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y)))
+ val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
@@ -372,8 +373,8 @@
|> forall_elim (cterm_of thy lhs)
|> forall_elim (cterm_of thy y)
|> forall_elim P
- |> implies_elim_swp G_lhs_y
- |> fold implies_elim_swp unique_clauses
+ |> flip implies_elim G_lhs_y
+ |> fold (flip implies_elim) unique_clauses
|> implies_intr (cprop_of G_lhs_y)
|> forall_intr (cterm_of thy y)
@@ -409,8 +410,8 @@
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
val ihyp = all domT $ Abs ("z", domT,
- implies $ Trueprop (R $ Bound 0 $ x)
- $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
+ implies $ HOLogic.mk_Trueprop (R $ Bound 0 $ x)
+ $ HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
|> cterm_of thy
@@ -430,7 +431,7 @@
|> forall_elim_vars 0
|> fold (curry op COMP) ex1s
|> implies_intr (ihyp)
- |> implies_intr (cterm_of thy (Trueprop (mk_acc domT R $ x)))
+ |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
|> forall_intr (cterm_of thy x)
|> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
|> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
@@ -453,11 +454,11 @@
fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
let
fun mk_h_assm (rcfix, rcassm, rcarg) =
- Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
+ HOLogic.mk_Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|> fold_rev (mk_forall o Free) rcfix
in
- Trueprop (Gvar $ lhs $ rhs)
+ HOLogic.mk_Trueprop (Gvar $ lhs $ rhs)
|> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
|> fold_rev (curry Logic.mk_implies) gs
|> fold_rev mk_forall (fvar :: qs)
@@ -494,7 +495,7 @@
val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
- Trueprop (Rvar $ rcarg $ lhs)
+ HOLogic.mk_Trueprop (Rvar $ rcarg $ lhs)
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|> fold_rev (curry Logic.mk_implies) gs
|> fold_rev (mk_forall o Free) rcfix
@@ -551,8 +552,8 @@
fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
let
- val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
- val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
+ val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+ val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
in
((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
|> (fn it => it COMP graph_is_function)
@@ -580,23 +581,23 @@
val Globals {domT, x, z, a, P, D, ...} = globals
val acc_R = mk_acc domT R
- val x_D = assume (cterm_of thy (Trueprop (D $ x)))
- val a_D = cterm_of thy (Trueprop (D $ a))
+ val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
+ val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
- val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
+ val D_subset = cterm_of thy (mk_forall x (implies $ HOLogic.mk_Trueprop (D $ x) $ HOLogic.mk_Trueprop (acc_R $ x)))
val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
mk_forall x
- (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
- Logic.mk_implies (Trueprop (R $ z $ x),
- Trueprop (D $ z)))))
+ (mk_forall z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
+ Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
+ HOLogic.mk_Trueprop (D $ z)))))
|> cterm_of thy
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
val ihyp = all domT $ Abs ("z", domT,
- implies $ Trueprop (R $ Bound 0 $ x)
- $ Trueprop (P $ Bound 0))
+ implies $ HOLogic.mk_Trueprop (R $ Bound 0 $ x)
+ $ HOLogic.mk_Trueprop (P $ Bound 0))
|> cterm_of thy
val aihyp = assume ihyp
@@ -612,26 +613,26 @@
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
sih |> forall_elim (cterm_of thy rcarg)
- |> implies_elim_swp llRI
+ |> flip implies_elim llRI
|> fold_rev (implies_intr o cprop_of) CCas
|> fold_rev (forall_intr o cterm_of thy o Free) RIvs
val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
- val step = Trueprop (P $ lhs)
+ val step = HOLogic.mk_Trueprop (P $ lhs)
|> fold_rev (curry Logic.mk_implies o prop_of) P_recs
|> fold_rev (curry Logic.mk_implies) gs
- |> curry Logic.mk_implies (Trueprop (D $ lhs))
+ |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|> cterm_of thy
val P_lhs = assume step
|> fold forall_elim cqs
- |> implies_elim_swp lhs_D
- |> fold implies_elim_swp ags
- |> fold implies_elim_swp P_recs
+ |> flip implies_elim lhs_D
+ |> fold (flip implies_elim) ags
+ |> fold (flip implies_elim) P_recs
- val res = cterm_of thy (Trueprop (P $ x))
+ val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
|> Simplifier.rewrite replace_x_ss
|> symmetric (* P lhs == P x *)
|> (fn eql => equal_elim eql P_lhs) (* "P x" *)
@@ -687,7 +688,7 @@
let
val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
qglr = (oqs, _, _, _), ...} = clause
- val goal = Trueprop (mk_acc domT R $ lhs)
+ val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
|> fold_rev (curry Logic.mk_implies) gs
|> cterm_of thy
in
@@ -719,7 +720,7 @@
let
val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
- val hyp = Trueprop (R' $ arg $ lhs)
+ val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
|> fold_rev (curry Logic.mk_implies o prop_of) used
|> FundefCtxTree.export_term (fixes, map prop_of assumes)
|> fold_rev (curry Logic.mk_implies o prop_of) ags
@@ -728,13 +729,13 @@
val thm = assume hyp
|> fold forall_elim cqs
- |> fold implies_elim_swp ags
+ |> fold (flip implies_elim) ags
|> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *)
- |> fold implies_elim_swp used
+ |> fold (flip implies_elim) used
val acc = thm COMP ih_case
- val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
+ val z_eq_arg = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (z, arg)))
val arg_eq_z = (assume z_eq_arg) RS sym
@@ -742,8 +743,8 @@
|> implies_intr (cprop_of case_hyp)
|> implies_intr z_eq_arg
- val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
- val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
+ val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
+ val x_eq_lhs = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
|> FundefCtxTree.export_thm thy (fixes,
@@ -767,20 +768,20 @@
val R' = Free ("R", fastype_of R)
- val Rrel = Free ("R", mk_relT (domT, domT))
- val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
+ val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
+ val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
- val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
+ val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const ("Wellfounded_Recursion.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
val ihyp = all domT $ Abs ("z", domT,
- implies $ Trueprop (R' $ Bound 0 $ x)
- $ Trueprop (acc_R $ Bound 0))
+ implies $ HOLogic.mk_Trueprop (R' $ Bound 0 $ x)
+ $ HOLogic.mk_Trueprop (acc_R $ Bound 0))
|> cterm_of thy
val ihyp_a = assume ihyp |> forall_elim_vars 0
- val R_z_x = cterm_of thy (Trueprop (R $ z $ x))
+ val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
in
@@ -842,14 +843,15 @@
val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
+ fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
in
Goal.prove ctxt [] [] trsimp
(fn _ =>
rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
THEN (rtac (forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
- THEN (SIMPSET (fn ss => asm_full_simp_tac (ss addsimps [default_thm]) 1))
+ THEN (SIMPSET' simp_default_tac 1)
THEN (etac not_acc_down 1)
- THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps [default_thm])))) 1)
+ THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' simp_default_tac)) 1)
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
in
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jul 16 21:17:12 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jul 16 21:22:43 2007 +0200
@@ -249,13 +249,21 @@
|> tap (check_defs ctxt fixes) (* Standard checks *)
|> tap (map (check_pats ctxt)) (* More checks for sequential mode *)
|> curry op ~~ flags'
- |> add_catchall fixes (* Completion: still disabled *)
+ |> add_catchall fixes (* Completion *)
|> FundefSplit.split_some_equations ctxt
fun restore_spec thms =
nas ~~ Library.take (length nas, Library.unflat spliteqs thms)
+
+ val spliteqs' = flat (Library.take (length nas, spliteqs))
+ val fnames = map (fst o fst) fixes
+ val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
+
+ fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
+ |> map (map snd)
+
in
- (flat spliteqs, restore_spec)
+ (flat spliteqs, restore_spec, sort)
end
else
FundefCommon.empty_preproc check_defs config flags ctxt fixes spec
--- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Jul 16 21:17:12 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Jul 16 21:22:43 2007 +0200
@@ -73,8 +73,6 @@
(ctx, [], t)
-fun implies_elim_swp a b = implies_elim b a
-
fun map3 _ [] [] [] = []
| map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
| map3 _ _ _ _ = raise Library.UnequalLengths;
--- a/src/HOL/Tools/function_package/fundef_package.ML Mon Jul 16 21:17:12 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Jul 16 21:22:43 2007 +0200
@@ -44,20 +44,20 @@
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
-fun add_simps fixes post sort label moreatts simps lthy =
+fun add_simps fnames post sort label moreatts simps lthy =
let
- val fnames = map (fst o fst) fixes
+ val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
+ val spec = post simps
+ |> map (apfst (apsnd (append atts)))
val (saved_spec_simps, lthy) =
- fold_map note_theorem (post simps) lthy
+ fold_map note_theorem spec lthy
+
val saved_simps = flat (map snd saved_spec_simps)
-
val simps_by_f = sort saved_simps
fun add_for_f fname simps =
- note_theorem
- ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts),
- simps) #> snd
+ note_theorem ((NameSpace.qualified fname label, []), simps) #> snd
in
(saved_simps,
fold2 add_for_f fnames simps_by_f lthy)
@@ -68,8 +68,9 @@
val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} =
cont (Goal.close_result proof)
+ val fnames = map (fst o fst) fixes
val qualify = NameSpace.qualified defname
- val addsmps = add_simps fixes post sort_cont
+ val addsmps = add_simps fnames post sort_cont
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
@@ -107,11 +108,11 @@
fun gen_add_fundef prep fixspec eqnss config flags lthy =
let
val ((fixes, spec), ctxt') = prepare_spec prep fixspec eqnss lthy
- val (eqs, post) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
+ val (eqs, post, sort_cont) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
val defname = mk_defname fixes
- val ((goalstate, cont, sort_cont), lthy) =
+ val ((goalstate, cont), lthy) =
FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy
val afterqed = fundef_afterqed config fixes post defname cont sort_cont
@@ -190,6 +191,7 @@
DatatypeHooks.add case_cong_hook
#> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
+
(* ad-hoc method to convert elimination-style goals to existential statements *)
fun insert_int_goal thy subg st =
--- a/src/HOL/Tools/function_package/mutual.ML Mon Jul 16 21:17:12 2007 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML Mon Jul 16 21:22:43 2007 +0200
@@ -16,7 +16,6 @@
-> local_theory
-> ((thm (* goalstate *)
* (thm -> FundefCommon.fundef_result) (* proof continuation *)
- * (thm list -> thm list list) (* sorting continuation *)
) * local_theory)
end
@@ -332,19 +331,6 @@
trsimps=mtrsimps}
end
-(* puts an object in the "right bucket" *)
-fun store_grouped P x [] = []
- | store_grouped P x ((l, xs)::bs) =
- if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs)
-
-fun sort_by_function (Mutual {fqgars, ...}) names xs =
- fold_rev (store_grouped (op = o apfst fst)) (* fill *)
- (map name_of_fqgar (Library.take (length xs, fqgars)) ~~ xs) (* the name-thm pairs *)
- (map (rpair []) names) (* in the empty buckets labeled with names *)
-
- |> map (snd #> map snd) (* and remove the labels afterwards *)
-
-
fun prepare_fundef_mutual config defname fixes eqss lthy =
let
val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
@@ -356,9 +342,8 @@
val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
- val sort_cont = sort_by_function mutual' (map (fst o fst) fixes)
in
- ((goalstate, mutual_cont, sort_cont), lthy'')
+ ((goalstate, mutual_cont), lthy'')
end