[isabelle-dev] [isabelle] Code_Abstract_Nat raises exception for a variable with name g

[Florian Haftmann]

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
-------------- next part --------------
# 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;
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140618/089a9ef8/attachment.asc>