src/HOL/Tools/function_package/fundef_proof.ML

removed obsolete mem_ix;

(*  Title:      HOL/Tools/function_package/fundef_proof.ML
    ID:         $Id$
    Author:     Alexander Krauss, TU Muenchen

A package for general recursive function definitions. 
Internal proofs.
*)


signature FUNDEF_PROOF =
sig

    val mk_partial_rules : theory -> FundefCommon.prep_result 
			   -> thm -> FundefCommon.fundef_result
end


structure FundefProof : FUNDEF_PROOF = 
struct

open FundefCommon
open FundefAbbrev

(* Theory dependencies *)
val subsetD = thm "subsetD"
val subset_refl = thm "subset_refl"
val split_apply = thm "Product_Type.split"
val wf_induct_rule = thm "wf_induct_rule";
val Pair_inject = thm "Product_Type.Pair_inject";

val acc_induct_rule = thm "acc_induct_rule" (* from: Accessible_Part *)
val acc_downward = thm "acc_downward"
val accI = thm "accI"

val ex1_implies_ex = thm "fundef_ex1_existence"   (* from: Fundef.thy *) 
val ex1_implies_un = thm "fundef_ex1_uniqueness"
val ex1_implies_iff = thm "fundef_ex1_iff"
val acc_subset_induct = thm "acc_subset_induct"

