src/HOL/Library/SCT_Interpretation.thy
changeset 23394 474ff28210c0
parent 23374 a2f492c599e0
child 23416 b73a6b72f706
     1.1 --- a/src/HOL/Library/SCT_Interpretation.thy	Thu Jun 14 23:04:36 2007 +0200
     1.2 +++ b/src/HOL/Library/SCT_Interpretation.thy	Thu Jun 14 23:04:39 2007 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4  lemma some_rd:
     1.5    assumes "mk_rel rds x y"
     1.6    shows "\<exists>rd\<in>set rds. in_cdesc rd x y"
     1.7 -  using prems
     1.8 +  using assms
     1.9    by (induct rds) (auto simp:in_cdesc_def)
    1.10  
    1.11  (* from a value sequence, get a sequence of rds *)
    1.12 @@ -125,19 +125,19 @@
    1.13  
    1.14  
    1.15  lemma decr_in_cdesc:
    1.16 -  assumes	"in_cdesc RD1 y x"
    1.17 +  assumes "in_cdesc RD1 y x"
    1.18    assumes "in_cdesc RD2 z y"
    1.19    assumes "decr RD1 RD2 m1 m2"
    1.20    shows "m2 y < m1 x"
    1.21 -  using prems
    1.22 +  using assms
    1.23    by (cases RD1, cases RD2, auto simp:decr_def)
    1.24  
    1.25  lemma decreq_in_cdesc:
    1.26 -  assumes	"in_cdesc RD1 y x"
    1.27 +  assumes "in_cdesc RD1 y x"
    1.28    assumes "in_cdesc RD2 z y"
    1.29    assumes "decreq RD1 RD2 m1 m2"
    1.30    shows "m2 y \<le> m1 x"
    1.31 -  using prems
    1.32 +  using assms
    1.33    by (cases RD1, cases RD2, auto simp:decreq_def)
    1.34  
    1.35  
    1.36 @@ -208,7 +208,7 @@
    1.37    assumes "stepP c1 c2 (ms1 i) (ms2 j) (op <)"
    1.38    assumes "approx (Graph Es) c1 c2 ms1 ms2"
    1.39    shows "approx (Graph (insert (i, \<down>, j) Es)) c1 c2 ms1 ms2"
    1.40 -  using prems
    1.41 +  using assms
    1.42    unfolding approx_def has_edge_def dest_graph.simps decr_def
    1.43    by auto
    1.44  
    1.45 @@ -216,7 +216,7 @@
    1.46    assumes "stepP c1 c2 (ms1 i) (ms2 j) (op \<le>)"
    1.47    assumes "approx (Graph Es) c1 c2 ms1 ms2"
    1.48    shows "approx (Graph (insert (i, \<Down>, j) Es)) c1 c2 ms1 ms2"
    1.49 -  using prems
    1.50 +  using assms
    1.51    unfolding approx_def has_edge_def dest_graph.simps decreq_def
    1.52    by auto
    1.53  
    1.54 @@ -276,7 +276,7 @@
    1.55    assumes "in_cdesc RD1 y x"
    1.56    assumes "in_cdesc RD2 z y"
    1.57    shows "\<not> no_step RD1 RD2"
    1.58 -  using prems
    1.59 +  using assms
    1.60    by (cases RD1, cases RD2) (auto simp:no_step_def)
    1.61  
    1.62