Fixed name clash.
authorkrauss
Mon Jun 19 18:25:34 2006 +0200 (2006-06-19)
changeset 19922984ae977f7aa
parent 19921 2a48a5550045
child 19923 e34105dd441d
Fixed name clash.
Function-goals are now fully quantified.
Avoiding large meta-conjunctions when setting up the goal.
Cleanup.
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/mutual.ML
src/HOL/ex/Fundefs.thy
     1.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Mon Jun 19 18:02:49 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Mon Jun 19 18:25:34 2006 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4      val cong_deps : thm -> int IntGraph.T
     1.5      val add_congs : thm list
     1.6  
     1.7 -    val mk_tree: theory -> (thm * FundefCommon.depgraph) list -> term -> term -> FundefCommon.ctx_tree
     1.8 +    val mk_tree: theory -> (thm * FundefCommon.depgraph) list -> term -> ProofContext.context -> term -> FundefCommon.ctx_tree
     1.9  
    1.10      val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list
    1.11  
    1.12 @@ -70,45 +70,40 @@
    1.13  
    1.14  
    1.15  (* Called on the INSTANTIATED branches of the congruence rule *)
    1.16 -fun mk_branch t = 
    1.17 +fun mk_branch ctx t = 
    1.18      let
    1.19 -	val (fixes, impl) = dest_all_all t
    1.20 +	val (ctx', fixes, impl) = dest_all_all_ctx ctx t
    1.21  	val (assumes, term) = dest_implies_list impl
    1.22      in
    1.23 -	(map dest_Free fixes, assumes, rhs_of term)
    1.24 +      (ctx', fixes, assumes, rhs_of term)
    1.25      end
    1.26  
    1.27 -
    1.28 -
    1.29 -
    1.30 -
    1.31 -
    1.32 -fun find_cong_rule thy ((r,dep)::rs) t =
    1.33 +fun find_cong_rule thy ctx ((r,dep)::rs) t =
    1.34      (let
    1.35  	val (c, subs) = (meta_rhs_of (concl_of r), prems_of r)
    1.36  
    1.37  	val subst = Pattern.match thy (c, t) (Vartab.empty, Vartab.empty)
    1.38  
    1.39 -	val branches = map (mk_branch o Envir.beta_norm o Envir.subst_vars subst) subs
    1.40 +	val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
    1.41       in
    1.42  	 (r, dep, branches)
    1.43       end
    1.44 -    handle Pattern.MATCH => find_cong_rule thy rs t)
    1.45 -  | find_cong_rule thy [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
    1.46 +    handle Pattern.MATCH => find_cong_rule thy ctx rs t)
    1.47 +  | find_cong_rule thy _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
    1.48  
    1.49  
    1.50  fun matchcall f (a $ b) = if a = f then SOME b else NONE
    1.51    | matchcall f _ = NONE
    1.52  
    1.53 -fun mk_tree thy congs f t =
    1.54 +fun mk_tree thy congs f ctx t =
    1.55      case matchcall f t of
    1.56 -	SOME arg => RCall (t, mk_tree thy congs f arg)
    1.57 +	SOME arg => RCall (t, mk_tree thy congs f ctx arg)
    1.58        | NONE => 
    1.59  	if not (exists_Const (curry op = (dest_Const f)) t) then Leaf t
    1.60  	else 
    1.61 -	    let val (r, dep, branches) = find_cong_rule thy congs t in
    1.62 -		Cong (t, r, dep, map (fn (fixes, assumes, st) => 
    1.63 -					 (fixes, map (assume o cterm_of thy) assumes, mk_tree thy congs f st)) branches)
    1.64 +	    let val (r, dep, branches) = find_cong_rule thy ctx congs t in
    1.65 +		Cong (t, r, dep, map (fn (ctx', fixes, assumes, st) => 
    1.66 +					 (fixes, map (assume o cterm_of thy) assumes, mk_tree thy congs f ctx' st)) branches)
    1.67  	    end
    1.68  		
    1.69  		
    1.70 @@ -121,7 +116,7 @@
    1.71  fun compose (fs1, as1) (fs2, as2) = (fs1 @ fs2, as1 @ as2)
    1.72  
    1.73  fun export_term (fixes, assumes) =
    1.74 -    fold_rev (curry Logic.mk_implies) assumes #> fold (mk_forall o Free) fixes
    1.75 +    fold_rev (curry Logic.mk_implies) assumes #> fold_rev (mk_forall o Free) fixes
    1.76  
    1.77  fun export_thm thy (fixes, assumes) =
    1.78      fold_rev (implies_intr o cterm_of thy) assumes
    1.79 @@ -194,18 +189,17 @@
    1.80  	fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
    1.81  	  | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
    1.82  	    let
    1.83 -		val (inner, (Ri,ha)::x') = rewrite_help fix f_as h_as x st
    1.84 +		val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st
    1.85  					   
    1.86  					   (* Need not use the simplifier here. Can use primitive steps! *)
    1.87  		val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
    1.88  			     
    1.89  		val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
    1.90 -		val iRi = import_thm thy (fix, f_as) Ri (* a < lhs *)
    1.91  		val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
    1.92  				     |> rew_ha
    1.93  
    1.94  		val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
    1.95 -		val eq = implies_elim (implies_elim inst_ih iRi) iha
    1.96 +		val eq = implies_elim (implies_elim inst_ih lRi) iha
    1.97  			 
    1.98  		val h_a'_eq_f_a' = eq RS eq_reflection
    1.99  		val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
     2.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Jun 19 18:02:49 2006 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Jun 19 18:25:34 2006 +0200
     2.3 @@ -34,22 +34,20 @@
     2.4         glrs: (term list * term list * term * term) list,
     2.5         glrs': (term list * term list * term * term) list,
     2.6         f_def: thm,
     2.7 -       used: string list,
     2.8 -       trees: ctx_tree list
     2.9 +       ctx: ProofContext.context
    2.10       }
    2.11  
    2.12  
    2.13  datatype rec_call_info = 
    2.14    RCInfo of
    2.15    {
    2.16 -   RI: thm, 
    2.17 -   RIvs: (string * typ) list,
    2.18 -   lRI: thm, 
    2.19 -   lRIq: thm, 
    2.20 +   RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
    2.21 +   CCas: thm list,
    2.22 +   rcarg: term,                 (* The recursive argument *)
    2.23 +
    2.24 +   llRI: thm,
    2.25     Gh: thm, 
    2.26 -   Gh': thm,
    2.27 -   GmAs: term list,
    2.28 -   rcarg: term
    2.29 +   Gh': thm
    2.30    } 
    2.31       
    2.32  datatype clause_info =
    2.33 @@ -57,31 +55,28 @@
    2.34       {
    2.35        no: int,
    2.36  
    2.37 +      tree: ctx_tree,
    2.38 +      case_hyp: thm,
    2.39 +
    2.40        qs: term list, 
    2.41        gs: term list,
    2.42        lhs: term,
    2.43        rhs: term,
    2.44  
    2.45        cqs: cterm list,
    2.46 -      cvqs: cterm list,
    2.47        ags: thm list,
    2.48        
    2.49        cqs': cterm list, 
    2.50        ags': thm list,
    2.51        lhs': term,
    2.52        rhs': term,
    2.53 -      ordcqs': cterm list, 
    2.54  
    2.55 -      GI: thm,
    2.56        lGI: thm,
    2.57        RCs: rec_call_info list,
    2.58  
    2.59 -      tree: ctx_tree,
    2.60 -      case_hyp: thm
    2.61 +      ordcqs': cterm list
    2.62       }
    2.63  
    2.64 -type inj_proj = ((term -> term) * (term -> term))
    2.65 -
    2.66  type qgar = (string * typ) list * term list * term list * term
    2.67  
    2.68  datatype mutual_part =
    2.69 @@ -115,9 +110,13 @@
    2.70    Prep of
    2.71       {
    2.72        names: naming_context, 
    2.73 -      complete : term,
    2.74 -      compat : term list,
    2.75 -      clauses: clause_info list
    2.76 +      goal: term,
    2.77 +      goalI: thm,
    2.78 +      values: thm list,
    2.79 +      clauses: clause_info list,
    2.80 +
    2.81 +      R_cases: thm,
    2.82 +      ex1_iff: thm
    2.83       }
    2.84  
    2.85  datatype fundef_result =
    2.86 @@ -127,7 +126,6 @@
    2.87        G : term,
    2.88        R : term,
    2.89        completeness : thm,
    2.90 -      compatibility : thm list,
    2.91  
    2.92        psimps : thm list, 
    2.93        subset_pinduct : thm, 
     3.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jun 19 18:02:49 2006 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Jun 19 18:25:34 2006 +0200
     3.3 @@ -126,35 +126,34 @@
     3.4      in
     3.5  	o_alg thy P 2 [x] (map2 (pair o single) pats assums)
     3.6  	      |> fold_rev implies_intr hyps
     3.7 -	      |> zero_var_indexes
     3.8 -	      |> forall_intr_frees
     3.9 -	      |> forall_elim_vars 0 
    3.10      end
    3.11  
    3.12  
    3.13  
    3.14  fun pat_complete_tac i thm =
    3.15      let 
    3.16 +      val thy = theory_of_thm thm
    3.17 +
    3.18  	val subgoal = nth (prems_of thm) (i - 1)
    3.19 -	val assums = Logic.strip_imp_prems subgoal
    3.20 -	val _ $ P = Logic.strip_imp_concl subgoal
    3.21 +
    3.22 +        val ([P, x], subgf) = dest_all_all subgoal
    3.23 +
    3.24 +	val assums = Logic.strip_imp_prems subgf
    3.25  		    
    3.26  	fun pat_of assum = 
    3.27  	    let
    3.28  		val (qs, imp) = dest_all_all assum
    3.29  	    in
    3.30  		case Logic.dest_implies imp of 
    3.31 -		    (_ $ (_ $ x $ pat), _) => (x, (qs, pat))
    3.32 +		    (_ $ (_ $ _ $ pat), _) => (qs, pat)
    3.33  		  | _ => raise COMPLETENESS
    3.34  	    end
    3.35  
    3.36 -	val (x, (qss, pats)) = 
    3.37 -	    case (map pat_of assums) of
    3.38 -		[] => raise COMPLETENESS
    3.39 -	      | rs as ((x,_) :: _) 
    3.40 -		=> (x, split_list (snd (split_list rs)))
    3.41 +	val (qss, pats) = split_list (map pat_of assums)
    3.42  
    3.43 -	val complete_thm = prove_completeness (theory_of_thm thm) x P qss pats
    3.44 +	val complete_thm = prove_completeness thy x P qss pats
    3.45 +                                              |> forall_intr (cterm_of thy x)
    3.46 +                                              |> forall_intr (cterm_of thy P)
    3.47      in
    3.48  	Seq.single (Drule.compose_single(complete_thm, i, thm))
    3.49      end
     4.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jun 19 18:02:49 2006 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Mon Jun 19 18:25:34 2006 +0200
     4.3 @@ -9,11 +9,12 @@
     4.4  
     4.5  fun mk_forall (var as Free (v,T)) t =
     4.6      all T $ Abs (v,T, abstract_over (var,t))
     4.7 -  | mk_forall _ _ = raise Match
     4.8 +  | mk_forall v _ = let val _ = print v in sys_error "mk_forall" end
     4.9  
    4.10  (* Builds a quantification with a new name for the variable. *)
    4.11 -fun mk_forall_rename ((v,T),newname) t =
    4.12 -    all T $ Abs (newname,T, abstract_over (Free (v,T),t))
    4.13 +fun mk_forall_rename (v as Free (_,T),newname) t =
    4.14 +    all T $ Abs (newname, T, abstract_over (v, t))
    4.15 +  | mk_forall_rename (v, _) _ = let val _ = print v in sys_error "mk_forall_rename" end
    4.16  
    4.17  (* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *)
    4.18  fun tupled_lambda vars t =
    4.19 @@ -44,6 +45,24 @@
    4.20      end
    4.21    | dest_all_all t = ([],t)
    4.22  
    4.23 +
    4.24 +fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
    4.25 +    let
    4.26 +      val [(n', _)] = Variable.rename_wrt ctx [] [(n,T)]
    4.27 +      val (_, ctx') = ProofContext.add_fixes_i [(n', SOME T, NoSyn)] ctx
    4.28 +
    4.29 +      val (n'', body) = Term.dest_abs (n', T, b) 
    4.30 +      val _ = assert (n' = n'') "dest_all_ctx" (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
    4.31 +
    4.32 +      val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
    4.33 +    in
    4.34 +	(ctx'', (n', T) :: vs, bd)
    4.35 +    end
    4.36 +  | dest_all_all_ctx ctx t = 
    4.37 +    (ctx, [], t)
    4.38 +
    4.39 +
    4.40 +
    4.41  (* unfold *)
    4.42  fun unfold P f g b x = if (P x) then ((f x)::(unfold P f g b (g x))) else (b x)
    4.43  
    4.44 @@ -56,11 +75,15 @@
    4.45    | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
    4.46    | map3 _ _ _ _ = raise Library.UnequalLengths;
    4.47  
    4.48 +fun map6 _ [] [] [] [] [] [] = []
    4.49 +  | 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
    4.50 +  | map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths;
    4.51 +
    4.52  
    4.53  
    4.54  (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
    4.55 -fun upairs [] = []
    4.56 -  | upairs (x::xs) = map (pair x) (x::xs) @ upairs xs
    4.57 +fun unordered_pairs [] = []
    4.58 +  | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
    4.59  
    4.60  
    4.61  fun the_single [x] = x
     5.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Jun 19 18:02:49 2006 +0200
     5.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Jun 19 18:25:34 2006 +0200
     5.3 @@ -48,12 +48,11 @@
     5.4  
     5.5  
     5.6  
     5.7 -fun fundef_afterqed congs curry_info name data names atts thmss thy =
     5.8 +fun fundef_afterqed congs mutual_info name data names atts [[result]] thy =
     5.9      let
    5.10 -	val (complete_thm :: compat_thms) = map hd thmss
    5.11 -	val fundef_data = FundefMutual.mk_partial_rules_mutual thy congs curry_info data (Thm.freezeT complete_thm) (map Thm.freezeT compat_thms)
    5.12 -	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, ...} = fundef_data
    5.13 -        val Mutual {parts, ...} = curry_info
    5.14 +	val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
    5.15 +	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    5.16 +        val Mutual {parts, ...} = mutual_info
    5.17  
    5.18  	val Prep {names = Names {acc_R=accR, ...}, ...} = data
    5.19  	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    5.20 @@ -62,13 +61,13 @@
    5.21          val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) (names ~~ atts) thy
    5.22  
    5.23  	val thy = thy |> Theory.add_path name
    5.24 -	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names (flat names)])] thy
    5.25 +	val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names (flat names)])] thy
    5.26  	val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
    5.27 -	val (_, thy) = PureThy.add_thms [(("termination", termination), [])] thy
    5.28 +	val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
    5.29  	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names (flat names), InductAttrib.induct_set ""])] thy
    5.30  	val thy = thy |> Theory.parent_path
    5.31      in
    5.32 -	add_fundef_data name (fundef_data, curry_info, names, atts) thy
    5.33 +	add_fundef_data name (fundef_data, mutual_info, names, atts) thy
    5.34      end
    5.35  
    5.36  fun gen_add_fundef prep_att eqns_attss thy =
    5.37 @@ -93,14 +92,14 @@
    5.38  	val t_eqns = map (map (Sign.read_prop thy)) eqns
    5.39  			 |> map (map (term_of o cterm_of thy)) (* HACK to prevent strange things from happening with abbreviations *)
    5.40  
    5.41 -	val (curry_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
    5.42 -	val Prep {complete, compat, ...} = data
    5.43 -
    5.44 -	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
    5.45 +	val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqns thy
    5.46 +	val Prep {goal, goalI, ...} = data
    5.47      in
    5.48  	thy |> ProofContext.init
    5.49 -	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data names atts) NONE ("", [])
    5.50 -	    (map (fn t => (("", []), [(t, [])])) props)
    5.51 +	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data names atts) NONE ("", [])
    5.52 +	    [(("", []), [(goal, [])])]
    5.53 +            |> Proof.refine (Method.primitive_text (fn _ => goalI))
    5.54 +            |> Seq.hd
    5.55      end
    5.56  
    5.57  
    5.58 @@ -167,7 +166,7 @@
    5.59      in
    5.60  	thy |> ProofContext.init
    5.61  	    |> ProofContext.note_thmss_i [(("termination", 
    5.62 -					    [ContextRules.intro_query NONE]), [([termination], [])])] |> snd
    5.63 +					    [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
    5.64  	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", [])
    5.65  	    [(("", []), [(goal, [])])]
    5.66      end	
     6.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Mon Jun 19 18:02:49 2006 +0200
     6.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Mon Jun 19 18:25:34 2006 +0200
     6.3 @@ -18,13 +18,23 @@
     6.4  
     6.5  
     6.6  
     6.7 -structure FundefPrep : FUNDEF_PREP =
     6.8 +structure FundefPrep (*: FUNDEF_PREP*) =
     6.9  struct
    6.10  
    6.11  
    6.12  open FundefCommon
    6.13  open FundefAbbrev 
    6.14  
    6.15 +(* Theory dependencies. *)
    6.16 +val Pair_inject = thm "Product_Type.Pair_inject";
    6.17 +
    6.18 +val acc_induct_rule = thm "Accessible_Part.acc_induct_rule"
    6.19 +
    6.20 +val ex1_implies_ex = thm "FunDef.fundef_ex1_existence"
    6.21 +val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness"
    6.22 +val ex1_implies_iff = thm "FunDef.fundef_ex1_iff"
    6.23 +
    6.24 +val conjunctionI = thm "conjunctionI";
    6.25  
    6.26  
    6.27  
    6.28 @@ -37,15 +47,27 @@
    6.29      end
    6.30  
    6.31  
    6.32 -fun build_tree thy f congs (qs, gs, lhs, rhs) =
    6.33 +fun build_tree thy f congs ctx (qs, gs, lhs, rhs) =
    6.34      let
    6.35  	(* FIXME: Save precomputed dependencies in a theory data slot *)
    6.36  	val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
    6.37 +
    6.38 +        val (_(*FIXME*), ctx') = ProofContext.add_fixes_i (map (fn Free (n, T) => (n, SOME T, NoSyn)) qs) ctx 
    6.39      in
    6.40 -	FundefCtxTree.mk_tree thy congs_deps f rhs
    6.41 +	FundefCtxTree.mk_tree thy congs_deps f ctx' rhs
    6.42      end
    6.43  
    6.44  
    6.45 +fun find_calls tree =
    6.46 +    let
    6.47 +      fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
    6.48 +	| add_Ri _ _ _ _ = raise Match
    6.49 +    in                                 
    6.50 +      rev (FundefCtxTree.traverse_tree add_Ri tree [])
    6.51 +    end
    6.52 +
    6.53 +
    6.54 +
    6.55  (* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
    6.56  fun mk_primed_vars thy glrs =
    6.57      let
    6.58 @@ -63,104 +85,39 @@
    6.59      end
    6.60  
    6.61  
    6.62 -fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs =
    6.63 -    let
    6.64 -	val Names {domT, G, R, h, f, fvar, used, x, ...} = names
    6.65 -				 
    6.66 -	val zv = Var (("z",0), domT) (* for generating h_assums *)
    6.67 -	val xv = Var (("x",0), domT)
    6.68 -	val rw_RI_to_h_assum = (mk_mem (mk_prod (zv, xv), R),
    6.69 -				mk_mem (mk_prod (zv, h $ zv), G))
    6.70 -	val rw_f_to_h = (f, h)
    6.71 -			
    6.72 -	val cqs = map (cterm_of thy) qs
    6.73 -		  
    6.74 -	val vqs = map free_to_var qs
    6.75 -	val cvqs = map (cterm_of thy) vqs
    6.76 -
    6.77 -	val ags = map (assume o cterm_of thy) gs
    6.78 -		  
    6.79 -	val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
    6.80 -	val cqs' = map (cterm_of thy) qs'
    6.81 -
    6.82 -	val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
    6.83 -	val ags' = map (assume o cterm_of thy o rename_vars) gs
    6.84 -	val lhs' = rename_vars lhs
    6.85 -	val rhs' = rename_vars rhs
    6.86 -
    6.87 -	val localize = instantiate ([], cvqs ~~ cqs) 
    6.88 -					   #> fold implies_elim_swp ags
    6.89 -
    6.90 -	val GI = Thm.freezeT GI
    6.91 -	val lGI = localize GI
    6.92 -
    6.93 -	val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [] o var_to_free) (term_vars (prop_of GI))
    6.94 -			  
    6.95 -	fun mk_call_info (RIvs, RI) =
    6.96 -	    let
    6.97 -		fun mk_var0 (v,T) = Var ((v,0),T)
    6.98 -
    6.99 -		val RI = Thm.freezeT RI
   6.100 -		val lRI = localize RI
   6.101 -		val lRIq = fold_rev (forall_intr o cterm_of thy o mk_var0) RIvs lRI
   6.102 -		val plRI = prop_of lRI
   6.103 -		val GmAs = Logic.strip_imp_prems plRI
   6.104 -		val rcarg = case Logic.strip_imp_concl plRI of
   6.105 -				trueprop $ (memb $ (pair $ rcarg $ _) $ R) => rcarg
   6.106 -			      | _ => raise Match
   6.107 -			  
   6.108 -		val Gh_term = Pattern.rewrite_term thy [rw_RI_to_h_assum, rw_f_to_h] [] (prop_of lRIq)
   6.109 -		val Gh = assume (cterm_of thy Gh_term)
   6.110 -		val Gh' = assume (cterm_of thy (rename_vars Gh_term))
   6.111 -	    in
   6.112 -		RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh', GmAs=GmAs, rcarg=rcarg}
   6.113 -	    end
   6.114 -
   6.115 -	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   6.116 -    in
   6.117 -	ClauseInfo
   6.118 -	    {
   6.119 -	     no=no,
   6.120 -	     qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
   6.121 -	     cqs=cqs, cvqs=cvqs, ags=ags,		 
   6.122 -	     cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
   6.123 -	     GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
   6.124 -	     tree=tree, case_hyp = case_hyp
   6.125 -	    }
   6.126 -    end
   6.127 -
   6.128 -
   6.129 -
   6.130  
   6.131  (* Chooses fresh free names, declares G and R, defines f and returns a record
   6.132     with all the information *)  
   6.133 -fun setup_context (f, glrs, used) defname congs thy =
   6.134 +fun setup_context f glrs defname thy =
   6.135      let
   6.136 -	val trees = map (build_tree thy f congs) glrs
   6.137 -	val allused = fold FundefCtxTree.add_context_varnames trees used
   6.138 -
   6.139  	val Const (f_fullname, fT) = f
   6.140  	val fname = Sign.base_name f_fullname
   6.141  
   6.142  	val domT = domain_type fT 
   6.143  	val ranT = range_type fT
   6.144  
   6.145 -	val h = Free (variant allused "h", domT --> ranT)
   6.146 -	val y = Free (variant allused "y", ranT)
   6.147 -	val x = Free (variant allused "x", domT)
   6.148 -	val z = Free (variant allused "z", domT)
   6.149 -	val a = Free (variant allused "a", domT)
   6.150 -	val D = Free (variant allused "D", HOLogic.mk_setT domT)
   6.151 -	val P = Free (variant allused "P", domT --> boolT)
   6.152 -	val Pbool = Free (variant allused "P", boolT)
   6.153 -	val fvarname = variant allused "f"
   6.154 -	val fvar = Free (fvarname, domT --> ranT)
   6.155 -
   6.156  	val GT = mk_relT (domT, ranT)
   6.157  	val RT = mk_relT (domT, domT)
   6.158  	val G_name = defname ^ "_graph"
   6.159  	val R_name = defname ^ "_rel"
   6.160  
   6.161 +        val gfixes = [("h_fd", domT --> ranT),
   6.162 +	              ("y_fd", ranT),
   6.163 +	              ("x_fd", domT),
   6.164 +	              ("z_fd", domT),
   6.165 +	              ("a_fd", domT),
   6.166 +	              ("D_fd", HOLogic.mk_setT domT),
   6.167 +	              ("P_fd", domT --> boolT),
   6.168 +	              ("Pb_fd", boolT),
   6.169 +	              ("f_fd", fT)]
   6.170 +
   6.171 +        val (fxnames, ctx) = (ProofContext.init thy)
   6.172 +                               |> ProofContext.add_fixes_i (map (fn (n,T) => (n, SOME T, NoSyn)) gfixes)
   6.173 +
   6.174 +        val [h, y, x, z, a, D, P, Pbool, fvar] = map (fn (n,(_,T)) => Free (n, T)) (fxnames ~~ gfixes)
   6.175 +                                                                                    
   6.176 +        val Free (fvarname, _) = fvar
   6.177 +
   6.178  	val glrs' = mk_primed_vars thy glrs
   6.179  
   6.180  	val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
   6.181 @@ -175,53 +132,24 @@
   6.182  
   6.183  	val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
   6.184      in
   6.185 -	(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, used=allused, trees=trees}, thy)
   6.186 +	(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)
   6.187      end
   6.188  
   6.189  
   6.190 -(* Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
   6.191 +
   6.192 +
   6.193 +
   6.194 +(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
   6.195  fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
   6.196      (implies $ Trueprop (mk_eq (lhs, lhs'))
   6.197  	     $ Trueprop (mk_eq (rhs, rhs')))
   6.198  	|> fold_rev (curry Logic.mk_implies) (gs @ gs')
   6.199 -
   6.200 +        |> fold_rev mk_forall (qs @ qs')
   6.201  
   6.202  (* all proof obligations *)
   6.203  fun mk_compat_proof_obligations glrs glrs' =
   6.204 -    map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (upairs (glrs ~~ glrs'))
   6.205 -
   6.206 -
   6.207 -fun extract_Ris thy congs f R tree (qs, gs, lhs, rhs) =
   6.208 -    let
   6.209 -	fun add_Ri2 (fixes,assumes) (_ $ arg) _ (_, x) = ([], (FundefCtxTree.export_term (fixes, map prop_of assumes) (mk_relmem (arg, lhs) R)) :: x)
   6.210 -	  | add_Ri2 _ _ _ _ = raise Match
   6.211 -
   6.212 -	val preRis = rev (FundefCtxTree.traverse_tree add_Ri2 tree [])
   6.213 -	val (vRis, preRis_unq) = split_list (map dest_all_all preRis)
   6.214 -
   6.215 -	val Ris = map (fold_rev (curry Logic.mk_implies) gs) preRis_unq
   6.216 -    in
   6.217 -	(map (map dest_Free) vRis, preRis, Ris)
   6.218 -    end
   6.219 +    map (fn ((x,_), (_,y')) => mk_compat_impl (x,y')) (unordered_pairs (glrs ~~ glrs'))
   6.220  
   6.221 -fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
   6.222 -    let
   6.223 -	val Names { domT, R, G, f, fvar, h, y, Pbool, ... } = names
   6.224 -
   6.225 -	val z = Var (("z",0), domT)
   6.226 -	val x = Var (("x",0), domT)
   6.227 -
   6.228 -	val rew1 = (mk_mem (mk_prod (z, x), R),
   6.229 -		    mk_mem (mk_prod (z, fvar $ z), G))
   6.230 -	val rew2 = (f, fvar)
   6.231 -
   6.232 -	val prems = map (Pattern.rewrite_term thy [rew1, rew2] []) Ris
   6.233 -	val rhs' = Pattern.rewrite_term thy [rew2] [] rhs 
   6.234 -    in
   6.235 -	mk_relmem (lhs, rhs') G
   6.236 -		  |> fold_rev (curry Logic.mk_implies) prems
   6.237 -		  |> fold_rev (curry Logic.mk_implies) gs
   6.238 -    end
   6.239  
   6.240  fun mk_completeness names glrs =
   6.241      let
   6.242 @@ -234,61 +162,411 @@
   6.243      in
   6.244  	Trueprop Pbool
   6.245  		 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
   6.246 +                 |> mk_forall_rename (x, "x")
   6.247 +                 |> mk_forall_rename (Pbool, "P")
   6.248      end
   6.249  
   6.250  
   6.251 -fun extract_conditions thy names trees congs =
   6.252 -    let
   6.253 -	val Names {f, R, glrs, glrs', ...} = names
   6.254 +fun inductive_def_wrap defs (thy, const) = 
   6.255 +    let 
   6.256 +      val qdefs = map dest_all_all defs
   6.257  
   6.258 -	val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
   6.259 -	val Gis = map2 (mk_GIntro thy names) glrs preRiss
   6.260 -	val complete = mk_completeness names glrs
   6.261 -	val compat = mk_compat_proof_obligations glrs glrs'
   6.262 -    in
   6.263 -	{G_intros = Gis, vRiss = vRiss, R_intross = Riss, complete = complete, compat = compat}
   6.264 -    end
   6.265 -
   6.266 -
   6.267 -fun inductive_def defs (thy, const) =
   6.268 -    let
   6.269 - 	val (thy, {intrs, elims = [elim], ...}) = 
   6.270 -	    InductivePackage.add_inductive_i true (*verbose*)
   6.271 +      val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) = 
   6.272 +	  InductivePackage.add_inductive_i true (*verbose*)
   6.273  					     false (*add_consts*)
   6.274  					     "" (* no altname *)
   6.275  					     false (* no coind *)
   6.276  					     false (* elims, please *)
   6.277  					     false (* induction thm please *)
   6.278  					     [const] (* the constant *)
   6.279 -					     (map (fn t=>(("", t),[])) defs) (* the intros *)
   6.280 +					     (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *)
   6.281  					     [] (* no special monos *)
   6.282  					     thy
   6.283 +
   6.284 +(* It would be nice if this worked... But this is actually HO-Unification... *)
   6.285 +(*      fun inst (qs, intr) intr_gen =
   6.286 +          Goal.init (cterm_of thy intr)
   6.287 +                    |> curry op COMP intr_gen
   6.288 +                    |> Goal.finish
   6.289 +                    |> fold_rev (forall_intr o cterm_of thy) qs*)
   6.290 +
   6.291 +      fun inst (qs, intr) intr_gen =
   6.292 +          intr_gen 
   6.293 +            |> Thm.freezeT
   6.294 +            |> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs
   6.295 +
   6.296 +      val intrs = map2 inst qdefs intrs_gen
   6.297 +      val elim = elim_gen
   6.298 +                   |> Thm.freezeT
   6.299 +                   |> forall_intr_vars (* FIXME *)
   6.300      in
   6.301 -	(intrs, (thy, elim))
   6.302 +      (intrs, (thy, const, elim))
   6.303 +    end
   6.304 +
   6.305 +
   6.306 +
   6.307 +
   6.308 +
   6.309 +(*
   6.310 + * "!!qs xs. CS ==> G => (r, lhs) : R" 
   6.311 + *)
   6.312 +fun mk_RIntro R (qs, gs, lhs, rhs) (rcfix, rcassm, rcarg) =
   6.313 +    mk_relmem (rcarg, lhs) R 
   6.314 +              |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   6.315 +              |> fold_rev (curry Logic.mk_implies) gs
   6.316 +              |> fold_rev (mk_forall o Free) rcfix
   6.317 +              |> fold_rev mk_forall qs
   6.318 +
   6.319 +
   6.320 +fun mk_GIntro thy f_const f_var G (qs, gs, lhs, rhs) RCs =
   6.321 +    let
   6.322 +      fun mk_h_assm (rcfix, rcassm, rcarg) =
   6.323 +          mk_relmem (rcarg, f_var $ rcarg) G
   6.324 +                    |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   6.325 +                    |> fold_rev (mk_forall o Free) rcfix
   6.326 +    in
   6.327 +      mk_relmem (lhs, rhs) G
   6.328 +                |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
   6.329 +                |> fold_rev (curry Logic.mk_implies) gs
   6.330 +                |> Pattern.rewrite_term thy [(f_const, f_var)] []
   6.331 +                |> fold_rev mk_forall (f_var :: qs)
   6.332 +    end
   6.333 +
   6.334 +
   6.335 +
   6.336 +fun mk_clause_info thy names no (qs,gs,lhs,rhs) tree RCs GIntro_thm RIntro_thms =
   6.337 +    let
   6.338 +	val Names {G, h, f, fvar, x, ...} = names 
   6.339 +				 
   6.340 +	val cqs = map (cterm_of thy) qs
   6.341 +	val ags = map (assume o cterm_of thy) gs
   6.342 +
   6.343 +        val used = [] (* XXX *)
   6.344 +                  (* FIXME: What is the relationship between this and mk_primed_vars? *)
   6.345 +	val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
   6.346 +	val cqs' = map (cterm_of thy) qs'
   6.347 +
   6.348 +	val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
   6.349 +	val ags' = map (assume o cterm_of thy o rename_vars) gs
   6.350 +	val lhs' = rename_vars lhs
   6.351 +	val rhs' = rename_vars rhs
   6.352 +
   6.353 +        val lGI = GIntro_thm
   6.354 +                    |> forall_elim (cterm_of thy f)
   6.355 +                    |> fold forall_elim cqs
   6.356 +                    |> fold implies_elim_swp ags
   6.357 +		
   6.358 +        (* FIXME: Can be removed when inductive-package behaves nicely. *)
   6.359 +        val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) []) 
   6.360 +                          (term_frees (snd (dest_all_all (prop_of GIntro_thm))))
   6.361 +               	  
   6.362 +	fun mk_call_info (rcfix, rcassm, rcarg) RI =
   6.363 +	    let
   6.364 +                val crcfix = map (cterm_of thy o Free) rcfix
   6.365 +
   6.366 +                val llRI = RI
   6.367 +                             |> fold forall_elim cqs
   6.368 +                             |> fold forall_elim crcfix
   6.369 +                             |> fold implies_elim_swp ags
   6.370 +                             |> fold implies_elim_swp rcassm
   6.371 +
   6.372 +                val h_assum = 
   6.373 +                    mk_relmem (rcarg, h $ rcarg) G
   6.374 +                              |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
   6.375 +                              |> fold_rev (mk_forall o Free) rcfix
   6.376 +                              |> Pattern.rewrite_term thy [(f, h)] []
   6.377 +
   6.378 +		val Gh = assume (cterm_of thy h_assum)
   6.379 +		val Gh' = assume (cterm_of thy (rename_vars h_assum))
   6.380 +	    in
   6.381 +		RCInfo {RIvs=rcfix, Gh=Gh, Gh'=Gh', rcarg=rcarg, CCas=rcassm, llRI=llRI}
   6.382 +	    end
   6.383 +
   6.384 +	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
   6.385 +
   6.386 +        val RC_infos = map2 mk_call_info RCs RIntro_thms
   6.387 +    in
   6.388 +	ClauseInfo
   6.389 +	    {
   6.390 +	     no=no,
   6.391 +	     qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
   6.392 +	     cqs=cqs, ags=ags,		 
   6.393 +	     cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', 
   6.394 +	     lGI=lGI, RCs=RC_infos,
   6.395 +	     tree=tree, case_hyp = case_hyp,
   6.396 +             ordcqs'=ordcqs'
   6.397 +	    }
   6.398 +    end
   6.399 +
   6.400 +
   6.401 +
   6.402 +
   6.403 +
   6.404 +(* Copied from fundef_proof.ML: *)
   6.405 +
   6.406 +(***********************************************)
   6.407 +(* Compat thms are stored in normal form (with vars) *)
   6.408 +
   6.409 +(* replace this by a table later*)
   6.410 +fun store_compat_thms 0 thms = []
   6.411 +  | store_compat_thms n thms =
   6.412 +    let
   6.413 +	val (thms1, thms2) = chop n thms
   6.414 +    in
   6.415 +	(thms1 :: store_compat_thms (n - 1) thms2)
   6.416 +    end
   6.417 +
   6.418 +
   6.419 +(* needs i <= j *)
   6.420 +fun lookup_compat_thm i j cts =
   6.421 +    nth (nth cts (i - 1)) (j - i)
   6.422 +(***********************************************)
   6.423 +
   6.424 +
   6.425 +(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
   6.426 +(* if j < i, then turn around *)
   6.427 +fun get_compat_thm thy cts clausei clausej =
   6.428 +    let 
   6.429 +	val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
   6.430 +	val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
   6.431 +
   6.432 +	val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
   6.433 +    in if j < i then
   6.434 +	   let 
   6.435 +	       val compat = lookup_compat_thm j i cts
   6.436 +	   in
   6.437 +	       compat         (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
   6.438 +                |> fold forall_elim (qsj' @ qsi) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *)
   6.439 +		|> fold implies_elim_swp gsj'
   6.440 +		|> fold implies_elim_swp gsi
   6.441 +		|> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
   6.442 +	   end
   6.443 +       else
   6.444 +	   let
   6.445 +	       val compat = lookup_compat_thm i j cts
   6.446 +	   in
   6.447 +	       compat        (* "!!qi qj'. Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
   6.448 +                 |> fold forall_elim (qsi @ qsj') (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
   6.449 +		 |> fold implies_elim_swp gsi
   6.450 +		 |> fold implies_elim_swp gsj'
   6.451 +		 |> implies_elim_swp (assume lhsi_eq_lhsj')
   6.452 +		 |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
   6.453 +	   end
   6.454      end
   6.455  
   6.456  
   6.457  
   6.458 +(* Generates the replacement lemma with primed variables. A problem here is that one should not do
   6.459 +the complete requantification at the end to replace the variables. One should find a way to be more efficient
   6.460 +here. *)
   6.461 +fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = 
   6.462 +    let 
   6.463 +	val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
   6.464 +	val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
   6.465 +
   6.466 +	val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
   6.467 +
   6.468 +	val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
   6.469 +	val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
   6.470 +	val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
   6.471 +
   6.472 +	val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
   6.473 +
   6.474 +	val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
   6.475 +
   6.476 +	val replace_lemma = (eql RS meta_eq_to_obj_eq)
   6.477 +				|> implies_intr (cprop_of case_hyp)
   6.478 +				|> fold_rev (implies_intr o cprop_of) h_assums
   6.479 +				|> fold_rev (implies_intr o cprop_of) ags
   6.480 +				|> fold_rev forall_intr cqs
   6.481 +				|> fold forall_elim cqs'
   6.482 +				|> fold implies_elim_swp ags'
   6.483 +				|> fold implies_elim_swp h_assums'
   6.484 +    in
   6.485 +      replace_lemma
   6.486 +    end
   6.487 +
   6.488 +
   6.489 +
   6.490 +
   6.491 +fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
   6.492 +    let
   6.493 +	val Names {f, h, y, ...} = names
   6.494 +	val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
   6.495 +	val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
   6.496 +
   6.497 +	val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
   6.498 +	val compat = get_compat_thm thy compat_store clausei clausej
   6.499 +	val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
   6.500 +
   6.501 +	val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
   6.502 +	val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j'	*)
   6.503 +
   6.504 +	val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
   6.505 +    in
   6.506 +	(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
   6.507 +        |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
   6.508 +	|> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
   6.509 +	|> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
   6.510 +	|> implies_intr (cprop_of y_eq_rhsj'h)
   6.511 +	|> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
   6.512 +	|> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
   6.513 +	|> implies_elim_swp eq_pairs
   6.514 +	|> fold_rev (implies_intr o cprop_of) Ghsj' 
   6.515 +	|> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
   6.516 +	|> implies_intr (cprop_of eq_pairs)
   6.517 +	|> fold_rev forall_intr ordcqs'j
   6.518 +    end
   6.519 +
   6.520 +
   6.521 +
   6.522 +fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
   6.523 +    let
   6.524 +	val Names {x, y, G, fvar, f, ranT, ...} = names
   6.525 +	val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
   6.526 +
   6.527 +	val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
   6.528 +
   6.529 +	fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
   6.530 +                                                            |> fold_rev (implies_intr o cprop_of) CCas
   6.531 +						            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   6.532 +
   6.533 +	val existence = lGI (*|> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])*)
   6.534 +			    |> fold (curry op COMP o prep_RC) RCs 
   6.535 +
   6.536 +	val a = cterm_of thy (mk_prod (lhs, y))
   6.537 +	val P = cterm_of thy (mk_eq (y, rhs))
   6.538 +	val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
   6.539 +
   6.540 +	val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
   6.541 +
   6.542 +	val uniqueness = G_cases 
   6.543 +                           |> forall_elim a
   6.544 +                           |> forall_elim P
   6.545 +			   |> implies_elim_swp a_in_G
   6.546 +			   |> fold implies_elim_swp unique_clauses
   6.547 +			   |> implies_intr (cprop_of a_in_G)
   6.548 +			   |> forall_intr (cterm_of thy y) 
   6.549 +
   6.550 +	val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
   6.551 +
   6.552 +	val exactly_one =
   6.553 +	    ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
   6.554 +		 |> curry (op COMP) existence
   6.555 +		 |> curry (op COMP) uniqueness
   6.556 +		 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
   6.557 +		 |> implies_intr (cprop_of case_hyp) 
   6.558 +		 |> fold_rev (implies_intr o cprop_of) ags
   6.559 +		 |> fold_rev forall_intr cqs
   6.560 +
   6.561 +	val function_value =
   6.562 +	    existence 
   6.563 +		|> fold_rev (implies_intr o cprop_of) ags
   6.564 +		|> implies_intr ihyp
   6.565 +		|> implies_intr (cprop_of case_hyp)
   6.566 +		|> forall_intr (cterm_of thy x)
   6.567 +		|> forall_elim (cterm_of thy lhs)
   6.568 +		|> curry (op RS) refl
   6.569 +    in
   6.570 +	(exactly_one, function_value)
   6.571 +    end
   6.572 +
   6.573 +
   6.574 +
   6.575 +
   6.576 +fun prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim =
   6.577 +    let
   6.578 +	val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, Pbool, ...}:naming_context = names
   6.579 +
   6.580 +	val f_def_fr = Thm.freezeT f_def
   6.581 +
   6.582 +	val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] 
   6.583 +						[SOME (cterm_of thy f), SOME (cterm_of thy G)])
   6.584 +				      #> curry op COMP (forall_intr_vars f_def_fr)
   6.585 +			  
   6.586 +	val inst_ex1_ex = instantiate_and_def ex1_implies_ex
   6.587 +	val inst_ex1_un = instantiate_and_def ex1_implies_un
   6.588 +	val inst_ex1_iff = instantiate_and_def ex1_implies_iff
   6.589 +
   6.590 +	(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   6.591 +	val ihyp = all domT $ Abs ("z", domT, 
   6.592 +				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
   6.593 +					   $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
   6.594 +							     Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
   6.595 +		       |> cterm_of thy
   6.596 +		   
   6.597 +	val ihyp_thm = assume ihyp |> forall_elim_vars 0
   6.598 +	val ih_intro = ihyp_thm RS inst_ex1_ex
   6.599 +	val ih_elim = ihyp_thm RS inst_ex1_un
   6.600 +
   6.601 +	val _ = Output.debug "Proving Replacement lemmas..."
   6.602 +	val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
   6.603 +
   6.604 +	val _ = Output.debug "Proving cases for unique existence..."
   6.605 +	val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
   6.606 +
   6.607 +	val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *)
   6.608 +	val graph_is_function = complete 
   6.609 +                                  |> forall_elim_vars 0
   6.610 +				  |> fold (curry op COMP) ex1s
   6.611 +				  |> implies_intr (ihyp)
   6.612 +				  |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
   6.613 +				  |> forall_intr (cterm_of thy x)
   6.614 +				  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   6.615 +                                  |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
   6.616 +				  |> Drule.close_derivation
   6.617 +
   6.618 +        val goal = complete COMP (graph_is_function COMP conjunctionI)
   6.619 +                            |> Drule.close_derivation
   6.620 +
   6.621 +        val goalI = Goal.protect goal
   6.622 +                                 |> fold_rev (implies_intr o cprop_of) compat
   6.623 +                                 |> implies_intr (cprop_of complete)
   6.624 +    in
   6.625 +      (prop_of goal, goalI, inst_ex1_iff, values)
   6.626 +    end
   6.627 +
   6.628 +
   6.629 +
   6.630 +
   6.631 +
   6.632  (*
   6.633   * This is the first step in a function definition.
   6.634   *
   6.635   * Defines the function, the graph and the termination relation, synthesizes completeness
   6.636   * and comatibility conditions and returns everything.
   6.637   *)
   6.638 -fun prepare_fundef thy congs defname f glrs used =
   6.639 +fun prepare_fundef thy congs defname f qglrs used =
   6.640      let
   6.641 -	val (names, thy) = setup_context (f, glrs, used) defname congs thy
   6.642 -	val Names {G, R, glrs, trees, ...} = names
   6.643 +      val (names, thy) = setup_context f qglrs defname thy
   6.644 +      val Names {G, R, ctx, glrs', fvar, ...} = names 
   6.645  
   6.646 -	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
   6.647 +                         
   6.648 +      val n = length qglrs
   6.649 +      val trees = map (build_tree thy f congs ctx) qglrs
   6.650 +      val RCss = map find_calls trees
   6.651 +
   6.652 +      val complete = mk_completeness names qglrs
   6.653 +                                     |> cterm_of thy
   6.654 +                                     |> assume
   6.655  
   6.656 -	val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G)
   6.657 -	val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R)
   6.658 +      val compat = mk_compat_proof_obligations qglrs glrs'
   6.659 +                           |> map (assume o cterm_of thy)
   6.660 +
   6.661 +      val compat_store = compat
   6.662 +                           |> store_compat_thms n
   6.663  
   6.664 -	val n = length glrs
   6.665 -	val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
   6.666 +      val R_intross = map2 (fn qglr => map (mk_RIntro R qglr)) qglrs RCss
   6.667 +      val G_intros = map2 (mk_GIntro thy f fvar G) qglrs RCss
   6.668 +                    
   6.669 +      val (GIntro_thms, (thy, _, G_elim)) = inductive_def_wrap G_intros (thy, G)
   6.670 +      val (RIntro_thmss, (thy, _, R_elim)) = fold_burrow inductive_def_wrap R_intross (thy, R)
   6.671 + 
   6.672 +      val clauses = map6 (mk_clause_info thy names) (1 upto n) qglrs trees RCss GIntro_thms RIntro_thmss
   6.673 +                  
   6.674 +      val (goal, goalI, ex1_iff, values) = prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim
   6.675      in
   6.676 -	(Prep {names = names, complete=complete, compat=compat, clauses = clauses},
   6.677 +	(Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim},
   6.678  	 thy) 
   6.679      end
   6.680  
     7.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Mon Jun 19 18:02:49 2006 +0200
     7.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Mon Jun 19 18:25:34 2006 +0200
     7.3 @@ -10,8 +10,8 @@
     7.4  signature FUNDEF_PROOF =
     7.5  sig
     7.6  
     7.7 -    val mk_partial_rules : theory -> thm list -> FundefCommon.prep_result 
     7.8 -			   -> thm -> thm list -> FundefCommon.fundef_result
     7.9 +    val mk_partial_rules : theory -> FundefCommon.prep_result 
    7.10 +			   -> thm -> FundefCommon.fundef_result
    7.11  end
    7.12  
    7.13  
    7.14 @@ -37,8 +37,8 @@
    7.15  val ex1_implies_iff = thm "fundef_ex1_iff"
    7.16  val acc_subset_induct = thm "acc_subset_induct"
    7.17  
    7.18 -
    7.19 -
    7.20 +val conjunctionD1 = thm "conjunctionD1"
    7.21 +val conjunctionD2 = thm "conjunctionD2"
    7.22  
    7.23  
    7.24      
    7.25 @@ -56,10 +56,6 @@
    7.26  	    |> (fn it => it COMP valthm)
    7.27  	    |> implies_intr lhs_acc 
    7.28  	    |> asm_simplify (HOL_basic_ss addsimps [f_iff])
    7.29 -(*	    |> fold forall_intr cqs
    7.30 -	    |> forall_elim_vars 0
    7.31 -	    |> varifyT
    7.32 -	    |> Drule.close_derivation*)
    7.33      end
    7.34  
    7.35  
    7.36 @@ -88,7 +84,7 @@
    7.37  					   $ Trueprop (P $ Bound 0))
    7.38  		       |> cterm_of thy
    7.39  
    7.40 -	val aihyp = assume ihyp |> forall_elim_vars 0
    7.41 +	val aihyp = assume ihyp
    7.42  
    7.43  	fun prove_case clause =
    7.44  	    let
    7.45 @@ -98,8 +94,13 @@
    7.46  		val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
    7.47  		val sih = full_simplify replace_x_ss aihyp
    7.48  					
    7.49 -					(* FIXME: Variable order destroyed by forall_intr_vars *)
    7.50 -		val P_recs = map (fn RCInfo {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs   (*  [P rec1, P rec2, ... ]  *)
    7.51 +                fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
    7.52 +                    sih |> forall_elim (cterm_of thy rcarg)
    7.53 +                        |> implies_elim_swp llRI
    7.54 +                        |> fold_rev (implies_intr o cprop_of) CCas
    7.55 +                        |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
    7.56 +
    7.57 +                val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
    7.58  			     
    7.59  		val step = Trueprop (P $ lhs)
    7.60  				    |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
    7.61 @@ -128,6 +129,7 @@
    7.62  	val (cases, steps) = split_list (map prove_case clauses)
    7.63  
    7.64  	val istep =  complete_thm
    7.65 +                       |> forall_elim_vars 0
    7.66  			 |> fold (curry op COMP) cases (*  P x  *)
    7.67  			 |> implies_intr ihyp
    7.68  			 |> implies_intr (cprop_of x_D)
    7.69 @@ -164,8 +166,6 @@
    7.70  
    7.71  
    7.72  
    7.73 -
    7.74 -
    7.75  (***********************************************)
    7.76  (* Compat thms are stored in normal form (with vars) *)
    7.77  
    7.78 @@ -187,7 +187,7 @@
    7.79  
    7.80  (* recover the order of Vars *)
    7.81  fun get_var_order thy clauses =
    7.82 -    map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
    7.83 +    map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (unordered_pairs clauses)
    7.84  
    7.85  
    7.86  (* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
    7.87 @@ -225,6 +225,8 @@
    7.88  
    7.89  
    7.90  
    7.91 +
    7.92 +
    7.93  (* Generates the replacement lemma with primed variables. A problem here is that one should not do
    7.94  the complete requantification at the end to replace the variables. One should find a way to be more efficient
    7.95  here. *)
    7.96 @@ -235,7 +237,7 @@
    7.97  
    7.98  	val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
    7.99  
   7.100 -	val Ris = map (fn RCInfo {lRIq, ...} => lRIq) RCs
   7.101 +	val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
   7.102  	val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
   7.103  	val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
   7.104  
   7.105 @@ -252,7 +254,7 @@
   7.106  				|> fold implies_elim_swp ags'
   7.107  				|> fold implies_elim_swp h_assums'
   7.108      in
   7.109 -	replace_lemma
   7.110 +      replace_lemma
   7.111      end
   7.112  
   7.113  
   7.114 @@ -296,10 +298,9 @@
   7.115  
   7.116  	val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
   7.117  
   7.118 -	fun prep_RC (RCInfo {lRIq,RIvs, ...}) = lRIq
   7.119 -						    |> fold (forall_elim o cterm_of thy o Free) RIvs
   7.120 -						    |> (fn it => it RS ih_intro_case)
   7.121 -						    |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   7.122 +	fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
   7.123 +                                                            |> fold_rev (implies_intr o cprop_of) CCas
   7.124 +						            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   7.125  
   7.126  	val existence = lGI |> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])
   7.127  			    |> fold (curry op COMP o prep_RC) RCs 
   7.128 @@ -353,7 +354,7 @@
   7.129      in
   7.130  	Goal.init goal 
   7.131  		  |> (SINGLE (resolve_tac [accI] 1)) |> the
   7.132 -		  |> (SINGLE (eresolve_tac [R_cases] 1))  |> the
   7.133 +		  |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1))  |> the
   7.134  		  |> (SINGLE (CLASIMPSET auto_tac)) |> the
   7.135  		  |> Goal.conclude
   7.136      end
   7.137 @@ -453,74 +454,32 @@
   7.138  	    |> fold implies_intr hyps
   7.139  	    |> implies_intr wfR'
   7.140  	    |> forall_intr (cterm_of thy R')
   7.141 -	    |> forall_elim_vars 0
   7.142 -	    |> varifyT
   7.143      end
   7.144  
   7.145  
   7.146  
   7.147  
   7.148 -fun mk_partial_rules thy congs data complete_thm compat_thms =
   7.149 +fun mk_partial_rules thy data provedgoal =
   7.150      let
   7.151 -	val Prep {names, clauses, complete, compat, ...} = data
   7.152 +	val Prep {names, clauses, values, R_cases, ex1_iff, ...} = data
   7.153  	val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
   7.154  
   7.155 -(*	val _ = Output.debug "closing derivation: completeness"
   7.156 -	val _ = Output.debug (Proofterm.size_of_proof (proof_of complete_thm))
   7.157 -	val _ = Output.debug (map (Proofterm.size_of_proof o proof_of) compat_thms)*)
   7.158 -	val complete_thm = Drule.close_derivation complete_thm
   7.159 -(*	val _ = Output.debug "closing derivation: compatibility"*)
   7.160 -	val compat_thms = map Drule.close_derivation compat_thms
   7.161 -(*	val _ = Output.debug "  done"*)
   7.162 +        val _ = print "Closing Derivation"
   7.163  
   7.164 -	val complete_thm_fr = Thm.freezeT complete_thm
   7.165 -	val compat_thms_fr = map Thm.freezeT compat_thms
   7.166 -	val f_def_fr = Thm.freezeT f_def
   7.167 +	val provedgoal = Drule.close_derivation provedgoal
   7.168  
   7.169 -	val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] 
   7.170 -						[SOME (cterm_of thy f), SOME (cterm_of thy G)])
   7.171 -				      #> curry op COMP (forall_intr_vars f_def_fr)
   7.172 -			  
   7.173 -	val inst_ex1_ex = instantiate_and_def ex1_implies_ex
   7.174 -	val inst_ex1_un = instantiate_and_def ex1_implies_un
   7.175 -	val inst_ex1_iff = instantiate_and_def ex1_implies_iff
   7.176 +        val _ = print "Getting gif"
   7.177  
   7.178 -	(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
   7.179 -	val ihyp = all domT $ Abs ("z", domT, 
   7.180 -				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
   7.181 -					   $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
   7.182 -							     Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
   7.183 -		       |> cterm_of thy
   7.184 -		   
   7.185 -	val ihyp_thm = assume ihyp
   7.186 -			      |> forall_elim_vars 0
   7.187 -		       
   7.188 -	val ih_intro = ihyp_thm RS inst_ex1_ex
   7.189 -	val ih_elim = ihyp_thm RS inst_ex1_un
   7.190 +        val graph_is_function = (provedgoal COMP conjunctionD1)
   7.191 +                                  |> forall_elim_vars 0
   7.192  
   7.193 -	val _ = Output.debug "Proving Replacement lemmas..."
   7.194 -	val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
   7.195 +        val _ = print "Getting cases"
   7.196  
   7.197 -	val n = length clauses
   7.198 -	val var_order = get_var_order thy clauses
   7.199 -	val compat_store = store_compat_thms n (var_order ~~ compat_thms_fr)
   7.200 -
   7.201 -	val R_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R)))))) |> Thm.freezeT
   7.202 -	val G_cases = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const G)))))) |> Thm.freezeT
   7.203 -
   7.204 -	val _ = Output.debug "Proving cases for unique existence..."
   7.205 -	val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses repLemmas) clauses)
   7.206 +        val complete_thm = provedgoal COMP conjunctionD2
   7.207  
   7.208 -	val _ = Output.debug "Proving: Graph is a function"
   7.209 -	val graph_is_function = complete_thm_fr
   7.210 -				    |> fold (curry op COMP) ex1s
   7.211 -				    |> implies_intr (ihyp)
   7.212 -				    |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
   7.213 -				    |> forall_intr (cterm_of thy x)
   7.214 -				    |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   7.215 -				    |> Drule.close_derivation
   7.216 +        val _ = print "making f_iff"
   7.217  
   7.218 -	val f_iff = (graph_is_function RS inst_ex1_iff)
   7.219 +	val f_iff = (graph_is_function RS ex1_iff) 
   7.220  
   7.221  	val _ = Output.debug "Proving simplification rules"
   7.222  	val psimps  = map2 (mk_psimp thy names f_iff graph_is_function) clauses values
   7.223 @@ -534,7 +493,7 @@
   7.224  	val _ = Output.debug "Proving domain introduction rules"
   7.225  	val dom_intros = map (mk_domain_intro thy names R_cases) clauses
   7.226      in 
   7.227 -	FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
   7.228 +	FundefResult {f=f, G=G, R=R, completeness=complete_thm, 
   7.229  	 psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
   7.230  	 dom_intros=dom_intros}
   7.231      end
     8.1 --- a/src/HOL/Tools/function_package/mutual.ML	Mon Jun 19 18:02:49 2006 +0200
     8.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Mon Jun 19 18:25:34 2006 +0200
     8.3 @@ -14,7 +14,7 @@
     8.4                                (FundefCommon.mutual_info * string * (FundefCommon.prep_result * theory))
     8.5  
     8.6  
     8.7 -  val mk_partial_rules_mutual : theory -> thm list -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> thm list ->
     8.8 +  val mk_partial_rules_mutual : theory -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> 
     8.9                                  FundefCommon.fundef_mresult
    8.10  end
    8.11  
    8.12 @@ -217,10 +217,10 @@
    8.13  
    8.14  
    8.15  
    8.16 -fun mk_partial_rules_mutual thy congs (m as Mutual {qglrss, RST, parts, streeR, ...}) data complete_thm compat_thms =
    8.17 +fun mk_partial_rules_mutual thy (m as Mutual {qglrss, RST, parts, streeR, ...}) data result =
    8.18      let
    8.19 -	val result = FundefProof.mk_partial_rules thy congs data complete_thm compat_thms 
    8.20 -	val FundefResult {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
    8.21 +	val result = FundefProof.mk_partial_rules thy data result
    8.22 +	val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result
    8.23  
    8.24  	val sum_psimps = Library.unflat qglrss psimps
    8.25  
     9.1 --- a/src/HOL/ex/Fundefs.thy	Mon Jun 19 18:02:49 2006 +0200
     9.2 +++ b/src/HOL/ex/Fundefs.thy	Mon Jun 19 18:25:34 2006 +0200
     9.3 @@ -135,8 +135,8 @@
     9.4    "gcd3 0 y = y"
     9.5    "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
     9.6    "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
     9.7 -  apply (cases xa, case_tac a, auto)
     9.8 -  apply (case_tac b, auto)
     9.9 +  apply (case_tac x, case_tac a, auto)
    9.10 +  apply (case_tac ba, auto)
    9.11    done
    9.12  termination 
    9.13    by (auto_term "measure (\<lambda>(x,y). x + y)")
    9.14 @@ -152,6 +152,8 @@
    9.15    "ev (2 * n) = True"
    9.16    "ev (2 * n + 1) = False"
    9.17  proof -  -- {* completeness is more difficult here \dots *}
    9.18 +  fix P :: bool
    9.19 +    and x :: nat
    9.20    assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
    9.21      and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
    9.22    have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto