1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Jul 16 21:17:12 2007 +0200
1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Jul 16 21:22:43 2007 +0200
1.3 @@ -26,14 +26,6 @@
1.4 val rel_name = suffix "_rel"
1.5 val dom_name = suffix "_dom"
1.6
1.7 -type depgraph = int IntGraph.T
1.8 -
1.9 -datatype ctx_tree
1.10 - = Leaf of term
1.11 - | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
1.12 - | RCall of (term * ctx_tree)
1.13 -
1.14 -
1.15
1.16 datatype fundef_result =
1.17 FundefResult of
1.18 @@ -58,6 +50,7 @@
1.19 {
1.20 defname : string,
1.21
1.22 + (* contains no logical entities: invariant under morphisms *)
1.23 add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
1.24
1.25 fs : term list,
1.26 @@ -73,7 +66,7 @@
1.27 val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
1.28 val name = Morphism.name phi
1.29 in
1.30 - FundefCtxData { add_simps = add_simps (* contains no logical entities *),
1.31 + FundefCtxData { add_simps = add_simps,
1.32 fs = map term fs, R = term R, psimps = fact psimps,
1.33 pinducts = fact pinducts, termination = thm termination,
1.34 defname = name defname }
1.35 @@ -154,7 +147,6 @@
1.36 FundefData.map (fold (fn f => NetRules.insert (f, data)) fs)
1.37 #> store_termination_rule termination
1.38
1.39 -
1.40 (* Configuration management *)
1.41 datatype fundef_opt
1.42 = Sequential
1.43 @@ -186,6 +178,10 @@
1.44
1.45 fun target_of (FundefConfig {target, ...}) = target
1.46
1.47 +val default_config = FundefConfig { sequential=false, default="%x. arbitrary",
1.48 + target=NONE, domintros=false, tailrec=false }
1.49 +
1.50 +
1.51 (* Common operations on equations *)
1.52
1.53 fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
1.54 @@ -248,7 +244,7 @@
1.55 val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
1.56 ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
1.57
1.58 - val _ = forall (FundefLib.forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs
1.59 + val _ = forall (not o Term.exists_subterm (fn Free (n, _) => n mem fnames | _ => false)) gs
1.60 orelse error (input_error "Recursive Calls not allowed in premises")
1.61 in
1.62 fqgar
1.63 @@ -265,14 +261,23 @@
1.64
1.65 type fixes = ((string * typ) * mixfix) list
1.66 type 'a spec = ((bstring * Attrib.src list) * 'a list) list
1.67 -type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec -> (term list * (thm list -> thm spec))
1.68 +type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec
1.69 + -> (term list * (thm list -> thm spec) * (thm list -> thm list list))
1.70 +
1.71 +val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
1.72
1.73 fun empty_preproc check _ _ ctxt fixes spec =
1.74 let
1.75 val (nas,tss) = split_list spec
1.76 val _ = check ctxt fixes (flat tss)
1.77 + val ts = flat tss
1.78 + val fnames = map (fst o fst) fixes
1.79 + val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
1.80 +
1.81 + fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
1.82 + |> map (map snd)
1.83 in
1.84 - (flat tss, curry op ~~ nas o Library.unflat tss)
1.85 + (ts, curry op ~~ nas o Library.unflat tss, sort)
1.86 end
1.87
1.88 structure Preprocessor = GenericDataFun
1.89 @@ -313,44 +318,11 @@
1.90
1.91 val flags_statements = statements_ow
1.92 >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
1.93 -
1.94 - fun basic_apply_flags ((config, fixes), (flags, statements)) = ((config, fixes), statements)
1.95 in
1.96 fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements)
1.97 -
1.98 end
1.99
1.100
1.101 -
1.102 -
1.103 -
1.104 -val default_config = FundefConfig { sequential=false, default="%x. arbitrary",
1.105 - target=NONE, domintros=false, tailrec=false }
1.106 -
1.107 -
1.108 end
1.109 end
1.110
1.111 -(* Common Abbreviations *)
1.112 -
1.113 -structure FundefAbbrev =
1.114 -struct
1.115 -
1.116 -fun implies_elim_swp x y = implies_elim y x
1.117 -
1.118 -(* HOL abbreviations *)
1.119 -val boolT = HOLogic.boolT
1.120 -val mk_prod = HOLogic.mk_prod
1.121 -val mk_eq = HOLogic.mk_eq
1.122 -val eq_const = HOLogic.eq_const
1.123 -val Trueprop = HOLogic.mk_Trueprop
1.124 -val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
1.125 -
1.126 -fun free_to_var (Free (v,T)) = Var ((v,0),T)
1.127 - | free_to_var _ = raise Match
1.128 -
1.129 -fun var_to_free (Var ((v,_),T)) = Free (v,T)
1.130 - | var_to_free _ = raise Match
1.131 -
1.132 -
1.133 -end