--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Tue Aug 24 08:22:17 2010 +0200
@@ -348,6 +348,9 @@
code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
i => o => i => bool as suffix, i => i => i => bool) append .
+code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as "concat", o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as "slice", o \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool as prefix,
+ i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append .
+
code_pred [dseq] append .
code_pred [random_dseq] append .
@@ -409,6 +412,10 @@
code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
i * o * i => bool, i * i * i => bool) tupled_append .
+
+code_pred (expected_modes: i \<times> i \<times> o \<Rightarrow> bool, o \<times> o \<times> i \<Rightarrow> bool, o \<times> i \<times> i \<Rightarrow> bool,
+ i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append .
+
code_pred [random_dseq] tupled_append .
thm tupled_append.equation
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Aug 24 08:22:17 2010 +0200
@@ -200,10 +200,10 @@
(Args.$$$ "i" >> K Input || Args.$$$ "o" >> K Output ||
Args.$$$ "bool" >> K Bool || Args.$$$ "(" |-- parse_mode_expr --| Args.$$$ ")") xs
and parse_mode_tuple_expr xs =
- (parse_mode_basic_expr --| Args.$$$ "*" -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr)
+ (parse_mode_basic_expr --| (Args.$$$ "*" || Args.$$$ "\<times>") -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr)
xs
and parse_mode_expr xs =
- (parse_mode_tuple_expr --| Args.$$$ "=>" -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
+ (parse_mode_tuple_expr --| (Args.$$$ "=>" || Args.$$$ "\<Rightarrow>") -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
val mode_and_opt_proposal = parse_mode_expr --
Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
--- a/src/HOL/Tools/inductive.ML Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Tue Aug 24 08:22:17 2010 +0200
@@ -195,6 +195,21 @@
+(** equations **)
+
+structure Equation_Data = Generic_Data
+(
+ type T = thm Item_Net.T;
+ val empty = Item_Net.init (op aconv o pairself Thm.prop_of)
+ (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);
+ val extend = I;
+ val merge = Item_Net.merge;
+);
+
+val add_equation = Thm.declaration_attribute (Equation_Data.map o Item_Net.update)
+
+
+
(** misc utilities **)
fun message quiet_mode s = if quiet_mode then () else writeln s;
@@ -548,16 +563,20 @@
fun mk_simp_eq ctxt prop =
let
+ val thy = ProofContext.theory_of ctxt
val ctxt' = Variable.auto_fixes prop ctxt
- val cname = fst (dest_Const (fst (strip_comb (HOLogic.dest_Trueprop prop))))
- val info = the_inductive ctxt cname
- val eq = nth (#eqs (snd info)) (find_index (fn c => c = cname) (#names (fst info)))
- val lhs_eq = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of eq)))
- val subst = Pattern.match (ProofContext.theory_of ctxt) (lhs_eq, HOLogic.dest_Trueprop prop)
- (Vartab.empty, Vartab.empty)
- val certify = cterm_of (ProofContext.theory_of ctxt)
- val inst = map (fn v => (certify (Var v), certify (Envir.subst_term subst (Var v))))
- (Term.add_vars lhs_eq [])
+ val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
+ val substs = Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop)
+ |> map_filter
+ (fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop)
+ (Vartab.empty, Vartab.empty), eq)
+ handle Pattern.MATCH => NONE)
+ val (subst, eq) = case substs of
+ [s] => s
+ | _ => error
+ ("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique")
+ val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
+ (Term.add_vars (lhs_of eq) [])
in
cterm_instantiate inst eq
|> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
@@ -833,7 +852,8 @@
val (eqs', lthy3) = lthy2 |>
fold_map (fn (name, eq) => Local_Theory.note
- ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), []), [eq])
+ ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"),
+ [Attrib.internal (K add_equation)]), [eq])
#> apfst (hd o snd))
(if null eqs then [] else (cnames ~~ eqs))
val (inducts, lthy4) =
--- a/src/HOL/Tools/inductive_set.ML Mon Aug 23 19:35:57 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Tue Aug 24 08:22:17 2010 +0200
@@ -477,7 +477,7 @@
eta_contract (member op = cs' orf is_pred pred_arities))) intros;
val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
val monos' = map (to_pred [] (Context.Proof lthy)) monos;
- val ({preds, intrs, elims, raw_induct, ...}, lthy1) =
+ val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) =
Inductive.add_ind_def
{quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
coind = coind, no_elim = no_elim, no_ind = no_ind,
@@ -520,14 +520,13 @@
val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn; (* FIXME *)
val (intr_names, intr_atts) = split_list (map fst intros);
val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
- val eqs = [] (* TODO: define equations *)
val (intrs', elims', eqs', induct, inducts, lthy4) =
Inductive.declare_rules rec_name coind no_ind cnames (map fst defs)
(map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
(map (fn th => (to_set [] (Context.Proof lthy3) th,
map fst (fst (Rule_Cases.get th)),
Rule_Cases.get_constraints th)) elims)
- eqs raw_induct' lthy3;
+ (map (to_set [] (Context.Proof lthy3)) eqs) raw_induct' lthy3;
in
({intrs = intrs', elims = elims', induct = induct, inducts = inducts,
raw_induct = raw_induct', preds = map fst defs, eqs = eqs'},