merged

--- a/src/HOL/HOL.thy	Tue May 04 11:00:17 2010 +0200
+++ b/src/HOL/HOL.thy	Tue May 04 14:10:42 2010 +0200
@@ -1493,7 +1493,7 @@
   Context.theory_map (Induct.map_simpset (fn ss => ss
     setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
       map (Simplifier.rewrite_rule (map Thm.symmetric
-        @{thms induct_rulify_fallback induct_true_def induct_false_def})))
+        @{thms induct_rulify_fallback})))
     addsimprocs
       [Simplifier.simproc @{theory} "swap_induct_false"
          ["induct_false ==> PROP P ==> PROP Q"]

--- a/src/HOL/Hoare/Hoare_Logic.thy	Tue May 04 11:00:17 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Tue May 04 14:10:42 2010 +0200
@@ -27,18 +27,19 @@
 
 types 'a sem = "'a => 'a => bool"
 
-consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
-primrec
-"iter 0 b S = (%s s'. s ~: b & (s=s'))"
-"iter (Suc n) b S = (%s s'. s : b & (? s''. S s s'' & iter n b S s'' s'))"
+inductive Sem :: "'a com \<Rightarrow> 'a sem"
+where
+  "Sem (Basic f) s (f s)"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
+| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
+| "s \<notin> b \<Longrightarrow> Sem (While b x c) s s"
+| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
+   Sem (While b x c) s s'"
 
-consts Sem :: "'a com => 'a sem"
-primrec
-"Sem(Basic f) s s' = (s' = f s)"
-"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')"
-"Sem(IF b THEN c1 ELSE c2 FI) s s' = ((s  : b --> Sem c1 s s') &
-                                      (s ~: b --> Sem c2 s s'))"
-"Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')"
+inductive_cases [elim!]:
+  "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
+  "Sem (IF b THEN c1 ELSE c2 FI) s s'"
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
   "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
@@ -209,19 +210,18 @@
   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
 by (auto simp:Valid_def)
 
-lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
-       (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)";
-apply(induct n)
- apply clarsimp
-apply(simp (no_asm_use))
-apply blast
-done
+lemma While_aux:
+  assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+  shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
+    s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
+  using assms
+  by (induct "WHILE b INV {i} DO c OD" s s') auto
 
 lemma WhileRule:
  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
 apply (clarsimp simp:Valid_def)
-apply(drule iter_aux)
-  prefer 2 apply assumption
+apply(drule While_aux)
+  apply assumption
  apply blast
 apply blast
 done

--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Tue May 04 11:00:17 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Tue May 04 14:10:42 2010 +0200
@@ -25,22 +25,23 @@
 
 types 'a sem = "'a option => 'a option => bool"
 
-consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
-primrec
-"iter 0 b S = (\<lambda>s s'. s \<notin> Some ` b \<and> s=s')"
-"iter (Suc n) b S =
-  (\<lambda>s s'. s \<in> Some ` b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s'))"
+inductive Sem :: "'a com \<Rightarrow> 'a sem"
+where
+  "Sem (Basic f) None None"
+| "Sem (Basic f) (Some s) (Some (f s))"
+| "Sem Abort s None"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
+| "Sem (IF b THEN c1 ELSE c2 FI) None None"
+| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
+| "Sem (While b x c) None None"
+| "s \<notin> b \<Longrightarrow> Sem (While b x c) (Some s) (Some s)"
+| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
+   Sem (While b x c) (Some s) s'"
 
-consts Sem :: "'a com => 'a sem"
-primrec
-"Sem(Basic f) s s' = (case s of None \<Rightarrow> s' = None | Some t \<Rightarrow> s' = Some(f t))"
-"Sem Abort s s' = (s' = None)"
-"Sem(c1;c2) s s' = (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
-"Sem(IF b THEN c1 ELSE c2 FI) s s' =
- (case s of None \<Rightarrow> s' = None
-  | Some t \<Rightarrow> ((t \<in> b \<longrightarrow> Sem c1 s s') \<and> (t \<notin> b \<longrightarrow> Sem c2 s s')))"
-"Sem(While b x c) s s' =
- (if s = None then s' = None else \<exists>n. iter n b (Sem c) s s')"
+inductive_cases [elim!]:
+  "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
+  "Sem (IF b THEN c1 ELSE c2 FI) s s'"
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
   "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
@@ -212,23 +213,20 @@
   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
 by (fastsimp simp:Valid_def image_def)
 
-lemma iter_aux:
- "! s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
-  (\<And>s s'. s \<in> Some ` I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> Some ` (I \<inter> -b))";
-apply(unfold image_def)
-apply(induct n)
- apply clarsimp
-apply(simp (no_asm_use))
-apply blast
-done
+lemma While_aux:
+  assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+  shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
+    s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
+  using assms
+  by (induct "WHILE b INV {i} DO c OD" s s') auto
 
 lemma WhileRule:
  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
 apply(simp add:Valid_def)
 apply(simp (no_asm) add:image_def)
 apply clarify
-apply(drule iter_aux)
-  prefer 2 apply assumption
+apply(drule While_aux)
+  apply assumption
  apply blast
 apply blast
 done

--- a/src/HOL/Tools/inductive.ML	Tue May 04 11:00:17 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue May 04 14:10:42 2010 +0200
@@ -323,11 +323,11 @@
 
 (* prove monotonicity *)
 
-fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun params monos ctxt =
+fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
  (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
     "  Proving monotonicity ...";
   (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
-    (map (fst o dest_Free) params) []
+    [] []
     (HOLogic.mk_Trueprop
       (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
     (fn _ => EVERY [rtac @{thm monoI} 1,
@@ -340,7 +340,7 @@
 
 (* prove introduction rules *)
 
-fun prove_intrs quiet_mode coind mono fp_def k params intr_ts rec_preds_defs ctxt =
+fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' =
   let
     val _ = clean_message quiet_mode "  Proving the introduction rules ...";
 
@@ -354,27 +354,27 @@
 
     val rules = [refl, TrueI, notFalseI, exI, conjI];
 
-    val intrs = map_index (fn (i, intr) => rulify
-      (Skip_Proof.prove ctxt (map (fst o dest_Free) params) [] intr (fn _ => EVERY
+    val intrs = map_index (fn (i, intr) =>
+      Skip_Proof.prove ctxt [] [] intr (fn _ => EVERY
        [rewrite_goals_tac rec_preds_defs,
         rtac (unfold RS iffD2) 1,
         EVERY1 (select_disj (length intr_ts) (i + 1)),
         (*Not ares_tac, since refl must be tried before any equality assumptions;
           backtracking may occur if the premises have extra variables!*)
-        DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]))) intr_ts
+        DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)])
+       |> rulify
+       |> singleton (ProofContext.export ctxt ctxt')) intr_ts
 
   in (intrs, unfold) end;
 
 
 (* prove elimination rules *)
 
-fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt =
+fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt ctxt''' =
   let
     val _ = clean_message quiet_mode "  Proving the elimination rules ...";
 
-    val ([pname], ctxt') = ctxt |>
-      Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
-      Variable.variant_fixes ["P"];
+    val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt;
     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
 
     fun dest_intr r =
@@ -410,7 +410,7 @@
              EVERY (map (fn prem =>
                DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
           |> rulify
-          |> singleton (ProofContext.export ctxt'' ctxt),
+          |> singleton (ProofContext.export ctxt'' ctxt'''),
          map #2 c_intrs, length Ts)
       end
 
@@ -488,16 +488,14 @@
 (* prove induction rule *)
 
 fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
-    fp_def rec_preds_defs ctxt =
+    fp_def rec_preds_defs ctxt ctxt''' =
   let
     val _ = clean_message quiet_mode "  Proving the induction rule ...";
     val thy = ProofContext.theory_of ctxt;
 
     (* predicates for induction rule *)
 
-    val (pnames, ctxt') = ctxt |>
-      Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
-      Variable.variant_fixes (mk_names "P" (length cs));
+    val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt;
     val preds = map2 (curry Free) pnames
       (map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs);
 
@@ -592,7 +590,7 @@
             rewrite_goals_tac simp_thms',
             atac 1])])
 
-  in singleton (ProofContext.export ctxt'' ctxt) (induct RS lemma) end;
+  in singleton (ProofContext.export ctxt'' ctxt''') (induct RS lemma) end;
 
 
 
@@ -689,11 +687,13 @@
       ||> Local_Theory.restore_naming lthy';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
-    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun params monos lthy'';
-    val ((_, [mono']), lthy''') =
-      Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
+    val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
+    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''';
+    val (_, lthy'''') =
+      Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
+        ProofContext.export lthy''' lthy'' [mono]) lthy'';
 
-  in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
+  in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
     list_comb (rec_const, params), preds, argTs, bs, xs)
   end;
 
@@ -774,31 +774,30 @@
     val ((intr_names, intr_atts), intr_ts) =
       apfst split_list (split_list (map (check_rule lthy cs params) intros));
 
-    val (lthy1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
+    val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
       argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
         monos params cnames_syn lthy;
 
     val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
-      params intr_ts rec_preds_defs lthy1;
+      intr_ts rec_preds_defs lthy2 lthy1;
     val elims =
       if no_elim then []
       else
         prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
-          unfold rec_preds_defs lthy1;
+          unfold rec_preds_defs lthy2 lthy1;
     val raw_induct = zero_var_indexes
       (if no_ind then Drule.asm_rl
        else if coind then
-         singleton (ProofContext.export
-           (snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
+         singleton (ProofContext.export lthy2 lthy1)
            (rotate_prems ~1 (Object_Logic.rulify
              (fold_rule rec_preds_defs
                (rewrite_rule simp_thms'''
                 (mono RS (fp_def RS @{thm def_coinduct}))))))
        else
          prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
-           rec_preds_defs lthy1);
+           rec_preds_defs lthy2 lthy1);
 
-    val (intrs', elims', induct, inducts, lthy2) = declare_rules rec_name coind no_ind
+    val (intrs', elims', induct, inducts, lthy3) = declare_rules rec_name coind no_ind
       cnames preds intrs intr_names intr_atts elims raw_induct lthy1;
 
     val result =
@@ -809,11 +808,11 @@
        induct = induct,
        inducts = inducts};
 
-    val lthy3 = lthy2
+    val lthy4 = lthy3
       |> Local_Theory.declaration false (fn phi =>
         let val result' = morph_result phi result;
         in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
-  in (result, lthy3) end;
+  in (result, lthy4) end;
 
 
 (* external interfaces *)