--- a/src/HOL/Predicate.thy Fri Jun 25 11:48:37 2010 +0200
+++ b/src/HOL/Predicate.thy Fri Jun 25 14:05:49 2010 +0200
@@ -645,7 +645,7 @@
lemma "f () = False \<or> f () = True"
by simp
-lemma closure_of_bool_cases:
+lemma closure_of_bool_cases [no_atp]:
assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
assumes "f = (%u. True) \<Longrightarrow> P f"
shows "P f"
--- a/src/HOL/Sledgehammer.thy Fri Jun 25 11:48:37 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Fri Jun 25 14:05:49 2010 +0200
@@ -53,16 +53,6 @@
lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
by (simp add: fequal_def)
-text{*These two represent the equivalence between Boolean equality and iff.
-They can't be converted to clauses automatically, as the iff would be
-expanded...*}
-
-lemma iff_positive: "P \<or> Q \<or> P = Q"
-by blast
-
-lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
-by blast
-
text{*Theorems for translation to combinators*}
lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Jun 25 11:48:37 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Jun 25 14:05:49 2010 +0200
@@ -223,7 +223,7 @@
val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss
val result =
do_run false
- |> (fn (_, msecs0, _, SOME IncompleteUnprovable) =>
+ |> (fn (_, msecs0, _, SOME _) =>
do_run true
|> (fn (output, msecs, proof, outcome) =>
(output, msecs0 + msecs, proof, outcome))
@@ -298,9 +298,11 @@
val spass_config : prover_config =
{home_var = "SPASS_HOME",
executable = "SPASS",
+ (* "div 2" accounts for the fact that SPASS is often run twice. *)
arguments = fn complete => fn timeout =>
("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
- \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
+ \-VarWeight=3 -TimeLimit=" ^
+ string_of_int (to_generous_secs timeout div 2))
|> not complete ? prefix "-SOS=1 ",
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Jun 25 11:48:37 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Jun 25 14:05:49 2010 +0200
@@ -2520,6 +2520,8 @@
let
val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
val (in_ts, clause_out_ts) = split_mode mode ts;
+ val split_ss = HOL_basic_ss' addsimps [@{thm split_eta}, @{thm split_beta},
+ @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
fun prove_prems2 out_ts [] =
print_tac options "before prove_match2 - last call:"
THEN prove_match2 options ctxt out_ts
@@ -2530,14 +2532,12 @@
THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
THEN (asm_full_simp_tac HOL_basic_ss' 1)
THEN SOLVED (print_tac options "state before applying intro rule:"
- THEN (rtac pred_intro_rule 1)
+ THEN (rtac pred_intro_rule
(* How to handle equality correctly? *)
- THEN (print_tac options "state before assumption matching")
- THEN (REPEAT (atac 1 ORELSE
- (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
- [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"},
- @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
- THEN print_tac options "state after simp_tac:"))))
+ THEN_ALL_NEW (K (print_tac options "state before assumption matching")
+ THEN' (fn i => REPEAT (atac i ORELSE (CHANGED (asm_full_simp_tac split_ss i)
+ THEN print_tac options "state after pre-simplification:")))
+ THEN' (K (print_tac options "state after assumption matching:")))) 1)
| prove_prems2 out_ts ((p, deriv) :: ps) =
let
val mode = head_mode_of deriv
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 25 11:48:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 25 14:05:49 2010 +0200
@@ -446,13 +446,15 @@
of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
could then fail. See comment on mk_var.*)
fun resolve_inc_tyvars(tha,i,thb) =
- let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
+ let
+ val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
in
case distinct Thm.eq_thm ths of
[th] => th
| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
- end;
+ end
+ handle TERM (msg, _) => raise METIS ("resolve_inc_tyvars", msg)
fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
let
@@ -679,8 +681,7 @@
(*The modes FO and FT are sticky. HO can be downgraded to FO.*)
fun set_mode FO = FO
| set_mode HO =
- if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
- else HO
+ if forall (is_quasi_fol_theorem thy) (cls @ ths) then FO else HO
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Jun 25 11:48:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Jun 25 14:05:49 2010 +0200
@@ -21,7 +21,7 @@
val tvar_classes_of_terms : term list -> string list
val tfree_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
- val is_quasi_fol_term : theory -> term -> bool
+ val is_quasi_fol_theorem : theory -> thm -> bool
val relevant_facts :
bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
@@ -88,42 +88,75 @@
Symtab.map_default (c, [ctyps])
(fn [] => [] | ctypss => insert (op =) ctyps ctypss)
-val fresh_Ex_prefix = "Sledgehammer.Ex."
+val fresh_prefix = "Sledgehammer.Fresh."
+
+val flip = Option.map not
-fun get_goal_consts_typs thy goals =
+val boring_natural_consts = [@{const_name If}]
+(* Including equality in this list might be expected to stop rules like
+ subset_antisym from being chosen, but for some reason filtering works better
+ with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
+ because any remaining occurrences must be within comprehensions. *)
+val boring_cnf_consts =
+ [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
+ @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
+ @{const_name "op ="}]
+
+fun get_consts_typs thy pos ts =
let
- val use_natural_form = !use_natural_form
(* Free variables are included, as well as constants, to handle locales.
"skolem_id" is included to increase the complexity of theorems containing
Skolem functions. In non-CNF form, "Ex" is included but each occurrence
is considered fresh, to simulate the effect of Skolemization. *)
- fun aux (Const (x as (s, _))) =
- (if s = @{const_name Ex} andalso use_natural_form then
- (gensym fresh_Ex_prefix, [])
- else
- (const_with_typ thy x))
- |> add_const_type_to_table
- | aux (Free x) = add_const_type_to_table (const_with_typ thy x)
- | aux ((t as Const (@{const_name skolem_id}, _)) $ _) = aux t
- | aux (t $ u) = aux t #> aux u
- | aux (Abs (_, _, t)) = aux t
- | aux _ = I
- (* Including equality in this list might be expected to stop rules like
- subset_antisym from being chosen, but for some reason filtering works better
- with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
- because any remaining occurrences must be within comprehensions. *)
- val standard_consts =
- [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
- @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
- @{const_name "op ="}] @
- (if use_natural_form then
- [@{const_name All}, @{const_name Ex}, @{const_name "op &"},
- @{const_name "op -->"}]
- else
- [])
+ fun do_term t =
+ case t of
+ Const x => add_const_type_to_table (const_with_typ thy x)
+ | Free x => add_const_type_to_table (const_with_typ thy x)
+ | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t
+ | t1 $ t2 => do_term t1 #> do_term t2
+ | Abs (_, _, t) =>
+ (* Abstractions lead to combinators, so we add a penalty for them. *)
+ add_const_type_to_table (gensym fresh_prefix, [])
+ #> do_term t
+ | _ => I
+ fun do_quantifier sweet_pos pos body_t =
+ do_formula pos body_t
+ #> (if pos = SOME sweet_pos then I
+ else add_const_type_to_table (gensym fresh_prefix, []))
+ and do_equality T t1 t2 =
+ fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
+ else do_term) [t1, t2]
+ and do_formula pos t =
+ case t of
+ Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
+ do_quantifier false pos body_t
+ | @{const "==>"} $ t1 $ t2 =>
+ do_formula (flip pos) t1 #> do_formula pos t2
+ | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
+ do_equality T t1 t2
+ | @{const Trueprop} $ t1 => do_formula pos t1
+ | @{const Not} $ t1 => do_formula (flip pos) t1
+ | Const (@{const_name All}, _) $ Abs (_, _, body_t) =>
+ do_quantifier false pos body_t
+ | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
+ do_quantifier true pos body_t
+ | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const "op -->"} $ t1 $ t2 =>
+ do_formula (flip pos) t1 #> do_formula pos t2
+ | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
+ do_equality T t1 t2
+ | (t0 as Const (_, @{typ bool})) $ t1 =>
+ do_term t0 #> do_formula pos t1 (* theory constant *)
+ | _ => do_term t
in
- Symtab.empty |> fold (Symtab.update o rpair []) standard_consts
- |> fold aux goals
+ Symtab.empty
+ |> (if !use_natural_form then
+ fold (Symtab.update o rpair []) boring_natural_consts
+ #> fold (do_formula pos) ts
+ else
+ fold (Symtab.update o rpair []) boring_cnf_consts
+ #> fold do_term ts)
end
(*Inserts a dummy "constant" referring to the theory name, so that relevance
@@ -217,7 +250,7 @@
fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
fun consts_typs_of_term thy t =
- Symtab.fold add_expand_pairs (get_goal_consts_typs thy [t]) []
+ Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) []
fun pair_consts_typs_axiom theory_relevant thy axiom =
(axiom, axiom |> appropriate_prop_of theory_relevant
@@ -306,9 +339,11 @@
if weight >= threshold orelse
(defs_relevant andalso
defines thy (#1 clsthm) rel_const_tab) then
- (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^
- " passes: " ^ Real.toString weight);
- relevant ((ax, weight) :: newrels, rejects) axs)
+ (trace_msg (fn () =>
+ name ^ " clause " ^ Int.toString n ^
+ " passes: " ^ Real.toString weight
+ (* ^ " consts: " ^ commas (map fst consts_typs) *));
+ relevant ((ax, weight) :: newrels, rejects) axs)
else
relevant (newrels, ax :: rejects) axs
end
@@ -322,14 +357,24 @@
fun relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant relevance_override
thy (axioms : cnf_thm list) goals =
- if relevance_threshold > 0.0 then
+ if relevance_threshold > 1.0 then
+ []
+ else if relevance_threshold < 0.0 then
+ axioms
+ else
let
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
Symtab.empty
- val goal_const_tab = get_goal_consts_typs thy goals
+ val goal_const_tab = get_consts_typs thy (SOME true) goals
+ val relevance_threshold =
+ if !use_natural_form then 0.9 * relevance_threshold (* experimental *)
+ else relevance_threshold
val _ =
trace_msg (fn () => "Initial constants: " ^
- commas (Symtab.keys goal_const_tab))
+ commas (goal_const_tab
+ |> Symtab.dest
+ |> filter (curry (op <>) [] o snd)
+ |> map fst))
val relevant =
relevant_clauses ctxt relevance_convergence defs_relevant max_new
relevance_override const_tab relevance_threshold
@@ -340,8 +385,6 @@
trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
relevant
end
- else
- axioms;
(***************************************************************)
(* Retrieving and filtering lemmas *)
@@ -374,6 +417,9 @@
fun subtract_cls ax_clauses =
filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
+val exists_sledgehammer_const =
+ exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
+
fun all_name_thms_pairs respect_no_atp ctxt chained_ths =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
@@ -396,7 +442,8 @@
val name1 = Facts.extern facts name;
val name2 = Name_Space.extern full_space name;
- val ths = filter_out is_theorem_bad_for_atps ths0;
+ val ths = filter_out (is_theorem_bad_for_atps orf
+ exists_sledgehammer_const) ths0
in
case find_first check_thms [name1, name2, name] of
NONE => I
@@ -483,13 +530,8 @@
(* ATP invocation methods setup *)
(***************************************************************)
-fun is_quasi_fol_term thy =
- Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 []
-
-(*Ensures that no higher-order theorems "leak out"*)
-fun restrict_to_logic thy true cls =
- filter (is_quasi_fol_term thy o prop_of o fst) cls
- | restrict_to_logic _ false cls = cls
+fun is_quasi_fol_theorem thy =
+ Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
(**** Predicates to detect unwanted clauses (prolific or likely to cause
unsoundness) ****)
@@ -539,43 +581,35 @@
(has_typed_var dangerous_types t orelse
forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
-fun remove_dangerous_clauses full_types add_thms =
- filter_out (fn (cnf_th, (_, orig_th)) =>
- not (member Thm.eq_thm add_thms orig_th) andalso
- is_dangerous_term full_types (prop_of cnf_th))
-
fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
fun relevant_facts full_types respect_no_atp relevance_threshold
relevance_convergence defs_relevant max_new theory_relevant
(relevance_override as {add, del, only})
(ctxt, (chained_ths, _)) goal_cls =
- if (only andalso null add) orelse relevance_threshold > 1.0 then
- []
- else
- let
- val thy = ProofContext.theory_of ctxt
- val has_override = not (null add) orelse not (null del)
- val is_FO = is_fol_goal thy goal_cls
- val axioms =
- checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
- (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
- else all_name_thms_pairs respect_no_atp ctxt chained_ths)
- |> cnf_rules_pairs thy
- |> not has_override ? make_unique
- |> not only ? restrict_to_logic thy is_FO
- |> (if only then
- I
- else
- remove_dangerous_clauses full_types
- (maps (ProofContext.get_fact ctxt) add))
- in
- relevance_filter ctxt relevance_threshold relevance_convergence
- defs_relevant max_new theory_relevant relevance_override
- thy axioms (map prop_of goal_cls)
- |> has_override ? make_unique
- |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
- end
+ let
+ val thy = ProofContext.theory_of ctxt
+ val add_thms = maps (ProofContext.get_fact ctxt) add
+ val has_override = not (null add) orelse not (null del)
+ val is_FO = is_fol_goal thy goal_cls
+ val axioms =
+ checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
+ (map (name_thms_pair_from_ref ctxt chained_ths) add @
+ (if only then []
+ else all_name_thms_pairs respect_no_atp ctxt chained_ths))
+ |> cnf_rules_pairs thy
+ |> not has_override ? make_unique
+ |> filter (fn (cnf_thm, (_, orig_thm)) =>
+ member Thm.eq_thm add_thms orig_thm orelse
+ ((not is_FO orelse is_quasi_fol_theorem thy cnf_thm) andalso
+ not (is_dangerous_term full_types (prop_of cnf_thm))))
+ in
+ relevance_filter ctxt relevance_threshold relevance_convergence
+ defs_relevant max_new theory_relevant relevance_override
+ thy axioms (map prop_of goal_cls)
+ |> has_override ? make_unique
+ |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
+ end
(** Helper clauses **)
@@ -586,7 +620,7 @@
fun count_literal (Literal (_, t)) = count_combterm t
fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
-val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
+fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
fun cnf_helper_thms thy raw =
map (`Thm.get_name_hint)
#> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Jun 25 11:48:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Jun 25 14:05:49 2010 +0200
@@ -8,6 +8,8 @@
signature SLEDGEHAMMER_FACT_PREPROCESSOR =
sig
type cnf_thm = thm * ((string * int) * thm)
+
+ val sledgehammer_prefix: string
val chained_prefix: string
val trace: bool Unsynchronized.ref
val trace_msg: (unit -> string) -> unit
@@ -35,13 +37,15 @@
type cnf_thm = thm * ((string * int) * thm)
+val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
+
(* Used to label theorems chained into the goal. *)
-val chained_prefix = "Sledgehammer.chained_"
+val chained_prefix = sledgehammer_prefix ^ "chained_"
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();
-val skolem_theory_name = "Sledgehammer.Sko"
+val skolem_theory_name = sledgehammer_prefix ^ "Sko"
val skolem_prefix = "sko_"
val skolem_infix = "$"
@@ -183,25 +187,14 @@
fun vars_of_thm th =
map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
-(*Make a version of fun_cong with a given variable name*)
-local
- val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*)
- val cx = hd (vars_of_thm fun_cong');
- val ty = typ_of (ctyp_of_term cx);
- val thy = theory_of_thm fun_cong;
- fun mkvar a = cterm_of thy (Var((a,0),ty));
-in
-fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong'
-end;
+val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
-(*Removes the lambdas from an equation of the form t = (%x. u). A non-negative n,
- serves as an upper bound on how many to remove.*)
-fun strip_lambdas 0 th = th
- | strip_lambdas n th =
- case prop_of th of
- _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) =>
- strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
- | _ => th;
+(* Removes the lambdas from an equation of the form t = (%x. u). *)
+fun extensionalize th =
+ case prop_of th of
+ _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
+ $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
+ | _ => th
fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
| is_quasi_lambda_free (t1 $ t2) =
@@ -339,9 +332,9 @@
fun to_nnf th ctxt0 =
let val th1 = th |> transform_elim |> zero_var_indexes
val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
- val th3 = th2
- |> Conv.fconv_rule Object_Logic.atomize
- |> Meson.make_nnf ctxt |> strip_lambdas ~1
+ val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
+ |> extensionalize
+ |> Meson.make_nnf ctxt
in (th3, ctxt) end;
(*Generate Skolem functions for a theorem supplied in nnf*)
--- a/src/HOL/Tools/meson.ML Fri Jun 25 11:48:37 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Jun 25 14:05:49 2010 +0200
@@ -521,10 +521,9 @@
nnf_ss also includes the one-point simprocs,
which are needed to avoid the various one-point theorems from generating junk clauses.*)
val nnf_simps =
- [@{thm simp_implies_def}, @{thm Ex1_def}, @{thm Ball_def},@{thm Bex_def}, @{thm if_True},
- @{thm if_False}, @{thm if_cancel}, @{thm if_eq_cancel}, @{thm cases_simp}];
-val nnf_extra_simps =
- @{thms split_ifs} @ @{thms ex_simps} @ @{thms all_simps} @ @{thms simp_thms};
+ @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
+ if_eq_cancel cases_simp}
+val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
val nnf_ss =
HOL_basic_ss addsimps nnf_extra_simps
--- a/src/HOL/Word/BinGeneral.thy Fri Jun 25 11:48:37 2010 +0200
+++ b/src/HOL/Word/BinGeneral.thy Fri Jun 25 14:05:49 2010 +0200
@@ -127,29 +127,26 @@
subsection {* Destructors for binary integers *}
-definition bin_rl :: "int \<Rightarrow> int \<times> bit" where
- [code del]: "bin_rl w = (THE (r, l). w = r BIT l)"
+definition bin_last :: "int \<Rightarrow> bit" where
+ "bin_last w = (if w mod 2 = 0 then bit.B0 else bit.B1)"
+
+definition bin_rest :: "int \<Rightarrow> int" where
+ "bin_rest w = w div 2"
-lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
- apply (unfold bin_rl_def)
- apply safe
- apply (cases w rule: bin_exhaust)
- apply auto
+definition bin_rl :: "int \<Rightarrow> int \<times> bit" where
+ "bin_rl w = (bin_rest w, bin_last w)"
+
+lemma bin_rl_char: "bin_rl w = (r, l) \<longleftrightarrow> r BIT l = w"
+ apply (cases l)
+ apply (auto simp add: bin_rl_def bin_last_def bin_rest_def)
+ unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id
+ apply arith+
done
-definition
- bin_rest_def [code del]: "bin_rest w = fst (bin_rl w)"
-
-definition
- bin_last_def [code del] : "bin_last w = snd (bin_rl w)"
-
primrec bin_nth where
Z: "bin_nth w 0 = (bin_last w = bit.B1)"
| Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
-lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"
- unfolding bin_rest_def bin_last_def by auto
-
lemma bin_rl_simps [simp]:
"bin_rl Int.Pls = (Int.Pls, bit.B0)"
"bin_rl Int.Min = (Int.Min, bit.B1)"
@@ -160,7 +157,11 @@
declare bin_rl_simps(1-4) [code]
-lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
+thm iffD1 [OF bin_rl_char bin_rl_def]
+
+lemma bin_rl_simp [simp]:
+ "bin_rest w BIT bin_last w = w"
+ by (simp add: iffD1 [OF bin_rl_char bin_rl_def])
lemma bin_abs_lem:
"bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
@@ -209,7 +210,7 @@
"bin_rest (Int.Bit0 w) = w"
"bin_rest (Int.Bit1 w) = w"
"bin_rest (w BIT b) = w"
- unfolding bin_rest_def by auto
+ using bin_rl_simps bin_rl_def by auto
declare bin_rest_simps(1-4) [code]
@@ -219,7 +220,7 @@
"bin_last (Int.Bit0 w) = bit.B0"
"bin_last (Int.Bit1 w) = bit.B1"
"bin_last (w BIT b) = b"
- unfolding bin_last_def by auto
+ using bin_rl_simps bin_rl_def by auto
declare bin_last_simps(1-4) [code]
@@ -345,14 +346,9 @@
termination
apply (relation "measure (nat o abs o snd o snd o snd)")
- apply simp
- apply (simp add: Pls_def brlem)
- apply (clarsimp simp: bin_rl_char pred_def)
- apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]])
- apply (unfold Pls_def Min_def number_of_eq)
- prefer 2
- apply (erule asm_rl)
- apply auto
+ apply (auto simp add: bin_rl_def bin_last_def bin_rest_def)
+ unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id
+ apply auto
done
declare bin_rec.simps [simp del]