experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
authorkrauss
Fri Dec 07 09:42:20 2007 +0100 (2007-12-07)
changeset 255675720345ea689
parent 25566 33f740c5e022
child 25568 7bb10db582cf
experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)
src/HOL/FunDef.thy
src/HOL/Tools/function_package/induction_scheme.ML
src/HOL/ex/Induction_Scheme.thy
     1.1 --- a/src/HOL/FunDef.thy	Fri Dec 07 08:38:50 2007 +0100
     1.2 +++ b/src/HOL/FunDef.thy	Fri Dec 07 09:42:20 2007 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    ("Tools/function_package/pattern_split.ML")
     1.5    ("Tools/function_package/fundef_package.ML")
     1.6    ("Tools/function_package/auto_term.ML")
     1.7 +  ("Tools/function_package/induction_scheme.ML")
     1.8  begin
     1.9  
    1.10  text {* Definitions with default value. *}
    1.11 @@ -104,8 +105,12 @@
    1.12  use "Tools/function_package/pattern_split.ML"
    1.13  use "Tools/function_package/auto_term.ML"
    1.14  use "Tools/function_package/fundef_package.ML"
    1.15 +use "Tools/function_package/induction_scheme.ML"
    1.16  
    1.17 -setup {* FundefPackage.setup *}
    1.18 +setup {* 
    1.19 +  FundefPackage.setup 
    1.20 +  #> InductionScheme.setup
    1.21 +*}
    1.22  
    1.23  lemma let_cong [fundef_cong]:
    1.24    "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Tools/function_package/induction_scheme.ML	Fri Dec 07 09:42:20 2007 +0100
     2.3 @@ -0,0 +1,280 @@
     2.4 +
     2.5 +signature INDUCTION_SCHEME =
     2.6 +sig
     2.7 +  val mk_ind_tac : Proof.context -> thm list -> tactic  
     2.8 +  val setup : theory -> theory
     2.9 +end
    2.10 +
    2.11 +
    2.12 +structure InductionScheme : INDUCTION_SCHEME =
    2.13 +struct
    2.14 +
    2.15 +open FundefLib
    2.16 +
    2.17 +type rec_call_info = (string * typ) list * term list * term
    2.18 +
    2.19 +datatype scheme_case =
    2.20 +  SchemeCase of
    2.21 +  {
    2.22 +   qs: (string * typ) list,
    2.23 +   gs: term list,
    2.24 +   lhs: term,
    2.25 +   rs: rec_call_info list
    2.26 +  }
    2.27 +
    2.28 +datatype ind_scheme =
    2.29 +  IndScheme of
    2.30 +  {
    2.31 +   T: typ,
    2.32 +   cases: scheme_case list
    2.33 +  }
    2.34 +
    2.35 +
    2.36 +fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
    2.37 +
    2.38 +fun dest_hhf ctxt t = 
    2.39 +    let 
    2.40 +      val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
    2.41 +    in
    2.42 +      (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    2.43 +    end
    2.44 +
    2.45 +fun mk_case P ctxt premise =
    2.46 +    let
    2.47 +      val (ctxt', qs, prems, concl) = dest_hhf ctxt premise
    2.48 +      val _ $ (_ $ lhs) = concl 
    2.49 +
    2.50 +      fun mk_rcinfo pr =
    2.51 +          let
    2.52 +            val (ctxt'', Gvs, Gas, _ $ (_ $ rcarg)) = dest_hhf ctxt' pr
    2.53 +          in
    2.54 +            (Gvs, Gas, rcarg)
    2.55 +          end
    2.56 +
    2.57 +      val (gs, rcprs) = take_prefix (not o exists_aterm (fn Free v => v = P | _ => false)) prems
    2.58 +    in
    2.59 +      SchemeCase {qs=qs, gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
    2.60 +    end
    2.61 +
    2.62 +fun mk_scheme' ctxt cases (Pn, PT) =
    2.63 +    IndScheme {T=domain_type PT, cases=map (mk_case (Pn,PT) ctxt) cases }
    2.64 +
    2.65 +fun mk_completeness ctxt (IndScheme {T, cases}) =
    2.66 +    let
    2.67 +      val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) cases []
    2.68 +      val [Pbool, x] = map Free (Variable.variant_frees ctxt allqnames [("P", HOLogic.boolT), ("x", T)])
    2.69 +                       
    2.70 +      fun mk_case (SchemeCase {qs, gs, lhs, ...}) =
    2.71 +          HOLogic.mk_Trueprop Pbool
    2.72 +                     |> curry Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, lhs)))
    2.73 +                     |> fold_rev (curry Logic.mk_implies) gs
    2.74 +                     |> fold_rev (mk_forall o Free) qs
    2.75 +    in
    2.76 +      HOLogic.mk_Trueprop Pbool
    2.77 +       |> fold_rev (curry Logic.mk_implies o mk_case) cases
    2.78 +       |> mk_forall_rename ("x", x)
    2.79 +       |> mk_forall_rename ("P", Pbool)
    2.80 +    end
    2.81 +
    2.82 +fun mk_wf ctxt R (IndScheme {T, ...}) =
    2.83 +    HOLogic.Trueprop $ (Const (@{const_name "wf"}, mk_relT T --> HOLogic.boolT) $ R)
    2.84 +
    2.85 +fun mk_ineqs R (IndScheme {T, cases}) =
    2.86 +    let
    2.87 +      fun f (SchemeCase {qs, gs, lhs, rs, ...}) = 
    2.88 +          let
    2.89 +            fun g (Gvs, Gas, rcarg) =
    2.90 +                HOLogic.mk_mem (HOLogic.mk_prod (rcarg, lhs), R)
    2.91 +                  |> HOLogic.mk_Trueprop
    2.92 +                  |> fold_rev (curry Logic.mk_implies) Gas
    2.93 +                  |> fold_rev (curry Logic.mk_implies) gs
    2.94 +                  |> fold_rev (mk_forall o Free) Gvs
    2.95 +                  |> fold_rev (mk_forall o Free) qs
    2.96 +          in
    2.97 +            map g rs
    2.98 +          end
    2.99 +    in
   2.100 +      map f cases
   2.101 +    end
   2.102 +
   2.103 +
   2.104 +fun mk_induct_rule thy R complete_thm wf_thm ineqss (IndScheme {T, cases=scases}) =
   2.105 +    let
   2.106 +      val x = Free ("x", T)
   2.107 +      val P = Free ("P", T --> HOLogic.boolT)
   2.108 +
   2.109 +      val cert = cterm_of thy 
   2.110 +                
   2.111 +      (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   2.112 +      val ihyp = all T $ Abs ("z", T, 
   2.113 +               implies $ 
   2.114 +                  HOLogic.mk_Trueprop (
   2.115 +                  Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
   2.116 +                    $ (HOLogic.pair_const T T $ Bound 0 $ x) 
   2.117 +                    $ R)
   2.118 +             $ HOLogic.mk_Trueprop (P $ Bound 0))
   2.119 +           |> cert
   2.120 +
   2.121 +      val aihyp = assume ihyp
   2.122 +
   2.123 +      fun prove_case (SchemeCase {qs, gs, lhs, rs, ...}) ineqs =
   2.124 +          let
   2.125 +            val case_hyp = assume (cert (HOLogic.Trueprop $ (HOLogic.mk_eq (x, lhs))))
   2.126 +                           
   2.127 +            val cqs = map (cert o Free) qs
   2.128 +            val ags = map (assume o cert) gs
   2.129 +                      
   2.130 +            val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
   2.131 +            val sih = full_simplify replace_x_ss aihyp
   2.132 +                      
   2.133 +            fun mk_Prec (Gvs, Gas, rcarg) ineq =
   2.134 +                let
   2.135 +                  val cGas = map (assume o cert) Gas
   2.136 +                  val cGvs = map (cert o Free) Gvs
   2.137 +                  val loc_ineq = ineq 
   2.138 +                                   |> fold forall_elim (cqs @ cGvs)
   2.139 +                                   |> fold Thm.elim_implies (ags @ cGas)
   2.140 +                in
   2.141 +                  sih |> forall_elim (cert rcarg)
   2.142 +                      |> Thm.elim_implies loc_ineq
   2.143 +                      |> fold_rev (implies_intr o cprop_of) cGas
   2.144 +                      |> fold_rev forall_intr cGvs
   2.145 +                end
   2.146 +                
   2.147 +            val P_recs = map2 mk_Prec rs ineqs   (*  [P rec1, P rec2, ... ]  *)
   2.148 +                         
   2.149 +            val step = HOLogic.mk_Trueprop (P $ lhs)
   2.150 +                                           |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   2.151 +                                           |> fold_rev (curry Logic.mk_implies) gs
   2.152 +                                           |> fold_rev (mk_forall o Free) qs
   2.153 +                                           |> cert
   2.154 +                       
   2.155 +            val res = assume step
   2.156 +                       |> fold forall_elim cqs
   2.157 +                       |> fold Thm.elim_implies ags
   2.158 +                       |> fold Thm.elim_implies P_recs
   2.159 +                       |> Conv.fconv_rule 
   2.160 +                       (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (case_hyp RS eq_reflection))))) 
   2.161 +                       (* "P x" *)
   2.162 +                       |> implies_intr (cprop_of case_hyp)
   2.163 +                       |> fold_rev (implies_intr o cprop_of) ags
   2.164 +                       |> fold_rev forall_intr cqs
   2.165 +          in
   2.166 +            (res, step)
   2.167 +          end
   2.168 +          
   2.169 +      val (cases, steps) = split_list (map2 prove_case scases ineqss)
   2.170 +                           
   2.171 +      val istep = complete_thm 
   2.172 +                |> forall_elim (cert (P $ x))
   2.173 +                |> forall_elim (cert x)
   2.174 +                |> fold (Thm.elim_implies) cases
   2.175 +                |> implies_intr ihyp
   2.176 +                |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
   2.177 +         
   2.178 +      val induct_rule =
   2.179 +          @{thm "wf_induct_rule"}
   2.180 +            |> (curry op COMP) wf_thm 
   2.181 +            |> (curry op COMP) istep
   2.182 +            |> fold_rev implies_intr steps
   2.183 +            |> forall_intr (cert P)
   2.184 +    in
   2.185 +      induct_rule
   2.186 +    end
   2.187 +
   2.188 +fun mk_ind_tac ctxt facts = (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL 
   2.189 +(SUBGOAL (fn (t, i) =>
   2.190 +  let
   2.191 +    val (ctxt', _, cases, concl) = dest_hhf ctxt t
   2.192 +                                   
   2.193 +    fun get_types t = 
   2.194 +        let
   2.195 +          val (P, vs) = strip_comb (HOLogic.dest_Trueprop t)
   2.196 +          val Ts = map fastype_of vs
   2.197 +          val tupT = foldr1 HOLogic.mk_prodT Ts
   2.198 +        in 
   2.199 +          ((P, Ts), tupT)
   2.200 +        end
   2.201 +        
   2.202 +    val concls = Logic.dest_conjunction_list (Logic.strip_imp_concl concl)
   2.203 +    val (PTss, tupTs) = split_list (map get_types concls)
   2.204 +                        
   2.205 +    val n = length tupTs
   2.206 +    val ST = BalancedTree.make (uncurry SumTree.mk_sumT) tupTs
   2.207 +    val PsumT = ST --> HOLogic.boolT
   2.208 +    val Psum = ("Psum", PsumT)
   2.209 +               
   2.210 +    fun mk_rews (i, (P, Ts)) = 
   2.211 +        let
   2.212 +          val vs = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) Ts 
   2.213 +          val t = Free Psum $ SumTree.mk_inj ST n (i + 1) (foldr1 HOLogic.mk_prod vs)
   2.214 +                       |> fold_rev lambda vs
   2.215 +        in
   2.216 +          (P, t)
   2.217 +        end
   2.218 +        
   2.219 +    val rews = map_index mk_rews PTss
   2.220 +    val thy = ProofContext.theory_of ctxt'
   2.221 +    val cases' = map (Pattern.rewrite_term thy rews []) cases
   2.222 +                 
   2.223 +    val scheme = mk_scheme' ctxt' cases' Psum
   2.224 +
   2.225 +(*    val _ = sys_error (PolyML.makestring scheme)*)
   2.226 +                 
   2.227 +    val cert = cterm_of thy
   2.228 +
   2.229 +    val R = Free ("R", mk_relT ST)
   2.230 +    val ineqss = mk_ineqs R scheme
   2.231 +                   |> map (map (assume o cert))
   2.232 +    val complete = mk_completeness ctxt scheme |> cert |> assume
   2.233 +    val wf_thm = mk_wf ctxt R scheme |> cert |> assume
   2.234 +
   2.235 +    val indthm = mk_induct_rule thy R complete wf_thm ineqss scheme
   2.236 +
   2.237 +    fun mk_P (P, Ts) = 
   2.238 +        let
   2.239 +          val avars = map_index (fn (i,T) => Var (("a", i), T)) Ts
   2.240 +          val atup = foldr1 HOLogic.mk_prod avars
   2.241 +        in
   2.242 +          tupled_lambda atup (list_comb (P, avars))
   2.243 +        end
   2.244 +          
   2.245 +    val case_exp = cert (SumTree.mk_sumcases HOLogic.boolT (map mk_P PTss))
   2.246 + 
   2.247 +    val acases = map (assume o cert) cases
   2.248 +  (*
   2.249 +    val _ = sys_error (ProofContext.string_of_thm ctxt indthm)
   2.250 +    val _ = sys_error (cat_lines (map (ProofContext.string_of_thm ctxt) acases))
   2.251 +   *)
   2.252 +    val indthm' = indthm |> forall_elim case_exp
   2.253 +                         |> full_simplify SumTree.sumcase_split_ss
   2.254 +                         |> fold Thm.elim_implies acases
   2.255 +
   2.256 +    fun project (i,t) = 
   2.257 +        let
   2.258 +          val (P, vs) = strip_comb (HOLogic.dest_Trueprop t)
   2.259 +          val inst = cert (SumTree.mk_inj ST n (i + 1) (foldr1 HOLogic.mk_prod vs))
   2.260 +        in
   2.261 +          indthm' |> Drule.instantiate' [] [SOME inst]
   2.262 +                  |> simplify SumTree.sumcase_split_ss
   2.263 +        end                  
   2.264 +
   2.265 +    val res = Conjunction.intr_balanced (map_index project concls)
   2.266 +                |> fold_rev (implies_intr o cprop_of) acases
   2.267 +                |> forall_elim_vars 0
   2.268 +        in
   2.269 +          (fn st =>
   2.270 +        Drule.compose_single (res, i, st)
   2.271 +          |> fold_rev (implies_intr o cprop_of) (complete :: wf_thm :: flat ineqss)
   2.272 +          |> forall_intr (cert R)
   2.273 +          |> forall_elim_vars 0
   2.274 +          |> Seq.single
   2.275 +          )
   2.276 +  end))
   2.277 +
   2.278 +
   2.279 +val setup = Method.add_methods
   2.280 +  [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o mk_ind_tac),
   2.281 +    "proves an induction principle")]
   2.282 +
   2.283 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Induction_Scheme.thy	Fri Dec 07 09:42:20 2007 +0100
     3.3 @@ -0,0 +1,49 @@
     3.4 +(*  Title:      HOL/ex/Induction_Scheme.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Alexander Krauss, TU Muenchen
     3.7 +*)
     3.8 +
     3.9 +header {* Examples of automatically derived induction rules *}
    3.10 +
    3.11 +theory Induction_Scheme
    3.12 +imports Main
    3.13 +begin
    3.14 +
    3.15 +subsection {* Some simple induction principles on nat *}
    3.16 +
    3.17 +lemma nat_standard_induct: (* cf. Nat.thy *)
    3.18 +  "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
    3.19 +by induct_scheme (pat_completeness, lexicographic_order)
    3.20 +
    3.21 +lemma nat_induct2: (* cf. Nat.thy *)
    3.22 +  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc (Suc k)) \<rbrakk>
    3.23 +  \<Longrightarrow> P n"
    3.24 +by induct_scheme (pat_completeness, lexicographic_order)
    3.25 +
    3.26 +lemma minus_one_induct:
    3.27 +  "\<lbrakk>\<And>n::nat. (n \<noteq> 0 \<Longrightarrow> P (n - 1)) \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P x"
    3.28 +by induct_scheme (pat_completeness, lexicographic_order)
    3.29 +
    3.30 +theorem diff_induct: (* cf. Nat.thy *)
    3.31 +  "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    3.32 +    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
    3.33 +by induct_scheme (pat_completeness, lexicographic_order)
    3.34 +
    3.35 +lemma list_induct2': (* cf. List.thy *)
    3.36 +  "\<lbrakk> P [] [];
    3.37 +  \<And>x xs. P (x#xs) [];
    3.38 +  \<And>y ys. P [] (y#ys);
    3.39 +   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
    3.40 + \<Longrightarrow> P xs ys"
    3.41 +by induct_scheme (pat_completeness, lexicographic_order)
    3.42 +
    3.43 +theorem even_odd_induct:
    3.44 +  assumes "R 0"
    3.45 +  assumes "Q 0"
    3.46 +  assumes "\<And>n. Q n \<Longrightarrow> R (Suc n)"
    3.47 +  assumes "\<And>n. R n \<Longrightarrow> Q (Suc n)"
    3.48 +  shows "R n" "Q n"
    3.49 +  using assms
    3.50 +by induct_scheme (pat_completeness, lexicographic_order)
    3.51 +
    3.52 +end
    3.53 \ No newline at end of file