src/HOL/MicroJava/BV/Step.thy
changeset 10042 7164dc0d24d8
parent 9757 1024a2d80ac0
child 10496 f2d304bdf3cc
     1.1 --- a/src/HOL/MicroJava/BV/Step.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Step.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  text "Effect of instruction on the state type:"
     1.6  consts 
     1.7 -step' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
     1.8 +step' :: "instr \<times> jvm_prog \<times> state_type => state_type"
     1.9  
    1.10  recdef step' "{}"
    1.11  "step' (Load idx,  G, (ST, LT))          = (val (LT ! idx) # ST, LT)"
    1.12 @@ -40,13 +40,13 @@
    1.13  (* "step' (i,G,s)                           = None" *)
    1.14  
    1.15  constdefs
    1.16 -  step :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
    1.17 -  "step i G \<equiv> opt_map (\<lambda>s. step' (i,G,s))"
    1.18 +  step :: "instr => jvm_prog => state_type option => state_type option"
    1.19 +  "step i G == option_map (\<lambda>s. step' (i,G,s))"
    1.20  
    1.21  
    1.22  text "Conditions under which step is applicable:"
    1.23  consts
    1.24 -app' :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool"
    1.25 +app' :: "instr \<times> jvm_prog \<times> ty \<times> state_type => bool"
    1.26  
    1.27  recdef app' "{}"
    1.28  "app' (Load idx, G, rT, s)                  = (idx < length (snd s) \<and> 
    1.29 @@ -88,13 +88,13 @@
    1.30  
    1.31  
    1.32  constdefs
    1.33 -  app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> ty \<Rightarrow> state_type option \<Rightarrow> bool"
    1.34 -  "app i G rT s \<equiv> case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,rT,t)"
    1.35 +  app :: "instr => jvm_prog => ty => state_type option => bool"
    1.36 +  "app i G rT s == case s of None => True | Some t => app' (i,G,rT,t)"
    1.37  
    1.38  text {* program counter of successor instructions: *}
    1.39  
    1.40  consts
    1.41 -succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list"
    1.42 +succs :: "instr => p_count => p_count list"
    1.43  
    1.44  primrec 
    1.45  "succs (Load idx) pc         = [pc+1]"
    1.46 @@ -117,13 +117,13 @@
    1.47  "succs (Invoke C mn fpTs) pc = [pc+1]"
    1.48  
    1.49  
    1.50 -lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
    1.51 +lemma 1: "2 < length a ==> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
    1.52  proof (cases a)
    1.53    fix x xs assume "a = x#xs" "2 < length a"
    1.54    thus ?thesis by - (cases xs, simp, cases "tl xs", auto)
    1.55  qed auto
    1.56  
    1.57 -lemma 2: "\<not>(2 < length a) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
    1.58 +lemma 2: "\<not>(2 < length a) ==> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
    1.59  proof -;
    1.60    assume "\<not>(2 < length a)"
    1.61    hence "length a < (Suc 2)" by simp
    1.62 @@ -136,7 +136,7 @@
    1.63      hence "\<exists> l. x = [l]"  by - (cases x, auto)
    1.64    } note 0 = this
    1.65  
    1.66 -  have "length a = 2 \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
    1.67 +  have "length a = 2 ==> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
    1.68    with * show ?thesis by (auto dest: 0)
    1.69  qed
    1.70  
    1.71 @@ -149,7 +149,6 @@
    1.72    by (simp add: app_def)
    1.73  
    1.74  
    1.75 -
    1.76  lemma appLoad[simp]:
    1.77  "(app (Load idx) G rT (Some s)) = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err)"
    1.78    by (simp add: app_def)
    1.79 @@ -264,7 +263,7 @@
    1.80    method (G,C) (mn,fpTs) = Some (mD', rT', b'))" (is "?app s = ?P s")
    1.81  proof (cases (open) s)
    1.82    case Pair
    1.83 -  have "?app (a,b) \<Longrightarrow> ?P (a,b)"
    1.84 +  have "?app (a,b) ==> ?P (a,b)"
    1.85    proof -
    1.86      assume app: "?app (a,b)"
    1.87      hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> 
    1.88 @@ -286,7 +285,7 @@
    1.89      with app
    1.90      show ?thesis by (auto simp add: app_def) blast
    1.91    qed
    1.92 -  with Pair have "?app s \<Longrightarrow> ?P s" by simp
    1.93 +  with Pair have "?app s ==> ?P s" by simp
    1.94    thus ?thesis by (auto simp add: app_def)
    1.95  qed 
    1.96