extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics
authorbulwahn
Wed Sep 23 16:20:12 2009 +0200 (2009-09-23)
changeset 326658bf46a97ff79
parent 32664 5d4f32b02450
child 32666 fd96d5f49d59
extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics
src/HOL/ex/Predicate_Compile_ex.thy
src/HOL/ex/predicate_compile.ML
     1.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4      "partition f [] [] []"
     1.5    | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
     1.6    | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
     1.7 -
     1.8 +ML {* set Toplevel.debug *} 
     1.9  code_pred partition .
    1.10  
    1.11  thm partition.equation
     2.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
     2.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
     2.3 @@ -672,7 +672,7 @@
     2.4    let
     2.5      val Ts = binder_types T
     2.6      val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
     2.7 -    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs 
     2.8 +    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs
     2.9    in
    2.10      (paramTs' @ inargTs) ---> (mk_predT compfuns (mk_tupleT outargTs))
    2.11    end;
    2.12 @@ -1335,14 +1335,23 @@
    2.13  
    2.14  fun compile_pred compfuns mk_fun_of use_size thy all_vs param_vs s T mode moded_cls =
    2.15    let
    2.16 -    val (Ts1, (Us1, Us2)) = split_modeT mode (binder_types T)
    2.17 -    val funT_of = if use_size then sizelim_funT_of else funT_of 
    2.18 +	  val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
    2.19 +    val (Us1, Us2) = split_smodeT (snd mode) Ts2
    2.20 +    val funT_of = if use_size then sizelim_funT_of else funT_of
    2.21      val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) (fst mode) Ts1
    2.22 -    val xnames = Name.variant_list (all_vs @ param_vs)
    2.23 -      (map (fn (i, NONE) => "x" ^ string_of_int i | (i, SOME s) => error "pair mode") (snd mode));
    2.24 -    val size_name = Name.variant (all_vs @ param_vs @ xnames) "size"
    2.25 -    (* termify code: val xs = map2 (fn s => fn T => Free (s, termifyT T)) xnames Us1; *)
    2.26 -    val xs = map2 (fn s => fn T => Free (s, T)) xnames Us1;
    2.27 +    val size_name = Name.variant (all_vs @ param_vs) "size"
    2.28 +  	fun mk_input_term (i, NONE) =
    2.29 +		    [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
    2.30 +		  | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of
    2.31 +						   [] => error "strange unit input"
    2.32 +					   | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
    2.33 +						 | Ts => let
    2.34 +							 val vnames = Name.variant_list (all_vs @ param_vs)
    2.35 +								(map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
    2.36 +									pis)
    2.37 +						 in if null pis then []
    2.38 +						   else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end
    2.39 +		val in_ts = maps mk_input_term (snd mode)
    2.40      val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1'
    2.41      val size = Free (size_name, @{typ "code_numeral"})
    2.42      val decr_size =
    2.43 @@ -1353,7 +1362,7 @@
    2.44          NONE
    2.45      val cl_ts =
    2.46        map (compile_clause compfuns decr_size (fn out_ts => mk_single compfuns (mk_tuple out_ts))
    2.47 -        thy all_vs param_vs mode (mk_tuple xs)) moded_cls;
    2.48 +        thy all_vs param_vs mode (mk_tuple in_ts)) moded_cls;
    2.49      val t = foldr1 (mk_sup compfuns) cl_ts
    2.50      val T' = mk_predT compfuns (mk_tupleT Us2)
    2.51      val size_t = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
    2.52 @@ -1361,16 +1370,17 @@
    2.53        $ mk_bot compfuns (dest_predT compfuns T') $ t
    2.54      val fun_const = mk_fun_of compfuns thy (s, T) mode
    2.55      val eq = if use_size then
    2.56 -      (list_comb (fun_const, params @ xs @ [size]), size_t)
    2.57 +      (list_comb (fun_const, params @ in_ts @ [size]), size_t)
    2.58      else
    2.59 -      (list_comb (fun_const, params @ xs), t)
    2.60 +      (list_comb (fun_const, params @ in_ts), t)
    2.61    in
    2.62      HOLogic.mk_Trueprop (HOLogic.mk_eq eq)
    2.63    end;
    2.64    
    2.65  (* special setup for simpset *)                  
    2.66 -val HOL_basic_ss' = HOL_basic_ss addsimps @{thms "HOL.simp_thms"} setSolver 
    2.67 -  (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
    2.68 +val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms "HOL.simp_thms"} @ [@{thm Pair_eq}])
    2.69 +  setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
    2.70 +	setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
    2.71  
    2.72  (* Definition of executable functions and their intro and elim rules *)
    2.73  
    2.74 @@ -1381,35 +1391,93 @@
    2.75          (ks @ [SOME k]))) arities));
    2.76  
    2.77  fun mk_Eval_of ((x, T), NONE) names = (x, names)
    2.78 -  | mk_Eval_of ((x, T), SOME mode) names = let
    2.79 -  val Ts = binder_types T
    2.80 -  val argnames = Name.variant_list names
    2.81 +  | mk_Eval_of ((x, T), SOME mode) names =
    2.82 +	let
    2.83 +    val Ts = binder_types T
    2.84 +    (*val argnames = Name.variant_list names
    2.85          (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
    2.86 -  val args = map Free (argnames ~~ Ts)
    2.87 -  val (inargs, outargs) = split_smode mode args
    2.88 -  val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs), mk_tuple outargs)
    2.89 -  val t = fold_rev lambda args r 
    2.90 -in
    2.91 -  (t, argnames @ names)
    2.92 -end;
    2.93 +    val args = map Free (argnames ~~ Ts)
    2.94 +    val (inargs, outargs) = split_smode mode args*)
    2.95 +		fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", HOLogic.unitT)) t
    2.96 +			| mk_split_lambda [x] t = lambda x t
    2.97 +			| mk_split_lambda xs t =
    2.98 +			let
    2.99 +				fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
   2.100 +					| mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
   2.101 +			in
   2.102 +				mk_split_lambda' xs t
   2.103 +			end;
   2.104 +  	fun mk_arg (i, T) =
   2.105 +		  let
   2.106 +	  	  val vname = Name.variant names ("x" ^ string_of_int i)
   2.107 +		    val default = Free (vname, T)
   2.108 +		  in 
   2.109 +		    case AList.lookup (op =) mode i of
   2.110 +		      NONE => (([], [default]), [default])
   2.111 +			  | SOME NONE => (([default], []), [default])
   2.112 +			  | SOME (SOME pis) =>
   2.113 +				  case HOLogic.strip_tupleT T of
   2.114 +						[] => error "pair mode but unit tuple" (*(([default], []), [default])*)
   2.115 +					| [_] => error "pair mode but not a tuple" (*(([default], []), [default])*)
   2.116 +					| Ts =>
   2.117 +					  let
   2.118 +							val vnames = Name.variant_list names
   2.119 +								(map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
   2.120 +									(1 upto length Ts))
   2.121 +							val args = map Free (vnames ~~ Ts)
   2.122 +							fun split_args (i, arg) (ins, outs) =
   2.123 +							  if member (op =) pis i then
   2.124 +							    (arg::ins, outs)
   2.125 +								else
   2.126 +								  (ins, arg::outs)
   2.127 +							val (inargs, outargs) = fold_rev split_args ((1 upto length Ts) ~~ args) ([], [])
   2.128 +							fun tuple args = if null args then [] else [HOLogic.mk_tuple args]
   2.129 +						in ((tuple inargs, tuple outargs), args) end
   2.130 +			end
   2.131 +		val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts))
   2.132 +    val (inargs, outargs) = pairself flat (split_list inoutargs)
   2.133 +		val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs), mk_tuple outargs)
   2.134 +    val t = fold_rev mk_split_lambda args r
   2.135 +  in
   2.136 +    (t, names)
   2.137 +  end;
   2.138  
   2.139  fun create_intro_elim_rule (mode as (iss, is)) defthm mode_id funT pred thy =
   2.140  let
   2.141    val Ts = binder_types (fastype_of pred)
   2.142    val funtrm = Const (mode_id, funT)
   2.143 -  val argnames = Name.variant_list []
   2.144 -        (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
   2.145    val (Ts1, Ts2) = chop (length iss) Ts;
   2.146    val Ts1' = map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
   2.147 -  val args = map Free (argnames ~~ (Ts1' @ Ts2))
   2.148 -  val (params, ioargs) = chop (length iss) args
   2.149 -  val (inargs, outargs) = split_smode is ioargs
   2.150 -  val param_names = Name.variant_list argnames
   2.151 +	val param_names = Name.variant_list []
   2.152 +    (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1)));
   2.153 +  val params = map Free (param_names ~~ Ts1')
   2.154 +	fun mk_args (i, T) argnames =
   2.155 +    let
   2.156 +		  val vname = Name.variant (param_names @ argnames) ("x" ^ string_of_int (length Ts1' + i))
   2.157 +		  val default = (Free (vname, T), vname :: argnames)
   2.158 +	  in
   2.159 +  	  case AList.lookup (op =) is i of
   2.160 +						 NONE => default
   2.161 +					 | SOME NONE => default
   2.162 +        	 | SOME (SOME pis) =>
   2.163 +					   case HOLogic.strip_tupleT T of
   2.164 +						   [] => default
   2.165 +					   | [_] => default
   2.166 +						 | Ts => 
   2.167 +						let
   2.168 +							val vnames = Name.variant_list (param_names @ argnames)
   2.169 +								(map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
   2.170 +									(1 upto (length Ts)))
   2.171 +						 in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames  @ argnames) end
   2.172 +		end
   2.173 +	val (args, argnames) = fold_map mk_args (1 upto (length Ts2) ~~ Ts2) []
   2.174 +  val (inargs, outargs) = split_smode is args
   2.175 +  val param_names' = Name.variant_list (param_names @ argnames)
   2.176      (map (fn i => "p" ^ string_of_int i) (1 upto (length iss)))
   2.177 -  val param_vs = map Free (param_names ~~ Ts1)
   2.178 +  val param_vs = map Free (param_names' ~~ Ts1)
   2.179    val (params', names) = fold_map mk_Eval_of ((params ~~ Ts1) ~~ iss) []
   2.180 -  val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ ioargs))
   2.181 -  val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ ioargs))
   2.182 +  val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ args))
   2.183 +  val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ args))
   2.184    val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
   2.185    val funargs = params @ inargs
   2.186    val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs),
   2.187 @@ -1418,13 +1486,16 @@
   2.188                     mk_tuple outargs))
   2.189    val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
   2.190    val simprules = [defthm, @{thm eval_pred},
   2.191 -                   @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}]
   2.192 +	  @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
   2.193    val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
   2.194 -  val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
   2.195 +  val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
   2.196    val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
   2.197    val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
   2.198 -  val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
   2.199 -in 
   2.200 +  val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
   2.201 +	val _ = Output.tracing (Display.string_of_thm_global thy elimthm)
   2.202 +	val _ = Output.tracing (Display.string_of_thm_global thy introthm)
   2.203 +
   2.204 +in
   2.205    (introthm, elimthm)
   2.206  end;
   2.207  
   2.208 @@ -1439,7 +1510,33 @@
   2.209      (Sign.full_bname thy (prefix ^ (Long_Name.base_name name))) ^
   2.210        (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ (string_of_mode (snd mode))
   2.211    end;
   2.212 -  
   2.213 +
   2.214 +fun split_tupleT is T =
   2.215 +	let
   2.216 +		fun split_tuple' _ _ [] = ([], [])
   2.217 +			| split_tuple' is i (T::Ts) =
   2.218 +			(if i mem is then apfst else apsnd) (cons T)
   2.219 +				(split_tuple' is (i+1) Ts)
   2.220 +	in
   2.221 +	  split_tuple' is 1 (HOLogic.strip_tupleT T)
   2.222 +  end
   2.223 +	
   2.224 +fun mk_arg xin xout pis T =
   2.225 +  let
   2.226 +	  val n = length (HOLogic.strip_tupleT T)
   2.227 +		val ni = length pis
   2.228 +	  fun mk_proj i j t =
   2.229 +		  (if i = j then I else HOLogic.mk_fst)
   2.230 +			  (funpow (i - 1) HOLogic.mk_snd t)
   2.231 +	  fun mk_arg' i (si, so) = if i mem pis then
   2.232 +		    (mk_proj si ni xin, (si+1, so))
   2.233 +		  else
   2.234 +			  (mk_proj so (n - ni) xout, (si, so+1))
   2.235 +	  val (args, _) = fold_map mk_arg' (1 upto n) (1, 1)
   2.236 +	in
   2.237 +	  HOLogic.mk_tuple args
   2.238 +	end
   2.239 +
   2.240  fun create_definitions preds (name, modes) thy =
   2.241    let
   2.242      val compfuns = PredicateCompFuns.compfuns
   2.243 @@ -1454,10 +1551,50 @@
   2.244        val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (mk_tupleT Us2))
   2.245        val names = Name.variant_list []
   2.246          (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
   2.247 -      val xs = map Free (names ~~ (Ts1' @ Ts2))
   2.248 +			(* old *)
   2.249 +			(*
   2.250 +		  val xs = map Free (names ~~ (Ts1' @ Ts2))
   2.251        val (xparams, xargs) = chop (length iss) xs
   2.252        val (xins, xouts) = split_smode is xargs
   2.253 -      val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ iss) names
   2.254 +			*)
   2.255 +			(* new *)
   2.256 +			val param_names = Name.variant_list []
   2.257 +			  (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
   2.258 +		  val xparams = map Free (param_names ~~ Ts1')
   2.259 +      fun mk_vars (i, T) names =
   2.260 +			  let
   2.261 +				  val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
   2.262 +				in
   2.263 +					case AList.lookup (op =) is i of
   2.264 +						 NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names)
   2.265 +					 | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names)
   2.266 +        	 | SOME (SOME pis) =>
   2.267 +					   let
   2.268 +						   val (Tins, Touts) = split_tupleT pis T
   2.269 +							 val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in")
   2.270 +							 val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out")
   2.271 +						   val xin = Free (name_in, HOLogic.mk_tupleT Tins)
   2.272 +							 val xout = Free (name_out, HOLogic.mk_tupleT Touts)
   2.273 +							 val xarg = mk_arg xin xout pis T
   2.274 +						 in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
   2.275 +						(* HOLogic.strip_tupleT T of
   2.276 +						[] => 
   2.277 +							in (Free (vname, T), vname :: names) end
   2.278 +					| [_] => let val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
   2.279 +							in (Free (vname, T), vname :: names) end
   2.280 +					| Ts =>
   2.281 +						let
   2.282 +							val vnames = Name.variant_list names
   2.283 +								(map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
   2.284 +									(1 upto (length Ts)))
   2.285 +						 in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames @ names) end *)
   2.286 +				end
   2.287 +   	  val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
   2.288 +      val (xinout, xargs) = split_list xinoutargs
   2.289 +			val (xins, xouts) = pairself flat (split_list xinout)
   2.290 +			(*val (xins, xouts) = split_smode is xargs*)
   2.291 +			val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ iss) names
   2.292 +			val _ = Output.tracing ("xargs:" ^ commas (map (Syntax.string_of_term_global thy) xargs))
   2.293        fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
   2.294          | mk_split_lambda [x] t = lambda x t
   2.295          | mk_split_lambda xs t =
   2.296 @@ -1471,12 +1608,15 @@
   2.297          (list_comb (Const (name, T), xparams' @ xargs)))
   2.298        val lhs = list_comb (Const (mode_cname, funT), xparams @ xins)
   2.299        val def = Logic.mk_equals (lhs, predterm)
   2.300 +			val _ = Output.tracing ("def:" ^ (Syntax.string_of_term_global thy def))
   2.301        val ([definition], thy') = thy |>
   2.302          Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
   2.303          PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
   2.304        val (intro, elim) =
   2.305          create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
   2.306 -      in thy' |> add_predfun name mode (mode_cname, definition, intro, elim)
   2.307 +			val _ = Output.tracing (Display.string_of_thm_global thy' definition)
   2.308 +      in thy'
   2.309 +			  |> add_predfun name mode (mode_cname, definition, intro, elim)
   2.310          |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
   2.311          |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
   2.312          |> Theory.checkpoint
   2.313 @@ -1544,8 +1684,9 @@
   2.314      val (params, _) = chop (length ms) args
   2.315      val f_tac = case f of
   2.316        Const (name, T) => simp_tac (HOL_basic_ss addsimps 
   2.317 -         (@{thm eval_pred}::(predfun_definition_of thy name mode)::
   2.318 -         @{thm "Product_Type.split_conv"}::[])) 1
   2.319 +         ([@{thm eval_pred}, (predfun_definition_of thy name mode),
   2.320 +         @{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
   2.321 +				 @{thm "snd_conv"}, @{thm pair_collapse}, @{thm "Product_Type.split_conv"}])) 1
   2.322      | Free _ => TRY (rtac @{thm refl} 1)
   2.323      | Abs _ => error "prove_param: No valid parameter term"
   2.324    in
   2.325 @@ -1578,7 +1719,13 @@
   2.326          THEN (EVERY (map (prove_param thy) (ms ~~ args1)))
   2.327          THEN (REPEAT_DETERM (atac 1))
   2.328        end
   2.329 -  | _ => rtac @{thm bindI} 1 THEN atac 1
   2.330 +  | _ => rtac @{thm bindI} 1
   2.331 +	  THEN asm_full_simp_tac
   2.332 +		  (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
   2.333 +				 @{thm "snd_conv"}, @{thm pair_collapse}]) 1
   2.334 +	  THEN (atac 1)
   2.335 +	  THEN print_tac "after prove parameter call"
   2.336 +		
   2.337  
   2.338  fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; 
   2.339  
   2.340 @@ -1595,7 +1742,7 @@
   2.341  (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
   2.342  in
   2.343     (* make this simpset better! *)
   2.344 -  asm_simp_tac (HOL_basic_ss' addsimps simprules) 1
   2.345 +  asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
   2.346    THEN print_tac "after prove_match:"
   2.347    THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1
   2.348           THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss 1))))
   2.349 @@ -1629,7 +1776,9 @@
   2.350      val (in_ts, clause_out_ts) = split_smode is ts;
   2.351      fun prove_prems out_ts [] =
   2.352        (prove_match thy out_ts)
   2.353 -      THEN asm_simp_tac HOL_basic_ss' 1
   2.354 +			THEN print_tac "before simplifying assumptions"
   2.355 +      THEN asm_full_simp_tac HOL_basic_ss' 1
   2.356 +			THEN print_tac "before single intro rule"
   2.357        THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
   2.358      | prove_prems out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
   2.359        let
   2.360 @@ -1694,6 +1843,7 @@
   2.361      val pred_case_rule = the_elim_of thy pred
   2.362    in
   2.363      REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
   2.364 +		THEN print_tac "before applying elim rule"
   2.365      THEN etac (predfun_elim_of thy pred mode) 1
   2.366      THEN etac pred_case_rule 1
   2.367      THEN (EVERY (map
   2.368 @@ -1805,7 +1955,8 @@
   2.369        (* How to handle equality correctly? *)
   2.370        THEN (print_tac "state before assumption matching")
   2.371        THEN (REPEAT (atac 1 ORELSE 
   2.372 -         (CHANGED (asm_full_simp_tac HOL_basic_ss' 1)
   2.373 +         (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
   2.374 +					 [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
   2.375            THEN print_tac "state after simp_tac:"))))
   2.376      | prove_prems2 out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
   2.377        let
   2.378 @@ -1879,6 +2030,7 @@
   2.379        (if !do_proofs then
   2.380          (fn _ =>
   2.381          rtac @{thm pred_iffI} 1
   2.382 +				THEN print_tac "after pred_iffI"
   2.383          THEN prove_one_direction thy clauses preds modes pred mode moded_clauses
   2.384          THEN print_tac "proved one direction"
   2.385          THEN prove_other_direction thy modes pred mode moded_clauses
   2.386 @@ -2245,4 +2397,3 @@
   2.387  end;
   2.388  
   2.389  end;
   2.390 -