src/HOL/Tools/function_package/fundef_proof.ML

Fixed bug in the handling of congruence rules

(*  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 FundefLib
open FundefCommon
open FundefAbbrev

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

val wf_in_rel = thm "FunDef.wf_in_rel";
val in_rel_def = thm "FunDef.in_rel_def";

val acc_induct_rule = thm "FunDef.accP_induct_rule"
val acc_downward = thm "FunDef.accP_downward"
val accI = thm "FunDef.accPI"

val acc_subset_induct = thm "FunDef.accP_subset_induct"

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


fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
    let
	val Globals {domT, z, ...} = globals

	val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
	val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
	val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
    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])
          |> fold_rev (implies_intr o cprop_of) ags
          |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
    end



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

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

	val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))

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


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

	val aihyp = assume ihyp

	fun prove_case clause =
	    let
		val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs, 
                                qglr = (oqs, _, _, _), ...} = 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 (D $ lhs))
				    |> fold_rev mk_forall_rename (map fst oqs ~~ 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)
		|> assume_tac 1 |> Seq.hd
		|> (curry op COMP) (acc_downward
					|> (instantiate' [SOME (ctyp_of thy domT)]
							 (map (SOME o cterm_of thy) [R, x, 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



(* Does this work with Guards??? *)
fun mk_domain_intro thy globals R R_cases clause =
    let
	val Globals {z, domT, ...} = globals
	val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, 
                        qglr = (oqs, _, _, _), ...} = clause
	val goal = Trueprop (mk_acc domT R $ lhs)
                     |> 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
                  |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
    end




fun mk_nest_term_case thy globals R' ihyp clause =
    let
	val Globals {x, z, ...} = globals
	val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
                        qglr=(oqs, _, _, _), ...} = 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 = Trueprop (R' $ arg $ lhs)
				    |> 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_rename (map fst oqs ~~ 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 z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
                val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))

		val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
			       |> FundefCtxTree.export_thm thy (fixes, 
                                                                prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
                               |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)

		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 globals R R_cases clauses =
    let
	val Globals { domT, x, z, ... } = globals
        val acc_R = mk_acc domT R

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

        val Rrel = Free ("R", mk_relT (domT, domT))
        val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel

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

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

	val ihyp_a = assume ihyp |> forall_elim_vars 0

	val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) 

	val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
    in
	R_cases
            |> forall_elim (cterm_of thy z)
            |> forall_elim (cterm_of thy x)
            |> forall_elim (cterm_of thy (acc_R $ z))
	    |> curry op COMP (assume R_z_x)
	    |> fold_rev (curry op COMP) cases
	    |> implies_intr R_z_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))
	    |> curry op RS (assume wfR')
	    |> fold implies_intr hyps
	    |> implies_intr wfR'
	    |> forall_intr (cterm_of thy R')
            |> forall_elim (cterm_of thy (inrel_R))
            |> curry op RS wf_in_rel
            |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
	    |> forall_intr (cterm_of thy Rrel)
    end




fun mk_partial_rules thy data provedgoal =
    let
	val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data

        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 globals R f_iff graph_is_function) clauses values

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

	val _ = Output.debug "Proving nested termination rule"
	val total_intro = mk_nest_term_rule thy globals R R_cases clauses

	val _ = Output.debug "Proving domain introduction rules"
	val dom_intros = map (mk_domain_intro thy globals R 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