# HG changeset patch # User paulson # Date 894382102 -7200 # Node ID 4727272f3db6a560606f06e328ff16db277914bd # Parent 0fad2acb45fb143667dccf7f6b6cf99b63568b3f New syntax for function update; moved to main HOL directory diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue May 05 13:27:18 1998 +0200 +++ b/src/HOL/IsaMakefile Tue May 05 17:28:22 1998 +0200 @@ -46,7 +46,8 @@ Power.ML Power.thy Prod.ML Prod.thy Record.thy ROOT.ML RelPow.ML \ RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \ Sum.ML Sum.thy Tools/record_package.ML Tools/typedef_package.ML \ - Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML \ + Trancl.ML Trancl.thy Univ.ML Univ.thy \ + Update.ML Update.thy Vimage.ML Vimage.thy WF.ML \ WF.thy WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML cladata.ML \ datatype.ML equalities.ML equalities.thy hologic.ML ind_syntax.ML \ indrule.ML indrule.thy intr_elim.ML intr_elim.thy mono.ML mono.thy \ @@ -155,7 +156,7 @@ UNITY/Network.ML UNITY/Network.thy UNITY/Reach.ML UNITY/Reach.thy\ UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/Token.ML UNITY/Token.thy\ UNITY/Traces.ML UNITY/Traces.thy UNITY/UNITY.ML UNITY/UNITY.thy\ - UNITY/Update.ML UNITY/Update.thy UNITY/WFair.ML UNITY/WFair.thy + UNITY/WFair.ML UNITY/WFair.thy @$(ISATOOL) usedir $(OUT)/HOL UNITY diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Tue May 05 13:27:18 1998 +0200 +++ b/src/HOL/ROOT.ML Tue May 05 17:28:22 1998 +0200 @@ -57,6 +57,7 @@ use_thy "Sexp"; use_thy "WF_Rel"; use_thy "Map"; +use_thy "Update"; (*TFL: recursive function definitions*) cd "$ISABELLE_HOME/src/TFL"; diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/UNITY/Mutex.thy --- a/src/HOL/UNITY/Mutex.thy Tue May 05 13:27:18 1998 +0200 +++ b/src/HOL/UNITY/Mutex.thy Tue May 05 17:28:22 1998 +0200 @@ -26,24 +26,24 @@ constdefs cmd0 :: "[pvar,pvar] => (state*state) set" - "cmd0 u m == {(s,s'). s' = s[u|->1][m|->1] & s m = 0}" + "cmd0 u m == {(s,s'). s' = s[u:=1][m:=1] & s m = 0}" cmd1u :: "(state*state) set" - "cmd1u == {(s,s'). s' = s[PP|-> s VV][MM|->2] & s MM = 1}" + "cmd1u == {(s,s'). s' = s[PP:= s VV][MM:=2] & s MM = 1}" cmd1v :: "(state*state) set" - "cmd1v == {(s,s'). s' = s[PP|-> 1 - s UU][NN|->2] & s NN = 1}" + "cmd1v == {(s,s'). s' = s[PP:= 1 - s UU][NN:=2] & s NN = 1}" (*Put pv=0 for u's program and pv=1 for v's program*) cmd2 :: "[nat,pvar] => (state*state) set" - "cmd2 pv m == {(s,s'). s' = s[m|->3] & s PP = pv & s m = 2}" + "cmd2 pv m == {(s,s'). s' = s[m:=3] & s PP = pv & s m = 2}" cmd3 :: "[pvar,pvar] => (state*state) set" - "cmd3 u m == {(s,s'). s' = s[u|->0][m|->4] & s m = 3}" + "cmd3 u m == {(s,s'). s' = s[u:=0][m:=4] & s m = 3}" (*Put pv=1 for u's program and pv=0 for v's program*) cmd4 :: "[nat,pvar] => (state*state) set" - "cmd4 pv m == {(s,s'). s' = s[PP|->pv][m|->0] & s m = 4}" + "cmd4 pv m == {(s,s'). s' = s[PP:=pv][m:=0] & s m = 4}" mutex :: "(state*state) set set" "mutex == {id, diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/UNITY/Reach.ML --- a/src/HOL/UNITY/Reach.ML Tue May 05 13:27:18 1998 +0200 +++ b/src/HOL/UNITY/Reach.ML Tue May 05 17:28:22 1998 +0200 @@ -4,6 +4,7 @@ Copyright 1998 University of Cambridge Reachability in Directed Graphs. From Chandy and Misra, section 6.4. + [ this example took only four days!] *) open Reach; @@ -133,19 +134,19 @@ (*** Progress ***) -goalw thy [metric_def] "!!s. ~ s x ==> Suc (metric (s[x|->True])) = metric s"; -by (subgoal_tac "{v. ~ (s[x|->True]) v} = {v. ~ s v} - {x}" 1); +goalw thy [metric_def] "!!s. ~ s x ==> Suc (metric (s[x:=True])) = metric s"; +by (subgoal_tac "{v. ~ (s[x:=True]) v} = {v. ~ s v} - {x}" 1); by Auto_tac; by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1); qed "Suc_metric"; -goal thy "!!s. ~ s x ==> metric (s[x|->True]) < metric s"; +goal thy "!!s. ~ s x ==> metric (s[x:=True]) < metric s"; by (etac (Suc_metric RS subst) 1); by (Blast_tac 1); qed "metric_less"; AddSIs [metric_less]; -goal thy "metric (s[y|->s x | s y]) <= metric s"; +goal thy "metric (s[y:=s x | s y]) <= metric s"; by (case_tac "s x --> s y" 1); by (auto_tac (claset() addIs [less_imp_le], simpset() addsimps [update_idem])); diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/UNITY/Reach.thy --- a/src/HOL/UNITY/Reach.thy Tue May 05 13:27:18 1998 +0200 +++ b/src/HOL/UNITY/Reach.thy Tue May 05 17:28:22 1998 +0200 @@ -21,7 +21,7 @@ constdefs asgt :: "[vertex,vertex] => (state*state) set" - "asgt u v == {(s,s'). s' = s[v|-> s u | s v]}" + "asgt u v == {(s,s'). s' = s[v:= s u | s v]}" racts :: "(state*state) set set" "racts == insert id (UN (u,v): edges. {asgt u v})" diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/UNITY/Update.ML --- a/src/HOL/UNITY/Update.ML Tue May 05 13:27:18 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -(* Title: HOL/UNITY/Update.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Function updates: like the standard theory Map, but for ordinary functions -*) - -open Update; - -goalw thy [update_def] "(f[x|->y] = f) = (f x = y)"; -by Safe_tac; -by (etac subst 1); -by (rtac ext 2); -by Auto_tac; -qed "update_idem_iff"; - -(* f x = y ==> f[x|->y] = f *) -bind_thm("update_idem", update_idem_iff RS iffD2); - -AddIffs [refl RS update_idem]; - -goal thy "(f[x|->y])z = (if x=z then y else f z)"; -by (simp_tac (simpset() addsimps [update_def]) 1); -qed "update_apply"; -Addsimps [update_apply]; diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/UNITY/Update.thy --- a/src/HOL/UNITY/Update.thy Tue May 05 13:27:18 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -(* Title: HOL/UNITY/Update.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Function updates: like the standard theory Map, but for ordinary functions -*) - -Update = Fun + - -consts - update :: "('a => 'b) => 'a => 'b => ('a => 'b)" - ("_/[_/|->/_]" [900,0,0] 900) - -syntax (symbols) - update :: "('a => 'b) => 'a => 'b => ('a => 'b)" - ("_/[_/\\/_]" [900,0,0] 900) - -defs - update_def "f[a|->b] == %x. if x=a then b else f x" - -end diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/Update.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Update.ML Tue May 05 17:28:22 1998 +0200 @@ -0,0 +1,26 @@ +(* Title: HOL/UNITY/Update.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1998 University of Cambridge + +Function updates: like the standard theory Map, but for ordinary functions +*) + +open Update; + +goalw thy [update_def] "(f[x:=y] = f) = (f x = y)"; +by Safe_tac; +by (etac subst 1); +by (rtac ext 2); +by Auto_tac; +qed "update_idem_iff"; + +(* f x = y ==> f[x:=y] = f *) +bind_thm("update_idem", update_idem_iff RS iffD2); + +AddIffs [refl RS update_idem]; + +goal thy "(f[x:=y])z = (if x=z then y else f z)"; +by (simp_tac (simpset() addsimps [update_def]) 1); +qed "update_apply"; +Addsimps [update_apply]; diff -r 0fad2acb45fb -r 4727272f3db6 src/HOL/Update.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Update.thy Tue May 05 17:28:22 1998 +0200 @@ -0,0 +1,22 @@ +(* Title: HOL/UNITY/Update.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1998 University of Cambridge + +Function updates: like the standard theory Map, but for ordinary functions +*) + +Update = Fun + + +consts + update :: "('a => 'b) => 'a => 'b => ('a => 'b)" + ("_/[_/:=/_]" [900,0,0] 900) + +syntax (symbols) + update :: "('a => 'b) => 'a => 'b => ('a => 'b)" + ("_/[_/\\/_]" [900,0,0] 900) + +defs + update_def "f[a:=b] == %x. if x=a then b else f x" + +end