definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
authorkrauss
Fri Apr 20 10:06:11 2007 +0200 (2007-04-20)
changeset 227330b14bb35be90
parent 22732 5bd1a2a94e1b
child 22734 790f73fa8b36
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
do not depend on "termination" setup.
src/HOL/Tools/function_package/auto_term.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/function_package/mutual.ML
     1.1 --- a/src/HOL/Tools/function_package/auto_term.ML	Fri Apr 20 00:28:07 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/auto_term.ML	Fri Apr 20 10:06:11 2007 +0200
     1.3 @@ -15,18 +15,19 @@
     1.4  structure FundefRelation : FUNDEF_RELATION =
     1.5  struct
     1.6  
     1.7 -fun relation_tac ctxt rel =
     1.8 +fun inst_thm ctxt rel st =
     1.9      let
    1.10        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
    1.11 -
    1.12        val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
    1.13 -      val rule = FundefCommon.get_termination_rule ctxt |> the
    1.14 -                  |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
    1.15 +      val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
    1.16 +      val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
    1.17 +    in 
    1.18 +      Drule.cterm_instantiate [(Rvar, rel')] st' 
    1.19 +    end
    1.20  
    1.21 -      val _ $ premise $ _ = Thm.prop_of rule
    1.22 -      val Rvar = cert (Var (the_single (Term.add_vars premise [])))
    1.23 -    in rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) end
    1.24 -
    1.25 +fun relation_tac ctxt rel i = 
    1.26 +    FundefCommon.apply_termination_rule ctxt i 
    1.27 +    THEN PRIMITIVE (inst_thm ctxt rel)
    1.28  
    1.29  val setup = Method.add_methods
    1.30    [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
     2.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Apr 20 00:28:07 2007 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Apr 20 10:06:11 2007 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4  
     2.5  val acc_const_name = "Accessible_Part.acc"
     2.6  fun mk_acc domT R =
     2.7 -    Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R 
     2.8 +    Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
     2.9  
    2.10  val function_name = suffix "C"
    2.11  val graph_name = suffix "_graph"
    2.12 @@ -36,7 +36,7 @@
    2.13  datatype fundef_result =
    2.14    FundefResult of
    2.15       {
    2.16 -      f: term,
    2.17 +      fs: term list,
    2.18        G: term,
    2.19        R: term,
    2.20  
    2.21 @@ -50,12 +50,15 @@
    2.22        domintros : thm list option
    2.23       }
    2.24  
    2.25 +
    2.26  datatype fundef_context_data =
    2.27    FundefCtxData of
    2.28       {
    2.29 +      defname : string,
    2.30 +
    2.31        add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
    2.32  
    2.33 -      f : term,
    2.34 +      fs : term list,
    2.35        R : term,
    2.36        
    2.37        psimps: thm list,
    2.38 @@ -63,27 +66,26 @@
    2.39        termination: thm
    2.40       }
    2.41  
    2.42 -fun morph_fundef_data phi (FundefCtxData {add_simps, f, R, psimps, pinducts, termination}) =
    2.43 +fun morph_fundef_data phi (FundefCtxData {add_simps, fs, R, psimps, pinducts, termination, defname}) =
    2.44      let
    2.45 -      val term = Morphism.term phi
    2.46 -      val thm = Morphism.thm phi
    2.47 -      val fact = Morphism.fact phi
    2.48 +      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
    2.49 +      val name = Morphism.name phi
    2.50      in
    2.51 -      FundefCtxData { add_simps=add_simps (*FIXME ???*), 
    2.52 -                      f = term f, R = term R, psimps = fact psimps, 
    2.53 -                      pinducts = fact pinducts, termination = thm termination }
    2.54 +      FundefCtxData { add_simps = add_simps (* contains no logical entities *), 
    2.55 +                      fs = map term fs, R = term R, psimps = fact psimps, 
    2.56 +                      pinducts = fact pinducts, termination = thm termination,
    2.57 +                      defname = name defname }
    2.58      end
    2.59  
    2.60 -
    2.61  structure FundefData = GenericDataFun
    2.62  (struct
    2.63    val name = "HOL/function_def/data";
    2.64 -  type T = string * fundef_context_data Symtab.table
    2.65 +  type T = (term * fundef_context_data) NetRules.T
    2.66  
    2.67 -  val empty = ("", Symtab.empty);
    2.68 +  val empty = NetRules.init (op aconv o pairself fst) fst;
    2.69    val copy = I;
    2.70    val extend = I;
    2.71 -  fun merge _ ((l1,tab1),(l2,tab2)) = (l1, Symtab.merge (K true) (tab1, tab2))
    2.72 +  fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
    2.73  
    2.74    fun print _ _ = ();
    2.75  end);
    2.76 @@ -100,30 +102,61 @@
    2.77  end);
    2.78  
    2.79  
    2.80 -fun add_fundef_data name fundef_data =
    2.81 -    FundefData.map (fn (last,tab) => (name, Symtab.update_new (name, fundef_data) tab))
    2.82 +(* Generally useful?? *)
    2.83 +fun lift_morphism thy f = 
    2.84 +    let 
    2.85 +      val term = Drule.term_rule thy f
    2.86 +    in
    2.87 +      Morphism.thm_morphism f $> Morphism.term_morphism term $> Morphism.typ_morphism (Logic.type_map term)
    2.88 +    end
    2.89 +
    2.90 +fun import_fundef_data t ctxt =
    2.91 +    let
    2.92 +      val thy = Context.theory_of ctxt
    2.93 +      val ct = cterm_of thy t
    2.94 +      val inst_morph = lift_morphism thy o Thm.instantiate 
    2.95  
    2.96 -fun get_fundef_data name thy = Symtab.lookup (snd (FundefData.get thy)) name
    2.97 +      fun match data = 
    2.98 +          SOME (morph_fundef_data (inst_morph (Thm.cterm_match (cterm_of thy (fst data), ct))) (snd data))
    2.99 +          handle Pattern.MATCH => NONE
   2.100 +    in 
   2.101 +      get_first match (NetRules.retrieve (FundefData.get ctxt) t)
   2.102 +    end
   2.103  
   2.104 -fun set_last_fundef name = FundefData.map (apfst (K name))
   2.105 -fun get_last_fundef thy = fst (FundefData.get thy)
   2.106 +fun import_last_fundef ctxt =
   2.107 +    case NetRules.rules (FundefData.get ctxt) of
   2.108 +      [] => NONE
   2.109 +    | (t, data) :: _ =>
   2.110 +      let 
   2.111 +        val ([t'], ctxt') = Variable.import_terms true [t] (Context.proof_of ctxt)
   2.112 +      in
   2.113 +        import_fundef_data t' (Context.Proof ctxt')
   2.114 +      end
   2.115  
   2.116 +val all_fundef_data = NetRules.rules o FundefData.get
   2.117  
   2.118  val map_fundef_congs = FundefCongs.map 
   2.119  val get_fundef_congs = FundefCongs.get
   2.120  
   2.121  
   2.122  
   2.123 -structure TerminationRule = ProofDataFun
   2.124 +structure TerminationRule = GenericDataFun
   2.125  (struct
   2.126      val name = "HOL/function_def/termination"
   2.127 -    type T = thm option
   2.128 -    fun init _ = NONE
   2.129 +    type T = thm list
   2.130 +    val empty = []
   2.131 +    val extend = I
   2.132 +    fun merge _ = Drule.merge_rules
   2.133      fun print  _ _ = ()
   2.134  end);
   2.135  
   2.136 -val get_termination_rule = TerminationRule.get
   2.137 -val set_termination_rule = TerminationRule.map o K o SOME
   2.138 +val get_termination_rules = TerminationRule.get
   2.139 +val store_termination_rule = TerminationRule.map o cons
   2.140 +val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
   2.141 +
   2.142 +fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
   2.143 +    FundefData.map (fold (fn f => NetRules.insert (f, data)) fs)
   2.144 +    #> store_termination_rule termination
   2.145  
   2.146  
   2.147  
     3.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Fri Apr 20 00:28:07 2007 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Fri Apr 20 10:06:11 2007 +0200
     3.3 @@ -941,7 +941,7 @@
     3.4              val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
     3.5                                                                          
     3.6            in 
     3.7 -            FundefResult {f=f, G=G, R=R, cases=complete_thm, 
     3.8 +            FundefResult {fs=[f], G=G, R=R, cases=complete_thm, 
     3.9                            psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct], 
    3.10                            termination=total_intro, trsimps=trsimps,
    3.11                            domintros=dom_intros}
     4.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Apr 20 00:28:07 2007 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Apr 20 10:06:11 2007 +0200
     4.3 @@ -168,8 +168,8 @@
     4.4        (Method.Basic (K pat_completeness),
     4.5         SOME (Method.Source_i (Args.src (("HOL.simp_all", []), Position.none))))
     4.6  
     4.7 -fun termination_by_lexicographic_order name =
     4.8 -    FundefPackage.setup_termination_proof (SOME name)
     4.9 +val termination_by_lexicographic_order =
    4.10 +    FundefPackage.setup_termination_proof NONE
    4.11      #> Proof.global_terminal_proof (Method.Basic LexicographicOrder.lexicographic_order, NONE)
    4.12  
    4.13  val setup =
    4.14 @@ -184,8 +184,8 @@
    4.15  fun fun_cmd config fixes statements lthy =
    4.16      lthy
    4.17        |> FundefPackage.add_fundef fixes statements config
    4.18 -      ||> by_pat_completeness_simp
    4.19 -      |-> termination_by_lexicographic_order
    4.20 +      |> by_pat_completeness_simp
    4.21 +      |> termination_by_lexicographic_order
    4.22  
    4.23  
    4.24  val funP =
     5.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Apr 20 00:28:07 2007 +0200
     5.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Apr 20 10:06:11 2007 +0200
     5.3 @@ -13,13 +13,13 @@
     5.4                        -> ((bstring * Attrib.src list) * (string * bool)) list 
     5.5                        -> FundefCommon.fundef_config
     5.6                        -> local_theory
     5.7 -                      -> string * Proof.state
     5.8 +                      -> Proof.state
     5.9  
    5.10      val add_fundef_i:  (string * typ option * mixfix) list
    5.11                         -> ((bstring * Attrib.src list) * (term * bool)) list
    5.12                         -> FundefCommon.fundef_config
    5.13                         -> local_theory
    5.14 -                       -> string * Proof.state
    5.15 +                       -> Proof.state
    5.16  
    5.17      val setup_termination_proof : string option -> local_theory -> Proof.state
    5.18  
    5.19 @@ -70,7 +70,7 @@
    5.20  
    5.21  fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
    5.22      let
    5.23 -      val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    5.24 +      val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    5.25            cont (Goal.close_result proof)
    5.26  
    5.27        val qualify = NameSpace.qualified defname
    5.28 @@ -87,12 +87,12 @@
    5.29              ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
    5.30  
    5.31        val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
    5.32 -                                  pinducts=snd pinducts', termination=termination', f=f, R=R }
    5.33 +                                  pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname }
    5.34        val cdata' = cdata |> morph_fundef_data (LocalTheory.target_morphism lthy);  (* FIXME !? *)
    5.35      in
    5.36        lthy 
    5.37 -        |> LocalTheory.declaration (fn phi => add_fundef_data defname (morph_fundef_data phi cdata)) (* save in target *)
    5.38 -        |> Context.proof_map (add_fundef_data defname cdata') (* also save in local context *)
    5.39 +        |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata)) (* save in target *)
    5.40 +        |> Context.proof_map (add_fundef_data cdata') (* also save in local context *)
    5.41      end (* FIXME: Add cases for induct and cases thm *)
    5.42  
    5.43  
    5.44 @@ -129,18 +129,17 @@
    5.45  
    5.46        val afterqed = fundef_afterqed config fixes spec defname cont sort_cont
    5.47      in
    5.48 -      (defname, lthy
    5.49 -         |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
    5.50 -         |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd)
    5.51 +      lthy
    5.52 +        |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
    5.53 +        |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
    5.54      end
    5.55  
    5.56  
    5.57 -fun total_termination_afterqed defname data [[totality]] lthy =
    5.58 +fun total_termination_afterqed data [[totality]] lthy =
    5.59      let
    5.60 -      val FundefCtxData { add_simps, psimps, pinducts, ... } = data
    5.61 +      val FundefCtxData { add_simps, psimps, pinducts, defname, ... } = data
    5.62  
    5.63        val totality = Goal.close_result totality
    5.64 -                       |> Thm.varifyT (* FIXME ! *)
    5.65  
    5.66        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
    5.67  
    5.68 @@ -159,16 +158,16 @@
    5.69      end
    5.70  
    5.71  
    5.72 -fun setup_termination_proof name_opt lthy =
    5.73 +fun setup_termination_proof term_opt lthy =
    5.74      let
    5.75 -        val defname = the_default (get_last_fundef (Context.Proof lthy)) name_opt
    5.76 -        val data = the (get_fundef_data defname (Context.Proof lthy))
    5.77 -                   handle Option.Option => raise ERROR ("No such function definition: " ^ defname)
    5.78 +      val data = the (case term_opt of
    5.79 +                        SOME t => import_fundef_data (ProofContext.read_term lthy t) (Context.Proof lthy)
    5.80 +                      | NONE => import_last_fundef (Context.Proof lthy))
    5.81 +          handle Option.Option => raise ERROR ("Not a function: " ^ quote (the_default "" term_opt))
    5.82  
    5.83          val FundefCtxData {termination, R, ...} = data
    5.84          val domT = domain_type (fastype_of R)
    5.85          val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
    5.86 -                     |> Type.freeze (* FIXME ! *)
    5.87      in
    5.88        lthy
    5.89          |> ProofContext.note_thmss_i "" [(("", [ContextRules.rule_del]), [([allI], [])])] |> snd
    5.90 @@ -176,8 +175,7 @@
    5.91          |> ProofContext.note_thmss_i ""
    5.92            [(("termination", [ContextRules.intro_bang (SOME 0)]),
    5.93              [([Goal.norm_result termination], [])])] |> snd
    5.94 -        |> set_termination_rule termination
    5.95 -        |> Proof.theorem_i NONE (total_termination_afterqed defname data) [[(goal, [])]]
    5.96 +        |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
    5.97      end
    5.98  
    5.99  
   5.100 @@ -230,12 +228,12 @@
   5.101    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   5.102    (fundef_parser default_config
   5.103       >> (fn ((config, fixes), statements) =>
   5.104 -            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config #> snd)
   5.105 +            Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config)
   5.106              #> Toplevel.print));
   5.107  
   5.108  val terminationP =
   5.109    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   5.110 -  (P.opt_target -- Scan.option P.name
   5.111 +  (P.opt_target -- Scan.option P.term
   5.112      >> (fn (target, name) =>
   5.113             Toplevel.print o
   5.114             Toplevel.local_theory_to_proof target (setup_termination_proof name)));
     6.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Apr 20 00:28:07 2007 +0200
     6.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Apr 20 10:06:11 2007 +0200
     6.3 @@ -260,13 +260,11 @@
     6.4      end
     6.5        
     6.6  (* the main function: create table, search table, create relation,
     6.7 -   and prove the subgoals *)  (* FIXME proper goal addressing -- do not hardwire 1 *)
     6.8 +   and prove the subgoals *)  
     6.9  fun lexicographic_order_tac ctxt (st: thm) = 
    6.10      let
    6.11        val thy = theory_of_thm st
    6.12 -      val termination_thm = the (FundefCommon.get_termination_rule ctxt)
    6.13 -      val next_st = SINGLE (rtac termination_thm 1) st |> the
    6.14 -      val premlist = prems_of next_st
    6.15 +      val premlist = prems_of st
    6.16      in
    6.17        case premlist of 
    6.18              [] => error "invalid number of subgoals for this tactic - expecting at least 1 subgoal" 
    6.19 @@ -292,7 +290,7 @@
    6.20        val _ = writeln ("Instantiating R with " ^ (string_of_cterm crelterm))
    6.21        val _ = writeln "Proving subgoals"
    6.22          in
    6.23 -      next_st |> cterm_instantiate [(crel, crelterm)]
    6.24 +      st |> cterm_instantiate [(crel, crelterm)]
    6.25          |> SINGLE (rtac wf_measures 1) |> the
    6.26          |> fold prove_row clean_table
    6.27          |> Seq.single
    6.28 @@ -300,7 +298,9 @@
    6.29              end
    6.30      end
    6.31  
    6.32 -val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac
    6.33 +(* FIXME goal addressing ?? *)
    6.34 +val lexicographic_order = Method.SIMPLE_METHOD o (fn ctxt => FundefCommon.apply_termination_rule ctxt 1 
    6.35 +                                                              THEN lexicographic_order_tac ctxt)
    6.36  
    6.37  val setup = Method.add_methods [("lexicographic_order", Method.ctxt_args lexicographic_order, "termination prover for lexicographic orderings")]
    6.38  
     7.1 --- a/src/HOL/Tools/function_package/mutual.ML	Fri Apr 20 00:28:07 2007 +0200
     7.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Fri Apr 20 10:06:11 2007 +0200
     7.3 @@ -312,12 +312,13 @@
     7.4  fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
     7.5      let
     7.6        val result = inner_cont proof
     7.7 -      val FundefResult {f, G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct],
     7.8 +      val FundefResult {fs=[f], G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct],
     7.9                          termination,domintros} = result
    7.10                                                                                                                 
    7.11 -      val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} =>
    7.12 -                               mk_applied_form lthy cargTs (symmetric f_def))
    7.13 -                           parts
    7.14 +      val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
    7.15 +                                     (mk_applied_form lthy cargTs (symmetric f_def), f))
    7.16 +                                 parts
    7.17 +                             |> split_list
    7.18  
    7.19        val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
    7.20                             
    7.21 @@ -329,7 +330,7 @@
    7.22        val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
    7.23        val mtermination = full_simplify (HOL_basic_ss addsimps all_f_defs) termination
    7.24      in
    7.25 -      FundefResult { f=f, G=G, R=R,
    7.26 +      FundefResult { fs=fs, G=G, R=R,
    7.27                       psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
    7.28                       cases=cases, termination=mtermination,
    7.29                       domintros=domintros,