src/HOL/Tools/function_package/fundef_package.ML
changeset 20363 f34c5dbe74d5
parent 20338 ecdfc96cf4d0
child 20523 36a59e5d0039
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Aug 08 18:40:56 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Aug 09 00:12:33 2006 +0200
     1.3 @@ -3,18 +3,18 @@
     1.4      ID:         $Id$
     1.5      Author:     Alexander Krauss, TU Muenchen
     1.6  
     1.7 -A package for general recursive function definitions. 
     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 +signature FUNDEF_PACKAGE =
    1.15  sig
    1.16      val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *)
    1.17  
    1.18      val cong_add: attribute
    1.19      val cong_del: attribute
    1.20 -							 
    1.21 +
    1.22      val setup : theory -> theory
    1.23      val get_congs : theory -> thm list
    1.24  end
    1.25 @@ -27,24 +27,24 @@
    1.26  
    1.27  
    1.28  fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy =
    1.29 -    let 
    1.30 +    let
    1.31        val psimpss = Library.unflat (map snd spec_part) psimps
    1.32 -      val (names, attss) = split_list (map fst spec_part) 
    1.33 +      val (names, attss) = split_list (map fst spec_part)
    1.34  
    1.35 -      val thy = thy |> Theory.add_path f_name 
    1.36 -                
    1.37 +      val thy = thy |> Theory.add_path f_name
    1.38 +
    1.39        val thy = thy |> Theory.add_path label
    1.40        val spsimpss = map (map standard) psimpss (* FIXME *)
    1.41        val add_list = (names ~~ spsimpss) ~~ attss
    1.42        val (_, thy) = PureThy.add_thmss add_list thy
    1.43        val thy = thy |> Theory.parent_path
    1.44 -                
    1.45 +
    1.46        val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy
    1.47        val thy = thy |> Theory.parent_path
    1.48      in
    1.49        thy
    1.50      end
    1.51 -    
    1.52 +
    1.53  
    1.54  
    1.55  
    1.56 @@ -52,24 +52,24 @@
    1.57  
    1.58  fun fundef_afterqed congs mutual_info name data spec [[result]] thy =
    1.59      let
    1.60 -	val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
    1.61 -	val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    1.62 +        val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
    1.63 +        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    1.64          val Mutual {parts, ...} = mutual_info
    1.65  
    1.66 -	val Prep {names = Names {acc_R=accR, ...}, ...} = data
    1.67 -	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    1.68 -	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    1.69 +        val Prep {names = Names {acc_R=accR, ...}, ...} = data
    1.70 +        val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    1.71 +        val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    1.72  
    1.73          val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy
    1.74  
    1.75          val casenames = flat (map (map (fst o fst)) spec)
    1.76  
    1.77 -	val thy = thy |> Theory.add_path name
    1.78 -	val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy
    1.79 -	val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
    1.80 -	val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
    1.81 -	val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy
    1.82 -	val thy = thy |> Theory.parent_path
    1.83 +        val thy = thy |> Theory.add_path name
    1.84 +        val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy
    1.85 +        val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
    1.86 +        val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
    1.87 +        val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy
    1.88 +        val thy = thy |> Theory.parent_path
    1.89      in
    1.90        add_fundef_data name (fundef_data, mutual_info, spec) thy
    1.91      end
    1.92 @@ -78,10 +78,10 @@
    1.93      let
    1.94        fun prep_eqns neqs =
    1.95            neqs
    1.96 -            |> map (apsnd (Sign.read_prop thy))    
    1.97 +            |> map (apsnd (Sign.read_prop thy))
    1.98              |> map (apfst (apsnd (apfst (map (prep_att thy)))))
    1.99              |> FundefSplit.split_some_equations (ProofContext.init thy)
   1.100 -      
   1.101 +
   1.102        val spec = map prep_eqns eqns_attss
   1.103        val t_eqnss = map (flat o map snd) spec
   1.104  
   1.105 @@ -90,92 +90,94 @@
   1.106        val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
   1.107        val Prep {goal, goalI, ...} = data
   1.108      in
   1.109 -	thy |> ProofContext.init
   1.110 -	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs mutual_info name data spec) NONE ("", [])
   1.111 -	    [(("", []), [(goal, [])])]
   1.112 -            |> Proof.refine (Method.primitive_text (fn _ => goalI))
   1.113 -            |> Seq.hd
   1.114 +      thy |> ProofContext.init
   1.115 +          |> Proof.theorem_i PureThy.internalK NONE
   1.116 +              (ProofContext.theory o fundef_afterqed congs mutual_info name data spec) NONE ("", [])
   1.117 +              [(("", []), [(goal, [])])]
   1.118 +          |> Proof.refine (Method.primitive_text (fn _ => goalI))
   1.119 +          |> Seq.hd
   1.120      end
   1.121  
   1.122  
   1.123  fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy =
   1.124      let
   1.125 -	val totality = hd (hd thmss)
   1.126 +        val totality = hd (hd thmss)
   1.127  
   1.128 -	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
   1.129 -	  = the (get_fundef_data name thy)
   1.130 +        val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
   1.131 +          = the (get_fundef_data name thy)
   1.132  
   1.133 -	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
   1.134 +        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
   1.135  
   1.136 -	val tsimps = map (map remove_domain_condition) psimps
   1.137 -	val tinduct = map remove_domain_condition simple_pinducts
   1.138 +        val tsimps = map (map remove_domain_condition) psimps
   1.139 +        val tinduct = map remove_domain_condition simple_pinducts
   1.140  
   1.141          val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
   1.142          val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
   1.143  
   1.144          val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy
   1.145  
   1.146 -	val thy = Theory.add_path name thy
   1.147 -		  
   1.148 -	val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy 
   1.149 -	val thy = Theory.parent_path thy
   1.150 +        val thy = Theory.add_path name thy
   1.151 +
   1.152 +        val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy
   1.153 +        val thy = Theory.parent_path thy
   1.154      in
   1.155 -	thy
   1.156 +        thy
   1.157      end
   1.158  
   1.159  (*
   1.160  fun mk_partial_rules name D_name D domT idomT thmss thy =
   1.161      let
   1.162 -	val [subs, dcl] = (hd thmss)
   1.163 +        val [subs, dcl] = (hd thmss)
   1.164  
   1.165 -	val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
   1.166 -	  = the (Symtab.lookup (FundefData.get thy) name)
   1.167 +        val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
   1.168 +          = the (Symtab.lookup (FundefData.get thy) name)
   1.169  
   1.170 -	val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)] 
   1.171 -						    [SOME (cterm_of thy D)]
   1.172 -						    subsetD)
   1.173 +        val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)]
   1.174 +                                                    [SOME (cterm_of thy D)]
   1.175 +                                                    subsetD)
   1.176  
   1.177 -	val D_simps = map (curry op RS D_implies_dom) f_simps
   1.178 +        val D_simps = map (curry op RS D_implies_dom) f_simps
   1.179  
   1.180 -	val D_induct = subset_induct
   1.181 -			   |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
   1.182 -			   |> curry op COMP subs
   1.183 -			   |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
   1.184 -						 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
   1.185 +        val D_induct = subset_induct
   1.186 +                           |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
   1.187 +                           |> curry op COMP subs
   1.188 +                           |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
   1.189 +                                                 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
   1.190  
   1.191 -	val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
   1.192 -	val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
   1.193 +        val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
   1.194 +        val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
   1.195      in
   1.196 -	thy3
   1.197 +        thy3
   1.198      end
   1.199  *)
   1.200 - 
   1.201 +
   1.202  
   1.203 -fun fundef_setup_termination_proof name NONE thy = 
   1.204 +fun fundef_setup_termination_proof name NONE thy =
   1.205      let
   1.206 -	val name = if name = "" then get_last_fundef thy else name
   1.207 -	val data = the (get_fundef_data name thy)
   1.208 +        val name = if name = "" then get_last_fundef thy else name
   1.209 +        val data = the (get_fundef_data name thy)
   1.210                     handle Option.Option => raise ERROR ("No such function definition: " ^ name)
   1.211  
   1.212 -	val (res as FundefMResult {termination, ...}, mutual, _) = data
   1.213 -	val goal = FundefTermination.mk_total_termination_goal data
   1.214 +        val (res as FundefMResult {termination, ...}, mutual, _) = data
   1.215 +        val goal = FundefTermination.mk_total_termination_goal data
   1.216      in
   1.217 -	thy |> ProofContext.init
   1.218 -	    |> ProofContext.note_thmss_i [(("termination", 
   1.219 -					    [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
   1.220 -	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name mutual) NONE ("", [])
   1.221 -	    [(("", []), [(goal, [])])]
   1.222 -    end	
   1.223 +        thy |> ProofContext.init
   1.224 +            |> ProofContext.note_thmss_i [(("termination",
   1.225 +                                            [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
   1.226 +            |> Proof.theorem_i PureThy.internalK NONE
   1.227 +              (ProofContext.theory o total_termination_afterqed name mutual) NONE ("", [])
   1.228 +              [(("", []), [(goal, [])])]
   1.229 +    end
   1.230    | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
   1.231      let
   1.232 -	val name = if name = "" then get_last_fundef thy else name
   1.233 -	val data = the (get_fundef_data name thy)
   1.234 -	val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
   1.235 +        val name = if name = "" then get_last_fundef thy else name
   1.236 +        val data = the (get_fundef_data name thy)
   1.237 +        val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
   1.238      in
   1.239 -	thy |> ProofContext.init
   1.240 -	    |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
   1.241 -	    [(("", []), [(subs, []), (dcl, [])])]
   1.242 -    end	
   1.243 +        thy |> ProofContext.init
   1.244 +            |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
   1.245 +            [(("", []), [(subs, []), (dcl, [])])]
   1.246 +    end
   1.247  
   1.248  
   1.249  val add_fundef = gen_add_fundef Attrib.attribute
   1.250 @@ -190,9 +192,9 @@
   1.251  
   1.252  (* setup *)
   1.253  
   1.254 -val setup = FundefData.init #> FundefCongs.init 
   1.255 -	#>  Attrib.add_attributes
   1.256 -		[("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
   1.257 +val setup = FundefData.init #> FundefCongs.init
   1.258 +        #>  Attrib.add_attributes
   1.259 +                [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
   1.260  
   1.261  
   1.262  val get_congs = FundefCommon.get_fundef_congs o Context.Theory
   1.263 @@ -207,7 +209,7 @@
   1.264  val star = Scan.one (fn t => (OuterLex.val_of t = "*"));
   1.265  
   1.266  
   1.267 -val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME)) 
   1.268 +val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME))
   1.269                                                 >> (fn x => (map_filter I x, exists is_none x)))
   1.270                                --| P.$$$ "]";
   1.271  
   1.272 @@ -222,7 +224,7 @@
   1.273  
   1.274  val functionP =
   1.275    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   1.276 -  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) --    
   1.277 +  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) --
   1.278    P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
   1.279                                      Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
   1.280  
   1.281 @@ -230,7 +232,7 @@
   1.282    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   1.283    ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
   1.284         >> (fn (name,dom) =>
   1.285 -	      Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
   1.286 +              Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
   1.287  
   1.288  val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
   1.289