src/HOL/Tools/function_package/fundef_package.ML
changeset 19564 d3e2f532459a
child 19583 c5fa77b03442
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri May 05 17:17:21 2006 +0200
     1.3 @@ -0,0 +1,197 @@
     1.4 +(*  Title:      HOL/Tools/function_package/fundef_package.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Alexander Krauss, TU Muenchen
     1.7 +
     1.8 +A package for general recursive function definitions. 
     1.9 +Isar commands.
    1.10 +
    1.11 +*)
    1.12 +
    1.13 +signature FUNDEF_PACKAGE = 
    1.14 +sig
    1.15 +    val add_fundef : ((bstring * Attrib.src list) * string) list -> theory -> Proof.state (* Need an _i variant *)
    1.16 +
    1.17 +    val cong_add: attribute
    1.18 +    val cong_del: attribute
    1.19 +							 
    1.20 +    val setup : theory -> theory
    1.21 +end
    1.22 +
    1.23 +
    1.24 +structure FundefPackage : FUNDEF_PACKAGE =
    1.25 +struct
    1.26 +
    1.27 +open FundefCommon
    1.28 +
    1.29 +val True_implies = thm "True_implies"
    1.30 +
    1.31 +
    1.32 +(*#> FundefTermination.setup #> FundefDatatype.setup*)
    1.33 +
    1.34 +fun fundef_afterqed congs curry_info name data natts thmss thy =
    1.35 +    let
    1.36 +	val (complete_thm :: compat_thms) = map hd thmss
    1.37 +	val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
    1.38 +	val {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
    1.39 +
    1.40 +	val (names, attsrcs) = split_list natts
    1.41 +	val atts = map (map (Attrib.attribute thy)) attsrcs
    1.42 +
    1.43 +	val accR = (#acc_R(#names(data)))
    1.44 +	val dom_abbrev = Logic.mk_equals (Free ("dom", fastype_of accR), accR)
    1.45 +
    1.46 +	val thy = thy |> Theory.add_path name 
    1.47 +
    1.48 +	val thy = thy |> Theory.add_path "psimps"
    1.49 +	val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy;
    1.50 +	val thy = thy |> Theory.parent_path
    1.51 +
    1.52 +	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    1.53 +	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy
    1.54 +	val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy
    1.55 +	val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy
    1.56 +	val (_,thy) = PureThy.add_thms [(("pinduct", simple_pinduct), [RuleCases.case_names names, InductAttrib.induct_set ""])] thy
    1.57 +	val (_, thy) = PureThy.add_thmss [(("psimps", psimps), [Simplifier.simp_add])] thy
    1.58 +	val thy = thy |> Theory.parent_path
    1.59 +    in
    1.60 +	add_fundef_data name fundef_data thy
    1.61 +    end
    1.62 +
    1.63 +fun add_fundef eqns_atts thy =
    1.64 +    let
    1.65 +	val (natts, eqns) = split_list eqns_atts
    1.66 +
    1.67 +	val congs = get_fundef_congs (Context.Theory thy)
    1.68 +
    1.69 +	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs (map (Sign.read_prop thy) eqns) thy
    1.70 +	val {complete, compat, ...} = data
    1.71 +
    1.72 +	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
    1.73 +    in
    1.74 +	thy |> ProofContext.init
    1.75 +	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data natts) NONE ("", [])
    1.76 +	    (map (fn t => (("", []), [(t, ([], []))])) props)
    1.77 +    end
    1.78 +
    1.79 +
    1.80 +fun total_termination_afterqed name thmss thy =
    1.81 +    let
    1.82 +	val totality = hd (hd thmss)
    1.83 +
    1.84 +	val {psimps, simple_pinduct, ... }
    1.85 +	  = the (get_fundef_data name thy)
    1.86 +
    1.87 +	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
    1.88 +
    1.89 +	val tsimps = map remove_domain_condition psimps
    1.90 +	val tinduct = remove_domain_condition simple_pinduct
    1.91 +
    1.92 +	val thy = Theory.add_path name thy
    1.93 +		  
    1.94 +		  (* Need the names and attributes. Apply the attributes again? *)
    1.95 +(*	val thy = thy |> Theory.add_path "simps"
    1.96 +	val (_, thy) = PureThy.add_thms ((names ~~ tsimps) ~~ atts) thy;
    1.97 +	val thy = thy |> Theory.parent_path*)
    1.98 +
    1.99 +	val (_, thy) = PureThy.add_thms [(("induct", tinduct), [])] thy 
   1.100 +	val (_, thy) = PureThy.add_thmss [(("simps", tsimps), [Simplifier.simp_add, RecfunCodegen.add NONE])] thy
   1.101 +	val thy = Theory.parent_path thy
   1.102 +    in
   1.103 +	thy
   1.104 +    end
   1.105 +
   1.106 +(*
   1.107 +fun mk_partial_rules name D_name D domT idomT thmss thy =
   1.108 +    let
   1.109 +	val [subs, dcl] = (hd thmss)
   1.110 +
   1.111 +	val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
   1.112 +	  = the (Symtab.lookup (FundefData.get thy) name)
   1.113 +
   1.114 +	val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] 
   1.115 +						    [SOME (cterm_of thy D)]
   1.116 +						    subsetD)
   1.117 +
   1.118 +	val D_simps = map (curry op RS D_implies_dom) f_simps
   1.119 +
   1.120 +	val D_induct = subset_induct
   1.121 +			   |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
   1.122 +			   |> curry op COMP subs
   1.123 +			   |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
   1.124 +						 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
   1.125 +
   1.126 +	val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
   1.127 +	val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
   1.128 +    in
   1.129 +	thy3
   1.130 +    end
   1.131 +*)
   1.132 + 
   1.133 +
   1.134 +fun fundef_setup_termination_proof name NONE thy = 
   1.135 +    let
   1.136 +	val name = if name = "" then get_last_fundef thy else name
   1.137 +	val data = the (get_fundef_data name thy)
   1.138 +
   1.139 +	val {total_intro, ...} = data
   1.140 +	val goal = FundefTermination.mk_total_termination_goal data
   1.141 +    in
   1.142 +	thy |> ProofContext.init
   1.143 +	    |> ProofContext.note_thmss_i [(("termination_intro", 
   1.144 +					    [ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd
   1.145 +	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", [])
   1.146 +	    [(("", []), [(goal, ([], []))])]
   1.147 +    end	
   1.148 +  | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
   1.149 +    let
   1.150 +	val name = if name = "" then get_last_fundef thy else name
   1.151 +	val data = the (get_fundef_data name thy)
   1.152 +	val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
   1.153 +    in
   1.154 +	thy |> ProofContext.init
   1.155 +	    |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
   1.156 +	    [(("", []), [(subs, ([], [])), (dcl, ([], []))])]
   1.157 +    end	
   1.158 +
   1.159 +
   1.160 +
   1.161 +
   1.162 +(* congruence rules *)
   1.163 +
   1.164 +val cong_add = Thm.declaration_attribute (map_fundef_congs o cons o safe_mk_meta_eq);
   1.165 +val cong_del = Thm.declaration_attribute (map_fundef_congs o remove (op =) o safe_mk_meta_eq);
   1.166 +
   1.167 +
   1.168 +(* setup *)
   1.169 +
   1.170 +val setup = FundefData.init #> FundefCongs.init 
   1.171 +	#>  Attrib.add_attributes
   1.172 +		[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
   1.173 +
   1.174 +
   1.175 +(* outer syntax *)
   1.176 +
   1.177 +local structure P = OuterParse and K = OuterKeyword in
   1.178 +
   1.179 +val function_decl =
   1.180 +    Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
   1.181 +
   1.182 +val functionP =
   1.183 +  OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   1.184 +    (function_decl >> (fn eqns =>
   1.185 +      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqns)));
   1.186 +
   1.187 +val terminationP =
   1.188 +  OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   1.189 +  ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
   1.190 +       >> (fn (name,dom) =>
   1.191 +	      Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
   1.192 +
   1.193 +val _ = OuterSyntax.add_parsers [functionP];
   1.194 +val _ = OuterSyntax.add_parsers [terminationP];
   1.195 +
   1.196 +
   1.197 +end;
   1.198 +
   1.199 +
   1.200 +end
   1.201 \ No newline at end of file