--- a/src/HOL/BNF/BNF_FP_Base.thy Wed Sep 25 12:42:56 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Base.thy Wed Sep 25 12:52:21 2013 +0200
@@ -172,15 +172,6 @@
(if b then f y else if b' then x' else f y')"
by simp
-lemma if_then_else_True_False:
- "(if p then False else r) \<longleftrightarrow> \<not> p \<and> r"
- "(if p then True else r) \<longleftrightarrow> p \<or> r"
- "(if p then q else False) \<longleftrightarrow> p \<and> q"
- "(if p then q else True) \<longleftrightarrow> \<not> p \<or> q"
-by simp_all
-
-lemmas bool_if_simps = bool_simps(7,8,15-17,19,21-24,29-32) if_then_else_True_False
-
ML_file "Tools/bnf_fp_util.ML"
ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
ML_file "Tools/bnf_fp_def_sugar.ML"
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 25 12:42:56 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 25 12:52:21 2013 +0200
@@ -30,6 +30,7 @@
case_conv_ifs: thm list};
val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
+ val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
val rep_compat_prefix: string
@@ -39,9 +40,9 @@
val mk_ctr: typ list -> term -> term
val mk_case: typ list -> typ -> term -> term
val mk_disc_or_sel: typ list -> term -> term
-
val name_of_ctr: term -> string
val name_of_disc: term -> string
+ val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
(((bool * bool) * term list) * binding) *
@@ -103,6 +104,27 @@
expands = map (Morphism.thm phi) expands,
case_conv_ifs = map (Morphism.thm phi) case_conv_ifs};
+fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
+ {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
+ ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2;
+
+structure Data = Generic_Data
+(
+ type T = ctr_sugar Symtab.table;
+ val empty = Symtab.empty;
+ val extend = I;
+ val merge = Symtab.merge eq_ctr_sugar;
+);
+
+fun ctr_sugar_of ctxt =
+ Symtab.lookup (Data.get (Context.Proof ctxt))
+ #> Option.map (morph_ctr_sugar
+ (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
+
+fun register_ctr_sugar key ctr_sugar =
+ Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
+
val rep_compat_prefix = "new";
val isN = "is_";
@@ -193,6 +215,28 @@
val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
+fun dest_case ctxt s Ts t =
+ (case Term.strip_comb t of
+ (Const (c, _), args as _ :: _) =>
+ (case ctr_sugar_of ctxt s of
+ SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
+ if case_name = c then
+ let
+ val n = length discs0;
+ val (branches, obj :: leftovers) = chop n args;
+ val discs = map (mk_disc_or_sel Ts) discs0;
+ val selss = map (map (mk_disc_or_sel Ts)) selss0;
+ val conds = map (rapp obj) discs;
+ val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
+ val branches' = map2 (curry Term.betapplys) branches branch_argss;
+ in
+ SOME (conds, branches')
+ end
+ else
+ NONE
+ | _ => NONE)
+ | _ => NONE);
+
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, rep_compat), raw_ctrs),
@@ -787,19 +831,23 @@
val notes' =
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
+
+ val ctr_sugar =
+ {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
+ nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
+ case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
+ split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
+ discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
+ collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms};
in
- ({ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
- nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
- case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
- split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
- discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
- collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms},
+ (ctr_sugar,
lthy
|> not rep_compat ?
(Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Case_Translation.register
(Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
- |> Local_Theory.notes (notes' @ notes) |> snd)
+ |> Local_Theory.notes (notes' @ notes) |> snd
+ |> register_ctr_sugar dataT_name ctr_sugar)
end;
in
(goalss, after_qed, lthy')
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Sep 25 12:42:56 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Sep 25 12:52:21 2013 +0200
@@ -51,11 +51,6 @@
val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
fun drop_All t = subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
strip_qnt_body @{const_name all} t)
-fun s_not @{const True} = @{const False}
- | s_not @{const False} = @{const True}
- | s_not (@{const Not} $ t) = t
- | s_not (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
- | s_not t = HOLogic.mk_not t
val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
fun invert_prems [t] = map s_not (HOLogic.disjuncts t)
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 12:42:56 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 12:52:21 2013 +0200
@@ -51,6 +51,7 @@
nested_map_comps: thm list,
ctr_specs: corec_ctr_spec list}
+ val s_not: term -> term
val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
typ list -> term -> term -> term -> term
val massage_direct_corec_call: Proof.context -> (term -> bool) -> (term -> term) -> typ list ->
@@ -60,9 +61,8 @@
val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
val massage_corec_code_rhs: Proof.context -> (term -> term list -> term) -> typ list -> typ ->
term -> term
- val fold_rev_corec_code_rhs: Proof.context -> (term -> term list -> 'a -> 'a) -> typ list ->
- term -> 'a -> 'a
- val simplify_bool_ifs: theory -> term -> term list
+ val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
+ typ list -> term -> 'a -> 'a
val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
((term * term list list) list) list -> local_theory ->
(bool * rec_spec list * typ list * thm * thm list) * local_theory
@@ -139,6 +139,12 @@
fun unexpected_corec_call ctxt t =
error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
+fun s_not @{const True} = @{const False}
+ | s_not @{const False} = @{const True}
+ | s_not (@{const Not} $ t) = t
+ | s_not (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+ | s_not t = HOLogic.mk_not t
+
fun factor_out_types ctxt massage destU U T =
(case try destU U of
SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
@@ -175,7 +181,7 @@
val map' = mk_map (length fs) Us ran_Ts map0;
val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
in
- list_comb (map', fs')
+ Term.list_comb (map', fs')
end
| NONE => raise AINT_NO_MAP t)
| massage_map _ _ t = raise AINT_NO_MAP t
@@ -197,28 +203,32 @@
massage_call
end;
-(* TODO: also support old-style datatypes.
- (Ideally, we would have a proper registry for these things.) *)
-fun case_of ctxt =
- fp_sugar_of ctxt #> Option.map (fst o dest_Const o #casex o of_fp_sugar #ctr_sugars);
-
fun fold_rev_let_if_case ctxt f bound_Ts =
let
- fun fld t =
+ val thy = Proof_Context.theory_of ctxt;
+
+ fun fld conds t =
(case Term.strip_comb t of
- (Const (@{const_name Let}, _), [arg1, arg2]) => fld (betapply (arg2, arg1))
- | (Const (@{const_name If}, _), _ :: branches) => fold_rev fld branches
+ (Const (@{const_name Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1))
+ | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
+ fld (cond :: conds) then_branch o fld (s_not cond :: conds) else_branch
| (Const (c, _), args as _ :: _) =>
- let val (branches, obj) = split_last args in
- (case fastype_of1 (bound_Ts, obj) of
- Type (T_name, _) => if case_of ctxt T_name = SOME c then fold_rev fld branches else f t
- | _ => f t)
+ let val n = num_binder_types (Sign.the_const_type thy c) in
+ (case fastype_of1 (bound_Ts, nth args (n - 1)) of
+ Type (s, Ts) =>
+ (case dest_case ctxt s Ts t of
+ NONE => f conds t
+ | SOME (conds', branches) =>
+ fold_rev (uncurry fld) (map (fn cond => cond :: conds) conds' ~~ branches))
+ | _ => f conds t)
end
- | _ => f t)
+ | _ => f conds t)
in
- fld
+ fld []
end;
+fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
+
fun massage_let_if_case ctxt has_call massage_leaf bound_Ts U =
let
val typof = curry fastype_of1 bound_Ts;
@@ -228,7 +238,7 @@
(case Term.strip_comb t of
(Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec (betapply (arg2, arg1))
| (Const (@{const_name If}, _), obj :: branches) =>
- list_comb (If_const U $ tap check_obj obj, map massage_rec branches)
+ Term.list_comb (If_const U $ tap check_obj obj, map massage_rec branches)
| (Const (c, _), args as _ :: _) =>
let val (branches, obj) = split_last args in
(case fastype_of1 (bound_Ts, obj) of
@@ -238,7 +248,7 @@
val branches' = map massage_rec branches;
val casex' = Const (c, map typof branches' ---> typof obj);
in
- list_comb (casex', branches') $ tap check_obj obj
+ Term.list_comb (casex', branches') $ tap check_obj obj
end
else
massage_leaf t
@@ -273,7 +283,7 @@
val map' = mk_map (length fs) dom_Ts Us map0;
val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
in
- list_comb (map', fs')
+ Term.list_comb (map', fs')
end
| NONE => raise AINT_NO_MAP t)
| massage_map _ _ t = raise AINT_NO_MAP t
@@ -292,7 +302,8 @@
(case try (dest_ctr ctxt s) t of
SOME (f, args) =>
let val f' = mk_ctr Us f in
- list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
+ Term.list_comb (f',
+ map3 massage_call (binder_types (typof f')) (map typof args) args)
end
| NONE =>
(case t of
@@ -312,16 +323,9 @@
end;
fun expand_ctr_term ctxt s Ts t =
- (case fp_sugar_of ctxt s of
- SOME fp_sugar =>
- let
- val T = Type (s, Ts);
- val {ctrs = ctrs0, casex = case0, ...} = of_fp_sugar #ctr_sugars fp_sugar;
- val ctrs = map (mk_ctr Ts) ctrs0;
- val casex = mk_case Ts T case0;
- in
- list_comb (casex, ctrs) $ t
- end
+ (case ctr_sugar_of ctxt s of
+ SOME {ctrs, casex, ...} =>
+ Term.list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t
| NONE => raise Fail "expand_ctr_term");
fun expand_corec_code_rhs ctxt has_call bound_Ts t =
@@ -337,16 +341,8 @@
fun massage_corec_code_rhs ctxt massage_ctr =
massage_let_if_case ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
-fun fold_rev_corec_code_rhs ctxt f = fold_rev_let_if_case ctxt (uncurry f o Term.strip_comb);
-
-fun add_conjuncts (Const (@{const_name conj}, _) $ t $ t') = add_conjuncts t o add_conjuncts t'
- | add_conjuncts t = cons t;
-
-fun conjuncts t = add_conjuncts t [];
-
-fun simplify_bool_ifs thy =
- Raw_Simplifier.rewrite_term thy @{thms bool_if_simps[THEN eq_reflection]} []
- #> conjuncts #> (fn [@{term True}] => [] | ts => ts);
+fun fold_rev_corec_code_rhs ctxt f =
+ fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
fun indexedd xss = fold_map indexed xss;
--- a/src/HOL/IMP/Compiler.thy Wed Sep 25 12:42:56 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy Wed Sep 25 12:52:21 2013 +0200
@@ -21,16 +21,16 @@
where @{term i} is an @{typ int}.
*}
fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
-"(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
+"(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))"
text {*
The only additional lemma we need about this function
is indexing over append:
*}
lemma inth_append [simp]:
- "0 \<le> n \<Longrightarrow>
- (xs @ ys) !! n = (if n < size xs then xs !! n else ys !! (n - size xs))"
-by (induction xs arbitrary: n) (auto simp: algebra_simps)
+ "0 \<le> i \<Longrightarrow>
+ (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
+by (induction xs arbitrary: i) (auto simp: algebra_simps)
subsection "Instructions and Stack Machine"