Hi Andreas, thanks for reporting this.
The attached patch attempts to get this correct. Due to the current
breakdowns I have not yet been able to test or push it.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
# HG changeset patch
# Parent 3a20f8a24b13fc4c126859901a8c75db5b2dc7aa
proper trading of variables;
more appropriate ML variable names
diff -r 3a20f8a24b13 src/HOL/Library/Code_Abstract_Nat.thy
--- a/src/HOL/Library/Code_Abstract_Nat.thy Tue Jun 17 18:41:44 2014 +0200
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Wed Jun 18 23:15:53 2014 +0200
@@ -52,54 +52,54 @@
fun remove_suc ctxt thms =
let
- val thy = Proof_Context.theory_of ctxt;
val vname = singleton (Name.variant_list (map fst
(fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
- val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
- fun lhs_of th = snd (Thm.dest_comb
- (fst (Thm.dest_comb (cprop_of th))));
- fun rhs_of th = snd (Thm.dest_comb (cprop_of th));
+ val cv = cterm_of (Proof_Context.theory_of ctxt) (Var ((vname, 0),
HOLogic.natT));
+ val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o cprop_of;
+ val rhs_of = snd o Thm.dest_comb o cprop_of;
fun find_vars ct = (case term_of ct of
(Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb
ct))]
| _ $ _ =>
let val (ct1, ct2) = Thm.dest_comb ct
in
- map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
- map (apfst (Thm.apply ct1)) (find_vars ct2)
+ (map o apfst) (fn ct => Thm.apply ct ct2) (find_vars ct1) @
+ (map o apfst) (Thm.apply ct1) (find_vars ct2)
end
| _ => []);
- val eqs = maps
- (fn th => map (pair th) (find_vars (lhs_of th))) thms;
- fun mk_thms (th, (ct, cv')) =
+ val eqs = maps (fn thm => map (pair thm) (find_vars (lhs_of thm))) thms;
+ fun mk_thms (thm, (ct, cv')) =
let
- val th' =
+ val thm' =
Thm.implies_elim
(Conv.fconv_rule (Thm.beta_conversion true)
(Drule.instantiate'
[SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
- SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
- @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
+ SOME (Thm.lambda cv' (rhs_of thm)), NONE, SOME cv']
+ @{thm Suc_if_eq})) (Thm.forall_intr cv' thm)
in
- case map_filter (fn th'' =>
- SOME (th'', singleton
- (Variable.trade (K (fn [th'''] => [th''' RS th']))
- (Variable.global_thm_context th'')) th'')
+ case map_filter (fn thm'' => SOME (thm'', thm'' RS thm')
handle THM _ => NONE) thms of
[] => NONE
- | thps =>
- let val (ths1, ths2) = split_list thps
- in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
+ | thmps =>
+ let val (thms1, thms2) = split_list thmps
+ in SOME (subtract Thm.eq_thm (thm :: thms1) thms @ thms2) end
end
in get_first mk_thms eqs end;
-fun eqn_suc_base_preproc thy thms =
+fun remove_suc' ctxt [] = SOME []
+ | remove_suc' ctxt thms =
+ let
+ val thms' = Variable.trade (these oo remove_suc) ctxt thms;
+ in if null thms' then NONE else SOME thms' end;
+
+fun eqn_suc_base_preproc ctxt thms =
let
val dest = fst o Logic.dest_equals o prop_of;
val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
in
if forall (can dest) thms andalso exists (contains_suc o dest) thms
- then thms |> perhaps_loop (remove_suc thy) |> (Option.map o map)
Drule.zero_var_indexes
- else NONE
+ then perhaps_loop (remove_suc' ctxt) thms
+ else NONE
end;
val eqn_suc_preproc = Code_Preproc.simple_functrans eqn_suc_base_preproc;
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
