added first prototype of the extended predicate compiler
authorbulwahn
Wed Sep 23 16:20:12 2009 +0200 (2009-09-23)
changeset 32668b2de45007537
parent 32667 09546e654222
child 32669 462b1dd67a58
added first prototype of the extended predicate compiler
src/HOL/HOL.thy
src/HOL/Predicate.thy
src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML
src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML
src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML
src/HOL/Tools/Predicate_Compile/pred_compile_set.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/ex/Predicate_Compile.thy
src/HOL/ex/Predicate_Compile_ex.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -2023,7 +2023,27 @@
     1.4  
     1.5  subsection {* Preprocessing for the predicate compiler *}
     1.6  
     1.7 -setup {* Predicate_Compile_Preproc_Const_Defs.setup *}
     1.8 +ML {*
     1.9 +structure Predicate_Compile_Alternative_Defs = Named_Thms
    1.10 +(
    1.11 +  val name = "code_pred_def"
    1.12 +  val description = "alternative definitions of constants for the Predicate Compiler"
    1.13 +)
    1.14 +*}
    1.15 +
    1.16 +ML {*
    1.17 +structure Predicate_Compile_Inline_Defs = Named_Thms
    1.18 +(
    1.19 +  val name = "code_pred_inline"
    1.20 +  val description = "inlining definitions for the Predicate Compiler"
    1.21 +)
    1.22 +*}
    1.23 +
    1.24 +setup {*
    1.25 +  Predicate_Compile_Alternative_Defs.setup
    1.26 +  #> Predicate_Compile_Inline_Defs.setup
    1.27 +  #> Predicate_Compile_Preproc_Const_Defs.setup
    1.28 +*}
    1.29  
    1.30  subsection {* Nitpick setup *}
    1.31  
     2.1 --- a/src/HOL/Predicate.thy	Wed Sep 23 16:20:12 2009 +0200
     2.2 +++ b/src/HOL/Predicate.thy	Wed Sep 23 16:20:12 2009 +0200
     2.3 @@ -797,6 +797,10 @@
     2.4     (auto simp add: Seq_def the_only_singleton is_empty_def
     2.5        null_is_empty singleton_bot singleton_single singleton_sup Let_def)
     2.6  
     2.7 +lemma meta_fun_cong:
     2.8 +"f == g ==> f x == g x"
     2.9 +by simp
    2.10 +
    2.11  ML {*
    2.12  signature PREDICATE =
    2.13  sig
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Wed Sep 23 16:20:12 2009 +0200
     3.3 @@ -0,0 +1,100 @@
     3.4 +(* Author: Lukas Bulwahn, TU Muenchen
     3.5 +
     3.6 +Auxilary functions for predicate compiler
     3.7 +*)
     3.8 +
     3.9 +structure Predicate_Compile_Aux =
    3.10 +struct
    3.11 +
    3.12 +(* syntactic functions *)
    3.13 + 
    3.14 +fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
    3.15 +  | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
    3.16 +  | is_equationlike_term _ = false
    3.17 +  
    3.18 +val is_equationlike = is_equationlike_term o prop_of 
    3.19 +
    3.20 +fun is_pred_equation_term (Const ("==", _) $ u $ v) =
    3.21 +  (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
    3.22 +  | is_pred_equation_term _ = false
    3.23 +  
    3.24 +val is_pred_equation = is_pred_equation_term o prop_of 
    3.25 +
    3.26 +fun is_intro_term constname t =
    3.27 +  case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
    3.28 +    Const (c, _) => c = constname
    3.29 +  | _ => false
    3.30 +  
    3.31 +fun is_intro constname t = is_intro_term constname (prop_of t)
    3.32 +
    3.33 +fun is_pred thy constname =
    3.34 +  let
    3.35 +    val T = (Sign.the_const_type thy constname)
    3.36 +  in body_type T = @{typ "bool"} end;
    3.37 +  
    3.38 +
    3.39 +fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
    3.40 +  | is_predT _ = false
    3.41 +
    3.42 +  
    3.43 +(*** check if a term contains only constructor functions ***)
    3.44 +fun is_constrt thy =
    3.45 +  let
    3.46 +    val cnstrs = flat (maps
    3.47 +      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
    3.48 +      (Symtab.dest (Datatype.get_all thy)));
    3.49 +    fun check t = (case strip_comb t of
    3.50 +        (Free _, []) => true
    3.51 +      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
    3.52 +            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
    3.53 +          | _ => false)
    3.54 +      | _ => false)
    3.55 +  in check end;  
    3.56 +  
    3.57 +fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
    3.58 +  let
    3.59 +    val (xTs, t') = strip_ex t
    3.60 +  in
    3.61 +    ((x, T) :: xTs, t')
    3.62 +  end
    3.63 +  | strip_ex t = ([], t)
    3.64 +
    3.65 +fun focus_ex t nctxt =
    3.66 +  let
    3.67 +    val ((xs, Ts), t') = apfst split_list (strip_ex t) 
    3.68 +    val (xs', nctxt') = Name.variants xs nctxt;
    3.69 +    val ps' = xs' ~~ Ts;
    3.70 +    val vs = map Free ps';
    3.71 +    val t'' = Term.subst_bounds (rev vs, t');
    3.72 +  in ((ps', t''), nctxt') end;
    3.73 +
    3.74 +
    3.75 +
    3.76 +
    3.77 +(*
    3.78 +fun map_atoms f intro = 
    3.79 +fun fold_atoms f intro =
    3.80 +*)
    3.81 +fun fold_map_atoms f intro s =
    3.82 +  let
    3.83 +    val (literals, head) = Logic.strip_horn intro
    3.84 +    fun appl t s = (case t of
    3.85 +      (@{term "Not"} $ t') =>
    3.86 +        let
    3.87 +          val (t'', s') = f t' s
    3.88 +        in (@{term "Not"} $ t'', s') end
    3.89 +      | _ => f t s)
    3.90 +    val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
    3.91 +  in
    3.92 +    (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
    3.93 +  end;
    3.94 +  
    3.95 +(*
    3.96 +fun equals_conv lhs_cv rhs_cv ct =
    3.97 +  case Thm.term_of ct of
    3.98 +    Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct  
    3.99 +  | _ => error "equals_conv"  
   3.100 +*)
   3.101 +
   3.102 +
   3.103 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Wed Sep 23 16:20:12 2009 +0200
     4.3 @@ -0,0 +1,215 @@
     4.4 +(* Author: Lukas Bulwahn, TU Muenchen
     4.5 +
     4.6 +Book-keeping datastructure for the predicate compiler
     4.7 +
     4.8 +*)
     4.9 +signature PRED_COMPILE_DATA =
    4.10 +sig
    4.11 +  type specification_table;
    4.12 +  val make_const_spec_table : theory -> specification_table
    4.13 +  val get_specification :  specification_table -> string -> thm list
    4.14 +  val obtain_specification_graph : specification_table -> string -> thm list Graph.T
    4.15 +  val normalize_equation : theory -> thm -> thm
    4.16 +end;
    4.17 +
    4.18 +structure Pred_Compile_Data : PRED_COMPILE_DATA =
    4.19 +struct
    4.20 +
    4.21 +open Predicate_Compile_Aux;
    4.22 +
    4.23 +structure Data = TheoryDataFun
    4.24 +(
    4.25 +  type T =
    4.26 +    {const_spec_table : thm list Symtab.table};
    4.27 +  val empty =
    4.28 +    {const_spec_table = Symtab.empty};
    4.29 +  val copy = I;
    4.30 +  val extend = I;
    4.31 +  fun merge _
    4.32 +    ({const_spec_table = const_spec_table1},
    4.33 +     {const_spec_table = const_spec_table2}) =
    4.34 +     {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
    4.35 +);
    4.36 +
    4.37 +fun mk_data c = {const_spec_table = c}
    4.38 +fun map_data f {const_spec_table = c} = mk_data (f c)
    4.39 +
    4.40 +type specification_table = thm list Symtab.table
    4.41 +
    4.42 +fun defining_const_of_introrule_term t =
    4.43 +  let
    4.44 +    val _ $ u = Logic.strip_imp_concl t
    4.45 +    val (pred, all_args) = strip_comb u
    4.46 +  in case pred of
    4.47 +    Const (c, T) => c
    4.48 +    | _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
    4.49 +  end
    4.50 +
    4.51 +val defining_const_of_introrule = defining_const_of_introrule_term o prop_of
    4.52 +
    4.53 +(*TODO*)
    4.54 +fun is_introlike_term t = true
    4.55 +
    4.56 +val is_introlike = is_introlike_term o prop_of
    4.57 +
    4.58 +fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
    4.59 +  (case strip_comb u of
    4.60 +    (Const (c, T), args) =>
    4.61 +      if (length (binder_types T) = length args) then
    4.62 +        true
    4.63 +      else
    4.64 +        raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
    4.65 +  | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
    4.66 +  | check_equation_format_term t =
    4.67 +    raise TERM ("check_equation_format_term failed: Not an equation", [t])
    4.68 +
    4.69 +val check_equation_format = check_equation_format_term o prop_of
    4.70 +
    4.71 +fun defining_const_of_equation_term (t as (Const ("==", _) $ u $ v)) =
    4.72 +  (case fst (strip_comb u) of
    4.73 +    Const (c, _) => c
    4.74 +  | _ => raise TERM ("defining_const_of_equation_term failed: Not a constant", [t]))
    4.75 +  | defining_const_of_equation_term t =
    4.76 +    raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
    4.77 +
    4.78 +val defining_const_of_equation = defining_const_of_equation_term o prop_of
    4.79 +
    4.80 +(* Normalizing equations *)
    4.81 +
    4.82 +fun mk_meta_equation th =
    4.83 +  case prop_of th of
    4.84 +    Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
    4.85 +  | _ => th
    4.86 +
    4.87 +fun full_fun_cong_expand th =
    4.88 +  let
    4.89 +    val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
    4.90 +    val i = length (binder_types (fastype_of f)) - length args
    4.91 +  in funpow i (fn th => th RS @{thm meta_fun_cong}) th end;
    4.92 +
    4.93 +fun declare_names s xs ctxt =
    4.94 +  let
    4.95 +    val res = Name.names ctxt s xs
    4.96 +  in (res, fold Name.declare (map fst res) ctxt) end
    4.97 +  
    4.98 +fun split_all_pairs thy th =
    4.99 +  let
   4.100 +    val ctxt = ProofContext.init thy
   4.101 +    val ((_, [th']), ctxt') = Variable.import true [th] ctxt
   4.102 +    val t = prop_of th'
   4.103 +    val frees = Term.add_frees t [] 
   4.104 +    val freenames = Term.add_free_names t []
   4.105 +    val nctxt = Name.make_context freenames
   4.106 +    fun mk_tuple_rewrites (x, T) nctxt =
   4.107 +      let
   4.108 +        val Ts = HOLogic.flatten_tupleT T
   4.109 +        val (xTs, nctxt') = declare_names x Ts nctxt
   4.110 +        val paths = HOLogic.flat_tupleT_paths T
   4.111 +      in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
   4.112 +    val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
   4.113 +    val t' = Pattern.rewrite_term thy rewr [] t
   4.114 +    val tac = SkipProof.cheat_tac thy
   4.115 +    val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
   4.116 +    val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
   4.117 +  in
   4.118 +    th'''
   4.119 +  end;
   4.120 +
   4.121 +fun normalize_equation thy th =
   4.122 +  mk_meta_equation th
   4.123 +	|> Pred_Compile_Set.unfold_set_notation
   4.124 +  |> full_fun_cong_expand
   4.125 +  |> split_all_pairs thy
   4.126 +  |> tap check_equation_format
   4.127 +
   4.128 +fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite
   4.129 +((Simplifier.theory_context thy Simplifier.empty_ss) addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th
   4.130 +
   4.131 +fun store_thm_in_table ignore_consts thy th=
   4.132 +  let
   4.133 +    val th = AxClass.unoverload thy th
   4.134 +      |> inline_equations thy
   4.135 +    val (const, th) =
   4.136 +      if is_equationlike th then
   4.137 +        let
   4.138 +          val _ = priority "Normalizing definition..."
   4.139 +          val eq = normalize_equation thy th
   4.140 +        in
   4.141 +          (defining_const_of_equation eq, eq)
   4.142 +        end
   4.143 +      else if (is_introlike th) then
   4.144 +        let val th = Pred_Compile_Set.unfold_set_notation th
   4.145 +        in (defining_const_of_introrule th, th) end
   4.146 +      else error "store_thm: unexpected definition format"
   4.147 +  in
   4.148 +    if not (member (op =) ignore_consts const) then
   4.149 +      Symtab.cons_list (const, th)
   4.150 +    else I
   4.151 +  end
   4.152 +
   4.153 +(*
   4.154 +fun make_const_spec_table_warning thy =
   4.155 +  fold
   4.156 +    (fn th => fn thy => case try (store_thm th) thy of
   4.157 +      SOME thy => thy
   4.158 +    | NONE => (warning ("store_thm fails for " ^ Display.string_of_thm_global thy th) ; thy))
   4.159 +      (Predicate_Compile_Preproc_Const_Defs.get (ProofContext.init thy)) thy
   4.160 +
   4.161 +fun make_const_spec_table thy =
   4.162 +  fold store_thm (Predicate_Compile_Preproc_Const_Defs.get (ProofContext.init thy)) thy
   4.163 +  |> (fn thy => fold store_thm (Nitpick_Const_Simps.get (ProofContext.init thy)) thy)
   4.164 +*)
   4.165 +fun make_const_spec_table thy =
   4.166 +  let
   4.167 +    fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy)))
   4.168 +    val table = Symtab.empty
   4.169 +      |> store [] Predicate_Compile_Alternative_Defs.get
   4.170 +    val ignore_consts = Symtab.keys table
   4.171 +  in
   4.172 +    table   
   4.173 +    |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
   4.174 +    |> store ignore_consts Nitpick_Const_Simps.get
   4.175 +    |> store ignore_consts Nitpick_Ind_Intros.get
   4.176 +  end
   4.177 +  (*
   4.178 +fun get_specification thy constname =
   4.179 +  case Symtab.lookup (#const_spec_table (Data.get thy)) constname of
   4.180 +    SOME thms => thms
   4.181 +  | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
   4.182 +  *)
   4.183 +fun get_specification table constname =
   4.184 +  case Symtab.lookup table constname of
   4.185 +  SOME thms =>
   4.186 +    let
   4.187 +      val _ = tracing ("Looking up specification of " ^ constname ^ ": "
   4.188 +        ^ (commas (map Display.string_of_thm_without_context thms)))
   4.189 +    in thms end
   4.190 +  | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
   4.191 +
   4.192 +val logic_operator_names =
   4.193 +  [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "op &"}]
   4.194 +
   4.195 +val special_cases = member (op =) [@{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
   4.196 +    @{const_name Nat.one_nat_inst.one_nat},
   4.197 +@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
   4.198 +@{const_name "HOL.one_class.one"},  @{const_name HOL.plus_class.plus},
   4.199 +@{const_name "Nat.nat.nat_case"}, @{const_name "List.list.list_case"}, @{const_name Nat.ord_nat_inst.less_eq_nat}]
   4.200 +
   4.201 +fun obtain_specification_graph table constname =
   4.202 +  let
   4.203 +    fun is_nondefining_constname c = member (op =) logic_operator_names c
   4.204 +    val is_defining_constname = member (op =) (Symtab.keys table)
   4.205 +    fun defiants_of specs =
   4.206 +      fold (Term.add_const_names o prop_of) specs []
   4.207 +      |> filter is_defining_constname
   4.208 +      |> filter_out special_cases
   4.209 +    fun extend constname =
   4.210 +      let
   4.211 +        val specs = get_specification table constname
   4.212 +      in (specs, defiants_of specs) end;
   4.213 +  in
   4.214 +    Graph.extend extend constname Graph.empty
   4.215 +  end;
   4.216 +  
   4.217 +  
   4.218 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Wed Sep 23 16:20:12 2009 +0200
     5.3 @@ -0,0 +1,414 @@
     5.4 +(* Author: Lukas Bulwahn, TU Muenchen
     5.5 +
     5.6 +Preprocessing functions to predicates
     5.7 +*)
     5.8 +
     5.9 +signature PREDICATE_COMPILE_FUN =
    5.10 +sig
    5.11 +  val define_predicates : (string * thm list) list -> theory -> theory
    5.12 +  val rewrite_intro : theory -> thm -> thm list
    5.13 +  val setup_oracle : theory -> theory
    5.14 +end;
    5.15 +
    5.16 +structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
    5.17 +struct
    5.18 +
    5.19 +
    5.20 +(* Oracle for preprocessing  *)
    5.21 +
    5.22 +val (oracle : (string * (cterm -> thm)) option ref) = ref NONE;
    5.23 +
    5.24 +fun the_oracle () =
    5.25 +  case !oracle of
    5.26 +    NONE => error "Oracle is not setup"
    5.27 +  | SOME (_, oracle) => oracle
    5.28 +             
    5.29 +val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #->
    5.30 +  (fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end)
    5.31 +  
    5.32 +  
    5.33 +fun is_funtype (Type ("fun", [_, _])) = true
    5.34 +  | is_funtype _ = false;
    5.35 +
    5.36 +fun is_Type (Type _) = true
    5.37 +  | is_Type _ = false
    5.38 +
    5.39 +(* returns true if t is an application of an datatype constructor *)
    5.40 +(* which then consequently would be splitted *)
    5.41 +(* else false *)
    5.42 +(*
    5.43 +fun is_constructor thy t =
    5.44 +  if (is_Type (fastype_of t)) then
    5.45 +    (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of
    5.46 +      NONE => false
    5.47 +    | SOME info => (let
    5.48 +      val constr_consts = flat (map (fn (_, (_, _, constrs)) => map fst constrs) (#descr info))
    5.49 +      val (c, _) = strip_comb t
    5.50 +      in (case c of
    5.51 +        Const (name, _) => name mem_string constr_consts
    5.52 +        | _ => false) end))
    5.53 +  else false
    5.54 +*)
    5.55 +
    5.56 +(* must be exported in code.ML *)
    5.57 +fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
    5.58 +
    5.59 +(* Table from constant name (string) to term of inductive predicate *)
    5.60 +structure Pred_Compile_Preproc = TheoryDataFun
    5.61 +(
    5.62 +  type T = string Symtab.table;
    5.63 +  val empty = Symtab.empty;
    5.64 +  val copy = I;
    5.65 +  val extend = I;
    5.66 +  fun merge _ = Symtab.merge (op =);
    5.67 +)
    5.68 +
    5.69 +fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) 
    5.70 +
    5.71 +
    5.72 +fun transform_ho_typ (T as Type ("fun", _)) =
    5.73 +  let
    5.74 +    val (Ts, T') = strip_type T
    5.75 +  in (Ts @ [T']) ---> HOLogic.boolT end
    5.76 +| transform_ho_typ t = t
    5.77 +
    5.78 +fun transform_ho_arg arg = 
    5.79 +  case (fastype_of arg) of
    5.80 +    (T as Type ("fun", _)) => (* if T = bool might be a relation already *)
    5.81 +      (case arg of
    5.82 +        Free (name, _) => Free (name, transform_ho_typ T)
    5.83 +      | _ => error "I am surprised")
    5.84 +| _ => arg
    5.85 +
    5.86 +fun pred_type T =
    5.87 +  let  
    5.88 +    val (Ts, T') = strip_type T
    5.89 +    val Ts' = map transform_ho_typ Ts
    5.90 +  in
    5.91 +    (Ts' @ [T']) ---> HOLogic.boolT
    5.92 +  end;
    5.93 +
    5.94 +(* FIXME: create new predicate name -- does not avoid nameclashing *)
    5.95 +fun pred_of f =
    5.96 +  let
    5.97 +    val (name, T) = dest_Const f
    5.98 +  in
    5.99 +    if (body_type T = @{typ bool}) then
   5.100 +      (Free (Long_Name.base_name name ^ "P", T))
   5.101 +    else
   5.102 +      (Free (Long_Name.base_name name ^ "P", pred_type T))
   5.103 +  end
   5.104 +
   5.105 +fun mk_param lookup_pred (t as Free (v, _)) = lookup_pred t
   5.106 +  | mk_param lookup_pred t =
   5.107 +  let
   5.108 +    val (vs, body) = strip_abs t
   5.109 +    val names = Term.add_free_names body []
   5.110 +    val vs_names = Name.variant_list names (map fst vs)
   5.111 +    val vs' = map2 (curry Free) vs_names (map snd vs)
   5.112 +    val body' = subst_bounds (rev vs', body)
   5.113 +    val (f, args) = strip_comb body'
   5.114 +    val resname = Name.variant (vs_names @ names) "res"
   5.115 +    val resvar = Free (resname, body_type (fastype_of body'))
   5.116 +    val P = lookup_pred f
   5.117 +    val pred_body = list_comb (P, args @ [resvar])
   5.118 +    val param = fold_rev lambda (vs' @ [resvar]) pred_body
   5.119 +  in param end;
   5.120 +
   5.121 +
   5.122 +(* creates the list of premises for every intro rule *)
   5.123 +(* theory -> term -> (string list, term list list) *)
   5.124 +
   5.125 +fun dest_code_eqn eqn = let
   5.126 +  val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn))
   5.127 +  val (func, args) = strip_comb lhs
   5.128 +in ((func, args), rhs) end;
   5.129 +
   5.130 +fun string_of_typ T = Syntax.string_of_typ_global @{theory} T
   5.131 +
   5.132 +fun string_of_term t =
   5.133 +  case t of
   5.134 +    Const (c, T) => "Const (" ^ c ^ ", " ^ string_of_typ T ^ ")"
   5.135 +  | Free (c, T) => "Free (" ^ c ^ ", " ^ string_of_typ T ^ ")"
   5.136 +  | Var ((c, i), T) => "Var ((" ^ c ^ ", " ^ string_of_int i ^ "), " ^ string_of_typ T ^ ")"
   5.137 +  | Bound i => "Bound " ^ string_of_int i
   5.138 +  | Abs (x, T, t) => "Abs (" ^ x ^ ", " ^ string_of_typ T ^ ", " ^ string_of_term t ^ ")"
   5.139 +  | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")"
   5.140 +  
   5.141 +fun ind_package_get_nparams thy name =
   5.142 +  case try (Inductive.the_inductive (ProofContext.init thy)) name of
   5.143 +    SOME (_, result) => length (Inductive.params_of (#raw_induct result))
   5.144 +  | NONE => error ("No such predicate: " ^ quote name) 
   5.145 +
   5.146 +(* TODO: does not work with higher order functions yet *)
   5.147 +fun mk_rewr_eq (func, pred) =
   5.148 +  let
   5.149 +    val (argTs, resT) = (strip_type (fastype_of func))
   5.150 +    val nctxt =
   5.151 +      Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
   5.152 +    val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
   5.153 +    val ([resname], nctxt'') = Name.variants ["r"] nctxt'
   5.154 +    val args = map Free (argnames ~~ argTs)
   5.155 +    val res = Free (resname, resT)
   5.156 +  in Logic.mk_equals
   5.157 +      (HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res]))
   5.158 +  end;
   5.159 +
   5.160 +fun has_split_rule_cname @{const_name "nat_case"} = true
   5.161 +  | has_split_rule_cname @{const_name "list_case"} = true
   5.162 +  | has_split_rule_cname _ = false
   5.163 +  
   5.164 +fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true 
   5.165 +  | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true 
   5.166 +  | has_split_rule_term thy _ = false
   5.167 +
   5.168 +fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
   5.169 +  | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
   5.170 +  | has_split_rule_term' thy c = has_split_rule_term thy c
   5.171 +  
   5.172 +fun prepare_split_thm ctxt split_thm =
   5.173 +    (split_thm RS @{thm iffD2})
   5.174 +    |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]},
   5.175 +      @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
   5.176 +
   5.177 +fun find_split_thm thy (Const (name, typ)) =
   5.178 +  let
   5.179 +    fun split_name str =
   5.180 +      case first_field "." str
   5.181 +        of (SOME (field, rest)) => field :: split_name rest
   5.182 +         | NONE => [str]
   5.183 +    val splitted_name = split_name name
   5.184 +  in
   5.185 +    if length splitted_name > 0 andalso
   5.186 +       String.isSuffix "_case" (List.last splitted_name)
   5.187 +    then
   5.188 +      (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
   5.189 +      |> String.concatWith "."
   5.190 +      |> PureThy.get_thm thy
   5.191 +      |> SOME
   5.192 +      handle ERROR msg => NONE
   5.193 +    else NONE
   5.194 +  end
   5.195 +  | find_split_thm _ _ = NONE
   5.196 +
   5.197 +fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
   5.198 +  | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
   5.199 +  | find_split_thm' thy c = find_split_thm thy c
   5.200 +  
   5.201 +fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)  
   5.202 +  
   5.203 +fun folds_map f xs y =
   5.204 +  let
   5.205 +    fun folds_map' acc [] y = [(rev acc, y)]
   5.206 +      | folds_map' acc (x :: xs) y =
   5.207 +        maps (fn (x, y) => folds_map' (x :: acc) xs y) (f x y)     
   5.208 +    in
   5.209 +      folds_map' [] xs y
   5.210 +    end;
   5.211 +      
   5.212 +fun mk_prems thy (lookup_pred, get_nparams) t (names, prems) =
   5.213 +  let
   5.214 +    fun mk_prems' (t as Const (name, T)) (names, prems) =
   5.215 +      [(lookup_pred t, (names, prems))]
   5.216 +    | mk_prems' (t as Free (f, T)) (names, prems) = 
   5.217 +      [(lookup_pred t, (names, prems))]
   5.218 +    | mk_prems' t (names, prems) =
   5.219 +      if Predicate_Compile_Aux.is_constrt thy t then
   5.220 +        [(t, (names, prems))]
   5.221 +      else
   5.222 +        if has_split_rule_term' thy (fst (strip_comb t)) then
   5.223 +          let
   5.224 +            val (f, args) = strip_comb t
   5.225 +            val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
   5.226 +            (* TODO: contextify things - this line is to unvarify the split_thm *)
   5.227 +            (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
   5.228 +            val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
   5.229 +            val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
   5.230 +            val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
   5.231 +            val (_, split_args) = strip_comb split_t
   5.232 +            val match = split_args ~~ args
   5.233 +            fun mk_prems_of_assm assm =
   5.234 +              let
   5.235 +                val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
   5.236 +                val var_names = Name.variant_list names (map fst vTs)
   5.237 +                val vars = map Free (var_names ~~ (map snd vTs))
   5.238 +                val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
   5.239 +                val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
   5.240 +              in
   5.241 +                mk_prems' inner_t (var_names @ names, prems' @ prems)
   5.242 +              end
   5.243 +          in
   5.244 +            maps mk_prems_of_assm assms
   5.245 +          end
   5.246 +        else
   5.247 +          let 
   5.248 +            val (f, args) = strip_comb t
   5.249 +            val resname = Name.variant names "res"
   5.250 +            val resvar = Free (resname, body_type (fastype_of t))
   5.251 +            val names' = resname :: names
   5.252 +            fun mk_prems'' (t as Const (c, _)) =
   5.253 +              if is_constr thy c then
   5.254 +                folds_map mk_prems' args (names', prems) |>
   5.255 +                map
   5.256 +                  (fn (argvs, (names'', prems')) =>
   5.257 +                  let
   5.258 +                    val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
   5.259 +                  in (names'', prem :: prems') end)
   5.260 +              else
   5.261 +                let
   5.262 +                  val pred = lookup_pred t
   5.263 +                  val nparams = get_nparams pred
   5.264 +                  val (params, args) = chop nparams args
   5.265 +                  val params' = map (mk_param lookup_pred) params
   5.266 +                in
   5.267 +                  folds_map mk_prems' args (names', prems)
   5.268 +                  |> map (fn (argvs, (names'', prems')) =>
   5.269 +                    let
   5.270 +                      val prem = HOLogic.mk_Trueprop (list_comb (pred, params' @ argvs @ [resvar]))
   5.271 +                    in (names'', prem :: prems') end)
   5.272 +                end
   5.273 +            | mk_prems'' (t as Free (_, _)) =
   5.274 +                let
   5.275 +                  (* higher order argument call *)
   5.276 +                  val pred = lookup_pred t
   5.277 +                in
   5.278 +                  folds_map mk_prems' args (resname :: names, prems)
   5.279 +                  |> map (fn (argvs, (names', prems')) =>
   5.280 +                     let
   5.281 +                       val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar]))
   5.282 +                     in (names', prem :: prems') end)
   5.283 +                end
   5.284 +            | mk_prems'' t = error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
   5.285 +          in
   5.286 +            map (pair resvar) (mk_prems'' f)
   5.287 +          end
   5.288 +  in
   5.289 +    mk_prems' t (names, prems)
   5.290 +  end;    
   5.291 +
   5.292 +(* assumption: mutual recursive predicates all have the same parameters. *)  
   5.293 +fun define_predicates specs thy =
   5.294 +  if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get thy)) const) specs then
   5.295 +    thy
   5.296 +  else
   5.297 +  let
   5.298 +    val consts = map fst specs
   5.299 +    val eqns = maps snd specs
   5.300 +    (*val eqns = maps (Predicate_Compile_Preproc_Data.get_specification thy) consts*)
   5.301 +      (* create prednames *)
   5.302 +    val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
   5.303 +    val argss' = map (map transform_ho_arg) argss
   5.304 +    val pnames = map (dest_Free) (distinct (op =) (flat argss' \\ flat argss))
   5.305 +    val preds = map pred_of funs
   5.306 +    val prednames = map (fst o dest_Free) preds
   5.307 +    val funnames = map (fst o dest_Const) funs
   5.308 +    val fun_pred_names = (funnames ~~ prednames)  
   5.309 +      (* mapping from term (Free or Const) to term *)
   5.310 +    fun lookup_pred (Const (@{const_name Cons}, T)) =
   5.311 +      Const ("Preprocessing.ConsP", pred_type T) (* FIXME: temporary - Cons lookup *)
   5.312 +      | lookup_pred (Const (name, T)) =
   5.313 +      (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
   5.314 +          SOME c => Const (c, pred_type T)
   5.315 +        | NONE =>
   5.316 +          (case AList.lookup op = fun_pred_names name of
   5.317 +            SOME f => Free (f, pred_type T)
   5.318 +          | NONE => Const (name, T)))
   5.319 +      | lookup_pred  (Free (name, T)) =
   5.320 +        if member op = (map fst pnames) name then
   5.321 +          Free (name, transform_ho_typ T)
   5.322 +        else
   5.323 +          Free (name, T)
   5.324 +      | lookup_pred t =
   5.325 +         error ("lookup function is not defined for " ^ Syntax.string_of_term_global thy t)
   5.326 +     
   5.327 +        (* mapping from term (predicate term, not function term!) to int *)
   5.328 +    fun get_nparams (Const (name, _)) =
   5.329 +      the_default 0 (try (ind_package_get_nparams thy) name)
   5.330 +    | get_nparams (Free (name, _)) =
   5.331 +        (if member op = prednames name then
   5.332 +          length pnames
   5.333 +        else 0)
   5.334 +    | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
   5.335 +  
   5.336 +    (* create intro rules *)
   5.337 +  
   5.338 +    fun mk_intros ((func, pred), (args, rhs)) =
   5.339 +      if (body_type (fastype_of func) = @{typ bool}) then
   5.340 +       (*TODO: preprocess predicate definition of rhs *)
   5.341 +        [Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
   5.342 +      else
   5.343 +        let
   5.344 +          val names = Term.add_free_names rhs []
   5.345 +        in mk_prems thy (lookup_pred, get_nparams) rhs (names, [])
   5.346 +          |> map (fn (resultt, (names', prems)) =>
   5.347 +            Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
   5.348 +        end
   5.349 +    fun mk_rewr_thm (func, pred) = @{thm refl}
   5.350 +      
   5.351 +    val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
   5.352 +    val _ = map (tracing o (Syntax.string_of_term_global thy)) intr_ts
   5.353 +    (* define new inductive predicates *)
   5.354 +    val (ind_result, thy') =
   5.355 +      Inductive.add_inductive_global (serial_string ())
   5.356 +        {quiet_mode = false, verbose = false, kind = Thm.internalK,
   5.357 +          alt_name = Binding.empty, coind = false, no_elim = false,
   5.358 +          no_ind = false, skip_mono = false, fork_mono = false}
   5.359 +        (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
   5.360 +        pnames
   5.361 +        (map (fn x => (Attrib.empty_binding, x)) intr_ts)
   5.362 +        [] thy
   5.363 +    val prednames = map (fst o dest_Const) (#preds ind_result)
   5.364 +    (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *)
   5.365 +    (* add constants to my table *)
   5.366 +    val thy'' = thy'
   5.367 +      |> Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames))
   5.368 +  in
   5.369 +    thy''
   5.370 +  end
   5.371 +
   5.372 +(* preprocessing intro rules - uses oracle *)
   5.373 +
   5.374 +(* theory -> thm -> thm *)
   5.375 +fun rewrite_intro thy intro =
   5.376 +  let
   5.377 +    fun lookup_pred (Const (name, T)) =
   5.378 +      (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
   5.379 +        SOME c => Const (c, pred_type T)
   5.380 +      | NONE => Const (name, T))
   5.381 +    | lookup_pred (Free (name, T)) = Free (name, T)
   5.382 +    | lookup_pred _ = error "lookup function is not defined!"
   5.383 +
   5.384 +    fun get_nparams (Const (name, _)) =
   5.385 +      the_default 0 (try (ind_package_get_nparams thy) name)
   5.386 +    | get_nparams (Free _) = 0
   5.387 +    | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
   5.388 +    
   5.389 +    val intro_t = (Logic.unvarify o prop_of) intro
   5.390 +    val _ = tracing (Syntax.string_of_term_global thy intro_t)
   5.391 +    val (prems, concl) = Logic.strip_horn intro_t
   5.392 +    val frees = map fst (Term.add_frees intro_t [])
   5.393 +    fun opt_dest_Not t = the_default t (try HOLogic.dest_not t)
   5.394 +    fun rewrite prem names =
   5.395 +      let
   5.396 +        val (P, args) = (strip_comb o opt_dest_Not o HOLogic.dest_Trueprop) prem
   5.397 +      in
   5.398 +        folds_map (
   5.399 +          fn t => if (is_funtype (fastype_of t)) then (fn x => [(t, x)])
   5.400 +            else mk_prems thy (lookup_pred, get_nparams) t) args (names, [])
   5.401 +        |> map (fn (resargs, (names', prems')) =>
   5.402 +          let
   5.403 +            val prem' = HOLogic.mk_Trueprop (list_comb (P, resargs))
   5.404 +          in (prem'::prems', names') end)
   5.405 +      end
   5.406 +    val intro_ts' = folds_map rewrite prems frees
   5.407 +      |> maps (fn (prems', frees') =>
   5.408 +        rewrite concl frees'
   5.409 +        |> map (fn (concl'::conclprems, _) =>
   5.410 +          Logic.list_implies ((flat prems') @ conclprems, concl')))
   5.411 +    val _ = Output.tracing ("intro_ts': " ^
   5.412 +      commas (map (Syntax.string_of_term_global thy) intro_ts'))
   5.413 +  in
   5.414 +    map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
   5.415 +  end; 
   5.416 +
   5.417 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Wed Sep 23 16:20:12 2009 +0200
     6.3 @@ -0,0 +1,131 @@
     6.4 +(* Author: Lukas Bulwahn, TU Muenchen
     6.5 +
     6.6 +Preprocessing definitions of predicates to introduction rules
     6.7 +*)
     6.8 +
     6.9 +signature PREDICATE_COMPILE_PRED =
    6.10 +sig
    6.11 +  (* preprocesses an equation to a set of intro rules; defines new constants *)
    6.12 +  (*
    6.13 +  val preprocess_pred_equation : thm -> theory -> thm list * theory
    6.14 +  *)
    6.15 +  val preprocess : string -> theory -> (thm list list * theory) 
    6.16 +  (* output is the term list of clauses of an unknown predicate *)
    6.17 +  val preprocess_term : term -> theory -> (term list * theory)
    6.18 +  
    6.19 +  (*val rewrite : thm -> thm*)
    6.20 +  
    6.21 +end;
    6.22 +(* : PREDICATE_COMPILE_PREPROC_PRED *)
    6.23 +structure Predicate_Compile_Pred =
    6.24 +struct
    6.25 +
    6.26 +open Predicate_Compile_Aux
    6.27 +
    6.28 +fun is_compound ((Const ("Not", _)) $ t) =
    6.29 +    error "is_compound: Negation should not occur; preprocessing is defect"
    6.30 +  | is_compound ((Const ("Ex", _)) $ _) = true
    6.31 +  | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
    6.32 +  | is_compound ((Const ("op &", _)) $ _ $ _) =
    6.33 +    error "is_compound: Conjunction should not occur; preprocessing is defect"
    6.34 +  | is_compound _ = false
    6.35 +
    6.36 +fun flatten constname atom (defs, thy) =
    6.37 +  if is_compound atom then
    6.38 +    let
    6.39 +      val constname = Name.variant (map (Long_Name.base_name o fst) defs)
    6.40 +        ((Long_Name.base_name constname) ^ "_aux")
    6.41 +      val full_constname = Sign.full_bname thy constname
    6.42 +      val (params, args) = List.partition (is_predT o fastype_of)
    6.43 +        (map Free (Term.add_frees atom []))
    6.44 +      val constT = map fastype_of (params @ args) ---> HOLogic.boolT
    6.45 +      val lhs = list_comb (Const (full_constname, constT), params @ args)
    6.46 +      val def = Logic.mk_equals (lhs, atom)
    6.47 +      val ([definition], thy') = thy
    6.48 +        |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
    6.49 +        |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
    6.50 +    in
    6.51 +      (lhs, ((full_constname, [definition]) :: defs, thy'))
    6.52 +    end
    6.53 +  else
    6.54 +    (atom, (defs, thy))
    6.55 +
    6.56 +fun flatten_intros constname intros thy =
    6.57 +  let
    6.58 +    val ctxt = ProofContext.init thy
    6.59 +    val ((_, intros), ctxt') = Variable.import true intros ctxt
    6.60 +    val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
    6.61 +      (flatten constname) (map prop_of intros) ([], thy)
    6.62 +    val tac = fn {...} => SkipProof.cheat_tac thy'
    6.63 +    val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
    6.64 +      |> Variable.export ctxt' ctxt
    6.65 +  in
    6.66 +    (intros'', (local_defs, thy'))
    6.67 +  end
    6.68 +
    6.69 +(* TODO: same function occurs in inductive package *)
    6.70 +fun select_disj 1 1 = []
    6.71 +  | select_disj _ 1 = [rtac @{thm disjI1}]
    6.72 +  | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1));
    6.73 +
    6.74 +fun introrulify thy th = 
    6.75 +  let
    6.76 +    val ctxt = (ProofContext.init thy)
    6.77 +    val ((_, [th']), ctxt') = Variable.import true [th] ctxt
    6.78 +    val (lhs, rhs) = Logic.dest_equals (prop_of th')
    6.79 +    val frees = Term.add_free_names rhs []
    6.80 +    val disjuncts = HOLogic.dest_disj rhs
    6.81 +    val nctxt = Name.make_context frees
    6.82 +    fun mk_introrule t =
    6.83 +      let
    6.84 +        val ((ps, t'), nctxt') = focus_ex t nctxt
    6.85 +        val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t')
    6.86 +      in
    6.87 +        (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
    6.88 +      end
    6.89 +    val x = ((cterm_of thy) o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
    6.90 +      Logic.dest_implies o prop_of) @{thm exI}
    6.91 +    fun prove_introrule (index, (ps, introrule)) =
    6.92 +      let
    6.93 +        val tac = Simplifier.simp_tac (HOL_basic_ss addsimps [th]) 1
    6.94 +          THEN EVERY1 (select_disj (length disjuncts) (index + 1)) 
    6.95 +          THEN (EVERY (map (fn y =>
    6.96 +            rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps))
    6.97 +          THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1)
    6.98 +          THEN TRY (atac 1)
    6.99 +      in
   6.100 +        Goal.prove ctxt' (map fst ps) [] introrule (fn {...} => tac)
   6.101 +        |> singleton (Variable.export ctxt' ctxt)
   6.102 +      end
   6.103 +  in
   6.104 +    map_index prove_introrule (map mk_introrule disjuncts) 
   6.105 +  end;
   6.106 +
   6.107 +val rewrite =
   6.108 +  Simplifier.simplify (HOL_basic_ss addsimps [@{thm Ball_def}, @{thm Bex_def}])
   6.109 +  #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm all_not_ex}]) 
   6.110 +  #> Conv.fconv_rule nnf_conv 
   6.111 +  #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}])
   6.112 +  
   6.113 +fun preprocess (constname, specs) thy =
   6.114 +  let
   6.115 +    val ctxt = ProofContext.init thy
   6.116 +      val intros =
   6.117 +      if forall is_pred_equation specs then 
   6.118 +        maps (introrulify thy o rewrite) specs
   6.119 +      else if forall (is_intro constname) specs then
   6.120 +        specs
   6.121 +      else
   6.122 +        error ("unexpected specification for constant " ^ quote constname ^ ":\n"
   6.123 +          ^ commas (map (quote o Display.string_of_thm_global thy) specs))
   6.124 +    val _ = priority "Defining local predicates and their intro rules..."
   6.125 +    val (intros', (local_defs, thy')) = flatten_intros constname intros thy
   6.126 +    val (intross, thy'') = fold_map preprocess local_defs thy'
   6.127 +  in
   6.128 +    (intros' :: flat intross,thy'')
   6.129 +  end;
   6.130 +
   6.131 +fun preprocess_term t thy = error "preprocess_pred_term: to implement" 
   6.132 +  
   6.133 +  
   6.134 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML	Wed Sep 23 16:20:12 2009 +0200
     7.3 @@ -0,0 +1,51 @@
     7.4 +(* Author: Lukas Bulwahn, TU Muenchen
     7.5 +
     7.6 +Preprocessing sets to predicates
     7.7 +*)
     7.8 +
     7.9 +signature PRED_COMPILE_SET =
    7.10 +sig
    7.11 +(*
    7.12 +  val preprocess_intro : thm -> theory -> thm * theory
    7.13 +  val preprocess_clause : term -> theory -> term * theory
    7.14 +*)
    7.15 +  val unfold_set_notation : thm -> thm;
    7.16 +end;
    7.17 +
    7.18 +structure Pred_Compile_Set : PRED_COMPILE_SET =
    7.19 +struct
    7.20 +(*FIXME: unfolding Ball in pretty adhoc here *)
    7.21 +val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, @{thm Ball_def}]
    7.22 +
    7.23 +val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
    7.24 +
    7.25 +(*
    7.26 +fun find_set_theorems ctxt cname =
    7.27 +  let
    7.28 +    val _ = cname 
    7.29 +*)
    7.30 +
    7.31 +(*
    7.32 +fun preprocess_term t ctxt =
    7.33 +  case t of
    7.34 +    Const ("op :", _) $ x $ A => 
    7.35 +      case strip_comb A of
    7.36 +        (Const (cname, T), params) =>
    7.37 +          let 
    7.38 +            val _ = find_set_theorems
    7.39 +          in
    7.40 +            (t, ctxt)
    7.41 +          end
    7.42 +      | _ => (t, ctxt)  
    7.43 +  | _ => (t, ctxt)
    7.44 +*) 
    7.45 +(*
    7.46 +fun preprocess_intro th thy =
    7.47 +  let
    7.48 +    val cnames = find_heads_of_prems
    7.49 +    val set_cname = filter (has_set_definition
    7.50 +    val _ = define_preds
    7.51 +    val _ = prep_pred_def
    7.52 +  in
    7.53 +*)
    7.54 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
     8.3 @@ -0,0 +1,75 @@
     8.4 +(* Author: Lukas Bulwahn, TU Muenchen
     8.5 +
     8.6 +*)
     8.7 +signature PREDICATE_COMPILE =
     8.8 +sig
     8.9 +  val setup : theory -> theory
    8.10 +end;
    8.11 +
    8.12 +structure Predicate_Compile : PREDICATE_COMPILE =
    8.13 +struct
    8.14 +
    8.15 +open Predicate_Compile_Aux;
    8.16 +
    8.17 +val priority = tracing;
    8.18 +
    8.19 +(* Some last processing *)
    8.20 +fun remove_pointless_clauses intro =
    8.21 +  if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
    8.22 +    []
    8.23 +  else [intro]
    8.24 +
    8.25 +fun preprocess_strong_conn_constnames gr constnames thy =
    8.26 +  let
    8.27 +    val get_specs = map (fn k => (k, Graph.get_node gr k))
    8.28 +    val _ = priority ("Preprocessing scc of " ^ commas constnames)
    8.29 +    val (prednames, funnames) = List.partition (is_pred thy) constnames
    8.30 +    (* untangle recursion by defining predicates for all functions *)
    8.31 +    val _ = priority "Compiling functions to predicates..."
    8.32 +    val _ = Output.tracing ("funnames: " ^ commas funnames)
    8.33 +    val thy' =
    8.34 +      thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates
    8.35 +      (get_specs funnames)
    8.36 +    val _ = priority "Compiling predicates to flat introrules..."
    8.37 +    val (intross, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess
    8.38 +      (get_specs prednames) thy')
    8.39 +    val _ = tracing ("intross: " ^ commas (map (Display.string_of_thm_global thy'') (flat intross)))
    8.40 +    val _ = priority "Replacing functions in introrules..."
    8.41 +    val intross' = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross
    8.42 +    val intross'' = burrow (maps remove_pointless_clauses) intross
    8.43 +    val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy''
    8.44 +  in
    8.45 +    thy'''
    8.46 +  end;
    8.47 +
    8.48 +fun code_pred_cmd ((inductify_all, rpred), raw_const) lthy =
    8.49 +  if inductify_all then
    8.50 +    let
    8.51 +      val thy = ProofContext.theory_of lthy
    8.52 +      val const = Code.read_const thy raw_const
    8.53 +      val _ = Output.tracing ("fetching definition from theory")
    8.54 +      val table = Pred_Compile_Data.make_const_spec_table thy
    8.55 +      val gr = Pred_Compile_Data.obtain_specification_graph table const
    8.56 +      val _ = Output.tracing (commas (Graph.all_succs gr [const]))
    8.57 +      val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr
    8.58 +	    val lthy' = LocalTheory.theory (fold_rev (preprocess_strong_conn_constnames gr)
    8.59 +      (Graph.strong_conn gr)) lthy
    8.60 +        |> LocalTheory.checkpoint
    8.61 +    in Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy' end
    8.62 +  else
    8.63 +    Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy
    8.64 +
    8.65 +val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
    8.66 +
    8.67 +val _ = List.app OuterKeyword.keyword ["inductify_all", "rpred"]
    8.68 +
    8.69 +local structure P = OuterParse
    8.70 +in
    8.71 +
    8.72 +val _ = OuterSyntax.local_theory_to_proof "code_pred"
    8.73 +  "prove equations for predicate specified by intro/elim rules"
    8.74 +  OuterKeyword.thy_goal (P.opt_keyword "inductify_all" -- P.opt_keyword "rpred" -- P.term_group >> code_pred_cmd)
    8.75 +
    8.76 +end
    8.77 +
    8.78 +end
     9.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 23 16:20:12 2009 +0200
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 23 16:20:12 2009 +0200
     9.3 @@ -6,11 +6,15 @@
     9.4  
     9.5  signature PREDICATE_COMPILE_CORE =
     9.6  sig
     9.7 +  val setup: theory -> theory
     9.8 +  val code_pred: bool -> string -> Proof.context -> Proof.state
     9.9 +  val code_pred_cmd: bool -> string -> Proof.context -> Proof.state
    9.10    type smode = (int * int list option) list
    9.11    type mode = smode option list * smode
    9.12    datatype tmode = Mode of mode * smode * tmode option list;
    9.13    (*val add_equations_of: bool -> string list -> theory -> theory *)
    9.14    val register_predicate : (thm list * thm * int) -> theory -> theory
    9.15 +  val register_intros : thm list -> theory -> theory
    9.16    val is_registered : theory -> string -> bool
    9.17   (* val fetch_pred_data : theory -> string -> (thm list * thm * int)  *)
    9.18    val predfun_intro_of: theory -> string -> mode -> thm
    9.19 @@ -24,9 +28,7 @@
    9.20    val nparams_of: theory -> string -> int
    9.21    val add_intro: thm -> theory -> theory
    9.22    val set_elim: thm -> theory -> theory
    9.23 -  val setup: theory -> theory
    9.24 -  val code_pred: string -> Proof.context -> Proof.state
    9.25 -  val code_pred_cmd: string -> Proof.context -> Proof.state
    9.26 +  val set_nparams : string -> int -> theory -> theory
    9.27    val print_stored_rules: theory -> unit
    9.28    val print_all_modes: theory -> unit
    9.29    val do_proofs: bool ref
    9.30 @@ -106,6 +108,7 @@
    9.31  structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
    9.32  struct
    9.33  
    9.34 +open Predicate_Compile_Aux;
    9.35  (** auxiliary **)
    9.36  
    9.37  (* debug stuff *)
    9.38 @@ -187,7 +190,7 @@
    9.39  
    9.40  (** data structures **)
    9.41  
    9.42 -type smode = (int * int list option) list;
    9.43 +type smode = (int * int list option) list
    9.44  type mode = smode option list * smode;
    9.45  datatype tmode = Mode of mode * smode * tmode option list;
    9.46  
    9.47 @@ -238,7 +241,33 @@
    9.48    "predmode: " ^ (string_of_mode predmode) ^ 
    9.49    (if null param_modes then "" else
    9.50      "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes))
    9.51 +
    9.52 +(* generation of case rules from user-given introduction rules *)
    9.53 +
    9.54 +fun mk_casesrule ctxt nparams introrules =
    9.55 +  let
    9.56 +    val intros = map (Logic.unvarify o prop_of) introrules
    9.57 +    val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
    9.58 +    val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
    9.59 +    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
    9.60 +    val (argnames, ctxt2) = Variable.variant_fixes
    9.61 +      (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
    9.62 +    val argvs = map2 (curry Free) argnames (map fastype_of args)
    9.63 +    fun mk_case intro =
    9.64 +      let
    9.65 +        val (_, (_, args)) = strip_intro_concl nparams intro
    9.66 +        val prems = Logic.strip_imp_prems intro
    9.67 +        val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
    9.68 +        val frees = (fold o fold_aterms)
    9.69 +          (fn t as Free _ =>
    9.70 +              if member (op aconv) params t then I else insert (op aconv) t
    9.71 +           | _ => I) (args @ prems) []
    9.72 +      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
    9.73 +    val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
    9.74 +    val cases = map mk_case intros
    9.75 +  in Logic.list_implies (assm :: cases, prop) end;
    9.76      
    9.77 +
    9.78  datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
    9.79    GeneratorPrem of term list * term | Generator of (string * typ);
    9.80  
    9.81 @@ -579,9 +608,6 @@
    9.82        | find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs;
    9.83    in rev (find [] 0 xs) end;
    9.84  
    9.85 -fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
    9.86 -  | is_predT _ = false
    9.87 -  
    9.88  fun guess_nparams T =
    9.89    let
    9.90      val argTs = binder_types T
    9.91 @@ -611,16 +637,28 @@
    9.92      fun set (intros, elim, _ ) = (intros, elim, nparams) 
    9.93    in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
    9.94      
    9.95 -fun register_predicate (pre_intros, pre_elim, nparams) thy = let
    9.96 +fun register_predicate (pre_intros, pre_elim, nparams) thy =
    9.97 +  let
    9.98      val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd pre_intros))))
    9.99      (* preprocessing *)
   9.100      val intros = ind_set_codegen_preproc thy (map (preprocess_intro thy) pre_intros)
   9.101      val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim)
   9.102    in
   9.103 -    PredData.map
   9.104 +    if not (member (op =) (Graph.keys (PredData.get thy)) name) then
   9.105 +      PredData.map
   9.106        (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy
   9.107 +    else thy
   9.108    end
   9.109  
   9.110 +fun register_intros pre_intros thy =
   9.111 +  let
   9.112 +  val (_, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros))))
   9.113 +  val nparams = guess_nparams T
   9.114 +  val pre_elim = 
   9.115 +    (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy)))
   9.116 +    (mk_casesrule (ProofContext.init thy) nparams pre_intros)
   9.117 +  in register_predicate (pre_intros, pre_elim, nparams) thy end
   9.118 +
   9.119  fun set_generator_name pred mode name = 
   9.120    let
   9.121      val set = (apsnd o apsnd3 o cons) (mode, mk_function_data (name, NONE))
   9.122 @@ -864,7 +902,7 @@
   9.123         in merge (map (fn ks => i::ks) is) is end
   9.124       else [[]];
   9.125       
   9.126 -(* FIXME: should be in library - map_prod *)
   9.127 +(* FIXME: should be in library - cprod = map_prod I *)
   9.128  fun cprod ([], ys) = []
   9.129    | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
   9.130  
   9.131 @@ -986,7 +1024,9 @@
   9.132      (Generator (v, T), Mode (([], []), [], []))
   9.133    end;
   9.134  
   9.135 -fun gen_prem (Prem (us, t)) = GeneratorPrem (us, t) 
   9.136 +fun gen_prem (Prem (us, t)) = GeneratorPrem (us, t)
   9.137 +  | gen_prem (Negprem (us, t)) = error "it is a negated prem"
   9.138 +  | gen_prem (Sidecond t) = error "it is a sidecond"
   9.139    | gen_prem _ = error "gen_prem : invalid input for gen_prem"
   9.140  
   9.141  fun param_gen_prem param_vs (p as Prem (us, t as Free (v, _))) =
   9.142 @@ -997,6 +1037,11 @@
   9.143    
   9.144  fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
   9.145    let
   9.146 +    (*
   9.147 +  val _ = Output.tracing ("param_vs:" ^ commas param_vs)
   9.148 +  val _ = Output.tracing ("iss:" ^
   9.149 +    commas (map (fn is => case is of SOME is => string_of_smode is | NONE => "NONE") iss))
   9.150 +    *)
   9.151      val modes' = modes @ List.mapPartial
   9.152        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
   9.153          (param_vs ~~ iss);
   9.154 @@ -1010,7 +1055,7 @@
   9.155            NONE =>
   9.156              (if with_generator then
   9.157                (case select_mode_prem thy gen_modes' vs ps of
   9.158 -                  SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
   9.159 +                SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
   9.160                    (case p of Prem (us, _) => vs union terms_vs us | _ => vs)
   9.161                    (filter_out (equal p) ps)
   9.162                  | NONE =>
   9.163 @@ -1021,7 +1066,10 @@
   9.164                        (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of
   9.165                        SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
   9.166                          (vs union generator_vs) ps
   9.167 -                    | NONE => NONE
   9.168 +                    | NONE => let
   9.169 +                    val _ = Output.tracing ("ps:" ^ (commas
   9.170 +                    (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
   9.171 +                      in error "mode analysis failed" end
   9.172                    end)
   9.173              else
   9.174                NONE)
   9.175 @@ -1493,9 +1541,6 @@
   9.176    val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
   9.177    val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
   9.178    val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
   9.179 -	val _ = Output.tracing (Display.string_of_thm_global thy elimthm)
   9.180 -	val _ = Output.tracing (Display.string_of_thm_global thy introthm)
   9.181 -
   9.182  in
   9.183    (introthm, elimthm)
   9.184  end;
   9.185 @@ -1609,13 +1654,11 @@
   9.186          (list_comb (Const (name, T), xparams' @ xargs)))
   9.187        val lhs = list_comb (Const (mode_cname, funT), xparams @ xins)
   9.188        val def = Logic.mk_equals (lhs, predterm)
   9.189 -			val _ = Output.tracing ("def:" ^ (Syntax.string_of_term_global thy def))
   9.190        val ([definition], thy') = thy |>
   9.191          Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
   9.192          PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
   9.193        val (intro, elim) =
   9.194          create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
   9.195 -			val _ = Output.tracing (Display.string_of_thm_global thy' definition)
   9.196        in thy'
   9.197  			  |> add_predfun name mode (mode_cname, definition, intro, elim)
   9.198          |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
   9.199 @@ -2120,7 +2163,8 @@
   9.200              case HOLogic.strip_tupleT U of
   9.201                [] => [(i + 1, NONE)]
   9.202              | [U] => [(i + 1, NONE)]
   9.203 -	    | Us =>  map (pair (i + 1) o SOME) ((subsets 1 (length Us)) \\ [[], 1 upto (length Us)]))
   9.204 +            | Us =>  (i + 1, NONE) ::
   9.205 +              (map (pair (i + 1) o SOME) ((subsets 1 (length Us)) \\ [[], 1 upto (length Us)])))
   9.206            Ts)
   9.207        in
   9.208          cprod (cprods (map (fn T => case strip_type T of
   9.209 @@ -2220,41 +2264,30 @@
   9.210  
   9.211  (** user interface **)
   9.212  
   9.213 -(* generation of case rules from user-given introduction rules *)
   9.214 -
   9.215 -fun mk_casesrule ctxt nparams introrules =
   9.216 -  let
   9.217 -    val intros = map (Logic.unvarify o prop_of) introrules
   9.218 -    val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
   9.219 -    val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
   9.220 -    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
   9.221 -    val (argnames, ctxt2) = Variable.variant_fixes
   9.222 -      (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
   9.223 -    val argvs = map2 (curry Free) argnames (map fastype_of args)
   9.224 -    fun mk_case intro =
   9.225 -      let
   9.226 -        val (_, (_, args)) = strip_intro_concl nparams intro
   9.227 -        val prems = Logic.strip_imp_prems intro
   9.228 -        val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
   9.229 -        val frees = (fold o fold_aterms)
   9.230 -          (fn t as Free _ =>
   9.231 -              if member (op aconv) params t then I else insert (op aconv) t
   9.232 -           | _ => I) (args @ prems) []
   9.233 -      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
   9.234 -    val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
   9.235 -    val cases = map mk_case intros
   9.236 -  in Logic.list_implies (assm :: cases, prop) end;
   9.237 -
   9.238  (* code_pred_intro attribute *)
   9.239  
   9.240  fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   9.241  
   9.242  val code_pred_intros_attrib = attrib add_intro;
   9.243  
   9.244 -local
   9.245 +
   9.246 +(*FIXME
   9.247 +- Naming of auxiliary rules necessary?
   9.248 +- add default code equations P x y z = P_i_i_i x y z
   9.249 +*)
   9.250 +
   9.251 +val setup = PredData.put (Graph.empty) #>
   9.252 +  Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
   9.253 +    "adding alternative introduction rules for code generation of inductive predicates"
   9.254 +(*  Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib)
   9.255 +    "adding alternative elimination rules for code generation of inductive predicates";
   9.256 +    *)
   9.257 +  (*FIXME name discrepancy in attribs and ML code*)
   9.258 +  (*FIXME intros should be better named intro*)
   9.259 +  (*FIXME why distinguished attribute for cases?*)
   9.260  
   9.261  (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
   9.262 -fun generic_code_pred prep_const raw_const lthy =
   9.263 +fun generic_code_pred prep_const rpred raw_const lthy =
   9.264    let
   9.265      val thy = ProofContext.theory_of lthy
   9.266      val const = prep_const thy raw_const
   9.267 @@ -2282,40 +2315,18 @@
   9.268          val global_thms = ProofContext.export goal_ctxt
   9.269            (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
   9.270        in
   9.271 -        goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #> add_equations [const])
   9.272 +        goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #>
   9.273 +          (if rpred then
   9.274 +          (add_sizelim_equations [const] #> add_quickcheck_equations [const])
   9.275 +        else add_equations [const]))
   9.276        end  
   9.277    in
   9.278      Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
   9.279    end;
   9.280  
   9.281 -structure P = OuterParse
   9.282 -
   9.283 -in
   9.284 -
   9.285  val code_pred = generic_code_pred (K I);
   9.286  val code_pred_cmd = generic_code_pred Code.read_const
   9.287  
   9.288 -val setup = PredData.put (Graph.empty) #>
   9.289 -  Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
   9.290 -    "adding alternative introduction rules for code generation of inductive predicates"
   9.291 -(*  Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib)
   9.292 -    "adding alternative elimination rules for code generation of inductive predicates";
   9.293 -    *)
   9.294 -  (*FIXME name discrepancy in attribs and ML code*)
   9.295 -  (*FIXME intros should be better named intro*)
   9.296 -  (*FIXME why distinguished attribute for cases?*)
   9.297 -
   9.298 -val _ = OuterSyntax.local_theory_to_proof "code_pred"
   9.299 -  "prove equations for predicate specified by intro/elim rules"
   9.300 -  OuterKeyword.thy_goal (P.term_group >> code_pred_cmd)
   9.301 -
   9.302 -end
   9.303 -
   9.304 -(*FIXME
   9.305 -- Naming of auxiliary rules necessary?
   9.306 -- add default code equations P x y z = P_i_i_i x y z
   9.307 -*)
   9.308 -
   9.309  (* transformation for code generation *)
   9.310  
   9.311  val eval_ref = ref (NONE : (unit -> term Predicate.pred) option);
   9.312 @@ -2342,7 +2353,8 @@
   9.313                  ^ Syntax.string_of_term_global thy t_compr); m);
   9.314      val (inargs, outargs) = split_smode user_mode' args;
   9.315      val t_pred = list_comb (compile_expr NONE thy (m, list_comb (pred, params)), inargs);
   9.316 -    val t_eval = if null outargs then t_pred else let
   9.317 +    val t_eval = if null outargs then t_pred else
   9.318 +      let
   9.319          val outargs_bounds = map (fn Bound i => i) outargs;
   9.320          val outargsTs = map (nth Ts) outargs_bounds;
   9.321          val T_pred = HOLogic.mk_tupleT outargsTs;
   9.322 @@ -2361,7 +2373,7 @@
   9.323      val t = analyze_compr thy t_compr;
   9.324      val T = dest_predT PredicateCompFuns.compfuns (fastype_of t);
   9.325      val t' = mk_map PredicateCompFuns.compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
   9.326 -  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
   9.327 +  in (T, Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []) end;
   9.328  
   9.329  fun values ctxt k t_compr =
   9.330    let
    10.1 --- a/src/HOL/ex/Predicate_Compile.thy	Wed Sep 23 16:20:12 2009 +0200
    10.2 +++ b/src/HOL/ex/Predicate_Compile.thy	Wed Sep 23 16:20:12 2009 +0200
    10.3 @@ -1,6 +1,13 @@
    10.4  theory Predicate_Compile
    10.5  imports Complex_Main RPred
    10.6 -uses "../Tools/Predicate_Compile/predicate_compile_core.ML"
    10.7 +uses
    10.8 +  "../Tools/Predicate_Compile/pred_compile_aux.ML"
    10.9 +  "../Tools/Predicate_Compile/predicate_compile_core.ML"
   10.10 +  "../Tools/Predicate_Compile/pred_compile_set.ML"
   10.11 +  "../Tools/Predicate_Compile/pred_compile_data.ML"
   10.12 +  "../Tools/Predicate_Compile/pred_compile_fun.ML"
   10.13 +  "../Tools/Predicate_Compile/pred_compile_pred.ML"
   10.14 +  "../Tools/Predicate_Compile/predicate_compile.ML"
   10.15  begin
   10.16  
   10.17  setup {* Predicate_Compile.setup *}
    11.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
    11.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
    11.3 @@ -22,8 +22,10 @@
    11.4    | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
    11.5  
    11.6  code_pred append .
    11.7 +code_pred (inductify_all) (rpred) append .
    11.8  
    11.9  thm append.equation
   11.10 +thm append.rpred_equation
   11.11  
   11.12  values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
   11.13  values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
   11.14 @@ -44,11 +46,27 @@
   11.15      "partition f [] [] []"
   11.16    | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
   11.17    | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
   11.18 -ML {* set Toplevel.debug *} 
   11.19 +
   11.20  code_pred partition .
   11.21  
   11.22  thm partition.equation
   11.23  
   11.24 +
   11.25 +inductive member
   11.26 +for xs
   11.27 +where "x \<in> set xs ==> member xs x"
   11.28 +
   11.29 +lemma [code_pred_intros]:
   11.30 +  "member (x#xs') x"
   11.31 +by (auto intro: member.intros)
   11.32 +
   11.33 +lemma [code_pred_intros]:
   11.34 +"member xs x ==> member (x'#xs) x"
   11.35 +by (auto intro: member.intros elim!: member.cases)
   11.36 +(* strange bug must be repaired! *)
   11.37 +(*
   11.38 +code_pred member sorry
   11.39 +*)
   11.40  inductive is_even :: "nat \<Rightarrow> bool"
   11.41  where
   11.42    "n mod 2 = 0 \<Longrightarrow> is_even n"
   11.43 @@ -71,13 +89,9 @@
   11.44    from this converse_tranclpE[OF this(1)] show thesis by metis
   11.45  qed
   11.46  
   11.47 +code_pred (inductify_all) (rpred) tranclp .
   11.48  thm tranclp.equation
   11.49 -(*
   11.50 -setup {* Predicate_Compile.add_sizelim_equations [@{const_name tranclp}] *}
   11.51 -setup {* fn thy => exception_trace (fn () => Predicate_Compile.add_quickcheck_equations [@{const_name tranclp}] thy)  *}
   11.52 -
   11.53  thm tranclp.rpred_equation
   11.54 -*)
   11.55  
   11.56  inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   11.57      "succ 0 1"
   11.58 @@ -157,6 +171,7 @@
   11.59  values 3 "{(a,q). step (par nil nil) a q}"
   11.60  *)
   11.61  
   11.62 +subsection {* divmod *}
   11.63  
   11.64  inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
   11.65      "k < l \<Longrightarrow> divmod_rel k l 0 k"
   11.66 @@ -166,4 +181,75 @@
   11.67  
   11.68  value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)"
   11.69  
   11.70 +subsection {* Executing definitions *}
   11.71 +
   11.72 +definition Min
   11.73 +where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
   11.74 +
   11.75 +code_pred (inductify_all) Min .
   11.76 +
   11.77 +code_pred (inductify_all) lexord .
   11.78 +
   11.79 +thm lexord.equation
   11.80 +
   11.81 +
   11.82 +lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
   11.83 +
   11.84 +code_pred (inductify_all) lexn .
   11.85 +thm lexn.equation
   11.86 +
   11.87 +code_pred (inductify_all) lenlex .
   11.88 +thm lenlex.equation
   11.89 +(*
   11.90 +code_pred (inductify_all) (rpred) lenlex .
   11.91 +thm lenlex.rpred_equation
   11.92 +*)
   11.93 +
   11.94 +datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
   11.95 +fun height :: "'a tree => nat" where
   11.96 +"height ET = 0"
   11.97 +| "height (MKT x l r h) = max (height l) (height r) + 1"
   11.98 +
   11.99 +consts avl :: "'a tree => bool"
  11.100 +primrec
  11.101 +  "avl ET = True"
  11.102 +  "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
  11.103 +  h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
  11.104 +
  11.105 +code_pred (inductify_all) avl .
  11.106 +thm avl.equation
  11.107 +
  11.108 +fun set_of
  11.109 +where
  11.110 +"set_of ET = {}"
  11.111 +| "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
  11.112 +
  11.113 +fun is_ord
  11.114 +where
  11.115 +"is_ord ET = True"
  11.116 +| "is_ord (MKT n l r h) =
  11.117 + ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
  11.118 +
  11.119 +declare Un_def[code_pred_def]
  11.120 +
  11.121 +lemma [code_pred_inline]: "bot_fun_inst.bot_fun == (\<lambda>(y::'a::type). False)"
  11.122 +unfolding bot_fun_inst.bot_fun[symmetric]
  11.123 +unfolding bot_bool_eq[symmetric]
  11.124 +unfolding bot_fun_eq by simp
  11.125 +
  11.126 +code_pred (inductify_all) set_of .
  11.127 +thm set_of.equation
  11.128 +
  11.129 +code_pred (inductify_all) is_ord .
  11.130 +thm is_ord.equation
  11.131 +
  11.132 +section {* Definitions about Relations *}
  11.133 +
  11.134 +code_pred (inductify_all) converse .
  11.135 +thm converse.equation
  11.136 +
  11.137 +code_pred (inductify_all) Domain .
  11.138 +thm Domain.equation
  11.139 +
  11.140 +
  11.141  end
  11.142 \ No newline at end of file