modified induct method
authornipkow
Mon Sep 30 15:44:21 2002 +0200 (2002-09-30)
changeset 13596ee5f79b210c1
parent 13595 7e6cdcd113a2
child 13597 a8230e035e96
modified induct method
src/HOL/Auth/Guard/Extensions.thy
src/HOL/HOL.thy
src/HOL/Hyperreal/HyperNat.ML
src/HOL/IMP/VC.thy
src/HOL/Lambda/Type.thy
src/HOL/Library/Multiset.thy
src/HOL/Nat.thy
src/HOL/SetInterval.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/rule_cases.ML
     1.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Fri Sep 27 16:44:50 2002 +0200
     1.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Mon Sep 30 15:44:21 2002 +0200
     1.3 @@ -424,7 +424,7 @@
     1.4  subsubsection{*monotonicity of knows*}
     1.5  
     1.6  lemma knows_sub_Cons: "knows A evs <= knows A (ev#evs)"
     1.7 -by (cases A, (induct evs, (induct ev, auto simp: knows.simps)+))
     1.8 +by(cases A, induct evs, auto simp: knows.simps split:event.split)
     1.9  
    1.10  lemma knows_ConsI: "X:knows A evs ==> X:knows A (ev#evs)"
    1.11  by (auto dest: knows_sub_Cons [THEN subsetD])
     2.1 --- a/src/HOL/HOL.thy	Fri Sep 27 16:44:50 2002 +0200
     2.2 +++ b/src/HOL/HOL.thy	Mon Sep 30 15:44:21 2002 +0200
     2.3 @@ -857,8 +857,6 @@
     2.4    apply (blast intro: order_less_trans)
     2.5    done
     2.6  
     2.7 -declare order_less_irrefl [iff]
     2.8 -
     2.9  lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
    2.10  apply(simp add:max_def)
    2.11  apply(rule conjI)
    2.12 @@ -897,9 +895,6 @@
    2.13  lemmas min_ac = min_assoc min_commute
    2.14                  mk_left_commute[of min,OF min_assoc min_commute]
    2.15  
    2.16 -declare order_less_irrefl [iff del]
    2.17 -declare order_less_irrefl [simp]
    2.18 -
    2.19  lemma split_min:
    2.20      "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
    2.21    by (simp add: min_def)
     3.1 --- a/src/HOL/Hyperreal/HyperNat.ML	Fri Sep 27 16:44:50 2002 +0200
     3.2 +++ b/src/HOL/Hyperreal/HyperNat.ML	Mon Sep 30 15:44:21 2002 +0200
     3.3 @@ -4,7 +4,11 @@
     3.4      Description : Explicit construction of hypernaturals using 
     3.5                    ultrafilters
     3.6  *) 
     3.7 -       
     3.8 +
     3.9 +(* blast confuses different versions of < *)
    3.10 +DelIffs [order_less_irrefl];
    3.11 +Addsimps [order_less_irrefl];
    3.12 +
    3.13  (*------------------------------------------------------------------------
    3.14                         Properties of hypnatrel
    3.15   ------------------------------------------------------------------------*)
     4.1 --- a/src/HOL/IMP/VC.thy	Fri Sep 27 16:44:50 2002 +0200
     4.2 +++ b/src/HOL/IMP/VC.thy	Mon Sep 30 15:44:21 2002 +0200
     4.3 @@ -110,28 +110,44 @@
     4.4  apply (fast elim: awp_mono)
     4.5  done
     4.6  
     4.7 -lemma vc_complete: "|- {P}c{Q} ==>  
     4.8 -   (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))"
     4.9 -apply (erule hoare.induct)
    4.10 -     apply (rule_tac x = "Askip" in exI)
    4.11 -     apply (simp (no_asm))
    4.12 -    apply (rule_tac x = "Aass x a" in exI)
    4.13 -    apply (simp (no_asm))
    4.14 -   apply clarify
    4.15 -   apply (rule_tac x = "Asemi ac aca" in exI)
    4.16 -   apply (simp (no_asm_simp))
    4.17 -   apply (fast elim!: awp_mono vc_mono)
    4.18 -  apply clarify
    4.19 -  apply (rule_tac x = "Aif b ac aca" in exI)
    4.20 -  apply (simp (no_asm_simp))
    4.21 - apply clarify
    4.22 - apply (rule_tac x = "Awhile b P ac" in exI)
    4.23 - apply (simp (no_asm_simp))
    4.24 -apply safe
    4.25 -apply (rule_tac x = "ac" in exI)
    4.26 -apply (simp (no_asm_simp))
    4.27 -apply (fast elim!: awp_mono vc_mono)
    4.28 -done
    4.29 +lemma vc_complete: assumes der: "|- {P}c{Q}"
    4.30 +  shows "(? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))"
    4.31 +  (is "? ac. ?Eq P c Q ac")
    4.32 +using der
    4.33 +proof induct
    4.34 +  case skip
    4.35 +  show ?case (is "? ac. ?C ac")
    4.36 +  proof show "?C Askip" by simp qed
    4.37 +next
    4.38 +  case (ass P a x)
    4.39 +  show ?case (is "? ac. ?C ac")
    4.40 +  proof show "?C(Aass x a)" by simp qed
    4.41 +next
    4.42 +  case (semi P Q R c1 c2)
    4.43 +  from semi.hyps obtain ac1 where ih1: "?Eq P c1 Q ac1" by fast
    4.44 +  from semi.hyps obtain ac2 where ih2: "?Eq Q c2 R ac2" by fast
    4.45 +  show ?case (is "? ac. ?C ac")
    4.46 +  proof
    4.47 +    show "?C(Asemi ac1 ac2)"
    4.48 +      using ih1 ih2 by simp (fast elim!: awp_mono vc_mono)
    4.49 +  qed
    4.50 +next
    4.51 +  case (If P Q b c1 c2)
    4.52 +  from If.hyps obtain ac1 where ih1: "?Eq (%s. P s & b s) c1 Q ac1" by fast
    4.53 +  from If.hyps obtain ac2 where ih2: "?Eq (%s. P s & ~b s) c2 Q ac2" by fast
    4.54 +  show ?case (is "? ac. ?C ac")
    4.55 +  proof
    4.56 +    show "?C(Aif b ac1 ac2)"
    4.57 +      using ih1 ih2 by simp
    4.58 +  qed
    4.59 +next
    4.60 +  case (While P b c)
    4.61 +  from While.hyps obtain ac where ih: "?Eq (%s. P s & b s) c P ac" by fast
    4.62 +  show ?case (is "? ac. ?C ac")
    4.63 +  proof show "?C(Awhile b P ac)" using ih by simp qed
    4.64 +next
    4.65 +  case conseq thus ?case by(fast elim!: awp_mono vc_mono)
    4.66 +qed
    4.67  
    4.68  lemma vcawp_vc_awp: "!Q. vcawp c Q = (vc c Q, awp c Q)"
    4.69  apply (induct_tac "c")
     5.1 --- a/src/HOL/Lambda/Type.thy	Fri Sep 27 16:44:50 2002 +0200
     5.2 +++ b/src/HOL/Lambda/Type.thy	Mon Sep 30 15:44:21 2002 +0200
     5.3 @@ -332,7 +332,7 @@
     5.4      assume uIT: "u \<in> IT"
     5.5      assume uT: "e \<turnstile> u : T"
     5.6      {
     5.7 -      case (Var n rs)
     5.8 +      case (Var n rs e_ T'_ u_ i_)
     5.9        assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
    5.10        let ?ty = "{t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'}"
    5.11        let ?R = "\<lambda>t. \<forall>e T' u i.
    5.12 @@ -440,13 +440,13 @@
    5.13          with False show ?thesis by (auto simp add: subst_Var)
    5.14        qed
    5.15      next
    5.16 -      case (Lambda r)
    5.17 +      case (Lambda r e_ T'_ u_ i_)
    5.18        assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
    5.19          and "\<And>e T' u i. PROP ?Q r e T' u i T"
    5.20        with uIT uT show "Abs r[u/i] \<in> IT"
    5.21          by fastsimp
    5.22      next
    5.23 -      case (Beta r a as)
    5.24 +      case (Beta r a as e_ T'_ u_ i_)
    5.25        assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
    5.26        assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
    5.27        assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
     6.1 --- a/src/HOL/Library/Multiset.thy	Fri Sep 27 16:44:50 2002 +0200
     6.2 +++ b/src/HOL/Library/Multiset.thy	Mon Sep 30 15:44:21 2002 +0200
     6.3 @@ -691,7 +691,7 @@
     6.4  
     6.5  lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
     6.6    apply (insert mult_less_not_refl)
     6.7 -  apply blast
     6.8 +  apply fast
     6.9    done
    6.10  
    6.11  
     7.1 --- a/src/HOL/Nat.thy	Fri Sep 27 16:44:50 2002 +0200
     7.2 +++ b/src/HOL/Nat.thy	Mon Sep 30 15:44:21 2002 +0200
     7.3 @@ -448,7 +448,6 @@
     7.4    by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
     7.5  
     7.6  lemma le_anti_sym: "[| m <= n; n <= m |] ==> m = (n::nat)"
     7.7 -  -- {* @{text order_less_irrefl} could make this proof fail *}
     7.8    by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
     7.9  
    7.10  lemma Suc_le_mono [iff]: "(Suc n <= Suc m) = (n <= m)"
     8.1 --- a/src/HOL/SetInterval.ML	Fri Sep 27 16:44:50 2002 +0200
     8.2 +++ b/src/HOL/SetInterval.ML	Mon Sep 30 15:44:21 2002 +0200
     8.3 @@ -36,8 +36,7 @@
     8.4      "!!k:: 'a::linorder. -lessThan k = atLeast k";
     8.5  by Auto_tac;
     8.6  by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
     8.7 -by (blast_tac (claset() addIs [order_le_less_trans RS 
     8.8 -	                       (order_less_irrefl RS notE)]) 1);
     8.9 +by (blast_tac (claset() addDs [order_le_less_trans]) 1);
    8.10  qed "Compl_lessThan";
    8.11  
    8.12  Goal "!!k:: 'a::order. {k} - lessThan k = {k}";
    8.13 @@ -69,8 +68,7 @@
    8.14      "!!k:: 'a::linorder. -greaterThan k = atMost k";
    8.15  by Auto_tac;
    8.16  by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
    8.17 -by (blast_tac (claset() addIs [order_le_less_trans RS 
    8.18 -	                       (order_less_irrefl RS notE)]) 1);
    8.19 +by (blast_tac (claset() addDs [order_le_less_trans]) 1);
    8.20  qed "Compl_greaterThan";
    8.21  
    8.22  Goal "!!k:: 'a::linorder. -atMost k = greaterThan k";
    8.23 @@ -105,8 +103,7 @@
    8.24      "!!k:: 'a::linorder. -atLeast k = lessThan k";
    8.25  by Auto_tac;
    8.26  by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
    8.27 -by (blast_tac (claset() addIs [order_le_less_trans RS 
    8.28 -	                       (order_less_irrefl RS notE)]) 1);
    8.29 +by (blast_tac (claset() addDs [order_le_less_trans]) 1);
    8.30  qed "Compl_atLeast";
    8.31  
    8.32  Addsimps [Compl_lessThan, Compl_atLeast];
     9.1 --- a/src/Pure/Isar/proof.ML	Fri Sep 27 16:44:50 2002 +0200
     9.2 +++ b/src/Pure/Isar/proof.ML	Mon Sep 30 15:44:21 2002 +0200
     9.3 @@ -685,7 +685,7 @@
     9.4        (after_qed o map_context gen_binds, pr)))
     9.5      |> map_context (ProofContext.add_cases
     9.6       (if length props = 1 then
     9.7 -      RuleCases.make true None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
     9.8 +      RuleCases.make None None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
     9.9        else [(rule_contextN, RuleCases.empty)]))
    9.10      |> auto_bind_goal props
    9.11      |> (if is_chain state then use_facts else reset_facts)
    10.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Sep 27 16:44:50 2002 +0200
    10.2 +++ b/src/Pure/Isar/rule_cases.ML	Mon Sep 30 15:44:21 2002 +0200
    10.3 @@ -17,7 +17,8 @@
    10.4    val add: thm -> thm * (string list * int)
    10.5    type T
    10.6    val empty: T
    10.7 -  val make: bool -> term option -> Sign.sg * term -> string list -> (string * T) list
    10.8 +  val hhf_nth_subgoal: Sign.sg -> int * term -> term
    10.9 +  val make: int option -> term option -> Sign.sg * term -> string list -> (string * T) list
   10.10    val rename_params: string list list -> thm -> thm
   10.11    val params: string list list -> 'a attribute
   10.12  end;
   10.13 @@ -96,24 +97,38 @@
   10.14  
   10.15  val empty = {fixes = [], assumes = [], binds = []};
   10.16  
   10.17 -fun prep_case is_open split sg prop name i =
   10.18 +fun nth_subgoal(i,prop) =
   10.19 +  hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs prop)));
   10.20 +
   10.21 +fun hhf_nth_subgoal sg = Drule.norm_hhf sg o nth_subgoal
   10.22 +  
   10.23 +(* open_params = None
   10.24 +   ==> all parameters are "open", ie their default names are used.
   10.25 +   open_params = Some k
   10.26 +   ==> only the last k parameters, the ones coming from the original
   10.27 +   goal, not from the induction rule, are "open"
   10.28 +*)
   10.29 +fun prep_case open_params split sg prop name i =
   10.30    let
   10.31 -    val Bi = Drule.norm_hhf sg (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs prop))));
   10.32 -    val xs = map (if is_open then I else apfst Syntax.internal) (Logic.strip_params Bi);
   10.33 +    val Bi = hhf_nth_subgoal sg (i,prop);
   10.34 +    val all_xs = Logic.strip_params Bi
   10.35 +    val n = length all_xs - (if_none open_params 0)
   10.36 +    val ind_xs = take(n,all_xs) and goal_xs = drop(n,all_xs)
   10.37 +    val rename = if is_none open_params then I else apfst Syntax.internal
   10.38 +    val xs = map rename ind_xs @ goal_xs
   10.39      val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
   10.40      val named_asms =
   10.41        (case split of None => [("", asms)]
   10.42        | Some t =>
   10.43 -          let val h = length (Logic.strip_assums_hyp
   10.44 -            (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs t)))))
   10.45 +          let val h = length (Logic.strip_assums_hyp(nth_subgoal(i,t)))
   10.46            in [(hypsN, Library.take (h, asms)), (premsN, Library.drop (h, asms))] end);
   10.47      val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi);
   10.48      val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl));
   10.49    in (name, {fixes = xs, assumes = named_asms, binds = [bind]}) end;
   10.50  
   10.51 -fun make is_open split (sg, prop) names =
   10.52 +fun make open_params split (sg, prop) names =
   10.53    let val nprems = Logic.count_prems (Logic.skip_flexpairs prop, 0) in
   10.54 -    foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1))
   10.55 +    foldr (fn (name, (cases, i)) => (prep_case open_params split sg prop name i :: cases, i - 1))
   10.56        (Library.drop (length names - nprems, names), ([], length names)) |> #1
   10.57    end;
   10.58