diff --git a/thys/JinjaDCI/BV/BVExample.thy b/thys/JinjaDCI/BV/BVExample.thy deleted file mode 100644 --- a/thys/JinjaDCI/BV/BVExample.thy +++ /dev/null @@ -1,579 +0,0 @@ -(* Title: Jinja/BV/BVExample.thy - - Author: Gerwin Klein -*) - -section \ Example Welltypings \label{sec:BVExample} \ - -theory BVExample -imports "../JVM/JVMListExample" BVSpecTypeSafe BVExec - "HOL-Library.Code_Target_Numeral" -begin - -text \ - This theory shows type correctness of the example program in section - \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by - explicitly providing a welltyping. It also shows that the start - state of the program conforms to the welltyping; hence type safe - execution is guaranteed. -\ - -subsection "Setup" - -lemma distinct_classes': - "list_name \ test_name" - "list_name \ Object" - "list_name \ ClassCast" - "list_name \ OutOfMemory" - "list_name \ NullPointer" - "test_name \ Object" - "test_name \ OutOfMemory" - "test_name \ ClassCast" - "test_name \ NullPointer" - "ClassCast \ NullPointer" - "ClassCast \ Object" - "NullPointer \ Object" - "OutOfMemory \ ClassCast" - "OutOfMemory \ NullPointer" - "OutOfMemory \ Object" - by (simp_all add: list_name_def test_name_def Object_def NullPointer_def - OutOfMemory_def ClassCast_def) - -lemmas distinct_classes = distinct_classes' distinct_classes' [symmetric] - -lemma distinct_fields: - "val_name \ next_name" - "next_name \ val_name" - by (simp_all add: val_name_def next_name_def) - -text \ Abbreviations for definitions we will have to use often in the -proofs below: \ -lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def - OutOfMemoryC_def ClassCastC_def -lemmas class_defs = list_class_def test_class_def - -text \ These auxiliary proofs are for efficiency: class lookup, -subclass relation, method and field lookup are computed only once: -\ -lemma class_Object [simp]: - "class E Object = Some (undefined, [],[])" - by (simp add: class_def system_defs E_def) - -lemma class_NullPointer [simp]: - "class E NullPointer = Some (Object, [], [])" - by (simp add: class_def system_defs E_def distinct_classes) - -lemma class_OutOfMemory [simp]: - "class E OutOfMemory = Some (Object, [], [])" - by (simp add: class_def system_defs E_def distinct_classes) - -lemma class_ClassCast [simp]: - "class E ClassCast = Some (Object, [], [])" - by (simp add: class_def system_defs E_def distinct_classes) - -lemma class_list [simp]: - "class E list_name = Some list_class" - by (simp add: class_def system_defs E_def distinct_classes) - -lemma class_test [simp]: - "class E test_name = Some test_class" - by (simp add: class_def system_defs E_def distinct_classes) - -lemma E_classes [simp]: - "{C. is_class E C} = {list_name, test_name, NullPointer, - ClassCast, OutOfMemory, Object}" - by (auto simp add: is_class_def class_def system_defs E_def class_defs) - -text \ The subclass releation spelled out: \ -lemma subcls1: - "subcls1 E = {(list_name,Object), (test_name,Object), (NullPointer, Object), - (ClassCast, Object), (OutOfMemory, Object)}" -(*<*) - apply (simp add: subcls1_def2) - apply (simp add: class_defs system_defs E_def class_def) - (* FIXME: cannot simply expand class names, since - inequality proofs on strings are too inefficient *) - apply (auto simp: distinct_classes split!: if_splits) - done -(*>*) - -text \ The subclass relation is acyclic; hence its converse is well founded: \ -lemma notin_rtrancl: - "(a,b) \ r\<^sup>* \ a \ b \ (\y. (a,y) \ r) \ False" - by (auto elim: converse_rtranclE) - -lemma acyclic_subcls1_E: "acyclic (subcls1 E)" -(*<*) - apply (rule acyclicI) - apply (simp add: subcls1) - apply (auto dest!: tranclD) - apply (auto elim!: notin_rtrancl simp add: distinct_classes) - done -(*>*) - -lemma wf_subcls1_E: "wf ((subcls1 E)\)" -(*<*) - apply (rule finite_acyclic_wf_converse) - apply (simp add: subcls1) - apply (rule acyclic_subcls1_E) - done -(*>*) - -text \ Method and field lookup: \ - -lemma method_append [simp]: - "method E list_name append_name = - (list_name, [Class list_name], Void, 3, 0, append_ins, [(1, 2, NullPointer, 7, 0)])" -(*<*) - apply (insert class_list) - apply (unfold list_class_def) - apply (fastforce simp add: Method_def distinct_classes intro: method_def2 Methods.intros) - done -(*>*) - -lemma method_makelist [simp]: - "method E test_name makelist_name = - (test_name, [], Void, 3, 2, make_list_ins, [])" -(*<*) - apply (insert class_test) - apply (unfold test_class_def) - apply (fastforce simp add: Method_def distinct_classes intro: method_def2 Methods.intros) - done -(*>*) - -lemma field_val [simp]: - "field E list_name val_name = (list_name, Integer)" -(*<*) - apply (insert class_list) - apply (unfold list_class_def) - apply (fastforce simp add: sees_field_def distinct_classes intro: field_def2 Fields.intros) - done -(*>*) - -lemma field_next [simp]: - "field E list_name next_name = (list_name, Class list_name)" -(*<*) - apply (insert class_list) - apply (unfold list_class_def) - apply (fastforce simp add: distinct_fields sees_field_def distinct_classes intro: field_def2 Fields.intros) - done -(*>*) - -lemma [simp]: "fields E Object = []" - by (fastforce intro: fields_def2 Fields.intros) - -lemma [simp]: "fields E NullPointer = []" - by (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros) - -lemma [simp]: "fields E ClassCast = []" - by (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros) - -lemma [simp]: "fields E OutOfMemory = []" - by (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros) - -lemma [simp]: "fields E test_name = []" -(*<*) - apply (insert class_test) - apply (unfold test_class_def) - apply (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros) - done -(*>*) - -lemmas [simp] = is_class_def - - -subsection "Program structure" - -text \ - The program is structurally wellformed: -\ -lemma wf_struct: - "wf_prog (\G C mb. True) E" (is "wf_prog ?mb E") -(*<*) -proof - - have "distinct_fst E" - by (simp add: system_defs E_def class_defs distinct_classes) - moreover - have "set SystemClasses \ set E" by (simp add: system_defs E_def) - hence "wf_syscls E" by (rule wf_syscls) - moreover - have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def) - moreover - have "wf_cdecl ?mb E NullPointerC" - by (auto elim: notin_rtrancl - simp add: wf_cdecl_def distinct_classes NullPointerC_def subcls1) - moreover - have "wf_cdecl ?mb E ClassCastC" - by (auto elim: notin_rtrancl - simp add: wf_cdecl_def distinct_classes ClassCastC_def subcls1) - moreover - have "wf_cdecl ?mb E OutOfMemoryC" - by (auto elim: notin_rtrancl - simp add: wf_cdecl_def distinct_classes OutOfMemoryC_def subcls1) - moreover - have "wf_cdecl ?mb E (list_name, list_class)" - apply (auto elim!: notin_rtrancl - simp add: wf_cdecl_def wf_fdecl_def list_class_def - wf_mdecl_def subcls1) - apply (auto simp add: distinct_classes distinct_fields Method_def elim: Methods.cases) - done - moreover - have "wf_cdecl ?mb E (test_name, test_class)" - apply (auto elim!: notin_rtrancl - simp add: wf_cdecl_def wf_fdecl_def test_class_def - wf_mdecl_def subcls1) - apply (auto simp add: distinct_classes distinct_fields Method_def elim: Methods.cases) - done - ultimately - show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def) -qed -(*>*) - -subsection "Welltypings" -text \ - We show welltypings of the methods @{term append_name} in class @{term list_name}, - and @{term makelist_name} in class @{term test_name}: -\ -lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def -(*declare app'Invoke [simp del]*) - -definition phi_append :: ty\<^sub>m ("\\<^sub>a") -where - "\\<^sub>a \ map (\(x,y). Some (x, map OK y)) [ - ( [], [Class list_name, Class list_name]), - ( [Class list_name], [Class list_name, Class list_name]), - ( [Class list_name], [Class list_name, Class list_name]), - ( [Class list_name, Class list_name], [Class list_name, Class list_name]), - ( [Class list_name, Class list_name], [Class list_name, Class list_name]), - ([NT, Class list_name, Class list_name], [Class list_name, Class list_name]), - ( [Boolean, Class list_name], [Class list_name, Class list_name]), - - ( [Class Object], [Class list_name, Class list_name]), - ( [], [Class list_name, Class list_name]), - ( [Class list_name], [Class list_name, Class list_name]), - ( [Class list_name, Class list_name], [Class list_name, Class list_name]), - ( [], [Class list_name, Class list_name]), - ( [Void], [Class list_name, Class list_name]), - - ( [Class list_name], [Class list_name, Class list_name]), - ( [Class list_name, Class list_name], [Class list_name, Class list_name]), - ( [Void], [Class list_name, Class list_name])]" - -text \ - The next definition and three proof rules implement an algorithm to - enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} - transforms a goal of the form - @{prop [display] "pc < n \ P pc"} - into a series of goals - @{prop [display] "P 0"} - @{prop [display] "P (Suc 0)"} - - @{text "\"} - - @{prop [display] "P n"} -\ -definition intervall :: "nat \ nat \ nat \ bool" ("_ \ [_, _')") -where - "x \ [a, b) \ a \ x \ x < b" - -lemma pc_0: "x < n \ (x \ [0, n) \ P x) \ P x" - by (simp add: intervall_def) - -lemma pc_next: "x \ [n0, n) \ P n0 \ (x \ [Suc n0, n) \ P x) \ P x" -(*<*) - apply (cases "x=n0") - apply (auto simp add: intervall_def) - done -(*>*) - -lemma pc_end: "x \ [n,n) \ P x" - by (unfold intervall_def) arith - - -lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK \\<^sub>a)" -(*<*) - by (auto simp add: check_types_def phi_append_def JVM_states_unfold) -(*>*) - -lemma wt_append [simp]: - "wt_method E list_name [Class list_name] Void 3 0 append_ins - [(Suc 0, 2, NullPointer, 7, 0)] \\<^sub>a" -(*<*) - apply (simp add: wt_method_def wt_start_def wt_instr_def) - apply (simp add: append_ins_def phi_append_def) - apply clarify - apply (drule sym) - apply (erule_tac P="x = y" for x y in rev_mp) - apply (elim pc_end pc_next pc_0) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (fastforce simp add: matches_ex_entry_def subcls1 - relevant_entries_def is_relevant_entry_def sees_field_def list_class_def - distinct_classes distinct_fields intro: Fields.intros) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (fastforce simp add: - relevant_entries_def is_relevant_entry_def sees_field_def list_class_def - distinct_classes distinct_fields intro: Fields.intros) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (fastforce simp add: relevant_entries_def is_relevant_entry_def subcls1) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (fastforce simp add: - relevant_entries_def is_relevant_entry_def sees_field_def list_class_def - distinct_classes distinct_fields intro: Fields.intros) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (fastforce simp add: - relevant_entries_def is_relevant_entry_def list_class_def - distinct_classes Method_def intro: Methods.intros) - apply (simp add: relevant_entries_def is_relevant_entry_def) - done -(*>*) - -text \ Some abbreviations for readability \ -abbreviation "Clist == Class list_name" -abbreviation "Ctest == Class test_name" - -definition phi_makelist :: ty\<^sub>m ("\\<^sub>m") -where - "\\<^sub>m \ map (\(x,y). Some (x, y)) [ - ( [], [OK Ctest, Err , Err ]), - ( [Clist], [OK Ctest, Err , Err ]), - ( [], [OK Clist, Err , Err ]), - ( [Clist], [OK Clist, Err , Err ]), - ( [Integer, Clist], [OK Clist, Err , Err ]), - - ( [], [OK Clist, Err , Err ]), - ( [Clist], [OK Clist, Err , Err ]), - ( [], [OK Clist, OK Clist, Err ]), - ( [Clist], [OK Clist, OK Clist, Err ]), - ( [Integer, Clist], [OK Clist, OK Clist, Err ]), - - ( [], [OK Clist, OK Clist, Err ]), - ( [Clist], [OK Clist, OK Clist, Err ]), - ( [], [OK Clist, OK Clist, OK Clist]), - ( [Clist], [OK Clist, OK Clist, OK Clist]), - ( [Integer, Clist], [OK Clist, OK Clist, OK Clist]), - - ( [], [OK Clist, OK Clist, OK Clist]), - ( [Clist], [OK Clist, OK Clist, OK Clist]), - ( [Clist, Clist], [OK Clist, OK Clist, OK Clist]), - ( [Void], [OK Clist, OK Clist, OK Clist]), - ( [], [OK Clist, OK Clist, OK Clist]), - ( [Clist], [OK Clist, OK Clist, OK Clist]), - ( [Clist, Clist], [OK Clist, OK Clist, OK Clist]), - ( [Void], [OK Clist, OK Clist, OK Clist])]" - -lemma types_makelist [simp]: "check_types E 3 (Suc (Suc (Suc 0))) (map OK \\<^sub>m)" -(*<*) - by (auto simp add: check_types_def phi_makelist_def JVM_states_unfold) -(*>*) - -lemma wt_makelist [simp]: - "wt_method E test_name [] Void 3 2 make_list_ins [] \\<^sub>m" -(*<*) - apply (simp add: wt_method_def) - apply (unfold make_list_ins_def phi_makelist_def) - apply (simp add: wt_start_def eval_nat_numeral) - apply (simp add: wt_instr_def) - apply clarify - apply (drule sym) - apply (erule_tac P="x = y" for x y in rev_mp) - apply (elim pc_end pc_next pc_0) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (fastforce simp add: - relevant_entries_def is_relevant_entry_def sees_field_def list_class_def - distinct_classes intro: Fields.intros) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (fastforce simp add: - relevant_entries_def is_relevant_entry_def sees_field_def list_class_def - distinct_classes intro: Fields.intros) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (fastforce simp add: - relevant_entries_def is_relevant_entry_def sees_field_def list_class_def - distinct_classes intro: Fields.intros) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (fastforce simp add: - relevant_entries_def is_relevant_entry_def list_class_def - distinct_classes Method_def intro: Methods.intros) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (simp add: relevant_entries_def is_relevant_entry_def) - apply (fastforce simp add: - relevant_entries_def is_relevant_entry_def list_class_def - distinct_classes Method_def intro: Methods.intros) - apply (simp add: relevant_entries_def is_relevant_entry_def) - done -(*>*) - -lemma wf_md'E: - "\ wf_prog wf_md P; - \C S fs ms m.\(C,S,fs,ms) \ set P; m \ set ms\ \ wf_md' P C m \ - \ wf_prog wf_md' P" -(*<*) - apply (simp add: wf_prog_def) - apply auto - apply (simp add: wf_cdecl_def wf_mdecl_def) - apply fastforce - done -(*>*) - -text \ The whole program is welltyped: \ -definition Phi :: ty\<^sub>P ("\") -where - "\ C mn \ if C = test_name \ mn = makelist_name then \\<^sub>m else - if C = list_name \ mn = append_name then \\<^sub>a else []" - -lemma wf_prog: - "wf_jvm_prog\<^bsub>\\<^esub> E" -(*<*) - apply (unfold wf_jvm_prog_phi_def) - apply (rule wf_md'E [OF wf_struct]) - apply (simp add: E_def) - apply clarify - apply (fold E_def) - apply (simp add: system_defs class_defs Phi_def) - apply auto - apply (simp add: distinct_classes) - done -(*>*) - - -subsection "Conformance" -text \ Execution of the program will be typesafe, because its - start state conforms to the welltyping: \ - -lemma "E,\ \ start_state E test_name makelist_name \" -(*<*) - apply (rule BV_correct_initial) - apply (rule wf_prog) - apply (fastforce simp add: test_class_def distinct_classes Method_def intro: Methods.intros) - done -(*>*) - - -subsection "Example for code generation: inferring method types" - -definition test_kil :: "jvm_prog \ cname \ ty list \ ty \ nat \ nat \ - ex_table \ instr list \ ty\<^sub>i' err list" -where - "test_kil G C pTs rT mxs mxl et instr \ - (let first = Some ([],(OK (Class C))#(map OK pTs)@(replicate mxl Err)); - start = OK first#(replicate (size instr - 1) (OK None)) - in kiljvm G mxs (1+size pTs+mxl) rT instr et start)" - - -lemma [code]: - "unstables r step ss = - fold (\p A. if \stable r step ss p then insert p A else A) [0..stable r step ss p then {p} else {})" - apply (unfold unstables_def) - apply (rule equalityI) - apply (rule subsetI) - apply (erule CollectE) - apply (erule conjE) - apply (rule UN_I) - apply simp - apply simp - apply (rule subsetI) - apply (erule UN_E) - apply (case_tac "\ stable r step ss p") - apply simp+ - done - also have "\f. (UN p:{..) \ (\p. if \ stable r step ss p then {p} else {}) = - (\p A. if \stable r step ss p then insert p A else A)" - by(auto simp add: fun_eq_iff) - finally show ?thesis . -qed - -definition some_elem :: "'a set \ 'a" where [code del]: - "some_elem = (%S. SOME x. x : S)" -code_printing - constant some_elem \ (SML) "(case/ _ of/ Set/ xs/ =>/ hd/ xs)" - -text \ This code setup is just a demonstration and \emph{not} sound! \ -notepad begin - have "some_elem (set [False, True]) = False" by eval - moreover have "some_elem (set [True, False]) = True" by eval - ultimately have False by (simp add: some_elem_def) -end - -lemma [code]: - "iter f step ss w = while (\(ss, w). \ Set.is_empty w) - (\(ss, w). - let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p})) - (ss, w)" - unfolding iter_def Set.is_empty_def some_elem_def .. - -lemma JVM_sup_unfold [code]: - "JVM_SemiType.sup S m n = lift2 (Opt.sup - (Product.sup (Listn.sup (SemiType.sup S)) - (\x y. OK (map2 (lift2 (SemiType.sup S)) x y))))" - apply (unfold JVM_SemiType.sup_def JVM_SemiType.sl_def Opt.esl_def Err.sl_def - stk_esl_def loc_sl_def Product.esl_def - Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def) - by simp - -lemmas [code] = SemiType.sup_def [unfolded exec_lub_def] JVM_le_unfold - -lemmas [code] = lesub_def plussub_def - -lemma [code]: - "is_refT T = (case T of NT \ True | Class C \ True | _ \ False)" - by (simp add: is_refT_def split: ty.split) - -declare app\<^sub>i.simps [code] - -lemma [code]: - "app\<^sub>i (Getfield F C, P, pc, mxs, T\<^sub>r, (T#ST, LT)) = - Predicate.holds (Predicate.bind (sees_field_i_i_i_o_i P C F C) (\T\<^sub>f. if P \ T \ Class C then Predicate.single () else bot))" -by(auto simp add: Predicate.holds_eq intro: sees_field_i_i_i_o_iI elim: sees_field_i_i_i_o_iE) - -lemma [code]: - "app\<^sub>i (Putfield F C, P, pc, mxs, T\<^sub>r, (T\<^sub>1#T\<^sub>2#ST, LT)) = - Predicate.holds (Predicate.bind (sees_field_i_i_i_o_i P C F C) (\T\<^sub>f. if P \ T\<^sub>2 \ (Class C) \ P \ T\<^sub>1 \ T\<^sub>f then Predicate.single () else bot))" -by(auto simp add: Predicate.holds_eq simp del: eval_bind split: if_split_asm elim!: sees_field_i_i_i_o_iE Predicate.bindE intro: Predicate.bindI sees_field_i_i_i_o_iI) - -lemma [code]: - "app\<^sub>i (Invoke M n, P, pc, mxs, T\<^sub>r, (ST,LT)) = - (n < length ST \ - (ST!n \ NT \ - (case ST!n of - Class C \ Predicate.holds (Predicate.bind (Method_i_i_i_o_o_o_o P C M) (\(Ts, T, m, D). if P \ rev (take n ST) [\] Ts then Predicate.single () else bot)) - | _ \ False)))" -by (fastforce simp add: Predicate.holds_eq simp del: eval_bind split: ty.split_asm if_split_asm intro: bindI Method_i_i_i_o_o_o_oI elim!: bindE Method_i_i_i_o_o_o_oE) - -lemmas [code] = - SemiType.sup_def [unfolded exec_lub_def] - widen.equation - is_relevant_class.simps - -definition test1 where - "test1 = test_kil E list_name [Class list_name] Void 3 0 - [(Suc 0, 2, NullPointer, 7, 0)] append_ins" -definition test2 where - "test2 = test_kil E test_name [] Void 3 2 [] make_list_ins" -definition test3 where "test3 = \\<^sub>a" -definition test4 where "test4 = \\<^sub>m" - -ML_val \ - if @{code test1} = @{code map} @{code OK} @{code test3} then () else error "wrong result"; - if @{code test2} = @{code map} @{code OK} @{code test4} then () else error "wrong result" -\ - -end diff --git a/thys/JinjaDCI/J/Examples.thy b/thys/JinjaDCI/J/Examples.thy deleted file mode 100644 --- a/thys/JinjaDCI/J/Examples.thy +++ /dev/null @@ -1,123 +0,0 @@ -(* Title: Jinja/J/Examples.thy - - Author: Christoph Petzinger - Copyright 2004 Technische Universitaet Muenchen -*) -(* - Expanded to include support for static fields and methods. - Susannah Mansky - 2017, UIUC -*) - -section \ Example Expressions \ - -theory Examples imports Expr begin - -(* HERE: none of the below currently have static methods or fields; these should be - tested at some point! *) - -definition classObject::"J_mb cdecl" -where - "classObject == (''Object'','''',[],[])" - - -definition classI :: "J_mb cdecl" -where - "classI == - (''I'', Object, - [], - [(''mult'',NonStatic,[Integer,Integer],Integer,[''i'',''j''], - if (Var ''i'' \Eq\ Val(Intg 0)) (Val(Intg 0)) - else Var ''j'' \Add\ - Var this \ ''mult''([Var ''i'' \Add\ Val(Intg (- 1)),Var ''j''])) - ])" - - -definition classL :: "J_mb cdecl" -where - "classL == - (''L'', Object, - [(''F'',NonStatic,Integer), (''N'',NonStatic,Class ''L'')], - [(''app'',NonStatic,[Class ''L''],Void,[''l''], - if (Var this \ ''N''{''L''} \Eq\ null) - (Var this \ ''N''{''L''} := Var ''l'') - else (Var this \ ''N''{''L''}) \ ''app''([Var ''l''])) - ])" - - -definition testExpr_BuildList :: "expr" -where - "testExpr_BuildList == - {''l1'':Class ''L'' := new ''L''; - Var ''l1''\''F''{''L''} := Val(Intg 1);; - {''l2'':Class ''L'' := new ''L''; - Var ''l2''\ ''F''{''L''} := Val(Intg 2);; - {''l3'':Class ''L'' := new ''L''; - Var ''l3''\ ''F''{''L''} := Val(Intg 3);; - {''l4'':Class ''L'' := new ''L''; - Var ''l4''\ ''F''{''L''} := Val(Intg 4);; - Var ''l1''\''app''([Var ''l2'']);; - Var ''l1''\''app''([Var ''l3'']);; - Var ''l1''\''app''([Var ''l4''])}}}}" - -definition testExpr1 ::"expr" -where - "testExpr1 == Val(Intg 5)" -definition testExpr2 ::"expr" -where - "testExpr2 == BinOp (Val(Intg 5)) Add (Val(Intg 6))" -definition testExpr3 ::"expr" -where - "testExpr3 == BinOp (Var ''V'') Add (Val(Intg 6))" -definition testExpr4 ::"expr" -where - "testExpr4 == ''V'' := Val(Intg 6)" -definition testExpr5 ::"expr" -where - "testExpr5 == new ''Object'';; {''V'':(Class ''C'') := new ''C''; Var ''V''\''F''{''C''} := Val(Intg 42)}" -definition testExpr6 ::"expr" -where - "testExpr6 == {''V'':(Class ''I'') := new ''I''; Var ''V''\''mult''([Val(Intg 40),Val(Intg 4)])}" - -definition mb_isNull:: "expr" -where - "mb_isNull == Var this \ ''test''{''A''} \Eq\ null " - -definition mb_add:: "expr" -where - "mb_add == (Var this \ ''int''{''A''} :=( Var this \ ''int''{''A''} \Add\ Var ''i''));; (Var this \ ''int''{''A''})" - -definition mb_mult_cond:: "expr" -where - "mb_mult_cond == (Var ''j'' \Eq\ Val (Intg 0)) \Eq\ Val (Bool False)" - -definition mb_mult_block:: "expr" -where - "mb_mult_block == ''temp'':=(Var ''temp'' \Add\ Var ''i'');;''j'':=(Var ''j'' \Add\ Val (Intg (- 1)))" - -definition mb_mult:: "expr" -where - "mb_mult == {''temp'':Integer:=Val (Intg 0); While (mb_mult_cond) mb_mult_block;; ( Var this \ ''int''{''A''} := Var ''temp'';; Var ''temp'' )}" - -definition classA:: "J_mb cdecl" -where - "classA == - (''A'', Object, - [(''int'',NonStatic,Integer), - (''test'',NonStatic,Class ''A'') ], - [(''isNull'',NonStatic,[],Boolean,[], mb_isNull), - (''add'',NonStatic,[Integer],Integer,[''i''], mb_add), - (''mult'',NonStatic,[Integer,Integer],Integer,[''i'',''j''], mb_mult) ])" - - -definition testExpr_ClassA:: "expr" -where - "testExpr_ClassA == - {''A1'':Class ''A'':= new ''A''; - {''A2'':Class ''A'':= new ''A''; - {''testint'':Integer:= Val (Intg 5); - (Var ''A2''\ ''int''{''A''} := (Var ''A1''\ ''add''([Var ''testint''])));; - (Var ''A2''\ ''int''{''A''} := (Var ''A1''\ ''add''([Var ''testint''])));; - Var ''A2''\ ''mult''([Var ''A2''\ ''int''{''A''}, Var ''testint'']) }}}" - -end diff --git a/thys/JinjaDCI/J/execute_Bigstep.thy b/thys/JinjaDCI/J/execute_Bigstep.thy deleted file mode 100644 --- a/thys/JinjaDCI/J/execute_Bigstep.thy +++ /dev/null @@ -1,557 +0,0 @@ -(* Title: Jinja/J/execute_Bigstep.thy - Author: Tobias Nipkow - Copyright 2004 Technische Universitaet Muenchen - Expanded to include statics by Susannah Mansky - 2017, UIUC -*) - -section \ Code Generation For BigStep \ - -theory execute_Bigstep -imports - BigStep Examples - "HOL-Library.Code_Target_Numeral" -begin - -definition not_Done :: "cname \ sheap \ bool" where -"not_Done C sh \ sh C = None \ (\sfs i. sh C = Some(sfs,i) \ i \ Done)" - -lemma not_Done_conv: - "(\sfs. sh C = Some(sfs,Done)) = (not_Done C sh)" -apply(unfold not_Done_def) -apply(case_tac "sh C", simp) apply (rename_tac sfsi) -apply(case_tac sfsi, clarsimp) -done - -(* HERE: MOVE - MethodsAndFields? *) -(* HERE: to be computable, this also needs a def for when has_fields DNE: - such a thing exists in counter-form in MaF, but uses subcls/requires - something to be true of something above C - there are only finite things - above C, but this still might require some work (like proving finiteness *) -definition no_field :: "J_prog \ cname \ vname \ cname \ bool" where -"no_field P C F D \ (\FDTs. \ P \ C has_fields FDTs) \ (\FDTs. P \ C has_fields FDTs \ - ((map_of (map (\((F,D),b,T). (F,(D,b,T))) FDTs) F = None) \ - (\D' b T. D \ D' \ map_of (map (\((F,D),b,T). (F,(D,b,T))) FDTs) F = Some(D',b,T))))" - -lemma no_field_conv: - "(\(\b t. P \ C sees F,b:t in D)) = no_field P C F D" -apply(unfold no_field_def sees_field_def) -apply(case_tac "\FDTs. P \ C has_fields FDTs") - defer apply simp -apply(rule iffI) - apply clarsimp - apply(erule_tac x=FDTs in allE, clarsimp) apply(rename_tac D' b' t') - apply(erule disjE, simp) - apply fastforce -apply clarsimp -apply(erule disjE,simp) -apply clarsimp -apply((drule (1) has_fields_fun)+, simp) -done - -inductive map_val :: "expr list \ val list \ bool" -where - Nil: "map_val [] []" -| Cons: "map_val xs ys \ map_val (Val y # xs) (y # ys)" - -inductive map_val2 :: "expr list \ val list \ expr list \ bool" -where - Nil: "map_val2 [] [] []" -| Cons: "map_val2 xs ys zs \ map_val2 (Val y # xs) (y # ys) zs" -| Throw: "map_val2 (throw e # xs) [] (throw e # xs)" - -theorem map_val_conv: "(xs = map Val ys) = map_val xs ys" -(*<*) -proof - - have "\ys. xs = map Val ys \ map_val xs ys" - apply (induct xs type:list) - apply (case_tac ys) - apply simp - apply (rule map_val.Nil) - apply simp - apply (case_tac ys) - apply simp - apply simp - apply (erule conjE) - apply (rule map_val.Cons) - apply simp - done - moreover have "map_val xs ys \ xs = map Val ys" - by (erule map_val.induct) simp+ - ultimately show ?thesis .. -qed -(*>*) - -theorem map_val2_conv: - "(xs = map Val ys @ throw e # zs) = map_val2 xs ys (throw e # zs)" -(*<*) -proof - - have "\ys. xs = map Val ys @ throw e # zs \ map_val2 xs ys (throw e # zs)" - apply (induct xs type:list) - apply (case_tac ys) - apply simp - apply simp - apply simp - apply (case_tac ys) - apply simp - apply (rule map_val2.Throw) - apply simp - apply (rule map_val2.Cons) - apply simp - done - moreover have "map_val2 xs ys (throw e # zs) \ xs = map Val ys @ throw e # zs" - by (erule map_val2.induct) simp+ - ultimately show ?thesis .. -qed -(*>*) - -lemma NewInit2: - "\ not_Done C sh; P \ \C,(h,sh)\ \\<^sub>i \None,(h',sh')\; - new_Addr h' = Some a; h'' = h'(a\blank P C) \ - \ P \ \new C,(h,l,sh)\ \ \addr a,(h'',l,sh')\" -apply(rule NewInit) -apply(simp add: not_Done_conv[symmetric]) -apply(assumption+) -done - -lemma NewInitFail2: - "\ not_Done C sh; P \ \C,(h,sh)\ \\<^sub>i \Some e',(h',sh')\ \ - \ P \ \new C,(h,l,sh)\ \ \e',(h',l,sh')\" -apply(rule NewInitFail) -apply(simp add: not_Done_conv[symmetric]) -apply(assumption+) -done - -lemma NewInitOOM2: - "\ not_Done C sh; P \ \C,(h,sh)\ \\<^sub>i \None,(h',sh')\; - new_Addr h = None \ - \ P \ \new C,(h,l,sh)\ \ \THROW OutOfMemory,(h',l,sh')\" -apply(rule NewInitOOM) -apply(simp add: not_Done_conv[symmetric]) -apply(assumption+) -done - -(*| FAccNone: - "\ P \ \e,s\<^sub>0\ \ \addr a,(h,l,sh)\; h a = Some(C,fs); - \(\b t. P \ C sees F,b:t in D) \ - \ P \ \e\F{D},s\<^sub>0\ \ \THROW NoSuchFieldError,(h,l,sh)\"*) - -lemma SFAccInit2: - "\ P \ C sees F,Static:t in D; - not_Done D sh; P \ \D,(h,sh)\ \\<^sub>i \None,(h',sh')\; - sh' D = Some (sfs',Done); sfs' F = Some v \ - \ P \ \C\\<^sub>sF{D},(h,l,sh)\ \ \Val v,(h',l,sh')\" -apply(rule SFAccInit, assumption+) -apply(simp add: not_Done_conv[symmetric]) -apply(assumption+) -done - -lemma SFAccInitFail2: - "\ P \ C sees F,Static:t in D; - not_Done D sh; P \ \D,(h,sh)\ \\<^sub>i \Some e',(h',sh')\ \ - \ P \ \C\\<^sub>sF{D},(h,l,sh)\ \ \e',(h',l,sh')\" -apply(rule SFAccInitFail, assumption+) -apply(simp add: not_Done_conv[symmetric]) -apply(assumption+) -done - -(*| SFAccNone: - "\ \(\b t. P \ C sees F,b:t in D) \ - \ P \ \C\\<^sub>sF{D},s\ \ \THROW NoSuchFieldError,s\" - -| FAssNone: - "\ P \ \e\<^sub>1,s\<^sub>0\ \ \addr a,s\<^sub>1\; P \ \e\<^sub>2,s\<^sub>1\ \ \Val v,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\; - h\<^sub>2 a = Some(C,fs); \(\b t. P \ C sees F,b:t in D) \ - \ P \ \e\<^sub>1\F{D}:=e\<^sub>2,s\<^sub>0\ \ \THROW NoSuchFieldError,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\"*) - -lemma SFAssInit2: - "\ P \ \e\<^sub>2,s\<^sub>0\ \ \Val v,(h\<^sub>1,l\<^sub>1,sh\<^sub>1)\; - P \ C sees F,Static:t in D; - not_Done D sh\<^sub>1; P \ \D,(h\<^sub>1,sh\<^sub>1)\ \\<^sub>i \None,(h\<^sub>2,sh\<^sub>2)\; - sh\<^sub>2 D = Some(sfs\<^sub>2,Done); sfs\<^sub>2' = sfs\<^sub>2(F\v); sh\<^sub>2' = sh\<^sub>2(D\(sfs\<^sub>2',Done)) \ - \ P \ \C\\<^sub>sF{D}:=e\<^sub>2,s\<^sub>0\ \ \Val v,(h\<^sub>2,l\<^sub>1,sh\<^sub>2')\" -apply(rule SFAssInit, assumption+) -apply(simp add: not_Done_conv[symmetric]) -apply(assumption+) -done - -lemma SFAssInitFail2: - "\ P \ \e\<^sub>2,s\<^sub>0\ \ \Val v,(h\<^sub>1,l\<^sub>1,sh\<^sub>1)\; - P \ C sees F,Static:t in D; - not_Done D sh\<^sub>1; P \ \D,(h\<^sub>1,sh\<^sub>1)\ \\<^sub>i \Some e',(h\<^sub>2,sh\<^sub>2)\ \ - \ P \ \C\\<^sub>sF{D}:=e\<^sub>2,s\<^sub>0\ \ \e',(h\<^sub>2,l\<^sub>1,sh\<^sub>2)\" -apply(rule SFAssInitFail, assumption+) -apply(simp add: not_Done_conv[symmetric]) -apply(assumption+) -done - -(*| SFAssNone: - "\ P \ \e\<^sub>2,s\<^sub>0\ \ \Val v,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\; - \(\b t. P \ C sees F,b:t in D) \ - \ P \ \C\\<^sub>sF{D}:=e\<^sub>2,s\<^sub>0\ \ \THROW NoSuchFieldError,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\"*) - -lemma CallNull2: - "\ P \ \e,s\<^sub>0\ \ \null,s\<^sub>1\; P \ \ps,s\<^sub>1\ [\] \evs,s\<^sub>2\; map_val evs vs \ - \ P \ \e\M(ps),s\<^sub>0\ \ \THROW NullPointer,s\<^sub>2\" -apply(rule CallNull, assumption+) -apply(simp add: map_val_conv[symmetric]) -done - -lemma CallNone2: - "\ P \ \e,s\<^sub>0\ \ \addr a,s\<^sub>1\; P \ \ps,s\<^sub>1\ [\] \evs,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\; map_val evs vs; - h\<^sub>2 a = Some(C,fs); \(\b Ts T m D. P \ C sees M,b:Ts\T = m in D) \ - \ P \ \e\M(ps),s\<^sub>0\ \ \THROW NoSuchMethodError,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\" -apply(rule CallNone, assumption+) -apply(simp add: map_val_conv[symmetric]) -apply(assumption+) -done - -lemma CallStatic2: - "\ P \ \e,s\<^sub>0\ \ \addr a,s\<^sub>1\; P \ \ps,s\<^sub>1\ [\] \evs,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\; map_val evs vs; - h\<^sub>2 a = Some(C,fs); P \ C sees M,Static:Ts\T = m in D \ - \ P \ \e\M(ps),s\<^sub>0\ \ \THROW IncompatibleClassChangeError,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\" -apply(rule CallStatic, assumption+) -apply(simp add: map_val_conv[symmetric]) -apply(assumption+) -done - -lemma CallParamsThrow2: - "\ P \ \e,s\<^sub>0\ \ \Val v,s\<^sub>1\; P \ \es,s\<^sub>1\ [\] \evs,s\<^sub>2\; - map_val2 evs vs (throw ex # es'') \ - \ P \ \e\M(es),s\<^sub>0\ \ \throw ex,s\<^sub>2\" -apply(rule eval_evals_init_rinit.CallParamsThrow, assumption+) -apply(simp add: map_val2_conv[symmetric]) -done - -lemma Call2: - "\ P \ \e,s\<^sub>0\ \ \addr a,s\<^sub>1\; P \ \ps,s\<^sub>1\ [\] \evs,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\; - map_val evs vs; - h\<^sub>2 a = Some(C,fs); P \ C sees M,NonStatic:Ts\T = (pns,body) in D; - length vs = length pns; l\<^sub>2' = [this\Addr a, pns[\]vs]; - P \ \body,(h\<^sub>2,l\<^sub>2',sh\<^sub>2)\ \ \e',(h\<^sub>3,l\<^sub>3,sh\<^sub>3)\ \ - \ P \ \e\M(ps),s\<^sub>0\ \ \e',(h\<^sub>3,l\<^sub>2,sh\<^sub>3)\" -apply(rule Call, assumption+) -apply(simp add: map_val_conv[symmetric]) -apply assumption+ -done - -lemma SCallParamsThrow2: - "\ P \ \es,s\<^sub>0\ [\] \evs,s\<^sub>2\; - map_val2 evs vs (throw ex # es'') \ - \ P \ \C\\<^sub>sM(es),s\<^sub>0\ \ \throw ex,s\<^sub>2\" -apply(rule SCallParamsThrow) -apply(simp add: map_val2_conv[symmetric]) -done - -lemma SCallNone2: - "\ P \ \ps,s\<^sub>0\ [\] \evs,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\; map_val evs vs; - \(\b Ts T m D. P \ C sees M,b:Ts\T = m in D) \ - \ P \ \C\\<^sub>sM(ps),s\<^sub>0\ \ \THROW NoSuchMethodError,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\" -apply(rule SCallNone) -apply(simp add: map_val_conv[symmetric]) -apply assumption+ -done - -lemma SCallNonStatic2: - "\ P \ \ps,s\<^sub>0\ [\] \evs,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\; map_val evs vs; - P \ C sees M,NonStatic:Ts\T = m in D; - sh\<^sub>2 D = Some(sfs,Done) \ - \ P \ \C\\<^sub>sM(ps),s\<^sub>0\ \ \THROW IncompatibleClassChangeError,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\" -apply(rule SCallNonStatic) -apply(simp add: map_val_conv[symmetric]) -apply assumption+ -done - -lemma SCallInit2: - "\ P \ \ps,s\<^sub>0\ [\] \evs,(h\<^sub>1,l\<^sub>1,sh\<^sub>1)\; map_val evs vs; - P \ C sees M,Static:Ts\T = (pns,body) in D; - not_Done D sh\<^sub>1; - P \ \D,(h\<^sub>1,sh\<^sub>1)\ \\<^sub>i \None,(h\<^sub>2,sh\<^sub>2)\; - length vs = length pns; l\<^sub>2' = [pns[\]vs]; - P \ \body,(h\<^sub>2,l\<^sub>2',sh\<^sub>2)\ \ \e',(h\<^sub>3,l\<^sub>3,sh\<^sub>3)\ \ - \ P \ \C\\<^sub>sM(ps),s\<^sub>0\ \ \e',(h\<^sub>3,l\<^sub>1,sh\<^sub>3)\" -apply(rule SCallInit) -apply(simp add: map_val_conv[symmetric]) -apply assumption -apply(clarsimp simp: not_Done_def) -apply assumption+ -done - -lemma SCallInitFail2: - "\ P \ \ps,s\<^sub>0\ [\] \evs,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\; map_val evs vs; - P \ C sees M,Static:Ts\T = (pns,body) in D; - not_Done D sh\<^sub>2; - P \ \D,(h\<^sub>2,sh\<^sub>2)\ \\<^sub>i \Some e',(h\<^sub>3,sh\<^sub>3)\ \ - \ P \ \C\\<^sub>sM(ps),s\<^sub>0\ \ \e',(h\<^sub>3,l\<^sub>2,sh\<^sub>3)\" -apply(rule SCallInitFail) -apply(simp add: map_val_conv[symmetric]) -apply assumption -apply(clarsimp simp: not_Done_def) -apply assumption+ -done - -lemma SCall2: - "\ P \ \ps,s\<^sub>0\ [\] \evs,(h\<^sub>2,l\<^sub>2,sh\<^sub>2)\; - map_val evs vs; - P \ C sees M,Static:Ts\T = (pns,body) in D; - sh\<^sub>2 D = Some(sfs,Done); - length vs = length pns; l\<^sub>2' = [pns[\]vs]; - P \ \body,(h\<^sub>2,l\<^sub>2',sh\<^sub>2)\ \ \e',(h\<^sub>3,l\<^sub>3,sh\<^sub>3)\ \ - \ P \ \C\\<^sub>sM(ps),s\<^sub>0\ \ \e',(h\<^sub>3,l\<^sub>2,sh\<^sub>3)\" -apply(rule SCall) -apply(simp add: map_val_conv[symmetric]) -apply assumption+ -done - -declare not_Done_def [code_pred_def] - -code_pred - (modes: i \ o \ bool) - map_val -. - -code_pred - (modes: i \ o \ o \ bool) - map_val2 -. - -lemmas [code_pred_intro] = - eval_evals_init_rinit.New eval_evals_init_rinit.NewOOM - eval_evals_init_rinit.Cast eval_evals_init_rinit.CastNull eval_evals_init_rinit.CastFail eval_evals_init_rinit.CastThrow - eval_evals_init_rinit.Val eval_evals_init_rinit.Var - eval_evals_init_rinit.BinOp eval_evals_init_rinit.BinOpThrow1 eval_evals_init_rinit.BinOpThrow2 - eval_evals_init_rinit.LAss eval_evals_init_rinit.LAssThrow - eval_evals_init_rinit.FAcc eval_evals_init_rinit.FAccNull eval_evals_init_rinit.FAccThrow - eval_evals_init_rinit.FAccNone eval_evals_init_rinit.FAccStatic - eval_evals_init_rinit.SFAcc eval_evals_init_rinit.SFAccNone eval_evals_init_rinit.SFAccNonStatic - eval_evals_init_rinit.FAss eval_evals_init_rinit.FAssNull - eval_evals_init_rinit.FAssThrow1 eval_evals_init_rinit.FAssThrow2 - eval_evals_init_rinit.FAssNone eval_evals_init_rinit.FAssStatic - eval_evals_init_rinit.SFAss eval_evals_init_rinit.SFAssNone eval_evals_init_rinit.SFAssNonStatic - eval_evals_init_rinit.CallObjThrow - -declare NewInit2 [code_pred_intro NewInit2] -declare NewInitFail2 [code_pred_intro NewInitFail2] -declare NewInitOOM2 [code_pred_intro NewInitOOM2] -declare SFAccInit2 [code_pred_intro SFAccInit2] -declare SFAccInitFail2 [code_pred_intro SFAccInitFail2] -declare SFAssInit2 [code_pred_intro SFAssInit2] -declare SFAssInitFail2 [code_pred_intro SFAssInitFail2] -declare CallNull2 [code_pred_intro CallNull2] -declare CallParamsThrow2 [code_pred_intro CallParamsThrow2] -declare CallNone2 [code_pred_intro CallNone2] -declare CallStatic2 [code_pred_intro CallStatic2] -declare Call2 [code_pred_intro Call2] -declare SCallParamsThrow2 [code_pred_intro SCallParamsThrow2] -declare SCallNone2 [code_pred_intro SCallNone2] -declare SCallNonStatic2 [code_pred_intro SCallNonStatic2] -declare SCallInit2 [code_pred_intro SCallInit2] -declare SCallInitFail2 [code_pred_intro SCallInitFail2] -declare SCall2 [code_pred_intro SCall2] - -lemmas [code_pred_intro] = - eval_evals_init_rinit.Block - eval_evals_init_rinit.Seq eval_evals_init_rinit.SeqThrow - eval_evals_init_rinit.CondT eval_evals_init_rinit.CondF eval_evals_init_rinit.CondThrow - eval_evals_init_rinit.WhileF eval_evals_init_rinit.WhileT - eval_evals_init_rinit.WhileCondThrow - -declare eval_evals_init_rinit.WhileBodyThrow [code_pred_intro WhileBodyThrow2] - -lemmas [code_pred_intro] = - eval_evals_init_rinit.Throw eval_evals_init_rinit.ThrowNull - eval_evals_init_rinit.ThrowThrow - eval_evals_init_rinit.Try eval_evals_init_rinit.TryCatch eval_evals_init_rinit.TryThrow - eval_evals_init_rinit.Nil eval_evals_init_rinit.Cons eval_evals_init_rinit.ConsThrow - -lemmas [code_pred_intro] = - eval_evals_init_rinit.InitNone eval_evals_init_rinit.InitDone - eval_evals_init_rinit.InitProcessing eval_evals_init_rinit.InitError - eval_evals_init_rinit.InitObject eval_evals_init_rinit.InitNonObject eval_evals_init_rinit.InitFail - eval_evals_init_rinit.RInit eval_evals_init_rinit.RinitFail - -code_pred - (modes: i \ i \ i \ o \ o \ bool as execute) -(* [show_steps, - show_proof_trace, - show_intermediate_results, - show_mode_inference, - show_modes, - show_compilation, - show_invalid_clauses]*) - eval -proof - - case eval - from eval.prems show thesis - proof(cases (no_simp)) - case NewInit thus ?thesis - by-(rule eval.NewInit2[OF refl],simp_all add: not_Done_conv[symmetric]) - next - case NewInitFail thus ?thesis - by-(rule eval.NewInitFail2[OF refl],simp_all add: not_Done_conv[symmetric]) - next - case NewInitOOM thus ?thesis - by-(rule eval.NewInitOOM2[OF refl],simp_all add: not_Done_conv[symmetric]) - next - case SFAccInit thus ?thesis - using eval.SFAccInit2 not_Done_conv by auto - next - case SFAccInitFail thus ?thesis - by-(rule eval.SFAccInitFail2[OF refl],simp_all add: not_Done_conv[symmetric]) - next - case SFAssInit thus ?thesis - using eval.SFAssInit2 not_Done_conv by auto - next - case SFAssInitFail thus ?thesis - by-(rule eval.SFAssInitFail2[OF refl],simp_all add: not_Done_conv[symmetric]) - next - case CallNull thus ?thesis - by(rule eval.CallNull2[OF refl])(simp add: map_val_conv[symmetric]) - next - case CallParamsThrow thus ?thesis - by(rule eval.CallParamsThrow2[OF refl])(simp add: map_val2_conv[symmetric]) - next - case CallNone thus ?thesis - using eval.CallNone2[OF refl] map_val_conv[symmetric] by auto - next - case CallStatic thus ?thesis - using eval.CallStatic2 map_val_conv by blast - next - case Call thus ?thesis - by -(rule eval.Call2[OF refl], simp_all add: map_val_conv[symmetric]) - next - case SCallParamsThrow thus ?thesis - by(rule eval.SCallParamsThrow2[OF refl])(simp add: map_val2_conv[symmetric]) - next - case SCallNone thus ?thesis - by -(rule eval.SCallNone2[OF refl], simp_all add: map_val_conv[symmetric]) - next - case SCallNonStatic thus ?thesis - using eval.SCallNonStatic2 map_val_conv by blast - next - case SCallInit thus ?thesis - by -(rule eval.SCallInit2[OF refl], simp_all add: map_val_conv[symmetric] not_Done_conv[symmetric]) - next - case SCallInitFail thus ?thesis - by -(rule eval.SCallInitFail2[OF refl], simp_all add: map_val_conv[symmetric] not_Done_conv[symmetric]) - next - case SCall thus ?thesis - by -(rule eval.SCall2[OF refl], simp_all add: map_val_conv[symmetric]) - next - case WhileBodyThrow thus ?thesis by(rule eval.WhileBodyThrow2[OF refl]) - qed(assumption|erule (4) eval.that[OF refl]|erule (3) eval.that[OF refl])+ -next - case evals - from evals.prems show thesis - by(cases (no_simp))(assumption|erule (3) evals.that[OF refl])+ -next - case init - from init.prems show thesis - by(cases (no_simp))(assumption|erule (3) init.that[OF refl])+ -next - case rinit - from rinit.prems show thesis - by(cases (no_simp))(assumption|erule (3) rinit.that[OF refl])+ -qed - -notation execute ("_ \ ((1\_,/_\) \/ \'_, '_\)" [51,0,0] 81) - -definition "test1 = [] \ \testExpr1,(empty,empty,empty)\ \ \_,_\" -definition "test2 = [] \ \testExpr2,(empty,empty,empty)\ \ \_,_\" -definition "test3 = [] \ \testExpr3,(empty,empty(''V''\Intg 77),empty)\ \ \_,_\" -definition "test4 = [] \ \testExpr4,(empty,empty,empty)\ \ \_,_\" -definition "test5 = [(''Object'',('''',[],[])),(''C'',(''Object'',[(''F'',NonStatic,Integer)],[]))] \ \testExpr5,(empty,empty,empty)\ \ \_,_\" -definition "test6 = [(''Object'',('''',[],[])), classI] \ \testExpr6,(empty,empty,empty)\ \ \_,_\" - -definition "V = ''V''" -definition "C = ''C''" -definition "F = ''F''" - -(* HERE: MOVE THIS - also, don't really need *) -(* -lemma UNIV_staticb: "UNIV = {Static, NonStatic}" - by (auto intro: staticb.exhaust) - -instantiation staticb :: enum -begin - -definition - "enum_staticb = [Static, NonStatic]" - -definition - "enum_all_staticb P \ P NonStatic \ P Static" - -definition - "enum_ex_staticb P \ P NonStatic \ P Static" - -instance proof -qed (auto simp only: enum_staticb_def enum_all_staticb_def enum_ex_staticb_def UNIV_staticb, simp_all) - -end -*) - -ML_val \ - val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 5)), _), _) = Predicate.yield @{code test1}; - val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 11)), _), _) = Predicate.yield @{code test2}; - val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 83)), _), _) = Predicate.yield @{code test3}; - - val SOME ((_, (_, l, _)), _) = Predicate.yield @{code test4}; - val SOME (@{code Intg} (@{code int_of_integer} 6)) = l @{code V}; - - val SOME ((_, (h, _)), _) = Predicate.yield @{code test5}; - val SOME (c, fs) = h (@{code nat_of_integer} 1); - val SOME (obj, _) = h (@{code nat_of_integer} 0); - val SOME (@{code Intg} i) = fs (@{code F}, @{code C}); - @{assert} (c = @{code C} andalso obj = @{code Object} andalso i = @{code int_of_integer} 42); - - val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 160)), _), _) = Predicate.yield @{code test6}; -\ - -definition "test7 = [classObject, classL] \ \testExpr_BuildList, (empty,empty,empty)\ \ \_,_\" - -definition "L = ''L''" -definition "N = ''N''" - -ML_val \ - val SOME ((_, (h, _)), _) = Predicate.yield @{code test7}; - val SOME (_, fs1) = h (@{code nat_of_integer} 0); - val SOME (_, fs2) = h (@{code nat_of_integer} 1); - val SOME (_, fs3) = h (@{code nat_of_integer} 2); - val SOME (_, fs4) = h (@{code nat_of_integer} 3); - - val F = @{code "F"}; - val L = @{code "L"}; - val N = @{code "N"}; - - @{assert} (fs1 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 1)) andalso - fs1 (N, L) = SOME (@{code Addr} (@{code nat_of_integer} 1)) andalso - fs2 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 2)) andalso - fs2 (N, L) = SOME (@{code Addr} (@{code nat_of_integer} 2)) andalso - fs3 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 3)) andalso - fs3 (N, L) = SOME (@{code Addr} (@{code nat_of_integer} 3)) andalso - fs4 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 4)) andalso - fs4 (N, L) = SOME @{code Null}); -\ - -definition "test8 = [classObject, classA] \ \testExpr_ClassA, (empty,empty,empty)\ \ \_,_\" -definition "i = ''int''" -definition "t = ''test''" -definition "A = ''A''" - -ML_val \ - val SOME ((_, (h, l)), _) = Predicate.yield @{code test8}; - val SOME (_, fs1) = h (@{code nat_of_integer} 0); - val SOME (_, fs2) = h (@{code nat_of_integer} 1); - - val i = @{code "i"}; - val t = @{code "t"}; - val A = @{code "A"}; - - @{assert} (fs1 (i, A) = SOME (@{code Intg} (@{code int_of_integer} 10)) andalso - fs1 (t, A) = SOME @{code Null} andalso - fs2 (i, A) = SOME (@{code Intg} (@{code int_of_integer} 50)) andalso - fs2 (t, A) = SOME @{code Null}); -\ - -end - diff --git a/thys/JinjaDCI/J/execute_WellType.thy b/thys/JinjaDCI/J/execute_WellType.thy deleted file mode 100644 --- a/thys/JinjaDCI/J/execute_WellType.thy +++ /dev/null @@ -1,125 +0,0 @@ -(* Title: Jinja/J/execute_WellType.thy - Author: Christoph Petzinger - Copyright 2004 Technische Universitaet Muenchen -*) -(* - Expanded to include support for static fields and methods. - Susannah Mansky - 2017, UIUC -*) - -section \ Code Generation For WellType \ - -theory execute_WellType -imports - WellType Examples -begin - -(* Replace WT_WTs.WTCond with new intros WT_WTs.WTCond1 and WT_WTs.WTCond2 *) - -lemma WTCond1: - "\P,E \ e :: Boolean; P,E \ e\<^sub>1::T\<^sub>1; P,E \ e\<^sub>2::T\<^sub>2; P \ T\<^sub>1 \ T\<^sub>2; - P \ T\<^sub>2 \ T\<^sub>1 \ T\<^sub>2 = T\<^sub>1 \ \ P,E \ if (e) e\<^sub>1 else e\<^sub>2 :: T\<^sub>2" -by (fastforce) - -lemma WTCond2: - "\P,E \ e :: Boolean; P,E \ e\<^sub>1::T\<^sub>1; P,E \ e\<^sub>2::T\<^sub>2; P \ T\<^sub>2 \ T\<^sub>1; - P \ T\<^sub>1 \ T\<^sub>2 \ T\<^sub>1 = T\<^sub>2 \ \ P,E \ if (e) e\<^sub>1 else e\<^sub>2 :: T\<^sub>1" -by (fastforce) - -lemmas [code_pred_intro] = - WT_WTs.WTNew - WT_WTs.WTCast - WT_WTs.WTVal - WT_WTs.WTVar - WT_WTs.WTBinOpEq - WT_WTs.WTBinOpAdd - WT_WTs.WTLAss - WT_WTs.WTFAcc - WT_WTs.WTSFAcc - WT_WTs.WTFAss - WT_WTs.WTSFAss - WT_WTs.WTCall - WT_WTs.WTSCall - WT_WTs.WTBlock - WT_WTs.WTSeq - -declare - WTCond1 [code_pred_intro WTCond1] - WTCond2 [code_pred_intro WTCond2] - -lemmas [code_pred_intro] = - WT_WTs.WTWhile - WT_WTs.WTThrow - WT_WTs.WTTry - WT_WTs.WTNil - WT_WTs.WTCons - -code_pred - (modes: i \ i \ i \ i \ bool as type_check, i \ i \ i \ o \ bool as infer_type) - WT -proof - - case WT - from WT.prems show thesis - proof(cases (no_simp)) - case (WTCond E e e1 T1 e2 T2 T) - from `x \ T1 \ T2 \ x \ T2 \ T1` show thesis - proof - assume "x \ T1 \ T2" - with `x \ T1 \ T2 \ T = T2` have "T = T2" .. - from `xa = E` `xb = if (e) e1 else e2` `xc = T` `x,E \ e :: Boolean` - `x,E \ e1 :: T1` `x,E \ e2 :: T2` `x \ T1 \ T2` `x \ T2 \ T1 \ T = T1` - show ?thesis unfolding `T = T2` by(rule WT.WTCond1[OF refl]) - next - assume "x \ T2 \ T1" - with `x \ T2 \ T1 \ T = T1` have "T = T1" .. - from `xa = E` `xb = if (e) e1 else e2` `xc = T` `x,E \ e :: Boolean` - `x,E \ e1 :: T1` `x,E \ e2 :: T2` `x \ T2 \ T1` `x \ T1 \ T2 \ T = T2` - show ?thesis unfolding `T = T1` by(rule WT.WTCond2[OF refl]) - qed - qed(assumption|erule (2) WT.that[OF refl])+ -next - case WTs - from WTs.prems show thesis - by(cases (no_simp))(assumption|erule (2) WTs.that[OF refl])+ -qed - -notation infer_type ("_,_ \ _ :: '_" [51,51,51]100) - -definition test1 where "test1 = [],empty \ testExpr1 :: _" -definition test2 where "test2 = [], empty \ testExpr2 :: _" -definition test3 where "test3 = [], empty(''V'' \ Integer) \ testExpr3 :: _" -definition test4 where "test4 = [], empty(''V'' \ Integer) \ testExpr4 :: _" -definition test5 where "test5 = [classObject, (''C'',(''Object'',[(''F'',NonStatic,Integer)],[]))], empty \ testExpr5 :: _" -definition test6 where "test6 = [classObject, classI], empty \ testExpr6 :: _" - -ML_val \ - val SOME(@{code Integer}, _) = Predicate.yield @{code test1}; - val SOME(@{code Integer}, _) = Predicate.yield @{code test2}; - val SOME(@{code Integer}, _) = Predicate.yield @{code test3}; - val SOME(@{code Void}, _) = Predicate.yield @{code test4}; - val SOME(@{code Void}, _) = Predicate.yield @{code test5}; - val SOME(@{code Integer}, _) = Predicate.yield @{code test6}; -\ - -definition testmb_isNull where "testmb_isNull = [classObject, classA], empty([this] [\] [Class ''A'']) \ mb_isNull :: _" -definition testmb_add where "testmb_add = [classObject, classA], empty([this,''i''] [\] [Class ''A'',Integer]) \ mb_add :: _" -definition testmb_mult_cond where "testmb_mult_cond = [classObject, classA], empty([this,''j''] [\] [Class ''A'',Integer]) \ mb_mult_cond :: _" -definition testmb_mult_block where "testmb_mult_block = [classObject, classA], empty([this,''i'',''j'',''temp''] [\] [Class ''A'',Integer,Integer,Integer]) \ mb_mult_block :: _" -definition testmb_mult where "testmb_mult = [classObject, classA], empty([this,''i'',''j''] [\] [Class ''A'',Integer,Integer]) \ mb_mult :: _" - -ML_val \ - val SOME(@{code Boolean}, _) = Predicate.yield @{code testmb_isNull}; - val SOME(@{code Integer}, _) = Predicate.yield @{code testmb_add}; - val SOME(@{code Boolean}, _) = Predicate.yield @{code testmb_mult_cond}; - val SOME(@{code Void}, _) = Predicate.yield @{code testmb_mult_block}; - val SOME(@{code Integer}, _) = Predicate.yield @{code testmb_mult}; -\ - -definition test where "test = [classObject, classA], empty \ testExpr_ClassA :: _" - -ML_val \ - val SOME(@{code Integer}, _) = Predicate.yield @{code test}; -\ - -end