wneuper/isa: src/HOL/ex/predicate_compile.ML@7173bf123335

     1 (* Author: Lukas Bulwahn

     3 (Prototype of) A compiler from predicates specified by intro/elim rules

     4 to equations.

     5 *)

     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;

    21 structure Predicate_Compile: PREDICATE_COMPILE =

    22 struct

    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)))

    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 );

    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

    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

    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

    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

    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

   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

   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

   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

   118 (* Debug stuff and tactics ***********************************************************)

   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);

   123 fun debug_tac msg = (fn st =>

   124      (tracing msg; Seq.single st));

   126 (* removes first subgoal *)

   127 fun mycheat_tac thy i st =

   128   (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st

   130 val (do_proofs : bool ref) = ref true;

   132 (* Lightweight mode analysis **********************************************)

   134 (* Hack for message from old code generator *)

   135 val message = tracing;

   138 (**************************************************************************)

   139 (* source code from old code generator ************************************)

   141 (**** check if a term contains only constructor functions ****)

   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;

   156 (**** check if a type is an equality type (i.e. doesn't contain fun) ****)

   158 fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts

   159   | is_eqT _ = true;

   161 (**** mode inference ****)

   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]));

   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));

   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;

   175 (** collect all Frees in a term (with duplicates!) **)

   176 fun term_vTs tm =

   177   fold_aterms (fn Free xT => cons xT | _ => I) tm [];

   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

   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;

   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 [[]];

   195 fun cprod ([], ys) = []

   196   | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);

   198 fun cprods xss = foldr (map op :: o cprod) [[]] xss;

   200 datatype mode = Mode of (int list option list * int list) * int list * mode option list;

   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)

   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

   232 datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term;

   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);

   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;

   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;

   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;

   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);

   304 (*****************************************************************************************)

   305 (**** end of old source code *************************************************************)

   306 (*****************************************************************************************)

   307 (**** term construction ****)

   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;

   315 fun mk_tuple [] = HOLogic.unit

   316   | mk_tuple ts = foldr1 HOLogic.mk_prod ts;

   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]

   322 fun mk_tupleT [] = HOLogic.unitT

   323   | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;

   325 fun mk_pred_enumT T = Type ("Predicate.pred", [T])

   327 fun dest_pred_enumT (Type ("Predicate.pred", [T])) = T

   328   | dest_pred_enumT T = raise TYPE ("dest_pred_enumT", [T], []);

   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;

   334 fun mk_empty T = Const (@{const_name Orderings.bot}, mk_pred_enumT T);

   336 fun mk_if_predenum cond = Const (@{const_name Predicate.if_pred},

   337                           HOLogic.boolT --> mk_pred_enumT HOLogic.unitT)

   338                          $ cond

   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

   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;

   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;

   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;

   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;

   367 val mk_sup = HOLogic.mk_binop @{const_name sup};

   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;

   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;

   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);

   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;

   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;

   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

   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;

   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"

   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"

   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;

   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);

   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

   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;

   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;

   573 (* end of term construction ******************************************************)

   575 (* special setup for simpset *)

   576 val HOL_basic_ss' = HOL_basic_ss setSolver

   577   (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))

   580 (* misc: constructing and proving tupleE rules ***********************************)

   583 (* Creating definitions of functional programs

   584    and proving intro and elim rules **********************************************)

   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))))

   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)

   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));

   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;

   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;

   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;

   690 (**************************************************************************************)

   691 (* Proving equivalence of term *)

   694 fun intro_rule thy pred mode = modename thy pred mode

   695     |> Symtab.lookup (#function_intros (IndCodegenData.get thy)) |> the

   697 fun elim_rule thy pred mode = modename thy pred mode

   698     |> Symtab.lookup (#function_elims (IndCodegenData.get thy)) |> the

   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

   713 fun function_definition thy pred mode =

   714   modename thy pred mode |> Symtab.lookup (#function_defs (IndCodegenData.get thy)) |> the

   716 fun is_Type (Type _) = true

   717   | is_Type _ = false

   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

   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"

   729 fun preprocess_intro thy rule = Thm.transfer thy rule (*FIXME preprocessor

   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) *)

   735 fun preprocess_elim thy nargs elimrule = (*FIXME preprocessor -- 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*) elimrule;

   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

   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

   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"

   825 fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;

   827 fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st

   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;

   849 (* corresponds to compile_fun -- maybe call that also compile_sidecond? *)

   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 []

   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

   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;

   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;

   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));

   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

   964 val ind_set_codegen_preproc = InductiveSetPackage.codegen_preproc;

   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)

   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;

   995 (*******************************************************************************************************)

   996 (* Proof in the other direction ************************************************************************)

   997 (*******************************************************************************************************)

   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

  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

  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"

  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

  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;

  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;

  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;

  1183 fun prove_preds thy all_vs param_vs modes clauses pmts =

  1184   map (prove_pred thy all_vs param_vs modes clauses) pmts

  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

  1193 (* setup for alternative introduction and elimination rules *)

  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

  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

  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

  1224 (*************************************************************************************)

  1225 (* main function *********************************************************************)

  1226 (*************************************************************************************)

  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

  1314 fun set_nparams (pred, nparams) thy = map_nparams (Symtab.update (pred, nparams)) thy

  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;

  1331 fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I)

  1333 val code_ind_intros_attrib = attrib add_intro_thm

  1335 val code_ind_cases_attrib = attrib add_elim_thm

  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";

  1343 end;

  1345 fun pred_compile name thy = Predicate_Compile.create_def_equation

  1346   (Sign.intern_const thy name) thy;

author	wenzelm
	Sun, 15 Mar 2009 15:59:44 +0100
changeset 30530	7173bf123335
parent 30384	0affb9975547
child 30972	5b65835ccc92
child 31105	95f66b234086
permissions	-rw-r--r--