# HG changeset patch # User wenzelm # Date 1346359092 -7200 # Node ID 8e124393c281488312e617bb9da820a59aac6b30 # Parent b77e1910af8ac60304a5e5331c95a00cdb3015e1# Parent 1266b51f9bbc77e51dd7b65bae5e661b28359c62 merged; diff -r 1266b51f9bbc -r 8e124393c281 etc/isar-keywords.el --- a/etc/isar-keywords.el Thu Aug 30 21:50:49 2012 +0200 +++ b/etc/isar-keywords.el Thu Aug 30 22:38:12 2012 +0200 @@ -35,7 +35,7 @@ "bnf_codata" "bnf_data" "bnf_def" - "bnf_of_typ" + "bnf_sugar" "boogie_end" "boogie_open" "boogie_status" @@ -471,7 +471,6 @@ "axioms" "bnf_codata" "bnf_data" - "bnf_of_typ" "boogie_end" "boogie_open" "bundle" @@ -578,6 +577,7 @@ (defconst isar-keywords-theory-goal '("ax_specification" "bnf_def" + "bnf_sugar" "boogie_vc" "code_pred" "corollary" diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Codatatype/BNF_Comp.thy --- a/src/HOL/Codatatype/BNF_Comp.thy Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Comp.thy Thu Aug 30 22:38:12 2012 +0200 @@ -9,8 +9,6 @@ theory BNF_Comp imports Basic_BNFs -keywords - "bnf_of_typ" :: thy_decl uses "Tools/bnf_comp_tactics.ML" "Tools/bnf_comp.ML" diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Codatatype/Codatatype.thy --- a/src/HOL/Codatatype/Codatatype.thy Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Codatatype/Codatatype.thy Thu Aug 30 22:38:12 2012 +0200 @@ -1,5 +1,7 @@ (* Title: HOL/Codatatype/Codatatype.thy Author: Dmitriy Traytel, TU Muenchen + Author: Andrei Popescu, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen Copyright 2012 The (co)datatype package. @@ -9,6 +11,11 @@ theory Codatatype imports BNF_LFP BNF_GFP +keywords + "bnf_sugar" :: thy_goal +uses + "Tools/bnf_sugar_tactics.ML" + "Tools/bnf_sugar.ML" begin end diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Codatatype/Tools/bnf_comp.ML --- a/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Thu Aug 30 22:38:12 2012 +0200 @@ -15,16 +15,15 @@ val rel_unfolds_of: unfold_thms -> thm list val pred_unfolds_of: unfold_thms -> thm list - val default_comp_sort: (string * sort) list list -> (string * sort) list val bnf_of_typ: BNF_Def.const_policy -> binding -> (binding -> binding) -> ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context -> (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context) - val bnf_of_typ_cmd: binding * string -> Proof.context -> Proof.context - val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context -> - BNF_Def.BNF * local_theory + val default_comp_sort: (string * sort) list list -> (string * sort) list val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context -> (int list list * ''a list) * (BNF_Def.BNF list * (unfold_thms * Proof.context)) + val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context -> + BNF_Def.BNF * local_theory end; structure BNF_Comp : BNF_COMP = @@ -69,7 +68,6 @@ val bdTN = "bdT"; -val compN = "comp_" fun mk_killN n = "kill" ^ string_of_int n ^ "_"; fun mk_liftN n = "lift" ^ string_of_int n ^ "_"; fun mk_permuteN src dest = @@ -262,7 +260,7 @@ (maps wit_thms_of_bnf inners); val (bnf', lthy') = - add_bnf const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) + bnf_def const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) ((((b, comp_map), comp_sets), comp_bd), comp_wits) lthy; val outer_rel_Gr = rel_Gr_of_bnf outer RS sym; @@ -288,18 +286,6 @@ (bnf', (unfold', lthy')) end; -fun clean_compose_bnf_cmd (outer, inners) lthy = - let - val outer = the (bnf_of lthy outer) - val inners = map (the o bnf_of lthy) inners - val b = name_of_bnf outer - |> Binding.prefix_name compN - |> Binding.suffix_name ("_" ^ implode (map (Binding.name_of o name_of_bnf) inners)); - in - (snd o snd) (clean_compose_bnf Dont_Inline I b outer inners - (empty_unfold, lthy)) - end; - (* Killing live variables *) fun killN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else @@ -381,7 +367,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) + bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) ((((b, killN_map), killN_sets), Term.absdummy T killN_bd), killN_wits) lthy; val rel_Gr = rel_Gr_of_bnf bnf RS sym; @@ -406,9 +392,6 @@ (bnf', (unfold', lthy')) end; -fun killN_bnf_cmd (n, raw_bnf) lthy = - (snd o snd) (killN_bnf I n (the (bnf_of lthy raw_bnf)) (empty_unfold, lthy)); - (* Adding dummy live variables *) fun liftN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else @@ -489,7 +472,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) + bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) ((((b, liftN_map), liftN_sets), Term.absdummy T liftN_bd), liftN_wits) lthy; val liftN_rel_unfold_thm = @@ -505,9 +488,6 @@ (bnf', (unfold', lthy')) end; -fun liftN_bnf_cmd (n, raw_bnf) lthy = - (snd o snd) (liftN_bnf I n (the (bnf_of lthy raw_bnf)) (empty_unfold, lthy)); - (* Changing the order of live variables *) fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else @@ -580,7 +560,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - add_bnf Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) + bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds) ((((b, permute_map), permute_sets), Term.absdummy T permute_bd), permute_wits) lthy; val permute_rel_unfold_thm = @@ -596,9 +576,67 @@ (bnf', (unfold', lthy')) end; -fun permute_bnf_cmd ((src, dest), raw_bnf) lthy = - (snd o snd) (permute_bnf I src dest (the (bnf_of lthy raw_bnf)) - (empty_unfold, lthy)); +(* Composition pipeline *) + +fun permute_and_kill qualify n src dest bnf = + bnf + |> permute_bnf qualify src dest + #> uncurry (killN_bnf qualify n); + +fun lift_and_permute qualify n src dest bnf = + bnf + |> liftN_bnf qualify n + #> uncurry (permute_bnf qualify src dest); + +fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy = + let + val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; + val kill_poss = map (find_indices Ds) Ass; + val live_poss = map2 (subtract (op =)) kill_poss before_kill_src; + val before_kill_dest = map2 append kill_poss live_poss; + val kill_ns = map length kill_poss; + val (inners', (unfold', lthy')) = + fold_map5 (fn i => permute_and_kill (qualify i)) + (if length bnfs = 1 then [0] else (1 upto length bnfs)) + kill_ns before_kill_src before_kill_dest bnfs (unfold, lthy); + + val Ass' = map2 (map o nth) Ass live_poss; + val As = sort Ass'; + val after_lift_dest = replicate (length Ass') (0 upto (length As - 1)); + val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass'; + val new_poss = map2 (subtract (op =)) old_poss after_lift_dest; + val after_lift_src = map2 append new_poss old_poss; + val lift_ns = map (fn xs => length As - length xs) Ass'; + in + ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i)) + (if length bnfs = 1 then [0] else (1 upto length bnfs)) + lift_ns after_lift_src after_lift_dest inners' (unfold', lthy')) + end; + +fun default_comp_sort Ass = + Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); + +fun compose_bnf const_policy qualify' b sort outer inners oDs Dss tfreess (unfold, lthy) = + let + val name = Binding.name_of b; + fun qualify i bind = + let val namei = if i > 0 then name ^ string_of_int i else name; + in + if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind + else qualify' (Binding.prefix_name namei bind) + end; + + val Ass = map (map dest_TFree) tfreess; + val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; + + val ((kill_poss, As), (inners', (unfold', lthy'))) = + normalize_bnfs qualify Ass Ds sort inners unfold lthy; + + val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss); + val As = map TFree As; + in + apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy')) + end; (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) @@ -677,7 +715,7 @@ fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf)); - val (bnf', lthy') = add_bnf Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE + val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac NONE ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy; val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf'); @@ -687,8 +725,7 @@ val rel_unfold = Local_Defs.unfold lthy' (map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_def; - val unfold_defs'' = - unfold_defs' o (Local_Defs.unfold lthy' (filter_refl [rel_def_of_bnf bnf'])); + val unfold_defs'' = unfold_defs' o Local_Defs.unfold lthy' (filter_refl [rel_def_of_bnf bnf']); val pred_def = unfold_defs'' (pred_def_of_bnf bnf' RS abs_pred_sym_pred_abs); val pred_unfold = Local_Defs.unfold lthy' @@ -703,74 +740,6 @@ |> note pred_unfoldN [pred_unfold]) end; -(* Composition pipeline *) - -fun permute_and_kill qualify n src dest bnf = - bnf - |> permute_bnf qualify src dest - #> uncurry (killN_bnf qualify n); - -fun lift_and_permute qualify n src dest bnf = - bnf - |> liftN_bnf qualify n - #> uncurry (permute_bnf qualify src dest); - -fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy = - let - val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; - val kill_poss = map (find_indices Ds) Ass; - val live_poss = map2 (subtract (op =)) kill_poss before_kill_src; - val before_kill_dest = map2 append kill_poss live_poss; - val kill_ns = map length kill_poss; - val (inners', (unfold', lthy')) = - fold_map5 (fn i => permute_and_kill (qualify i)) - (if length bnfs = 1 then [0] else (1 upto length bnfs)) - kill_ns before_kill_src before_kill_dest bnfs (unfold, lthy); - - val Ass' = map2 (map o nth) Ass live_poss; - val As = sort Ass'; - val after_lift_dest = replicate (length Ass') (0 upto (length As - 1)); - val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass'; - val new_poss = map2 (subtract (op =)) old_poss after_lift_dest; - val after_lift_src = map2 append new_poss old_poss; - val lift_ns = map (fn xs => length As - length xs) Ass'; - in - ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i)) - (if length bnfs = 1 then [0] else (1 upto length bnfs)) - lift_ns after_lift_src after_lift_dest inners' (unfold', lthy')) - end; - -fun default_comp_sort Ass = - Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); - -fun compose_bnf const_policy qualify' b sort outer inners oDs Dss tfreess (unfold, lthy) = - let - val name = Binding.name_of b; - fun qualify i bind = - let val namei = if i > 0 then name ^ string_of_int i else name; - in - if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind - else qualify' (Binding.prefix_name namei bind) - end; - - val Ass = map (map dest_TFree) tfreess; - val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; - - val ((kill_poss, As), (inners', (unfold', lthy'))) = - normalize_bnfs qualify Ass Ds sort inners unfold lthy; - - val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss); - val As = map TFree As; - in - apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy')) - end; - -fun compose_bnf_cmd (((((b, outer), inners), oDs), Dss), Ass) lthy = (snd o snd) - (compose_bnf Dont_Inline I b default_comp_sort (the (bnf_of lthy outer)) - (map (the o bnf_of lthy) inners) - (map (Syntax.read_typ lthy) oDs) (map (map (Syntax.read_typ lthy)) Dss) - (map (map (Syntax.read_typ lthy)) Ass) (empty_unfold, lthy)); - fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) = ((Basic_BNFs.ID_bnf, ([], [T])), (add_to_unfold_opt NONE NONE (SOME Basic_BNFs.ID_rel_def) (SOME Basic_BNFs.ID_pred_def) unfold, lthy)) @@ -823,12 +792,4 @@ end end; -fun bnf_of_typ_cmd (b, rawT) lthy = (snd o snd) - (bnf_of_typ Dont_Inline b I default_comp_sort (Syntax.read_typ lthy rawT) - (empty_unfold, lthy)); - -val _ = - Outer_Syntax.local_theory @{command_spec "bnf_of_typ"} "parse a type as composition of BNFs" - (((Parse.binding --| Parse.$$$ "=") -- Parse.typ) >> bnf_of_typ_cmd); - end; diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Codatatype/Tools/bnf_def.ML --- a/src/HOL/Codatatype/Tools/bnf_def.ML Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML Thu Aug 30 22:38:12 2012 +0200 @@ -81,14 +81,14 @@ val user_policy: Proof.context -> fact_policy val print_bnfs: Proof.context -> unit - val add_bnf: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> + val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> ({prems: thm list, context: Proof.context} -> tactic) list -> ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> (((binding * term) * term list) * term) * term list -> local_theory -> BNF * local_theory val filter_refl: thm list -> thm list - val add_bnf_cmd: (((binding * string) * string list) * string) * string list -> local_theory -> + val bnf_def_cmd: (((binding * string) * string list) * string) * string list -> local_theory -> Proof.state end; @@ -507,8 +507,7 @@ val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false); fun user_policy ctxt = - if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms - else Derive_All_Facts_Note_Most; + if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else Derive_All_Facts_Note_Most; val smart_max_inline_size = 25; (*FUDGE*) @@ -529,7 +528,7 @@ (* Define new BNFs *) -fun prepare_bnf const_policy mk_fact_policy qualify prep_term Ds_opt +fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt ((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits) no_defs_lthy = let val fact_policy = mk_fact_policy no_defs_lthy; @@ -557,10 +556,10 @@ else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_witN i) b) (1 upto nwits); in map2 pair bs wit_rhss end; - fun maybe_define needed_for_fp (b, rhs) lthy = + fun maybe_define needed_for_extra_facts (b, rhs) lthy = let val inline = - (not needed_for_fp orelse fact_policy = Derive_Some_Facts) andalso + (not needed_for_extra_facts orelse fact_policy = Derive_Some_Facts) andalso (case const_policy of Dont_Inline => false | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs @@ -709,8 +708,7 @@ val goal_map_id = let - val bnf_map_app_id = Term.list_comb - (bnf_map_AsAs, map HOLogic.id_const As'); + val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As'); in HOLogic.mk_Trueprop (HOLogic.mk_eq (bnf_map_app_id, HOLogic.id_const CA')) @@ -718,8 +716,7 @@ val goal_map_comp = let - val bnf_map_app_comp = Term.list_comb - (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs); + val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs); val comp_bnf_map_app = HOLogic.mk_comp (Term.list_comb (bnf_map_BsCs, gs), Term.list_comb (bnf_map_AsBs, fs)); @@ -1156,7 +1153,7 @@ (goals, wit_goalss, after_qed, lthy', one_step_defs) end; -fun add_bnf const_policy fact_policy qualify tacs wit_tac Ds = +fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds = (fn (goals, wit_goalss, after_qed, lthy, defs) => let val wits_tac = K (TRYALL Goal.conjunction_tac) THEN' unfold_defs_tac lthy defs wit_tac; @@ -1170,14 +1167,14 @@ in (map2 (Skip_Proof.prove lthy [] []) goals (map (unfold_defs_tac lthy defs) tacs)) |> (fn thms => after_qed (map single thms @ wit_thms) lthy) - end) oo prepare_bnf const_policy fact_policy qualify + end) oo prepare_def const_policy fact_policy qualify (fn ctxt => singleton (Type_Infer_Context.infer_types ctxt)) Ds; -val add_bnf_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) => +val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) => Proof.unfolding ([[(defs, [])]]) (Proof.theorem NONE (snd oo after_qed) (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo - prepare_bnf Do_Inline user_policy I Syntax.read_term NONE; + prepare_def Do_Inline user_policy I Syntax.read_term NONE; fun print_bnfs ctxt = let @@ -1212,6 +1209,6 @@ Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type" (((Parse.binding --| Parse.$$$ "=") -- Parse.term -- (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term -- - (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]")) >> add_bnf_cmd); + (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]")) >> bnf_def_cmd); end; diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Thu Aug 30 22:38:12 2012 +0200 @@ -20,6 +20,7 @@ val coiterN: string val coiter_uniqueN: string val corecN: string + val exhaustN: string val fldN: string val fld_coiterN: string val fld_exhaustN: string @@ -30,6 +31,7 @@ val hsetN: string val hset_recN: string val inductN: string + val injectN: string val isNodeN: string val iterN: string val iter_uniqueN: string @@ -38,6 +40,7 @@ val map_uniqueN: string val min_algN: string val morN: string + val nchotomyN: string val pred_coinductN: string val pred_coinduct_uptoN: string val recN: string @@ -78,6 +81,8 @@ val mk_Field: term -> term val mk_union: term * term -> term + val mk_disjIN: int -> int -> thm + val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list @@ -153,9 +158,12 @@ val fld_unfN = fldN ^ "_" ^ unfN val unf_fldN = unfN ^ "_" ^ fldN -fun mk_nchotomyN s = s ^ "_nchotomy" -fun mk_injectN s = s ^ "_inject" -fun mk_exhaustN s = s ^ "_exhaust" +val nchotomyN = "nchotomy" +fun mk_nchotomyN s = s ^ "_" ^ nchotomyN +val injectN = "inject" +fun mk_injectN s = s ^ "_" ^ injectN +val exhaustN = "exhaust" +fun mk_exhaustN s = s ^ "_" ^ exhaustN val fld_injectN = mk_injectN fldN val fld_exhaustN = mk_exhaustN fldN val unf_injectN = mk_injectN unfN @@ -182,6 +190,11 @@ val mk_union = HOLogic.mk_binop @{const_name sup}; +fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]} + | mk_disjIN _ 1 = disjI1 + | mk_disjIN 2 2 = disjI2 + | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2; + (*dangerous; use with monotonic, converging functions only!*) fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X); diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Thu Aug 30 22:38:12 2012 +0200 @@ -2039,7 +2039,7 @@ val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms; val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms; val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms; - val unf_exhaust_thms = map (fn thm => thm RS @{thm exE}) unf_nchotomy_thms; + val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms; val bij_fld_thms = map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms; @@ -2047,7 +2047,7 @@ val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms; val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms; val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms; - val fld_exhaust_thms = map (fn thm => thm RS @{thm exE}) fld_nchotomy_thms; + val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms; val fld_coiter_thms = map3 (fn unf_inject => fn coiter => fn unf_fld => iffD1 OF [unf_inject, trans OF [coiter, unf_fld RS sym]]) @@ -2630,7 +2630,7 @@ val (Jbnfs, lthy) = fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => - add_bnf Dont_Inline user_policy I tacs wit_tac (SOME deads) + bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads) ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits)) tacss bs fs_maps setss_by_bnf Ts fld_witss lthy; diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Thu Aug 30 22:38:12 2012 +0200 @@ -124,6 +124,7 @@ open BNF_Tactics open BNF_Util +open BNF_FP_Util open BNF_GFP_Util fun mk_coalg_set_tac coalg_def = diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Codatatype/Tools/bnf_gfp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Thu Aug 30 22:38:12 2012 +0200 @@ -47,7 +47,6 @@ val mk_sum_case: term -> term -> term val mk_sum_caseN: term list -> term - val mk_disjIN: int -> int -> thm val mk_specN: int -> thm -> thm val mk_sum_casesN: int -> int -> thm val mk_sumEN: int -> thm @@ -193,11 +192,6 @@ A $ f1 $ f2 $ b1 $ b2 end; -fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]} - | mk_disjIN _ 1 = disjI1 - | mk_disjIN 2 2 = disjI2 - | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2; - fun mk_sumTN Ts = Library.foldr1 (mk_sumT) Ts; fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT)); diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Thu Aug 30 22:38:12 2012 +0200 @@ -1162,7 +1162,7 @@ val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms; val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms; val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms; - val unf_exhaust_thms = map (fn thm => thm RS @{thm exE}) unf_nchotomy_thms; + val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms; val bij_fld_thms = map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms; @@ -1170,7 +1170,7 @@ val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms; val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms; val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms; - val fld_exhaust_thms = map (fn thm => thm RS @{thm exE}) fld_nchotomy_thms; + val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms; val timer = time (timer "unf definitions & thms"); @@ -1661,7 +1661,7 @@ val (Ibnfs, lthy) = fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => - add_bnf Dont_Inline user_policy I tacs wit_tac (SOME deads) + bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads) ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits)) tacss bs fs_maps setss_by_bnf Ts fld_witss lthy; diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Codatatype/Tools/bnf_sugar.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML Thu Aug 30 22:38:12 2012 +0200 @@ -0,0 +1,360 @@ +(* Title: HOL/Codatatype/Tools/bnf_sugar.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Sugar on top of a BNF. +*) + +signature BNF_SUGAR = +sig +end; + +structure BNF_Sugar : BNF_SUGAR = +struct + +open BNF_Util +open BNF_FP_Util +open BNF_Sugar_Tactics + +val case_congN = "case_cong" +val case_discsN = "case_discs" +val casesN = "cases" +val ctr_selsN = "ctr_sels" +val disc_disjointN = "disc_disjoint" +val disc_exhaustN = "disc_exhaust" +val discsN = "discs" +val distinctN = "distinct" +val selsN = "sels" +val splitN = "split" +val split_asmN = "split_asm" +val weak_case_cong_thmsN = "weak_case_cong" + +fun mk_half_pairs [] = [] + | mk_half_pairs (x :: xs) = fold_rev (cons o pair x) xs (mk_half_pairs xs); + +fun index_of_half_row _ 0 = 0 + | index_of_half_row n j = index_of_half_row n (j - 1) + n - j; + +fun index_of_half_cell n j k = index_of_half_row n j + k - (j + 1); + +val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; + +fun eta_expand_caseof_arg f xs = fold_rev Term.lambda xs (Term.list_comb (f, xs)); + +fun prepare_sugar prep_term (((raw_ctrs, raw_caseof), disc_names), sel_namess) no_defs_lthy = + let + (* TODO: sanity checks on arguments *) + + (* TODO: normalize types of constructors w.r.t. each other *) + + val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; + val caseof0 = prep_term no_defs_lthy raw_caseof; + + val n = length ctrs0; + val ks = 1 upto n; + + val (T_name, As0) = dest_Type (body_type (fastype_of (hd ctrs0))); + val b = Binding.qualified_name T_name; + + val (As, B) = + no_defs_lthy + |> mk_TFrees (length As0) + ||> the_single o fst o mk_TFrees 1; + + fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T); + + fun mk_ctr Ts ctr = + let val Ts0 = snd (dest_Type (body_type (fastype_of ctr))) in + Term.subst_atomic_types (Ts0 ~~ Ts) ctr + end; + + fun mk_caseof Ts T = + let val (binders, body) = strip_type (fastype_of caseof0) in + Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ Ts)) caseof0 + end; + + val T = Type (T_name, As); + val ctrs = map (mk_ctr As) ctrs0; + val ctr_Tss = map (binder_types o fastype_of) ctrs; + + val ms = map length ctr_Tss; + + val caseofB = mk_caseof As B; + val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss; + + val (((((((xss, yss), fs), gs), (v, v')), w), p), names_lthy) = no_defs_lthy |> + mk_Freess "x" ctr_Tss + ||>> mk_Freess "y" ctr_Tss + ||>> mk_Frees "f" caseofB_Ts + ||>> mk_Frees "g" caseofB_Ts + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T + ||>> yield_singleton (mk_Frees "w") T + ||>> yield_singleton (mk_Frees "P") HOLogic.boolT; + + val xctrs = map2 (curry Term.list_comb) ctrs xss; + val yctrs = map2 (curry Term.list_comb) ctrs yss; + + val eta_fs = map2 eta_expand_caseof_arg fs xss; + val eta_gs = map2 eta_expand_caseof_arg gs xss; + + val exist_xs_v_eq_ctrs = + map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss; + + fun mk_sel_caseof_args k xs x T = + map2 (fn Ts => fn i => if i = k then fold_rev Term.lambda xs x else mk_undef T Ts) ctr_Tss ks; + + fun disc_spec b exist_xs_v_eq_ctr = + mk_Trueprop_eq (Free (Binding.name_of b, T --> HOLogic.boolT) $ v, exist_xs_v_eq_ctr); + + fun sel_spec b x xs k = + let val T' = fastype_of x in + mk_Trueprop_eq (Free (Binding.name_of b, T --> T') $ v, + Term.list_comb (mk_caseof As T', mk_sel_caseof_args k xs x T') $ v) + end; + + val (((raw_discs, (_, raw_disc_defs)), (raw_selss, (_, raw_sel_defss))), (lthy', lthy)) = + no_defs_lthy + |> apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn exist_xs_v_eq_ctr => + Specification.definition (SOME (b, NONE, NoSyn), + ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr))) disc_names exist_xs_v_eq_ctrs + ||>> apfst (apsnd split_list o split_list) o fold_map3 (fn bs => fn xs => fn k => + apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn x => + Specification.definition (SOME (b, NONE, NoSyn), + ((Thm.def_binding b, []), sel_spec b x xs k))) bs xs) sel_namess xss ks + ||> `Local_Theory.restore; + + (*transforms defined frees into consts (and more)*) + val phi = Proof_Context.export_morphism lthy lthy'; + + val disc_defs = map (Morphism.thm phi) raw_disc_defs; + val sel_defss = map (map (Morphism.thm phi)) raw_sel_defss; + + val discs0 = map (Morphism.term phi) raw_discs; + val selss0 = map (map (Morphism.term phi)) raw_selss; + + fun mk_disc_or_sel Ts t = + Term.subst_atomic_types (snd (dest_Type (domain_type (fastype_of t))) ~~ Ts) t; + + val discs = map (mk_disc_or_sel As) discs0; + val selss = map (map (mk_disc_or_sel As)) selss0; + + fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p); + + val goal_exhaust = + let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (v, xctr)]) in + mk_imp_p (map2 mk_prem xctrs xss) + end; + + val goal_injectss = + let + fun mk_goal _ _ [] [] = [] + | mk_goal xctr yctr xs ys = + [mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr), + Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))]; + in + map4 mk_goal xctrs yctrs xss yss + end; + + val goal_half_distincts = + map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq) (mk_half_pairs xctrs); + + val goal_cases = + let + val lhs0 = Term.list_comb (caseofB, eta_fs); + fun mk_goal xctr xs f = mk_Trueprop_eq (lhs0 $ xctr, Term.list_comb (f, xs)); + in + map3 mk_goal xctrs xss fs + end; + + val goals = [goal_exhaust] :: goal_injectss @ [goal_half_distincts, goal_cases]; + + fun after_qed thmss lthy = + let + val ([exhaust_thm], (inject_thmss, [half_distinct_thms, case_thms])) = + (hd thmss, chop n (tl thmss)); + + val exhaust_thm' = + let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in + Drule.instantiate' [] [SOME (certify lthy v)] + (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm)) + end; + + val other_half_distinct_thms = map (fn thm => thm RS not_sym) half_distinct_thms; + + val nchotomy_thm = + let + val goal = + HOLogic.mk_Trueprop (HOLogic.mk_all (fst v', snd v', + Library.foldr1 HOLogic.mk_disj exist_xs_v_eq_ctrs)); + in + Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm) + end; + + val sel_thmss = + let + fun mk_thm k xs goal_case case_thm x sel_def = + let + val T = fastype_of x; + val cTs = + map ((fn T' => certifyT lthy (if T' = B then T else T')) o TFree) + (rev (Term.add_tfrees goal_case [])); + val cxs = map (certify lthy) (mk_sel_caseof_args k xs x T); + in + Local_Defs.fold lthy [sel_def] + (Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm) + end; + fun mk_thms k xs goal_case case_thm sel_defs = + map2 (mk_thm k xs goal_case case_thm) xs sel_defs; + in + map5 mk_thms ks xss goal_cases case_thms sel_defss + end; + + val discD_thms = map (fn def => def RS iffD1) disc_defs; + val discI_thms = + map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs; + val not_disc_thms = + map2 (fn m => fn def => funpow m (fn thm => allI RS thm) + (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) + ms disc_defs; + + val disc_thms = + let + fun get_distinct_thm k k' = + if k > k' then nth half_distinct_thms (index_of_half_cell n (k' - 1) (k - 1)) + else nth other_half_distinct_thms (index_of_half_cell n (k' - 1) (k' - 1)) + fun mk_thm ((k, discI), not_disc) k' = + if k = k' then refl RS discI else get_distinct_thm k k' RS not_disc; + in + map_product mk_thm (ks ~~ discI_thms ~~ not_disc_thms) ks + end; + + val disc_disjoint_thms = + let + fun get_disc_thm k k' = nth disc_thms ((k' - 1) * n + (k - 1)); + fun mk_goal ((_, disc), (_, disc')) = + Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), + HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v)))); + fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); + + val bundles = ks ~~ ms ~~ discD_thms ~~ discs; + val half_pairs = mk_half_pairs bundles; + + val goal_halves = map mk_goal half_pairs; + val half_thms = + map2 (fn ((((k, m), discD), _), (((k', _), _), _)) => + prove (mk_half_disc_disjoint_tac m discD (get_disc_thm k k'))) + half_pairs goal_halves; + + val goal_other_halves = map (mk_goal o swap) half_pairs; + val other_half_thms = + map2 (prove o mk_other_half_disc_disjoint_tac) half_thms goal_other_halves; + in + half_thms @ other_half_thms + end; + + val disc_exhaust_thm = + let + fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (disc $ v)]; + val goal = fold Logic.all [p, v] (mk_imp_p (map mk_prem discs)); + in + Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms) + end; + + val ctr_sel_thms = + let + fun mk_goal ctr disc sels = + Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v), + mk_Trueprop_eq ((null sels ? swap) + (Term.list_comb (ctr, map (fn sel => sel $ v) sels), v)))); + val goals = map3 mk_goal ctrs discs selss; + in + map4 (fn goal => fn m => fn discD => fn sel_thms => + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + mk_ctr_sel_tac ctxt m discD sel_thms)) + goals ms discD_thms sel_thmss + end; + + val case_disc_thm = + let + fun mk_core f sels = Term.list_comb (f, map (fn sel => sel $ v) sels); + fun mk_rhs _ [f] [sels] = mk_core f sels + | mk_rhs (disc :: discs) (f :: fs) (sels :: selss) = + Const (@{const_name If}, HOLogic.boolT --> B --> B --> B) $ + (disc $ v) $ mk_core f sels $ mk_rhs discs fs selss; + + val lhs = Term.list_comb (caseofB, eta_fs) $ v; + val rhs = mk_rhs discs fs selss; + val goal = mk_Trueprop_eq (lhs, rhs); + in + Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thms sel_thmss) + |> singleton (Proof_Context.export names_lthy lthy) + end; + + val (case_cong_thm, weak_case_cong_thm) = + let + fun mk_prem xctr xs f g = + fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr), + mk_Trueprop_eq (f, g))); + fun mk_caseof_term fs = Term.list_comb (caseofB, fs); + + val v_eq_w = mk_Trueprop_eq (v, w); + val caseof_fs = mk_caseof_term eta_fs; + val caseof_gs = mk_caseof_term eta_gs; + + val goal = + Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs, + mk_Trueprop_eq (caseof_fs $ v, caseof_gs $ w)); + val goal_weak = + Logic.mk_implies (v_eq_w, mk_Trueprop_eq (caseof_fs $ v, caseof_fs $ w)); + in + (Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} => + mk_case_cong_tac ctxt exhaust_thm' case_thms), + Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1))) + |> pairself (singleton (Proof_Context.export names_lthy lthy)) + end; + + val split_thms = []; + + val split_asm_thms = []; + + (* case syntax *) + + fun note thmN thms = + snd o Local_Theory.note + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms); + in + lthy + |> note case_congN [case_cong_thm] + |> note case_discsN [case_disc_thm] + |> note casesN case_thms + |> note ctr_selsN ctr_sel_thms + |> note discsN disc_thms + |> note disc_disjointN disc_disjoint_thms + |> note disc_exhaustN [disc_exhaust_thm] + |> note distinctN (half_distinct_thms @ other_half_distinct_thms) + |> note exhaustN [exhaust_thm] + |> note injectN (flat inject_thmss) + |> note nchotomyN [nchotomy_thm] + |> note selsN (flat sel_thmss) + |> note splitN split_thms + |> note split_asmN split_asm_thms + |> note weak_case_cong_thmsN [weak_case_cong_thm] + end; + in + (goals, after_qed, lthy') + end; + +val parse_binding_list = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]"; + +val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) => + Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo + prepare_sugar Syntax.read_term; + +val _ = + Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF" + (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term -- + parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]")) + >> bnf_sugar_cmd); + +end; diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Thu Aug 30 22:38:12 2012 +0200 @@ -0,0 +1,71 @@ +(* Title: HOL/Codatatype/Tools/bnf_sugar_tactics.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Tactics for sugar on top of a BNF. +*) + +signature BNF_SUGAR_TACTICS = +sig + val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic + val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list -> thm list list -> tactic + val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic + val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic + val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic + val mk_nchotomy_tac: int -> thm -> tactic + val mk_other_half_disc_disjoint_tac: thm -> tactic +end; + +structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS = +struct + +open BNF_Tactics +open BNF_FP_Util + +fun eq_True_or_False thm = + thm RS @{thm eq_False[THEN iffD2]} + handle THM _ => thm RS @{thm eq_True[THEN iffD2]} + +fun context_ss_only thms = map_simpset (fn ss => Simplifier.clear_ss ss addsimps thms) + +fun mk_nchotomy_tac n exhaust = + (rtac allI THEN' rtac exhaust THEN' + EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; + +fun mk_half_disc_disjoint_tac m discD disc'_thm = + (dtac discD THEN' + REPEAT_DETERM_N m o etac exE THEN' + hyp_subst_tac THEN' + rtac disc'_thm) 1; + +fun mk_other_half_disc_disjoint_tac half_thm = + (etac @{thm contrapos_pn} THEN' etac half_thm) 1; + +fun mk_disc_exhaust_tac n exhaust discIs = + (rtac exhaust THEN' + EVERY' (map2 (fn k => fn discI => + dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1; + +fun mk_ctr_sel_tac ctxt m discD sel_thms = + (dtac discD THEN' + (if m = 0 then + atac + else + REPEAT_DETERM_N m o etac exE THEN' + hyp_subst_tac THEN' + SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN' + rtac refl)) 1; + +fun mk_case_disc_tac ctxt exhaust' case_thms disc_thms sel_thmss = + let val base_unfolds = @{thms if_True if_False} @ map eq_True_or_False disc_thms in + (rtac exhaust' THEN' + EVERY' (map2 (fn case_thm => fn sel_thms => EVERY' [ + hyp_subst_tac THEN' + SELECT_GOAL (Local_Defs.unfold_tac ctxt (base_unfolds @ sel_thms)) THEN' + rtac case_thm]) case_thms sel_thmss)) 1 + end; + +fun mk_case_cong_tac ctxt exhaust' case_thms = + rtac exhaust' 1 THEN ALLGOALS (clarsimp_tac (context_ss_only case_thms ctxt)); + +end; diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Nitpick_Examples/minipick.ML --- a/src/HOL/Nitpick_Examples/minipick.ML Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Nitpick_Examples/minipick.ML Thu Aug 30 22:38:12 2012 +0200 @@ -435,7 +435,7 @@ in case solve_any_problem debug overlord NONE max_threads max_solutions problems of - JavaNotInstalled => "unknown" + JavaNotFound => "unknown" | JavaTooOld => "unknown" | KodkodiNotInstalled => "unknown" | Normal ([], _, _) => "none" diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Tools/Datatype/rep_datatype.ML --- a/src/HOL/Tools/Datatype/rep_datatype.ML Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Thu Aug 30 22:38:12 2012 +0200 @@ -589,7 +589,7 @@ (case map_filter (fn (tyco, _) => if Symtab.defined (Datatype_Data.get_all thy) tyco then SOME tyco else NONE) raw_cs of [] => () - | tycos => error ("Type(s) " ^ commas_quote tycos ^ " already represented inductivly")); + | tycos => error ("Type(s) " ^ commas_quote tycos ^ " already represented inductively")); val raw_vss = maps (map (map snd o fst) o snd) raw_cs; val ms = (case distinct (op =) (map length raw_vss) of diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Aug 30 22:38:12 2012 +0200 @@ -155,7 +155,7 @@ type raw_bound = n_ary_index * int list list datatype outcome = - JavaNotInstalled | + JavaNotFound | JavaTooOld | KodkodiNotInstalled | Normal of (int * raw_bound list) list * int list * string | @@ -302,7 +302,7 @@ type raw_bound = n_ary_index * int list list datatype outcome = - JavaNotInstalled | + JavaNotFound | JavaTooOld | KodkodiNotInstalled | Normal of (int * raw_bound list) list * int list * string | @@ -1068,7 +1068,7 @@ else if code = 0 then Normal ([], js, first_error) else if code = 127 then - JavaNotInstalled + JavaNotFound else if has_error "UnsupportedClassVersionError" then JavaTooOld else if has_error "NoClassDefFoundError" then diff -r 1266b51f9bbc -r 8e124393c281 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Aug 30 21:50:49 2012 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Aug 30 22:38:12 2012 +0200 @@ -179,9 +179,13 @@ Pretty.str (if j = 1 then "." else ";")]) (length ts downto 1) ts))] -fun install_java_message () = - "Nitpick requires Java Development Kit 1.6 via ISABELLE_JDK_HOME setting." -fun install_kodkodi_message () = +val isabelle_wrong_message = + "Something appears to be wrong with your Isabelle installation." +fun java_not_found_message () = + "Java could not be launched. " ^ isabelle_wrong_message +fun java_too_old_message () = + "The Java version is too old. " ^ isabelle_wrong_message +fun kodkodi_not_installed_message () = "Nitpick requires the external Java program Kodkodi. To install it, download \ \the package from \"http://www21.in.tum.de/~blanchet/#software\" and add the \ \\"kodkodi-x.y.z\" directory's full path to " ^ @@ -802,14 +806,14 @@ else case KK.solve_any_problem debug overlord deadline max_threads max_solutions (map fst problems) of - KK.JavaNotInstalled => - (print_nt install_java_message; + KK.JavaNotFound => + (print_nt java_not_found_message; (found_really_genuine, max_potential, max_genuine, donno + 1)) | KK.JavaTooOld => - (print_nt install_java_message; + (print_nt java_too_old_message; (found_really_genuine, max_potential, max_genuine, donno + 1)) | KK.KodkodiNotInstalled => - (print_nt install_kodkodi_message; + (print_nt kodkodi_not_installed_message; (found_really_genuine, max_potential, max_genuine, donno + 1)) | KK.Normal ([], unsat_js, s) => (update_checked_problems problems unsat_js; show_kodkod_warning s; @@ -1062,7 +1066,7 @@ if getenv "KODKODI" = "" then (* The "expect" argument is deliberately ignored if Kodkodi is missing so that the "Nitpick_Examples" can be processed on any machine. *) - (print_nt (Pretty.string_of (plazy install_kodkodi_message)); + (print_nt (Pretty.string_of (plazy kodkodi_not_installed_message)); ("no_kodkodi", state)) else let