--- 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"
--- 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"
--- 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
--- 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;
--- 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;
--- 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);
--- 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;
--- 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 =
--- 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));
--- 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;
--- /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;
--- /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;
--- 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"
--- 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
--- 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
--- 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