untabified
authorkrauss
Tue Nov 07 22:06:32 2006 +0100 (2006-11-07)
changeset 21237b803f9870e97
parent 21236 890fafbcf8b0
child 21238 c46bc715bdfd
untabified
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_common.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/lexicographic_order.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
     1.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Tue Nov 07 21:30:03 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Tue Nov 07 22:06:32 2006 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4  (*** Dependency analysis for congruence rules ***)
     1.5  
     1.6  fun branch_vars t = 
     1.7 -    let	
     1.8 +    let 
     1.9        val t' = snd (dest_all_all t)
    1.10        val assumes = Logic.strip_imp_prems t'
    1.11        val concl = Logic.strip_imp_concl t'
    1.12 @@ -64,13 +64,13 @@
    1.13  
    1.14  fun cong_deps crule =
    1.15      let
    1.16 -	val branches = map branch_vars (prems_of crule)
    1.17 -	val num_branches = (1 upto (length branches)) ~~ branches
    1.18 +  val branches = map branch_vars (prems_of crule)
    1.19 +  val num_branches = (1 upto (length branches)) ~~ branches
    1.20      in
    1.21 -	IntGraph.empty
    1.22 -	    |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
    1.23 -	    |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
    1.24 -	    (product num_branches num_branches)
    1.25 +  IntGraph.empty
    1.26 +      |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
    1.27 +      |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
    1.28 +      (product num_branches num_branches)
    1.29      end
    1.30      
    1.31  val add_congs = map (fn c => c RS eq_reflection) [cong, ext] 
    1.32 @@ -80,7 +80,7 @@
    1.33  (* Called on the INSTANTIATED branches of the congruence rule *)
    1.34  fun mk_branch ctx t = 
    1.35      let
    1.36 -	val (ctx', fixes, impl) = dest_all_all_ctx ctx t
    1.37 +  val (ctx', fixes, impl) = dest_all_all_ctx ctx t
    1.38      in
    1.39        (ctx', fixes, Logic.strip_imp_prems impl, rhs_of (Logic.strip_imp_concl impl))
    1.40      end
    1.41 @@ -96,7 +96,7 @@
    1.42         val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
    1.43         val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c [])
    1.44       in
    1.45 -	 (cterm_instantiate inst r, dep, branches)
    1.46 +   (cterm_instantiate inst r, dep, branches)
    1.47       end
    1.48      handle Pattern.MATCH => find_cong_rule ctx fvar h rs t)
    1.49    | find_cong_rule _ _ _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
    1.50 @@ -111,13 +111,13 @@
    1.51      | NONE => 
    1.52        if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t
    1.53        else 
    1.54 -	let val (r, dep, branches) = find_cong_rule ctx fvar h congs t in
    1.55 -	  Cong (t, r, dep, 
    1.56 +  let val (r, dep, branches) = find_cong_rule ctx fvar h congs t in
    1.57 +    Cong (t, r, dep, 
    1.58                  map (fn (ctx', fixes, assumes, st) => 
    1.59 -			(fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes, 
    1.60 +      (fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes, 
    1.61                           mk_tree congs fvar h ctx' st)) branches)
    1.62 -	end
    1.63 -		
    1.64 +  end
    1.65 +    
    1.66  
    1.67  fun inst_tree thy fvar f tr =
    1.68      let
    1.69 @@ -142,7 +142,7 @@
    1.70  
    1.71  
    1.72  
    1.73 -(* FIXME: remove *)		
    1.74 +(* FIXME: remove *)   
    1.75  fun add_context_varnames (Leaf _) = I
    1.76    | add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (insert (op =) o fst) fs o add_context_varnames st) sub
    1.77    | add_context_varnames (RCall (_,st)) = add_context_varnames st
    1.78 @@ -164,30 +164,30 @@
    1.79  
    1.80  fun assume_in_ctxt thy (fixes, athms) prop =
    1.81      let
    1.82 -	val global_assum = export_term (fixes, map prop_of athms) prop
    1.83 +  val global_assum = export_term (fixes, map prop_of athms) prop
    1.84      in
    1.85 -	(global_assum,
    1.86 -	 assume (cterm_of thy global_assum) |> import_thm thy (fixes, athms))
    1.87 +  (global_assum,
    1.88 +   assume (cterm_of thy global_assum) |> import_thm thy (fixes, athms))
    1.89      end
    1.90  
    1.91  
    1.92  (* folds in the order of the dependencies of a graph. *)
    1.93  fun fold_deps G f x =
    1.94      let
    1.95 -	fun fill_table i (T, x) =
    1.96 -	    case Inttab.lookup T i of
    1.97 -		SOME _ => (T, x)
    1.98 -	      | NONE => 
    1.99 -		let
   1.100 -		    val (T', x') = fold fill_table (IntGraph.imm_succs G i) (T, x)
   1.101 -		    val (v, x'') = f (the o Inttab.lookup T') i x
   1.102 -		in
   1.103 -		    (Inttab.update (i, v) T', x'')
   1.104 -		end
   1.105 +  fun fill_table i (T, x) =
   1.106 +      case Inttab.lookup T i of
   1.107 +    SOME _ => (T, x)
   1.108 +        | NONE => 
   1.109 +    let
   1.110 +        val (T', x') = fold fill_table (IntGraph.imm_succs G i) (T, x)
   1.111 +        val (v, x'') = f (the o Inttab.lookup T') i x
   1.112 +    in
   1.113 +        (Inttab.update (i, v) T', x'')
   1.114 +    end
   1.115  
   1.116 -	val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
   1.117 +  val (T, x) = fold fill_table (IntGraph.keys G) (Inttab.empty, x)
   1.118      in
   1.119 -	(Inttab.fold (cons o snd) T [], x)
   1.120 +  (Inttab.fold (cons o snd) T [], x)
   1.121      end
   1.122  
   1.123  
   1.124 @@ -195,26 +195,26 @@
   1.125  
   1.126  fun traverse_tree rcOp tr x =
   1.127      let 
   1.128 -	fun traverse_help ctx (Leaf _) u x = ([], x)
   1.129 -	  | traverse_help ctx (RCall (t, st)) u x =
   1.130 -	    rcOp ctx t u (traverse_help ctx st u x)
   1.131 -	  | traverse_help ctx (Cong (t, crule, deps, branches)) u x =
   1.132 -	    let
   1.133 -		fun sub_step lu i x =
   1.134 -		    let
   1.135 -			val (fixes, assumes, subtree) = nth branches (i - 1)
   1.136 -			val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
   1.137 -			val (subs, x') = traverse_help (compose ctx (fixes, assumes)) subtree used x
   1.138 -			val exported_subs = map (apfst (compose (fixes, assumes))) subs
   1.139 -		    in
   1.140 -			(exported_subs, x')
   1.141 -		    end
   1.142 -	    in
   1.143 -		fold_deps deps sub_step x
   1.144 -			  |> apfst flatten
   1.145 -	    end
   1.146 +  fun traverse_help ctx (Leaf _) u x = ([], x)
   1.147 +    | traverse_help ctx (RCall (t, st)) u x =
   1.148 +      rcOp ctx t u (traverse_help ctx st u x)
   1.149 +    | traverse_help ctx (Cong (t, crule, deps, branches)) u x =
   1.150 +      let
   1.151 +    fun sub_step lu i x =
   1.152 +        let
   1.153 +      val (fixes, assumes, subtree) = nth branches (i - 1)
   1.154 +      val used = fold_rev (append o lu) (IntGraph.imm_succs deps i) u
   1.155 +      val (subs, x') = traverse_help (compose ctx (fixes, assumes)) subtree used x
   1.156 +      val exported_subs = map (apfst (compose (fixes, assumes))) subs
   1.157 +        in
   1.158 +      (exported_subs, x')
   1.159 +        end
   1.160 +      in
   1.161 +    fold_deps deps sub_step x
   1.162 +        |> apfst flatten
   1.163 +      end
   1.164      in
   1.165 -	snd (traverse_help ([], []) tr [] x)
   1.166 +  snd (traverse_help ([], []) tr [] x)
   1.167      end
   1.168  
   1.169  
   1.170 @@ -222,48 +222,47 @@
   1.171  
   1.172  fun rewrite_by_tree thy h ih x tr =
   1.173      let
   1.174 -	fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
   1.175 -	  | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
   1.176 -	    let
   1.177 -		val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st
   1.178 -					   
   1.179 -					   (* Need not use the simplifier here. Can use primitive steps! *)
   1.180 -		val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
   1.181 -			     
   1.182 -		val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
   1.183 -		val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
   1.184 -				     |> rew_ha
   1.185 -
   1.186 -		val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
   1.187 -		val eq = implies_elim (implies_elim inst_ih lRi) iha
   1.188 -			 
   1.189 -		val h_a'_eq_f_a' = eq RS eq_reflection
   1.190 -		val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
   1.191 -	    in
   1.192 -		(result, x')
   1.193 -	    end
   1.194 -	  | rewrite_help fix f_as h_as x (Cong (t, crule, deps, branches)) =
   1.195 -	    let
   1.196 -		fun sub_step lu i x =
   1.197 -		    let
   1.198 -			val (fixes, assumes, st) = nth branches (i - 1)
   1.199 -			val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
   1.200 -			val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
   1.201 -			val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
   1.202 -
   1.203 -			val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
   1.204 -			val subeq_exp = export_thm thy (fixes, map prop_of assumes) (subeq RS meta_eq_to_obj_eq)
   1.205 -		    in
   1.206 -			(subeq_exp, x')
   1.207 -		    end
   1.208 -		    
   1.209 -		val (subthms, x') = fold_deps deps sub_step x
   1.210 -	    in
   1.211 -		(fold_rev (curry op COMP) subthms crule, x')
   1.212 -	    end
   1.213 -	    
   1.214 +      fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
   1.215 +        | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
   1.216 +          let
   1.217 +            val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st
   1.218 +                                                     
   1.219 +             (* Need not use the simplifier here. Can use primitive steps! *)
   1.220 +            val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
   1.221 +           
   1.222 +            val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
   1.223 +            val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
   1.224 +                                 |> rew_ha
   1.225 +                      
   1.226 +            val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
   1.227 +            val eq = implies_elim (implies_elim inst_ih lRi) iha
   1.228 +                     
   1.229 +            val h_a'_eq_f_a' = eq RS eq_reflection
   1.230 +            val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
   1.231 +          in
   1.232 +            (result, x')
   1.233 +          end
   1.234 +        | rewrite_help fix f_as h_as x (Cong (t, crule, deps, branches)) =
   1.235 +          let
   1.236 +            fun sub_step lu i x =
   1.237 +                let
   1.238 +                  val (fixes, assumes, st) = nth branches (i - 1)
   1.239 +                  val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
   1.240 +                  val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
   1.241 +                  val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
   1.242 +                                 
   1.243 +                  val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
   1.244 +                  val subeq_exp = export_thm thy (fixes, map prop_of assumes) (subeq RS meta_eq_to_obj_eq)
   1.245 +                in
   1.246 +                  (subeq_exp, x')
   1.247 +                end
   1.248 +                
   1.249 +            val (subthms, x') = fold_deps deps sub_step x
   1.250 +          in
   1.251 +            (fold_rev (curry op COMP) subthms crule, x')
   1.252 +          end
   1.253      in
   1.254 -	rewrite_help [] [] [] x tr
   1.255 +      rewrite_help [] [] [] x tr
   1.256      end
   1.257 -
   1.258 +    
   1.259  end
     2.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Nov 07 21:30:03 2006 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Nov 07 22:06:32 2006 +0100
     2.3 @@ -97,35 +97,35 @@
     2.4  
     2.5  datatype mutual_part =
     2.6    MutualPart of 
     2.7 -	 {
     2.8 -          fvar : string * typ,
     2.9 -	  cargTs: typ list,
    2.10 -	  pthA: SumTools.sum_path,
    2.11 -	  pthR: SumTools.sum_path,
    2.12 -	  f_def: term,
    2.13 +   {
    2.14 +    fvar : string * typ,
    2.15 +    cargTs: typ list,
    2.16 +    pthA: SumTools.sum_path,
    2.17 +    pthR: SumTools.sum_path,
    2.18 +    f_def: term,
    2.19  
    2.20 -	  f: term option,
    2.21 -          f_defthm : thm option
    2.22 -	 }
    2.23 -	 
    2.24 +    f: term option,
    2.25 +    f_defthm : thm option
    2.26 +   }
    2.27 +   
    2.28  
    2.29  datatype mutual_info =
    2.30    Mutual of 
    2.31 -	 { 
    2.32 -	  defname: string,
    2.33 -          fsum_var : string * typ,
    2.34 +   { 
    2.35 +    defname: string,
    2.36 +    fsum_var : string * typ,
    2.37  
    2.38 -	  ST: typ,
    2.39 -	  RST: typ,
    2.40 -	  streeA: SumTools.sum_tree,
    2.41 -	  streeR: SumTools.sum_tree,
    2.42 +    ST: typ,
    2.43 +    RST: typ,
    2.44 +    streeA: SumTools.sum_tree,
    2.45 +    streeR: SumTools.sum_tree,
    2.46  
    2.47 -	  parts: mutual_part list,
    2.48 -	  fqgars: qgar list,
    2.49 -	  qglrs: ((string * typ) list * term list * term * term) list,
    2.50 +    parts: mutual_part list,
    2.51 +    fqgars: qgar list,
    2.52 +    qglrs: ((string * typ) list * term list * term * term) list,
    2.53  
    2.54 -          fsum : term option
    2.55 -	 }
    2.56 +    fsum : term option
    2.57 +   }
    2.58  
    2.59  
    2.60  datatype prep_result =
    2.61 @@ -299,12 +299,12 @@
    2.62  (* with explicit types: Needed with loose bounds *)
    2.63  fun mk_relmemT xT yT (x,y) R = 
    2.64      let 
    2.65 -	val pT = HOLogic.mk_prodT (xT, yT)
    2.66 -	val RT = HOLogic.mk_setT pT
    2.67 +  val pT = HOLogic.mk_prodT (xT, yT)
    2.68 +  val RT = HOLogic.mk_setT pT
    2.69      in
    2.70 -	Const ("op :", [pT, RT] ---> boolT)
    2.71 -	      $ (HOLogic.pair_const xT yT $ x $ y)
    2.72 -	      $ R
    2.73 +  Const ("op :", [pT, RT] ---> boolT)
    2.74 +        $ (HOLogic.pair_const xT yT $ x $ y)
    2.75 +        $ R
    2.76      end
    2.77  
    2.78  fun free_to_var (Free (v,T)) = Var ((v,0),T)
     3.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Tue Nov 07 21:30:03 2006 +0100
     3.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Tue Nov 07 22:06:32 2006 +0100
     3.3 @@ -17,18 +17,18 @@
     3.4  (* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
     3.5  fun tupled_lambda vars t =
     3.6      case vars of
     3.7 -	    (Free v) => lambda (Free v) t
     3.8 +      (Free v) => lambda (Free v) t
     3.9      | (Var v) => lambda (Var v) t
    3.10      | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
    3.11 -	    (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
    3.12 +      (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
    3.13      | _ => raise Match
    3.14                   
    3.15                   
    3.16  fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
    3.17      let
    3.18 -	    val (n, body) = Term.dest_abs a
    3.19 +      val (n, body) = Term.dest_abs a
    3.20      in
    3.21 -	    (Free (n, T), body)
    3.22 +      (Free (n, T), body)
    3.23      end
    3.24    | dest_all _ = raise Match
    3.25                           
    3.26 @@ -36,10 +36,10 @@
    3.27  (* Removes all quantifiers from a term, replacing bound variables by frees. *)
    3.28  fun dest_all_all (t as (Const ("all",_) $ _)) = 
    3.29      let
    3.30 -	val (v,b) = dest_all t
    3.31 -	val (vs, b') = dest_all_all b
    3.32 +  val (v,b) = dest_all t
    3.33 +  val (vs, b') = dest_all_all b
    3.34      in
    3.35 -	(v :: vs, b')
    3.36 +  (v :: vs, b')
    3.37      end
    3.38    | dest_all_all t = ([],t)
    3.39  
    3.40 @@ -54,7 +54,7 @@
    3.41  
    3.42        val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
    3.43      in
    3.44 -	(ctx'', (n', T) :: vs, bd)
    3.45 +      (ctx'', (n', T) :: vs, bd)
    3.46      end
    3.47    | dest_all_all_ctx ctx t = 
    3.48      (ctx, [], t)
     4.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 21:30:03 2006 +0100
     4.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 22:06:32 2006 +0100
     4.3 @@ -146,7 +146,7 @@
     4.4      in
     4.5        lthy
     4.6          |> ProofContext.note_thmss_i [(("termination",
     4.7 -                                 [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
     4.8 +                                        [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
     4.9          |> Proof.theorem_i PureThy.internalK NONE
    4.10                             (total_termination_afterqed name data) NONE ("", [])
    4.11                             [(("", []), [(goal, [])])]
     5.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Tue Nov 07 21:30:03 2006 +0100
     5.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Nov 07 22:06:32 2006 +0100
     5.3 @@ -465,8 +465,7 @@
     5.4  
     5.5  fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
     5.6      let
     5.7 -      fun inst_term t = 
     5.8 -          subst_bound(f, abstract_over (fvar, t))
     5.9 +      fun inst_term t = subst_bound(f, abstract_over (fvar, t))
    5.10      in
    5.11        (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
    5.12      end
     6.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Tue Nov 07 21:30:03 2006 +0100
     6.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Tue Nov 07 22:06:32 2006 +0100
     6.3 @@ -11,7 +11,7 @@
     6.4  sig
     6.5  
     6.6      val mk_partial_rules : theory -> FundefCommon.prep_result 
     6.7 -			   -> thm -> FundefCommon.fundef_result
     6.8 +         -> thm -> FundefCommon.fundef_result
     6.9  end
    6.10  
    6.11  
    6.12 @@ -43,128 +43,128 @@
    6.13  
    6.14  fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
    6.15      let
    6.16 -	val Globals {domT, z, ...} = globals
    6.17 +  val Globals {domT, z, ...} = globals
    6.18  
    6.19 -	val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
    6.20 -	val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
    6.21 -	val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
    6.22 +  val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
    6.23 +  val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
    6.24 +  val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
    6.25      in
    6.26 -	((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
    6.27 -	  |> (fn it => it COMP graph_is_function)
    6.28 -	  |> implies_intr z_smaller
    6.29 -	  |> forall_intr (cterm_of thy z)
    6.30 -	  |> (fn it => it COMP valthm)
    6.31 -	  |> implies_intr lhs_acc 
    6.32 -	  |> asm_simplify (HOL_basic_ss addsimps [f_iff])
    6.33 -          |> fold_rev (implies_intr o cprop_of) ags
    6.34 -          |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
    6.35 +      ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
    6.36 +        |> (fn it => it COMP graph_is_function)
    6.37 +        |> implies_intr z_smaller
    6.38 +        |> forall_intr (cterm_of thy z)
    6.39 +        |> (fn it => it COMP valthm)
    6.40 +        |> implies_intr lhs_acc 
    6.41 +        |> asm_simplify (HOL_basic_ss addsimps [f_iff])
    6.42 +        |> fold_rev (implies_intr o cprop_of) ags
    6.43 +        |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
    6.44      end
    6.45  
    6.46  
    6.47  
    6.48  fun mk_partial_induct_rule thy globals R complete_thm clauses =
    6.49      let
    6.50 -	val Globals {domT, x, z, a, P, D, ...} = globals
    6.51 +  val Globals {domT, x, z, a, P, D, ...} = globals
    6.52          val acc_R = mk_acc domT R
    6.53  
    6.54 -	val x_D = assume (cterm_of thy (Trueprop (D $ x)))
    6.55 -	val a_D = cterm_of thy (Trueprop (D $ a))
    6.56 +  val x_D = assume (cterm_of thy (Trueprop (D $ x)))
    6.57 +  val a_D = cterm_of thy (Trueprop (D $ a))
    6.58  
    6.59 -	val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
    6.60 +  val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
    6.61  
    6.62 -	val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
    6.63 -	    mk_forall x
    6.64 -		      (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
    6.65 -						      Logic.mk_implies (Trueprop (R $ z $ x),
    6.66 -									Trueprop (D $ z)))))
    6.67 -		      |> cterm_of thy
    6.68 +  val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
    6.69 +      mk_forall x
    6.70 +          (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
    6.71 +                  Logic.mk_implies (Trueprop (R $ z $ x),
    6.72 +                  Trueprop (D $ z)))))
    6.73 +          |> cterm_of thy
    6.74  
    6.75  
    6.76 -	(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
    6.77 -	val ihyp = all domT $ Abs ("z", domT, 
    6.78 -				   implies $ Trueprop (R $ Bound 0 $ x)
    6.79 -					   $ Trueprop (P $ Bound 0))
    6.80 -		       |> cterm_of thy
    6.81 -
    6.82 -	val aihyp = assume ihyp
    6.83 +  (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
    6.84 +  val ihyp = all domT $ Abs ("z", domT, 
    6.85 +           implies $ Trueprop (R $ Bound 0 $ x)
    6.86 +             $ Trueprop (P $ Bound 0))
    6.87 +           |> cterm_of thy
    6.88  
    6.89 -	fun prove_case clause =
    6.90 -	    let
    6.91 -		val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs, 
    6.92 -                                qglr = (oqs, _, _, _), ...} = clause
    6.93 -								       
    6.94 -		val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
    6.95 -		val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
    6.96 -		val sih = full_simplify replace_x_ss aihyp
    6.97 -					
    6.98 -                fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
    6.99 -                    sih |> forall_elim (cterm_of thy rcarg)
   6.100 -                        |> implies_elim_swp llRI
   6.101 -                        |> fold_rev (implies_intr o cprop_of) CCas
   6.102 -                        |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   6.103 +  val aihyp = assume ihyp
   6.104  
   6.105 -                val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
   6.106 -			     
   6.107 -		val step = Trueprop (P $ lhs)
   6.108 -				    |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   6.109 -				    |> fold_rev (curry Logic.mk_implies) gs
   6.110 -				    |> curry Logic.mk_implies (Trueprop (D $ lhs))
   6.111 -				    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   6.112 -				    |> cterm_of thy
   6.113 -			   
   6.114 -		val P_lhs = assume step
   6.115 -				   |> fold forall_elim cqs
   6.116 -				   |> implies_elim_swp lhs_D 
   6.117 -				   |> fold_rev implies_elim_swp ags
   6.118 -				   |> fold implies_elim_swp P_recs
   6.119 -			    
   6.120 -		val res = cterm_of thy (Trueprop (P $ x))
   6.121 -				   |> Simplifier.rewrite replace_x_ss
   6.122 -				   |> symmetric (* P lhs == P x *)
   6.123 -				   |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
   6.124 -				   |> implies_intr (cprop_of case_hyp)
   6.125 -				   |> fold_rev (implies_intr o cprop_of) ags
   6.126 -				   |> fold_rev forall_intr cqs
   6.127 -	    in
   6.128 -		(res, step)
   6.129 -	    end
   6.130 -
   6.131 -	val (cases, steps) = split_list (map prove_case clauses)
   6.132 +  fun prove_case clause =
   6.133 +      let
   6.134 +    val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs, 
   6.135 +                    qglr = (oqs, _, _, _), ...} = clause
   6.136 +                       
   6.137 +    val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
   6.138 +    val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
   6.139 +    val sih = full_simplify replace_x_ss aihyp
   6.140 +          
   6.141 +    fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
   6.142 +        sih |> forall_elim (cterm_of thy rcarg)
   6.143 +            |> implies_elim_swp llRI
   6.144 +            |> fold_rev (implies_intr o cprop_of) CCas
   6.145 +            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   6.146 +        
   6.147 +    val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
   6.148 +                 
   6.149 +    val step = Trueprop (P $ lhs)
   6.150 +            |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   6.151 +            |> fold_rev (curry Logic.mk_implies) gs
   6.152 +            |> curry Logic.mk_implies (Trueprop (D $ lhs))
   6.153 +            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   6.154 +            |> cterm_of thy
   6.155 +         
   6.156 +    val P_lhs = assume step
   6.157 +           |> fold forall_elim cqs
   6.158 +           |> implies_elim_swp lhs_D 
   6.159 +           |> fold_rev implies_elim_swp ags
   6.160 +           |> fold implies_elim_swp P_recs
   6.161 +          
   6.162 +    val res = cterm_of thy (Trueprop (P $ x))
   6.163 +           |> Simplifier.rewrite replace_x_ss
   6.164 +           |> symmetric (* P lhs == P x *)
   6.165 +           |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
   6.166 +           |> implies_intr (cprop_of case_hyp)
   6.167 +           |> fold_rev (implies_intr o cprop_of) ags
   6.168 +           |> fold_rev forall_intr cqs
   6.169 +      in
   6.170 +    (res, step)
   6.171 +      end
   6.172  
   6.173 -	val istep =  complete_thm
   6.174 -                       |> forall_elim_vars 0
   6.175 -		       |> fold (curry op COMP) cases (*  P x  *)
   6.176 -		       |> implies_intr ihyp
   6.177 -		       |> implies_intr (cprop_of x_D)
   6.178 -		       |> forall_intr (cterm_of thy x)
   6.179 -			   
   6.180 -	val subset_induct_rule = 
   6.181 -	    acc_subset_induct
   6.182 -		|> (curry op COMP) (assume D_subset)
   6.183 -		|> (curry op COMP) (assume D_dcl)
   6.184 -		|> (curry op COMP) (assume a_D)
   6.185 -		|> (curry op COMP) istep
   6.186 -		|> fold_rev implies_intr steps
   6.187 -		|> implies_intr a_D
   6.188 -		|> implies_intr D_dcl
   6.189 -		|> implies_intr D_subset
   6.190 +  val (cases, steps) = split_list (map prove_case clauses)
   6.191  
   6.192 -	val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
   6.193 +  val istep = complete_thm
   6.194 +                |> forall_elim_vars 0
   6.195 +                |> fold (curry op COMP) cases (*  P x  *)
   6.196 +                |> implies_intr ihyp
   6.197 +                |> implies_intr (cprop_of x_D)
   6.198 +                |> forall_intr (cterm_of thy x)
   6.199 +         
   6.200 +  val subset_induct_rule = 
   6.201 +      acc_subset_induct
   6.202 +        |> (curry op COMP) (assume D_subset)
   6.203 +        |> (curry op COMP) (assume D_dcl)
   6.204 +        |> (curry op COMP) (assume a_D)
   6.205 +        |> (curry op COMP) istep
   6.206 +        |> fold_rev implies_intr steps
   6.207 +        |> implies_intr a_D
   6.208 +        |> implies_intr D_dcl
   6.209 +        |> implies_intr D_subset
   6.210  
   6.211 -	val simple_induct_rule =
   6.212 -	    subset_induct_rule
   6.213 -		|> forall_intr (cterm_of thy D)
   6.214 -		|> forall_elim (cterm_of thy acc_R)
   6.215 -		|> assume_tac 1 |> Seq.hd
   6.216 -		|> (curry op COMP) (acc_downward
   6.217 -					|> (instantiate' [SOME (ctyp_of thy domT)]
   6.218 -							 (map (SOME o cterm_of thy) [R, x, z]))
   6.219 -					|> forall_intr (cterm_of thy z)
   6.220 -					|> forall_intr (cterm_of thy x))
   6.221 -		|> forall_intr (cterm_of thy a)
   6.222 -		|> forall_intr (cterm_of thy P)
   6.223 +  val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
   6.224 +
   6.225 +  val simple_induct_rule =
   6.226 +      subset_induct_rule
   6.227 +        |> forall_intr (cterm_of thy D)
   6.228 +        |> forall_elim (cterm_of thy acc_R)
   6.229 +        |> assume_tac 1 |> Seq.hd
   6.230 +        |> (curry op COMP) (acc_downward
   6.231 +                              |> (instantiate' [SOME (ctyp_of thy domT)]
   6.232 +                                               (map (SOME o cterm_of thy) [R, x, z]))
   6.233 +                              |> forall_intr (cterm_of thy z)
   6.234 +                              |> forall_intr (cterm_of thy x))
   6.235 +        |> forall_intr (cterm_of thy a)
   6.236 +        |> forall_intr (cterm_of thy P)
   6.237      in
   6.238 -	(subset_induct_all, simple_induct_rule)
   6.239 +      (subset_induct_all, simple_induct_rule)
   6.240      end
   6.241  
   6.242  
   6.243 @@ -172,19 +172,19 @@
   6.244  (* Does this work with Guards??? *)
   6.245  fun mk_domain_intro thy globals R R_cases clause =
   6.246      let
   6.247 -	val Globals {z, domT, ...} = globals
   6.248 -	val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
   6.249 -                        qglr = (oqs, _, _, _), ...} = clause
   6.250 -	val goal = Trueprop (mk_acc domT R $ lhs)
   6.251 -                     |> fold_rev (curry Logic.mk_implies) gs
   6.252 -                     |> cterm_of thy
   6.253 +      val Globals {z, domT, ...} = globals
   6.254 +      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
   6.255 +                      qglr = (oqs, _, _, _), ...} = clause
   6.256 +      val goal = Trueprop (mk_acc domT R $ lhs)
   6.257 +                          |> fold_rev (curry Logic.mk_implies) gs
   6.258 +                          |> cterm_of thy
   6.259      in
   6.260 -	Goal.init goal 
   6.261 -		  |> (SINGLE (resolve_tac [accI] 1)) |> the
   6.262 -		  |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1))  |> the
   6.263 -		  |> (SINGLE (CLASIMPSET auto_tac)) |> the
   6.264 -		  |> Goal.conclude
   6.265 -                  |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   6.266 +      Goal.init goal 
   6.267 +      |> (SINGLE (resolve_tac [accI] 1)) |> the
   6.268 +      |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1))  |> the
   6.269 +      |> (SINGLE (CLASIMPSET auto_tac)) |> the
   6.270 +      |> Goal.conclude
   6.271 +      |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   6.272      end
   6.273  
   6.274  
   6.275 @@ -192,145 +192,145 @@
   6.276  
   6.277  fun mk_nest_term_case thy globals R' ihyp clause =
   6.278      let
   6.279 -	val Globals {x, z, ...} = globals
   6.280 -	val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
   6.281 -                        qglr=(oqs, _, _, _), ...} = clause
   6.282 -
   6.283 -	val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
   6.284 -
   6.285 -	fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
   6.286 -	    let
   6.287 -		val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
   6.288 -
   6.289 -		val hyp = Trueprop (R' $ arg $ lhs)
   6.290 -				    |> fold_rev (curry Logic.mk_implies o prop_of) used
   6.291 -				    |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
   6.292 -				    |> fold_rev (curry Logic.mk_implies o prop_of) ags
   6.293 -				    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   6.294 -				    |> cterm_of thy
   6.295 -
   6.296 -		val thm = assume hyp
   6.297 -				 |> fold forall_elim cqs
   6.298 -				 |> fold implies_elim_swp ags
   6.299 -				 |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
   6.300 -				 |> fold implies_elim_swp used
   6.301 -
   6.302 -		val acc = thm COMP ih_case
   6.303 +      val Globals {x, z, ...} = globals
   6.304 +      val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
   6.305 +                      qglr=(oqs, _, _, _), ...} = clause
   6.306 +          
   6.307 +      val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
   6.308 +                    
   6.309 +      fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
   6.310 +          let
   6.311 +            val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
   6.312 +                       
   6.313 +            val hyp = Trueprop (R' $ arg $ lhs)
   6.314 +                      |> fold_rev (curry Logic.mk_implies o prop_of) used
   6.315 +                      |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
   6.316 +                      |> fold_rev (curry Logic.mk_implies o prop_of) ags
   6.317 +                      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
   6.318 +                      |> cterm_of thy
   6.319 +                      
   6.320 +            val thm = assume hyp
   6.321 +                      |> fold forall_elim cqs
   6.322 +                      |> fold implies_elim_swp ags
   6.323 +                      |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
   6.324 +                      |> fold implies_elim_swp used
   6.325 +                      
   6.326 +            val acc = thm COMP ih_case
   6.327 +                      
   6.328 +            val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
   6.329 +                           
   6.330 +            val arg_eq_z = (assume z_eq_arg) RS sym
   6.331 +                           
   6.332 +            val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
   6.333 +                        |> implies_intr (cprop_of case_hyp)
   6.334 +                        |> implies_intr z_eq_arg
   6.335  
   6.336 -		val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
   6.337 -
   6.338 -		val arg_eq_z = (assume z_eq_arg) RS sym
   6.339 -
   6.340 -		val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
   6.341 -				     |> implies_intr (cprop_of case_hyp)
   6.342 -				     |> implies_intr z_eq_arg
   6.343 -
   6.344 -                val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
   6.345 -                val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   6.346 +            val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
   6.347 +            val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   6.348 +                           
   6.349 +            val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
   6.350 +                         |> FundefCtxTree.export_thm thy (fixes, 
   6.351 +                                                          prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
   6.352 +                         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   6.353  
   6.354 -		val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
   6.355 -			       |> FundefCtxTree.export_thm thy (fixes, 
   6.356 -                                                                prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
   6.357 -                               |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   6.358 -
   6.359 -		val sub' = sub @ [(([],[]), acc)]
   6.360 -	    in
   6.361 -		(sub', (hyp :: hyps, ethm :: thms))
   6.362 -	    end
   6.363 -	  | step _ _ _ _ = raise Match
   6.364 +            val sub' = sub @ [(([],[]), acc)]
   6.365 +          in
   6.366 +            (sub', (hyp :: hyps, ethm :: thms))
   6.367 +          end
   6.368 +        | step _ _ _ _ = raise Match
   6.369      in
   6.370 -	FundefCtxTree.traverse_tree step tree
   6.371 +      FundefCtxTree.traverse_tree step tree
   6.372      end
   6.373 -
   6.374 -
   6.375 +    
   6.376 +    
   6.377  fun mk_nest_term_rule thy globals R R_cases clauses =
   6.378      let
   6.379 -	val Globals { domT, x, z, ... } = globals
   6.380 -        val acc_R = mk_acc domT R
   6.381 -
   6.382 -	val R' = Free ("R", fastype_of R)
   6.383 -
   6.384 -        val Rrel = Free ("R", mk_relT (domT, domT))
   6.385 -        val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
   6.386 -
   6.387 -	val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
   6.388 +      val Globals { domT, x, z, ... } = globals
   6.389 +      val acc_R = mk_acc domT R
   6.390 +                  
   6.391 +      val R' = Free ("R", fastype_of R)
   6.392 +               
   6.393 +      val Rrel = Free ("R", mk_relT (domT, domT))
   6.394 +      val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
   6.395 +                    
   6.396 +      val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
   6.397 +                          
   6.398 +      (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
   6.399 +      val ihyp = all domT $ Abs ("z", domT, 
   6.400 +                                 implies $ Trueprop (R' $ Bound 0 $ x)
   6.401 +                                         $ Trueprop (acc_R $ Bound 0))
   6.402 +                     |> cterm_of thy
   6.403  
   6.404 -	(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
   6.405 -	val ihyp = all domT $ Abs ("z", domT, 
   6.406 -				   implies $ Trueprop (R' $ Bound 0 $ x)
   6.407 -					   $ Trueprop (acc_R $ Bound 0))
   6.408 -		       |> cterm_of thy
   6.409 -
   6.410 -	val ihyp_a = assume ihyp |> forall_elim_vars 0
   6.411 -
   6.412 -	val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) 
   6.413 -
   6.414 -	val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
   6.415 +      val ihyp_a = assume ihyp |> forall_elim_vars 0
   6.416 +                   
   6.417 +      val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) 
   6.418 +                  
   6.419 +      val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
   6.420      in
   6.421 -	R_cases
   6.422 -            |> forall_elim (cterm_of thy z)
   6.423 -            |> forall_elim (cterm_of thy x)
   6.424 -            |> forall_elim (cterm_of thy (acc_R $ z))
   6.425 -	    |> curry op COMP (assume R_z_x)
   6.426 -	    |> fold_rev (curry op COMP) cases
   6.427 -	    |> implies_intr R_z_x
   6.428 -	    |> forall_intr (cterm_of thy z)
   6.429 -	    |> (fn it => it COMP accI)
   6.430 -	    |> implies_intr ihyp
   6.431 -	    |> forall_intr (cterm_of thy x)
   6.432 -	    |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
   6.433 -	    |> curry op RS (assume wfR')
   6.434 -	    |> fold implies_intr hyps
   6.435 -	    |> implies_intr wfR'
   6.436 -	    |> forall_intr (cterm_of thy R')
   6.437 -            |> forall_elim (cterm_of thy (inrel_R))
   6.438 -            |> curry op RS wf_in_rel
   6.439 -            |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
   6.440 -	    |> forall_intr (cterm_of thy Rrel)
   6.441 +      R_cases
   6.442 +        |> forall_elim (cterm_of thy z)
   6.443 +        |> forall_elim (cterm_of thy x)
   6.444 +        |> forall_elim (cterm_of thy (acc_R $ z))
   6.445 +        |> curry op COMP (assume R_z_x)
   6.446 +        |> fold_rev (curry op COMP) cases
   6.447 +        |> implies_intr R_z_x
   6.448 +        |> forall_intr (cterm_of thy z)
   6.449 +        |> (fn it => it COMP accI)
   6.450 +        |> implies_intr ihyp
   6.451 +        |> forall_intr (cterm_of thy x)
   6.452 +        |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
   6.453 +        |> curry op RS (assume wfR')
   6.454 +        |> fold implies_intr hyps
   6.455 +        |> implies_intr wfR'
   6.456 +        |> forall_intr (cterm_of thy R')
   6.457 +        |> forall_elim (cterm_of thy (inrel_R))
   6.458 +        |> curry op RS wf_in_rel
   6.459 +        |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
   6.460 +        |> forall_intr (cterm_of thy Rrel)
   6.461      end
   6.462 -
   6.463 +    
   6.464  
   6.465  
   6.466  
   6.467  fun mk_partial_rules thy data provedgoal =
   6.468      let
   6.469 -	val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
   6.470 -
   6.471 -        val _ = print "Closing Derivation"
   6.472 -
   6.473 -	val provedgoal = Drule.close_derivation provedgoal
   6.474 -
   6.475 -        val _ = print "Getting gif"
   6.476 -
   6.477 -        val graph_is_function = (provedgoal COMP conjunctionD1)
   6.478 -                                  |> forall_elim_vars 0
   6.479 -
   6.480 -        val _ = print "Getting cases"
   6.481 -
   6.482 -        val complete_thm = provedgoal COMP conjunctionD2
   6.483 -
   6.484 -        val _ = print "making f_iff"
   6.485 -
   6.486 -	val f_iff = (graph_is_function RS ex1_iff) 
   6.487 -
   6.488 -	val _ = Output.debug "Proving simplification rules"
   6.489 -	val psimps  = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
   6.490 -
   6.491 -	val _ = Output.debug "Proving partial induction rule"
   6.492 -	val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
   6.493 -
   6.494 -	val _ = Output.debug "Proving nested termination rule"
   6.495 -	val total_intro = mk_nest_term_rule thy globals R R_cases clauses
   6.496 -
   6.497 -	val _ = Output.debug "Proving domain introduction rules"
   6.498 -	val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
   6.499 +      val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
   6.500 +                                                                            
   6.501 +      val _ = Output.debug "Closing Derivation"
   6.502 +              
   6.503 +      val provedgoal = Drule.close_derivation provedgoal
   6.504 +                       
   6.505 +      val _ = Output.debug "Getting function theorem"
   6.506 +              
   6.507 +      val graph_is_function = (provedgoal COMP conjunctionD1)
   6.508 +                                |> forall_elim_vars 0
   6.509 +                              
   6.510 +      val _ = Output.debug "Getting cases"
   6.511 +              
   6.512 +      val complete_thm = provedgoal COMP conjunctionD2
   6.513 +                         
   6.514 +      val _ = Output.debug "Making f_iff"
   6.515 +              
   6.516 +      val f_iff = (graph_is_function RS ex1_iff) 
   6.517 +                  
   6.518 +      val _ = Output.debug "Proving simplification rules"
   6.519 +      val psimps  = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
   6.520 +                    
   6.521 +      val _ = Output.debug "Proving partial induction rule"
   6.522 +      val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
   6.523 +                                             
   6.524 +      val _ = Output.debug "Proving nested termination rule"
   6.525 +      val total_intro = mk_nest_term_rule thy globals R R_cases clauses
   6.526 +                        
   6.527 +      val _ = Output.debug "Proving domain introduction rules"
   6.528 +      val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
   6.529      in 
   6.530 -	FundefResult {f=f, G=G, R=R, completeness=complete_thm, 
   6.531 -	 psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
   6.532 -	 dom_intros=dom_intros}
   6.533 +      FundefResult {f=f, G=G, R=R, completeness=complete_thm, 
   6.534 +                    psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
   6.535 +                    dom_intros=dom_intros}
   6.536      end
   6.537 -
   6.538 -
   6.539 +    
   6.540 +    
   6.541  end
   6.542  
   6.543  
     7.1 --- a/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Nov 07 21:30:03 2006 +0100
     7.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Nov 07 22:06:32 2006 +0100
     7.3 @@ -3,21 +3,8 @@
     7.4      Author:     Alexander Krauss, TU Muenchen
     7.5  
     7.6  
     7.7 -This is a wrapper around the inductive package which corrects some of its
     7.8 -slightly annoying behaviours and makes the whole business more controllable.
     7.9 -
    7.10 -Specifically:
    7.11 -
    7.12 -- Following newer Isar conventions, declaration and definition are done in one step
    7.13 -
    7.14 -- The specification is expected in fully quantified form. This allows the client to 
    7.15 -  control the variable order. The variables will appear in the result in the same order.
    7.16 -  This is especially relevant for the elimination rule, where the order usually *does* matter.
    7.17 -
    7.18 -
    7.19 -All this will probably become obsolete in the near future, when the new "predicate" package
    7.20 -is in place.
    7.21 -
    7.22 +A wrapper around the inductive package, restoring the quantifiers in
    7.23 +the introduction and elimination rules.
    7.24  *)
    7.25  
    7.26  signature FUNDEF_INDUCTIVE_WRAP =
    7.27 @@ -36,7 +23,7 @@
    7.28      let
    7.29        val thy = theory_of_thm thm
    7.30        val frees = frees_in_term ctxt t 
    7.31 -                                  |> remove (op =) lfix
    7.32 +                  |> remove (op =) lfix
    7.33        val vars = Term.add_vars (prop_of thm) [] |> rev
    7.34                   
    7.35        val varmap = frees ~~ vars
     8.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Tue Nov 07 21:30:03 2006 +0100
     8.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Tue Nov 07 22:06:32 2006 +0100
     8.3 @@ -7,8 +7,8 @@
     8.4  
     8.5  signature LEXICOGRAPHIC_ORDER =
     8.6  sig
     8.7 -    val lexicographic_order : Method.method
     8.8 -    val setup: theory -> theory
     8.9 +  val lexicographic_order : Method.method
    8.10 +  val setup: theory -> theory
    8.11  end
    8.12  
    8.13  structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
    8.14 @@ -19,222 +19,222 @@
    8.15  val wf_measures = thm "wf_measures"
    8.16  val measures_less = thm "measures_less"
    8.17  val measures_lesseq = thm "measures_lesseq"
    8.18 -
    8.19 +                      
    8.20  fun del_index (n, []) = []
    8.21    | del_index (n, x :: xs) =
    8.22 -      if n>0 then x :: del_index (n - 1, xs) else xs 
    8.23 +    if n>0 then x :: del_index (n - 1, xs) else xs 
    8.24  
    8.25  fun transpose ([]::_) = []
    8.26    | transpose xss = map hd xss :: transpose (map tl xss)
    8.27  
    8.28  fun mk_sum_case (f1, f2) =
    8.29      case (fastype_of f1, fastype_of f2) of
    8.30 -	(Type("fun", [A, B]), Type("fun", [C, D])) =>
    8.31 -	if (B = D) then
    8.32 -            Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) $ f1 $ f2
    8.33 -	else raise TERM ("mk_sum_case: range type mismatch", [f1, f2]) 
    8.34 -      | _ => raise TERM ("mk_sum_case", [f1, f2])
    8.35 -
    8.36 +      (Type("fun", [A, B]), Type("fun", [C, D])) =>
    8.37 +      if (B = D) then
    8.38 +        Const("Datatype.sum.sum_case", (A --> B) --> (C --> D) --> Type("+", [A,C]) --> B) $ f1 $ f2
    8.39 +      else raise TERM ("mk_sum_case: range type mismatch", [f1, f2]) 
    8.40 +    | _ => raise TERM ("mk_sum_case", [f1, f2])
    8.41 +                 
    8.42  fun dest_wf (Const ("Wellfounded_Recursion.wf", _) $ t) = t
    8.43    | dest_wf t = raise TERM ("dest_wf", [t])
    8.44 -
    8.45 +                      
    8.46  datatype cell = Less of thm | LessEq of thm | None of thm | False of thm;
    8.47 -
    8.48 +         
    8.49  fun is_Less cell = case cell of (Less _) => true | _ => false  
    8.50 -
    8.51 +                                                        
    8.52  fun is_LessEq cell = case cell of (LessEq _) => true | _ => false
    8.53 -
    8.54 +                                                            
    8.55  fun thm_of_cell cell =
    8.56      case cell of 
    8.57 -	Less thm => thm
    8.58 -      | LessEq thm => thm
    8.59 -      | False thm => thm
    8.60 -      | None thm => thm
    8.61 -			   
    8.62 +      Less thm => thm
    8.63 +    | LessEq thm => thm
    8.64 +    | False thm => thm
    8.65 +    | None thm => thm
    8.66 +                  
    8.67  fun mk_base_fun_bodys (t : term) (tt : typ) =
    8.68      case tt of
    8.69 -	Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) $ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) $ t) st)      
    8.70 -      | _ => [(t, tt)]
    8.71 -	     
    8.72 +      Type("*", [ft, st]) => (mk_base_fun_bodys (Const("fst", tt --> ft) $ t) ft) @ (mk_base_fun_bodys (Const("snd", tt --> st) $ t) st)      
    8.73 +    | _ => [(t, tt)]
    8.74 +           
    8.75  fun mk_base_fun_header fulltyp (t, typ) =
    8.76      if typ = HOLogic.natT then
    8.77 -	Abs ("x", fulltyp, t)
    8.78 +      Abs ("x", fulltyp, t)
    8.79      else Abs ("x", fulltyp, Const("Nat.size", typ --> HOLogic.natT) $ t)
    8.80 -	 	 
    8.81 +         
    8.82  fun mk_base_funs (tt: typ) = 
    8.83      mk_base_fun_bodys (Bound 0) tt |>
    8.84 -		      map (mk_base_fun_header tt)
    8.85 -		   
    8.86 +                      map (mk_base_fun_header tt)
    8.87 +    
    8.88  fun mk_ext_base_funs (tt : typ) =
    8.89      case tt of
    8.90 -	Type("+", [ft, st]) =>
    8.91 -	product (mk_ext_base_funs ft) (mk_ext_base_funs st)
    8.92 -        |> map mk_sum_case
    8.93 -      | _ => mk_base_funs tt
    8.94 -
    8.95 +      Type("+", [ft, st]) =>
    8.96 +      product (mk_ext_base_funs ft) (mk_ext_base_funs st)
    8.97 +              |> map mk_sum_case
    8.98 +    | _ => mk_base_funs tt
    8.99 +           
   8.100  fun dest_term (t : term) =
   8.101      let
   8.102 -	val (vars, prop) = (FundefLib.dest_all_all t)
   8.103 -	val prems = Logic.strip_imp_prems prop
   8.104 -	val (tuple, rel) = Logic.strip_imp_concl prop
   8.105 -                           |> HOLogic.dest_Trueprop 
   8.106 -                           |> HOLogic.dest_mem
   8.107 -	val (lhs, rhs) = HOLogic.dest_prod tuple
   8.108 +      val (vars, prop) = (FundefLib.dest_all_all t)
   8.109 +      val prems = Logic.strip_imp_prems prop
   8.110 +      val (tuple, rel) = Logic.strip_imp_concl prop
   8.111 +                         |> HOLogic.dest_Trueprop 
   8.112 +                         |> HOLogic.dest_mem
   8.113 +      val (lhs, rhs) = HOLogic.dest_prod tuple
   8.114      in
   8.115 -	(vars, prems, lhs, rhs, rel)
   8.116 +      (vars, prems, lhs, rhs, rel)
   8.117      end
   8.118 -
   8.119 +    
   8.120  fun mk_goal (vars, prems, lhs, rhs) rel =
   8.121      let 
   8.122 -	val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
   8.123 -    in	
   8.124 -	Logic.list_implies (prems, concl) |>
   8.125 -	fold_rev FundefLib.mk_forall vars
   8.126 +      val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
   8.127 +    in  
   8.128 +      Logic.list_implies (prems, concl) |>
   8.129 +                         fold_rev FundefLib.mk_forall vars
   8.130      end
   8.131 -
   8.132 +    
   8.133  fun prove (thy: theory) (t: term) =
   8.134      cterm_of thy t |> Goal.init 
   8.135      |> SINGLE (CLASIMPSET auto_tac) |> the
   8.136 -
   8.137 +    
   8.138  fun mk_cell (thy : theory) (vars, prems) (lhs, rhs) = 
   8.139 -    let	
   8.140 -	val goals = mk_goal (vars, prems, lhs, rhs) 
   8.141 -	val less_thm = goals "Orderings.less" |> prove thy
   8.142 +    let 
   8.143 +      val goals = mk_goal (vars, prems, lhs, rhs) 
   8.144 +      val less_thm = goals "Orderings.less" |> prove thy
   8.145      in
   8.146 -	if Thm.no_prems less_thm then
   8.147 -	    Less (Goal.finish less_thm)
   8.148 -	else
   8.149 -	    let
   8.150 -		val lesseq_thm = goals "Orderings.less_eq" |> prove thy
   8.151 -	    in
   8.152 -		if Thm.no_prems lesseq_thm then
   8.153 -		    LessEq (Goal.finish lesseq_thm)
   8.154 -		else 
   8.155 -		    if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
   8.156 -		    else None lesseq_thm
   8.157 -	    end
   8.158 +      if Thm.no_prems less_thm then
   8.159 +        Less (Goal.finish less_thm)
   8.160 +      else
   8.161 +        let
   8.162 +          val lesseq_thm = goals "Orderings.less_eq" |> prove thy
   8.163 +        in
   8.164 +          if Thm.no_prems lesseq_thm then
   8.165 +            LessEq (Goal.finish lesseq_thm)
   8.166 +          else 
   8.167 +            if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
   8.168 +            else None lesseq_thm
   8.169 +        end
   8.170      end
   8.171 -
   8.172 +    
   8.173  fun mk_row (thy: theory) base_funs (t : term) =
   8.174      let
   8.175 -	val (vars, prems, lhs, rhs, _) = dest_term t
   8.176 -	val lhs_list = map (fn x => x $ lhs) base_funs
   8.177 -	val rhs_list = map (fn x => x $ rhs) base_funs
   8.178 +      val (vars, prems, lhs, rhs, _) = dest_term t
   8.179 +      val lhs_list = map (fn x => x $ lhs) base_funs
   8.180 +      val rhs_list = map (fn x => x $ rhs) base_funs
   8.181      in
   8.182 -	map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
   8.183 +      map (mk_cell thy (vars, prems)) (lhs_list ~~ rhs_list)
   8.184      end
   8.185 -
   8.186 +      
   8.187  (* simple depth-first search algorithm for the table *)
   8.188  fun search_table table =
   8.189      case table of
   8.190 -	[] => SOME []
   8.191 -      | _ =>
   8.192 -	let
   8.193 -	    val check_col = forall (fn c => is_Less c orelse is_LessEq c)
   8.194 -            val col = find_index (check_col) (transpose table)
   8.195 -	in case col of
   8.196 -	       ~1 => NONE 
   8.197 -             | _ =>
   8.198 -               let
   8.199 -		   val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table
   8.200 -		   val transform_order = (fn col => map (fn x => if x>=col then x+1 else x))
   8.201 -               in case order_opt of
   8.202 -		      NONE => NONE
   8.203 -		    | SOME order =>SOME (col::(transform_order col order))
   8.204 -	       end
   8.205 -	end
   8.206 -
   8.207 +      [] => SOME []
   8.208 +    | _ =>
   8.209 +      let
   8.210 +        val check_col = forall (fn c => is_Less c orelse is_LessEq c)
   8.211 +        val col = find_index (check_col) (transpose table)
   8.212 +      in case col of
   8.213 +           ~1 => NONE 
   8.214 +         | _ =>
   8.215 +           let
   8.216 +             val order_opt = table |> filter_out (fn x => is_Less (nth x col)) |> map (curry del_index col) |> search_table
   8.217 +             val transform_order = (fn col => map (fn x => if x>=col then x+1 else x))
   8.218 +           in case order_opt of
   8.219 +                NONE => NONE
   8.220 +              | SOME order =>SOME (col::(transform_order col order))
   8.221 +           end
   8.222 +      end
   8.223 +      
   8.224  fun prove_row row (st : thm) =
   8.225      case row of
   8.226 -        [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)" 
   8.227 -      | cell::tail =>
   8.228 -	case cell of
   8.229 -	    Less less_thm =>
   8.230 -	    let
   8.231 -		val next_thm = st |> SINGLE (rtac measures_less 1) |> the
   8.232 -	    in
   8.233 -		implies_elim next_thm less_thm
   8.234 -	    end
   8.235 -	  | LessEq lesseq_thm =>
   8.236 -	    let
   8.237 -		val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
   8.238 -	    in
   8.239 -		implies_elim next_thm lesseq_thm |>
   8.240 -                prove_row tail
   8.241 -	    end
   8.242 -          | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
   8.243 -
   8.244 +      [] => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (row is empty)" 
   8.245 +    | cell::tail =>
   8.246 +      case cell of
   8.247 +        Less less_thm =>
   8.248 +        let
   8.249 +          val next_thm = st |> SINGLE (rtac measures_less 1) |> the
   8.250 +        in
   8.251 +          implies_elim next_thm less_thm
   8.252 +        end
   8.253 +      | LessEq lesseq_thm =>
   8.254 +        let
   8.255 +          val next_thm = st |> SINGLE (rtac measures_lesseq 1) |> the
   8.256 +        in
   8.257 +          implies_elim next_thm lesseq_thm 
   8.258 +          |> prove_row tail
   8.259 +        end
   8.260 +      | _ => sys_error "INTERNAL ERROR IN lexicographic order termination tactic - fun prove_row (Only expecting Less or LessEq)"
   8.261 +             
   8.262  fun pr_unprovable_subgoals table =
   8.263      filter (fn x => not (is_Less x) andalso not (is_LessEq x)) (flat table)
   8.264 -	   |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
   8.265 -
   8.266 +    |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
   8.267 +    
   8.268  fun pr_goal thy t i = 
   8.269      let
   8.270 -	val (_, prems, lhs, rhs, _) = dest_term t 
   8.271 -	val prterm = string_of_cterm o (cterm_of thy)
   8.272 +      val (_, prems, lhs, rhs, _) = dest_term t 
   8.273 +      val prterm = string_of_cterm o (cterm_of thy)
   8.274      in
   8.275 -	(* also show prems? *)
   8.276 +      (* also show prems? *)
   8.277          i ^ ") " ^ (prterm lhs) ^ " '<' " ^ (prterm rhs) 
   8.278      end
   8.279 -
   8.280 +    
   8.281  fun pr_fun thy t i =
   8.282      (string_of_int i) ^ ") " ^ (string_of_cterm (cterm_of thy t))
   8.283 -
   8.284 +    
   8.285  fun pr_cell cell = case cell of Less _ => " <  " 
   8.286 -				| LessEq _ => " <= " 
   8.287 -				| None _ => " N  "
   8.288 -				| False _ => " F  "
   8.289 -       
   8.290 +                              | LessEq _ => " <= " 
   8.291 +                              | None _ => " N  "
   8.292 +                              | False _ => " F  "
   8.293 +                                             
   8.294  (* fun pr_err: prints the table if tactic failed *)
   8.295  fun pr_err table thy tl base_funs =  
   8.296      let 
   8.297 -	val gc = map (fn i => chr (i + 96)) (1 upto (length table))
   8.298 -	val mc = 1 upto (length base_funs)
   8.299 -	val tstr = ("   " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ "  ") mc))) ::
   8.300 -		   (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
   8.301 -	val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
   8.302 -	val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc))   
   8.303 -	val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
   8.304 +      val gc = map (fn i => chr (i + 96)) (1 upto (length table))
   8.305 +      val mc = 1 upto (length base_funs)
   8.306 +      val tstr = ("   " ^ (concat (map (fn i => " " ^ (string_of_int i) ^ "  ") mc))) ::
   8.307 +                 (map2 (fn r => fn i => i ^ ": " ^ (concat (map pr_cell r))) table gc)
   8.308 +      val gstr = ("Goals:"::(map2 (pr_goal thy) tl gc))
   8.309 +      val mstr = ("Measures:"::(map2 (pr_fun thy) base_funs mc))   
   8.310 +      val ustr = ("Unfinished subgoals:"::(pr_unprovable_subgoals table))
   8.311      in
   8.312 -	tstr @ gstr @ mstr @ ustr
   8.313 +      tstr @ gstr @ mstr @ ustr
   8.314      end
   8.315 -
   8.316 +      
   8.317  (* the main function: create table, search table, create relation,
   8.318     and prove the subgoals *)
   8.319  fun lexicographic_order_tac (st: thm) = 
   8.320      let
   8.321 -	val thy = theory_of_thm st
   8.322 -        val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
   8.323 -	val next_st = SINGLE (rtac termination_thm 1) st |> the
   8.324 -        val premlist = prems_of next_st
   8.325 +      val thy = theory_of_thm st
   8.326 +      val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
   8.327 +      val next_st = SINGLE (rtac termination_thm 1) st |> the
   8.328 +      val premlist = prems_of next_st
   8.329      in
   8.330 -        case premlist of 
   8.331 +      case premlist of 
   8.332              [] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal" 
   8.333            | (wf::tl) => let
   8.334 -		val (var, prop) = FundefLib.dest_all wf
   8.335 -		val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
   8.336 -		val crel = cterm_of thy rel
   8.337 -		val base_funs = mk_ext_base_funs (fastype_of var)
   8.338 -		val _ = writeln "Creating table"
   8.339 -		val table = map (mk_row thy base_funs) tl
   8.340 -		val _ = writeln "Searching for lexicographic order"
   8.341 -		val possible_order = search_table table
   8.342 -	    in
   8.343 -		case possible_order of 
   8.344 -		    NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
   8.345 -		  | SOME order  => let
   8.346 -			val clean_table = map (fn x => map (nth x) order) table
   8.347 -			val funs = map (nth base_funs) order
   8.348 -			val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
   8.349 -			val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list)
   8.350 -			val crelterm = cterm_of thy relterm
   8.351 -			val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
   8.352 -			val _ = writeln "Proving subgoals"
   8.353 -		    in
   8.354 -			next_st |> cterm_instantiate [(crel, crelterm)]
   8.355 -				|> SINGLE (rtac wf_measures 1) |> the
   8.356 -				|> fold prove_row clean_table
   8.357 -				|> Seq.single
   8.358 +    val (var, prop) = FundefLib.dest_all wf
   8.359 +    val rel = HOLogic.dest_Trueprop prop |> dest_wf |> head_of
   8.360 +    val crel = cterm_of thy rel
   8.361 +    val base_funs = mk_ext_base_funs (fastype_of var)
   8.362 +    val _ = writeln "Creating table"
   8.363 +    val table = map (mk_row thy base_funs) tl
   8.364 +    val _ = writeln "Searching for lexicographic order"
   8.365 +    val possible_order = search_table table
   8.366 +      in
   8.367 +    case possible_order of 
   8.368 +        NONE => error (cat_lines ("Could not prove it by lexicographic order:"::(pr_err table thy tl base_funs)))
   8.369 +      | SOME order  => let
   8.370 +      val clean_table = map (fn x => map (nth x) order) table
   8.371 +      val funs = map (nth base_funs) order
   8.372 +      val list = HOLogic.mk_list (fn x => x) (fastype_of var --> HOLogic.natT) funs
   8.373 +      val relterm = Abs ("x", fastype_of var, Const(measures, (fastype_of list) --> (range_type (fastype_of rel))) $ list)
   8.374 +      val crelterm = cterm_of thy relterm
   8.375 +      val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
   8.376 +      val _ = writeln "Proving subgoals"
   8.377 +        in
   8.378 +      next_st |> cterm_instantiate [(crel, crelterm)]
   8.379 +        |> SINGLE (rtac wf_measures 1) |> the
   8.380 +        |> fold prove_row clean_table
   8.381 +        |> Seq.single
   8.382                      end
   8.383              end
   8.384      end
     9.1 --- a/src/HOL/Tools/function_package/mutual.ML	Tue Nov 07 21:30:03 2006 +0100
     9.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Tue Nov 07 22:06:32 2006 +0100
     9.3 @@ -50,7 +50,7 @@
     9.4  fun split_def ctxt fnames geq arities =
     9.5      let
     9.6        fun input_error msg = error (cat_lines [msg, ProofContext.string_of_term ctxt geq])
     9.7 -
     9.8 +                            
     9.9        val (qs, imp) = open_all_all geq
    9.10  
    9.11        val gs = Logic.strip_imp_prems imp
    9.12 @@ -69,7 +69,7 @@
    9.13        fun add_bvs t is = add_loose_bnos (t, 0, is)
    9.14        val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
    9.15                    |> map (fst o nth (rev qs))
    9.16 -
    9.17 +                
    9.18        val _ = if null rvs then ()
    9.19                else input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
    9.20                                  ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
    9.21 @@ -83,17 +83,17 @@
    9.22        val k = length args
    9.23  
    9.24        val arities' = case Symtab.lookup arities fname of
    9.25 -                   NONE => Symtab.update (fname, k) arities
    9.26 -                 | SOME i => if (i <> k)
    9.27 -                             then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
    9.28 -                             else arities
    9.29 +                       NONE => Symtab.update (fname, k) arities
    9.30 +                     | SOME i => if (i <> k)
    9.31 +                                 then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
    9.32 +                                 else arities
    9.33      in
    9.34 -        ((fname, qs, gs, args, rhs), arities')
    9.35 +      ((fname, qs, gs, args, rhs), arities')
    9.36      end
    9.37 -
    9.38 +    
    9.39  fun get_part fname =
    9.40      the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
    9.41 -
    9.42 +                     
    9.43  (* FIXME *)
    9.44  fun mk_prod_abs e (t1, t2) =
    9.45      let
    9.46 @@ -141,7 +141,7 @@
    9.47              in
    9.48                  (MutualPart {fvar=fvar,cargTs=caTs,pthA=pthA,pthR=pthR,f_def=def,f=NONE,f_defthm=NONE}, rew)
    9.49              end
    9.50 -
    9.51 +            
    9.52          val (parts, rews) = split_list (map4 define fs caTss pthsA pthsR)
    9.53  
    9.54          fun convert_eqs (f, qs, gs, args, rhs) =
    9.55 @@ -171,10 +171,10 @@
    9.56                                                                lthy
    9.57            in
    9.58              (MutualPart {fvar=(fname, fT), cargTs=cargTs, pthA=pthA, pthR=pthR, f_def=f_def,
    9.59 -                        f=SOME f, f_defthm=SOME f_defthm },
    9.60 +                         f=SOME f, f_defthm=SOME f_defthm },
    9.61               lthy')
    9.62            end
    9.63 -
    9.64 +          
    9.65        val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual
    9.66        val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
    9.67      in
    9.68 @@ -186,39 +186,39 @@
    9.69  
    9.70  fun prepare_fundef_mutual fixes eqss default lthy =
    9.71      let
    9.72 -        val mutual = analyze_eqs lthy (map fst fixes) eqss
    9.73 -        val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
    9.74 -
    9.75 -        val (prep_result, fsum, lthy') =
    9.76 -            FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
    9.77 -
    9.78 -        val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
    9.79 +      val mutual = analyze_eqs lthy (map fst fixes) eqss
    9.80 +      val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
    9.81 +          
    9.82 +      val (prep_result, fsum, lthy') =
    9.83 +          FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
    9.84 +          
    9.85 +      val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
    9.86      in
    9.87        ((mutual', defname, prep_result), lthy'')
    9.88      end
    9.89 -
    9.90 +      
    9.91  
    9.92  (* Beta-reduce both sides of a meta-equality *)
    9.93  fun beta_norm_eq thm =
    9.94      let
    9.95 -        val (lhs, rhs) = dest_equals (cprop_of thm)
    9.96 -        val lhs_conv = beta_conversion false lhs
    9.97 -        val rhs_conv = beta_conversion false rhs
    9.98 +      val (lhs, rhs) = dest_equals (cprop_of thm)
    9.99 +      val lhs_conv = beta_conversion false lhs
   9.100 +      val rhs_conv = beta_conversion false rhs
   9.101      in
   9.102 -        transitive (symmetric lhs_conv) (transitive thm rhs_conv)
   9.103 +      transitive (symmetric lhs_conv) (transitive thm rhs_conv)
   9.104      end
   9.105 -
   9.106 +    
   9.107  fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm
   9.108 -
   9.109 -
   9.110 +                      
   9.111 +                      
   9.112  fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
   9.113      let
   9.114        val thy = ProofContext.theory_of ctxt
   9.115 -
   9.116 +                
   9.117        val oqnames = map fst pre_qs
   9.118        val (qs, ctxt') = Variable.variant_fixes oqnames ctxt
   9.119 -                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
   9.120 -
   9.121 +                        |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
   9.122 +                        
   9.123        fun inst t = subst_bounds (rev qs, t)
   9.124        val gs = map inst pre_gs
   9.125        val args = map inst pre_args
   9.126 @@ -240,7 +240,7 @@
   9.127  fun recover_mutual_psimp thy RST streeR all_f_defs parts (f, _, _, args, _) import (export : thm -> thm) sum_psimp_eq =
   9.128      let
   9.129        val (MutualPart {f_defthm=SOME f_def, pthR, ...}) = get_part f parts
   9.130 -
   9.131 +          
   9.132        val psimp = import sum_psimp_eq
   9.133        val (simp, restore_cond) = case cprems_of psimp of
   9.134                                     [] => (psimp, I)
   9.135 @@ -275,46 +275,46 @@
   9.136             |> fold_rev forall_intr xs
   9.137             |> forall_elim_vars 0
   9.138      end
   9.139 -
   9.140 +    
   9.141  
   9.142  fun mutual_induct_rules thy induct all_f_defs (Mutual {RST, parts, streeA, ...}) =
   9.143      let
   9.144        val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => 
   9.145 -                                   Free (Pname, cargTs ---> HOLogic.boolT))
   9.146 +                                       Free (Pname, cargTs ---> HOLogic.boolT))
   9.147                         (mutual_induct_Pnames (length parts))
   9.148                         parts
   9.149 -
   9.150 -        fun mk_P (MutualPart {cargTs, ...}) P =
   9.151 -            let
   9.152 -                val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
   9.153 -                val atup = foldr1 HOLogic.mk_prod avars
   9.154 -            in
   9.155 -                tupled_lambda atup (list_comb (P, avars))
   9.156 -            end
   9.157 -
   9.158 -        val Ps = map2 mk_P parts newPs
   9.159 -        val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
   9.160 -
   9.161 -        val induct_inst =
   9.162 -            forall_elim (cterm_of thy case_exp) induct
   9.163 -                        |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
   9.164 -                        |> full_simplify (HOL_basic_ss addsimps all_f_defs)
   9.165 -
   9.166 -        fun mk_proj rule (MutualPart {cargTs, pthA, ...}) =
   9.167 -            let
   9.168 -                val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs
   9.169 -                val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs)
   9.170 -            in
   9.171 -                rule
   9.172 -                    |> forall_elim (cterm_of thy inj)
   9.173 -                    |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
   9.174 -                    |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs)
   9.175 -            end
   9.176 -
   9.177 +                       
   9.178 +      fun mk_P (MutualPart {cargTs, ...}) P =
   9.179 +          let
   9.180 +            val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
   9.181 +            val atup = foldr1 HOLogic.mk_prod avars
   9.182 +          in
   9.183 +            tupled_lambda atup (list_comb (P, avars))
   9.184 +          end
   9.185 +          
   9.186 +      val Ps = map2 mk_P parts newPs
   9.187 +      val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
   9.188 +                     
   9.189 +      val induct_inst =
   9.190 +          forall_elim (cterm_of thy case_exp) induct
   9.191 +                      |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
   9.192 +                      |> full_simplify (HOL_basic_ss addsimps all_f_defs)
   9.193 +          
   9.194 +      fun mk_proj rule (MutualPart {cargTs, pthA, ...}) =
   9.195 +          let
   9.196 +            val afs = map_index (fn (i,T) => Free ("a" ^ string_of_int i, T)) cargTs
   9.197 +            val inj = SumTools.mk_inj streeA pthA (foldr1 HOLogic.mk_prod afs)
   9.198 +          in
   9.199 +            rule
   9.200 +              |> forall_elim (cterm_of thy inj)
   9.201 +              |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
   9.202 +              |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs)
   9.203 +          end
   9.204 +          
   9.205      in
   9.206        map (mk_proj induct_inst) parts
   9.207      end
   9.208 -
   9.209 +    
   9.210  
   9.211  
   9.212  
   9.213 @@ -322,44 +322,44 @@
   9.214  fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result =
   9.215      let
   9.216        val thy = ProofContext.theory_of lthy
   9.217 -
   9.218 +                                       
   9.219        (* FIXME !? *)
   9.220 -      val expand = Assumption.export false lthy (LocalTheory.target_of lthy);
   9.221 -      val expand_term = Drule.term_rule thy expand;
   9.222 -
   9.223 +      val expand = Assumption.export false lthy (LocalTheory.target_of lthy)
   9.224 +      val expand_term = Drule.term_rule thy expand
   9.225 +                        
   9.226        val result = FundefProof.mk_partial_rules thy data prep_result
   9.227        val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
   9.228 -
   9.229 +                                                                                                               
   9.230        val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} =>
   9.231                                 mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def)))
   9.232                             parts
   9.233 -
   9.234 +                           
   9.235        fun mk_mpsimp fqgar sum_psimp =
   9.236            in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
   9.237 -
   9.238 +          
   9.239        val mpsimps = map2 mk_mpsimp fqgars psimps
   9.240 -
   9.241 +                    
   9.242        val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
   9.243        val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro
   9.244      in
   9.245        FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R,
   9.246 -                                  psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
   9.247 -                                  cases=expand completeness, termination=expand termination,
   9.248 +                      psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
   9.249 +                      cases=expand completeness, termination=expand termination,
   9.250                        domintros=map expand dom_intros }
   9.251      end
   9.252 -
   9.253 -
   9.254 -
   9.255 +      
   9.256 +      
   9.257 +      
   9.258  (* puts an object in the "right bucket" *)
   9.259  fun store_grouped P x [] = []
   9.260    | store_grouped P x ((l, xs)::bs) =
   9.261      if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs)
   9.262 -
   9.263 +                                           
   9.264  fun sort_by_function (Mutual {fqgars, ...}) names xs =
   9.265 -      fold_rev (store_grouped (eq_str o apfst fst))  (* fill *)
   9.266 -               (map name_of_fqgar fqgars ~~ xs)      (* the name-thm pairs *)
   9.267 -               (map (rpair []) names)                (* in the empty buckets labeled with names *)
   9.268 -
   9.269 -         |> map (snd #> map snd)                     (* and remove the labels afterwards *)
   9.270 -
   9.271 +    fold_rev (store_grouped (eq_str o apfst fst))  (* fill *)
   9.272 +             (map name_of_fqgar fqgars ~~ xs)      (* the name-thm pairs *)
   9.273 +             (map (rpair []) names)                (* in the empty buckets labeled with names *)
   9.274 +             
   9.275 +             |> map (snd #> map snd)                     (* and remove the labels afterwards *)
   9.276 +    
   9.277  end
    10.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Tue Nov 07 21:30:03 2006 +0100
    10.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Tue Nov 07 22:06:32 2006 +0100
    10.3 @@ -12,10 +12,10 @@
    10.4  signature FUNDEF_SPLIT =
    10.5  sig
    10.6    val split_some_equations :
    10.7 -    Proof.context -> (bool * term) list -> term list list
    10.8 +      Proof.context -> (bool * term) list -> term list list
    10.9  
   10.10    val split_all_equations :
   10.11 -    Proof.context -> term list -> term list list
   10.12 +      Proof.context -> term list -> term list list
   10.13  end
   10.14  
   10.15  structure FundefSplit : FUNDEF_SPLIT =
   10.16 @@ -36,16 +36,16 @@
   10.17  fun saturate ctx vs t =
   10.18      fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op $ t))
   10.19           (binder_types (fastype_of t)) (vs, t)
   10.20 -
   10.21 -
   10.22 +         
   10.23 +         
   10.24  (* This is copied from "fundef_datatype.ML" *)
   10.25  fun inst_constrs_of thy (T as Type (name, _)) =
   10.26 -        map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
   10.27 -            (the (DatatypePackage.get_datatype_constrs thy name))
   10.28 +    map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
   10.29 +        (the (DatatypePackage.get_datatype_constrs thy name))
   10.30    | inst_constrs_of thy t = (print t; sys_error "inst_constrs_of")
   10.31 -
   10.32 -
   10.33 -
   10.34 +                            
   10.35 +                            
   10.36 +                            
   10.37  
   10.38  fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
   10.39  fun join_product (xs, ys) = map join (product xs ys)
   10.40 @@ -91,12 +91,12 @@
   10.41  fun pattern_subtract ctx eq2 eq1 =
   10.42      let
   10.43        val thy = ProofContext.theory_of ctx
   10.44 -      
   10.45 +                
   10.46        val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
   10.47        val (_,  _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
   10.48 -
   10.49 +                                     
   10.50        val substs = pattern_subtract_subst ctx vs lhs1 lhs2
   10.51 -
   10.52 +                   
   10.53        fun instantiate (vs', sigma) =
   10.54            let
   10.55              val t = Pattern.rewrite_term thy sigma [] feq1
   10.56 @@ -106,7 +106,7 @@
   10.57      in
   10.58        map instantiate substs
   10.59      end
   10.60 -
   10.61 +      
   10.62  
   10.63  (* ps - p' *)
   10.64  fun pattern_subtract_from_many ctx p'=
   10.65 @@ -128,7 +128,7 @@
   10.66      in
   10.67        split_aux [] eqns
   10.68      end
   10.69 -
   10.70 +    
   10.71  fun split_all_equations ctx =
   10.72      split_some_equations ctx o map (pair true)
   10.73  
    11.1 --- a/src/HOL/Tools/function_package/sum_tools.ML	Tue Nov 07 21:30:03 2006 +0100
    11.2 +++ b/src/HOL/Tools/function_package/sum_tools.ML	Tue Nov 07 22:06:32 2006 +0100
    11.3 @@ -46,30 +46,30 @@
    11.4    | Branch of (typ * (typ * sum_tree) * (typ * sum_tree))
    11.5  
    11.6  type sum_path = bool list (* true: left, false: right *)
    11.7 -
    11.8 +                
    11.9  fun sum_type_of (Leaf T) = T
   11.10    | sum_type_of (Branch (ST,(LT,_),(RT,_))) = ST
   11.11 -
   11.12 -
   11.13 +                                              
   11.14 +                                              
   11.15  fun mk_tree Ts =
   11.16      let 
   11.17 -	fun mk_tree' 1 [T] = (T, Leaf T, [[]])
   11.18 -	  | mk_tree' n Ts =
   11.19 -	    let 
   11.20 -		val n2 = n div 2
   11.21 -		val (lTs, rTs) = chop n2 Ts
   11.22 -		val (TL, ltree, lpaths) = mk_tree' n2 lTs
   11.23 -		val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs
   11.24 -		val T = mk_sumT TL TR
   11.25 -		val pths = map (cons true) lpaths @ map (cons false) rpaths 
   11.26 -	    in
   11.27 -		(T, Branch (T, (TL, ltree), (TR, rtree)), pths)
   11.28 -	    end
   11.29 +      fun mk_tree' 1 [T] = (T, Leaf T, [[]])
   11.30 +        | mk_tree' n Ts =
   11.31 +          let 
   11.32 +            val n2 = n div 2
   11.33 +            val (lTs, rTs) = chop n2 Ts
   11.34 +            val (TL, ltree, lpaths) = mk_tree' n2 lTs
   11.35 +            val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs
   11.36 +            val T = mk_sumT TL TR
   11.37 +            val pths = map (cons true) lpaths @ map (cons false) rpaths 
   11.38 +          in
   11.39 +            (T, Branch (T, (TL, ltree), (TR, rtree)), pths)
   11.40 +          end
   11.41      in
   11.42 -	mk_tree' (length Ts) Ts
   11.43 +      mk_tree' (length Ts) Ts
   11.44      end
   11.45 -
   11.46 -
   11.47 +    
   11.48 +    
   11.49  fun mk_tree_distinct Ts =
   11.50      let
   11.51        fun insert_once T Ts =
   11.52 @@ -78,9 +78,9 @@
   11.53            in
   11.54              if i = ~1 then (length Ts, Ts @ [T]) else (i, Ts)
   11.55            end
   11.56 -
   11.57 +          
   11.58        val (idxs, dist_Ts) = fold_map insert_once Ts []
   11.59 -
   11.60 +                            
   11.61        val (ST, tree, pths) = mk_tree dist_Ts
   11.62      in
   11.63        (ST, tree, map (nth pths) idxs)
   11.64 @@ -104,19 +104,19 @@
   11.65  
   11.66  fun mk_sumcases tree T ts =
   11.67      let
   11.68 -	fun mk_sumcases' (Leaf _) (t::ts) = (t,ts)
   11.69 -	  | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts =
   11.70 -	    let
   11.71 -		val (lcase, ts') = mk_sumcases' ltr ts
   11.72 -		val (rcase, ts'') = mk_sumcases' rtr ts'
   11.73 -	    in
   11.74 -		(mk_sumcase LT RT T lcase rcase, ts'')
   11.75 -	    end
   11.76 -	  | mk_sumcases' _ [] = sys_error "mk_sumcases"
   11.77 +      fun mk_sumcases' (Leaf _) (t::ts) = (t,ts)
   11.78 +        | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts =
   11.79 +          let
   11.80 +            val (lcase, ts') = mk_sumcases' ltr ts
   11.81 +            val (rcase, ts'') = mk_sumcases' rtr ts'
   11.82 +          in
   11.83 +            (mk_sumcase LT RT T lcase rcase, ts'')
   11.84 +          end
   11.85 +        | mk_sumcases' _ [] = sys_error "mk_sumcases"
   11.86      in
   11.87 -	fst (mk_sumcases' tree ts)
   11.88 +      fst (mk_sumcases' tree ts)
   11.89      end
   11.90 -
   11.91 +    
   11.92  end
   11.93  
   11.94  
    12.1 --- a/src/HOL/Tools/function_package/termination.ML	Tue Nov 07 21:30:03 2006 +0100
    12.2 +++ b/src/HOL/Tools/function_package/termination.ML	Tue Nov 07 22:06:32 2006 +0100
    12.3 @@ -9,8 +9,8 @@
    12.4  
    12.5  signature FUNDEF_TERMINATION =
    12.6  sig
    12.7 -    val mk_total_termination_goal : FundefCommon.result_with_names -> term
    12.8 -    val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
    12.9 +  val mk_total_termination_goal : FundefCommon.result_with_names -> term
   12.10 +  val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
   12.11  end
   12.12  
   12.13  structure FundefTermination : FUNDEF_TERMINATION =
   12.14 @@ -20,41 +20,40 @@
   12.15  open FundefLib
   12.16  open FundefCommon
   12.17  open FundefAbbrev
   12.18 -
   12.19 +     
   12.20  fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _) =
   12.21      let
   12.22 -	val domT = domain_type (fastype_of f)
   12.23 -	val x = Free ("x", domT)
   12.24 +      val domT = domain_type (fastype_of f)
   12.25 +      val x = Free ("x", domT)
   12.26      in
   12.27        mk_forall x (Trueprop (mk_acc domT R $ x))
   12.28      end
   12.29 -
   12.30 +    
   12.31  fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
   12.32      let
   12.33 -	val domT = domain_type (fastype_of f)
   12.34 -	val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
   12.35 -	val DT = type_of D
   12.36 -	val idomT = HOLogic.dest_setT DT
   12.37 -
   12.38 -	val x = Free ("x", idomT)
   12.39 -	val z = Free ("z", idomT)
   12.40 -	val Rname = fst (dest_Const R)
   12.41 -	val iRT = mk_relT (idomT, idomT)
   12.42 -	val iR = Const (Rname, iRT)
   12.43 -		
   12.44 +      val domT = domain_type (fastype_of f)
   12.45 +      val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
   12.46 +      val DT = type_of D
   12.47 +      val idomT = HOLogic.dest_setT DT
   12.48 +                  
   12.49 +      val x = Free ("x", idomT)
   12.50 +      val z = Free ("z", idomT)
   12.51 +      val Rname = fst (dest_Const R)
   12.52 +      val iRT = mk_relT (idomT, idomT)
   12.53 +      val iR = Const (Rname, iRT)
   12.54 +               
   12.55 +      val subs = HOLogic.mk_Trueprop 
   12.56 +                   (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
   12.57 +                          (Const (acc_const_name, iRT --> DT) $ iR))
   12.58 +                   |> Type.freeze
   12.59  
   12.60 -	val subs = HOLogic.mk_Trueprop 
   12.61 -			 (Const ("Orderings.less_eq", DT --> DT --> boolT) $ D $
   12.62 -				(Const (acc_const_name, iRT --> DT) $ iR))
   12.63 -			 |> Type.freeze
   12.64 -
   12.65 -	val dcl = mk_forall x
   12.66 -			    (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
   12.67 -							    Logic.mk_implies (mk_relmem (z, x) iR,
   12.68 -									      Trueprop (mk_mem (z, D))))))
   12.69 -			    |> Type.freeze
   12.70 +      val dcl = mk_forall x
   12.71 +                (mk_forall z (Logic.mk_implies (Trueprop (HOLogic.mk_mem (x, D)),
   12.72 +                                                Logic.mk_implies (mk_relmem (z, x) iR,
   12.73 +                                                                  Trueprop (mk_mem (z, D))))))
   12.74 +                |> Type.freeze
   12.75      in
   12.76 -	(subs, dcl)
   12.77 +      (subs, dcl)
   12.78      end
   12.79  
   12.80  end