src/HOL/ex/predicate_compile.ML
author bulwahn
Wed Apr 22 11:10:23 2009 +0200 (2009-04-22)
changeset 31105 95f66b234086
parent 30528 7173bf123335
child 31106 9a1178204dc0
permissions -rw-r--r--
added general preprocessing of equality in predicates for code generation
     1 (* Author: Lukas Bulwahn
     2 
     3 (Prototype of) A compiler from predicates specified by intro/elim rules
     4 to equations.
     5 *)
     6 
     7 signature PREDICATE_COMPILE =
     8 sig
     9   val create_def_equation': string -> (int list option list * int list) option -> theory -> theory
    10   val create_def_equation: string -> theory -> theory
    11   val intro_rule: theory -> string -> (int list option list * int list) -> thm
    12   val elim_rule: theory -> string -> (int list option list * int list) -> thm
    13   val strip_intro_concl : term -> int -> (term * (term list * term list))
    14   val code_ind_intros_attrib : attribute
    15   val code_ind_cases_attrib : attribute
    16   val setup : theory -> theory
    17   val print_alternative_rules : theory -> theory
    18   val do_proofs: bool ref
    19 end;
    20 
    21 structure Predicate_Compile: PREDICATE_COMPILE =
    22 struct
    23 
    24 structure PredModetab = TableFun(
    25   type key = (string * (int list option list * int list))
    26   val ord = prod_ord fast_string_ord (prod_ord
    27             (list_ord (option_ord (list_ord int_ord))) (list_ord int_ord)))
    28 
    29 
    30 structure IndCodegenData = TheoryDataFun
    31 (
    32   type T = {names : string PredModetab.table,
    33             modes : ((int list option list * int list) list) Symtab.table,
    34             function_defs : Thm.thm Symtab.table,
    35             function_intros : Thm.thm Symtab.table,
    36             function_elims : Thm.thm Symtab.table,
    37             intro_rules : (Thm.thm list) Symtab.table,
    38             elim_rules : Thm.thm Symtab.table,
    39             nparams : int Symtab.table
    40            };
    41       (* names: map from inductive predicate and mode to function name (string).
    42          modes: map from inductive predicates to modes
    43          function_defs: map from function name to definition
    44          function_intros: map from function name to intro rule
    45          function_elims: map from function name to elim rule
    46          intro_rules: map from inductive predicate to alternative intro rules
    47          elim_rules: map from inductive predicate to alternative elimination rule
    48          nparams: map from const name to number of parameters (* assuming there exist intro and elimination rules *) 
    49        *)
    50   val empty = {names = PredModetab.empty,
    51                modes = Symtab.empty,
    52                function_defs = Symtab.empty,
    53                function_intros = Symtab.empty,
    54                function_elims = Symtab.empty,
    55                intro_rules = Symtab.empty,
    56                elim_rules = Symtab.empty,
    57                nparams = Symtab.empty};
    58   val copy = I;
    59   val extend = I;
    60   fun merge _ r = {names = PredModetab.merge (op =) (pairself #names r),
    61                    modes = Symtab.merge (op =) (pairself #modes r),
    62                    function_defs = Symtab.merge Thm.eq_thm (pairself #function_defs r),
    63                    function_intros = Symtab.merge Thm.eq_thm (pairself #function_intros r),
    64                    function_elims = Symtab.merge Thm.eq_thm (pairself #function_elims r),
    65                    intro_rules = Symtab.merge ((forall Thm.eq_thm) o (op ~~)) (pairself #intro_rules r),
    66                    elim_rules = Symtab.merge Thm.eq_thm (pairself #elim_rules r),
    67                    nparams = Symtab.merge (op =) (pairself #nparams r)};
    68 );
    69 
    70   fun map_names f thy = IndCodegenData.map
    71     (fn x => {names = f (#names x), modes = #modes x, function_defs = #function_defs x,
    72             function_intros = #function_intros x, function_elims = #function_elims x,
    73             intro_rules = #intro_rules x, elim_rules = #elim_rules x,
    74             nparams = #nparams x}) thy
    75 
    76   fun map_modes f thy = IndCodegenData.map
    77     (fn x => {names = #names x, modes = f (#modes x), function_defs = #function_defs x,
    78             function_intros = #function_intros x, function_elims = #function_elims x,
    79             intro_rules = #intro_rules x, elim_rules = #elim_rules x,
    80             nparams = #nparams x}) thy
    81 
    82   fun map_function_defs f thy = IndCodegenData.map
    83     (fn x => {names = #names x, modes = #modes x, function_defs = f (#function_defs x),
    84             function_intros = #function_intros x, function_elims = #function_elims x,
    85             intro_rules = #intro_rules x, elim_rules = #elim_rules x,
    86             nparams = #nparams x}) thy 
    87   
    88   fun map_function_elims f thy = IndCodegenData.map
    89     (fn x => {names = #names x, modes = #modes x, function_defs = #function_defs x,
    90             function_intros = #function_intros x, function_elims = f (#function_elims x),
    91             intro_rules = #intro_rules x, elim_rules = #elim_rules x,
    92             nparams = #nparams x}) thy
    93 
    94   fun map_function_intros f thy = IndCodegenData.map
    95     (fn x => {names = #names x, modes = #modes x, function_defs = #function_defs x,
    96             function_intros = f (#function_intros x), function_elims = #function_elims x,
    97             intro_rules = #intro_rules x, elim_rules = #elim_rules x,
    98             nparams = #nparams x}) thy
    99 
   100   fun map_intro_rules f thy = IndCodegenData.map
   101     (fn x => {names = #names x, modes = #modes x, function_defs = #function_defs x,
   102             function_intros = #function_intros x, function_elims = #function_elims x,
   103             intro_rules = f (#intro_rules x), elim_rules = #elim_rules x,
   104             nparams = #nparams x}) thy 
   105   
   106   fun map_elim_rules f thy = IndCodegenData.map
   107     (fn x => {names = #names x, modes = #modes x, function_defs = #function_defs x,
   108             function_intros = #function_intros x, function_elims = #function_elims x,
   109             intro_rules = #intro_rules x, elim_rules = f (#elim_rules x),
   110             nparams = #nparams x}) thy
   111 
   112   fun map_nparams f thy = IndCodegenData.map
   113     (fn x => {names = #names x, modes = #modes x, function_defs = #function_defs x,
   114             function_intros = #function_intros x, function_elims = #function_elims x,
   115             intro_rules = #intro_rules x, elim_rules = #elim_rules x,
   116             nparams = f (#nparams x)}) thy
   117 
   118 (* Debug stuff and tactics ***********************************************************)
   119 
   120 fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
   121 fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single);
   122 
   123 fun debug_tac msg = (fn st =>
   124      (tracing msg; Seq.single st));
   125 
   126 (* removes first subgoal *)
   127 fun mycheat_tac thy i st =
   128   (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
   129 
   130 val (do_proofs : bool ref) = ref true;
   131 
   132 (* Lightweight mode analysis **********************************************)
   133 
   134 (* Hack for message from old code generator *)
   135 val message = tracing;
   136 
   137 
   138 (**************************************************************************)
   139 (* source code from old code generator ************************************)
   140 
   141 (**** check if a term contains only constructor functions ****)
   142 
   143 fun is_constrt thy =
   144   let
   145     val cnstrs = flat (maps
   146       (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
   147       (Symtab.dest (DatatypePackage.get_datatypes thy)));
   148     fun check t = (case strip_comb t of
   149         (Free _, []) => true
   150       | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
   151             (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
   152           | _ => false)
   153       | _ => false)
   154   in check end;
   155 
   156 (**** check if a type is an equality type (i.e. doesn't contain fun) ****)
   157 
   158 fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
   159   | is_eqT _ = true;
   160 
   161 (**** mode inference ****)
   162 
   163 fun string_of_mode (iss, is) = space_implode " -> " (map
   164   (fn NONE => "X"
   165     | SOME js => enclose "[" "]" (commas (map string_of_int js)))
   166        (iss @ [SOME is]));
   167 
   168 fun print_modes modes = message ("Inferred modes:\n" ^
   169   cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
   170     string_of_mode ms)) modes));
   171 
   172 fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
   173 val terms_vs = distinct (op =) o maps term_vs;
   174 
   175 (** collect all Frees in a term (with duplicates!) **)
   176 fun term_vTs tm =
   177   fold_aterms (fn Free xT => cons xT | _ => I) tm [];
   178 
   179 fun get_args is ts = let
   180   fun get_args' _ _ [] = ([], [])
   181     | get_args' is i (t::ts) = (if i mem is then apfst else apsnd) (cons t)
   182         (get_args' is (i+1) ts)
   183 in get_args' is 1 ts end
   184 
   185 fun merge xs [] = xs
   186   | merge [] ys = ys
   187   | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)
   188       else y::merge (x::xs) ys;
   189 
   190 fun subsets i j = if i <= j then
   191        let val is = subsets (i+1) j
   192        in merge (map (fn ks => i::ks) is) is end
   193      else [[]];
   194 
   195 fun cprod ([], ys) = []
   196   | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
   197 
   198 fun cprods xss = foldr (map op :: o cprod) [[]] xss;
   199 
   200 datatype mode = Mode of (int list option list * int list) * int list * mode option list;
   201 
   202 fun modes_of modes t =
   203   let
   204     val ks = 1 upto length (binder_types (fastype_of t));
   205     val default = [Mode (([], ks), ks, [])];
   206     fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) =>
   207         let
   208           val (args1, args2) =
   209             if length args < length iss then
   210               error ("Too few arguments for inductive predicate " ^ name)
   211             else chop (length iss) args;
   212           val k = length args2;
   213           val prfx = 1 upto k
   214         in
   215           if not (is_prefix op = prfx is) then [] else
   216           let val is' = map (fn i => i - k) (List.drop (is, k))
   217           in map (fn x => Mode (m, is', x)) (cprods (map
   218             (fn (NONE, _) => [NONE]
   219               | (SOME js, arg) => map SOME (filter
   220                   (fn Mode (_, js', _) => js=js') (modes_of modes arg)))
   221                     (iss ~~ args1)))
   222           end
   223         end)) (AList.lookup op = modes name)
   224 
   225   in (case strip_comb t of
   226       (Const (name, _), args) => the_default default (mk_modes name args)
   227     | (Var ((name, _), _), args) => the (mk_modes name args)
   228     | (Free (name, _), args) => the (mk_modes name args)
   229     | _ => default)
   230   end
   231 
   232 datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term;
   233 
   234 fun select_mode_prem thy modes vs ps =
   235   find_first (is_some o snd) (ps ~~ map
   236     (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>
   237           let
   238             val (in_ts, out_ts) = get_args is us;
   239             val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
   240             val vTs = maps term_vTs out_ts';
   241             val dupTs = map snd (duplicates (op =) vTs) @
   242               List.mapPartial (AList.lookup (op =) vTs) vs;
   243           in
   244             terms_vs (in_ts @ in_ts') subset vs andalso
   245             forall (is_eqT o fastype_of) in_ts' andalso
   246             term_vs t subset vs andalso
   247             forall is_eqT dupTs
   248           end)
   249             (modes_of modes t handle Option =>
   250                error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   251       | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
   252             length us = length is andalso
   253             terms_vs us subset vs andalso
   254             term_vs t subset vs)
   255             (modes_of modes t handle Option =>
   256                error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
   257       | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
   258           else NONE
   259       ) ps);
   260 
   261 fun check_mode_clause thy param_vs modes (iss, is) (ts, ps) =
   262   let
   263     val modes' = modes @ List.mapPartial
   264       (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
   265         (param_vs ~~ iss); 
   266     fun check_mode_prems vs [] = SOME vs
   267       | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
   268           NONE => NONE
   269         | SOME (x, _) => check_mode_prems
   270             (case x of Prem (us, _) => vs union terms_vs us | _ => vs)
   271             (filter_out (equal x) ps))
   272     val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is ts));
   273     val in_vs = terms_vs in_ts;
   274     val concl_vs = terms_vs ts
   275   in
   276     forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
   277     forall (is_eqT o fastype_of) in_ts' andalso
   278     (case check_mode_prems (param_vs union in_vs) ps of
   279        NONE => false
   280      | SOME vs => concl_vs subset vs)
   281   end;
   282 
   283 fun check_modes_pred thy param_vs preds modes (p, ms) =
   284   let val SOME rs = AList.lookup (op =) preds p
   285   in (p, List.filter (fn m => case find_index
   286     (not o check_mode_clause thy param_vs modes m) rs of
   287       ~1 => true
   288     | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^
   289       p ^ " violates mode " ^ string_of_mode m); false)) ms)
   290   end;
   291 
   292 fun fixp f (x : (string * (int list option list * int list) list) list) =
   293   let val y = f x
   294   in if x = y then x else fixp f y end;
   295 
   296 fun infer_modes thy extra_modes arities param_vs preds = fixp (fn modes =>
   297   map (check_modes_pred thy param_vs preds (modes @ extra_modes)) modes)
   298     (map (fn (s, (ks, k)) => (s, cprod (cprods (map
   299       (fn NONE => [NONE]
   300         | SOME k' => map SOME (subsets 1 k')) ks),
   301       subsets 1 k))) arities);
   302 
   303 
   304 (*****************************************************************************************)
   305 (**** end of old source code *************************************************************)
   306 (*****************************************************************************************)
   307 (**** term construction ****)
   308 
   309 fun mk_eq (x, xs) =
   310   let fun mk_eqs _ [] = []
   311         | mk_eqs a (b::cs) =
   312             HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
   313   in mk_eqs x xs end;
   314 
   315 fun mk_tuple [] = HOLogic.unit
   316   | mk_tuple ts = foldr1 HOLogic.mk_prod ts;
   317 
   318 fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = []
   319   | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)
   320   | dest_tuple t = [t]
   321 
   322 fun mk_tupleT [] = HOLogic.unitT
   323   | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;
   324 
   325 fun mk_pred_enumT T = Type ("Predicate.pred", [T])
   326 
   327 fun dest_pred_enumT (Type ("Predicate.pred", [T])) = T
   328   | dest_pred_enumT T = raise TYPE ("dest_pred_enumT", [T], []);
   329 
   330 fun mk_single t =
   331   let val T = fastype_of t
   332   in Const(@{const_name Predicate.single}, T --> mk_pred_enumT T) $ t end;
   333 
   334 fun mk_empty T = Const (@{const_name Orderings.bot}, mk_pred_enumT T);
   335 
   336 fun mk_if_predenum cond = Const (@{const_name Predicate.if_pred},
   337                           HOLogic.boolT --> mk_pred_enumT HOLogic.unitT) 
   338                          $ cond
   339 
   340 fun mk_not_pred t = let val T = mk_pred_enumT HOLogic.unitT
   341   in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
   342 
   343 fun mk_bind (x, f) =
   344   let val T as Type ("fun", [_, U]) = fastype_of f
   345   in
   346     Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
   347   end;
   348 
   349 fun mk_Enum f =
   350   let val T as Type ("fun", [T', _]) = fastype_of f
   351   in
   352     Const (@{const_name Predicate.Pred}, T --> mk_pred_enumT T') $ f    
   353   end;
   354 
   355 fun mk_Eval (f, x) =
   356   let val T = fastype_of x
   357   in
   358     Const (@{const_name Predicate.eval}, mk_pred_enumT T --> T --> HOLogic.boolT) $ f $ x
   359   end;
   360 
   361 fun mk_Eval' f =
   362   let val T = fastype_of f
   363   in
   364     Const (@{const_name Predicate.eval}, T --> dest_pred_enumT T --> HOLogic.boolT) $ f
   365   end; 
   366 
   367 val mk_sup = HOLogic.mk_binop @{const_name sup};
   368 
   369 (* for simple modes (e.g. parameters) only: better call it param_funT *)
   370 (* or even better: remove it and only use funT'_of - some modifications to funT'_of necessary *) 
   371 fun funT_of T NONE = T
   372   | funT_of T (SOME mode) = let
   373      val Ts = binder_types T;
   374      val (Us1, Us2) = get_args mode Ts
   375    in Us1 ---> (mk_pred_enumT (mk_tupleT Us2)) end;
   376 
   377 fun funT'_of (iss, is) T = let
   378     val Ts = binder_types T
   379     val (paramTs, argTs) = chop (length iss) Ts
   380     val paramTs' = map2 (fn SOME is => funT'_of ([], is) | NONE => I) iss paramTs 
   381     val (inargTs, outargTs) = get_args is argTs
   382   in
   383     (paramTs' @ inargTs) ---> (mk_pred_enumT (mk_tupleT outargTs))
   384   end; 
   385 
   386 
   387 fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of
   388       NONE => ((names, (s, [])::vs), Free (s, T))
   389     | SOME xs =>
   390         let
   391           val s' = Name.variant names s;
   392           val v = Free (s', T)
   393         in
   394           ((s'::names, AList.update (op =) (s, v::xs) vs), v)
   395         end);
   396 
   397 fun distinct_v (nvs, Free (s, T)) = mk_v nvs s T
   398   | distinct_v (nvs, t $ u) =
   399       let
   400         val (nvs', t') = distinct_v (nvs, t);
   401         val (nvs'', u') = distinct_v (nvs', u);
   402       in (nvs'', t' $ u') end
   403   | distinct_v x = x;
   404 
   405 fun compile_match thy eqs eqs' out_ts success_t =
   406   let 
   407     val eqs'' = maps mk_eq eqs @ eqs'
   408     val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
   409     val name = Name.variant names "x";
   410     val name' = Name.variant (name :: names) "y";
   411     val T = mk_tupleT (map fastype_of out_ts);
   412     val U = fastype_of success_t;
   413     val U' = dest_pred_enumT U;
   414     val v = Free (name, T);
   415     val v' = Free (name', T);
   416   in
   417     lambda v (fst (DatatypePackage.make_case
   418       (ProofContext.init thy) false [] v
   419       [(mk_tuple out_ts,
   420         if null eqs'' then success_t
   421         else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
   422           foldr1 HOLogic.mk_conj eqs'' $ success_t $
   423             mk_empty U'),
   424        (v', mk_empty U')]))
   425   end;
   426 
   427 fun modename thy name mode = let
   428     val v = (PredModetab.lookup (#names (IndCodegenData.get thy)) (name, mode))
   429   in if (is_some v) then the v
   430      else error ("fun modename - definition not found: name: " ^ name ^ " mode: " ^  (makestring mode))
   431   end
   432 
   433 (* function can be removed *)
   434 fun mk_funcomp f t =
   435   let
   436     val names = Term.add_free_names t [];
   437     val Ts = binder_types (fastype_of t);
   438     val vs = map Free
   439       (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
   440   in
   441     fold_rev lambda vs (f (list_comb (t, vs)))
   442   end;
   443 
   444 fun compile_param thy modes (NONE, t) = t
   445   | compile_param thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) = let
   446     val (f, args) = strip_comb t
   447     val (params, args') = chop (length ms) args
   448     val params' = map (compile_param thy modes) (ms ~~ params)
   449     val f' = case f of
   450         Const (name, T) =>
   451           if AList.defined op = modes name then
   452             Const (modename thy name (iss, is'), funT'_of (iss, is') T)
   453           else error "compile param: Not an inductive predicate with correct mode"
   454       | Free (name, T) => Free (name, funT_of T (SOME is'))
   455     in list_comb (f', params' @ args') end
   456   | compile_param _ _ _ = error "compile params"
   457 
   458 fun compile_expr thy modes (SOME (Mode (mode, is, ms)), t) =
   459       (case strip_comb t of
   460          (Const (name, T), params) =>
   461            if AList.defined op = modes name then
   462              let
   463                val (Ts, Us) = get_args is
   464                  (curry Library.drop (length ms) (fst (strip_type T)))
   465                val params' = map (compile_param thy modes) (ms ~~ params)
   466                val mode_id = modename thy name mode
   467              in list_comb (Const (mode_id, ((map fastype_of params') @ Ts) --->
   468                mk_pred_enumT (mk_tupleT Us)), params')
   469              end
   470            else error "not a valid inductive expression"
   471        | (Free (name, T), args) =>
   472          (*if name mem param_vs then *)
   473          (* Higher order mode call *)
   474          let val r = Free (name, funT_of T (SOME is))
   475          in list_comb (r, args) end)
   476   | compile_expr _ _ _ = error "not a valid inductive expression"
   477 
   478 
   479 fun compile_clause thy all_vs param_vs modes (iss, is) (ts, ps) inp =
   480   let
   481     val modes' = modes @ List.mapPartial
   482       (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
   483         (param_vs ~~ iss);
   484     fun check_constrt ((names, eqs), t) =
   485       if is_constrt thy t then ((names, eqs), t) else
   486         let
   487           val s = Name.variant names "x";
   488           val v = Free (s, fastype_of t)
   489         in ((s::names, HOLogic.mk_eq (v, t)::eqs), v) end;
   490 
   491     val (in_ts, out_ts) = get_args is ts;
   492     val ((all_vs', eqs), in_ts') =
   493       (*FIXME*) Library.foldl_map check_constrt ((all_vs, []), in_ts);
   494 
   495     fun compile_prems out_ts' vs names [] =
   496           let
   497             val ((names', eqs'), out_ts'') =
   498               (*FIXME*) Library.foldl_map check_constrt ((names, []), out_ts');
   499             val (nvs, out_ts''') = (*FIXME*) Library.foldl_map distinct_v
   500               ((names', map (rpair []) vs), out_ts'');
   501           in
   502             compile_match thy (snd nvs) (eqs @ eqs') out_ts'''
   503               (mk_single (mk_tuple out_ts))
   504           end
   505       | compile_prems out_ts vs names ps =
   506           let
   507             val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
   508             val SOME (p, mode as SOME (Mode (_, js, _))) =
   509               select_mode_prem thy modes' vs' ps
   510             val ps' = filter_out (equal p) ps
   511             val ((names', eqs), out_ts') =
   512               (*FIXME*) Library.foldl_map check_constrt ((names, []), out_ts)
   513             val (nvs, out_ts'') = (*FIXME*) Library.foldl_map distinct_v
   514               ((names', map (rpair []) vs), out_ts')
   515             val (compiled_clause, rest) = case p of
   516                Prem (us, t) =>
   517                  let
   518                    val (in_ts, out_ts''') = get_args js us;
   519                    val u = list_comb (compile_expr thy modes (mode, t), in_ts)
   520                    val rest = compile_prems out_ts''' vs' (fst nvs) ps'
   521                  in
   522                    (u, rest)
   523                  end
   524              | Negprem (us, t) =>
   525                  let
   526                    val (in_ts, out_ts''') = get_args js us
   527                    val u = list_comb (compile_expr thy modes (mode, t), in_ts)
   528                    val rest = compile_prems out_ts''' vs' (fst nvs) ps'
   529                  in
   530                    (mk_not_pred u, rest)
   531                  end
   532              | Sidecond t =>
   533                  let
   534                    val rest = compile_prems [] vs' (fst nvs) ps';
   535                  in
   536                    (mk_if_predenum t, rest)
   537                  end
   538           in
   539             compile_match thy (snd nvs) eqs out_ts'' 
   540               (mk_bind (compiled_clause, rest))
   541           end
   542     val prem_t = compile_prems in_ts' param_vs all_vs' ps;
   543   in
   544     mk_bind (mk_single inp, prem_t)
   545   end
   546 
   547 fun compile_pred thy all_vs param_vs modes s T cls mode =
   548   let
   549     val Ts = binder_types T;
   550     val (Ts1, Ts2) = chop (length param_vs) Ts;
   551     val Ts1' = map2 funT_of Ts1 (fst mode)
   552     val (Us1, Us2) = get_args (snd mode) Ts2;
   553     val xnames = Name.variant_list param_vs
   554       (map (fn i => "x" ^ string_of_int i) (snd mode));
   555     val xs = map2 (fn s => fn T => Free (s, T)) xnames Us1;
   556     val cl_ts =
   557       map (fn cl => compile_clause thy
   558         all_vs param_vs modes mode cl (mk_tuple xs)) cls;
   559     val mode_id = modename thy s mode
   560   in
   561     HOLogic.mk_Trueprop (HOLogic.mk_eq
   562       (list_comb (Const (mode_id, (Ts1' @ Us1) --->
   563            mk_pred_enumT (mk_tupleT Us2)),
   564          map2 (fn s => fn T => Free (s, T)) param_vs Ts1' @ xs),
   565        foldr1 mk_sup cl_ts))
   566   end;
   567 
   568 fun compile_preds thy all_vs param_vs modes preds =
   569   map (fn (s, (T, cls)) =>
   570     map (compile_pred thy all_vs param_vs modes s T cls)
   571       ((the o AList.lookup (op =) modes) s)) preds;
   572 
   573 (* end of term construction ******************************************************)
   574 
   575 (* special setup for simpset *)                  
   576 val HOL_basic_ss' = HOL_basic_ss setSolver 
   577   (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
   578 
   579 
   580 (* misc: constructing and proving tupleE rules ***********************************)
   581 
   582 
   583 (* Creating definitions of functional programs 
   584    and proving intro and elim rules **********************************************) 
   585 
   586 fun is_ind_pred thy c = 
   587   (can (InductivePackage.the_inductive (ProofContext.init thy)) c) orelse
   588   (c mem_string (Symtab.keys (#intro_rules (IndCodegenData.get thy))))
   589 
   590 fun get_name_of_ind_calls_of_clauses thy preds intrs =
   591     fold Term.add_consts intrs [] |> map fst
   592     |> filter_out (member (op =) preds) |> filter (is_ind_pred thy)
   593 
   594 fun print_arities arities = message ("Arities:\n" ^
   595   cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
   596     space_implode " -> " (map
   597       (fn NONE => "X" | SOME k' => string_of_int k')
   598         (ks @ [SOME k]))) arities));
   599 
   600 fun mk_Eval_of ((x, T), NONE) names = (x, names)
   601   | mk_Eval_of ((x, T), SOME mode) names = let
   602   val Ts = binder_types T
   603   val argnames = Name.variant_list names
   604         (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
   605   val args = map Free (argnames ~~ Ts)
   606   val (inargs, outargs) = get_args mode args
   607   val r = mk_Eval (list_comb (x, inargs), mk_tuple outargs)
   608   val t = fold_rev lambda args r 
   609 in
   610   (t, argnames @ names)
   611 end;
   612 
   613 fun create_intro_rule nparams mode defthm mode_id funT pred thy =
   614 let
   615   val Ts = binder_types (fastype_of pred)
   616   val funtrm = Const (mode_id, funT)
   617   val argnames = Name.variant_list []
   618         (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
   619   val (Ts1, Ts2) = chop nparams Ts;
   620   val Ts1' = map2 funT_of Ts1 (fst mode)
   621   val args = map Free (argnames ~~ (Ts1' @ Ts2))
   622   val (params, io_args) = chop nparams args
   623   val (inargs, outargs) = get_args (snd mode) io_args
   624   val (params', names) = fold_map mk_Eval_of ((params ~~ Ts1) ~~ (fst mode)) []
   625   val predprop = HOLogic.mk_Trueprop (list_comb (pred, params' @ io_args))
   626   val funargs = params @ inargs
   627   val funpropE = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs),
   628                   if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs))
   629   val funpropI = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs),
   630                    mk_tuple outargs))
   631   val introtrm = Logic.mk_implies (predprop, funpropI)
   632   val simprules = [defthm, @{thm eval_pred},
   633                    @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}]
   634   val unfolddef_tac = (Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1)
   635   val introthm = Goal.prove (ProofContext.init thy) (argnames @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
   636   val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
   637   val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predprop, P)], P)
   638   val elimthm = Goal.prove (ProofContext.init thy) (argnames @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
   639 in
   640   map_function_intros (Symtab.update_new (mode_id, introthm)) thy
   641   |> map_function_elims (Symtab.update_new (mode_id, elimthm))
   642   |> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "I"), introthm) |> snd
   643   |> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "E"), elimthm)  |> snd
   644 end;
   645 
   646 fun create_definitions preds nparams (name, modes) thy =
   647   let
   648     val _ = tracing "create definitions"
   649     val T = AList.lookup (op =) preds name |> the
   650     fun create_definition mode thy = let
   651       fun string_of_mode mode = if null mode then "0"
   652         else space_implode "_" (map string_of_int mode)
   653       val HOmode = let
   654         fun string_of_HOmode m s = case m of NONE => s | SOME mode => s ^ "__" ^ (string_of_mode mode)    
   655         in (fold string_of_HOmode (fst mode) "") end;
   656       val mode_id = name ^ (if HOmode = "" then "_" else HOmode ^ "___")
   657         ^ (string_of_mode (snd mode))
   658       val Ts = binder_types T;
   659       val (Ts1, Ts2) = chop nparams Ts;
   660       val Ts1' = map2 funT_of Ts1 (fst mode)
   661       val (Us1, Us2) = get_args (snd mode) Ts2;
   662       val names = Name.variant_list []
   663         (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
   664       val xs = map Free (names ~~ (Ts1' @ Ts2));
   665       val (xparams, xargs) = chop nparams xs;
   666       val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ (fst mode)) names
   667       val (xins, xouts) = get_args (snd mode) xargs;
   668       fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
   669        | mk_split_lambda [x] t = lambda x t
   670        | mk_split_lambda xs t = let
   671          fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
   672            | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
   673          in mk_split_lambda' xs t end;
   674       val predterm = mk_Enum (mk_split_lambda xouts (list_comb (Const (name, T), xparams' @ xargs)))
   675       val funT = (Ts1' @ Us1) ---> (mk_pred_enumT (mk_tupleT Us2))
   676       val mode_id = Sign.full_bname thy (Long_Name.base_name mode_id)
   677       val lhs = list_comb (Const (mode_id, funT), xparams @ xins)
   678       val def = Logic.mk_equals (lhs, predterm)
   679       val ([defthm], thy') = thy |>
   680         Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_id), funT, NoSyn)] |>
   681         PureThy.add_defs false [((Binding.name (Long_Name.base_name mode_id ^ "_def"), def), [])]
   682       in thy' |> map_names (PredModetab.update_new ((name, mode), mode_id))
   683            |> map_function_defs (Symtab.update_new (mode_id, defthm))
   684            |> create_intro_rule nparams mode defthm mode_id funT (Const (name, T))
   685       end;
   686   in
   687     fold create_definition modes thy
   688   end;
   689 
   690 (**************************************************************************************)
   691 (* Proving equivalence of term *)
   692 
   693 
   694 fun intro_rule thy pred mode = modename thy pred mode
   695     |> Symtab.lookup (#function_intros (IndCodegenData.get thy)) |> the
   696 
   697 fun elim_rule thy pred mode = modename thy pred mode
   698     |> Symtab.lookup (#function_elims (IndCodegenData.get thy)) |> the
   699 
   700 fun pred_intros thy predname = let
   701     fun is_intro_of pred intro = let
   702       val const = fst (strip_comb (HOLogic.dest_Trueprop (concl_of intro)))
   703     in (fst (dest_Const const) = pred) end;
   704     val d = IndCodegenData.get thy
   705   in
   706     if (Symtab.defined (#intro_rules d) predname) then
   707       rev (Symtab.lookup_list (#intro_rules d) predname)
   708     else
   709       InductivePackage.the_inductive (ProofContext.init thy) predname
   710       |> snd |> #intrs |> filter (is_intro_of predname)
   711   end
   712 
   713 fun function_definition thy pred mode =
   714   modename thy pred mode |> Symtab.lookup (#function_defs (IndCodegenData.get thy)) |> the
   715 
   716 fun is_Type (Type _) = true
   717   | is_Type _ = false
   718 
   719 fun imp_prems_conv cv ct =
   720   case Thm.term_of ct of
   721     Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   722   | _ => Conv.all_conv ct
   723 
   724 fun Trueprop_conv cv ct =
   725   case Thm.term_of ct of
   726     Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
   727   | _ => error "Trueprop_conv"
   728 
   729 fun preprocess_intro thy rule =
   730   Conv.fconv_rule
   731     (imp_prems_conv
   732       (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
   733     (Thm.transfer thy rule)
   734 
   735 fun preprocess_elim thy nargs elimrule = let
   736    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
   737       HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
   738     | replace_eqs t = t
   739    fun preprocess_case t = let
   740      val params = Logic.strip_params t
   741      val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)
   742      val assums_hyp' = assums1 @ (map replace_eqs assums2)
   743      in list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t)) end
   744    val prems = Thm.prems_of elimrule
   745    val cases' = map preprocess_case (tl prems)
   746    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
   747  in
   748    Thm.equal_elim
   749      (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}])
   750         (cterm_of thy elimrule')))
   751      elimrule
   752  end;
   753 
   754 
   755 (* returns true if t is an application of an datatype constructor *)
   756 (* which then consequently would be splitted *)
   757 (* else false *)
   758 fun is_constructor thy t =
   759   if (is_Type (fastype_of t)) then
   760     (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of
   761       NONE => false
   762     | SOME info => (let
   763       val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
   764       val (c, _) = strip_comb t
   765       in (case c of
   766         Const (name, _) => name mem_string constr_consts
   767         | _ => false) end))
   768   else false
   769 
   770 (* MAJOR FIXME:  prove_params should be simple
   771  - different form of introrule for parameters ? *)
   772 fun prove_param thy modes (NONE, t) = all_tac 
   773   | prove_param thy modes (m as SOME (Mode (mode, is, ms)), t) = let
   774     val  (f, args) = strip_comb t
   775     val (params, _) = chop (length ms) args
   776     val f_tac = case f of
   777         Const (name, T) => simp_tac (HOL_basic_ss addsimps 
   778            @{thm eval_pred}::function_definition thy name mode::[]) 1
   779       | Free _ => all_tac
   780   in  
   781     print_tac "before simplification in prove_args:"
   782     THEN debug_tac ("mode" ^ (makestring mode))
   783     THEN f_tac
   784     THEN print_tac "after simplification in prove_args"
   785     (* work with parameter arguments *)
   786     THEN (EVERY (map (prove_param thy modes) (ms ~~ params)))
   787     THEN (REPEAT_DETERM (atac 1))
   788   end
   789 
   790 fun prove_expr thy modes (SOME (Mode (mode, is, ms)), t, us) (premposition : int) =
   791   (case strip_comb t of
   792     (Const (name, T), args) =>
   793       if AList.defined op = modes name then (let
   794           val introrule = intro_rule thy name mode
   795           (*val (in_args, out_args) = get_args is us
   796           val (pred, rargs) = strip_comb (HOLogic.dest_Trueprop
   797             (hd (Logic.strip_imp_prems (prop_of introrule))))
   798           val nparams = length ms (* get_nparams thy (fst (dest_Const pred)) *)
   799           val (_, args) = chop nparams rargs
   800           val _ = tracing ("args: " ^ (makestring args))
   801           val subst = map (pairself (cterm_of thy)) (args ~~ us)
   802           val _ = tracing ("subst: " ^ (makestring subst))
   803           val inst_introrule = Drule.cterm_instantiate subst introrule*)
   804          (* the next line is old and probably wrong *)
   805           val (args1, args2) = chop (length ms) args
   806           val _ = tracing ("premposition: " ^ (makestring premposition))
   807         in
   808         rtac @{thm bindI} 1
   809         THEN print_tac "before intro rule:"
   810         THEN debug_tac ("mode" ^ (makestring mode))
   811         THEN debug_tac (makestring introrule)
   812         THEN debug_tac ("premposition: " ^ (makestring premposition))
   813         (* for the right assumption in first position *)
   814         THEN rotate_tac premposition 1
   815         THEN rtac introrule 1
   816         THEN print_tac "after intro rule"
   817         (* work with parameter arguments *)
   818         THEN (EVERY (map (prove_param thy modes) (ms ~~ args1)))
   819         THEN (REPEAT_DETERM (atac 1)) end)
   820       else error "Prove expr if case not implemented"
   821     | _ => rtac @{thm bindI} 1
   822            THEN atac 1)
   823   | prove_expr _ _ _ _ =  error "Prove expr not implemented"
   824 
   825 fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; 
   826 
   827 fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st
   828 
   829 fun prove_match thy (out_ts : term list) = let
   830   fun get_case_rewrite t =
   831     if (is_constructor thy t) then let
   832       val case_rewrites = (#case_rewrites (DatatypePackage.the_datatype thy
   833         ((fst o dest_Type o fastype_of) t)))
   834       in case_rewrites @ (flat (map get_case_rewrite (snd (strip_comb t)))) end
   835     else []
   836   val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: (flat (map get_case_rewrite out_ts))
   837 (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
   838 in
   839   print_tac ("before prove_match rewriting: simprules = " ^ (makestring simprules))
   840    (* make this simpset better! *)
   841   THEN asm_simp_tac (HOL_basic_ss' addsimps simprules) 1
   842   THEN print_tac "after prove_match:"
   843   THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1
   844          THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss 1))))
   845          THEN (SOLVED (asm_simp_tac HOL_basic_ss 1)))))
   846   THEN print_tac "after if simplification"
   847 end;
   848 
   849 (* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
   850 
   851 fun prove_sidecond thy modes t = let
   852   val _ = tracing ("prove_sidecond:" ^ (makestring t))
   853   fun preds_of t nameTs = case strip_comb t of 
   854     (f as Const (name, T), args) =>
   855       if AList.defined (op =) modes name then (name, T) :: nameTs
   856         else fold preds_of args nameTs
   857     | _ => nameTs
   858   val preds = preds_of t []
   859   
   860   val _ = tracing ("preds: " ^ (makestring preds))
   861   val defs = map
   862     (fn (pred, T) => function_definition thy pred ([], (1 upto (length (binder_types T)))))
   863       preds
   864   val _ = tracing ("defs: " ^ (makestring defs))
   865 in 
   866    (* remove not_False_eq_True when simpset in prove_match is better *)
   867    simp_tac (HOL_basic_ss addsimps @{thm not_False_eq_True} :: @{thm eval_pred} :: defs) 1 
   868    (* need better control here! *)
   869    THEN print_tac "after sidecond simplification"
   870    end
   871 
   872 fun prove_clause thy nargs all_vs param_vs modes (iss, is) (ts, ps) = let
   873   val modes' = modes @ List.mapPartial
   874    (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
   875      (param_vs ~~ iss);
   876   fun check_constrt ((names, eqs), t) =
   877       if is_constrt thy t then ((names, eqs), t) else
   878         let
   879           val s = Name.variant names "x";
   880           val v = Free (s, fastype_of t)
   881         in ((s::names, HOLogic.mk_eq (v, t)::eqs), v) end;
   882   
   883   val (in_ts, clause_out_ts) = get_args is ts;
   884   val ((all_vs', eqs), in_ts') =
   885       (*FIXME*) Library.foldl_map check_constrt ((all_vs, []), in_ts);
   886   fun prove_prems out_ts vs [] =
   887     (prove_match thy out_ts)
   888     THEN asm_simp_tac HOL_basic_ss' 1
   889     THEN print_tac "before the last rule of singleI:"
   890     THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
   891   | prove_prems out_ts vs rps =
   892     let
   893       val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
   894       val SOME (p, mode as SOME (Mode ((iss, js), _, param_modes))) =
   895         select_mode_prem thy modes' vs' rps;
   896       val premposition = (find_index (equal p) ps) + nargs
   897       val rps' = filter_out (equal p) rps;
   898       val rest_tac = (case p of Prem (us, t) =>
   899           let
   900             val (in_ts, out_ts''') = get_args js us
   901             val rec_tac = prove_prems out_ts''' vs' rps'
   902           in
   903             print_tac "before clause:"
   904             THEN asm_simp_tac HOL_basic_ss 1
   905             THEN print_tac "before prove_expr:"
   906             THEN prove_expr thy modes (mode, t, us) premposition
   907             THEN print_tac "after prove_expr:"
   908             THEN rec_tac
   909           end
   910         | Negprem (us, t) =>
   911           let
   912             val (in_ts, out_ts''') = get_args js us
   913             val rec_tac = prove_prems out_ts''' vs' rps'
   914             val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
   915             val (_, params) = strip_comb t
   916           in
   917             print_tac "before negated clause:"
   918             THEN rtac @{thm bindI} 1
   919             THEN (if (is_some name) then
   920                 simp_tac (HOL_basic_ss addsimps [function_definition thy (the name) (iss, js)]) 1
   921                 THEN rtac @{thm not_predI} 1
   922                 THEN print_tac "after neg. intro rule"
   923                 THEN print_tac ("t = " ^ (makestring t))
   924                 (* FIXME: work with parameter arguments *)
   925                 THEN (EVERY (map (prove_param thy modes) (param_modes ~~ params)))
   926               else
   927                 rtac @{thm not_predI'} 1)
   928             THEN (REPEAT_DETERM (atac 1))
   929             THEN rec_tac
   930           end
   931         | Sidecond t =>
   932          rtac @{thm bindI} 1
   933          THEN rtac @{thm if_predI} 1
   934          THEN print_tac "before sidecond:"
   935          THEN prove_sidecond thy modes t
   936          THEN print_tac "after sidecond:"
   937          THEN prove_prems [] vs' rps')
   938     in (prove_match thy out_ts)
   939         THEN rest_tac
   940     end;
   941   val prems_tac = prove_prems in_ts' param_vs ps
   942 in
   943   rtac @{thm bindI} 1
   944   THEN rtac @{thm singleI} 1
   945   THEN prems_tac
   946 end;
   947 
   948 fun select_sup 1 1 = []
   949   | select_sup _ 1 = [rtac @{thm supI1}]
   950   | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
   951 
   952 fun get_nparams thy s = let
   953     val _ = tracing ("get_nparams: " ^ s)
   954   in
   955   if Symtab.defined (#nparams (IndCodegenData.get thy)) s then
   956     the (Symtab.lookup (#nparams (IndCodegenData.get thy)) s) 
   957   else
   958     case try (InductivePackage.the_inductive (ProofContext.init thy)) s of
   959       SOME info => info |> snd |> #raw_induct |> Thm.unvarify
   960         |> InductivePackage.params_of |> length
   961     | NONE => 0 (* default value *)
   962   end
   963 
   964 val ind_set_codegen_preproc = InductiveSetPackage.codegen_preproc;
   965 
   966 fun pred_elim thy predname =
   967   if (Symtab.defined (#elim_rules (IndCodegenData.get thy)) predname) then
   968     the (Symtab.lookup (#elim_rules (IndCodegenData.get thy)) predname)
   969   else
   970     (let
   971       val ind_result = InductivePackage.the_inductive (ProofContext.init thy) predname
   972       val index = find_index (fn s => s = predname) (#names (fst ind_result))
   973     in nth (#elims (snd ind_result)) index end)
   974 
   975 fun prove_one_direction thy all_vs param_vs modes clauses ((pred, T), mode) = let
   976   val elim_rule = the (Symtab.lookup (#function_elims (IndCodegenData.get thy)) (modename thy pred mode))
   977 (*  val ind_result = InductivePackage.the_inductive (ProofContext.init thy) pred
   978   val index = find_index (fn s => s = pred) (#names (fst ind_result))
   979   val (_, T) = dest_Const (nth (#preds (snd ind_result)) index) *)
   980   val nargs = length (binder_types T) - get_nparams thy pred
   981   val pred_case_rule = singleton (ind_set_codegen_preproc thy)
   982     (preprocess_elim thy nargs (pred_elim thy pred))
   983   (* FIXME preprocessor |> Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}])*)
   984   val _ = tracing ("pred_case_rule " ^ (makestring pred_case_rule))
   985 in
   986   REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
   987   THEN etac elim_rule 1
   988   THEN etac pred_case_rule 1
   989   THEN (EVERY (map
   990          (fn i => EVERY' (select_sup (length clauses) i) i) 
   991            (1 upto (length clauses))))
   992   THEN (EVERY (map (prove_clause thy nargs all_vs param_vs modes mode) clauses))
   993 end;
   994 
   995 (*******************************************************************************************************)
   996 (* Proof in the other direction ************************************************************************)
   997 (*******************************************************************************************************)
   998 
   999 fun prove_match2 thy out_ts = let
  1000   fun split_term_tac (Free _) = all_tac
  1001     | split_term_tac t =
  1002       if (is_constructor thy t) then let
  1003         val info = DatatypePackage.the_datatype thy ((fst o dest_Type o fastype_of) t)
  1004         val num_of_constrs = length (#case_rewrites info)
  1005         (* special treatment of pairs -- because of fishing *)
  1006         val split_rules = case (fst o dest_Type o fastype_of) t of
  1007           "*" => [@{thm prod.split_asm}] 
  1008           | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm")
  1009         val (_, ts) = strip_comb t
  1010       in
  1011         print_tac ("splitting with t = " ^ (makestring t))
  1012         THEN (Splitter.split_asm_tac split_rules 1)
  1013 (*        THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
  1014           THEN (DETERM (TRY (etac @{thm Pair_inject} 1))) *)
  1015         THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))
  1016         THEN (EVERY (map split_term_tac ts))
  1017       end
  1018     else all_tac
  1019   in
  1020     split_term_tac (mk_tuple out_ts)
  1021     THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2))))
  1022   end
  1023 
  1024 (* VERY LARGE SIMILIRATIY to function prove_param 
  1025 -- join both functions
  1026 *) 
  1027 fun prove_param2 thy modes (NONE, t) = all_tac 
  1028   | prove_param2 thy modes (m as SOME (Mode (mode, is, ms)), t) = let
  1029     val  (f, args) = strip_comb t
  1030     val (params, _) = chop (length ms) args
  1031     val f_tac = case f of
  1032         Const (name, T) => full_simp_tac (HOL_basic_ss addsimps 
  1033            @{thm eval_pred}::function_definition thy name mode::[]) 1
  1034       | Free _ => all_tac
  1035   in  
  1036     print_tac "before simplification in prove_args:"
  1037     THEN debug_tac ("function : " ^ (makestring f) ^ " - mode" ^ (makestring mode))
  1038     THEN f_tac
  1039     THEN print_tac "after simplification in prove_args"
  1040     (* work with parameter arguments *)
  1041     THEN (EVERY (map (prove_param2 thy modes) (ms ~~ params)))
  1042   end
  1043 
  1044 fun prove_expr2 thy modes (SOME (Mode (mode, is, ms)), t) = 
  1045   (case strip_comb t of
  1046     (Const (name, T), args) =>
  1047       if AList.defined op = modes name then
  1048         etac @{thm bindE} 1
  1049         THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
  1050         THEN (etac (elim_rule thy name mode) 1)
  1051         THEN (EVERY (map (prove_param2 thy modes) (ms ~~ args)))
  1052       else error "Prove expr2 if case not implemented"
  1053     | _ => etac @{thm bindE} 1)
  1054   | prove_expr2 _ _ _ = error "Prove expr2 not implemented"
  1055 
  1056 fun prove_sidecond2 thy modes t = let
  1057   val _ = tracing ("prove_sidecond:" ^ (makestring t))
  1058   fun preds_of t nameTs = case strip_comb t of 
  1059     (f as Const (name, T), args) =>
  1060       if AList.defined (op =) modes name then (name, T) :: nameTs
  1061         else fold preds_of args nameTs
  1062     | _ => nameTs
  1063   val preds = preds_of t []
  1064   val _ = tracing ("preds: " ^ (makestring preds))
  1065   val defs = map
  1066     (fn (pred, T) => function_definition thy pred ([], (1 upto (length (binder_types T)))))
  1067       preds
  1068   in
  1069    (* only simplify the one assumption *)
  1070    full_simp_tac (HOL_basic_ss' addsimps @{thm eval_pred} :: defs) 1 
  1071    (* need better control here! *)
  1072    THEN print_tac "after sidecond2 simplification"
  1073    end
  1074   
  1075 fun prove_clause2 thy all_vs param_vs modes (iss, is) (ts, ps) pred i = let
  1076   val modes' = modes @ List.mapPartial
  1077    (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
  1078      (param_vs ~~ iss);
  1079   fun check_constrt ((names, eqs), t) =
  1080       if is_constrt thy t then ((names, eqs), t) else
  1081         let
  1082           val s = Name.variant names "x";
  1083           val v = Free (s, fastype_of t)
  1084         in ((s::names, HOLogic.mk_eq (v, t)::eqs), v) end;
  1085   val pred_intro_rule = nth (pred_intros thy pred) (i - 1)
  1086     |> preprocess_intro thy
  1087     |> (fn thm => hd (ind_set_codegen_preproc thy [thm]))
  1088     (* FIXME preprocess |> Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}]) *)
  1089   val (in_ts, clause_out_ts) = get_args is ts;
  1090   val ((all_vs', eqs), in_ts') =
  1091       (*FIXME*) Library.foldl_map check_constrt ((all_vs, []), in_ts);
  1092   fun prove_prems2 out_ts vs [] =
  1093     print_tac "before prove_match2 - last call:"
  1094     THEN prove_match2 thy out_ts
  1095     THEN print_tac "after prove_match2 - last call:"
  1096     THEN (etac @{thm singleE} 1)
  1097     THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
  1098     THEN (asm_full_simp_tac HOL_basic_ss' 1)
  1099     THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
  1100     THEN (asm_full_simp_tac HOL_basic_ss' 1)
  1101     THEN SOLVED (print_tac "state before applying intro rule:"
  1102       THEN (rtac pred_intro_rule 1)
  1103       (* How to handle equality correctly? *)
  1104       THEN (print_tac "state before assumption matching")
  1105       THEN (REPEAT (atac 1 ORELSE 
  1106          (CHANGED (asm_full_simp_tac HOL_basic_ss' 1)
  1107           THEN print_tac "state after simp_tac:"))))
  1108   | prove_prems2 out_ts vs ps = let
  1109       val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
  1110       val SOME (p, mode as SOME (Mode ((iss, js), _, param_modes))) =
  1111         select_mode_prem thy modes' vs' ps;
  1112       val ps' = filter_out (equal p) ps;
  1113       val rest_tac = (case p of Prem (us, t) =>
  1114           let
  1115             val (in_ts, out_ts''') = get_args js us
  1116             val rec_tac = prove_prems2 out_ts''' vs' ps'
  1117           in
  1118             (prove_expr2 thy modes (mode, t)) THEN rec_tac
  1119           end
  1120         | Negprem (us, t) =>
  1121           let
  1122             val (in_ts, out_ts''') = get_args js us
  1123             val rec_tac = prove_prems2 out_ts''' vs' ps'
  1124             val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
  1125             val (_, params) = strip_comb t
  1126           in
  1127             print_tac "before neg prem 2"
  1128             THEN etac @{thm bindE} 1
  1129             THEN (if is_some name then
  1130                 full_simp_tac (HOL_basic_ss addsimps [function_definition thy (the name) (iss, js)]) 1 
  1131                 THEN etac @{thm not_predE} 1
  1132                 THEN (EVERY (map (prove_param2 thy modes) (param_modes ~~ params)))
  1133               else
  1134                 etac @{thm not_predE'} 1)
  1135             THEN rec_tac
  1136           end 
  1137         | Sidecond t =>
  1138             etac @{thm bindE} 1
  1139             THEN etac @{thm if_predE} 1
  1140             THEN prove_sidecond2 thy modes t 
  1141             THEN prove_prems2 [] vs' ps')
  1142     in print_tac "before prove_match2:"
  1143        THEN prove_match2 thy out_ts
  1144        THEN print_tac "after prove_match2:"
  1145        THEN rest_tac
  1146     end;
  1147   val prems_tac = prove_prems2 in_ts' param_vs ps 
  1148 in
  1149   print_tac "starting prove_clause2"
  1150   THEN etac @{thm bindE} 1
  1151   THEN (etac @{thm singleE'} 1)
  1152   THEN (TRY (etac @{thm Pair_inject} 1))
  1153   THEN print_tac "after singleE':"
  1154   THEN prems_tac
  1155 end;
  1156  
  1157 fun prove_other_direction thy all_vs param_vs modes clauses (pred, mode) = let
  1158   fun prove_clause (clause, i) =
  1159     (if i < length clauses then etac @{thm supE} 1 else all_tac)
  1160     THEN (prove_clause2 thy all_vs param_vs modes mode clause pred i)
  1161 in
  1162   (DETERM (TRY (rtac @{thm unit.induct} 1)))
  1163    THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
  1164    THEN (rtac (intro_rule thy pred mode) 1)
  1165    THEN (EVERY (map prove_clause (clauses ~~ (1 upto (length clauses)))))
  1166 end;
  1167 
  1168 fun prove_pred thy all_vs param_vs modes clauses (((pred, T), mode), t) = let
  1169   val ctxt = ProofContext.init thy
  1170   val clauses' = the (AList.lookup (op =) clauses pred)
  1171 in
  1172   Goal.prove ctxt (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) t []) [] t
  1173     (if !do_proofs then
  1174       (fn _ =>
  1175       rtac @{thm pred_iffI} 1
  1176       THEN prove_one_direction thy all_vs param_vs modes clauses' ((pred, T), mode)
  1177       THEN print_tac "proved one direction"
  1178       THEN prove_other_direction thy all_vs param_vs modes clauses' (pred, mode)
  1179       THEN print_tac "proved other direction")
  1180      else (fn _ => mycheat_tac thy 1))
  1181 end;
  1182 
  1183 fun prove_preds thy all_vs param_vs modes clauses pmts =
  1184   map (prove_pred thy all_vs param_vs modes clauses) pmts
  1185 
  1186 (* look for other place where this functionality was used before *)
  1187 fun strip_intro_concl intro nparams = let
  1188   val _ $ u = Logic.strip_imp_concl intro
  1189   val (pred, all_args) = strip_comb u
  1190   val (params, args) = chop nparams all_args
  1191 in (pred, (params, args)) end
  1192 
  1193 (* setup for alternative introduction and elimination rules *)
  1194 
  1195 fun add_intro_thm thm thy = let
  1196    val (pred, _) = dest_Const (fst (strip_intro_concl (prop_of thm) 0))
  1197  in map_intro_rules (Symtab.insert_list Thm.eq_thm (pred, thm)) thy end
  1198 
  1199 fun add_elim_thm thm thy = let
  1200     val (pred, _) = dest_Const (fst 
  1201       (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
  1202   in map_elim_rules (Symtab.update (pred, thm)) thy end
  1203 
  1204 
  1205 (* special case: inductive predicate with no clauses *)
  1206 fun noclause (predname, T) thy = let
  1207   val Ts = binder_types T
  1208   val names = Name.variant_list []
  1209         (map (fn i => "x" ^ (string_of_int i)) (1 upto (length Ts)))
  1210   val vs = map Free (names ~~ Ts)
  1211   val clausehd =  HOLogic.mk_Trueprop (list_comb(Const (predname, T), vs))
  1212   val intro_t = Logic.mk_implies (@{prop False}, clausehd)
  1213   val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))
  1214   val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P)
  1215   val intro_thm = Goal.prove (ProofContext.init thy) names [] intro_t
  1216         (fn {...} => etac @{thm FalseE} 1)
  1217   val elim_thm = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t
  1218         (fn {...} => etac (pred_elim thy predname) 1) 
  1219 in
  1220   add_intro_thm intro_thm thy
  1221   |> add_elim_thm elim_thm
  1222 end
  1223 
  1224 (*************************************************************************************)
  1225 (* main function *********************************************************************)
  1226 (*************************************************************************************)
  1227 
  1228 fun create_def_equation' ind_name (mode : (int list option list * int list) option) thy =
  1229 let
  1230   val _ = tracing ("starting create_def_equation' with " ^ ind_name)
  1231   val (prednames, preds) = 
  1232     case (try (InductivePackage.the_inductive (ProofContext.init thy)) ind_name) of
  1233       SOME info => let val preds = info |> snd |> #preds
  1234         in (map (fst o dest_Const) preds, map ((apsnd Logic.unvarifyT) o dest_Const) preds) end
  1235     | NONE => let
  1236         val pred = Symtab.lookup (#intro_rules (IndCodegenData.get thy)) ind_name
  1237           |> the |> hd |> prop_of
  1238           |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> strip_comb
  1239           |> fst |>  dest_Const |> apsnd Logic.unvarifyT
  1240        in ([ind_name], [pred]) end
  1241   val thy' = fold (fn pred as (predname, T) => fn thy =>
  1242     if null (pred_intros thy predname) then noclause pred thy else thy) preds thy
  1243   val intrs = map (preprocess_intro thy') (maps (pred_intros thy') prednames)
  1244     |> ind_set_codegen_preproc thy' (*FIXME preprocessor
  1245     |> map (Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}]))*)
  1246     |> map (Logic.unvarify o prop_of)
  1247   val _ = tracing ("preprocessed intro rules:" ^ (makestring (map (cterm_of thy') intrs)))
  1248   val name_of_calls = get_name_of_ind_calls_of_clauses thy' prednames intrs 
  1249   val _ = tracing ("calling preds: " ^ makestring name_of_calls)
  1250   val _ = tracing "starting recursive compilations"
  1251   fun rec_call name thy = 
  1252     if not (name mem (Symtab.keys (#modes (IndCodegenData.get thy)))) then
  1253       create_def_equation name thy else thy
  1254   val thy'' = fold rec_call name_of_calls thy'
  1255   val _ = tracing "returning from recursive calls"
  1256   val _ = tracing "starting mode inference"
  1257   val extra_modes = Symtab.dest (#modes (IndCodegenData.get thy''))
  1258   val nparams = get_nparams thy'' ind_name
  1259   val _ $ u = Logic.strip_imp_concl (hd intrs);
  1260   val params = List.take (snd (strip_comb u), nparams);
  1261   val param_vs = maps term_vs params
  1262   val all_vs = terms_vs intrs
  1263   fun dest_prem t =
  1264       (case strip_comb t of
  1265         (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t
  1266       | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem t of
  1267           Prem (ts, t) => Negprem (ts, t)
  1268         | Negprem _ => error ("Double negation not allowed in premise: " ^ (makestring (c $ t))) 
  1269         | Sidecond t => Sidecond (c $ t))
  1270       | (c as Const (s, _), ts) =>
  1271         if is_ind_pred thy'' s then
  1272           let val (ts1, ts2) = chop (get_nparams thy'' s) ts
  1273           in Prem (ts2, list_comb (c, ts1)) end
  1274         else Sidecond t
  1275       | _ => Sidecond t)
  1276   fun add_clause intr (clauses, arities) =
  1277   let
  1278     val _ $ t = Logic.strip_imp_concl intr;
  1279     val (Const (name, T), ts) = strip_comb t;
  1280     val (ts1, ts2) = chop nparams ts;
  1281     val prems = map (dest_prem o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr);
  1282     val (Ts, Us) = chop nparams (binder_types T)
  1283   in
  1284     (AList.update op = (name, these (AList.lookup op = clauses name) @
  1285       [(ts2, prems)]) clauses,
  1286      AList.update op = (name, (map (fn U => (case strip_type U of
  1287                  (Rs as _ :: _, Type ("bool", [])) => SOME (length Rs)
  1288                | _ => NONE)) Ts,
  1289              length Us)) arities)
  1290   end;
  1291   val (clauses, arities) = fold add_clause intrs ([], []);
  1292   val modes = infer_modes thy'' extra_modes arities param_vs clauses
  1293   val _ = print_arities arities;
  1294   val _ = print_modes modes;
  1295   val modes = if (is_some mode) then AList.update (op =) (ind_name, [the mode]) modes else modes
  1296   val _ = print_modes modes
  1297   val thy''' = fold (create_definitions preds nparams) modes thy''
  1298     |> map_modes (fold Symtab.update_new modes)
  1299   val clauses' = map (fn (s, cls) => (s, (the (AList.lookup (op =) preds s), cls))) clauses
  1300   val _ = tracing "compiling predicates..."
  1301   val ts = compile_preds thy''' all_vs param_vs (extra_modes @ modes) clauses'
  1302   val _ = tracing "returned term from compile_preds"
  1303   val pred_mode = maps (fn (s, (T, _)) => map (pair (s, T)) ((the o AList.lookup (op =) modes) s)) clauses'
  1304   val _ = tracing "starting proof"
  1305   val result_thms = prove_preds thy''' all_vs param_vs (extra_modes @ modes) clauses (pred_mode ~~ (flat ts))
  1306   val (_, thy'''') = yield_singleton PureThy.add_thmss
  1307     ((Binding.name (Long_Name.base_name ind_name ^ "_codegen" (*FIXME other suffix*)), result_thms),
  1308       [Attrib.attribute_i thy''' Code.add_default_eqn_attrib]) thy'''
  1309 in
  1310   thy''''
  1311 end
  1312 and create_def_equation ind_name thy = create_def_equation' ind_name NONE thy
  1313 
  1314 fun set_nparams (pred, nparams) thy = map_nparams (Symtab.update (pred, nparams)) thy
  1315 
  1316 fun print_alternative_rules thy = let
  1317     val d = IndCodegenData.get thy
  1318     val preds = (Symtab.keys (#intro_rules d)) union (Symtab.keys (#elim_rules d))
  1319     val _ = tracing ("preds: " ^ (makestring preds))
  1320     fun print pred = let
  1321       val _ = tracing ("predicate: " ^ pred)
  1322       val _ = tracing ("introrules: ")
  1323       val _ = fold (fn thm => fn u => tracing (makestring thm))
  1324         (rev (Symtab.lookup_list (#intro_rules d) pred)) ()
  1325       val _ = tracing ("casesrule: ")
  1326       val _ = tracing (makestring (Symtab.lookup (#elim_rules d) pred))
  1327     in () end
  1328     val _ = map print preds
  1329  in thy end; 
  1330   
  1331 fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I)
  1332 
  1333 val code_ind_intros_attrib = attrib add_intro_thm
  1334 
  1335 val code_ind_cases_attrib = attrib add_elim_thm
  1336 
  1337 val setup =
  1338   Attrib.setup @{binding code_ind_intros} (Scan.succeed code_ind_intros_attrib)
  1339     "adding alternative introduction rules for code generation of inductive predicates" #>
  1340   Attrib.setup @{binding code_ind_cases} (Scan.succeed code_ind_cases_attrib)
  1341     "adding alternative elimination rules for code generation of inductive predicates";
  1342 
  1343 end;
  1344 
  1345 fun pred_compile name thy = Predicate_Compile.create_def_equation
  1346   (Sign.intern_const thy name) thy;