Major update to function package, including new syntax and the (only theoretical)
authorkrauss
Wed Sep 13 12:05:50 2006 +0200 (2006-09-13)
changeset 2052336a59e5d0039
parent 20522 05072ae0d435
child 20524 1493053fc111
Major update to function package, including new syntax and the (only theoretical)
ability to handle local contexts.
etc/isar-keywords.el
src/HOL/Datatype.thy
src/HOL/FunDef.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Integ/IntArith.thy
src/HOL/Isar_examples/ExprCompiler.thy
src/HOL/Lattice/Lattice.thy
src/HOL/Lattice/Orders.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/function_package/fundef_proof.ML
src/HOL/Tools/function_package/inductive_wrap.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/function_package/pattern_split.ML
src/HOL/Tools/function_package/sum_tools.ML
src/HOL/Tools/function_package/termination.ML
src/HOL/W0/W0.thy
src/HOL/ex/CodeCollections.thy
src/HOL/ex/CodeOperationalEquality.thy
src/HOL/ex/Fundefs.thy
src/HOL/ex/Higher_Order_Logic.thy
src/HOL/ex/NormalForm.thy
src/HOLCF/Ffun.thy
src/Pure/Tools/codegen_theorems.ML
     1.1 --- a/etc/isar-keywords.el	Wed Sep 13 00:38:38 2006 +0200
     1.2 +++ b/etc/isar-keywords.el	Wed Sep 13 12:05:50 2006 +0200
     1.3 @@ -46,12 +46,10 @@
     1.4      "code_const"
     1.5      "code_constname"
     1.6      "code_gen"
     1.7 -    "code_generate"
     1.8      "code_instance"
     1.9      "code_library"
    1.10      "code_module"
    1.11      "code_purge"
    1.12 -    "code_serialize"
    1.13      "code_simtype"
    1.14      "code_type"
    1.15      "code_typename"
    1.16 @@ -89,6 +87,7 @@
    1.17      "fixrec"
    1.18      "from"
    1.19      "full_prf"
    1.20 +    "fun"
    1.21      "function"
    1.22      "global"
    1.23      "guess"
    1.24 @@ -393,12 +392,10 @@
    1.25      "code_const"
    1.26      "code_constname"
    1.27      "code_gen"
    1.28 -    "code_generate"
    1.29      "code_instance"
    1.30      "code_library"
    1.31      "code_module"
    1.32      "code_purge"
    1.33 -    "code_serialize"
    1.34      "code_type"
    1.35      "code_typename"
    1.36      "coinductive"
    1.37 @@ -417,6 +414,7 @@
    1.38      "finalconsts"
    1.39      "fixpat"
    1.40      "fixrec"
    1.41 +    "fun"
    1.42      "global"
    1.43      "hide"
    1.44      "inductive"
     2.1 --- a/src/HOL/Datatype.thy	Wed Sep 13 00:38:38 2006 +0200
     2.2 +++ b/src/HOL/Datatype.thy	Wed Sep 13 12:05:50 2006 +0200
     2.3 @@ -233,27 +233,27 @@
     2.4  
     2.5  lemmas [code] = imp_conv_disj
     2.6  
     2.7 -lemma [code fun]:
     2.8 +lemma [code func]:
     2.9    "(\<not> True) = False" by (rule HOL.simp_thms)
    2.10  
    2.11 -lemma [code fun]:
    2.12 +lemma [code func]:
    2.13    "(\<not> False) = True" by (rule HOL.simp_thms)
    2.14  
    2.15 -lemma [code fun]:
    2.16 +lemma [code func]:
    2.17    shows "(False \<and> x) = False"
    2.18    and   "(True \<and> x) = x"
    2.19    and   "(x \<and> False) = False"
    2.20    and   "(x \<and> True) = x" by simp_all
    2.21  
    2.22 -lemma [code fun]:
    2.23 +lemma [code func]:
    2.24    shows "(False \<or> x) = x"
    2.25    and   "(True \<or> x) = True"
    2.26    and   "(x \<or> False) = x"
    2.27    and   "(x \<or> True) = True" by simp_all
    2.28  
    2.29  declare
    2.30 -  if_True [code fun]
    2.31 -  if_False [code fun]
    2.32 +  if_True [code func]
    2.33 +  if_False [code func]
    2.34    fst_conv [code]
    2.35    snd_conv [code]
    2.36  
     3.1 --- a/src/HOL/FunDef.thy	Wed Sep 13 00:38:38 2006 +0200
     3.2 +++ b/src/HOL/FunDef.thy	Wed Sep 13 12:05:50 2006 +0200
     3.3 @@ -11,6 +11,7 @@
     3.4  ("Tools/function_package/sum_tools.ML")
     3.5  ("Tools/function_package/fundef_common.ML")
     3.6  ("Tools/function_package/fundef_lib.ML")
     3.7 +("Tools/function_package/inductive_wrap.ML")
     3.8  ("Tools/function_package/context_tree.ML")
     3.9  ("Tools/function_package/fundef_prep.ML")
    3.10  ("Tools/function_package/fundef_proof.ML")
    3.11 @@ -23,20 +24,20 @@
    3.12  begin
    3.13  
    3.14  lemma fundef_ex1_existence:
    3.15 -assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
    3.16 +assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
    3.17  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    3.18  shows "(x, f x)\<in>G"
    3.19    by (simp only:f_def, rule theI', rule ex1)
    3.20  
    3.21  lemma fundef_ex1_uniqueness:
    3.22 -assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
    3.23 +assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
    3.24  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    3.25  assumes elm: "(x, h x)\<in>G"
    3.26  shows "h x = f x"
    3.27    by (simp only:f_def, rule the1_equality[symmetric], rule ex1, rule elm)
    3.28  
    3.29  lemma fundef_ex1_iff:
    3.30 -assumes f_def: "\<And>x. f x \<equiv> THE y. (x,y)\<in>G"
    3.31 +assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
    3.32  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    3.33  shows "((x, y)\<in>G) = (f x = y)"
    3.34    apply (auto simp:ex1 f_def the1_equality)
    3.35 @@ -71,6 +72,7 @@
    3.36  use "Tools/function_package/sum_tools.ML"
    3.37  use "Tools/function_package/fundef_common.ML"
    3.38  use "Tools/function_package/fundef_lib.ML"
    3.39 +use "Tools/function_package/inductive_wrap.ML"
    3.40  use "Tools/function_package/context_tree.ML"
    3.41  use "Tools/function_package/fundef_prep.ML"
    3.42  use "Tools/function_package/fundef_proof.ML"
     4.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Wed Sep 13 00:38:38 2006 +0200
     4.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Wed Sep 13 12:05:50 2006 +0200
     4.3 @@ -351,7 +351,7 @@
     4.4  subsection{*Injectivity of @{term FnCall}*}
     4.5  
     4.6  definition
     4.7 -  fun :: "exp \<Rightarrow> nat"
     4.8 +  "fun" :: "exp \<Rightarrow> nat"
     4.9    "fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
    4.10  
    4.11  lemma fun_respects: "(%U. {freefun U}) respects exprel"
     5.1 --- a/src/HOL/Integ/IntArith.thy	Wed Sep 13 00:38:38 2006 +0200
     5.2 +++ b/src/HOL/Integ/IntArith.thy	Wed Sep 13 12:05:50 2006 +0200
     5.3 @@ -376,23 +376,23 @@
     5.4    "Numeral.B1" "IntDef.b1"
     5.5  
     5.6  lemma
     5.7 -  Numeral_Pls_refl [code fun]: "Numeral.Pls = Numeral.Pls" ..
     5.8 +  Numeral_Pls_refl [code func]: "Numeral.Pls = Numeral.Pls" ..
     5.9  
    5.10  lemma
    5.11 -  Numeral_Min_refl [code fun]: "Numeral.Min = Numeral.Min" ..
    5.12 +  Numeral_Min_refl [code func]: "Numeral.Min = Numeral.Min" ..
    5.13  
    5.14  lemma
    5.15 -  Numeral_Bit_refl [code fun]: "Numeral.Bit = Numeral.Bit" ..
    5.16 +  Numeral_Bit_refl [code func]: "Numeral.Bit = Numeral.Bit" ..
    5.17  
    5.18 -lemma zero_is_num_zero [code fun, code inline]:
    5.19 +lemma zero_is_num_zero [code func, code inline]:
    5.20    "(0::int) = Numeral.Pls" 
    5.21    unfolding Pls_def ..
    5.22  
    5.23 -lemma one_is_num_one [code fun, code inline]:
    5.24 +lemma one_is_num_one [code func, code inline]:
    5.25    "(1::int) = Numeral.Pls BIT bit.B1" 
    5.26    unfolding Pls_def Bit_def by simp 
    5.27  
    5.28 -lemma number_of_is_id [code fun, code inline]:
    5.29 +lemma number_of_is_id [code func, code inline]:
    5.30    "number_of (k::int) = k"
    5.31    unfolding int_number_of_def by simp
    5.32  
     6.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Wed Sep 13 00:38:38 2006 +0200
     6.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Wed Sep 13 12:05:50 2006 +0200
     6.3 @@ -173,14 +173,14 @@
     6.4      case (Load adr)
     6.5      from Cons show ?case by simp -- {* same as above *}
     6.6    next
     6.7 -    case (Apply fun)
     6.8 -    have "exec ((Apply fun # xs) @ ys) s env =
     6.9 -        exec (Apply fun # xs @ ys) s env" by simp
    6.10 +    case (Apply fn)
    6.11 +    have "exec ((Apply fn # xs) @ ys) s env =
    6.12 +        exec (Apply fn # xs @ ys) s env" by simp
    6.13      also have "... =
    6.14 -        exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
    6.15 +        exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
    6.16      also from Cons have "... =
    6.17 -        exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env" .
    6.18 -    also have "... = exec ys (exec (Apply fun # xs) s env) env" by simp
    6.19 +        exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .
    6.20 +    also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp
    6.21      finally show ?case .
    6.22    qed
    6.23  qed
    6.24 @@ -199,19 +199,19 @@
    6.25      case (Constant val s)
    6.26      show ?case by simp -- {* same as above *}
    6.27    next
    6.28 -    case (Binop fun e1 e2 s)
    6.29 -    have "exec (compile (Binop fun e1 e2)) s env =
    6.30 -        exec (compile e2 @ compile e1 @ [Apply fun]) s env" by simp
    6.31 -    also have "... = exec [Apply fun]
    6.32 +    case (Binop fn e1 e2 s)
    6.33 +    have "exec (compile (Binop fn e1 e2)) s env =
    6.34 +        exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp
    6.35 +    also have "... = exec [Apply fn]
    6.36          (exec (compile e1) (exec (compile e2) s env) env) env"
    6.37        by (simp only: exec_append)
    6.38      also have "exec (compile e2) s env = eval e2 env # s" by fact
    6.39      also have "exec (compile e1) ... env = eval e1 env # ..." by fact
    6.40 -    also have "exec [Apply fun] ... env =
    6.41 -        fun (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
    6.42 -    also have "... = fun (eval e1 env) (eval e2 env) # s" by simp
    6.43 -    also have "fun (eval e1 env) (eval e2 env) =
    6.44 -        eval (Binop fun e1 e2) env"
    6.45 +    also have "exec [Apply fn] ... env =
    6.46 +        fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
    6.47 +    also have "... = fn (eval e1 env) (eval e2 env) # s" by simp
    6.48 +    also have "fn (eval e1 env) (eval e2 env) =
    6.49 +        eval (Binop fn e1 e2) env"
    6.50        by simp
    6.51      finally show ?case .
    6.52    qed
     7.1 --- a/src/HOL/Lattice/Lattice.thy	Wed Sep 13 00:38:38 2006 +0200
     7.2 +++ b/src/HOL/Lattice/Lattice.thy	Wed Sep 13 12:05:50 2006 +0200
     7.3 @@ -519,7 +519,7 @@
     7.4    qed
     7.5  qed
     7.6  
     7.7 -instance fun :: (type, lattice) lattice
     7.8 +instance "fun" :: (type, lattice) lattice
     7.9  proof
    7.10    fix f g :: "'a \<Rightarrow> 'b::lattice"
    7.11    show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)
     8.1 --- a/src/HOL/Lattice/Orders.thy	Wed Sep 13 00:38:38 2006 +0200
     8.2 +++ b/src/HOL/Lattice/Orders.thy	Wed Sep 13 12:05:50 2006 +0200
     8.3 @@ -249,7 +249,7 @@
     8.4    orders need \emph{not} be linear in general.
     8.5  *}
     8.6  
     8.7 -instance fun :: (type, leq) leq ..
     8.8 +instance "fun" :: (type, leq) leq ..
     8.9  
    8.10  defs (overloaded)
    8.11    leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
    8.12 @@ -260,7 +260,7 @@
    8.13  lemma leq_funD [dest?]: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
    8.14    by (unfold leq_fun_def) blast
    8.15  
    8.16 -instance fun :: (type, quasi_order) quasi_order
    8.17 +instance "fun" :: (type, quasi_order) quasi_order
    8.18  proof
    8.19    fix f g h :: "'a \<Rightarrow> 'b::quasi_order"
    8.20    show "f \<sqsubseteq> f"
    8.21 @@ -276,7 +276,7 @@
    8.22    qed
    8.23  qed
    8.24  
    8.25 -instance fun :: (type, partial_order) partial_order
    8.26 +instance "fun" :: (type, partial_order) partial_order
    8.27  proof
    8.28    fix f g :: "'a \<Rightarrow> 'b::partial_order"
    8.29    assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"
     9.1 --- a/src/HOL/Library/EfficientNat.thy	Wed Sep 13 00:38:38 2006 +0200
     9.2 +++ b/src/HOL/Library/EfficientNat.thy	Wed Sep 13 12:05:50 2006 +0200
     9.3 @@ -112,23 +112,23 @@
     9.4  lemma [code]: "(m < n) = (int m < int n)"
     9.5    by simp
     9.6  
     9.7 -lemma [code fun, code inline]: "m + n = nat_plus m n"
     9.8 +lemma [code func, code inline]: "m + n = nat_plus m n"
     9.9    unfolding nat_plus_def by arith
    9.10 -lemma [code fun, code inline]: "m - n = nat_minus m n"
    9.11 +lemma [code func, code inline]: "m - n = nat_minus m n"
    9.12    unfolding nat_minus_def by arith
    9.13 -lemma [code fun, code inline]: "m * n = nat_mult m n"
    9.14 +lemma [code func, code inline]: "m * n = nat_mult m n"
    9.15    unfolding nat_mult_def by (simp add: zmult_int)
    9.16 -lemma [code fun, code inline]: "m div n = nat_div m n"
    9.17 +lemma [code func, code inline]: "m div n = nat_div m n"
    9.18    unfolding nat_div_def div_def [symmetric] zdiv_int [symmetric] by simp
    9.19 -lemma [code fun, code inline]: "m mod n = nat_mod m n"
    9.20 +lemma [code func, code inline]: "m mod n = nat_mod m n"
    9.21    unfolding nat_mod_def mod_def [symmetric] zmod_int [symmetric] by simp
    9.22 -lemma [code fun, code inline]: "(m < n) = nat_less m n"
    9.23 +lemma [code func, code inline]: "(m < n) = nat_less m n"
    9.24    unfolding nat_less_def by simp
    9.25 -lemma [code fun, code inline]: "(m <= n) = nat_less_equal m n"
    9.26 +lemma [code func, code inline]: "(m <= n) = nat_less_equal m n"
    9.27    unfolding nat_less_equal_def by simp
    9.28 -lemma [code fun, code inline]: "(m = n) = nat_eq m n"
    9.29 +lemma [code func, code inline]: "(m = n) = nat_eq m n"
    9.30    unfolding nat_eq_def by simp
    9.31 -lemma [code fun]:
    9.32 +lemma [code func]:
    9.33    "int_aux i n = (if nat_eq n 0 then i else int_aux (i + 1) (nat_minus n 1))"
    9.34    unfolding nat_eq_def nat_minus_def int_aux_def by simp
    9.35  
    10.1 --- a/src/HOL/Library/ExecutableSet.thy	Wed Sep 13 00:38:38 2006 +0200
    10.2 +++ b/src/HOL/Library/ExecutableSet.thy	Wed Sep 13 12:05:50 2006 +0200
    10.3 @@ -84,51 +84,55 @@
    10.4  
    10.5  subsection {* Derived definitions *}
    10.6  
    10.7 -consts
    10.8 -  unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    10.9 -  intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   10.10 -  subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   10.11 -  map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   10.12 -  unions :: "'a list list \<Rightarrow> 'a list"
   10.13 -  intersects :: "'a list list \<Rightarrow> 'a list"
   10.14  
   10.15 -function
   10.16 +function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   10.17 +where
   10.18    "unionl [] ys = ys"
   10.19 -  "unionl xs ys = foldr insertl xs ys"
   10.20 -  by pat_completeness auto
   10.21 +| "unionl xs ys = foldr insertl xs ys"
   10.22 +by pat_completeness auto
   10.23  termination unionl by (auto_term "{}")
   10.24  lemmas unionl_def = unionl.simps(2)
   10.25 +declare unionl.simps[code]
   10.26  
   10.27 -function
   10.28 +function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   10.29 +where
   10.30    "intersect [] ys = []"
   10.31 -  "intersect xs [] = []"
   10.32 -  "intersect xs ys = filter (member xs) ys"
   10.33 -  by pat_completeness simp_all
   10.34 +| "intersect xs [] = []"
   10.35 +| "intersect xs ys = filter (member xs) ys"
   10.36 +  by pat_completeness auto
   10.37  termination intersect by (auto_term "{}")
   10.38  lemmas intersect_def = intersect.simps(3)
   10.39 +declare intersect.simps[code]
   10.40  
   10.41 -function
   10.42 +function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   10.43 +where
   10.44    "subtract [] ys = ys"
   10.45 -  "subtract xs [] = []"
   10.46 -  "subtract xs ys = foldr remove1 xs ys"
   10.47 -  by pat_completeness simp_all
   10.48 +| "subtract xs [] = []"
   10.49 +| "subtract xs ys = foldr remove1 xs ys"
   10.50 +  by pat_completeness auto
   10.51  termination subtract by (auto_term "{}")
   10.52  lemmas subtract_def = subtract.simps(3)
   10.53 +declare subtract.simps[code]
   10.54  
   10.55 -function
   10.56 +function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   10.57 +where
   10.58    "map_distinct f [] = []"
   10.59 -  "map_distinct f xs = foldr (insertl o f) xs []"
   10.60 -  by pat_completeness simp_all
   10.61 +| "map_distinct f xs = foldr (insertl o f) xs []"
   10.62 +  by pat_completeness auto
   10.63  termination map_distinct by (auto_term "{}")
   10.64  lemmas map_distinct_def = map_distinct.simps(2)
   10.65 +declare map_distinct.simps[code]
   10.66  
   10.67 -function
   10.68 +function unions :: "'a list list \<Rightarrow> 'a list"
   10.69 +where
   10.70    "unions [] = []"
   10.71    "unions xs = foldr unionl xs []"
   10.72 -  by pat_completeness simp_all
   10.73 +  by pat_completeness auto
   10.74  termination unions by (auto_term "{}")
   10.75  lemmas unions_def = unions.simps(2)
   10.76 +declare unions.simps[code]
   10.77  
   10.78 +consts intersects :: "'a list list \<Rightarrow> 'a list"
   10.79  primrec
   10.80    "intersects (x#xs) = foldr intersect xs x"
   10.81  
   10.82 @@ -156,7 +160,8 @@
   10.83  
   10.84  lemma iso_union:
   10.85    "set (unionl xs ys) = set xs \<union> set ys"
   10.86 -  unfolding unionl_def by (induct xs arbitrary: ys) (simp_all add: iso_insert)
   10.87 +  unfolding unionl_def
   10.88 + by (induct xs arbitrary: ys) (simp_all add: iso_insert)
   10.89  
   10.90  lemma iso_intersect:
   10.91    "set (intersect xs ys) = set xs \<inter> set ys"
    11.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Wed Sep 13 00:38:38 2006 +0200
    11.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Wed Sep 13 12:05:50 2006 +0200
    11.3 @@ -18,33 +18,33 @@
    11.4  subsection {* Basic definitions *}
    11.5  
    11.6  instance set :: (plus) plus ..
    11.7 -instance fun :: (type, plus) plus ..
    11.8 +instance "fun" :: (type, plus) plus ..
    11.9  
   11.10  defs (overloaded)
   11.11    func_plus: "f + g == (%x. f x + g x)"
   11.12    set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}"
   11.13  
   11.14  instance set :: (times) times ..
   11.15 -instance fun :: (type, times) times ..
   11.16 +instance "fun" :: (type, times) times ..
   11.17  
   11.18  defs (overloaded)
   11.19    func_times: "f * g == (%x. f x * g x)"
   11.20    set_times:"A * B == {c. EX a:A. EX b:B. c = a * b}"
   11.21  
   11.22 -instance fun :: (type, minus) minus ..
   11.23 +instance "fun" :: (type, minus) minus ..
   11.24  
   11.25  defs (overloaded)
   11.26    func_minus: "- f == (%x. - f x)"
   11.27    func_diff: "f - g == %x. f x - g x"
   11.28  
   11.29 -instance fun :: (type, zero) zero ..
   11.30 +instance "fun" :: (type, zero) zero ..
   11.31  instance set :: (zero) zero ..
   11.32  
   11.33  defs (overloaded)
   11.34    func_zero: "0::(('a::type) => ('b::zero)) == %x. 0"
   11.35    set_zero: "0::('a::zero)set == {0}"
   11.36  
   11.37 -instance fun :: (type, one) one ..
   11.38 +instance "fun" :: (type, one) one ..
   11.39  instance set :: (one) one ..
   11.40  
   11.41  defs (overloaded)
   11.42 @@ -62,29 +62,29 @@
   11.43    elt_set_eq :: "'a => 'a set => bool"      (infix "=o" 50)
   11.44    "x =o A == x : A"
   11.45  
   11.46 -instance fun :: (type,semigroup_add)semigroup_add
   11.47 +instance "fun" :: (type,semigroup_add)semigroup_add
   11.48    by default (auto simp add: func_plus add_assoc)
   11.49  
   11.50 -instance fun :: (type,comm_monoid_add)comm_monoid_add
   11.51 +instance "fun" :: (type,comm_monoid_add)comm_monoid_add
   11.52    by default (auto simp add: func_zero func_plus add_ac)
   11.53  
   11.54 -instance fun :: (type,ab_group_add)ab_group_add
   11.55 +instance "fun" :: (type,ab_group_add)ab_group_add
   11.56    apply default
   11.57     apply (simp add: func_minus func_plus func_zero)
   11.58    apply (simp add: func_minus func_plus func_diff diff_minus)
   11.59    done
   11.60  
   11.61 -instance fun :: (type,semigroup_mult)semigroup_mult
   11.62 +instance "fun" :: (type,semigroup_mult)semigroup_mult
   11.63    apply default
   11.64    apply (auto simp add: func_times mult_assoc)
   11.65    done
   11.66  
   11.67 -instance fun :: (type,comm_monoid_mult)comm_monoid_mult
   11.68 +instance "fun" :: (type,comm_monoid_mult)comm_monoid_mult
   11.69    apply default
   11.70     apply (auto simp add: func_one func_times mult_ac)
   11.71    done
   11.72  
   11.73 -instance fun :: (type,comm_ring_1)comm_ring_1
   11.74 +instance "fun" :: (type,comm_ring_1)comm_ring_1
   11.75    apply default
   11.76     apply (auto simp add: func_plus func_times func_minus func_diff ext
   11.77       func_one func_zero ring_eq_simps)
    12.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Wed Sep 13 00:38:38 2006 +0200
    12.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Wed Sep 13 12:05:50 2006 +0200
    12.3 @@ -15,8 +15,11 @@
    12.4      val cong_deps : thm -> int IntGraph.T
    12.5      val add_congs : thm list
    12.6  
    12.7 -    val mk_tree: theory -> (thm * FundefCommon.depgraph) list ->
    12.8 -      term -> Proof.context -> term -> FundefCommon.ctx_tree
    12.9 +    val mk_tree: (thm * FundefCommon.depgraph) list ->
   12.10 +                 (string * typ) -> Proof.context -> term -> FundefCommon.ctx_tree
   12.11 +
   12.12 +    val inst_tree: theory -> term -> term -> FundefCommon.ctx_tree
   12.13 +                   -> FundefCommon.ctx_tree
   12.14  
   12.15      val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list
   12.16  
   12.17 @@ -32,7 +35,7 @@
   12.18     (((string * typ) list * thm list) * thm) list * 'b)
   12.19     -> FundefCommon.ctx_tree -> 'b -> 'b
   12.20  
   12.21 -    val rewrite_by_tree : theory -> 'a -> term -> thm -> (thm * thm) list -> FundefCommon.ctx_tree -> thm * (thm * thm) list
   12.22 +    val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> FundefCommon.ctx_tree -> thm * (thm * thm) list
   12.23  end
   12.24  
   12.25  structure FundefCtxTree : FUNDEF_CTXTREE =
   12.26 @@ -79,35 +82,61 @@
   12.27        (ctx', fixes, assumes, rhs_of term)
   12.28      end
   12.29  
   12.30 -fun find_cong_rule thy ctx ((r,dep)::rs) t =
   12.31 +fun find_cong_rule ctx ((r,dep)::rs) t =
   12.32      (let
   12.33  	val (c, subs) = (meta_rhs_of (concl_of r), prems_of r)
   12.34  
   12.35 -	val subst = Pattern.match thy (c, t) (Vartab.empty, Vartab.empty)
   12.36 +	val subst = Pattern.match (ProofContext.theory_of ctx) (c, t) (Vartab.empty, Vartab.empty)
   12.37  
   12.38  	val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
   12.39       in
   12.40  	 (r, dep, branches)
   12.41       end
   12.42 -    handle Pattern.MATCH => find_cong_rule thy ctx rs t)
   12.43 -  | find_cong_rule thy _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
   12.44 +    handle Pattern.MATCH => find_cong_rule ctx rs t)
   12.45 +  | find_cong_rule _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
   12.46  
   12.47  
   12.48 -fun matchcall f (a $ b) = if a = f then SOME b else NONE
   12.49 -  | matchcall f _ = NONE
   12.50 +fun matchcall fvar (a $ b) = if a = Free fvar then SOME b else NONE
   12.51 +  | matchcall fvar _ = NONE
   12.52 +
   12.53 +fun mk_tree congs fvar ctx t =
   12.54 +    case matchcall fvar t of
   12.55 +      SOME arg => RCall (t, mk_tree congs fvar ctx arg)
   12.56 +    | NONE => 
   12.57 +      if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t
   12.58 +      else 
   12.59 +	let val (r, dep, branches) = find_cong_rule ctx congs t in
   12.60 +	  Cong (t, r, dep, 
   12.61 +                map (fn (ctx', fixes, assumes, st) => 
   12.62 +			(fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes, 
   12.63 +                         mk_tree congs fvar ctx' st)) branches)
   12.64 +	end
   12.65 +		
   12.66  
   12.67 -fun mk_tree thy congs f ctx t =
   12.68 -    case matchcall f t of
   12.69 -	SOME arg => RCall (t, mk_tree thy congs f ctx arg)
   12.70 -      | NONE => 
   12.71 -	if not (exists_Const (curry op = (dest_Const f)) t) then Leaf t
   12.72 -	else 
   12.73 -	    let val (r, dep, branches) = find_cong_rule thy ctx congs t in
   12.74 -		Cong (t, r, dep, map (fn (ctx', fixes, assumes, st) => 
   12.75 -					 (fixes, map (assume o cterm_of thy) assumes, mk_tree thy congs f ctx' st)) branches)
   12.76 -	    end
   12.77 -		
   12.78 -		
   12.79 +fun inst_tree thy fvar f tr =
   12.80 +    let
   12.81 +      val cfvar = cterm_of thy fvar
   12.82 +      val cf = cterm_of thy f
   12.83 +               
   12.84 +      fun inst_term t = 
   12.85 +          subst_bound(f, abstract_over (fvar, t))
   12.86 +
   12.87 +      val inst_thm = forall_elim cf o forall_intr cfvar 
   12.88 +
   12.89 +      fun inst_tree_aux (Leaf t) = Leaf t
   12.90 +        | inst_tree_aux (Cong (t, crule, deps, branches)) =
   12.91 +          Cong (inst_term t, inst_thm crule, deps, map inst_branch branches)
   12.92 +        | inst_tree_aux (RCall (t, str)) =
   12.93 +          RCall (inst_term t, inst_tree_aux str)
   12.94 +      and inst_branch (fxs, assms, str) = 
   12.95 +          (fxs, map (assume o cterm_of thy o inst_term o prop_of) assms, inst_tree_aux str)
   12.96 +    in
   12.97 +      inst_tree_aux tr
   12.98 +    end
   12.99 +
  12.100 +
  12.101 +
  12.102 +(* FIXME: remove *)		
  12.103  fun add_context_varnames (Leaf _) = I
  12.104    | add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (curry op ins_string o fst) fs o add_context_varnames st) sub
  12.105    | add_context_varnames (RCall (_,st)) = add_context_varnames st
  12.106 @@ -185,7 +214,7 @@
  12.107  
  12.108  fun is_refl thm = let val (l,r) = Logic.dest_equals (prop_of thm) in l = r end
  12.109  
  12.110 -fun rewrite_by_tree thy f h ih x tr =
  12.111 +fun rewrite_by_tree thy h ih x tr =
  12.112      let
  12.113  	fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
  12.114  	  | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
    13.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Wed Sep 13 00:38:38 2006 +0200
    13.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Wed Sep 13 12:05:50 2006 +0200
    13.3 @@ -12,6 +12,8 @@
    13.4  (* Theory Dependencies *)
    13.5  val acc_const_name = "Accessible_Part.acc"
    13.6  
    13.7 +fun mk_acc domT R =
    13.8 +    Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R 
    13.9  
   13.10  
   13.11  type depgraph = int IntGraph.T
   13.12 @@ -25,17 +27,20 @@
   13.13  type glrs = (term list * term list * term * term) list
   13.14  
   13.15  
   13.16 -(* A record containing all the relevant symbols and types needed during the proof.
   13.17 -   This is set up at the beginning and does not change. *)
   13.18 -datatype naming_context =
   13.19 -   Names of { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ,
   13.20 -       G: term, R: term, acc_R: term, h: term, y: term, x: term, z: term, a:term, P: term, 
   13.21 -       D: term, Pbool:term,
   13.22 -       glrs: (term list * term list * term * term) list,
   13.23 -       glrs': (term list * term list * term * term) list,
   13.24 -       f_def: thm,
   13.25 -       ctx: Proof.context
   13.26 -     }
   13.27 +datatype globals =
   13.28 +   Globals of { 
   13.29 +         fvar: term, 
   13.30 +         domT: typ, 
   13.31 +         ranT: typ,
   13.32 +         h: term, 
   13.33 +         y: term, 
   13.34 +         x: term, 
   13.35 +         z: term, 
   13.36 +         a:term, 
   13.37 +         P: term, 
   13.38 +         D: term, 
   13.39 +         Pbool:term
   13.40 +}
   13.41  
   13.42  
   13.43  datatype rec_call_info = 
   13.44 @@ -46,70 +51,91 @@
   13.45     rcarg: term,                 (* The recursive argument *)
   13.46  
   13.47     llRI: thm,
   13.48 -   Gh: thm, 
   13.49 -   Gh': thm
   13.50 +   h_assum: term
   13.51    } 
   13.52 -     
   13.53 +
   13.54 +
   13.55 +datatype clause_context =
   13.56 +  ClauseContext of
   13.57 +  {
   13.58 +    ctxt : Proof.context,
   13.59 +
   13.60 +    qs : term list,
   13.61 +    gs : term list,
   13.62 +    lhs: term,
   13.63 +    rhs: term,
   13.64 +
   13.65 +    cqs: cterm list,
   13.66 +    ags: thm list,     
   13.67 +    case_hyp : thm
   13.68 +  }
   13.69 +
   13.70 +
   13.71 +fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
   13.72 +    ClauseContext { ctxt = ProofContext.transfer thy ctxt,
   13.73 +                    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
   13.74 +
   13.75 +
   13.76  datatype clause_info =
   13.77    ClauseInfo of 
   13.78       {
   13.79        no: int,
   13.80 +      qglr : ((string * typ) list * term list * term * term),
   13.81 +      cdata : clause_context,
   13.82  
   13.83        tree: ctx_tree,
   13.84 -      case_hyp: thm,
   13.85 -
   13.86 -      qs: term list, 
   13.87 -      gs: term list,
   13.88 -      lhs: term,
   13.89 -      rhs: term,
   13.90 -
   13.91 -      cqs: cterm list,
   13.92 -      ags: thm list,
   13.93 -      
   13.94 -      cqs': cterm list, 
   13.95 -      ags': thm list,
   13.96 -      lhs': term,
   13.97 -      rhs': term,
   13.98 -
   13.99        lGI: thm,
  13.100 -      RCs: rec_call_info list,
  13.101 -
  13.102 -      ordcqs': cterm list
  13.103 +      RCs: rec_call_info list
  13.104       }
  13.105  
  13.106 -type qgar = (string * typ) list * term list * term list * term
  13.107 +
  13.108 +
  13.109 +
  13.110 +type qgar = string * (string * typ) list * term list * term list * term
  13.111 +
  13.112 +fun name_of_fqgar (f, _, _, _, _) = f
  13.113  
  13.114  datatype mutual_part =
  13.115    MutualPart of 
  13.116  	 {
  13.117 -          f_name: string,
  13.118 -	  const: string * typ,
  13.119 +          fvar : string * typ,
  13.120  	  cargTs: typ list,
  13.121  	  pthA: SumTools.sum_path,
  13.122  	  pthR: SumTools.sum_path,
  13.123 -	  qgars: qgar list,
  13.124 -	  f_def: thm
  13.125 +	  f_def: term,
  13.126 +
  13.127 +	  f: term option,
  13.128 +          f_defthm : thm option
  13.129  	 }
  13.130  	 
  13.131  
  13.132  datatype mutual_info =
  13.133    Mutual of 
  13.134  	 { 
  13.135 -	  name: string, 
  13.136 -	  sum_const: string * typ,
  13.137 +	  defname: string,
  13.138 +          fsum_var : string * typ,
  13.139 +
  13.140  	  ST: typ,
  13.141  	  RST: typ,
  13.142  	  streeA: SumTools.sum_tree,
  13.143  	  streeR: SumTools.sum_tree,
  13.144 +
  13.145  	  parts: mutual_part list,
  13.146 -	  qglrss: (term list * term list * term * term) list list
  13.147 +	  fqgars: qgar list,
  13.148 +	  qglrs: ((string * typ) list * term list * term * term) list,
  13.149 +
  13.150 +          fsum : term option
  13.151  	 }
  13.152  
  13.153  
  13.154  datatype prep_result =
  13.155    Prep of
  13.156       {
  13.157 -      names: naming_context, 
  13.158 +      globals: globals,
  13.159 +      f: term,
  13.160 +      G: term,
  13.161 +      R: term,
  13.162 + 
  13.163        goal: term,
  13.164        goalI: thm,
  13.165        values: thm list,
  13.166 @@ -138,10 +164,10 @@
  13.167    FundefMResult of
  13.168       {
  13.169        f: term,
  13.170 -      G : term,
  13.171 -      R : term,
  13.172 +      G: term,
  13.173 +      R: term,
  13.174  
  13.175 -      psimps : thm list list, 
  13.176 +      psimps : thm list, 
  13.177        subset_pinducts : thm list, 
  13.178        simple_pinducts : thm list, 
  13.179        cases : thm,
  13.180 @@ -150,10 +176,10 @@
  13.181       }
  13.182  
  13.183  
  13.184 -type fundef_spec = ((string * attribute list) * term list) list list
  13.185 +type fundef_spec = ((string * typ) * mixfix) list *((string * Attrib.src list) * term list) list list
  13.186  type result_with_names = fundef_mresult * mutual_info * fundef_spec
  13.187  
  13.188 -structure FundefData = TheoryDataFun
  13.189 +structure FundefData = GenericDataFun
  13.190  (struct
  13.191    val name = "HOL/function_def/data";
  13.192    type T = string * result_with_names Symtab.table
  13.193 @@ -204,6 +230,7 @@
  13.194  val mk_prod = HOLogic.mk_prod
  13.195  val mk_mem = HOLogic.mk_mem
  13.196  val mk_eq = HOLogic.mk_eq
  13.197 +val eq_const = HOLogic.eq_const
  13.198  val Trueprop = HOLogic.mk_Trueprop
  13.199  
  13.200  val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
    14.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Sep 13 00:38:38 2006 +0200
    14.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Sep 13 12:05:50 2006 +0200
    14.3 @@ -10,6 +10,7 @@
    14.4  sig
    14.5      val pat_complete_tac: int -> tactic
    14.6  
    14.7 +    val pat_completeness : method
    14.8      val setup : theory -> theory
    14.9  end
   14.10  
   14.11 @@ -160,8 +161,48 @@
   14.12      handle COMPLETENESS => Seq.empty
   14.13  
   14.14  
   14.15 +val pat_completeness = Method.SIMPLE_METHOD (pat_complete_tac 1)
   14.16 +
   14.17 +val by_pat_completeness_simp =
   14.18 +    Proof.global_terminal_proof
   14.19 +      (Method.Basic (K pat_completeness),
   14.20 +       SOME (Method.Source (Args.src (("simp_all", []), Position.none))))
   14.21 +
   14.22  
   14.23  val setup =
   14.24 -    Method.add_methods [("pat_completeness", Method.no_args (Method.SIMPLE_METHOD (pat_complete_tac 1)), "Completeness prover for datatype patterns")]
   14.25 +    Method.add_methods [("pat_completeness", Method.no_args pat_completeness, "Completeness prover for datatype patterns")]
   14.26 +
   14.27 +
   14.28 +
   14.29 +
   14.30 +
   14.31 +
   14.32 +local structure P = OuterParse and K = OuterKeyword in
   14.33 +
   14.34 +
   14.35 +fun local_theory_to_proof f = 
   14.36 +    Toplevel.theory_to_proof (f o LocalTheory.init NONE)
   14.37 +
   14.38 +fun or_list1 s = P.enum1 "|" s
   14.39 +val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
   14.40 +val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
   14.41 +val statements_ow = or_list1 statement_ow
   14.42  
   14.43 +val funP =
   14.44 +  OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
   14.45 +  ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
   14.46 +     >> (fn ((target, fixes), statements) =>
   14.47 +            Toplevel.print o Toplevel.local_theory NONE (FundefPackage.add_fundef fixes statements true 
   14.48 +                                                                                  #> by_pat_completeness_simp)));
   14.49 +
   14.50 +val _ = OuterSyntax.add_parsers [funP];
   14.51  end
   14.52 +
   14.53 +
   14.54 +
   14.55 +
   14.56 +
   14.57 +
   14.58 +
   14.59 +
   14.60 +end
   14.61 \ No newline at end of file
    15.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Wed Sep 13 00:38:38 2006 +0200
    15.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Wed Sep 13 12:05:50 2006 +0200
    15.3 @@ -7,14 +7,12 @@
    15.4  *)
    15.5  
    15.6  
    15.7 +fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
    15.8 +
    15.9  fun mk_forall (var as Free (v,T)) t =
   15.10      all T $ Abs (v,T, abstract_over (var,t))
   15.11    | mk_forall v _ = let val _ = print v in sys_error "mk_forall" end
   15.12  
   15.13 -(* Builds a quantification with a new name for the variable. *)
   15.14 -fun mk_forall_rename (v as Free (_,T),newname) t =
   15.15 -    all T $ Abs (newname, T, abstract_over (v, t))
   15.16 -  | mk_forall_rename (v, _) _ = let val _ = print v in sys_error "mk_forall_rename" end
   15.17  
   15.18  (* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
   15.19  fun tupled_lambda vars t =
   15.20 @@ -75,10 +73,18 @@
   15.21    | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
   15.22    | map3 _ _ _ _ = raise Library.UnequalLengths;
   15.23  
   15.24 +fun map4 _ [] [] [] [] = []
   15.25 +  | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
   15.26 +  | map4 _ _ _ _ _ = raise Library.UnequalLengths;
   15.27 +
   15.28  fun map6 _ [] [] [] [] [] [] = []
   15.29    | map6 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) = f x y z u v w :: map6 f xs ys zs us vs ws
   15.30    | map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths;
   15.31  
   15.32 +fun map7 _ [] [] [] [] [] [] [] = []
   15.33 +  | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
   15.34 +  | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
   15.35 +
   15.36  
   15.37  
   15.38  (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
   15.39 @@ -88,3 +94,36 @@
   15.40  
   15.41  fun the_single [x] = x
   15.42    | the_single _ = sys_error "the_single"
   15.43 +
   15.44 +
   15.45 +(* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *)
   15.46 +fun replace_frees assoc =
   15.47 +    map_aterms (fn c as Free (n, _) => (case AList.lookup (op =) assoc n of
   15.48 +                                          NONE => c
   15.49 +                                        | SOME t => t)
   15.50 +                 | t => t)
   15.51 +
   15.52 +
   15.53 +
   15.54 +fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
   15.55 +  | rename_bound n _ = raise Match
   15.56 +
   15.57 +fun mk_forall_rename (n, v) =
   15.58 +    rename_bound n o mk_forall v 
   15.59 +
   15.60 +fun forall_intr_rename (n, cv) thm =
   15.61 +    let
   15.62 +      val allthm = forall_intr cv thm
   15.63 +      val reflx = prop_of allthm
   15.64 +                   |> rename_bound n
   15.65 +                   |> cterm_of (theory_of_thm thm)
   15.66 +                   |> reflexive
   15.67 +    in
   15.68 +      equal_elim reflx allthm
   15.69 +    end
   15.70 +
   15.71 +
   15.72 +(* Returns the frees in a term in canonical order, excluding the fixes from the context *)
   15.73 +fun frees_in_term ctxt t =
   15.74 +    rev (fold_aterms (fn  Free (v as (x, _)) =>
   15.75 +                          if Variable.is_fixed ctxt x then I else insert (fn ((x, _),(y, _)) => x = y) v | _ => I) t [])
    16.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 13 00:38:38 2006 +0200
    16.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 13 12:05:50 2006 +0200
    16.3 @@ -1,4 +1,3 @@
    16.4 -
    16.5  (*  Title:      HOL/Tools/function_package/fundef_package.ML
    16.6      ID:         $Id$
    16.7      Author:     Alexander Krauss, TU Muenchen
    16.8 @@ -10,7 +9,17 @@
    16.9  
   16.10  signature FUNDEF_PACKAGE =
   16.11  sig
   16.12 -    val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *)
   16.13 +    val add_fundef :  (string * string option * mixfix) list 
   16.14 +                      -> ((bstring * Attrib.src list) * string list) list list
   16.15 +                      -> bool 
   16.16 +                      -> local_theory 
   16.17 +                      -> Proof.state
   16.18 +
   16.19 +    val add_fundef_i:  (string * typ option * mixfix) list 
   16.20 +                       -> ((bstring * Attrib.src list) * term list) list list
   16.21 +                       -> bool 
   16.22 +                       -> local_theory 
   16.23 +                       -> Proof.state
   16.24  
   16.25      val cong_add: attribute
   16.26      val cong_del: attribute
   16.27 @@ -20,167 +29,136 @@
   16.28  end
   16.29  
   16.30  
   16.31 -structure FundefPackage : FUNDEF_PACKAGE =
   16.32 +structure FundefPackage  =
   16.33  struct
   16.34  
   16.35  open FundefCommon
   16.36  
   16.37  
   16.38 -fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy =
   16.39 -    let
   16.40 -      val psimpss = Library.unflat (map snd spec_part) psimps
   16.41 -      val (names, attss) = split_list (map fst spec_part)
   16.42 +fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
   16.43 +    let val (xs, ys) = split_list ps
   16.44 +    in xs ~~ f ys end
   16.45  
   16.46 -      val thy = thy |> Theory.add_path f_name
   16.47 +fun restore_spec_structure reps spec =
   16.48 +    (burrow o burrow_snd o burrow o K) reps spec
   16.49  
   16.50 -      val thy = thy |> Theory.add_path label
   16.51 -      val spsimpss = map (map standard) psimpss (* FIXME *)
   16.52 -      val add_list = (names ~~ spsimpss) ~~ attss
   16.53 -      val (_, thy) = PureThy.add_thmss add_list thy
   16.54 -      val thy = thy |> Theory.parent_path
   16.55 -
   16.56 -      val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy
   16.57 -      val thy = thy |> Theory.parent_path
   16.58 +fun with_local_path path f lthy =
   16.59 +    let 
   16.60 +      val restore = Theory.restore_naming (ProofContext.theory_of lthy)
   16.61      in
   16.62 -      thy
   16.63 +      lthy
   16.64 +        |> LocalTheory.theory (Theory.add_path path)
   16.65 +        |> f
   16.66 +        |> LocalTheory.theory restore
   16.67      end
   16.68  
   16.69 -
   16.70 -
   16.71 -
   16.72 -
   16.73 -
   16.74 -fun fundef_afterqed congs mutual_info name data spec [[result]] thy =
   16.75 +fun add_simps label moreatts mutual_info fixes psimps spec lthy =
   16.76      let
   16.77 -        val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
   16.78 -        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
   16.79 -        val Mutual {parts, ...} = mutual_info
   16.80 +      val fnames = map (fst o fst) fixes
   16.81 +      val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames psimps
   16.82  
   16.83 -        val Prep {names = Names {acc_R=accR, ...}, ...} = data
   16.84 -        val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
   16.85 -        val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
   16.86 -
   16.87 -        val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy
   16.88 -
   16.89 -        val casenames = flat (map (map (fst o fst)) spec)
   16.90 -
   16.91 -        val thy = thy |> Theory.add_path name
   16.92 -        val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy
   16.93 -        val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
   16.94 -        val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
   16.95 -        val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy
   16.96 -        val thy = thy |> Theory.parent_path
   16.97 +      fun add_for_f fname psimps =
   16.98 +          with_local_path fname
   16.99 +                          (LocalTheory.note ((label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd)
  16.100      in
  16.101 -      add_fundef_data name (fundef_data, mutual_info, spec) thy
  16.102 -    end
  16.103 -
  16.104 -fun gen_add_fundef prep_att eqns_attss (preprocess : bool) thy =
  16.105 -    let
  16.106 -      fun prep_eqns neqs =
  16.107 -          neqs
  16.108 -            |> map (apsnd (Sign.read_prop thy))
  16.109 -            |> map (apfst (apsnd (apfst (map (prep_att thy)))))
  16.110 -            |> FundefSplit.split_some_equations (ProofContext.init thy)
  16.111 -
  16.112 -      val spec = map prep_eqns eqns_attss
  16.113 -      val t_eqnss = map (flat o map snd) spec
  16.114 -
  16.115 -      val congs = get_fundef_congs (Context.Theory thy)
  16.116 -
  16.117 -      val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
  16.118 -      val Prep {goal, goalI, ...} = data
  16.119 -    in
  16.120 -      thy |> ProofContext.init
  16.121 -          |> Proof.theorem_i PureThy.internalK NONE
  16.122 -              (ProofContext.theory o fundef_afterqed congs mutual_info name data spec) NONE ("", [])
  16.123 -              [(("", []), [(goal, [])])]
  16.124 -          |> Proof.refine (Method.primitive_text (fn _ => goalI))
  16.125 -          |> Seq.hd
  16.126 +      lthy
  16.127 +        |> fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) |> snd
  16.128 +        |> fold2 add_for_f fnames psimps_by_f
  16.129      end
  16.130  
  16.131  
  16.132 -fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy =
  16.133 +fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy =
  16.134 +    let
  16.135 +        val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
  16.136 +        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
  16.137 +    in
  16.138 +      lthy
  16.139 +        |> add_simps "psimps" [] mutual_info fixes psimps spec
  16.140 +        |> with_local_path defname
  16.141 +                  (LocalTheory.note (("domintros", []), domintros) #> snd
  16.142 +                   #> LocalTheory.note (("termination", []), [termination]) #> snd
  16.143 +                   #> LocalTheory.note (("cases", []), [cases]) #> snd
  16.144 +                   #> LocalTheory.note (("pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) #> snd)
  16.145 +        |> LocalTheory.theory (Context.theory_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))))
  16.146 +    end (* FIXME: Add cases for induct and cases thm *)
  16.147 +
  16.148 +
  16.149 +
  16.150 +fun prep_with_flags prep fixspec eqnss_flags global_flag lthy =
  16.151      let
  16.152 -        val totality = hd (hd thmss)
  16.153 +      val eqnss = map (map (apsnd (map fst))) eqnss_flags
  16.154 +      val flags = map (map (map (fn (_, f) => global_flag orelse f) o snd)) eqnss_flags
  16.155 +
  16.156 +      val ((fixes, _), ctxt') = prep fixspec [] lthy
  16.157 +      val spec = map (fn eqns => snd (fst (prep [] eqns ctxt'))) eqnss
  16.158 +                     |> map (map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)))) (* Add quantifiers *)
  16.159 +                     |> map2 (map2 (fn fs => fn (r, thms) => (r, fs ~~ thms))) flags
  16.160 +                     |> (burrow o burrow_snd o burrow) 
  16.161 +                          (FundefSplit.split_some_equations lthy)
  16.162 +                     |> map (map (apsnd flat))
  16.163 +    in
  16.164 +      ((fixes, spec), ctxt')
  16.165 +    end
  16.166 +
  16.167  
  16.168 -        val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
  16.169 -          = the (get_fundef_data name thy)
  16.170 +fun gen_add_fundef prep_spec fixspec eqnss_flags preprocess lthy =
  16.171 +    let
  16.172 +      val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags preprocess lthy
  16.173 +      val t_eqns = spec
  16.174 +                     |> flat |> map snd |> flat (* flatten external structure *)
  16.175 +
  16.176 +      val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) = 
  16.177 +          FundefMutual.prepare_fundef_mutual fixes t_eqns lthy
  16.178 +
  16.179 +      val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
  16.180 +    in
  16.181 +        lthy
  16.182 +          |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
  16.183 +          |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd
  16.184 +    end
  16.185 +
  16.186 +
  16.187 +fun total_termination_afterqed defname data [[totality]] lthy =
  16.188 +    let
  16.189 +        val (FundefMResult {psimps, simple_pinducts, ... }, mutual_info, (fixes, stmts)) = data
  16.190  
  16.191          val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
  16.192  
  16.193 -        val tsimps = map (map remove_domain_condition) psimps
  16.194 +        val tsimps = map remove_domain_condition psimps
  16.195          val tinduct = map remove_domain_condition simple_pinducts
  16.196  
  16.197 -        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
  16.198 -        val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
  16.199 -
  16.200 -        val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy
  16.201 -
  16.202 -        val thy = Theory.add_path name thy
  16.203 -
  16.204 -        val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy
  16.205 -        val thy = Theory.parent_path thy
  16.206 +        (* FIXME: How to generate code from (possibly) local contexts 
  16.207 +        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
  16.208 +        val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
  16.209 +        *)
  16.210      in
  16.211 -        thy
  16.212 -    end
  16.213 -
  16.214 -(*
  16.215 -fun mk_partial_rules name D_name D domT idomT thmss thy =
  16.216 -    let
  16.217 -        val [subs, dcl] = (hd thmss)
  16.218 -
  16.219 -        val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
  16.220 -          = the (Symtab.lookup (FundefData.get thy) name)
  16.221 -
  16.222 -        val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)]
  16.223 -                                                    [SOME (cterm_of thy D)]
  16.224 -                                                    subsetD)
  16.225 -
  16.226 -        val D_simps = map (curry op RS D_implies_dom) f_simps
  16.227 -
  16.228 -        val D_induct = subset_induct
  16.229 -                           |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
  16.230 -                           |> curry op COMP subs
  16.231 -                           |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
  16.232 -                                                 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
  16.233 -
  16.234 -        val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
  16.235 -        val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
  16.236 -    in
  16.237 -        thy3
  16.238 -    end
  16.239 -*)
  16.240 -
  16.241 -
  16.242 -fun fundef_setup_termination_proof name NONE thy =
  16.243 -    let
  16.244 -        val name = if name = "" then get_last_fundef thy else name
  16.245 -        val data = the (get_fundef_data name thy)
  16.246 -                   handle Option.Option => raise ERROR ("No such function definition: " ^ name)
  16.247 -
  16.248 -        val (res as FundefMResult {termination, ...}, mutual, _) = data
  16.249 -        val goal = FundefTermination.mk_total_termination_goal data
  16.250 -    in
  16.251 -        thy |> ProofContext.init
  16.252 -            |> ProofContext.note_thmss_i [(("termination",
  16.253 -                                            [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
  16.254 -            |> Proof.theorem_i PureThy.internalK NONE
  16.255 -              (ProofContext.theory o total_termination_afterqed name mutual) NONE ("", [])
  16.256 -              [(("", []), [(goal, [])])]
  16.257 -    end
  16.258 -  | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
  16.259 -    let
  16.260 -        val name = if name = "" then get_last_fundef thy else name
  16.261 -        val data = the (get_fundef_data name thy)
  16.262 -        val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
  16.263 -    in
  16.264 -        thy |> ProofContext.init
  16.265 -            |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
  16.266 -            [(("", []), [(subs, []), (dcl, [])])]
  16.267 +        lthy
  16.268 +          |> add_simps "simps" [] mutual_info fixes tsimps stmts
  16.269 +          |> with_local_path defname
  16.270 +                (LocalTheory.note (("induct", [Attrib.internal (InductAttrib.induct_set "")]), tinduct) #> snd)
  16.271      end
  16.272  
  16.273  
  16.274 -val add_fundef = gen_add_fundef Attrib.attribute
  16.275 +fun fundef_setup_termination_proof name_opt lthy =
  16.276 +    let
  16.277 +        val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt
  16.278 +        val data = the (get_fundef_data name (Context.Proof lthy))
  16.279 +                   handle Option.Option => raise ERROR ("No such function definition: " ^ name)
  16.280 +
  16.281 +        val (res as FundefMResult {termination, ...}, _, _) = data
  16.282 +        val goal = FundefTermination.mk_total_termination_goal data
  16.283 +    in
  16.284 +      lthy 
  16.285 +        |> ProofContext.note_thmss_i [(("termination",
  16.286 +                                 [ContextRules.intro_query NONE]), [(ProofContext.export_standard lthy lthy [termination], [])])] |> snd
  16.287 +        |> Proof.theorem_i PureThy.internalK NONE
  16.288 +                           (total_termination_afterqed name data) NONE ("", [])
  16.289 +                           [(("", []), [(goal, [])])]
  16.290 +    end
  16.291 +
  16.292 +
  16.293 +val add_fundef = gen_add_fundef Specification.read_specification
  16.294 +val add_fundef_i = gen_add_fundef Specification.cert_specification
  16.295  
  16.296  
  16.297  
  16.298 @@ -206,39 +184,34 @@
  16.299  
  16.300  
  16.301  
  16.302 -val star = Scan.one (fn t => (OuterLex.val_of t = "*"));
  16.303 +fun or_list1 s = P.enum1 "|" s
  16.304 +
  16.305 +val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
  16.306 +
  16.307 +val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
  16.308 +val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
  16.309 +val statements_ow = or_list1 statement_ow
  16.310  
  16.311  
  16.312 -val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME))
  16.313 -                                               >> (fn x => (map_filter I x, exists is_none x)))
  16.314 -                              --| P.$$$ "]";
  16.315 -
  16.316 -val opt_attribs_with_star = Scan.optional attribs_with_star ([], false);
  16.317 -
  16.318 -val opt_thm_name_star =
  16.319 -  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ ":") ("", ([], false));
  16.320 -
  16.321 -
  16.322 -val function_decl =
  16.323 -    Scan.repeat1 (opt_thm_name_star -- P.prop);
  16.324 +fun local_theory_to_proof f = 
  16.325 +    Toplevel.theory_to_proof (f o LocalTheory.init NONE)
  16.326  
  16.327  val functionP =
  16.328    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
  16.329 -  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) --
  16.330 -  P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
  16.331 -                                    Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
  16.332 +  ((opt_sequential -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
  16.333 +     >> (fn (((sequential, target), fixes), statements) =>
  16.334 +            Toplevel.print o local_theory_to_proof (add_fundef fixes statements sequential)));
  16.335 +
  16.336  
  16.337  val terminationP =
  16.338    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
  16.339 -  ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
  16.340 -       >> (fn (name,dom) =>
  16.341 -              Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
  16.342 +  (Scan.option P.name 
  16.343 +    >> (fn name => Toplevel.print o local_theory_to_proof (fundef_setup_termination_proof name)));
  16.344  
  16.345 -val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
  16.346  
  16.347  val _ = OuterSyntax.add_parsers [functionP];
  16.348  val _ = OuterSyntax.add_parsers [terminationP];
  16.349 -
  16.350 +val _ = OuterSyntax.add_keywords ["sequential", "otherwise"]; (* currently unused *)
  16.351  
  16.352  end;
  16.353  
    17.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Wed Sep 13 00:38:38 2006 +0200
    17.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Wed Sep 13 12:05:50 2006 +0200
    17.3 @@ -9,12 +9,15 @@
    17.4  
    17.5  signature FUNDEF_PREP =
    17.6  sig
    17.7 -    val prepare_fundef : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list
    17.8 -                         -> FundefCommon.prep_result * theory
    17.9 +    val prepare_fundef : string (* defname *)
   17.10 +                         -> (string * typ * mixfix) (* defined symbol *)
   17.11 +                         -> ((string * typ) list * term list * term * term) list (* specification *)
   17.12 +                         -> local_theory
   17.13 +                         -> FundefCommon.prep_result * term * local_theory
   17.14  
   17.15  end
   17.16  
   17.17 -structure FundefPrep (*: FUNDEF_PREP*) =
   17.18 +structure FundefPrep : FUNDEF_PREP =
   17.19  struct
   17.20  
   17.21  
   17.22 @@ -34,26 +37,6 @@
   17.23  
   17.24  
   17.25  
   17.26 -fun split_list3 [] = ([],[],[])
   17.27 -  | split_list3 ((x,y,z)::xyzs) =
   17.28 -    let
   17.29 -        val (xs, ys, zs) = split_list3 xyzs
   17.30 -    in
   17.31 -        (x::xs,y::ys,z::zs)
   17.32 -    end
   17.33 -
   17.34 -
   17.35 -fun build_tree thy f congs ctx (qs, gs, lhs, rhs) =
   17.36 -    let
   17.37 -        (* FIXME: Save precomputed dependencies in a theory data slot *)
   17.38 -        val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
   17.39 -
   17.40 -        val (_(*FIXME*), ctx') = ProofContext.add_fixes_i (map (fn Free (n, T) => (n, SOME T, NoSyn)) qs) ctx
   17.41 -    in
   17.42 -        FundefCtxTree.mk_tree thy congs_deps f ctx' rhs
   17.43 -    end
   17.44 -
   17.45 -
   17.46  fun find_calls tree =
   17.47      let
   17.48        fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
   17.49 @@ -64,205 +47,97 @@
   17.50  
   17.51  
   17.52  
   17.53 -(* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
   17.54 -fun mk_primed_vars thy glrs =
   17.55 +(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
   17.56 +(* Takes bound form of qglrs tuples *)
   17.57 +fun mk_compat_impl domT ranT fvar f ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
   17.58      let
   17.59 -        val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
   17.60 -
   17.61 -        fun rename_vars (qs,gs,lhs,rhs) =
   17.62 -            let
   17.63 -                val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs
   17.64 -                val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
   17.65 -            in
   17.66 -                (qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
   17.67 -            end
   17.68 +      val shift = incr_boundvars (length qs')
   17.69      in
   17.70 -        map rename_vars glrs
   17.71 +      (implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
   17.72 +               $ Trueprop (eq_const ranT $ shift rhs $ rhs'))
   17.73 +        |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
   17.74 +        |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
   17.75 +        |> curry abstract_over fvar
   17.76 +        |> curry subst_bound f
   17.77      end
   17.78  
   17.79 +fun mk_compat_proof_obligations domT ranT fvar f glrs =
   17.80 +    map (mk_compat_impl domT ranT fvar f) (unordered_pairs glrs)
   17.81  
   17.82  
   17.83 -(* Chooses fresh free names, declares G and R, defines f and returns a record
   17.84 -   with all the information *)
   17.85 -fun setup_context f glrs defname thy =
   17.86 +fun mk_completeness globals clauses qglrs =
   17.87      let
   17.88 -        val Const (f_fullname, fT) = f
   17.89 -        val fname = Sign.base_name f_fullname
   17.90 -
   17.91 -        val domT = domain_type fT
   17.92 -        val ranT = range_type fT
   17.93 -
   17.94 -        val GT = mk_relT (domT, ranT)
   17.95 -        val RT = mk_relT (domT, domT)
   17.96 -        val G_name = defname ^ "_graph"
   17.97 -        val R_name = defname ^ "_rel"
   17.98 -
   17.99 -        val gfixes = [("h_fd", domT --> ranT),
  17.100 -                      ("y_fd", ranT),
  17.101 -                      ("x_fd", domT),
  17.102 -                      ("z_fd", domT),
  17.103 -                      ("a_fd", domT),
  17.104 -                      ("D_fd", HOLogic.mk_setT domT),
  17.105 -                      ("P_fd", domT --> boolT),
  17.106 -                      ("Pb_fd", boolT),
  17.107 -                      ("f_fd", fT)]
  17.108 -
  17.109 -        val (fxnames, ctx) = (ProofContext.init thy)
  17.110 -                               |> ProofContext.add_fixes_i (map (fn (n,T) => (n, SOME T, NoSyn)) gfixes)
  17.111 -
  17.112 -        val [h, y, x, z, a, D, P, Pbool, fvar] = map (fn (n,(_,T)) => Free (n, T)) (fxnames ~~ gfixes)
  17.113 -
  17.114 -        val Free (fvarname, _) = fvar
  17.115 -
  17.116 -        val glrs' = mk_primed_vars thy glrs
  17.117 +        val Globals {x, Pbool, ...} = globals
  17.118  
  17.119 -        val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
  17.120 -
  17.121 -        val G = Const (Sign.full_name thy G_name, GT)
  17.122 -        val R = Const (Sign.full_name thy R_name, RT)
  17.123 -        val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
  17.124 -
  17.125 -        val f_eq = Logic.mk_equals (f $ x,
  17.126 -                                    Const ("The", (ranT --> boolT) --> ranT) $
  17.127 -                                          Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
  17.128 -
  17.129 -        val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
  17.130 -    in
  17.131 -        (Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, ctx=ctx}, thy)
  17.132 -    end
  17.133 -
  17.134 -
  17.135 -
  17.136 -
  17.137 -
  17.138 -(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
  17.139 -fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
  17.140 -    (implies $ Trueprop (mk_eq (lhs, lhs'))
  17.141 -             $ Trueprop (mk_eq (rhs, rhs')))
  17.142 -        |> fold_rev (curry Logic.mk_implies) (gs @ gs')
  17.143 -        |> fold_rev mk_forall (qs @ qs')
  17.144 -
  17.145 -(* all proof obligations *)
  17.146 -fun mk_compat_proof_obligations glrs glrs' =
  17.147 -    map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (unordered_pairs (glrs ~~ glrs'))
  17.148 -
  17.149 -
  17.150 -fun mk_completeness names glrs =
  17.151 -    let
  17.152 -        val Names {domT, x, Pbool, ...} = names
  17.153 -
  17.154 -        fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
  17.155 +        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = Trueprop Pbool
  17.156                                                  |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
  17.157                                                  |> fold_rev (curry Logic.mk_implies) gs
  17.158 -                                                |> fold_rev mk_forall qs
  17.159 +                                                |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  17.160      in
  17.161          Trueprop Pbool
  17.162 -                 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
  17.163 -                 |> mk_forall_rename (x, "x")
  17.164 -                 |> mk_forall_rename (Pbool, "P")
  17.165 +                 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
  17.166 +                 |> mk_forall_rename ("x", x)
  17.167 +                 |> mk_forall_rename ("P", Pbool)
  17.168      end
  17.169  
  17.170  
  17.171 -fun inductive_def_wrap defs (thy, const) =
  17.172 +fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
  17.173      let
  17.174 -      val qdefs = map dest_all_all defs
  17.175 +      val (qs, ctxt') = Variable.invent_fixes (map fst pre_qs) ctxt
  17.176 +                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
  17.177  
  17.178 -      val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) =
  17.179 -          InductivePackage.add_inductive_i true (*verbose*)
  17.180 -                                             false (*add_consts*)
  17.181 -                                             "" (* no altname *)
  17.182 -                                             false (* no coind *)
  17.183 -                                             false (* elims, please *)
  17.184 -                                             false (* induction thm please *)
  17.185 -                                             [const] (* the constant *)
  17.186 -                                             (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *)
  17.187 -                                             [] (* no special monos *)
  17.188 -                                             thy
  17.189 +      val thy = ProofContext.theory_of ctxt'
  17.190  
  17.191 -(* It would be nice if this worked... But this is actually HO-Unification... *)
  17.192 -(*      fun inst (qs, intr) intr_gen =
  17.193 -          Goal.init (cterm_of thy intr)
  17.194 -                    |> curry op COMP intr_gen
  17.195 -                    |> Goal.finish
  17.196 -                    |> fold_rev (forall_intr o cterm_of thy) qs*)
  17.197 +      fun inst t = subst_bounds (rev qs, t)
  17.198 +      val gs = map inst pre_gs
  17.199 +      val lhs = inst pre_lhs
  17.200 +      val rhs = inst pre_rhs
  17.201 +                
  17.202 +      val cqs = map (cterm_of thy) qs
  17.203 +      val ags = map (assume o cterm_of thy) gs
  17.204 +                  
  17.205 +      val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
  17.206 +    in
  17.207 +      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, 
  17.208 +                      cqs = cqs, ags = ags, case_hyp = case_hyp }
  17.209 +    end
  17.210 +      
  17.211  
  17.212 -      fun inst (qs, intr) intr_gen =
  17.213 -          intr_gen
  17.214 -            |> Thm.freezeT
  17.215 -            |> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs
  17.216 -
  17.217 -      val intrs = map2 inst qdefs intrs_gen
  17.218 -      val elim = elim_gen
  17.219 -                   |> Thm.freezeT
  17.220 -                   |> forall_intr_vars (* FIXME *)
  17.221 -    in
  17.222 -      (intrs, (thy, const, elim))
  17.223 -    end
  17.224 -
  17.225 -
  17.226 +(* lowlevel term function *)
  17.227 +fun abstract_over_list vs body =
  17.228 +  let
  17.229 +    exception SAME;
  17.230 +    fun abs lev v tm =
  17.231 +      if v aconv tm then Bound lev
  17.232 +      else
  17.233 +        (case tm of
  17.234 +          Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
  17.235 +        | t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
  17.236 +        | _ => raise SAME);
  17.237 +  in 
  17.238 +    fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
  17.239 +  end
  17.240  
  17.241  
  17.242  
  17.243 -(*
  17.244 - * "!!qs xs. CS ==> G => (r, lhs) : R"
  17.245 - *)
  17.246 -fun mk_RIntro R (qs, gs, lhs, rhs) (rcfix, rcassm, rcarg) =
  17.247 -    mk_relmem (rcarg, lhs) R
  17.248 -              |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  17.249 -              |> fold_rev (curry Logic.mk_implies) gs
  17.250 -              |> fold_rev (mk_forall o Free) rcfix
  17.251 -              |> fold_rev mk_forall qs
  17.252 -
  17.253 -
  17.254 -fun mk_GIntro thy f_const f_var G (qs, gs, lhs, rhs) RCs =
  17.255 +fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
  17.256      let
  17.257 -      fun mk_h_assm (rcfix, rcassm, rcarg) =
  17.258 -          mk_relmem (rcarg, f_var $ rcarg) G
  17.259 -                    |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  17.260 -                    |> fold_rev (mk_forall o Free) rcfix
  17.261 -    in
  17.262 -      mk_relmem (lhs, rhs) G
  17.263 -                |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
  17.264 -                |> fold_rev (curry Logic.mk_implies) gs
  17.265 -                |> Pattern.rewrite_term thy [(f_const, f_var)] []
  17.266 -                |> fold_rev mk_forall (f_var :: qs)
  17.267 -    end
  17.268 -
  17.269 -
  17.270 +        val Globals {h, fvar, x, ...} = globals
  17.271  
  17.272 -fun mk_clause_info thy names no (qs,gs,lhs,rhs) tree RCs GIntro_thm RIntro_thms =
  17.273 -    let
  17.274 -        val Names {G, h, f, fvar, x, ...} = names
  17.275 -
  17.276 -        val cqs = map (cterm_of thy) qs
  17.277 -        val ags = map (assume o cterm_of thy) gs
  17.278 +        val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
  17.279 +        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
  17.280  
  17.281 -        val used = [] (* XXX *)
  17.282 -                  (* FIXME: What is the relationship between this and mk_primed_vars? *)
  17.283 -        val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs
  17.284 -        val cqs' = map (cterm_of thy) qs'
  17.285 -
  17.286 -        val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
  17.287 -        val ags' = map (assume o cterm_of thy o rename_vars) gs
  17.288 -        val lhs' = rename_vars lhs
  17.289 -        val rhs' = rename_vars rhs
  17.290 -
  17.291 +        (* Instantiate the GIntro thm with "f" and import into the clause context. *)
  17.292          val lGI = GIntro_thm
  17.293 -                    |> forall_elim (cterm_of thy f)
  17.294 +                    |> forall_elim (cert f)
  17.295                      |> fold forall_elim cqs
  17.296                      |> fold implies_elim_swp ags
  17.297  
  17.298 -        (* FIXME: Can be removed when inductive-package behaves nicely. *)
  17.299 -        val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [])
  17.300 -                          (term_frees (snd (dest_all_all (prop_of GIntro_thm))))
  17.301 -
  17.302          fun mk_call_info (rcfix, rcassm, rcarg) RI =
  17.303              let
  17.304 -                val crcfix = map (cterm_of thy o Free) rcfix
  17.305 -
  17.306                  val llRI = RI
  17.307                               |> fold forall_elim cqs
  17.308 -                             |> fold forall_elim crcfix
  17.309 +                             |> fold (forall_elim o cert o Free) rcfix
  17.310                               |> fold implies_elim_swp ags
  17.311                               |> fold implies_elim_swp rcassm
  17.312  
  17.313 @@ -270,27 +145,23 @@
  17.314                      mk_relmem (rcarg, h $ rcarg) G
  17.315                                |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  17.316                                |> fold_rev (mk_forall o Free) rcfix
  17.317 -                              |> Pattern.rewrite_term thy [(f, h)] []
  17.318 -
  17.319 -                val Gh = assume (cterm_of thy h_assum)
  17.320 -                val Gh' = assume (cterm_of thy (rename_vars h_assum))
  17.321 +                              |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
  17.322 +                              |> abstract_over_list (rev qs)
  17.323              in
  17.324 -                RCInfo {RIvs=rcfix, Gh=Gh, Gh'=Gh', rcarg=rcarg, CCas=rcassm, llRI=llRI}
  17.325 +                RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
  17.326              end
  17.327  
  17.328 -        val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
  17.329 -
  17.330          val RC_infos = map2 mk_call_info RCs RIntro_thms
  17.331      in
  17.332          ClauseInfo
  17.333              {
  17.334               no=no,
  17.335 -             qs=qs, gs=gs, lhs=lhs, rhs=rhs,
  17.336 -             cqs=cqs, ags=ags,
  17.337 -             cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs',
  17.338 -             lGI=lGI, RCs=RC_infos,
  17.339 -             tree=tree, case_hyp = case_hyp,
  17.340 -             ordcqs'=ordcqs'
  17.341 +             cdata=cdata,
  17.342 +             qglr=qglr,
  17.343 +
  17.344 +             lGI=lGI, 
  17.345 +             RCs=RC_infos,
  17.346 +             tree=tree
  17.347              }
  17.348      end
  17.349  
  17.350 @@ -298,10 +169,7 @@
  17.351  
  17.352  
  17.353  
  17.354 -(* Copied from fundef_proof.ML: *)
  17.355  
  17.356 -(***********************************************)
  17.357 -(* Compat thms are stored in normal form (with vars) *)
  17.358  
  17.359  (* replace this by a table later*)
  17.360  fun store_compat_thms 0 thms = []
  17.361 @@ -312,72 +180,63 @@
  17.362          (thms1 :: store_compat_thms (n - 1) thms2)
  17.363      end
  17.364  
  17.365 -
  17.366 -(* needs i <= j *)
  17.367 +(* expects i <= j *)
  17.368  fun lookup_compat_thm i j cts =
  17.369      nth (nth cts (i - 1)) (j - i)
  17.370 -(***********************************************)
  17.371  
  17.372 -
  17.373 -(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
  17.374 +(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
  17.375  (* if j < i, then turn around *)
  17.376 -fun get_compat_thm thy cts clausei clausej =
  17.377 +fun get_compat_thm thy cts i j ctxi ctxj = 
  17.378      let
  17.379 -        val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
  17.380 -        val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
  17.381 +        val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
  17.382 +        val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
  17.383  
  17.384 -        val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
  17.385 +        val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
  17.386      in if j < i then
  17.387             let
  17.388                 val compat = lookup_compat_thm j i cts
  17.389             in
  17.390 -               compat         (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
  17.391 -                |> fold forall_elim (qsj' @ qsi) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *)
  17.392 -                |> fold implies_elim_swp gsj'
  17.393 -                |> fold implies_elim_swp gsi
  17.394 -                |> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
  17.395 +               compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
  17.396 +                |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
  17.397 +                |> fold implies_elim_swp agsj
  17.398 +                |> fold implies_elim_swp agsi
  17.399 +                |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
  17.400             end
  17.401         else
  17.402             let
  17.403                 val compat = lookup_compat_thm i j cts
  17.404             in
  17.405 -               compat        (* "!!qi qj'. Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
  17.406 -                 |> fold forall_elim (qsi @ qsj') (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
  17.407 -                 |> fold implies_elim_swp gsi
  17.408 -                 |> fold implies_elim_swp gsj'
  17.409 -                 |> implies_elim_swp (assume lhsi_eq_lhsj')
  17.410 -                 |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
  17.411 +               compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
  17.412 +                 |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
  17.413 +                 |> fold implies_elim_swp agsi
  17.414 +                 |> fold implies_elim_swp agsj
  17.415 +                 |> implies_elim_swp (assume lhsi_eq_lhsj)
  17.416 +                 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
  17.417             end
  17.418      end
  17.419  
  17.420  
  17.421  
  17.422 -(* Generates the replacement lemma with primed variables. A problem here is that one should not do
  17.423 -the complete requantification at the end to replace the variables. One should find a way to be more efficient
  17.424 -here. *)
  17.425 -fun mk_replacement_lemma thy (names:naming_context) ih_elim clause =
  17.426 +
  17.427 +(* Generates the replacement lemma in fully quantified form. *)
  17.428 +fun mk_replacement_lemma thy h ih_elim clause =
  17.429      let
  17.430 -        val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names
  17.431 -        val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
  17.432 +        val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
  17.433  
  17.434          val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
  17.435  
  17.436          val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
  17.437 -        val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
  17.438 -        val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
  17.439 +        val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
  17.440  
  17.441          val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
  17.442  
  17.443 -        val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
  17.444 +        val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (Ris ~~ h_assums) tree
  17.445  
  17.446          val replace_lemma = (eql RS meta_eq_to_obj_eq)
  17.447                                  |> implies_intr (cprop_of case_hyp)
  17.448                                  |> fold_rev (implies_intr o cprop_of) h_assums
  17.449                                  |> fold_rev (implies_intr o cprop_of) ags
  17.450                                  |> fold_rev forall_intr cqs
  17.451 -                                |> fold forall_elim cqs'
  17.452 -                                |> fold implies_elim_swp ags'
  17.453 -                                |> fold implies_elim_swp h_assums'
  17.454      in
  17.455        replace_lemma
  17.456      end
  17.457 @@ -385,15 +244,30 @@
  17.458  
  17.459  
  17.460  
  17.461 -fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
  17.462 +fun pr (s:string) x =
  17.463 +    let val _ = print s
  17.464 +    in
  17.465 +      x
  17.466 +    end
  17.467 +
  17.468 +
  17.469 +fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
  17.470      let
  17.471 -        val Names {f, h, y, ...} = names
  17.472 -        val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
  17.473 -        val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
  17.474 +        val Globals {h, y, x, fvar, ...} = globals
  17.475 +        val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
  17.476 +        val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
  17.477 +
  17.478 +        val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} 
  17.479 +            = mk_clause_context x ctxti cdescj
  17.480  
  17.481 -        val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
  17.482 -        val compat = get_compat_thm thy compat_store clausei clausej
  17.483 -        val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
  17.484 +        val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
  17.485 +        val compat = get_compat_thm thy compat_store i j cctxi cctxj
  17.486 +        val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
  17.487 +
  17.488 +        val RLj_import = 
  17.489 +            RLj |> fold forall_elim cqsj'
  17.490 +                |> fold implies_elim_swp agsj'
  17.491 +                |> fold implies_elim_swp Ghsj'
  17.492  
  17.493          val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
  17.494          val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
  17.495 @@ -401,7 +275,7 @@
  17.496          val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
  17.497      in
  17.498          (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
  17.499 -        |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
  17.500 +        |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
  17.501          |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
  17.502          |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
  17.503          |> implies_intr (cprop_of y_eq_rhsj'h)
  17.504 @@ -409,17 +283,18 @@
  17.505          |> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
  17.506          |> implies_elim_swp eq_pairs
  17.507          |> fold_rev (implies_intr o cprop_of) Ghsj'
  17.508 -        |> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
  17.509 +        |> fold_rev (implies_intr o cprop_of) agsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
  17.510          |> implies_intr (cprop_of eq_pairs)
  17.511 -        |> fold_rev forall_intr ordcqs'j
  17.512 +        |> fold_rev forall_intr (cterm_of thy h :: cqsj')
  17.513      end
  17.514  
  17.515  
  17.516  
  17.517 -fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
  17.518 +fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
  17.519      let
  17.520 -        val Names {x, y, G, fvar, f, ranT, ...} = names
  17.521 -        val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
  17.522 +        val Globals {x, y, ranT, fvar, ...} = globals
  17.523 +        val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
  17.524 +        val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
  17.525  
  17.526          val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
  17.527  
  17.528 @@ -427,14 +302,13 @@
  17.529                                                              |> fold_rev (implies_intr o cprop_of) CCas
  17.530                                                              |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  17.531  
  17.532 -        val existence = lGI (*|> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])*)
  17.533 -                            |> fold (curry op COMP o prep_RC) RCs
  17.534 +        val existence = fold (curry op COMP o prep_RC) RCs lGI
  17.535  
  17.536          val a = cterm_of thy (mk_prod (lhs, y))
  17.537 -        val P = cterm_of thy (mk_eq (y, rhs))
  17.538 +        val P = cterm_of thy (mk_eq (y, rhsC))
  17.539          val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
  17.540  
  17.541 -        val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
  17.542 +        val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
  17.543  
  17.544          val uniqueness = G_cases
  17.545                             |> forall_elim a
  17.546 @@ -447,7 +321,7 @@
  17.547          val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
  17.548  
  17.549          val exactly_one =
  17.550 -            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
  17.551 +            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
  17.552                   |> curry (op COMP) existence
  17.553                   |> curry (op COMP) uniqueness
  17.554                   |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
  17.555 @@ -457,7 +331,6 @@
  17.556  
  17.557          val function_value =
  17.558              existence
  17.559 -                |> fold_rev (implies_intr o cprop_of) ags
  17.560                  |> implies_intr ihyp
  17.561                  |> implies_intr (cprop_of case_hyp)
  17.562                  |> forall_intr (cterm_of thy x)
  17.563 @@ -470,19 +343,13 @@
  17.564  
  17.565  
  17.566  
  17.567 -fun prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim =
  17.568 +fun prove_stuff thy congs globals G f R clauses complete compat compat_store G_elim f_def =
  17.569      let
  17.570 -        val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, Pbool, ...}:naming_context = names
  17.571 -
  17.572 -        val f_def_fr = Thm.freezeT f_def
  17.573 +        val Globals {h, domT, ranT, x, ...} = globals
  17.574  
  17.575 -        val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)]
  17.576 -                                                [SOME (cterm_of thy f), SOME (cterm_of thy G)])
  17.577 -                                      #> curry op COMP (forall_intr_vars f_def_fr)
  17.578 -
  17.579 -        val inst_ex1_ex = instantiate_and_def ex1_implies_ex
  17.580 -        val inst_ex1_un = instantiate_and_def ex1_implies_un
  17.581 -        val inst_ex1_iff = instantiate_and_def ex1_implies_iff
  17.582 +        val inst_ex1_ex = f_def RS ex1_implies_ex
  17.583 +        val inst_ex1_un = f_def RS ex1_implies_un
  17.584 +        val inst_ex1_iff = f_def RS ex1_implies_iff
  17.585  
  17.586          (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
  17.587          val ihyp = all domT $ Abs ("z", domT,
  17.588 @@ -496,17 +363,18 @@
  17.589          val ih_elim = ihyp_thm RS inst_ex1_un
  17.590  
  17.591          val _ = Output.debug "Proving Replacement lemmas..."
  17.592 -        val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
  17.593 +        val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
  17.594  
  17.595          val _ = Output.debug "Proving cases for unique existence..."
  17.596 -        val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
  17.597 +        val (ex1s, values) = 
  17.598 +            split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
  17.599  
  17.600          val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *)
  17.601          val graph_is_function = complete
  17.602                                    |> forall_elim_vars 0
  17.603                                    |> fold (curry op COMP) ex1s
  17.604                                    |> implies_intr (ihyp)
  17.605 -                                  |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
  17.606 +                                  |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, mk_acc domT R))))
  17.607                                    |> forall_intr (cterm_of thy x)
  17.608                                    |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
  17.609                                    |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
  17.610 @@ -523,47 +391,152 @@
  17.611      end
  17.612  
  17.613  
  17.614 +fun define_graph Gname fvar domT ranT clauses RCss lthy =
  17.615 +    let
  17.616 +      val GT = mk_relT (domT, ranT)
  17.617 +      val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
  17.618 +
  17.619 +      fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
  17.620 +          let
  17.621 +            fun mk_h_assm (rcfix, rcassm, rcarg) =
  17.622 +                mk_relmem (rcarg, fvar $ rcarg) Gvar
  17.623 +                          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  17.624 +                          |> fold_rev (mk_forall o Free) rcfix
  17.625 +          in
  17.626 +            mk_relmem (lhs, rhs) Gvar
  17.627 +                      |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
  17.628 +                      |> fold_rev (curry Logic.mk_implies) gs
  17.629 +                      |> fold_rev mk_forall (fvar :: qs)
  17.630 +          end
  17.631 +          
  17.632 +      val G_intros = map2 mk_GIntro clauses RCss
  17.633 +                     
  17.634 +      val (GIntro_thms, (G, G_elim, lthy)) = 
  17.635 +          FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
  17.636 +    in
  17.637 +      ((G, GIntro_thms, G_elim), lthy)
  17.638 +    end
  17.639  
  17.640  
  17.641  
  17.642 -(*
  17.643 - * This is the first step in a function definition.
  17.644 - *
  17.645 - * Defines the function, the graph and the termination relation, synthesizes completeness
  17.646 - * and comatibility conditions and returns everything.
  17.647 - *)
  17.648 -fun prepare_fundef thy congs defname f qglrs used =
  17.649 +fun define_function fdefname (fname, mixfix) domT ranT G lthy =
  17.650 +    let
  17.651 +      val f_def = 
  17.652 +          Abs ("x", domT, Const ("The", (ranT --> boolT) --> ranT) $
  17.653 +                                Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G))
  17.654 +          
  17.655 +      val ((f, (_, f_defthm)), lthy) = LocalTheory.def ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
  17.656 +    in
  17.657 +      ((f, f_defthm), lthy)
  17.658 +    end
  17.659 +
  17.660 +
  17.661 +fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
  17.662      let
  17.663 -      val (names, thy) = setup_context f qglrs defname thy
  17.664 -      val Names {G, R, ctx, glrs', fvar, ...} = names
  17.665 +
  17.666 +      val RT = mk_relT (domT, domT)
  17.667 +      val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
  17.668 +
  17.669 +      fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
  17.670 +          mk_relmem (rcarg, lhs) Rvar
  17.671 +                    |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  17.672 +                    |> fold_rev (curry Logic.mk_implies) gs
  17.673 +                    |> fold_rev (mk_forall o Free) rcfix
  17.674 +                    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  17.675 +                    (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
  17.676 +
  17.677 +      val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
  17.678 +
  17.679 +      val (RIntro_thmss, (R, R_elim, lthy)) = 
  17.680 +          fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
  17.681 +    in
  17.682 +      ((R, RIntro_thmss, R_elim), lthy)
  17.683 +    end
  17.684  
  17.685  
  17.686 -      val n = length qglrs
  17.687 -      val trees = map (build_tree thy f congs ctx) qglrs
  17.688 +fun fix_globals domT ranT fvar ctxt =
  17.689 +    let
  17.690 +      val ([h, y, x, z, a, D, P, Pbool],ctxt') = 
  17.691 +          Variable.invent_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
  17.692 +    in
  17.693 +      (Globals {h = Free (h, domT --> ranT),
  17.694 +                y = Free (y, ranT),
  17.695 +                x = Free (x, domT),
  17.696 +                z = Free (z, domT),
  17.697 +                a = Free (a, domT),
  17.698 +                D = Free (D, HOLogic.mk_setT domT),
  17.699 +                P = Free (P, domT --> boolT),
  17.700 +                Pbool = Free (Pbool, boolT),
  17.701 +                fvar = fvar,
  17.702 +                domT = domT,
  17.703 +                ranT = ranT
  17.704 +               },
  17.705 +       ctxt')
  17.706 +    end
  17.707 +
  17.708 +
  17.709 +
  17.710 +fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
  17.711 +    let
  17.712 +      fun inst_term t = 
  17.713 +          subst_bound(f, abstract_over (fvar, t))
  17.714 +    in
  17.715 +      (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
  17.716 +    end
  17.717 +
  17.718 +
  17.719 +
  17.720 +fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs lthy =
  17.721 +    let
  17.722 +      val fvar = Free (fname, fT)
  17.723 +      val domT = domain_type fT
  17.724 +      val ranT = range_type fT
  17.725 +
  17.726 +      val congs = get_fundef_congs (Context.Proof lthy)
  17.727 +      val (globals, ctxt') = fix_globals domT ranT fvar lthy
  17.728 +
  17.729 +      val Globals { x, ... } = globals
  17.730 +
  17.731 +      val clauses = map (mk_clause_context x ctxt') abstract_qglrs 
  17.732 +
  17.733 +      val n = length abstract_qglrs
  17.734 +
  17.735 +      val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *)
  17.736 +              
  17.737 +      fun build_tree (ClauseContext { ctxt, rhs, ...}) = 
  17.738 +            FundefCtxTree.mk_tree congs_deps (fname, fT) ctxt rhs
  17.739 +
  17.740 +      val trees = map build_tree clauses
  17.741        val RCss = map find_calls trees
  17.742  
  17.743 -      val complete = mk_completeness names qglrs
  17.744 -                                     |> cterm_of thy
  17.745 -                                     |> assume
  17.746 +      val ((G, GIntro_thms, G_elim), lthy) = define_graph (defname ^ "_graph") fvar domT ranT clauses RCss lthy
  17.747 +      val ((f, f_defthm), lthy) = define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G lthy
  17.748 +
  17.749 +      val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
  17.750 +      val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
  17.751  
  17.752 -      val compat = mk_compat_proof_obligations qglrs glrs'
  17.753 -                           |> map (assume o cterm_of thy)
  17.754 +      val ((R, RIntro_thmss, R_elim), lthy) = 
  17.755 +          define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss lthy
  17.756  
  17.757 -      val compat_store = compat
  17.758 -                           |> store_compat_thms n
  17.759 +      val dom_abbrev = Logic.mk_equals (Free (defname ^ "_dom", fastype_of (mk_acc domT R)), mk_acc domT R)
  17.760 +      val lthy = Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)] lthy
  17.761  
  17.762 -      val R_intross = map2 (fn qglr => map (mk_RIntro R qglr)) qglrs RCss
  17.763 -      val G_intros = map2 (mk_GIntro thy f fvar G) qglrs RCss
  17.764 +      val newthy = ProofContext.theory_of lthy
  17.765 +      val clauses = map (transfer_clause_ctx newthy) clauses
  17.766  
  17.767 -      val (GIntro_thms, (thy, _, G_elim)) = inductive_def_wrap G_intros (thy, G)
  17.768 -      val (RIntro_thmss, (thy, _, R_elim)) = fold_burrow inductive_def_wrap R_intross (thy, R)
  17.769 +      val cert = cterm_of (ProofContext.theory_of lthy)
  17.770 +
  17.771 +      val xclauses = map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms RIntro_thmss
  17.772  
  17.773 -      val clauses = map6 (mk_clause_info thy names) (1 upto n) qglrs trees RCss GIntro_thms RIntro_thmss
  17.774 +      val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
  17.775 +      val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
  17.776 +
  17.777 +      val compat_store = store_compat_thms n compat
  17.778  
  17.779 -      val (goal, goalI, ex1_iff, values) = prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim
  17.780 +      val (goal, goalI, ex1_iff, values) = prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim f_defthm
  17.781      in
  17.782 -        (Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim},
  17.783 -         thy)
  17.784 +        (Prep {globals = globals, f = f, G = G, R = R, goal = goal, goalI = goalI, values = values, clauses = xclauses, ex1_iff = ex1_iff, R_cases = R_elim}, f,
  17.785 +         lthy)
  17.786      end
  17.787  
  17.788  
    18.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Wed Sep 13 00:38:38 2006 +0200
    18.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Wed Sep 13 12:05:50 2006 +0200
    18.3 @@ -28,25 +28,22 @@
    18.4  val wf_induct_rule = thm "wf_induct_rule";
    18.5  val Pair_inject = thm "Product_Type.Pair_inject";
    18.6  
    18.7 -val acc_induct_rule = thm "acc_induct_rule" (* from: Accessible_Part *)
    18.8 -val acc_downward = thm "acc_downward"
    18.9 -val accI = thm "accI"
   18.10 +val acc_induct_rule = thm "Accessible_Part.acc_induct_rule"
   18.11 +val acc_downward = thm "Accessible_Part.acc_downward"
   18.12 +val accI = thm "Accessible_Part.accI"
   18.13  
   18.14 -val ex1_implies_ex = thm "fundef_ex1_existence"   (* from: Fundef.thy *) 
   18.15 -val ex1_implies_un = thm "fundef_ex1_uniqueness"
   18.16 -val ex1_implies_iff = thm "fundef_ex1_iff"
   18.17 -val acc_subset_induct = thm "acc_subset_induct"
   18.18 +val acc_subset_induct = thm "Accessible_Part.acc_subset_induct"
   18.19  
   18.20  val conjunctionD1 = thm "conjunctionD1"
   18.21  val conjunctionD2 = thm "conjunctionD2"
   18.22  
   18.23  
   18.24 -    
   18.25 -fun mk_psimp thy names f_iff graph_is_function clause valthm =
   18.26 +fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
   18.27      let
   18.28 -	val Names {R, acc_R, domT, z, ...} = names
   18.29 -	val ClauseInfo {qs, cqs, gs, lhs, rhs, ...} = clause
   18.30 -	val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, acc_R))) (* "lhs : acc R" *)
   18.31 +	val Globals {domT, z, ...} = globals
   18.32 +
   18.33 +	val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
   18.34 +	val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, mk_acc domT R))) (* "lhs : acc R" *)
   18.35  	val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *)
   18.36      in
   18.37  	((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
   18.38 @@ -56,14 +53,16 @@
   18.39  	    |> (fn it => it COMP valthm)
   18.40  	    |> implies_intr lhs_acc 
   18.41  	    |> asm_simplify (HOL_basic_ss addsimps [f_iff])
   18.42 +            |> fold_rev (implies_intr o cprop_of) ags
   18.43 +            |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   18.44      end
   18.45  
   18.46  
   18.47  
   18.48 -
   18.49 -fun mk_partial_induct_rule thy names complete_thm clauses =
   18.50 +fun mk_partial_induct_rule thy globals R complete_thm clauses =
   18.51      let
   18.52 -	val Names {domT, R, acc_R, x, z, a, P, D, ...} = names
   18.53 +	val Globals {domT, x, z, a, P, D, ...} = globals
   18.54 +        val acc_R = mk_acc domT R
   18.55  
   18.56  	val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D))))
   18.57  	val a_D = cterm_of thy (Trueprop (mk_mem (a, D)))
   18.58 @@ -88,7 +87,8 @@
   18.59  
   18.60  	fun prove_case clause =
   18.61  	    let
   18.62 -		val ClauseInfo {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause
   18.63 +		val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs, 
   18.64 +                                qglr = (oqs, _, _, _), ...} = clause
   18.65  								       
   18.66  		val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
   18.67  		val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
   18.68 @@ -106,7 +106,7 @@
   18.69  				    |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   18.70  				    |> fold_rev (curry Logic.mk_implies) gs
   18.71  				    |> curry Logic.mk_implies (Trueprop (mk_mem (lhs, D)))
   18.72 -				    |> fold_rev mk_forall qs
   18.73 +				    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   18.74  				    |> cterm_of thy
   18.75  			   
   18.76  		val P_lhs = assume step
   18.77 @@ -130,10 +130,10 @@
   18.78  
   18.79  	val istep =  complete_thm
   18.80                         |> forall_elim_vars 0
   18.81 -			 |> fold (curry op COMP) cases (*  P x  *)
   18.82 -			 |> implies_intr ihyp
   18.83 -			 |> implies_intr (cprop_of x_D)
   18.84 -			 |> forall_intr (cterm_of thy x)
   18.85 +		       |> fold (curry op COMP) cases (*  P x  *)
   18.86 +		       |> implies_intr ihyp
   18.87 +		       |> implies_intr (cprop_of x_D)
   18.88 +		       |> forall_intr (cterm_of thy x)
   18.89  			   
   18.90  	val subset_induct_rule = 
   18.91  	    acc_subset_induct
   18.92 @@ -166,189 +166,13 @@
   18.93  
   18.94  
   18.95  
   18.96 -(***********************************************)
   18.97 -(* Compat thms are stored in normal form (with vars) *)
   18.98 -
   18.99 -(* replace this by a table later*)
  18.100 -fun store_compat_thms 0 cts = []
  18.101 -  | store_compat_thms n cts =
  18.102 +(* Does this work with Guards??? *)
  18.103 +fun mk_domain_intro thy globals R R_cases clause =
  18.104      let
  18.105 -	val (cts1, cts2) = chop n cts
  18.106 -    in
  18.107 -	(cts1 :: store_compat_thms (n - 1) cts2)
  18.108 -    end
  18.109 -
  18.110 -
  18.111 -(* needs i <= j *)
  18.112 -fun lookup_compat_thm i j cts =
  18.113 -    nth (nth cts (i - 1)) (j - i)
  18.114 -(***********************************************)
  18.115 -
  18.116 -
  18.117 -(* recover the order of Vars *)
  18.118 -fun get_var_order thy clauses =
  18.119 -    map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (unordered_pairs clauses)
  18.120 -
  18.121 -
  18.122 -(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
  18.123 -(* if j < i, then turn around *)
  18.124 -fun get_compat_thm thy cts clausei clausej =
  18.125 -    let 
  18.126 -	val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
  18.127 -	val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
  18.128 -
  18.129 -	val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
  18.130 -    in if j < i then
  18.131 -	   let 
  18.132 -	       val (var_ord, compat) = lookup_compat_thm j i cts
  18.133 -	   in
  18.134 -	       compat         (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
  18.135 -		|> instantiate ([],(var_ord ~~ (qsj' @ qsi))) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *)
  18.136 -		|> fold implies_elim_swp gsj'
  18.137 -		|> fold implies_elim_swp gsi
  18.138 -		|> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
  18.139 -	   end
  18.140 -       else
  18.141 -	   let
  18.142 -	       val (var_ord, compat) = lookup_compat_thm i j cts
  18.143 -	   in
  18.144 -	       compat        (* "?Gsi => ?Gsj' => ?lhsi = ?lhsj' ==> ?rhsi = ?rhsj'" *)
  18.145 -	         |> instantiate ([], (var_ord ~~ (qsi @ qsj'))) (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
  18.146 -		 |> fold implies_elim_swp gsi
  18.147 -		 |> fold implies_elim_swp gsj'
  18.148 -		 |> implies_elim_swp (assume lhsi_eq_lhsj')
  18.149 -		 |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
  18.150 -	   end
  18.151 -    end
  18.152 -
  18.153 -
  18.154 -
  18.155 -
  18.156 -
  18.157 -
  18.158 -
  18.159 -(* Generates the replacement lemma with primed variables. A problem here is that one should not do
  18.160 -the complete requantification at the end to replace the variables. One should find a way to be more efficient
  18.161 -here. *)
  18.162 -fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = 
  18.163 -    let 
  18.164 -	val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
  18.165 -	val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
  18.166 -
  18.167 -	val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
  18.168 -
  18.169 -	val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
  18.170 -	val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
  18.171 -	val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
  18.172 -
  18.173 -	val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
  18.174 -
  18.175 -	val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
  18.176 -
  18.177 -	val replace_lemma = (eql RS meta_eq_to_obj_eq)
  18.178 -				|> implies_intr (cprop_of case_hyp)
  18.179 -				|> fold_rev (implies_intr o cprop_of) h_assums
  18.180 -				|> fold_rev (implies_intr o cprop_of) ags
  18.181 -				|> fold_rev forall_intr cqs
  18.182 -				|> fold forall_elim cqs'
  18.183 -				|> fold implies_elim_swp ags'
  18.184 -				|> fold implies_elim_swp h_assums'
  18.185 -    in
  18.186 -      replace_lemma
  18.187 -    end
  18.188 -
  18.189 -
  18.190 -
  18.191 -
  18.192 -fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
  18.193 -    let
  18.194 -	val Names {f, h, y, ...} = names
  18.195 -	val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
  18.196 -	val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
  18.197 -
  18.198 -	val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
  18.199 -	val compat = get_compat_thm thy compat_store clausei clausej
  18.200 -	val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
  18.201 -
  18.202 -	val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
  18.203 -	val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j'	*)
  18.204 -
  18.205 -	val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
  18.206 -    in
  18.207 -	(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
  18.208 -        |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
  18.209 -	|> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
  18.210 -	|> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
  18.211 -	|> implies_intr (cprop_of y_eq_rhsj'h)
  18.212 -	|> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
  18.213 -	|> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
  18.214 -	|> implies_elim_swp eq_pairs
  18.215 -	|> fold_rev (implies_intr o cprop_of) Ghsj' 
  18.216 -	|> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
  18.217 -	|> implies_intr (cprop_of eq_pairs)
  18.218 -	|> fold_rev forall_intr ordcqs'j
  18.219 -    end
  18.220 -
  18.221 -
  18.222 -
  18.223 -fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
  18.224 -    let
  18.225 -	val Names {x, y, G, fvar, f, ranT, ...} = names
  18.226 -	val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
  18.227 -
  18.228 -	val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
  18.229 -
  18.230 -	fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
  18.231 -                                                            |> fold_rev (implies_intr o cprop_of) CCas
  18.232 -						            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  18.233 -
  18.234 -	val existence = lGI |> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])
  18.235 -			    |> fold (curry op COMP o prep_RC) RCs 
  18.236 -
  18.237 -
  18.238 -	val a = cterm_of thy (mk_prod (lhs, y))
  18.239 -	val P = cterm_of thy (mk_eq (y, rhs))
  18.240 -	val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
  18.241 -
  18.242 -	val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
  18.243 -
  18.244 -	val uniqueness = G_cases 
  18.245 -			     |> instantiate' [] [SOME a, SOME P]
  18.246 -			     |> implies_elim_swp a_in_G
  18.247 -			     |> fold implies_elim_swp unique_clauses
  18.248 -			     |> implies_intr (cprop_of a_in_G)
  18.249 -			     |> forall_intr (cterm_of thy y) 
  18.250 -
  18.251 -	val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
  18.252 -
  18.253 -	val exactly_one =
  18.254 -	    ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
  18.255 -		 |> curry (op COMP) existence
  18.256 -		 |> curry (op COMP) uniqueness
  18.257 -		 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
  18.258 -		 |> implies_intr (cprop_of case_hyp) 
  18.259 -		 |> fold_rev (implies_intr o cprop_of) ags
  18.260 -		 |> fold_rev forall_intr cqs
  18.261 -	val function_value =
  18.262 -	    existence 
  18.263 -		|> fold_rev (implies_intr o cprop_of) ags
  18.264 -		|> implies_intr ihyp
  18.265 -		|> implies_intr (cprop_of case_hyp)
  18.266 -		|> forall_intr (cterm_of thy x)
  18.267 -		|> forall_elim (cterm_of thy lhs)
  18.268 -		|> curry (op RS) refl
  18.269 -    in
  18.270 -	(exactly_one, function_value)
  18.271 -    end
  18.272 -
  18.273 -
  18.274 -
  18.275 -(* Does this work with Guards??? *)
  18.276 -fun mk_domain_intro thy names R_cases clause =
  18.277 -    let
  18.278 -	val Names {z, R, acc_R, ...} = names
  18.279 -	val ClauseInfo {qs, gs, lhs, rhs, ...} = clause
  18.280 -	val goal = (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
  18.281 +	val Globals {z, domT, ...} = globals
  18.282 +	val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
  18.283 +                        qglr = (oqs, _, _, _), ...} = clause
  18.284 +	val goal = (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs, mk_acc domT R)))
  18.285                       |> fold_rev (curry Logic.mk_implies) gs
  18.286                       |> cterm_of thy
  18.287      in
  18.288 @@ -357,15 +181,17 @@
  18.289  		  |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1))  |> the
  18.290  		  |> (SINGLE (CLASIMPSET auto_tac)) |> the
  18.291  		  |> Goal.conclude
  18.292 +                  |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  18.293      end
  18.294  
  18.295  
  18.296  
  18.297  
  18.298 -fun mk_nest_term_case thy names R' ihyp clause =
  18.299 +fun mk_nest_term_case thy globals R' ihyp clause =
  18.300      let
  18.301 -	val Names {x, z, ...} = names
  18.302 -	val ClauseInfo {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause
  18.303 +	val Globals {x, z, ...} = globals
  18.304 +	val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
  18.305 +                        qglr=(oqs, _, _, _), ...} = clause
  18.306  
  18.307  	val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
  18.308  
  18.309 @@ -377,7 +203,7 @@
  18.310  				    |> fold_rev (curry Logic.mk_implies o prop_of) used
  18.311  				    |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
  18.312  				    |> fold_rev (curry Logic.mk_implies o prop_of) ags
  18.313 -				    |> fold_rev mk_forall qs
  18.314 +				    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  18.315  				    |> cterm_of thy
  18.316  
  18.317  		val thm = assume hyp
  18.318 @@ -398,16 +224,10 @@
  18.319  
  18.320  		val zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs))))
  18.321  
  18.322 -		val z_acc' = (z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject))
  18.323 -                               |> FundefCtxTree.export_thm thy ([], (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes))
  18.324 -
  18.325 -                val occvars = fold (OrdList.insert Term.term_ord) (term_frees (prop_of z_acc')) [] 
  18.326 -                val ordvars = fold (OrdList.insert Term.term_ord) (map Free fixes @ qs) [] (* FIXME... remove when inductive behaves nice *)
  18.327 -                                   |> OrdList.inter Term.term_ord occvars
  18.328 -
  18.329 -		val ethm = z_acc'
  18.330 -			       |> FundefCtxTree.export_thm thy (map dest_Free ordvars, [])
  18.331 -
  18.332 +		val ethm = (z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject))
  18.333 +			       |> FundefCtxTree.export_thm thy (fixes, 
  18.334 +                                                                (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes))
  18.335 +                               |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  18.336  
  18.337  		val sub' = sub @ [(([],[]), acc)]
  18.338  	    in
  18.339 @@ -419,11 +239,10 @@
  18.340      end
  18.341  
  18.342  
  18.343 -fun mk_nest_term_rule thy names clauses =
  18.344 +fun mk_nest_term_rule thy globals R R_cases clauses =
  18.345      let
  18.346 -	val Names { R, acc_R, domT, x, z, ... } = names
  18.347 -
  18.348 -	val R_elim = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R))))))
  18.349 +	val Globals { domT, x, z, ... } = globals
  18.350 +        val acc_R = mk_acc domT R
  18.351  
  18.352  	val R' = Free ("R", fastype_of R)
  18.353  
  18.354 @@ -439,13 +258,12 @@
  18.355  	val ihyp_a = assume ihyp |> forall_elim_vars 0
  18.356  
  18.357  	val z_ltR_x = cterm_of thy (mk_relmem (z, x) R) (* "(z, x) : R" *)
  18.358 -	val z_acc = cterm_of thy (mk_mem (z, acc_R))
  18.359  
  18.360 -	val (hyps,cases) = fold (mk_nest_term_case thy names R' ihyp_a) clauses ([],[])
  18.361 +	val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
  18.362      in
  18.363 -	R_elim
  18.364 -	    |> Thm.freezeT
  18.365 -	    |> instantiate' [] [SOME (cterm_of thy (mk_prod (z,x))), SOME z_acc]
  18.366 +	R_cases
  18.367 +            |> forall_elim (cterm_of thy (mk_prod (z,x)))
  18.368 +            |> forall_elim (cterm_of thy (mk_mem (z, acc_R)))
  18.369  	    |> curry op COMP (assume z_ltR_x)
  18.370  	    |> fold_rev (curry op COMP) cases
  18.371  	    |> implies_intr z_ltR_x
  18.372 @@ -465,8 +283,7 @@
  18.373  
  18.374  fun mk_partial_rules thy data provedgoal =
  18.375      let
  18.376 -	val Prep {names, clauses, values, R_cases, ex1_iff, ...} = data
  18.377 -	val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
  18.378 +	val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
  18.379  
  18.380          val _ = print "Closing Derivation"
  18.381  
  18.382 @@ -486,16 +303,16 @@
  18.383  	val f_iff = (graph_is_function RS ex1_iff) 
  18.384  
  18.385  	val _ = Output.debug "Proving simplification rules"
  18.386 -	val psimps  = map2 (mk_psimp thy names f_iff graph_is_function) clauses values
  18.387 +	val psimps  = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
  18.388  
  18.389  	val _ = Output.debug "Proving partial induction rule"
  18.390 -	val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy names complete_thm clauses
  18.391 +	val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
  18.392  
  18.393  	val _ = Output.debug "Proving nested termination rule"
  18.394 -	val total_intro = mk_nest_term_rule thy names clauses
  18.395 +	val total_intro = mk_nest_term_rule thy globals R R_cases clauses
  18.396  
  18.397  	val _ = Output.debug "Proving domain introduction rules"
  18.398 -	val dom_intros = map (mk_domain_intro thy names R_cases) clauses
  18.399 +	val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
  18.400      in 
  18.401  	FundefResult {f=f, G=G, R=R, completeness=complete_thm, 
  18.402  	 psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Wed Sep 13 12:05:50 2006 +0200
    19.3 @@ -0,0 +1,110 @@
    19.4 +(*  Title:      HOL/Tools/function_package/inductive_wrap.ML
    19.5 +    ID:         $Id$
    19.6 +    Author:     Alexander Krauss, TU Muenchen
    19.7 +
    19.8 +
    19.9 +This is a wrapper around the inductive package which corrects some of its
   19.10 +slightly annoying behaviours and makes the whole business more controllable.
   19.11 +
   19.12 +Specifically:
   19.13 +
   19.14 +- Following newer Isar conventions, declaration and definition are done in one step
   19.15 +
   19.16 +- The specification is expected in fully quantified form. This allows the client to 
   19.17 +  control the variable order. The variables will appear in the result in the same order.
   19.18 +  This is especially relevant for the elimination rule, where the order usually *does* matter.
   19.19 +
   19.20 +
   19.21 +All this will probably become obsolete in the near future, when the new "predicate" package
   19.22 +is in place.
   19.23 +
   19.24 +*)
   19.25 +
   19.26 +signature FUNDEF_INDUCTIVE_WRAP =
   19.27 +sig
   19.28 +  val inductive_def :  term list 
   19.29 +                       -> ((bstring * typ) * mixfix) * local_theory
   19.30 +                       -> thm list * (term * thm * local_theory)
   19.31 +end
   19.32 +
   19.33 +structure FundefInductiveWrap =
   19.34 +struct
   19.35 +
   19.36 +
   19.37 +fun inst_forall (Free (n,_)) (_ $ Abs (_, T, b)) = subst_bound (Free (n, T), b)
   19.38 +  | inst_forall t1 t2 = sys_error ((Sign.string_of_term (the_context ()) t1))
   19.39 +
   19.40 +fun permute_bounds_in_premises thy [] impl = impl
   19.41 +  | permute_bounds_in_premises thy ((oldvs, newvs) :: perms) impl =
   19.42 +    let
   19.43 +      val (prem, concl) = dest_implies (cprop_of impl)
   19.44 +
   19.45 +      val newprem = term_of prem
   19.46 +                      |> fold inst_forall oldvs
   19.47 +                      |> fold_rev mk_forall newvs
   19.48 +                      |> cterm_of thy
   19.49 +    in
   19.50 +      assume newprem
   19.51 +             |> fold (forall_elim o cterm_of thy) newvs
   19.52 +             |> fold_rev (forall_intr o cterm_of thy) oldvs
   19.53 +             |> implies_elim impl
   19.54 +             |> permute_bounds_in_premises thy perms
   19.55 +             |> implies_intr newprem
   19.56 +    end
   19.57 +
   19.58 +
   19.59 +fun inductive_def defs (((R, T), mixfix), lthy) =
   19.60 +    let
   19.61 +      fun wrap1 thy =
   19.62 +          let
   19.63 +            val thy = Sign.add_consts_i [(R, T, mixfix)] thy
   19.64 +            val RC = Const (Sign.full_name thy R, T)
   19.65 +
   19.66 +            val cdefs = map (Pattern.rewrite_term thy [(Free (R, T), RC)] []) defs
   19.67 +            val qdefs = map dest_all_all cdefs
   19.68 +
   19.69 +            val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) =
   19.70 +                InductivePackage.add_inductive_i true (*verbose*)
   19.71 +                                                 false (* dont add_consts *)
   19.72 +                                                 "" (* no altname *)
   19.73 +                                                 false (* no coind *)
   19.74 +                                                 false (* elims, please *)
   19.75 +                                                 false (* induction thm please *)
   19.76 +                                                 [RC] (* the constant *)
   19.77 +                                                 (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *)
   19.78 +                                                 [] (* no special monos *)
   19.79 +                                                 thy
   19.80 +
   19.81 +            val perms = map (fn (qs, t) => ((term_frees t) inter qs, qs)) qdefs
   19.82 +
   19.83 +            fun inst (qs, _) intr_gen =
   19.84 +                intr_gen
   19.85 +                  |> Thm.freezeT
   19.86 +                  |> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs
   19.87 +
   19.88 +
   19.89 +            val a = cterm_of thy (Free ("a0123", HOLogic.dest_setT T)) (* Let's just hope there are no clashes :-} *)
   19.90 +            val P = cterm_of thy (Free ("P0123", HOLogic.boolT))
   19.91 +                
   19.92 +            val intrs = map2 inst qdefs intrs_gen
   19.93 +
   19.94 +            val elim = elim_gen
   19.95 +                         |> Thm.freezeT
   19.96 +                         |> forall_intr_vars (* FIXME... *)
   19.97 +                         |> forall_elim a
   19.98 +                         |> forall_elim P
   19.99 +                         |> permute_bounds_in_premises thy (([],[]) :: perms)
  19.100 +                         |> forall_intr P
  19.101 +                         |> forall_intr a
  19.102 +          in
  19.103 +            ((RC, (intrs, elim)), thy)
  19.104 +          end
  19.105 +
  19.106 +      val ((RC, (intrs, elim)), lthy) = LocalTheory.theory_result wrap1 lthy
  19.107 +    in
  19.108 +      (intrs, (RC, elim, lthy))
  19.109 +    end
  19.110 +
  19.111 +
  19.112 +end
  19.113 +
    20.1 --- a/src/HOL/Tools/function_package/mutual.ML	Wed Sep 13 00:38:38 2006 +0200
    20.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Wed Sep 13 12:05:50 2006 +0200
    20.3 @@ -10,12 +10,17 @@
    20.4  signature FUNDEF_MUTUAL = 
    20.5  sig
    20.6    
    20.7 -  val prepare_fundef_mutual : thm list -> term list list -> theory ->
    20.8 -                              (FundefCommon.mutual_info * string * (FundefCommon.prep_result * theory))
    20.9 +  val prepare_fundef_mutual : ((string * typ) * mixfix) list 
   20.10 +                              -> term list 
   20.11 +                              -> local_theory 
   20.12 +                              -> ((FundefCommon.mutual_info * string * FundefCommon.prep_result) * local_theory)
   20.13  
   20.14  
   20.15 -  val mk_partial_rules_mutual : theory -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> 
   20.16 +  val mk_partial_rules_mutual : Proof.context -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> 
   20.17                                  FundefCommon.fundef_mresult
   20.18 +
   20.19 +  val sort_by_function : FundefCommon.mutual_info -> string list -> 'a list -> 'a list list
   20.20 +
   20.21  end
   20.22  
   20.23  
   20.24 @@ -24,46 +29,83 @@
   20.25  
   20.26  open FundefCommon
   20.27  
   20.28 +(* Theory dependencies *)
   20.29 +val sum_case_rules = thms "Datatype.sum.cases"
   20.30 +val split_apply = thm "Product_Type.split"
   20.31 +
   20.32  
   20.33  
   20.34 -fun check_const (Const C) = C
   20.35 -  | check_const _ = raise ERROR "Head symbol of every left hand side must be a constant." (* FIXME: Output the equation here *)
   20.36 +fun mutual_induct_Pnames n = 
   20.37 +    if n < 5 then fst (chop n ["P","Q","R","S"])
   20.38 +    else map (fn i => "P" ^ string_of_int i) (1 upto n)
   20.39 +	 
   20.40 +
   20.41 +fun check_head fs t =
   20.42 +    if (case t of 
   20.43 +          (Free (n, _)) => n mem fs
   20.44 +        | _ => false)
   20.45 +    then dest_Free t
   20.46 +    else raise ERROR "Head symbol of every left hand side must be the new function." (* FIXME: Output the equation here *)
   20.47  
   20.48  
   20.49 +fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
   20.50 +  | open_all_all t = ([], t)
   20.51  
   20.52  
   20.53  
   20.54 -fun split_def geq =
   20.55 +(* Builds a curried clause description in abstracted form *)
   20.56 +fun split_def fnames geq =
   20.57      let
   20.58 -	val gs = Logic.strip_imp_prems geq
   20.59 -	val eq = Logic.strip_imp_concl geq
   20.60 -	val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
   20.61 -	val (fc, args) = strip_comb f_args
   20.62 -	val f = check_const fc
   20.63 -		    
   20.64 -	val qs = fold_rev Term.add_frees args []
   20.65 -		 
   20.66 -	val rhs_new_vars = (Term.add_frees rhs []) \\ qs
   20.67 -	val _ = if null rhs_new_vars then () 
   20.68 -		else raise ERROR "Variables occur on right hand side only: " (* FIXME: Output vars here *)
   20.69 +      val (qs, imp) = open_all_all geq
   20.70 +
   20.71 +      val gs = Logic.strip_imp_prems imp
   20.72 +      val eq = Logic.strip_imp_concl imp
   20.73 +
   20.74 +      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
   20.75 +      val (fc, args) = strip_comb f_args
   20.76 +      val f as (fname, _) = check_head fnames fc
   20.77 +
   20.78 +      val add_bvs = fold_aterms (fn Bound i => insert (op =) i | _ => I)
   20.79 +      val rhs_only = (add_bvs rhs [] \\ fold add_bvs args [])
   20.80 +                        |> map (fst o nth (rev qs))
   20.81 +      val _ = if null rhs_only then () 
   20.82 +	      else raise ERROR "Variables occur on right hand side only." (* FIXME: Output vars *)
   20.83      in
   20.84 -	((f, length args), (qs, gs, args, rhs))
   20.85 +	((f, length args), (fname, qs, gs, args, rhs))
   20.86      end
   20.87  
   20.88 +fun get_part fname =
   20.89 +    the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
   20.90  
   20.91 -fun analyze_eqs thy eqss =
   20.92 +(* FIXME *)
   20.93 +fun mk_prod_abs e (t1, t2) =
   20.94 +    let 
   20.95 +      val bTs = rev (map snd e)
   20.96 +      val T1 = fastype_of1 (bTs, t1)
   20.97 +      val T2 = fastype_of1 (bTs, t2)
   20.98 +    in
   20.99 +      HOLogic.pair_const T1 T2 $ t1 $ t2
  20.100 +    end;
  20.101 +
  20.102 +
  20.103 +fun analyze_eqs ctxt fnames eqs =
  20.104      let
  20.105 +      (* FIXME: Add check for number of arguments
  20.106  	fun all_equal ((x as ((n:string,T), k:int))::xs) = if forall (fn ((n',_),k') => n = n' andalso k = k') xs then x
  20.107  							   else raise ERROR ("All equations in a block must describe the same "
  20.108 -									     ^ "constant and have the same number of arguments.")
  20.109 +									     ^ "function and have the same number of arguments.")
  20.110 +       *)
  20.111  								      
  20.112 -	val def_infoss = map (split_list o map split_def) eqss
  20.113 -	val (consts, qgarss) = split_list (map (fn (Cis, eqs) => (all_equal Cis, eqs)) def_infoss)
  20.114 +        val (consts, fqgars) = split_list (map (split_def fnames) eqs)
  20.115  
  20.116 -	val cnames = map (fst o fst) consts
  20.117 -	val check_rcs = exists_Const (fn (n,_) => if n mem cnames 
  20.118 -						  then raise ERROR "Recursive Calls not allowed in premises." else false)
  20.119 -	val _ = forall (forall (fn (_, gs, _, _) => forall check_rcs gs)) qgarss
  20.120 +        val different_consts = distinct (eq_fst (eq_fst eq_str)) consts
  20.121 +	val cnames = map (fst o fst) different_consts
  20.122 +
  20.123 +	val check_rcs = exists_subterm (fn Free (n, _) => if n mem cnames 
  20.124 +						          then raise ERROR "Recursive Calls not allowed in premises." else false
  20.125 +                                         | _ => false)
  20.126 +                        
  20.127 +	val _ = forall (fn (_, _, gs, _, _) => forall check_rcs gs) fqgars
  20.128  
  20.129  	fun curried_types ((_,T), k) =
  20.130  	    let
  20.131 @@ -72,61 +114,87 @@
  20.132  		(caTs, uaTs ---> body_type T)
  20.133  	    end
  20.134  
  20.135 -	val (caTss, resultTs) = split_list (map curried_types consts)
  20.136 +	val (caTss, resultTs) = split_list (map curried_types different_consts)
  20.137  	val argTs = map (foldr1 HOLogic.mk_prodT) caTss
  20.138  
  20.139 -	val (RST,streeR, pthsR) = SumTools.mk_tree resultTs
  20.140 +	val (RST,streeR, pthsR) = SumTools.mk_tree_distinct resultTs
  20.141  	val (ST, streeA, pthsA) = SumTools.mk_tree argTs
  20.142  
  20.143  	val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name cnames)
  20.144 -	val sfun_xname = def_name ^ "_sum"
  20.145 -	val sfun_type = ST --> RST
  20.146 +	val fsum_type = ST --> RST
  20.147  
  20.148 -    	val thy = Sign.add_consts_i [(sfun_xname, sfun_type, NoSyn)] thy (* Add the sum function *)
  20.149 -	val sfun = Const (Sign.full_name thy sfun_xname, sfun_type)
  20.150 +        val ([fsum_var_name], _) = Variable.add_fixes [ def_name ^ "_sum" ] ctxt
  20.151 +        val fsum_var = (fsum_var_name, fsum_type)
  20.152  
  20.153 -	fun define (((((n, T), _), caTs), (pthA, pthR)), qgars) (thy, rews) = 
  20.154 +	fun define (fvar as (n, T), _) caTs pthA pthR = 
  20.155  	    let 
  20.156 -		val fxname = Sign.base_name n
  20.157 -		val f = Const (n, T)
  20.158 -		val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs
  20.159 +		val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs (* FIXME: Bind xs properly *)
  20.160  
  20.161 -		val f_exp = SumTools.mk_proj streeR pthR (sfun $ SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod vars))
  20.162 -		val def = Logic.mk_equals (list_comb (f, vars), f_exp)
  20.163 -
  20.164 -		val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy
  20.165 -		val rews' = (f, fold_rev lambda vars f_exp) :: rews
  20.166 +		val f_exp = SumTools.mk_proj streeR pthR (Free fsum_var $ SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod vars))
  20.167 +		val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
  20.168 +                                          
  20.169 +		val rew = (n, fold_rev lambda vars f_exp) 
  20.170  	    in
  20.171 -		(MutualPart {f_name=fxname, const=(n, T),cargTs=caTs,pthA=pthA,pthR=pthR,qgars=qgars,f_def=f_def}, (thy, rews'))
  20.172 +		(MutualPart {fvar=fvar,cargTs=caTs,pthA=pthA,pthR=pthR,f_def=def,f=NONE,f_defthm=NONE}, rew)
  20.173  	    end
  20.174  
  20.175 -	val (parts, (thy, rews)) = fold_map define (((consts ~~ caTss)~~ (pthsA ~~ pthsR)) ~~ qgarss) (thy, [])
  20.176 +	val (parts, rews) = split_list (map4 define different_consts caTss pthsA pthsR)
  20.177  
  20.178 -	fun mk_qglrss (MutualPart {qgars, pthA, pthR, ...}) =
  20.179 -	    let
  20.180 -		fun convert_eqs (qs, gs, args, rhs) =
  20.181 -		    (map Free qs, gs, SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod args), 
  20.182 -		     SumTools.mk_inj streeR pthR (Pattern.rewrite_term thy rews [] rhs))
  20.183 -	    in
  20.184 -		map convert_eqs qgars
  20.185 -	    end
  20.186 -	    
  20.187 -	val qglrss = map mk_qglrss parts
  20.188 +        fun convert_eqs (f, qs, gs, args, rhs) =
  20.189 +            let
  20.190 +              val MutualPart {pthA, pthR, ...} = get_part f parts
  20.191 +            in
  20.192 +	      (qs, gs, SumTools.mk_inj streeA pthA (foldr1 (mk_prod_abs qs) args), 
  20.193 +	       SumTools.mk_inj streeR pthR (replace_frees rews rhs)
  20.194 +                               |> Envir.norm_term (Envir.empty 0))
  20.195 +            end
  20.196 +
  20.197 +	val qglrs = map convert_eqs fqgars
  20.198      in
  20.199 -	(Mutual {name=def_name,sum_const=dest_Const sfun, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts, qglrss=qglrss}, thy)
  20.200 +	Mutual {defname=def_name,fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, 
  20.201 +                parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
  20.202      end
  20.203  
  20.204  
  20.205  
  20.206  
  20.207 -fun prepare_fundef_mutual congs eqss thy =
  20.208 +fun define_projections fixes mutual fsum lthy =
  20.209 +    let
  20.210 +      fun def ((MutualPart {fvar=(fname, fT), cargTs, pthA, pthR, f_def, ...}), (_, mixfix)) lthy =
  20.211 +          let
  20.212 +            val ((f, (_, f_defthm)), lthy') = LocalTheory.def ((fname, mixfix), 
  20.213 +                                                               ((fname ^ "_def", []), Term.subst_bound (fsum, f_def))) 
  20.214 +                                                              lthy
  20.215 +          in
  20.216 +            (MutualPart {fvar=(fname, fT), cargTs=cargTs, pthA=pthA, pthR=pthR, f_def=f_def, 
  20.217 +                        f=SOME f, f_defthm=SOME f_defthm },
  20.218 +             lthy')
  20.219 +          end
  20.220 +
  20.221 +      val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual
  20.222 +      val (parts', lthy') = fold_map def (parts ~~ fixes) lthy 
  20.223 +    in
  20.224 +      (Mutual { defname=defname, fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts', 
  20.225 +                fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
  20.226 +       lthy')
  20.227 +    end
  20.228 +
  20.229 +
  20.230 +
  20.231 +  
  20.232 +
  20.233 +
  20.234 +fun prepare_fundef_mutual fixes eqss lthy =
  20.235      let 
  20.236 -	val (mutual, thy) = analyze_eqs thy eqss
  20.237 -	val Mutual {name, sum_const, qglrss, ...} = mutual
  20.238 -	val global_glrs = flat qglrss
  20.239 -	val used = fold (fn (qs, _, _, _) => fold (curry op ins_string o fst o dest_Free) qs) global_glrs []
  20.240 +	val mutual = analyze_eqs lthy (map (fst o fst) fixes) eqss
  20.241 +	val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
  20.242 +
  20.243 +        val (prep_result, fsum, lthy') =
  20.244 +            FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs lthy
  20.245 +
  20.246 +        val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
  20.247      in
  20.248 -	(mutual, name, FundefPrep.prepare_fundef thy congs name (Const sum_const) global_glrs used)
  20.249 +      ((mutual', defname, prep_result), lthy'')
  20.250      end
  20.251  
  20.252  
  20.253 @@ -140,48 +208,76 @@
  20.254  	transitive (symmetric lhs_conv) (transitive thm rhs_conv)
  20.255      end
  20.256  
  20.257 -
  20.258 -
  20.259 -
  20.260 -fun map_mutual2 f (Mutual {parts, ...}) =
  20.261 -    map2 (fn (p as MutualPart {qgars, ...}) => map2 (f p) qgars) parts
  20.262 -
  20.263 +fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm
  20.264  
  20.265  
  20.266 -fun recover_mutual_psimp thy RST streeR all_f_defs (MutualPart {f_def, pthR, ...}) (_,_,args,_) sum_psimp =
  20.267 +fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
  20.268      let
  20.269 -	val conds = cprems_of sum_psimp (* dom-condition and guards *)
  20.270 -	val plain_eq = sum_psimp
  20.271 -                         |> fold (implies_elim_swp o assume) conds
  20.272 +      val thy = ProofContext.theory_of ctxt
  20.273  
  20.274 -	val x = Free ("x", RST)
  20.275 +      val oqnames = map fst pre_qs
  20.276 +      val (qs, ctxt') = Variable.invent_fixes oqnames ctxt
  20.277 +                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
  20.278  
  20.279 -	val f_def_inst = instantiate' [] (map (SOME o cterm_of thy) args) (Thm.freezeT f_def) (* FIXME: freezeT *)
  20.280 +      fun inst t = subst_bounds (rev qs, t)
  20.281 +      val gs = map inst pre_gs
  20.282 +      val args = map inst pre_args
  20.283 +      val rhs = inst pre_rhs
  20.284 +
  20.285 +      val cqs = map (cterm_of thy) qs
  20.286 +      val ags = map (assume o cterm_of thy) gs
  20.287 +                
  20.288 +      val import = fold forall_elim cqs
  20.289 +                   #> fold implies_elim_swp ags
  20.290 +
  20.291 +      val export = fold_rev (implies_intr o cprop_of) ags
  20.292 +                   #> fold_rev forall_intr_rename (oqnames ~~ cqs)
  20.293      in
  20.294 -	reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x)))  (*  PR(x) == PR(x) *)
  20.295 -		  |> (fn it => combination it (plain_eq RS eq_reflection))
  20.296 -		  |> beta_norm_eq (*  PR(S(I(as))) == PR(IR(...)) *)
  20.297 -		  |> transitive f_def_inst (*  f ... == PR(IR(...)) *)
  20.298 -		  |> simplify (HOL_basic_ss addsimps [SumTools.projl_inl, SumTools.projr_inr]) (*  f ... == ... *)
  20.299 -		  |> simplify (HOL_basic_ss addsimps all_f_defs) (*  f ... == ... *)
  20.300 -		  |> (fn it => it RS meta_eq_to_obj_eq)
  20.301 -		  |> fold_rev implies_intr conds
  20.302 +      F (f, qs, gs, args, rhs) import export
  20.303      end
  20.304  
  20.305  
  20.306 +fun recover_mutual_psimp thy RST streeR all_f_defs parts (f, _, _, args, _) import (export : thm -> thm) sum_psimp_eq =
  20.307 +    let
  20.308 +      val (MutualPart {f_defthm=SOME f_def, pthR, ...}) = get_part f parts
  20.309  
  20.310 +      val psimp = import sum_psimp_eq
  20.311 +      val (simp, restore_cond) = case cprems_of psimp of
  20.312 +                                   [] => (psimp, I)
  20.313 +                                 | [cond] => (implies_elim psimp (assume cond), implies_intr cond)
  20.314 +                                 | _ => sys_error "Too many conditions"
  20.315 +
  20.316 +      val x = Free ("x", RST)
  20.317 +
  20.318 +      val f_def_inst = fold (fn arg => fn thm => combination thm (reflexive (cterm_of thy arg))) args (Thm.freezeT f_def) (* FIXME *)
  20.319 +                            |> beta_reduce
  20.320 +    in
  20.321 +      reflexive (cterm_of thy (lambda x (SumTools.mk_proj streeR pthR x)))  (*  PR(x) == PR(x) *)
  20.322 +                |> (fn it => combination it (simp RS eq_reflection))
  20.323 +	        |> beta_norm_eq (*  PR(S(I(as))) == PR(IR(...)) *)
  20.324 +                |> transitive f_def_inst (*  f ... == PR(IR(...)) *)
  20.325 +                |> simplify (HOL_basic_ss addsimps [SumTools.projl_inl, SumTools.projr_inr]) (*  f ... == ... *)
  20.326 +                |> simplify (HOL_basic_ss addsimps all_f_defs) (*  f ... == ... *)
  20.327 +                |> (fn it => it RS meta_eq_to_obj_eq)
  20.328 +                |> restore_cond
  20.329 +                |> export
  20.330 +    end 
  20.331  
  20.332  
  20.333 -fun mutual_induct_Pnames n = 
  20.334 -    if n < 5 then fst (chop n ["P","Q","R","S"])
  20.335 -    else map (fn i => "P" ^ string_of_int i) (1 upto n)
  20.336 -	 
  20.337 -	 
  20.338 -val sum_case_rules = thms "Datatype.sum.cases"
  20.339 -val split_apply = thm "Product_Type.split"
  20.340 +(* FIXME HACK *)
  20.341 +fun mk_applied_form ctxt caTs thm = 
  20.342 +    let
  20.343 +      val thy = ProofContext.theory_of ctxt
  20.344 +      val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
  20.345 +    in
  20.346 +      fold (fn x => fn thm => combination thm (reflexive x)) xs thm
  20.347 +           |> beta_reduce
  20.348 +           |> fold_rev forall_intr xs
  20.349 +           |> forall_elim_vars 0
  20.350 +    end
  20.351 +
  20.352  		     
  20.353 -		     
  20.354 -fun mutual_induct_rules thy induct all_f_defs (Mutual {qglrss, RST, parts, streeA, ...}) =
  20.355 +fun mutual_induct_rules thy induct all_f_defs (Mutual {RST, parts, streeA, ...}) =
  20.356      let
  20.357  	fun mk_P (MutualPart {cargTs, ...}) Pname =
  20.358  	    let
  20.359 @@ -210,29 +306,53 @@
  20.360  	    end
  20.361  
  20.362      in
  20.363 -	map (mk_proj induct_inst) parts
  20.364 +      map (mk_proj induct_inst) parts
  20.365      end
  20.366 -    
  20.367 +
  20.368      
  20.369  
  20.370  
  20.371  
  20.372 -fun mk_partial_rules_mutual thy (m as Mutual {qglrss, RST, parts, streeR, ...}) data result =
  20.373 +fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result =
  20.374      let
  20.375 -	val result = FundefProof.mk_partial_rules thy data result
  20.376 -	val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
  20.377 -
  20.378 -	val sum_psimps = Library.unflat qglrss psimps
  20.379 +      val thy = ProofContext.theory_of lthy
  20.380 +                
  20.381 +      val result = FundefProof.mk_partial_rules thy data prep_result
  20.382 +      val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
  20.383 +                                                                                                               
  20.384 +      val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} => 
  20.385 +                               mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def))) 
  20.386 +                           parts
  20.387 +                           |> print
  20.388 +                          
  20.389 +      fun mk_mpsimp fqgar sum_psimp = 
  20.390 +          in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
  20.391 +          
  20.392 +      val mpsimps = map2 mk_mpsimp fqgars psimps
  20.393 +                    
  20.394 +      val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
  20.395 +      val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro
  20.396 +    in
  20.397 +      FundefMResult { f=f, G=G, R=R,
  20.398 +		      psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
  20.399 +		      cases=completeness, termination=termination, domintros=dom_intros }
  20.400 +    end
  20.401  
  20.402 -	val all_f_defs = map (fn MutualPart {f_def, ...} => symmetric f_def) parts
  20.403 -	val mpsimps = map_mutual2 (recover_mutual_psimp thy RST streeR all_f_defs) m sum_psimps
  20.404 -	val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
  20.405 -        val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro
  20.406 -    in
  20.407 -	FundefMResult { f=f, G=G, R=R,
  20.408 -			psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
  20.409 -			cases=completeness, termination=termination, domintros=dom_intros}
  20.410 -    end
  20.411 +
  20.412 +
  20.413 +(* puts an object in the "right bucket" *) 
  20.414 +fun store_grouped P x [] = []
  20.415 +  | store_grouped P x ((l, xs)::bs) = 
  20.416 +    if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs)
  20.417 +
  20.418 +fun sort_by_function (Mutual {fqgars, ...}) names xs =
  20.419 +      fold_rev (store_grouped (eq_str o apfst fst))  (* fill *)
  20.420 +               (map name_of_fqgar fqgars ~~ xs)      (* the name-thm pairs *)
  20.421 +               (map (rpair []) names)                (* in the empty buckets labeled with names *)
  20.422 +
  20.423 +         |> map (snd #> map snd)                     (* and remove the labels afterwards *)
  20.424 +
  20.425 +
  20.426      
  20.427  
  20.428  end
    21.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Wed Sep 13 00:38:38 2006 +0200
    21.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Wed Sep 13 12:05:50 2006 +0200
    21.3 @@ -12,8 +12,10 @@
    21.4  signature FUNDEF_SPLIT =
    21.5  sig
    21.6    val split_some_equations :
    21.7 -    Proof.context -> (('a * ('b * bool)) * term) list -> (('a * 'b) * term list) list
    21.8 +    Proof.context -> (bool * term) list -> term list list
    21.9  
   21.10 +  val split_all_equations :
   21.11 +    Proof.context -> term list -> term list list
   21.12  end
   21.13  
   21.14  structure FundefSplit : FUNDEF_SPLIT =
   21.15 @@ -51,7 +53,7 @@
   21.16              val (vs', t) = saturate ctx vs constr
   21.17              val substs = pattern_subtract_subst ctx vs' t t'
   21.18            in
   21.19 -            map (cons (v, t)) substs
   21.20 +            map (fn (vs, subst) => (vs, (v,t)::subst)) substs
   21.21            end
   21.22      in
   21.23        flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T))
   21.24 @@ -63,24 +65,29 @@
   21.25      in
   21.26        if C = C'
   21.27        then flat (map2 (pattern_subtract_subst ctx vs) ps qs)
   21.28 -      else [[]]
   21.29 +      else [(vs, [])]
   21.30      end
   21.31  
   21.32 -fun pattern_subtract_parallel ctx vs ps qs =
   21.33 -    flat (map2 (pattern_subtract_subst ctx vs) ps qs)
   21.34 -
   21.35 -
   21.36  
   21.37 -(* ps - qs *)
   21.38 +(* p - q *)
   21.39  fun pattern_subtract ctx eq2 eq1 =
   21.40      let
   21.41 -      val _ $ (_ $ lhs1 $ _) = eq1
   21.42 -      val _ $ (_ $ lhs2 $ _) = eq2
   21.43 +      
   21.44 +      val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
   21.45 +      val (_,  _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
   21.46  
   21.47        val thy = ProofContext.theory_of ctx
   21.48 -      val vs = term_frees eq1
   21.49 +
   21.50 +      val substs = pattern_subtract_subst ctx vs lhs1 lhs2
   21.51 +
   21.52 +      fun instantiate (vs', sigma) =
   21.53 +          let
   21.54 +            val t = Pattern.rewrite_term thy sigma [] feq1
   21.55 +          in
   21.56 +            fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
   21.57 +          end
   21.58      in
   21.59 -      map (fn sigma => Pattern.rewrite_term thy sigma [] eq1) (pattern_subtract_subst ctx vs lhs1 lhs2)
   21.60 +      map instantiate substs
   21.61      end
   21.62  
   21.63  
   21.64 @@ -94,24 +101,21 @@
   21.65  
   21.66  
   21.67  
   21.68 -fun split_all_equations ctx eqns =
   21.69 -    let
   21.70 -      fun split_aux prev [] = []
   21.71 -        | split_aux prev (e::es) = pattern_subtract_many ctx prev [e] @ split_aux (e::prev) es
   21.72 -    in
   21.73 -      split_aux [] eqns
   21.74 -end
   21.75 -
   21.76 -
   21.77  fun split_some_equations ctx eqns =
   21.78      let
   21.79        fun split_aux prev [] = []
   21.80 -        | split_aux prev (((n, (att, true)), eq) :: es) = ((n, att), pattern_subtract_many ctx prev [eq])
   21.81 -                                                          :: split_aux (eq :: prev) es
   21.82 -        | split_aux prev (((n, (att, false)), eq) :: es) = ((n, att), [eq])
   21.83 -                                                                :: split_aux (eq :: prev) es
   21.84 +        | split_aux prev ((true, eq) :: es) = pattern_subtract_many ctx prev [eq]
   21.85 +                                              :: split_aux (eq :: prev) es
   21.86 +        | split_aux prev ((false, eq) :: es) = [eq]
   21.87 +                                               :: split_aux (eq :: prev) es
   21.88      in
   21.89        split_aux [] eqns
   21.90      end
   21.91  
   21.92 +fun split_all_equations ctx =
   21.93 +    split_some_equations ctx o map (pair true)
   21.94 +
   21.95 +
   21.96 +
   21.97 +
   21.98  end
    22.1 --- a/src/HOL/Tools/function_package/sum_tools.ML	Wed Sep 13 00:38:38 2006 +0200
    22.2 +++ b/src/HOL/Tools/function_package/sum_tools.ML	Wed Sep 13 12:05:50 2006 +0200
    22.3 @@ -17,6 +17,7 @@
    22.4    val projr_inr: thm
    22.5  
    22.6    val mk_tree : typ list -> typ * sum_tree * sum_path list
    22.7 +  val mk_tree_distinct : typ list -> typ * sum_tree * sum_path list
    22.8  
    22.9    val mk_proj: sum_tree -> sum_path -> term -> term
   22.10    val mk_inj: sum_tree -> sum_path -> term -> term
   22.11 @@ -37,12 +38,9 @@
   22.12  val projl_inl = thm "FunDef.lproj_inl"
   22.13  val projr_inr = thm "FunDef.rproj_inr"
   22.14  
   22.15 -
   22.16 -
   22.17  fun mk_sumT LT RT = Type ("+", [LT, RT])
   22.18  fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
   22.19  
   22.20 -
   22.21  datatype sum_tree 
   22.22    = Leaf of typ
   22.23    | Branch of (typ * (typ * sum_tree) * (typ * sum_tree))
   22.24 @@ -72,6 +70,23 @@
   22.25      end
   22.26  
   22.27  
   22.28 +fun mk_tree_distinct Ts =
   22.29 +    let
   22.30 +      fun insert_once T Ts =
   22.31 +          let
   22.32 +            val i = find_index_eq T Ts
   22.33 +          in
   22.34 +            if i = ~1 then (length Ts, Ts @ [T]) else (i, Ts)
   22.35 +          end
   22.36 +
   22.37 +      val (idxs, dist_Ts) = fold_map insert_once Ts []
   22.38 +
   22.39 +      val (ST, tree, pths) = mk_tree dist_Ts
   22.40 +    in
   22.41 +      (ST, tree, map (nth pths) idxs)
   22.42 +    end
   22.43 +
   22.44 +
   22.45  fun mk_inj (Leaf _) [] t = t
   22.46    | mk_inj (Branch (ST, (LT, tr), _)) (true::pth) t = 
   22.47      Const (inlN, LT --> ST) $ mk_inj tr pth t
    23.1 --- a/src/HOL/Tools/function_package/termination.ML	Wed Sep 13 00:38:38 2006 +0200
    23.2 +++ b/src/HOL/Tools/function_package/termination.ML	Wed Sep 13 12:05:50 2006 +0200
    23.3 @@ -25,7 +25,7 @@
    23.4  	val domT = domain_type (fastype_of f)
    23.5  	val x = Free ("x", domT)
    23.6      in
    23.7 -	Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
    23.8 +      Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
    23.9      end
   23.10  
   23.11  fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
    24.1 --- a/src/HOL/W0/W0.thy	Wed Sep 13 00:38:38 2006 +0200
    24.2 +++ b/src/HOL/W0/W0.thy	Wed Sep 13 12:05:50 2006 +0200
    24.3 @@ -57,7 +57,7 @@
    24.4  
    24.5  instance "typ" :: type_struct ..
    24.6  instance list :: (type_struct) type_struct ..
    24.7 -instance fun :: (type, type_struct) type_struct ..
    24.8 +instance "fun" :: (type, type_struct) type_struct ..
    24.9  
   24.10  
   24.11  subsection {* Substitutions *}
    25.1 --- a/src/HOL/ex/CodeCollections.thy	Wed Sep 13 00:38:38 2006 +0200
    25.2 +++ b/src/HOL/ex/CodeCollections.thy	Wed Sep 13 12:05:50 2006 +0200
    25.3 @@ -5,7 +5,7 @@
    25.4  header {* Collection classes as examples for code generation *}
    25.5  
    25.6  theory CodeCollections
    25.7 -imports CodeOperationalEquality
    25.8 +imports "../FundefDebug" CodeOperationalEquality
    25.9  begin
   25.10  
   25.11  section {* Collection classes as examples for code generation *}
   25.12 @@ -66,16 +66,16 @@
   25.13    max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a"
   25.14    "max x y = (if x <<= y then y else x)"
   25.15  
   25.16 -consts
   25.17 -  abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
   25.18 -
   25.19 -function
   25.20 +fun abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
   25.21 +where
   25.22    "abs_sorted cmp [] = True"
   25.23 -  "abs_sorted cmp [x] = True"
   25.24 -  "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))"
   25.25 -by pat_completeness simp_all
   25.26 +| "abs_sorted cmp [x] = True"
   25.27 +| "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))"
   25.28 +
   25.29  termination by (auto_term "measure (length o snd)")
   25.30  
   25.31 +thm abs_sorted.simps
   25.32 +
   25.33  abbreviation (in ordered)
   25.34    "sorted \<equiv> abs_sorted le"
   25.35  
   25.36 @@ -90,7 +90,8 @@
   25.37  next
   25.38    case (Cons x' xs)
   25.39    from this(5) have "sorted (x # x' # xs)" .
   25.40 -  then show "sorted (x' # xs)" by auto
   25.41 +  then show "sorted (x' # xs)"
   25.42 +    by auto
   25.43  qed
   25.44  
   25.45  instance bool :: ordered
   25.46 @@ -109,14 +110,13 @@
   25.47    "u <<= v == True"
   25.48    by default (simp_all add:  ordered_unit_def)
   25.49  
   25.50 -consts
   25.51 -  le_option' :: "'a::ordered option \<Rightarrow> 'a option \<Rightarrow> bool"
   25.52  
   25.53 -function
   25.54 +fun le_option' :: "'a::ordered option \<Rightarrow> 'a option \<Rightarrow> bool"
   25.55 +where
   25.56    "le_option' None y = True"
   25.57 -  "le_option' (Some x) None = False"
   25.58 -  "le_option' (Some x) (Some y) = x <<= y"
   25.59 -  by pat_completeness simp_all
   25.60 +| "le_option' (Some x) None = False"
   25.61 +| "le_option' (Some x) (Some y) = x <<= y"
   25.62 +
   25.63  termination by (auto_term "{}")
   25.64  
   25.65  instance (ordered) option :: ordered
   25.66 @@ -144,12 +144,9 @@
   25.67    "Some v <<= Some w = v <<= w"
   25.68    unfolding ordered_option_def le_option'.simps by rule+
   25.69  
   25.70 -consts
   25.71 -  le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   25.72 -
   25.73 -function
   25.74 +fun le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   25.75 +where
   25.76    "le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
   25.77 -  by pat_completeness simp_all
   25.78  termination by (auto_term "{}")
   25.79  
   25.80  instance (ordered, ordered) * :: ordered
   25.81 @@ -164,14 +161,14 @@
   25.82    "(x1, y1) <<= (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
   25.83    unfolding "ordered_*_def" le_pair'.simps ..
   25.84  
   25.85 -(* consts
   25.86 -  le_list' :: "'a::ordered list \<Rightarrow> 'a list \<Rightarrow> bool"
   25.87 +(*   
   25.88  
   25.89 -function
   25.90 +fun le_list' :: "'a::ordered list \<Rightarrow> 'a list \<Rightarrow> bool"
   25.91 +where
   25.92    "le_list' [] ys = True"
   25.93 -  "le_list' (x#xs) [] = False"
   25.94 -  "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> le_list' xs ys)"
   25.95 -    by pat_completeness simp_all
   25.96 +| "le_list' (x#xs) [] = False"
   25.97 +| "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> le_list' xs ys)"
   25.98 +
   25.99  termination by (auto_term "measure (length o fst)")
  25.100  
  25.101  instance (ordered) list :: ordered
  25.102 @@ -213,14 +210,13 @@
  25.103    shows no_smaller: "a = inf"
  25.104  using prem inf by (rule order_antisym)
  25.105  
  25.106 -consts
  25.107 -  abs_max_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a"
  25.108  
  25.109  ML {* set quick_and_dirty *}
  25.110 -function
  25.111 +function abs_max_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a"
  25.112 +where
  25.113    "abs_max_of cmp inff [] = inff"
  25.114 -  "abs_max_of cmp inff [x] = x"
  25.115 -  "abs_max_of cmp inff (x#xs) =
  25.116 +| "abs_max_of cmp inff [x] = x"
  25.117 +| "abs_max_of cmp inff (x#xs) =
  25.118       ordered.max cmp x (abs_max_of cmp inff xs)"
  25.119  apply pat_completeness sorry
  25.120  
    26.1 --- a/src/HOL/ex/CodeOperationalEquality.thy	Wed Sep 13 00:38:38 2006 +0200
    26.2 +++ b/src/HOL/ex/CodeOperationalEquality.thy	Wed Sep 13 12:05:50 2006 +0200
    26.3 @@ -113,7 +113,7 @@
    26.4  
    26.5  instance int :: eq ..
    26.6  
    26.7 -lemma [code fun]:
    26.8 +lemma [code func]:
    26.9    "eq k l = eq_integer k l"
   26.10  unfolding eq_integer_def eq_def ..
   26.11  
    27.1 --- a/src/HOL/ex/Fundefs.thy	Wed Sep 13 00:38:38 2006 +0200
    27.2 +++ b/src/HOL/ex/Fundefs.thy	Wed Sep 13 12:05:50 2006 +0200
    27.3 @@ -6,26 +6,31 @@
    27.4  *)
    27.5  
    27.6  theory Fundefs 
    27.7 -imports Main
    27.8 +imports Main "../FundefDebug"
    27.9  begin
   27.10  
   27.11 +
   27.12  section {* Very basic *}
   27.13  
   27.14 -consts fib :: "nat \<Rightarrow> nat"
   27.15 -function
   27.16 +ML "trace_simp := false"
   27.17 +
   27.18 +fun fib :: "nat \<Rightarrow> nat"
   27.19 +where
   27.20    "fib 0 = 1"
   27.21 -  "fib (Suc 0) = 1"
   27.22 -  "fib (Suc (Suc n)) = fib n + fib (Suc n)"
   27.23 -by pat_completeness  -- {* shows that the patterns are complete *}
   27.24 -  auto  -- {* shows that the patterns are compatible *}
   27.25 +| "fib (Suc 0) = 1"
   27.26 +| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
   27.27 +
   27.28  
   27.29  text {* we get partial simp and induction rules: *}
   27.30  thm fib.psimps
   27.31 -thm pinduct
   27.32 +thm fib.pinduct
   27.33  
   27.34  text {* There is also a cases rule to distinguish cases along the definition *}
   27.35  thm fib.cases
   27.36  
   27.37 +thm fib.domintros
   27.38 +
   27.39 +
   27.40  text {* Now termination: *}
   27.41  termination fib
   27.42    by (auto_term "less_than")
   27.43 @@ -36,34 +41,30 @@
   27.44  
   27.45  section {* Currying *}
   27.46  
   27.47 -consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   27.48 -function
   27.49 +fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   27.50 +where
   27.51    "add 0 y = y"
   27.52 -  "add (Suc x) y = Suc (add x y)"
   27.53 -thm add_rel.cases
   27.54 -
   27.55 -by pat_completeness auto
   27.56 +| "add (Suc x) y = Suc (add x y)"
   27.57  termination
   27.58    by (auto_term "measure fst")
   27.59  
   27.60 +thm add.simps
   27.61  thm add.induct -- {* Note the curried induction predicate *}
   27.62  
   27.63  
   27.64  section {* Nested recursion *}
   27.65  
   27.66 -consts nz :: "nat \<Rightarrow> nat"
   27.67 -function
   27.68 +fun nz :: "nat \<Rightarrow> nat"
   27.69 +where
   27.70    "nz 0 = 0"
   27.71 -  "nz (Suc x) = nz (nz x)"
   27.72 -by pat_completeness auto
   27.73 +| "nz (Suc x) = nz (nz x)"
   27.74 +
   27.75  
   27.76  lemma nz_is_zero: -- {* A lemma we need to prove termination *}
   27.77    assumes trm: "x \<in> nz_dom"
   27.78    shows "nz x = 0"
   27.79  using trm
   27.80 -apply induct 
   27.81 -apply auto
   27.82 -done
   27.83 +by induct auto
   27.84  
   27.85  termination nz
   27.86    apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
   27.87 @@ -74,10 +75,10 @@
   27.88  
   27.89  text {* Here comes McCarthy's 91-function *}
   27.90  
   27.91 -consts f91 :: "nat => nat"
   27.92 -function 
   27.93 +fun f91 :: "nat => nat"
   27.94 +where
   27.95    "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
   27.96 -by pat_completeness auto
   27.97 +
   27.98  
   27.99  (* Prove a lemma before attempting a termination proof *)
  27.100  lemma f91_estimate: 
  27.101 @@ -85,7 +86,6 @@
  27.102    shows "n < f91 n + 11"
  27.103  using trm by induct auto
  27.104  
  27.105 -(* Now go for termination *)
  27.106  termination
  27.107  proof
  27.108    let ?R = "measure (%x. 101 - x)"
  27.109 @@ -109,15 +109,16 @@
  27.110  no automatic splitting takes place. But the following definition of
  27.111  gcd is ok, although patterns overlap: *}
  27.112  
  27.113 -consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  27.114 -function
  27.115 +fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  27.116 +where
  27.117    "gcd2 x 0 = x"
  27.118 -  "gcd2 0 y = y"
  27.119 -  "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
  27.120 -                                else gcd2 (x - y) (Suc y))"
  27.121 -by pat_completeness auto
  27.122 +| "gcd2 0 y = y"
  27.123 +| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
  27.124 +                                    else gcd2 (x - y) (Suc y))"
  27.125 +
  27.126 +
  27.127  termination 
  27.128 -  by (auto_term "measure (\<lambda>(x,y). x + y)")
  27.129 +  by (auto_term "(measure (%x. x)) <*lex*> (measure (%x. x))")
  27.130  
  27.131  thm gcd2.simps
  27.132  thm gcd2.induct
  27.133 @@ -127,8 +128,8 @@
  27.134  
  27.135  text {* We can reformulate the above example using guarded patterns *}
  27.136  
  27.137 -consts gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  27.138 -function
  27.139 +function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
  27.140 +where
  27.141    "gcd3 x 0 = x"
  27.142    "gcd3 0 y = y"
  27.143    "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
  27.144 @@ -136,6 +137,7 @@
  27.145    apply (case_tac x, case_tac a, auto)
  27.146    apply (case_tac ba, auto)
  27.147    done
  27.148 +
  27.149  termination 
  27.150    by (auto_term "measure (\<lambda>(x,y). x + y)")
  27.151  
  27.152 @@ -143,10 +145,10 @@
  27.153  thm gcd3.induct
  27.154  
  27.155  
  27.156 +text {* General patterns allow even strange definitions: *}
  27.157  
  27.158 -text {* General patterns allow even strange definitions: *}
  27.159 -consts ev :: "nat \<Rightarrow> bool"
  27.160 -function
  27.161 +function ev :: "nat \<Rightarrow> bool"
  27.162 +where
  27.163    "ev (2 * n) = True"
  27.164    "ev (2 * n + 1) = False"
  27.165  proof -  -- {* completeness is more difficult here \dots *}
  27.166 @@ -166,7 +168,7 @@
  27.167      with divmod have "x = 2 * (x div 2) + 1" by simp
  27.168      with c2 show "P" .
  27.169    qed
  27.170 -qed presburger+   -- {* solve compatibility with presburger *}
  27.171 +qed presburger+ -- {* solve compatibility with presburger *}
  27.172  termination by (auto_term "{}")
  27.173  
  27.174  thm ev.simps
  27.175 @@ -176,18 +178,12 @@
  27.176  
  27.177  section {* Mutual Recursion *}
  27.178  
  27.179 -
  27.180 -consts
  27.181 -  evn :: "nat \<Rightarrow> bool"
  27.182 -  od :: "nat \<Rightarrow> bool"
  27.183 -
  27.184 -function
  27.185 +fun evn od :: "nat \<Rightarrow> bool"
  27.186 +where
  27.187    "evn 0 = True"
  27.188 -  "evn (Suc n) = od n"
  27.189 -and
  27.190 -  "od 0 = False"
  27.191 -  "od (Suc n) = evn n"
  27.192 -  by pat_completeness auto
  27.193 +| "od 0 = False"
  27.194 +| "evn (Suc n) = od n"
  27.195 +| "od (Suc n) = evn n"
  27.196  
  27.197  thm evn.psimps
  27.198  thm od.psimps
    28.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Wed Sep 13 00:38:38 2006 +0200
    28.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Wed Sep 13 12:05:50 2006 +0200
    28.3 @@ -25,7 +25,7 @@
    28.4  typedecl o
    28.5  arities
    28.6    o :: type
    28.7 -  fun :: (type, type) type
    28.8 +  "fun" :: (type, type) type
    28.9  
   28.10  
   28.11  subsubsection {* Basic logical connectives *}
    29.1 --- a/src/HOL/ex/NormalForm.thy	Wed Sep 13 00:38:38 2006 +0200
    29.2 +++ b/src/HOL/ex/NormalForm.thy	Wed Sep 13 12:05:50 2006 +0200
    29.3 @@ -9,7 +9,7 @@
    29.4  begin
    29.5  
    29.6  lemma "p \<longrightarrow> True" by normalization
    29.7 -declare disj_assoc [code fun]
    29.8 +declare disj_assoc [code func]
    29.9  normal_form  "(P | Q) | R"
   29.10  
   29.11  lemma "0 + (n::nat) = n" by normalization
    30.1 --- a/src/HOLCF/Ffun.thy	Wed Sep 13 00:38:38 2006 +0200
    30.2 +++ b/src/HOLCF/Ffun.thy	Wed Sep 13 12:05:50 2006 +0200
    30.3 @@ -15,7 +15,7 @@
    30.4  
    30.5  subsection {* Full function space is a partial order *}
    30.6  
    30.7 -instance fun  :: (type, sq_ord) sq_ord ..
    30.8 +instance "fun"  :: (type, sq_ord) sq_ord ..
    30.9  
   30.10  defs (overloaded)
   30.11    less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  
   30.12 @@ -36,7 +36,7 @@
   30.13  apply (erule spec)
   30.14  done
   30.15  
   30.16 -instance fun  :: (type, po) po
   30.17 +instance "fun"  :: (type, po) po
   30.18  by intro_classes
   30.19    (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+
   30.20  
   30.21 @@ -90,7 +90,7 @@
   30.22    "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
   30.23  by (rule exI, erule lub_fun)
   30.24  
   30.25 -instance fun  :: (type, cpo) cpo
   30.26 +instance "fun"  :: (type, cpo) cpo
   30.27  by intro_classes (rule cpo_fun)
   30.28  
   30.29  subsection {* Full function space is pointed *}
   30.30 @@ -103,7 +103,7 @@
   30.31  apply (rule minimal_fun [THEN allI])
   30.32  done
   30.33  
   30.34 -instance fun  :: (type, pcpo) pcpo
   30.35 +instance "fun"  :: (type, pcpo) pcpo
   30.36  by intro_classes (rule least_fun)
   30.37  
   30.38  text {* for compatibility with old HOLCF-Version *}
    31.1 --- a/src/Pure/Tools/codegen_theorems.ML	Wed Sep 13 00:38:38 2006 +0200
    31.2 +++ b/src/Pure/Tools/codegen_theorems.ML	Wed Sep 13 12:05:50 2006 +0200
    31.3 @@ -918,7 +918,7 @@
    31.4        (Context.map_theory o f);
    31.5  in
    31.6    val _ = map (Context.add_setup o add_simple_attribute) [
    31.7 -    ("fun", add_fun),
    31.8 +    ("func", add_fun),
    31.9      ("nofun", del_fun),
   31.10      ("unfold", (fn thm => Codegen.add_unfold thm #> add_unfold thm)),
   31.11      ("inline", add_unfold),