src/HOL/Induct/Com.thy
changeset 23746 a455e69c31cc
parent 19736 d8d0f8f51d69
child 24178 4ff1dc2aa18d
     1.1 --- a/src/HOL/Induct/Com.thy	Wed Jul 11 11:13:08 2007 +0200
     1.2 +++ b/src/HOL/Induct/Com.thy	Wed Jul 11 11:14:51 2007 +0200
     1.3 @@ -15,8 +15,6 @@
     1.4  types  state = "loc => nat"
     1.5         n2n2n = "nat => nat => nat"
     1.6  
     1.7 -arities loc :: type
     1.8 -
     1.9  datatype
    1.10    exp = N nat
    1.11        | X loc
    1.12 @@ -33,36 +31,38 @@
    1.13  subsection {* Commands *}
    1.14  
    1.15  text{* Execution of commands *}
    1.16 -consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
    1.17 -
    1.18 -abbreviation
    1.19 -  exec_rel  ("_/ -[_]-> _" [50,0,50] 50)
    1.20 -  "csig -[eval]-> s == (csig,s) \<in> exec eval"
    1.21  
    1.22  abbreviation (input)
    1.23 -  generic_rel  ("_/ -|[_]-> _" [50,0,50] 50)
    1.24 +  generic_rel  ("_/ -|[_]-> _" [50,0,50] 50)  where
    1.25    "esig -|[eval]-> ns == (esig,ns) \<in> eval"
    1.26  
    1.27  text{*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*}
    1.28 -inductive "exec eval"
    1.29 -  intros
    1.30 -    Skip:    "(SKIP,s) -[eval]-> s"
    1.31  
    1.32 -    Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
    1.33 +inductive_set
    1.34 +  exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
    1.35 +  and exec_rel :: "com * state => ((exp*state) * (nat*state)) set => state => bool"
    1.36 +    ("_/ -[_]-> _" [50,0,50] 50)
    1.37 +  for eval :: "((exp*state) * (nat*state)) set"
    1.38 +  where
    1.39 +    "csig -[eval]-> s == (csig,s) \<in> exec eval"
    1.40  
    1.41 -    Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
    1.42 +  | Skip:    "(SKIP,s) -[eval]-> s"
    1.43 +
    1.44 +  | Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
    1.45 +
    1.46 +  | Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
    1.47               ==> (c0 ;; c1, s) -[eval]-> s1"
    1.48  
    1.49 -    IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |]
    1.50 +  | IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |]
    1.51               ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    1.52  
    1.53 -    IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |]
    1.54 +  | IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |]
    1.55                ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    1.56  
    1.57 -    WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)
    1.58 +  | WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)
    1.59                   ==> (WHILE e DO c, s) -[eval]-> s1"
    1.60  
    1.61 -    WhileTrue:  "[| (e,s) -|[eval]-> (0,s1);
    1.62 +  | WhileTrue:  "[| (e,s) -|[eval]-> (0,s1);
    1.63                      (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |]
    1.64                   ==> (WHILE e DO c, s) -[eval]-> s3"
    1.65  
    1.66 @@ -79,11 +79,20 @@
    1.67  
    1.68  text{*Justifies using "exec" in the inductive definition of "eval"*}
    1.69  lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
    1.70 -apply (unfold exec.defs )
    1.71 -apply (rule lfp_mono)
    1.72 -apply (assumption | rule basic_monos)+
    1.73 +apply (rule subsetI)
    1.74 +apply (simp add: split_paired_all)
    1.75 +apply (erule exec.induct)
    1.76 +apply blast+
    1.77  done
    1.78  
    1.79 +lemma [pred_set_conv]:
    1.80 +  "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
    1.81 +  by (auto simp add: le_fun_def le_bool_def)
    1.82 +
    1.83 +lemma [pred_set_conv]:
    1.84 +  "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
    1.85 +  by (auto simp add: le_fun_def le_bool_def)
    1.86 +
    1.87  ML {*
    1.88  Unify.trace_bound := 30;
    1.89  Unify.search_bound := 60;
    1.90 @@ -102,23 +111,21 @@
    1.91  subsection {* Expressions *}
    1.92  
    1.93  text{* Evaluation of arithmetic expressions *}
    1.94 -consts
    1.95 -  eval    :: "((exp*state) * (nat*state)) set"
    1.96 -
    1.97 -abbreviation
    1.98 -  eval_rel :: "[exp*state,nat*state] => bool"         (infixl "-|->" 50)
    1.99 -  "esig -|-> ns == (esig, ns) \<in> eval"
   1.100  
   1.101 -inductive eval
   1.102 -  intros
   1.103 -    N [intro!]: "(N(n),s) -|-> (n,s)"
   1.104 +inductive_set
   1.105 +  eval    :: "((exp*state) * (nat*state)) set"
   1.106 +  and eval_rel :: "[exp*state,nat*state] => bool"  (infixl "-|->" 50)
   1.107 +  where
   1.108 +    "esig -|-> ns == (esig, ns) \<in> eval"
   1.109  
   1.110 -    X [intro!]: "(X(x),s) -|-> (s(x),s)"
   1.111 +  | N [intro!]: "(N(n),s) -|-> (n,s)"
   1.112  
   1.113 -    Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |]
   1.114 +  | X [intro!]: "(X(x),s) -|-> (s(x),s)"
   1.115 +
   1.116 +  | Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |]
   1.117                   ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
   1.118  
   1.119 -    valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |]
   1.120 +  | valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |]
   1.121                      ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
   1.122  
   1.123    monos exec_mono
   1.124 @@ -135,7 +142,7 @@
   1.125  by (rule fun_upd_same [THEN subst], fast)
   1.126  
   1.127  
   1.128 -text{* Make the induction rule look nicer -- though eta_contract makes the new
   1.129 +text{* Make the induction rule look nicer -- though @{text eta_contract} makes the new
   1.130      version look worse than it is...*}
   1.131  
   1.132  lemma split_lemma:
   1.133 @@ -167,11 +174,11 @@
   1.134  done
   1.135  
   1.136  
   1.137 -text{*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
   1.138 +text{*Lemma for @{text Function_eval}.  The major premise is that @{text "(c,s)"} executes to @{text "s1"}
   1.139    using eval restricted to its functional part.  Note that the execution
   1.140 -  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that
   1.141 -  the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
   1.142 -  functional on the argument (c,s).
   1.143 +  @{text "(c,s) -[eval]-> s2"} can use unrestricted @{text eval}!  The reason is that
   1.144 +  the execution @{text "(c,s) -[eval Int {...}]-> s1"} assures us that execution is
   1.145 +  functional on the argument @{text "(c,s)"}.
   1.146  *}
   1.147  lemma com_Unique:
   1.148   "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1