more robust simproces
authorhaftmann
Tue Aug 07 09:38:48 2007 +0200 (2007-08-07)
changeset 24165605f664d5115
parent 24164 911b46812018
child 24166 7b28dc69bdbb
more robust simproces
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
     1.1 --- a/src/HOL/Bali/Eval.thy	Tue Aug 07 09:38:47 2007 +0200
     1.2 +++ b/src/HOL/Bali/Eval.thy	Tue Aug 07 09:38:48 2007 +0200
     1.3 @@ -965,7 +965,7 @@
     1.4  simproc_setup eval_no_abrupt ("G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')") = {*
     1.5    fn _ => fn _ => fn ct =>
     1.6      (case Thm.term_of ct of
     1.7 -      (_ $ _ $ (Const ("Pair", _) $ (Const ("Datatype.option.None",_)) $ _) $ _  $ _ $ _) => NONE
     1.8 +      (_ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name None}, _)) $ _) $ _  $ _ $ _) => NONE
     1.9      | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))
    1.10  *}
    1.11  
    1.12 @@ -985,11 +985,10 @@
    1.13  simproc_setup eval_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')") = {*
    1.14    fn _ => fn _ => fn ct =>
    1.15      (case Thm.term_of ct of
    1.16 -      (_ $ _ $ _ $ _ $ _ $ (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _)) => NONE
    1.17 +      (_ $ _ $ _ $ _ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name Some}, _) $ _)$ _)) => NONE
    1.18      | _ => SOME (mk_meta_eq @{thm eval_abrupt}))
    1.19  *}
    1.20  
    1.21 -
    1.22  lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
    1.23  apply (case_tac "s", case_tac "a = None")
    1.24  by (auto intro!: eval.Lit)
     2.1 --- a/src/HOL/Bali/Evaln.thy	Tue Aug 07 09:38:47 2007 +0200
     2.2 +++ b/src/HOL/Bali/Evaln.thy	Tue Aug 07 09:38:48 2007 +0200
     2.3 @@ -360,7 +360,7 @@
     2.4  simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = {*
     2.5    fn _ => fn _ => fn ct =>
     2.6      (case Thm.term_of ct of
     2.7 -      (_ $ _ $ _ $ _ $ _ $ _ $ (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _))
     2.8 +      (_ $ _ $ _ $ _ $ _ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name Some},_) $ _)$ _))
     2.9          => NONE
    2.10      | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
    2.11  *}