--- a/etc/isar-keywords.el Thu Aug 30 09:47:46 2012 +0200
+++ b/etc/isar-keywords.el Thu Aug 30 09:47:46 2012 +0200
@@ -35,6 +35,7 @@
"bnf_codata"
"bnf_data"
"bnf_def"
+ "bnf_sugar"
"boogie_end"
"boogie_open"
"boogie_status"
@@ -576,6 +577,7 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
"bnf_def"
+ "bnf_sugar"
"boogie_vc"
"code_pred"
"corollary"
--- a/src/HOL/Codatatype/Codatatype.thy Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Codatatype.thy Thu Aug 30 09:47:46 2012 +0200
@@ -14,6 +14,7 @@
keywords
"bnf_sugar" :: thy_goal
uses
+ "Tools/bnf_sugar_tactics.ML"
"Tools/bnf_sugar.ML"
begin
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Thu Aug 30 09:47:46 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
@@ -39,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
@@ -79,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
@@ -154,10 +158,12 @@
val fld_unfN = fldN ^ "_" ^ unfN
val unf_fldN = unfN ^ "_" ^ fldN
-fun mk_nchotomyN s = s ^ "_nchotomy"
+val nchotomyN = "nchotomy"
+fun mk_nchotomyN s = s ^ "_" ^ nchotomyN
val injectN = "inject"
fun mk_injectN s = s ^ "_" ^ injectN
-fun mk_exhaustN s = s ^ "_exhaust"
+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
@@ -184,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_tactics.ML Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Thu Aug 30 09:47:46 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 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Thu Aug 30 09:47:46 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_sugar.ML Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML Thu Aug 30 09:47:46 2012 +0200
@@ -14,33 +14,51 @@
open BNF_Util
open BNF_FP_Util
+open BNF_Sugar_Tactics
val distinctN = "distinct";
-fun prepare_sugar prep_typ prep_term ((((raw_T, raw_ctors), raw_dtors), raw_storss), raw_recur)
+fun prepare_sugar prep_term (((raw_ctors, raw_dtors), raw_storss), raw_recur)
lthy =
let
(* TODO: sanity checks on arguments *)
- val T as Type (T_name, _) = prep_typ lthy raw_T;
- val b = Binding.qualified_name T_name;
-
val ctors = map (prep_term lthy) raw_ctors;
val ctor_Tss = map (binder_types o fastype_of) ctors;
- val ((xss, yss), _) = lthy |>
+ val T as Type (T_name, _) = body_type (fastype_of (hd ctors));
+ val b = Binding.qualified_name T_name;
+
+ val n = length ctors;
+
+ val ((((xss, yss), (v, v')), p), _) = lthy |>
mk_Freess "x" ctor_Tss
- ||>> mk_Freess "y" ctor_Tss;
+ ||>> mk_Freess "y" ctor_Tss
+ ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") T
+ ||>> yield_singleton (mk_Frees "P") HOLogic.boolT;
+
+ val xs_ctors = map2 (curry Term.list_comb) ctors xss;
+ val ys_ctors = map2 (curry Term.list_comb) ctors yss;
+
+ val goal_exhaust =
+ let
+ fun mk_imp_p Q = Logic.list_implies (Q, HOLogic.mk_Trueprop p);
+ fun mk_prem xs_ctor xs =
+ fold_rev Logic.all xs
+ (mk_imp_p [HOLogic.mk_Trueprop (HOLogic.mk_eq (v, xs_ctor))]);
+ in
+ mk_imp_p (map2 mk_prem xs_ctors xss)
+ end;
val goal_injects =
let
- fun mk_goal _ [] [] = NONE
- | mk_goal ctor xs ys =
+ fun mk_goal _ _ [] [] = NONE
+ | mk_goal xs_ctor ys_ctor xs ys =
SOME (HOLogic.mk_Trueprop (HOLogic.mk_eq
- (HOLogic.mk_eq (Term.list_comb (ctor, xs), Term.list_comb (ctor, ys)),
+ (HOLogic.mk_eq (xs_ctor, ys_ctor),
Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys))));
in
- map_filter I (map3 mk_goal ctors xss yss)
+ map_filter I (map4 mk_goal xs_ctors ys_ctors xss yss)
end;
val goal_half_distincts =
@@ -49,24 +67,37 @@
fun mk_goals [] = []
| mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts);
in
- mk_goals (map2 (curry Term.list_comb) ctors xss)
+ mk_goals xs_ctors
end;
- val goals = [goal_injects, goal_half_distincts];
+ val goals = [[goal_exhaust], goal_injects, goal_half_distincts];
fun after_qed thmss lthy =
let
- val [inject_thms, half_distinct_thms] = thmss;
+ val [[exhaust_thm], inject_thms, half_distinct_thms] = thmss;
val other_half_distinct_thms = map (fn thm => thm RS not_sym) half_distinct_thms;
+ val nchotomy_thm =
+ let
+ fun mk_disjunct xs_ctor xs = list_exists_free xs (HOLogic.mk_eq (v, xs_ctor))
+ val goal =
+ HOLogic.mk_Trueprop
+ (HOLogic.mk_all (fst v', snd v',
+ Library.foldr1 HOLogic.mk_disj (map2 mk_disjunct xs_ctors xss)));
+ in
+ Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
+ end;
+
fun note thmN thms =
snd o Local_Theory.note
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
in
lthy
+ |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
+ |> note exhaustN [exhaust_thm]
|> note injectN inject_thms
- |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
+ |> note nchotomyN [nchotomy_thm]
end;
in
(goals, after_qed, lthy)
@@ -76,11 +107,11 @@
val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) =>
Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo
- prepare_sugar Syntax.read_typ Syntax.read_term;
+ prepare_sugar Syntax.read_term;
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF"
- ((Parse.typ -- (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") --
+ (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") --
parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]") --
Parse.term) >> bnf_sugar_cmd);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML Thu Aug 30 09:47:46 2012 +0200
@@ -0,0 +1,22 @@
+(* 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_nchotomy_tac: int -> thm -> tactic
+end;
+
+structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
+struct
+
+open BNF_FP_Util
+
+fun mk_nchotomy_tac n exhaust =
+ (rtac allI THEN' rtac exhaust THEN'
+ EVERY' (maps (fn i => [rtac (mk_disjIN n i), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
+
+end;
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Thu Aug 30 09:47:46 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