*** empty log message ***
authornipkow
Tue Jan 02 10:27:10 2001 +0100 (2001-01-02)
changeset 10759994877ee68cb
parent 10758 9d766f21cf41
child 10760 02d727c441bb
*** empty log message ***
src/HOL/Induct/Com.ML
src/HOL/Induct/Com.thy
src/HOL/Induct/Exp.ML
src/HOL/Induct/PropLog.ML
src/HOL/Induct/PropLog.thy
     1.1 --- a/src/HOL/Induct/Com.ML	Mon Jan 01 11:52:04 2001 +0100
     1.2 +++ b/src/HOL/Induct/Com.ML	Tue Jan 02 10:27:10 2001 +0100
     1.3 @@ -30,29 +30,15 @@
     1.4  Unify.search_bound := 60;
     1.5  
     1.6  (*Command execution is functional (deterministic) provided evaluation is*)
     1.7 -Goal "Function ev ==> Function(exec ev)";
     1.8 -by (simp_tac (simpset() addsimps [Function_def, Unique_def]) 1);
     1.9 +Goal "univalent ev ==> univalent(exec ev)";
    1.10 +by (simp_tac (simpset() addsimps [univalent_def]) 1);
    1.11  by (REPEAT (rtac allI 1));
    1.12  by (rtac impI 1);
    1.13  by (etac exec.induct 1);
    1.14  by (Blast_tac 3);
    1.15  by (Blast_tac 1);
    1.16 -by (rewrite_goals_tac [Function_def, Unique_def]);
    1.17 +by (rewrite_goals_tac [univalent_def]);
    1.18  by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
    1.19 -qed "Function_exec";
    1.20 -
    1.21 -
    1.22 -Goalw [assign_def] "(s[v/x])x = v";
    1.23 -by (Simp_tac 1);
    1.24 -qed "assign_same";
    1.25 +qed "univalent_exec";
    1.26  
    1.27 -Goalw [assign_def] "y~=x ==> (s[v/x])y = s y";
    1.28 -by (Asm_simp_tac 1);
    1.29 -qed "assign_different";
    1.30 -
    1.31 -Goalw [assign_def] "s[s x/x] = s";
    1.32 -by (rtac ext 1);
    1.33 -by (Simp_tac 1);
    1.34 -qed "assign_triv";
    1.35 -
    1.36 -Addsimps [assign_same, assign_different, assign_triv];
    1.37 +Addsimps [fun_upd_same, fun_upd_other];
     2.1 --- a/src/HOL/Induct/Com.thy	Mon Jan 01 11:52:04 2001 +0100
     2.2 +++ b/src/HOL/Induct/Com.thy	Tue Jan 02 10:27:10 2001 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     2.5  *)
     2.6  
     2.7 -Com = Datatype +
     2.8 +Com = Main +
     2.9  
    2.10  types loc
    2.11        state = "loc => nat"
    2.12 @@ -14,23 +14,22 @@
    2.13  
    2.14  arities loc :: term
    2.15  
    2.16 -(*To avoid a mutually recursive datatype declaration, expressions and commands
    2.17 -  are combined to form a single datatype.*)
    2.18  datatype
    2.19    exp = N nat
    2.20        | X loc
    2.21        | Op n2n2n exp exp
    2.22 -      | valOf exp exp          ("VALOF _ RESULTIS _"  60)
    2.23 -      | SKIP
    2.24 +      | valOf com exp          ("VALOF _ RESULTIS _"  60)
    2.25 +and
    2.26 +  com = SKIP
    2.27        | ":="  loc exp          (infixl  60)
    2.28 -      | Semi  exp exp          ("_;;_"  [60, 60] 60)
    2.29 -      | Cond  exp exp exp      ("IF _ THEN _ ELSE _"  60)
    2.30 -      | While exp exp          ("WHILE _ DO _"  60)
    2.31 +      | Semi  com com          ("_;;_"  [60, 60] 60)
    2.32 +      | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
    2.33 +      | While exp com          ("WHILE _ DO _"  60)
    2.34  
    2.35  (** Execution of commands **)
    2.36 -consts  exec    :: "((exp*state) * (nat*state)) set => ((exp*state)*state)set"
    2.37 +consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
    2.38         "@exec"  :: "((exp*state) * (nat*state)) set => 
    2.39 -                    [exp*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
    2.40 +                    [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
    2.41  
    2.42  translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
    2.43  
    2.44 @@ -40,16 +39,12 @@
    2.45  translations
    2.46      "esig -|[eval]-> ns" => "(esig,ns) : eval"
    2.47  
    2.48 -constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
    2.49 -  "s[m/x] ==  (%y. if y=x then m else s y)"
    2.50 -
    2.51 -
    2.52  (*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
    2.53  inductive "exec eval"
    2.54    intrs
    2.55      Skip    "(SKIP,s) -[eval]-> s"
    2.56  
    2.57 -    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'[v/x]"
    2.58 +    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
    2.59  
    2.60      Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
    2.61              ==> (c0 ;; c1, s) -[eval]-> s1"
    2.62 @@ -65,11 +60,4 @@
    2.63      WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
    2.64                  (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
    2.65                  ==> (WHILE e DO c, s) -[eval]-> s3"
    2.66 -
    2.67 -constdefs
    2.68 -    Unique   :: "['a, 'b, ('a*'b) set] => bool"
    2.69 -    "Unique x y r == ALL y'. (x,y'): r --> y = y'"
    2.70 -
    2.71 -    Function :: "('a*'b) set => bool"
    2.72 -    "Function r == ALL x y. (x,y): r --> Unique x y r"
    2.73  end
     3.1 --- a/src/HOL/Induct/Exp.ML	Mon Jan 01 11:52:04 2001 +0100
     3.2 +++ b/src/HOL/Induct/Exp.ML	Tue Jan 02 10:27:10 2001 +0100
     3.3 @@ -19,8 +19,8 @@
     3.4  AddSEs eval_elim_cases;
     3.5  
     3.6  
     3.7 -Goal "(X x, s[n/x]) -|-> (n, s[n/x])";
     3.8 -by (rtac (assign_same RS subst) 1 THEN resolve_tac eval.intrs 1);
     3.9 +Goal "(X x, s(x:=n)) -|-> (n, s(x:=n))";
    3.10 +by (rtac (fun_upd_same RS subst) 1 THEN resolve_tac eval.intrs 1);
    3.11  qed "var_assign_eval";
    3.12  
    3.13  AddSIs [var_assign_eval];
    3.14 @@ -66,33 +66,32 @@
    3.15    the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
    3.16    functional on the argument (c,s).
    3.17  *)
    3.18 -Goal "(c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
    3.19 +Goal "(c,s) -[eval Int {((e,s),(n,t)). ALL nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1 \
    3.20  \     ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
    3.21  by (etac exec.induct 1);
    3.22  by (ALLGOALS Full_simp_tac);
    3.23 -by (Blast_tac 3);
    3.24 -by (Blast_tac 1);
    3.25 -by (rewtac Unique_def);
    3.26 -by (Blast_tac 1);
    3.27 -by (Blast_tac 1);
    3.28 -by (Blast_tac 1);
    3.29 -by (blast_tac (claset() addEs [exec_WHILE_case]) 1);
    3.30 +      by (Blast_tac 1);
    3.31 +     by (Force_tac 1);
    3.32 +    by (Blast_tac 1);
    3.33 +   by (Blast_tac 1);
    3.34 +  by (Blast_tac 1);
    3.35 + by (blast_tac (claset() addEs [exec_WHILE_case]) 1);
    3.36  by (thin_tac "(?c,s2) -[?ev]-> s3" 1);
    3.37  by (Clarify_tac 1);
    3.38  by (etac exec_WHILE_case 1);
    3.39 -by (ALLGOALS Fast_tac);         (*Blast_tac: proof fails*)
    3.40 + by (ALLGOALS Blast_tac);
    3.41  qed "com_Unique";
    3.42  
    3.43  
    3.44  (*Expression evaluation is functional, or deterministic*)
    3.45 -Goalw [Function_def] "Function eval";
    3.46 -by (strip_tac 1);
    3.47 +Goalw [univalent_def] "univalent eval";
    3.48 +by (EVERY1[rtac allI, rtac allI, rtac impI]);
    3.49  by (split_all_tac 1);
    3.50  by (etac eval_induct 1);
    3.51  by (dtac com_Unique 4);
    3.52 -by (ALLGOALS (full_simp_tac (simpset() addsimps [Unique_def])));
    3.53 +by (ALLGOALS Full_simp_tac);
    3.54  by (ALLGOALS Blast_tac);
    3.55 -qed "Function_eval";
    3.56 +qed "univalent_eval";
    3.57  
    3.58  
    3.59  Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
    3.60 @@ -215,11 +214,12 @@
    3.61  
    3.62  (** Equivalence of  VALOF x:=e RESULTIS x  and  e **)
    3.63  
    3.64 +Delsimps [fun_upd_apply];
    3.65  Goal "(e',s) -|-> (v,s'') ==> \
    3.66  \              (e' = VALOF x:=e RESULTIS X x) --> \
    3.67 -\              (EX s'. (e, s) -|-> (v,s') & (s'' = s'[v/x]))";
    3.68 +\              (EX s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))";
    3.69  by (etac eval_induct 1);
    3.70 -by (ALLGOALS Asm_simp_tac);
    3.71 +   by (ALLGOALS Asm_simp_tac);
    3.72  by (thin_tac "?PP-->?QQ" 1);
    3.73  by (Clarify_tac 1);
    3.74  by (Simp_tac 1);
    3.75 @@ -228,6 +228,6 @@
    3.76  
    3.77  
    3.78  Goal "(e,s) -|-> (v,s') ==> \
    3.79 -\              (VALOF x:=e RESULTIS X x, s) -|-> (v,s'[v/x])";
    3.80 +\              (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))";
    3.81  by (Blast_tac 1);
    3.82  qed "valof_assign2";
     4.1 --- a/src/HOL/Induct/PropLog.ML	Mon Jan 01 11:52:04 2001 +0100
     4.2 +++ b/src/HOL/Induct/PropLog.ML	Tue Jan 02 10:27:10 2001 +0100
     4.3 @@ -56,21 +56,6 @@
     4.4  (* [| H |- p->false;  H |- p;  q: pl |] ==> H |- q *)
     4.5  bind_thm ("thms_notE", (thms.MP RS thms_falseE));
     4.6  
     4.7 -(** The function eval **)
     4.8 -
     4.9 -Goalw [eval_def] "tt[[false]] = False";
    4.10 -by (Simp_tac 1);
    4.11 -qed "eval_false";
    4.12 -
    4.13 -Goalw [eval_def] "tt[[#v]] = (v:tt)";
    4.14 -by (Simp_tac 1);
    4.15 -qed "eval_var";
    4.16 -
    4.17 -Goalw [eval_def] "tt[[p->q]] = (tt[[p]]-->tt[[q]])";
    4.18 -by (Simp_tac 1);
    4.19 -qed "eval_imp";
    4.20 -
    4.21 -Addsimps [eval_false, eval_var, eval_imp];
    4.22  
    4.23  (*Soundness of the rules wrt truth-table semantics*)
    4.24  Goalw [sat_def] "H |- p ==> H |= p";
     5.1 --- a/src/HOL/Induct/PropLog.thy	Mon Jan 01 11:52:04 2001 +0100
     5.2 +++ b/src/HOL/Induct/PropLog.thy	Tue Jan 02 10:27:10 2001 +0100
     5.3 @@ -14,7 +14,6 @@
     5.4    thms :: 'a pl set => 'a pl set
     5.5    "|-"  :: ['a pl set, 'a pl] => bool   (infixl 50)
     5.6    "|="  :: ['a pl set, 'a pl] => bool   (infixl 50)
     5.7 -  eval2 :: ['a pl, 'a set] => bool
     5.8    eval  :: ['a set, 'a pl] => bool      ("_[[_]]" [100,0] 100)
     5.9    hyps  :: ['a pl, 'a set] => 'a pl set
    5.10  
    5.11 @@ -31,17 +30,16 @@
    5.12  
    5.13  defs
    5.14    sat_def  "H |= p  ==  (!tt. (!q:H. tt[[q]]) --> tt[[p]])"
    5.15 -  eval_def "tt[[p]] == eval2 p tt"
    5.16  
    5.17  primrec
    5.18 -  "eval2(false) = (%x. False)"
    5.19 -  "eval2(#v) = (%tt. v:tt)"
    5.20 -  "eval2(p->q) = (%tt. eval2 p tt-->eval2 q tt)"
    5.21 +         "tt[[false]] = False"
    5.22 +         "tt[[#v]]    = (v:tt)"
    5.23 +eval_imp "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
    5.24  
    5.25  primrec
    5.26 -  "hyps(false) = (%tt.{})"
    5.27 -  "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
    5.28 -  "hyps(p->q) = (%tt. hyps p tt Un hyps q tt)"
    5.29 +  "hyps false  tt = {}"
    5.30 +  "hyps (#v)   tt = {if v:tt then #v else #v->false}"
    5.31 +  "hyps (p->q) tt = hyps p tt Un hyps q tt"
    5.32  
    5.33  end
    5.34