--- a/src/HOL/MicroJava/J/Eval.thy Fri Aug 05 14:16:44 2011 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Fri Aug 05 16:55:14 2011 +0200
@@ -189,4 +189,55 @@
apply (fast)
done
+
+lemma eval_LAcc_code: "G\<turnstile>Norm (h, l) -LAcc v\<succ>the (l v)-> Norm (h, l)"
+using LAcc[of G "(h, l)" v] by simp
+
+lemma eval_Call_code:
+ "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
+ G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
+ (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
+ G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) -blk-> s3;
+ G\<turnstile> s3 -res\<succ>v -> (x4,(h4, l4)) |] ==>
+ G\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\<succ>v-> (x4,(h4,l))"
+using Call[of G s0 e a' s1 a ps pvs x h l dynT md rT pns lvars blk res mn pTs s3 v x4 "(h4, l4)" C]
+by simp
+
+lemmas [code_pred_intro] = XcptE NewC Cast Lit BinOp
+lemmas [code_pred_intro LAcc_code] = eval_LAcc_code
+lemmas [code_pred_intro] = LAss FAcc FAss
+lemmas [code_pred_intro Call_code] = eval_Call_code
+lemmas [code_pred_intro] = XcptEs Nil Cons XcptS Skip Expr Comp Cond LoopF
+lemmas [code_pred_intro LoopT_code] = LoopT
+
+code_pred
+ (modes:
+ eval: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> o \<Rightarrow> bool
+ and
+ evals: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> o \<Rightarrow> bool
+ and
+ exec: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
+ eval
+proof -
+ case eval
+ from eval.prems show thesis
+ proof(cases (no_simp))
+ case LAcc with LAcc_code show ?thesis by auto
+ next
+ case (Call a b c d e f g h i j k l m n o p q r s t u v s4)
+ with Call_code show ?thesis
+ by(cases "s4")(simp, (erule meta_allE meta_impE|rule conjI refl| assumption)+)
+ qed(erule (3) that[OF refl]|assumption)+
+next
+ case evals
+ from evals.prems show thesis
+ by(cases (no_simp))(erule (3) that[OF refl]|assumption)+
+next
+ case exec
+ from exec.prems show thesis
+ proof(cases (no_simp))
+ case LoopT thus ?thesis by(rule LoopT_code[OF refl])
+ qed(erule (2) that[OF refl]|assumption)+
+qed
+
end
--- a/src/HOL/MicroJava/J/JListExample.thy Fri Aug 05 14:16:44 2011 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Fri Aug 05 16:55:14 2011 +0200
@@ -11,15 +11,19 @@
declare [[syntax_ambiguity_level = 100000]]
consts
- list_name :: cname
+ list_nam :: cnam
append_name :: mname
- val_nam :: vnam
- next_nam :: vnam
- l_nam :: vnam
- l1_nam :: vnam
- l2_nam :: vnam
- l3_nam :: vnam
- l4_nam :: vnam
+
+axiomatization val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam :: vnam
+where distinct_fields: "val_name \<noteq> next_name"
+ and distinct_vars:
+ "l_nam \<noteq> l1_nam" "l_nam \<noteq> l2_nam" "l_nam \<noteq> l3_nam" "l_nam \<noteq> l4_nam"
+ "l1_nam \<noteq> l2_nam" "l1_nam \<noteq> l3_nam" "l1_nam \<noteq> l4_nam"
+ "l2_nam \<noteq> l3_nam" "l2_nam \<noteq> l4_nam"
+ "l3_nam \<noteq> l4_nam"
+
+definition list_name :: cname where
+ "list_name = Cname list_nam"
definition val_name :: vname where
"val_name == VName val_nam"
@@ -58,71 +62,119 @@
definition example_prg :: "java_mb prog" where
"example_prg == [ObjectC, (list_name, list_class)]"
-types_code
- cname ("string")
- vnam ("string")
- mname ("string")
- loc' ("int")
+code_datatype list_nam
+lemma equal_cnam_code [code]:
+ "HOL.equal list_nam list_nam \<longleftrightarrow> True"
+ by(simp add: equal_cnam_def)
+
+code_datatype append_name
+lemma equal_mname_code [code]:
+ "HOL.equal append_name append_name \<longleftrightarrow> True"
+ by(simp add: equal_mname_def)
-consts_code
- "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}")
-attach {*
-fun new_addr p none loc hp =
- let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
- in nr 0 end;
-*}
+code_datatype val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam
+lemma equal_vnam_code [code]:
+ "HOL.equal val_nam val_nam \<longleftrightarrow> True"
+ "HOL.equal next_nam next_nam \<longleftrightarrow> True"
+ "HOL.equal l_nam l_nam \<longleftrightarrow> True"
+ "HOL.equal l1_nam l1_nam \<longleftrightarrow> True"
+ "HOL.equal l2_nam l2_nam \<longleftrightarrow> True"
+ "HOL.equal l3_nam l3_nam \<longleftrightarrow> True"
+ "HOL.equal l4_nam l4_nam \<longleftrightarrow> True"
+
+ "HOL.equal val_nam next_nam \<longleftrightarrow> False"
+ "HOL.equal next_nam val_nam \<longleftrightarrow> False"
- "undefined" ("(raise Match)")
- "undefined :: val" ("{* Unit *}")
- "undefined :: cname" ("\"\"")
+ "HOL.equal l_nam l1_nam \<longleftrightarrow> False"
+ "HOL.equal l_nam l2_nam \<longleftrightarrow> False"
+ "HOL.equal l_nam l3_nam \<longleftrightarrow> False"
+ "HOL.equal l_nam l4_nam \<longleftrightarrow> False"
+
+ "HOL.equal l1_nam l_nam \<longleftrightarrow> False"
+ "HOL.equal l1_nam l2_nam \<longleftrightarrow> False"
+ "HOL.equal l1_nam l3_nam \<longleftrightarrow> False"
+ "HOL.equal l1_nam l4_nam \<longleftrightarrow> False"
+
+ "HOL.equal l2_nam l_nam \<longleftrightarrow> False"
+ "HOL.equal l2_nam l1_nam \<longleftrightarrow> False"
+ "HOL.equal l2_nam l3_nam \<longleftrightarrow> False"
+ "HOL.equal l2_nam l4_nam \<longleftrightarrow> False"
- "Object" ("\"Object\"")
- "list_name" ("\"list\"")
- "append_name" ("\"append\"")
- "val_nam" ("\"val\"")
- "next_nam" ("\"next\"")
- "l_nam" ("\"l\"")
- "l1_nam" ("\"l1\"")
- "l2_nam" ("\"l2\"")
- "l3_nam" ("\"l3\"")
- "l4_nam" ("\"l4\"")
+ "HOL.equal l3_nam l_nam \<longleftrightarrow> False"
+ "HOL.equal l3_nam l1_nam \<longleftrightarrow> False"
+ "HOL.equal l3_nam l2_nam \<longleftrightarrow> False"
+ "HOL.equal l3_nam l4_nam \<longleftrightarrow> False"
+
+ "HOL.equal l4_nam l_nam \<longleftrightarrow> False"
+ "HOL.equal l4_nam l1_nam \<longleftrightarrow> False"
+ "HOL.equal l4_nam l2_nam \<longleftrightarrow> False"
+ "HOL.equal l4_nam l3_nam \<longleftrightarrow> False"
+ by(simp_all add: distinct_fields distinct_fields[symmetric] distinct_vars distinct_vars[symmetric] equal_vnam_def)
+
+axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
+lemma equal_loc'_code [code]:
+ "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'"
+ by(simp add: equal_loc'_def nat_to_loc'_inject)
-code_module J
-contains
- test = "example_prg\<turnstile>Norm (empty, empty)
- -(Expr (l1_name::=NewC list_name);;
- Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));;
- Expr (l2_name::=NewC list_name);;
- Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));;
- Expr (l3_name::=NewC list_name);;
- Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));;
- Expr (l4_name::=NewC list_name);;
- Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));;
- Expr ({list_name}(LAcc l1_name)..
- append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));;
- Expr ({list_name}(LAcc l1_name)..
- append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));;
- Expr ({list_name}(LAcc l1_name)..
- append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _"
+definition undefined_cname :: cname
+ where [code del]: "undefined_cname = undefined"
+declare undefined_cname_def[symmetric, code_inline]
+code_datatype Object Xcpt Cname undefined_cname
+
+definition undefined_val :: val
+ where [code del]: "undefined_val = undefined"
+declare undefined_val_def[symmetric, code_inline]
+code_datatype Unit Null Bool Intg Addr undefined_val
+
+definition E where
+ "E = Expr (l1_name::=NewC list_name);;
+ Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));;
+ Expr (l2_name::=NewC list_name);;
+ Expr ({list_name}(LAcc l2_name)..val_name:=Lit (Intg 2));;
+ Expr (l3_name::=NewC list_name);;
+ Expr ({list_name}(LAcc l3_name)..val_name:=Lit (Intg 3));;
+ Expr (l4_name::=NewC list_name);;
+ Expr ({list_name}(LAcc l4_name)..val_name:=Lit (Intg 4));;
+ Expr ({list_name}(LAcc l1_name)..
+ append_name({[RefT (ClassT list_name)]}[LAcc l2_name]));;
+ Expr ({list_name}(LAcc l1_name)..
+ append_name({[RefT (ClassT list_name)]}[LAcc l3_name]));;
+ Expr ({list_name}(LAcc l1_name)..
+ append_name({[RefT (ClassT list_name)]}[LAcc l4_name]))"
+
+definition test where
+ "test = Predicate.Pred (\<lambda>s. example_prg\<turnstile>Norm (empty, empty) -E-> s)"
-section {* Big step execution *}
+lemma test_code [code]:
+ "test = exec_i_i_i_o example_prg (Norm (empty, empty)) E"
+by(auto intro: exec_i_i_i_oI intro!: pred_eqI elim: exec_i_i_i_oE simp add: test_def)
-ML {*
+ML {*
+ val SOME ((_, (heap, locs)), _) = Predicate.yield @{code test};
+ locs @{code l1_name};
+ locs @{code l2_name};
+ locs @{code l3_name};
+ locs @{code l4_name};
-val SOME ((_, (heap, locs)), _) = DSeq.pull J.test;
-locs J.l1_name;
-locs J.l2_name;
-locs J.l3_name;
-locs J.l4_name;
-snd (J.the (heap (J.Loc 0))) (J.val_name, "list");
-snd (J.the (heap (J.Loc 0))) (J.next_name, "list");
-snd (J.the (heap (J.Loc 1))) (J.val_name, "list");
-snd (J.the (heap (J.Loc 1))) (J.next_name, "list");
-snd (J.the (heap (J.Loc 2))) (J.val_name, "list");
-snd (J.the (heap (J.Loc 2))) (J.next_name, "list");
-snd (J.the (heap (J.Loc 3))) (J.val_name, "list");
-snd (J.the (heap (J.Loc 3))) (J.next_name, "list");
+ fun list_fields n =
+ @{code snd} (@{code the} (heap (@{code Loc} (@{code "nat_to_loc'"} n))));
+ fun val_field n =
+ list_fields n (@{code val_name}, @{code "list_name"});
+ fun next_field n =
+ list_fields n (@{code next_name}, @{code "list_name"});
+ val Suc = @{code Suc};
+ val_field @{code "0 :: nat"};
+ next_field @{code "0 :: nat"};
+
+ val_field @{code "1 :: nat"};
+ next_field @{code "1 :: nat"};
+
+ val_field (Suc (Suc @{code "0 :: nat"}));
+ next_field (Suc (Suc @{code "0 :: nat"}));
+
+ val_field (Suc (Suc (Suc @{code "0 :: nat"})));
+ next_field (Suc (Suc (Suc @{code "0 :: nat"})));
*}
end
--- a/src/HOL/MicroJava/J/Type.thy Fri Aug 05 14:16:44 2011 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Fri Aug 05 16:55:14 2011 +0200
@@ -12,6 +12,20 @@
definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'"
instance proof qed(simp add: equal_cnam_def)
end
+text {* These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME *}
+instantiation cnam :: typerep begin
+definition "typerep_class.typerep \<equiv> \<lambda>_ :: cnam itself. Typerep.Typerep (STR ''Type.cnam'') []"
+instance proof qed
+end
+instantiation cnam :: term_of begin
+definition "term_of_class.term_of (C :: cnam) \<equiv>
+ Code_Evaluation.Const (STR ''dummy_cnam'') (Typerep.Typerep (STR ''Type.cnam'') [])"
+instance proof qed
+end
+instantiation cnam :: partial_term_of begin
+definition "partial_term_of_class.partial_term_of (C :: cnam itself) n = undefined"
+instance proof qed
+end
-- "exceptions"
datatype
@@ -31,12 +45,38 @@
definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'"
instance proof qed(simp add: equal_vnam_def)
end
+instantiation vnam :: typerep begin
+definition "typerep_class.typerep \<equiv> \<lambda>_ :: vnam itself. Typerep.Typerep (STR ''Type.vnam'') []"
+instance proof qed
+end
+instantiation vnam :: term_of begin
+definition "term_of_class.term_of (V :: vnam) \<equiv>
+ Code_Evaluation.Const (STR ''dummy_vnam'') (Typerep.Typerep (STR ''Type.vnam'') [])"
+instance proof qed
+end
+instantiation vnam :: partial_term_of begin
+definition "partial_term_of_class.partial_term_of (V :: vnam itself) n = undefined"
+instance proof qed
+end
typedecl mname -- "method name"
instantiation mname :: equal begin
definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'"
instance proof qed(simp add: equal_mname_def)
end
+instantiation mname :: typerep begin
+definition "typerep_class.typerep \<equiv> \<lambda>_ :: mname itself. Typerep.Typerep (STR ''Type.mname'') []"
+instance proof qed
+end
+instantiation mname :: term_of begin
+definition "term_of_class.term_of (M :: mname) \<equiv>
+ Code_Evaluation.Const (STR ''dummy_mname'') (Typerep.Typerep (STR ''Type.mname'') [])"
+instance proof qed
+end
+instantiation mname :: partial_term_of begin
+definition "partial_term_of_class.partial_term_of (M :: mname itself) n = undefined"
+instance proof qed
+end
-- "names for @{text This} pointer and local/field variables"
datatype vname