# HG changeset patch # User blanchet # Date 1392640302 -3600 # Node ID 10194808430d100bd945dea4b4296dd53f19c935 # Parent b18bdcbda41b8f5de7396ce7d63c9f205244e74f name derivations in 'primrec' for code extraction from proof terms diff -r b18bdcbda41b -r 10194808430d src/HOL/Proofs/Extraction/Pigeonhole.thy --- a/src/HOL/Proofs/Extraction/Pigeonhole.thy Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy Mon Feb 17 13:31:42 2014 +0100 @@ -253,4 +253,3 @@ ML_val "timeit @{code test''}" end - diff -r b18bdcbda41b -r 10194808430d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 17 13:31:42 2014 +0100 @@ -1346,9 +1346,9 @@ in (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar), lthy - |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) map_thms) - |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) rel_eq_thms) - |> Spec_Rules.add Spec_Rules.Equational (`(lhs_heads_of o hd) set_thms) + |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms) + |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms) + |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set_thms) |> Local_Theory.notes (anonymous_notes @ notes) |> snd) end; diff -r b18bdcbda41b -r 10194808430d src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Feb 17 13:31:42 2014 +0100 @@ -466,13 +466,13 @@ map_idents) THEN HEADGOAL (rtac refl); -fun prepare_primrec fixes specs lthy = +fun prepare_primrec fixes specs lthy0 = let - val thy = Proof_Context.theory_of lthy; + val thy = Proof_Context.theory_of lthy0; val (bs, mxs) = map_split (apfst fst) fixes; val fun_names = map Binding.name_of bs; - val eqns_data = map (dissect_eqn lthy fun_names) specs; + val eqns_data = map (dissect_eqn lthy0 fun_names) specs; val funs_data = eqns_data |> partition_eq ((op =) o pairself #fun_name) |> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst @@ -488,7 +488,7 @@ |> map (maps (map_filter (find_rec_calls has_call))); fun is_only_old_datatype (Type (s, _)) = - is_none (fp_sugar_of lthy s) andalso is_some (Datatype_Data.get_info thy s) + is_none (fp_sugar_of lthy0 s) andalso is_some (Datatype_Data.get_info thy s) | is_only_old_datatype _ = false; val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else (); @@ -496,35 +496,41 @@ [] => () | (b, _) :: _ => primrec_error ("type of " ^ Binding.print b ^ " contains top sort")); - val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy') = - rec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy; + val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy) = + rec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy0; val actual_nn = length funs_data; val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse - primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy' ctr) ^ + primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^ " is not a constructor in left-hand side") user_eqn) eqns_data end; - val defs = build_defs lthy' bs mxs funs_data rec_specs has_call; + val defs = build_defs lthy bs mxs funs_data rec_specs has_call; - fun prove lthy def_thms' ({ctr_specs, nested_map_idents, nested_map_comps, ...} : rec_spec) + fun prove lthy' def_thms' ({ctr_specs, nested_map_idents, nested_map_comps, ...} : rec_spec) (fun_data : eqn_data list) = let + val js = + find_indices (op = o pairself (fn {fun_name, ctr, ...} => (fun_name, ctr))) + fun_data eqns_data; + val def_thms = map (snd o snd) def_thms'; - val simp_thmss = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs + val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs |> fst |> map_filter (try (fn (x, [y]) => - (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y))) - |> map (fn (user_eqn, num_extra_args, rec_thm) => - mk_primrec_tac lthy num_extra_args nested_map_idents nested_map_comps def_thms rec_thm - |> K |> Goal.prove_sorry lthy [] [] user_eqn - |> Thm.close_derivation); - val poss = - find_indices (op = o pairself (fn {fun_name, ctr, ...} => (fun_name, ctr))) - fun_data eqns_data; + (#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y))) + |> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) => + mk_primrec_tac lthy' num_extra_args nested_map_idents nested_map_comps def_thms rec_thm + |> K |> Goal.prove_sorry lthy' [] [] user_eqn + (* for code extraction from proof terms: *) + |> singleton (Proof_Context.export lthy' lthy) + |> Thm.name_derivation (Sign.full_name thy (Binding.name fun_name) ^ + Long_Name.separator ^ simpsN ^ + (if js = [0] then "" else "_" ^ string_of_int (j + 1)))) + js; in - (poss, simp_thmss) + (js, simp_thms) end; val notes = @@ -546,7 +552,7 @@ (((fun_names, defs), fn lthy => fn defs => split_list (map2 (prove lthy defs) (take actual_nn rec_specs) funs_data)), - lthy' |> Local_Theory.notes (notes @ common_notes) |> snd) + lthy |> Local_Theory.notes (notes @ common_notes) |> snd) end; fun add_primrec_simple fixes ts lthy = @@ -574,9 +580,9 @@ val (fixes, specs) = fst (prep_spec raw_fixes raw_spec lthy); val mk_notes = - flat ooo map3 (fn poss => fn prefix => fn thms => + flat ooo map3 (fn js => fn prefix => fn thms => let - val (bs, attrss) = map_split (fst o nth specs) poss; + val (bs, attrss) = map_split (fst o nth specs) js; val notes = map3 (fn b => fn attrs => fn thm => ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs), @@ -588,9 +594,9 @@ in lthy |> add_primrec_simple fixes (map snd specs) - |-> (fn (names, (ts, (posss, simpss))) => + |-> (fn (names, (ts, (jss, simpss))) => Spec_Rules.add Spec_Rules.Equational (ts, flat simpss) - #> Local_Theory.notes (mk_notes posss names simpss) + #> Local_Theory.notes (mk_notes jss names simpss) #>> pair ts o map snd) end handle OLD_PRIMREC () => old_primrec raw_fixes raw_spec lthy |>> apsnd single; @@ -598,19 +604,15 @@ val add_primrec = gen_primrec Primrec.add_primrec Specification.check_spec; val add_primrec_cmd = gen_primrec Primrec.add_primrec_cmd Specification.read_spec; -fun add_primrec_global fixes specs thy = - let - val lthy = Named_Target.theory_init thy; - val ((ts, simpss), lthy') = add_primrec fixes specs lthy; - val simpss' = burrow (Proof_Context.export lthy' lthy) simpss; - in ((ts, simpss'), Local_Theory.exit_global lthy') end; +fun add_primrec_global fixes specs = + Named_Target.theory_init + #> add_primrec fixes specs + ##> Local_Theory.exit_global; -fun add_primrec_overloaded ops fixes specs thy = - let - val lthy = Overloading.overloading ops thy; - val ((ts, simpss), lthy') = add_primrec fixes specs lthy; - val simpss' = burrow (Proof_Context.export lthy' lthy) simpss; - in ((ts, simpss'), Local_Theory.exit_global lthy') end; +fun add_primrec_overloaded ops fixes specs = + Overloading.overloading ops + #> add_primrec fixes specs + ##> Local_Theory.exit_global; val _ = Outer_Syntax.local_theory @{command_spec "primrec"} "define primitive recursive functions" diff -r b18bdcbda41b -r 10194808430d src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Feb 17 13:31:42 2014 +0100 @@ -942,7 +942,7 @@ lthy |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms) |> fold (Spec_Rules.add Spec_Rules.Equational) - (AList.group (eq_list (op aconv)) (map (`lhs_heads_of) all_sel_thms)) + (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms)) |> fold (Spec_Rules.add Spec_Rules.Equational) (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss)) |> Local_Theory.declaration {syntax = false, pervasive = true} diff -r b18bdcbda41b -r 10194808430d src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Mon Feb 17 13:31:42 2014 +0100 @@ -40,7 +40,7 @@ val typ_subst_nonatomic: (typ * typ) list -> typ -> typ val subst_nonatomic_types: (typ * typ) list -> term -> term - val lhs_heads_of : thm -> term list + val lhs_head_of : thm -> term val mk_predT: typ list -> typ val mk_pred1T: typ -> typ @@ -182,8 +182,7 @@ fun subst_nonatomic_types [] = I | subst_nonatomic_types inst = map_types (typ_subst_nonatomic inst); -fun lhs_heads_of thm = - [Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))))]; +fun lhs_head_of thm = Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)))); fun mk_predT Ts = Ts ---> HOLogic.boolT; fun mk_pred1T T = mk_predT [T];