val conjunctionD1 = thm "conjunctionD1"
val conjunctionD2 = thm "conjunctionD2"


    
fun mk_psimp thy names f_iff graph_is_function clause valthm =
    let
	val Names {R, acc_R, domT, z, ...} = names
	val ClauseInfo {qs, cqs, gs, lhs, rhs, ...} = clause
	val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, acc_R))) (* "lhs : acc R" *)
	val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *)
    in
	((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
	    |> (fn it => it COMP graph_is_function)
	    |> implies_intr z_smaller
	    |> forall_intr (cterm_of thy z)
	    |> (fn it => it COMP valthm)
	    |> implies_intr lhs_acc 
	    |> asm_simplify (HOL_basic_ss addsimps [f_iff])
    end




fun mk_partial_induct_rule thy names complete_thm clauses =
    let
	val Names {domT, R, acc_R, x, z, a, P, D, ...} = names

	val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D))))
	val a_D = cterm_of thy (Trueprop (mk_mem (a, D)))

	val D_subset = cterm_of thy (Trueprop (mk_subset domT D acc_R))

	val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
	    mk_forall x
		      (mk_forall z (Logic.mk_implies (Trueprop (mk_mem (x, D)),
						      Logic.mk_implies (mk_relmem (z, x) R,
									Trueprop (mk_mem (z, D))))))
		      |> cterm_of thy


	(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
	val ihyp = all domT $ Abs ("z", domT, 
				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
					   $ Trueprop (P $ Bound 0))
		       |> cterm_of thy

	val aihyp = assume ihyp

	fun prove_case clause =
	    let
		val ClauseInfo {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause
								       
		val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
		val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
		val sih = full_simplify replace_x_ss aihyp
					
                fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
                    sih |> forall_elim (cterm_of thy rcarg)
                        |> implies_elim_swp llRI
                        |> fold_rev (implies_intr o cprop_of) CCas
                        |> fold_rev (forall_intr o cterm_of thy o Free) RIvs

                val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
			     
		val step = Trueprop (P $ lhs)
				    |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
				    |> fold_rev (curry Logic.mk_implies) gs
				    |> curry Logic.mk_implies (Trueprop (mk_mem (lhs, D)))
				    |> fold_rev mk_forall qs
				    |> cterm_of thy
			   
		val P_lhs = assume step
				   |> fold forall_elim cqs
				   |> implies_elim_swp lhs_D 
				   |> fold_rev implies_elim_swp ags
				   |> fold implies_elim_swp P_recs
			    
		val res = cterm_of thy (Trueprop (P $ x))
				   |> Simplifier.rewrite replace_x_ss
				   |> symmetric (* P lhs == P x *)
				   |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
				   |> implies_intr (cprop_of case_hyp)
				   |> fold_rev (implies_intr o cprop_of) ags
				   |> fold_rev forall_intr cqs
	    in
		(res, step)
	    end

	val (cases, steps) = split_list (map prove_case clauses)

	val istep =  complete_thm
                       |> forall_elim_vars 0
			 |> fold (curry op COMP) cases (*  P x  *)
			 |> implies_intr ihyp
			 |> implies_intr (cprop_of x_D)
			 |> forall_intr (cterm_of thy x)
			   
	val subset_induct_rule = 
	    acc_subset_induct
		|> (curry op COMP) (assume D_subset)
		|> (curry op COMP) (assume D_dcl)
		|> (curry op COMP) (assume a_D)
		|> (curry op COMP) istep
		|> fold_rev implies_intr steps
		|> implies_intr a_D
		|> implies_intr D_dcl
		|> implies_intr D_subset

	val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule

	val simple_induct_rule =
	    subset_induct_rule
		|> forall_intr (cterm_of thy D)
		|> forall_elim (cterm_of thy acc_R)
		|> (curry op COMP) subset_refl
		|> (curry op COMP) (acc_downward
					|> (instantiate' [SOME (ctyp_of thy domT)]
							 (map (SOME o cterm_of thy) [x, R, z]))
					|> forall_intr (cterm_of thy z)
					|> forall_intr (cterm_of thy x))
		|> forall_intr (cterm_of thy a)
		|> forall_intr (cterm_of thy P)
    in
	(subset_induct_all, simple_induct_rule)
    end



(***********************************************)
(* Compat thms are stored in normal form (with vars) *)

(* replace this by a table later*)
fun store_compat_thms 0 cts = []
  | store_compat_thms n cts =
    let
	val (cts1, cts2) = chop n cts
    in
	(cts1 :: store_compat_thms (n - 1) cts2)
    end


(* needs i <= j *)
fun lookup_compat_thm i j cts =
    nth (nth cts (i - 1)) (j - i)
(***********************************************)


(* recover the order of Vars *)
fun get_var_order thy clauses =
    map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (unordered_pairs clauses)


(* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
(* if j < i, then turn around *)
fun get_compat_thm thy cts clausei clausej =
    let 
	val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
	val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej

	val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
    in if j < i then
	   let 
	       val (var_ord, compat) = lookup_compat_thm j i cts
	   in
	       compat         (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
		|> instantiate ([],(var_ord ~~ (qsj' @ qsi))) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *)
		|> fold implies_elim_swp gsj'
		|> fold implies_elim_swp gsi
		|> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
	   end
       else
	   let
	       val (var_ord, compat) = lookup_compat_thm i j cts
	   in
	       compat        (* "?Gsi => ?Gsj' => ?lhsi = ?lhsj' ==> ?rhsi = ?rhsj'" *)
	         |> instantiate ([], (var_ord ~~ (qsi @ qsj'))) (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
		 |> fold implies_elim_swp gsi
		 |> fold implies_elim_swp gsj'
		 |> implies_elim_swp (assume lhsi_eq_lhsj')
		 |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
	   end
    end







(* Generates the replacement lemma with primed variables. A problem here is that one should not do
the complete requantification at the end to replace the variables. One should find a way to be more efficient
here. *)
fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = 
    let 
	val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
	val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause

	val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim

	val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
	val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
	val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs

	val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)

	val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree

	val replace_lemma = (eql RS meta_eq_to_obj_eq)
				|> implies_intr (cprop_of case_hyp)
				|> fold_rev (implies_intr o cprop_of) h_assums
				|> fold_rev (implies_intr o cprop_of) ags
				|> fold_rev forall_intr cqs
				|> fold forall_elim cqs'
				|> fold implies_elim_swp ags'
				|> fold implies_elim_swp h_assums'
    in
      replace_lemma
    end




fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
    let
	val Names {f, h, y, ...} = names
	val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
	val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej

	val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
	val compat = get_compat_thm thy compat_store clausei clausej
	val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj

	val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
	val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j'	*)

	val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
    in
	(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
        |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
	|> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
	|> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
	|> implies_intr (cprop_of y_eq_rhsj'h)
	|> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
	|> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
	|> implies_elim_swp eq_pairs
	|> fold_rev (implies_intr o cprop_of) Ghsj' 
	|> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
	|> implies_intr (cprop_of eq_pairs)
	|> fold_rev forall_intr ordcqs'j
    end



fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
    let
	val Names {x, y, G, fvar, f, ranT, ...} = names
	val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei

	val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro

	fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
                                                            |> fold_rev (implies_intr o cprop_of) CCas
						            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs

	val existence = lGI |> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])
			    |> fold (curry op COMP o prep_RC) RCs 


	val a = cterm_of thy (mk_prod (lhs, y))
	val P = cterm_of thy (mk_eq (y, rhs))
	val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))

	val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas

	val uniqueness = G_cases 
			     |> instantiate' [] [SOME a, SOME P]
			     |> implies_elim_swp a_in_G
			     |> fold implies_elim_swp unique_clauses
			     |> implies_intr (cprop_of a_in_G)
			     |> forall_intr (cterm_of thy y) 

	val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)

	val exactly_one =
	    ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
		 |> curry (op COMP) existence
		 |> curry (op COMP) uniqueness
		 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
		 |> implies_intr (cprop_of case_hyp) 
		 |> fold_rev (implies_intr o cprop_of) ags
		 |> fold_rev forall_intr cqs
	val function_value =
	    existence 
		|> fold_rev (implies_intr o cprop_of) ags
		|> implies_intr ihyp
		|> implies_intr (cprop_of case_hyp)
		|> forall_intr (cterm_of thy x)
		|> forall_elim (cterm_of thy lhs)
		|> curry (op RS) refl
    in
	(exactly_one, function_value)
    end



(* Does this work with Guards??? *)
fun mk_domain_intro thy names R_cases clause =
    let
	val Names {z, R, acc_R, ...} = names
	val ClauseInfo {qs, gs, lhs, rhs, ...} = clause
	val goal = (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
                     |> fold_rev (curry Logic.mk_implies) gs
                     |> cterm_of thy
    in
	Goal.init goal 
		  |> (SINGLE (resolve_tac [accI] 1)) |> the
		  |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1))  |> the
		  |> (SINGLE (CLASIMPSET auto_tac)) |> the
		  |> Goal.conclude
    end




fun mk_nest_term_case thy names R' ihyp clause =
    let
	val Names {x, z, ...} = names
	val ClauseInfo {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause

	val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp

	fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = 
	    let
		val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)

		val hyp = mk_relmem (arg, lhs) R'
				    |> fold_rev (curry Logic.mk_implies o prop_of) used
				    |> FundefCtxTree.export_term (fixes, map prop_of assumes) 
				    |> fold_rev (curry Logic.mk_implies o prop_of) ags
				    |> fold_rev mk_forall qs
				    |> cterm_of thy

		val thm = assume hyp
				 |> fold forall_elim cqs
				 |> fold implies_elim_swp ags
				 |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
				 |> fold implies_elim_swp used

		val acc = thm COMP ih_case

		val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))

		val arg_eq_z = (assume z_eq_arg) RS sym

		val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
				     |> implies_intr (cprop_of case_hyp)
				     |> implies_intr z_eq_arg

		val zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs))))

		val z_acc' = (z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject))
                               |> FundefCtxTree.export_thm thy ([], (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes))

                val occvars = fold (OrdList.insert Term.term_ord) (term_frees (prop_of z_acc')) [] 
                val ordvars = fold (OrdList.insert Term.term_ord) (map Free fixes @ qs) [] (* FIXME... remove when inductive behaves nice *)
                                   |> OrdList.inter Term.term_ord occvars

		val ethm = z_acc'
			       |> FundefCtxTree.export_thm thy (map dest_Free ordvars, [])


		val sub' = sub @ [(([],[]), acc)]
	    in
		(sub', (hyp :: hyps, ethm :: thms))
	    end
	  | step _ _ _ _ = raise Match
    in
	FundefCtxTree.traverse_tree step tree
    end


fun mk_nest_term_rule thy names clauses =
    let
	val Names { R, acc_R, domT, x, z, ... } = names

	val R_elim = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R))))))

	val R' = Free ("R", fastype_of R)

	val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wf", mk_relT (domT, domT) --> boolT) $ R')) (* "wf R'" *)

	(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
	val ihyp = all domT $ Abs ("z", domT, 
				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R')
					   $ Trueprop ((Const ("op :", [domT, HOLogic.mk_setT domT] ---> boolT))
							   $ Bound 0 $ acc_R))
		       |> cterm_of thy

	val ihyp_a = assume ihyp |> forall_elim_vars 0

	val z_ltR_x = cterm_of thy (mk_relmem (z, x) R) (* "(z, x) : R" *)
	val z_acc = cterm_of thy (mk_mem (z, acc_R))

	val (hyps,cases) = fold (mk_nest_term_case thy names R' ihyp_a) clauses ([],[])
    in
	R_elim
	    |> Thm.freezeT
	    |> instantiate' [] [SOME (cterm_of thy (mk_prod (z,x))), SOME z_acc]
	    |> curry op COMP (assume z_ltR_x)
	    |> fold_rev (curry op COMP) cases
	    |> implies_intr z_ltR_x
	    |> forall_intr (cterm_of thy z)
	    |> (fn it => it COMP accI)
	    |> implies_intr ihyp
	    |> forall_intr (cterm_of thy x)
	    |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
	    |> implies_elim_swp (assume wfR')
	    |> fold implies_intr hyps
	    |> implies_intr wfR'
	    |> forall_intr (cterm_of thy R')
    end




fun mk_partial_rules thy data provedgoal =
    let
	val Prep {names, clauses, values, R_cases, ex1_iff, ...} = data
	val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names

        val _ = print "Closing Derivation"

	val provedgoal = Drule.close_derivation provedgoal

        val _ = print "Getting gif"

        val graph_is_function = (provedgoal COMP conjunctionD1)
                                  |> forall_elim_vars 0

        val _ = print "Getting cases"

        val complete_thm = provedgoal COMP conjunctionD2

        val _ = print "making f_iff"

	val f_iff = (graph_is_function RS ex1_iff) 

	val _ = Output.debug "Proving simplification rules"
	val psimps  = map2 (mk_psimp thy names f_iff graph_is_function) clauses values

	val _ = Output.debug "Proving partial induction rule"
	val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy names complete_thm clauses

	val _ = Output.debug "Proving nested termination rule"
	val total_intro = mk_nest_term_rule thy names clauses

	val _ = Output.debug "Proving domain introduction rules"
	val dom_intros = map (mk_domain_intro thy names R_cases) clauses
    in 
	FundefResult {f=f, G=G, R=R, completeness=complete_thm, 
	 psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
	 dom_intros=dom_intros}
    end


end