# HG changeset patch # User bulwahn # Date 1282630937 -7200 # Node ID 12096ea0cc1cbed094d14155afc94be4fe21a9a5 # Parent e92223c886f8b7f91510ea7097b266e80490cec8# Parent d5d342611edb1723e36625e37971bb16ed72db54 merged diff -r d5d342611edb -r 12096ea0cc1c src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy --- 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 \ 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 [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 \ i \ o \ bool, o \ o \ i \ bool, o \ i \ i \ bool, + i \ o \ i \ bool, i \ i \ i \ bool) tupled_append . + code_pred [random_dseq] tupled_append . thm tupled_append.equation diff -r d5d342611edb -r 12096ea0cc1c src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- 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.$$$ "\") -- 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.$$$ "\") -- 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 diff -r d5d342611edb -r 12096ea0cc1c src/HOL/Tools/inductive.ML --- 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) = diff -r d5d342611edb -r 12096ea0cc1c src/HOL/Tools/inductive_set.ML --- 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'},