Theory PhiSem_Variable
chapter ‹Typed Variable›
text ‹This is a generic formalization variables supporting either typed variables or non-typed.
If the formalization is untyped, variables in the formalization can be assigned by values of any type.
You can set the flag φvariable_is_typed to indicate whether the formalization of variables is typed.›
theory PhiSem_Variable
imports Phi_System.Resource_Template PhSm_Ag_Base
abbrevs "<var>" = "𝗏𝖺𝗋"
and "<uninited>" = "𝗎𝗇𝗂𝗇𝗂𝗍𝖾𝖽"
and "<may>" = "𝗆𝖺𝗒"
and "<inited>" = "𝗂𝗇𝗂𝗍𝖾𝖽"
begin
section ‹Semantics›
subsection ‹Models›
subsubsection ‹Resource›
declare [[typedef_overloaded]]
datatype varname = varname nat (type: ‹TY option›)
hide_const (open) type
declare [[typedef_overloaded = false]]
setup ‹Sign.mandatory_path "RES"›
type_synonym Var = ‹varname ⇀ VAL option discrete›
setup ‹Sign.parent_path›
lemma infinite_varname:
‹infinite {k. varname.type k = TY}›
using inj_on_finite[where A = ‹UNIV::nat set› and B = ‹{k. varname.type k = TY}›
and f = ‹λn. varname n TY›]
using inj_def by fastforce
resource_space φvar =
Var :: ‹{vars::RES.Var. finite (dom vars)}› (partial_map_resource ‹(λ_::varname. UNIV :: VAL option discrete set)›)
by (standard, simp, metis domIff notin_range_Some)
hide_fact RES.φvar_res_ax RES.φvar_res_axioms RES.φvar_res_fields_axioms
subsubsection ‹Fiction›
fiction_space φvar =
Var :: ‹RES.Var.basic_fiction ⨾ ℱ_pointwise (λ_. Itself)›
(pointwise_fiction_for_partial_mapping_resource RES.Var ‹(λ_::varname. UNIV :: VAL option discrete set)›)
by (standard; simp add: BI_eq_iff)
section ‹φ-Types›
subsection ‹Variable›
φtype_def Var :: ‹varname ⇒ (VAL option,'a) φ ⇒ (fiction,'a) φ›
where ‹Var vname T ≡ (FIC.Var.φ (vname ❙→ ● (Discrete T)))›
deriving Basic
and Functional_Transformation_Functor
and ‹Gen_Br_Join (Var v) (Var v) (Var v) P True ›
and ‹Identifier_of (Var v T) v (Var v T')›
abbreviation Inited_Var :: ‹varname ⇒ (VAL,'a) φ ⇒ (fiction,'a) φ›
where ‹Inited_Var vname T ≡ Var vname (● T)›
abbreviation Uninited_Var :: ‹varname ⇒ assn› ("𝗎𝗇𝗂𝗇𝗂𝗍𝖾𝖽 𝗏𝖺𝗋[_]" [22] 21)
where ‹Uninited_Var vname ≡ () ⦂ Var vname ○›
abbreviation May_Inited_Var :: ‹varname ⇒ (VAL,'a) φ ⇒ (fiction,'a option) φ›
where ‹May_Inited_Var vname T ≡ Var vname (◒ T)›
subsubsection ‹Syntax›
syntax Inited_Var_ :: ‹logic ⇒ logic› ("𝗏𝖺𝗋[_]")
May_Inited_Var_ :: ‹logic ⇒ logic› ("𝗆𝖺𝗒 𝗂𝗇𝗂𝗍𝖾𝖽 𝗏𝖺𝗋[_]")
ML_file "library/variable_pre.ML"
parse_translation ‹let
fun get_bound ctxt (Const (\<^syntax_const>‹_constrain›, _) $ X $ _) = get_bound ctxt X
| get_bound ctxt (Free (N, _)) = Option.map (K N) (Generic_Variable_Access.lookup_bindings ctxt N)
| get_bound _ _ = NONE
in [
(\<^syntax_const>‹Inited_Var_›, (fn ctxt => fn [v] =>
Const (\<^const_abbrev>‹Inited_Var›, dummyT)
$ (if Generic_Variable_Access.under_context ctxt
then (case get_bound ctxt v
of SOME N => Const (\<^const_name>‹φidentifier›, dummyT) $ Abs (N, dummyT, Term.dummy)
| NONE => v)
else v))),
(\<^syntax_const>‹May_Inited_Var_›, (fn ctxt => fn [v] =>
Const (\<^const_abbrev>‹May_Inited_Var›, dummyT)
$ (if Generic_Variable_Access.under_context ctxt
then (case get_bound ctxt v
of SOME N => Const (\<^const_name>‹φidentifier›, dummyT) $ Abs (N, dummyT, Term.dummy)
| NONE => v)
else v)))
] end›
print_translation ‹let
fun recovery ctxt (Const (\<^syntax_const>‹_free›, _) $ X) = recovery ctxt X
| recovery ctxt (Free (N, TY)) =
(case Phi_Variable.external_name_of ctxt N
of SOME N' => SOME (Free (N', TY))
| _ => NONE)
| recovery ctxt (Var ((N,idx), TY)) =
(case Phi_Variable.external_name_of ctxt N
of SOME N' => SOME (Var ((N',idx), TY))
| _ => NONE)
| recovery _ _ = NONE
fun recovery' ctxt X = case recovery ctxt X of SOME Y => Y | _ => X
in [(\<^const_syntax>‹Inited_Var›, (fn ctxt => fn [a,b] =>
Const(\<^syntax_const>‹Inited_Var_›, dummyT) $ recovery' ctxt a $ b))]
end
›
text ‹The rules below sets-up the IDE-CP synthesis engine, which is independent with our φ-type theory›
lemma [φreason %φsynthesis_parse for
‹Synthesis_Parse (?v::varname) (?Y::?'ret ⇒ assn)›
]:
‹Synthesis_Parse v (λ_. x ⦂ Var v T :: assn)›
unfolding Synthesis_Parse_def ..
lemma [φreason %φsynthesis_parse for
‹Synthesis_Parse (Var _) (?Y::?'ret ⇒ assn)›
]:
‹Synthesis_Parse (Var v) (λ_. x ⦂ Var v T :: assn)›
unfolding Synthesis_Parse_def ..
lemma [φreason %φsynthesis_parse for
‹Synthesis_Parse (Inited_Var _) (?Y::?'ret ⇒ assn)›
]:
‹Synthesis_Parse (Inited_Var v) (λ_. x ⦂ Inited_Var v T :: assn)›
unfolding Synthesis_Parse_def ..
lemma [φreason %φsynthesis_parse for
‹Synthesis_Parse (Uninited_Var _) (?Y::?'ret ⇒ assn)›
]:
‹Synthesis_Parse (Uninited_Var v) (λ_. Uninited_Var v :: assn)›
unfolding Synthesis_Parse_def ..
section ‹Semantic Operations›
subsection ‹Preliminary - Reasoning Process›
subsubsection ‹Local Variable›
definition LOCAL_VAR :: ‹varname ⇒ TY option ⇒ bool›
where ‹LOCAL_VAR v TY ≡ (varname.type v = TY)›
declare [[φreason_default_pattern
‹LOCAL_VAR ?v _› ⇒ ‹LOCAL_VAR ?v _› (100)
]]
φreasoner_group local_var = (1000, [1000,1000]) for (‹LOCAL_VAR vari TY›)
‹storing semantic types of local variables›
subsubsection ‹Aggregate_Mapper that can handle option›
definition ‹index_mode_value_opt idx g = (λu. case u of Some u' ⇒ index_mod_value idx (g o Some) u' | _ ⇒ g None)›
definition φAggregate_Mapper_Opt :: ‹aggregate_path ⇒ (VAL option,'a) φ ⇒ (VAL,'a2) φ ⇒ (VAL option,'b) φ ⇒ (VAL,'b2) φ ⇒ (('b ⇒ 'b2) ⇒ 'a ⇒ 'a2) ⇒ bool›
where ‹φAggregate_Mapper_Opt idx T T' U U' f
⟷ (∀g g'. φType_Mapping U U' g' g ⟶ φType_Mapping T T' (f g') (index_mode_value_opt idx g)) ›
declare [[φreason_default_pattern ‹φAggregate_Mapper_Opt ?idx ?T _ _ _ _ › ⇒ ‹φAggregate_Mapper_Opt ?idx ?T _ _ _ _› (100) ]]
lemma φAggregate_Mapper_Opt_Nil[φreason 1200]:
‹φAggregate_Mapper_Opt [] U U' U U' id›
unfolding φAggregate_Mapper_Opt_def index_mode_value_opt_def
by (clarsimp simp add: φType_Mapping_def split: option.split)
lemma [φreason 1180]:
‹ φAggregate_Mapper idx T T' U U' f
⟹ φAggregate_Mapper_Opt idx (● T) T' (● U) U' f›
unfolding φAggregate_Mapper_Opt_def φAggregate_Mapper_def index_mode_value_opt_def
by (clarsimp simp add: φType_Mapping_def φSome_expn split: option.split)
definition ‹φSemType_opt S TY ⟷ (case TY of Some TY' ⇒ (∀p. Some p ⊨ S ⟶ p ∈ Well_Type TY')
| _ ⇒ S = 1) ›
declare [[φreason_default_pattern ‹φSemType_opt ?S _› ⇒ ‹φSemType_opt ?S _› (100) ]]
lemma [φreason 1200]:
‹ Semantic_Type' (x ⦂ T) TY
⟹ φSemType_opt (x ⦂ ● T) (Some TY)›
unfolding φSemType_opt_def Semantic_Type'_def
by (clarsimp simp add: image_iff subset_iff)
lemma [φreason 1200]:
‹φSemType_opt (x ⦂ ○) None›
unfolding φSemType_opt_def
by (clarsimp simp add: set_eq_iff)
lemma [φreason 1200]:
‹ (⋀x'. 𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 x = Some x' ⟹ Semantic_Type' (x' ⦂ T) TY)
⟹ φSemType_opt (x ⦂ ◒ T) (Some TY)›
unfolding Premise_def φSemType_opt_def Semantic_Type'_def
by (cases ‹x›; clarsimp simp add: image_iff subset_iff φOption.unfold set_eq_iff)
definition ‹
parse_eleidx_input_least1_opt TY input_index sem_idx idx reject
⟷ (case TY of Some TY' ⇒ parse_eleidx_input_least1 TY' input_index sem_idx idx reject
| None ⇒ reject = input_index ∧ sem_idx = [] ∧ idx = [])
›
lemma [φreason %parse_eleidx_input]:
‹ parse_eleidx_input_least1 TY input_index sem_idx idx reject
⟹ parse_eleidx_input_least1_opt (Some TY) input_index sem_idx idx reject›
unfolding parse_eleidx_input_least1_opt_def
parse_eleidx_input_least1_def
by simp
lemma [φreason %parse_eleidx_input]:
‹ parse_eleidx_input_least1_opt None input [] [] input›
unfolding parse_eleidx_input_least1_opt_def
by simp
lemma parse_eleidx_input_least1_opt_NIL:
‹ parse_eleidx_input_least1_opt TY [] [] [] [] ›
unfolding parse_eleidx_input_least1_opt_def
parse_eleidx_input_least1_def
parse_eleidx_input_def
by (cases TY; simp)
subsection ‹Variable Operations›
proc op_get_var:
input ‹x ⦂ 𝗏𝖺𝗋[v] T›
requires [φreason, unfolded Semantic_Type'_def, useful]: ‹Semantic_Type' (x ⦂ T) TY›
and [φreason 10000]: ‹parse_eleidx_input_least1 TY input_index sem_idx idx reject›
and [φreason 10000]: ‹φAggregate_Getter idx T U f›
and [φreason 10000]: ‹report_unprocessed_element_index reject ℰℐℋ𝒪𝒪𝒦_none›
output ‹f x ⦂ 𝗏𝖺𝗅 U❟ x ⦂ 𝗏𝖺𝗋[v] T›
❴
to Itself
unfold Var.unfold
FIC.Var.getter_rule
semantic_assert ‹discrete.dest (φarg.dest 𝗏0) ∈ Some ` Well_Type TY›
semantic_return ‹the (discrete.dest (φarg.dest 𝗏0)) ⊨ (x ⦂ T)›
‹MAKE _(𝗏𝖺𝗋[v] Itself)›
apply_rule op_get_aggregate[where input_index=input_index and sem_idx=sem_idx and spec_idx=idx
and reject=reject, unfolded Is_Aggregate_def]
❵ .
lemma op_get_var0:
‹ Semantic_Type' (x ⦂ T) TY
⟹ 𝗉𝗋𝗈𝖼 op_get_var v TY [] ⦃ x ⦂ 𝗏𝖺𝗋[v] T ⟼ λret. x ⦂ 𝗏𝖺𝗅[ret] T❟ x ⦂ 𝗏𝖺𝗋[v] T ⦄ ›
by (rule op_get_var_φapp[where input_index=‹[]› and idx=‹[]› and reject=‹[]› and f=id, simplified];
simp add: parse_eleidx_input_least1_def
parse_eleidx_input_def
φAggregate_Getter_Nil report_unprocessed_element_index_def)
proc op_set_var:
input ‹y ⦂ 𝗏𝖺𝗅 U'❟ x ⦂ Var v T›
requires [useful]: ‹LOCAL_VAR v TY_var›
and ‹φSemType_opt (x ⦂ T) TY›
and [useful]: ‹pred_option (λTY_var. pred_option ((=) TY_var) TY) TY_var›
and [useful]: ‹parse_eleidx_input_least1_opt TY input_index sem_idx idx reject›
and AMO: ‹φAggregate_Mapper_Opt idx T T' U U' f›
and ‹Semantic_Type U' UY›
and [useful]: ‹pred_option (λTY. is_valid_index_of sem_idx TY UY) TY_var›
and ‹report_unprocessed_element_index reject ℰℐℋ𝒪𝒪𝒦_none›
output ‹f (λ_. y) x ⦂ 𝗏𝖺𝗋[v] T'›
❴
$y semantic_local_value UY
‹v› to Itself
unfold Var.unfold
FIC.Var.getter_rule
semantic_assert ‹
pred_option (λTY_var. pred_option ((=) TY_var) TY ∧ index_type sem_idx TY_var = UY) (varname.type v) ∧
pred_option (λTY'. valid_index TY' sem_idx) TY›
certified by (insert φ; cases TY; cases TY_var;
simp add: parse_eleidx_input_least1_opt_def
parse_eleidx_input_least1_def
parse_eleidx_input_def
is_valid_index_of_def
LOCAL_VAR_def) ；
apply_rule FIC.Var.setter_rule[
where U=‹{Some (discrete (Some (index_mode_value_opt sem_idx (λ_. φarg.dest 𝖺𝗋𝗀1)
(discrete.dest (φarg.dest 𝗏1)))))}›]
‹MAKE _ (𝗏𝖺𝗋[v] Itself)›
❵ certified
by (insert φ AMO; cases TY;
clarsimp simp add: φAggregate_Mapper_Opt_def φType_Mapping_def
parse_eleidx_input_least1_opt_def
parse_eleidx_input_least1_def
parse_eleidx_input_def) .
lemma op_set_var_0:
‹ LOCAL_VAR vari TY_var
⟹ φSemType_opt (x ⦂ U) TY
⟹ pred_option (λTY_var. pred_option ((=) TY_var) TY) TY_var
⟹ Semantic_Type U' UY
⟹ pred_option ((=) UY) TY_var
⟹ 𝗉𝗋𝗈𝖼 op_set_var UY vari TY [] v ⦃ y ⦂ 𝗏𝖺𝗅[v] U'❟ x ⦂ Var vari U ⟼ λ𝗋𝖾𝗍. y ⦂ 𝗏𝖺𝗋[vari] U' ⦄ ›
by (rule op_set_var_φapp[where f=id and input_index=‹[]› and sem_idx=‹[]› and idx=‹[]›
and reject=‹[]› and T=U and T'=U' and U=U and U'=U',
simplified];
simp add: parse_eleidx_input_least1_opt_NIL
φAggregate_Mapper_Opt_Nil report_unprocessed_element_index_def
is_valid_index_of_Nil;
cases TY_var; simp)
proc op_free_var:
requires ‹𝗉𝖺𝗋𝖺𝗆 vari›
and ‹𝖼𝗈𝗇𝖽𝗂𝗍𝗂𝗈𝗇 vari' = vari›
input ‹x ⦂ Var vari' T›
output ‹Void›
❴
to Itself
unfold Var.unfold
apply_rule FIC.Var.setter_rule[where U=‹{None}› and k=‹vari›]
❵ .
proc op_var_scope:
requires ‹𝗉𝖺𝗋𝖺𝗆 TY›
and BLK: ‹⋀vari. LOCAL_VAR vari TY
⟹ 𝗉𝗋𝗈𝖼 F vari ⦃ 𝗎𝗇𝗂𝗇𝗂𝗍𝖾𝖽 𝗏𝖺𝗋[vari]❟ X ⟼ λret. () ⦂ Var vari φAny❟ Y ret ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (λv. () ⦂ Var vari φAny❟ E v) ›
input ‹X›
output ‹Y›
throws E
❴
note LOCAL_VAR_def[φsledgehammer_simps] ；
apply_rule FIC.Var.allocate_rule[where P=‹(λv. LOCAL_VAR v TY)› and U=‹λ_. {Some (discrete None)}›]
∃v ‹() ⦂ MAKE _ (Var v ○)›
try'' ❴
apply_rule BLK[of ‹φarg.dest 𝗏0›, unfolded atomize_eq, OF Premise_D[where mode=default], simplified]
op_free_var ‹φarg.dest 𝗏0›
❵ ❴
op_free_var ‹φarg.dest 𝗏0›
throw ‹v›
❵
❵ .
syntax "_var_scope_" :: ‹idts ⇒ do_bind› ("𝗏𝖺𝗋𝗂𝖺𝖻𝗅𝖾 _" [14] 13)
optional_translations (do_notation)
"_do_cons (_var_scope_ v) P " <= "CONST op_var_scope T TY (λv. P)"
"_do_cons (_var_scope_ v) P" <= "_do_cons (_var_scope_ v) (_do_block P)"
"_do_cons (_var_scope_ (v1 v2)) P" <= "_do_cons (_var_scope_ v1) (_do_cons (_var_scope_ v2) P)"
ML ‹Synchronized.change Phi_Syntax.semantic_oprs (
Symtab.update (\<^const_name>‹op_var_scope›, 0)
#> Symtab.update (\<^const_name>‹op_set_var›, 0)
#> Symtab.update (\<^const_name>‹op_get_var›, 0)
)›
subsection ‹Rules of Variable Operations›
subsubsection ‹Get›
proc [φreason 1200]:
input ‹X›
requires Find: ‹X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ 𝗏𝖺𝗋[vari] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Y 𝗐𝗂𝗍𝗁 Any›
and ‹Semantic_Type T TY›
and [φreason 10000]: ‹parse_eleidx_input_least1 TY input_index sem_idx idx reject›
and [φreason 10000]: ‹φAggregate_Getter idx T U f›
and [φreason 10000]: ‹report_unprocessed_element_index reject ℰℐℋ𝒪𝒪𝒦_none›
output ‹𝗏𝖺𝗅 f x <val-of> vari <path> input_index ⦂ U 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 x ⦂ 𝗏𝖺𝗋[vari] T❟ Y›
@tag synthesis
unfolding REMAINS_def
❴
Find
apply_rule op_get_var[where input_index=input_index and sem_idx=sem_idx and idx=idx and reject=reject]
❵ .
proc [φreason 1210]:
input ‹X›
requires Find: ‹X 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ 𝗏𝖺𝗋[vari] T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 Y 𝗐𝗂𝗍𝗁 Any›
and ‹Semantic_Type T TY›
output ‹𝗏𝖺𝗅 x <val-of> vari <path> [] ⦂ T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 x ⦂ 𝗏𝖺𝗋[vari] T❟ Y›
@tag synthesis
unfolding REMAINS_def
❴
Find
op_get_var0
❵ .
subsubsection ‹Set›
proc (nodef) [φreason 1200]:
input X
requires G : ‹𝗉𝗋𝗈𝖼 g ⦃ X ⟼ 𝗏𝖺𝗅 y ⦂ U' 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 X1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag synthesis›
and S : ‹X1 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ Var vari T❟ Y 𝗐𝗂𝗍𝗁 Any›
and T1: ‹LOCAL_VAR vari TY_var›
and T2: ‹φSemType_opt (x ⦂ T) TY›
and T3: ‹pred_option (λTY_var. pred_option ((=) TY_var) TY) TY_var›
and T4: ‹parse_eleidx_input_least1_opt TY input_index sem_idx idx reject›
and ‹chk_element_index_all_solved reject›
and T5: ‹φAggregate_Mapper_Opt idx T T' U U' f›
and T6: ‹Semantic_Type U' UY›
and T7: ‹pred_option (λTY. is_valid_index_of sem_idx TY UY) TY_var›
output ‹𝗏𝖺𝗅 (y <set-to> vari <path> input_index) ⦂ U' 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 f (λ_. y) x ⦂ 𝗏𝖺𝗋[vari] T'❟ Y›
throws E
@tag synthesis
unfolding REMAINS_def
❴
G
S → val v
$v apply_rule op_set_var[OF T1 T2 T3 T4 T5 T6 T7 report_unprocessed_element_index_I]
$v
❵ .
proc (nodef) [φreason 1210]:
input X
requires G : ‹𝗉𝗋𝗈𝖼 g ⦃ X ⟼ 𝗏𝖺𝗅 y ⦂ T' 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 X1 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag synthesis›
and S : ‹X1 𝗍𝗋𝖺𝗇𝗌𝖿𝗈𝗋𝗆𝗌 x ⦂ Var vari T❟ Y 𝗐𝗂𝗍𝗁 Any›
and T1: ‹LOCAL_VAR vari TY_var›
and T2: ‹φSemType_opt (x ⦂ T) TY›
and T3: ‹pred_option (λTY_var. pred_option ((=) TY_var) TY) TY_var›
and T6: ‹Semantic_Type T' UY›
and T7: ‹pred_option ((=) UY) TY_var›
output ‹𝗏𝖺𝗅 (y <set-to> vari <path> []) ⦂ T' 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 y ⦂ 𝗏𝖺𝗋[vari] T'❟ Y›
throws E
@tag synthesis
unfolding REMAINS_def
❴
G
S → val v
$v apply_rule op_set_var_0[OF T1 T2 T3 T6 T7]
$v
❵ .
subsection ‹Implementing IDE-CP Generic Variable Access›
ML ‹Generic_Variable_Access.parse_phi_type_of_generic_var :=
Symtab.update (\<^const_name>‹Var›, fn _ $ _ $ (_ $ T) => SOME T)
(!Generic_Variable_Access.parse_phi_type_of_generic_var)›
proc (nodef) "__set_var_rule_":
input ‹X❟ y ⦂ 𝗏𝖺𝗅[raw] U'❟ x ⦂ Var vari T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R›
requires G : ‹𝗉𝗋𝗈𝖼 g ⦃ X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 f (λ_. y) x ⦂ 𝗏𝖺𝗋[vari] T'❟ R ⟼ Z ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E›
and T1: ‹LOCAL_VAR vari TY_var›
and T2: ‹φSemType_opt (x ⦂ T) TY›
and T3: ‹pred_option (λTY_var. pred_option ((=) TY_var) TY) TY_var›
and T4: ‹parse_eleidx_input_least1_opt TY input_index sem_idx idx reject›
and T8: ‹report_unprocessed_element_index reject ℰℐℋ𝒪𝒪𝒦_none›
and T5: ‹φAggregate_Mapper_Opt idx T T' U U' f›
and T6: ‹Semantic_Type U' UY›
and T7: ‹pred_option (λTY. is_valid_index_of sem_idx TY UY) TY_var›
output ‹Z›
throws E
❴
apply_rule op_set_var_φapp[OF T1 T2 T3 T4 T5 T6 T7 T8]
G
❵ .
proc (nodef) "__set_var_rule_0_":
input ‹X❟ y ⦂ 𝗏𝖺𝗅[raw] U'❟ x ⦂ Var vari T 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R›
requires G : ‹𝗉𝗋𝗈𝖼 g ⦃ X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 y ⦂ 𝗏𝖺𝗋[vari] U'❟ R ⟼ Z ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E›
and T1: ‹LOCAL_VAR vari TY_var›
and T2: ‹φSemType_opt (x ⦂ T) TY›
and T3: ‹pred_option (λTY_var. pred_option ((=) TY_var) TY) TY_var›
and T4: ‹Semantic_Type U' UY›
and T5: ‹pred_option ((=) UY) TY_var›
output ‹Z›
throws E
❴
apply_rule op_set_var_0[OF T1 T2 T3 T4 T5]
G
❵ .
lemma "__new_var_rule__":
‹ (⋀vari. LOCAL_VAR vari TY
⟹ 𝗉𝗋𝗈𝖼 g vari ⦃ X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 𝗎𝗇𝗂𝗇𝗂𝗍𝖾𝖽 𝗏𝖺𝗋[vari]❟ R ⟼ λret. () ⦂ Var vari φAny❟ Z ret ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (λe. () ⦂ Var vari φAny❟ E e))
⟹ 𝗉𝗋𝗈𝖼 op_var_scope TYPE('a) TY g ⦃ X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⟼ Z ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E ›
❴ premises G
op_var_scope ‹TY› ❴ premises [φreason for ‹LOCAL_VAR vari _›] G ❵
❵ .
proc (nodef) "__set_new_var_rule_":
input ‹X❟ y ⦂ 𝗏𝖺𝗅[raw] U 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R›
requires G: ‹⋀vari. LOCAL_VAR vari (Some TY)
⟹ 𝗉𝗋𝗈𝖼 g vari ⦃ X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 y ⦂ 𝗏𝖺𝗋[vari] U❟ R ⟼ λret. () ⦂ Var vari φAny❟ Z ret ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (λe. () ⦂ Var vari φAny❟ E e)›
and ‹Semantic_Type U TY›
output ‹Z›
throws E
❴
op_var_scope ‹Some TY› ❴
premises [φreason for ‹LOCAL_VAR vari _›]
op_set_var_0
G
❵
❵ .
proc (nodef) "__set_new_var_noty_rule_":
input ‹X❟ y ⦂ 𝗏𝖺𝗅[raw] U 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R›
requires G: ‹⋀vari. LOCAL_VAR vari None
⟹ 𝗉𝗋𝗈𝖼 g vari ⦃ X 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 y ⦂ 𝗏𝖺𝗋[vari] U❟ R ⟼ λret. () ⦂ Var vari φAny❟ Z ret ⦄
𝗍𝗁𝗋𝗈𝗐𝗌 (λe. () ⦂ Var vari φAny❟ E e)›
and ‹Semantic_Type U TY›
output ‹Z›
throws E
❴
op_var_scope None ❴
premises [φreason for ‹LOCAL_VAR vari _›]
op_set_var_0
G
❵
❵ .
ML_file "library/variable.ML"
setup ‹Context.theory_map (Generic_Variable_Access.Process_of_Argument.put NONE)›
end