src/HOL/Induct/Com.thy

 
 typedecl loc
 
 types  state = "loc => nat"
        n2n2n = "nat => nat => nat"
-
-arities loc :: type
 
 datatype
   exp = N nat
       | X loc
       | Op n2n2n exp exp

 
 
 subsection {* Commands *}
 
 text{* Execution of commands *}
-consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
-
-abbreviation
-  exec_rel  ("_/ -[_]-> _" [50,0,50] 50)
-  "csig -[eval]-> s == (csig,s) \<in> exec eval"
 
 abbreviation (input)
-  generic_rel  ("_/ -|[_]-> _" [50,0,50] 50)
+  generic_rel  ("_/ -|[_]-> _" [50,0,50] 50)  where
   "esig -|[eval]-> ns == (esig,ns) \<in> eval"
 
 text{*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*}
-inductive "exec eval"
-  intros
-    Skip:    "(SKIP,s) -[eval]-> s"
-
-    Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
-
-    Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
+
+inductive_set
+  exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
+  and exec_rel :: "com * state => ((exp*state) * (nat*state)) set => state => bool"
+    ("_/ -[_]-> _" [50,0,50] 50)
+  for eval :: "((exp*state) * (nat*state)) set"
+  where
+    "csig -[eval]-> s == (csig,s) \<in> exec eval"
+
+  | Skip:    "(SKIP,s) -[eval]-> s"
+
+  | Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
+
+  | Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
              ==> (c0 ;; c1, s) -[eval]-> s1"
 
-    IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |]
+  | IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |]
              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
 
-    IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |]
+  | IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |]
               ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
 
-    WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)
+  | WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)
                  ==> (WHILE e DO c, s) -[eval]-> s1"
 
-    WhileTrue:  "[| (e,s) -|[eval]-> (0,s1);
+  | WhileTrue:  "[| (e,s) -|[eval]-> (0,s1);
                     (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |]
                  ==> (WHILE e DO c, s) -[eval]-> s3"
 
 declare exec.intros [intro]
 

     and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
 
 
 text{*Justifies using "exec" in the inductive definition of "eval"*}
 lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
-apply (unfold exec.defs )
-apply (rule lfp_mono)
-apply (assumption | rule basic_monos)+
-done
+apply (rule subsetI)
+apply (simp add: split_paired_all)
+apply (erule exec.induct)
+apply blast+
+done
+
+lemma [pred_set_conv]:
+  "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
+  by (auto simp add: le_fun_def le_bool_def)
+
+lemma [pred_set_conv]:
+  "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
+  by (auto simp add: le_fun_def le_bool_def)
 
 ML {*
 Unify.trace_bound := 30;
 Unify.search_bound := 60;
 *}

 
 
 subsection {* Expressions *}
 
 text{* Evaluation of arithmetic expressions *}
-consts
+
+inductive_set
   eval    :: "((exp*state) * (nat*state)) set"
-
-abbreviation
-  eval_rel :: "[exp*state,nat*state] => bool"         (infixl "-|->" 50)
-  "esig -|-> ns == (esig, ns) \<in> eval"
-
-inductive eval
-  intros
-    N [intro!]: "(N(n),s) -|-> (n,s)"
-
-    X [intro!]: "(X(x),s) -|-> (s(x),s)"
-
-    Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |]
+  and eval_rel :: "[exp*state,nat*state] => bool"  (infixl "-|->" 50)
+  where
+    "esig -|-> ns == (esig, ns) \<in> eval"
+
+  | N [intro!]: "(N(n),s) -|-> (n,s)"
+
+  | X [intro!]: "(X(x),s) -|-> (s(x),s)"
+
+  | Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |]
                  ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
 
-    valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |]
+  | valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |]
                     ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
 
   monos exec_mono
 
 

 
 lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
 by (rule fun_upd_same [THEN subst], fast)
 
 
-text{* Make the induction rule look nicer -- though eta_contract makes the new
+text{* Make the induction rule look nicer -- though @{text eta_contract} makes the new
     version look worse than it is...*}
 
 lemma split_lemma:
      "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
 by auto

 apply (frule Int_lower1 [THEN exec_mono, THEN subsetD])
 apply (auto simp add: split_lemma)
 done
 
 
-text{*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
+text{*Lemma for @{text Function_eval}.  The major premise is that @{text "(c,s)"} executes to @{text "s1"}
   using eval restricted to its functional part.  Note that the execution
-  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that
-  the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
-  functional on the argument (c,s).
+  @{text "(c,s) -[eval]-> s2"} can use unrestricted @{text eval}!  The reason is that
+  the execution @{text "(c,s) -[eval Int {...}]-> s1"} assures us that execution is
+  functional on the argument @{text "(c,s)"}.
 *}
 lemma com_Unique:
  "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
   ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
 apply (induct set: exec)