# HG changeset patch
# User blanchet
# Date 1388702671 -3600
# Node ID 862c36b6e57ce231d11d93f676745a78c9002676
# Parent  8f50ad61b0a9fc88f936e0013125a9fbb4e78d5f
avoid schematic variable in goal, which sometimes gets instantiated by tactic

diff -r 8f50ad61b0a9 -r 862c36b6e57c src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Thu Jan 02 23:07:49 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Thu Jan 02 23:44:31 2014 +0100
@@ -1020,10 +1020,10 @@
         map wit_goal (0 upto live - 1)
       end;
 
-    val trivial_wit_tac = mk_trivial_wit_tac bnf_wit_defs;
+    val triv_wit_tac = mk_trivial_wit_tac bnf_wit_defs;
 
     val wit_goalss =
-      (if null raw_wits then SOME trivial_wit_tac else NONE, map mk_wit_goals bnf_wit_As);
+      (if null raw_wits then SOME triv_wit_tac else NONE, map mk_wit_goals bnf_wit_As);
 
     fun after_qed mk_wit_thms thms lthy =
       let
diff -r 8f50ad61b0a9 -r 862c36b6e57c src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 23:07:49 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 23:44:31 2014 +0100
@@ -850,6 +850,10 @@
 fun applied_fun_of fun_name fun_T fun_args =
   list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
 
+fun is_trivial_implies thm =
+  op aconv (Logic.dest_implies (Thm.prop_of thm))
+  handle TERM _ => false;
+
 fun add_primcorec_ursive maybe_tac opts fixes specs maybe_of_specs lthy =
   let
     val thy = Proof_Context.theory_of lthy;
@@ -933,9 +937,9 @@
       |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
       |> split_list o map split_list;
 
-    val list_all_fun_args =
+    fun list_all_fun_args extras =
       map2 (fn [] => I
-          | {fun_args, ...} :: _ => map (curry Logic.list_all (map dest_Free fun_args)))
+          | {fun_args, ...} :: _ => map (curry Logic.list_all (extras @ map dest_Free fun_args)))
         disc_eqnss;
 
     val syntactic_exhaustives =
@@ -951,7 +955,7 @@
     val nchotomy_goalss =
       map2 (fn false => K [] | true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems)
         de_facto_exhaustives disc_eqnss
-      |> list_all_fun_args
+      |> list_all_fun_args []
     val nchotomy_taut_thmss =
       map2 (fn syntactic_exhaustive =>
           (case maybe_tac of
@@ -969,12 +973,6 @@
         else
           I);
 
-    val p = Var (("P", 0), HOLogic.boolT); (* safe since there are no other variables around *)
-
-    fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
-
-    val p_imp_p = mk_imp_p [mk_imp_p []];
-
     fun prove thmss'' def_thms' lthy =
       let
         val def_thms = map (snd o snd) def_thms';
@@ -985,17 +983,22 @@
 
         val exhaust_thmss =
           map2 (fn false => K []
-              | true => single o mk_imp_p o map (mk_imp_p o map HOLogic.mk_Trueprop o #prems))
+              | true => fn disc_eqns as {fun_args, ...} :: _ =>
+                let
+                  val p = Bound (length fun_args);
+                  fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
+                in
+                  [mk_imp_p (map (mk_imp_p o map HOLogic.mk_Trueprop o #prems) disc_eqns)]
+                end)
             de_facto_exhaustives disc_eqnss
-          |> list_all_fun_args
+          |> list_all_fun_args [("P", HOLogic.boolT)]
           |> map3 (fn disc_eqns => fn [] => K []
               | [nchotomy_thm] => fn [goal] =>
                 [mk_primcorec_exhaust_tac (length disc_eqns) nchotomy_thm
                  |> K |> Goal.prove lthy [] [] goal
                  |> Thm.close_derivation])
             disc_eqnss nchotomy_thmss;
-        val nontriv_exhaust_thmss =
-          map (filter_out (fn thm => prop_of thm aconv p_imp_p)) exhaust_thmss;
+        val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss;
 
         val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss);
         fun mk_excludesss excludes n =
diff -r 8f50ad61b0a9 -r 862c36b6e57c src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Thu Jan 02 23:07:49 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Thu Jan 02 23:44:31 2014 +0100
@@ -130,7 +130,6 @@
   val mk_sym: thm -> thm
   val mk_trans: thm -> thm -> thm
 
-  val is_triv_implies: thm -> bool
   val is_refl: thm -> bool
   val is_concl_refl: thm -> bool
   val no_refl: thm list -> thm list
@@ -569,10 +568,6 @@
     | mk_UnIN n m = mk_UnIN' (n - m)
 end;
 
-fun is_triv_implies thm =
-  op aconv (Logic.dest_implies (Thm.prop_of thm))
-  handle TERM _ => false;
-
 fun is_refl_prop t =
   op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop t))
   handle TERM _ => false;