src/HOL/UNITY/Simple/Common.thy
changeset 13812 91713a1915ee
parent 13806 fd40c9d9076b
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/UNITY/Simple/Common.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -54,20 +54,27 @@
     1.4  by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
     1.5  
     1.6  (*This one is  t := ftime t || t := gtime t*)
     1.7 -lemma "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV)
     1.8 +lemma "mk_total_program
     1.9 +         (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV)
    1.10         \<in> {m} co (maxfg m)"
    1.11 -by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
    1.12 +apply (simp add: mk_total_program_def) 
    1.13 +apply (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
    1.14 +done
    1.15  
    1.16  (*This one is  t := max (ftime t) (gtime t)*)
    1.17 -lemma  "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)  
    1.18 +lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
    1.19         \<in> {m} co (maxfg m)"
    1.20 -by (simp add: constrains_def maxfg_def max_def gasc)
    1.21 +apply (simp add: mk_total_program_def) 
    1.22 +apply (simp add: constrains_def maxfg_def max_def gasc)
    1.23 +done
    1.24  
    1.25  (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
    1.26 -lemma  "mk_program   
    1.27 +lemma  "mk_total_program
    1.28            (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
    1.29         \<in> {m} co (maxfg m)"
    1.30 -by (simp add: constrains_def maxfg_def max_def gasc)
    1.31 +apply (simp add: mk_total_program_def) 
    1.32 +apply (simp add: constrains_def maxfg_def max_def gasc)
    1.33 +done
    1.34  
    1.35  
    1.36  (*It remans to prove that they satisfy CMT3': t does not decrease,