src/HOL/MicroJava/BV/StepMono.thy
changeset 10042 7164dc0d24d8
parent 9941 fe05af7ec816
child 10496 f2d304bdf3cc
     1.1 --- a/src/HOL/MicroJava/BV/StepMono.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/StepMono.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  
     1.6  lemma sup_loc_some [rule_format]:
     1.7 -"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Ok t \<longrightarrow> 
     1.8 +"\<forall> y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = Ok t --> 
     1.9    (\<exists>t. b!n = Ok t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
    1.10  proof (induct (open) ?P b)
    1.11    show "?P []" by simp
    1.12 @@ -41,9 +41,9 @@
    1.13     
    1.14  
    1.15  lemma all_widen_is_sup_loc:
    1.16 -"\<forall>b. length a = length b \<longrightarrow> 
    1.17 +"\<forall>b. length a = length b --> 
    1.18       (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map Ok a) <=l (map Ok b))" 
    1.19 - (is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
    1.20 + (is "\<forall>b. length a = length b --> ?Q a b" is "?P a")
    1.21  proof (induct "a")
    1.22    show "?P []" by simp
    1.23  
    1.24 @@ -60,7 +60,7 @@
    1.25   
    1.26  
    1.27  lemma append_length_n [rule_format]: 
    1.28 -"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
    1.29 +"\<forall>n. n \<le> length x --> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
    1.30  proof (induct (open) ?P x)
    1.31    show "?P []" by simp
    1.32  
    1.33 @@ -94,7 +94,7 @@
    1.34  
    1.35  
    1.36  lemma rev_append_cons:
    1.37 -"\<lbrakk>n < length x\<rbrakk> \<Longrightarrow> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
    1.38 +"[|n < length x|] ==> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
    1.39  proof -
    1.40    assume n: "n < length x"
    1.41    hence "n \<le> length x" by simp
    1.42 @@ -118,7 +118,7 @@
    1.43  
    1.44  
    1.45  lemma app_mono: 
    1.46 -"\<lbrakk>G \<turnstile> s <=' s'; app i G rT s'\<rbrakk> \<Longrightarrow> app i G rT s";
    1.47 +"[|G \<turnstile> s <=' s'; app i G rT s'|] ==> app i G rT s";
    1.48  proof -
    1.49  
    1.50    { fix s1 s2