Theory PhiSem_Common_Int
theory PhiSem_Common_Int
imports PhiSem_Generic_Boolean "HOL-Library.Signed_Division"
begin
section ‹Common Integer Base›
subsection ‹Logic Syntax and Isabelle Syntax Hijack›
setup ‹
let val remove_synt = Sign.notation false Syntax.mode_default [
(Const (\<^const_abbrev>‹inter›, dummyT), Infixl (Input.string "Int", 70, Position.no_range)),
(Const (\<^const_abbrev>‹union›, dummyT), Infixl (Input.string "Un", 65, Position.no_range)),
(Const (\<^const_name>‹Nats›, dummyT), Mixfix (Input.string "ℕ", [], 1000, Position.no_range)),
(Const (\<^const_name>‹Ints›, dummyT), Mixfix (Input.string "ℤ", [], 1000, Position.no_range)),
(Const (\<^const_name>‹Rats›, dummyT), Mixfix (Input.string "ℚ", [], 1000, Position.no_range)),
(Const ("Real_Vector_Spaces.Reals", dummyT), Mixfix (Input.string "ℝ", [], 1000, Position.no_range))
]
in fn thy => thy
|> remove_synt
|> Context.theory_map (Phi_Hacks.Thy_At_Begin.add' (66, thy) (K remove_synt))
end›
abbreviation LshR (infixl "LSHR" 70) where ‹x LSHR y ≡ x div 2 ^ Big y›
abbreviation LshL (infixl "LSHL" 70) where ‹x LSHL y ≡ x * 2 ^ Big y›
subsection ‹Semantic Base›
debt_axiomatization φSem_int_to_logic_int :: ‹VAL ⇒ int option›
and φSem_int_to_logic_nat :: ‹VAL ⇒ nat option›
subsubsection ‹Reasoner Base for getting the logical int from a semantic int spec›
definition get_logical_int_from_semantic_int :: ‹VAL BI ⇒ int ⇒ bool›
where ‹get_logical_int_from_semantic_int S i = (∀v. v ⊨ S ⟶ Some i = φSem_int_to_logic_int v)›
definition get_logical_nat_from_semantic_int :: ‹VAL BI ⇒ nat ⇒ bool›
where ‹get_logical_nat_from_semantic_int S i = (∀v. v ⊨ S ⟶ Some i = φSem_int_to_logic_nat v)›
declare [[φreason_default_pattern
‹get_logical_nat_from_semantic_int ?S _› ⇒ ‹get_logical_nat_from_semantic_int ?S _› (100)
and ‹get_logical_int_from_semantic_int ?S _› ⇒ ‹get_logical_int_from_semantic_int ?S _› (100)
]]
φreasoner_group logical_spec_of_semantics = (1000, [1000,1000])
for (‹get_logical_int_from_semantic_int S i›, ‹get_logical_nat_from_semantic_int S i›)
‹returning logical images of semantic representations.›
definition 𝗋nat_to_suc_nat :: ‹nat ⇒ nat ⇒ bool›
where [simp, φsafe_simp]: ‹𝗋nat_to_suc_nat n sn ⟷ n = sn›
definition 𝗋int_to_suc_nat :: ‹int ⇒ nat ⇒ bool›
where [simp, φsafe_simp]: ‹𝗋int_to_suc_nat z n ⟷ z = of_nat n›
φreasoner_ML 𝗋nat_to_suc_nat 1000 (‹𝗋nat_to_suc_nat _ _› | ‹𝗋int_to_suc_nat _ _›) =
‹fn (_, (ctxt,sequent0)) => let
exception Not_A_Number
fun dest_number (Const ("Groups.zero_class.zero", _)) = 0
| dest_number (Const ("Groups.one_class.one", _)) = 1
| dest_number (Const (\<^const_name>‹Suc›, _) $ X) = 1 + dest_number X
| dest_number (Const ("Num.numeral_class.numeral", _) $ t) = HOLogic.dest_numeral t
| dest_number (Const ("Groups.uminus_class.uminus", _) $ t) = ~ (dest_number t)
| dest_number t = raise Not_A_Number;
val sequent = Conv.gconv_rule (Phi_Conv.hhf_concl_conv (fn ctxt =>
Conv.arg_conv (Conv.arg1_conv (Simplifier.rewrite ctxt))) ctxt) 1 sequent0
in case Thm.major_prem_of sequent
of (_ $ (Const(N, _) $ Z $ Var v))
=> Seq.make (fn () =>
let val z = dest_number Z
in if z < 0 then NONE
else let
val v' = funpow z (fn x => \<^const>‹Suc› $ x) \<^term>‹0::nat›
in case Seq.pull (
Thm.instantiate (TVars.empty, Vars.make [(v, Thm.cterm_of ctxt v')]) sequent
|> SOLVED' (Simplifier.simp_tac (Phi_Safe_Simps.equip ctxt)) 1
|> Seq.map (pair ctxt)
) of NONE => (
warning (Pretty.string_of (Pretty.block [
Syntax.pretty_term ctxt Z,
Pretty.str " is not a literal number"
]));
NONE)
| some => some
end
end
handle Not_A_Number => NONE
)
| _ => Seq.empty
end
›
subsection ‹Conventions›
φreasoner_group ToA_num_conv = (800, [800, 830]) in ToA_bk
‹Conversion between abstractions of numbers›
and ToA_num_conv_cut = (1000, [1000, 1030]) in ToA_cut
‹Conversion between abstractions of numbers›
subsection ‹Operator Overloading›
φoverloads nat and int
φoverloads floor and ceiling
declare [[
overloaded_operator_in_synthesis ‹(+)›,
overloaded_operator_in_synthesis ‹(-)›,
overloaded_operator_in_synthesis ‹uminus›,
overloaded_operator_in_synthesis ‹(*)›,
overloaded_operator_in_synthesis ‹(div)›,
overloaded_operator_in_synthesis ‹(mod)›,
overloaded_operator_in_synthesis ‹(sdiv)›,
overloaded_operator_in_synthesis ‹(/)›,
overloaded_operator_in_synthesis ‹λv. x1 ⦂ T1 v› ‹λv. x2 ⦂ T2 v› ⇒ ‹λv. x1 < x2 ⦂ 𝗏𝖺𝗅[v] 𝔹›,
overloaded_operator_in_synthesis ‹λv. x1 ⦂ T1 v› ‹λv. x2 ⦂ T2 v› ⇒ ‹λv. x1 ≤ x2 ⦂ 𝗏𝖺𝗅[v] 𝔹›,
overloaded_operator_in_synthesis ‹drop_bit›,
overloaded_operator_in_synthesis ‹push_bit›
]]
declare_φlang_operator
infixl 65 +
infixl 65 -
prefix 80 ~
infixl 70 *
infixl 70 /
infixl 70 %
infix 50 <
infix 50 ≤
infix 50 >
infix 50 ≥
infixl 40 "<<"
infixl 40 ">>"
φreasoner_group φsynthesis_literal_number = (%φsynthesis_literal, [%φsynthesis_literal, %φsynthesis_literal+10])
in φsynthesis_literal
‹literal number›
and φsynthesis_transformation = (300, [300, 330]) in φsynthesis < φsynthesis_literal
‹transformation between abstractions, no opcode emits›
and synthesis_arith = (100, [100,120]) in φsynthesis and < φsynthesis_transformation
‹arithmetic operations›
and synthesis_arith_cut = (1000, [1000,1020]) in φsynthesis_cut
‹cutting arithmetic operations›
lemmas [φreason %φsynthesis_literal_number] = "_synthesis_literal_"[where const=‹0›]
lemmas [φreason %φsynthesis_literal_number] = "_synthesis_literal_"[where const=‹1›]
lemmas [φreason %φsynthesis_literal_number] = "_synthesis_literal_"[where const=‹numeral x› for x]
lemmas [φreason %φsynthesis_literal_number] = "_synthesis_literal_"[where const=‹- numeral x› for x]
lemma [φreason %φsynthesis_normalize]:
‹ 𝗉𝗋𝗈𝖼 H ⦃ R1 ⟼ λret. 1 ⦂ T ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 H ⦃ R1 ⟼ λret. Suc 0 ⦂ T ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R2 ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag synthesis›
unfolding One_nat_def .
lemma [φreason %φsynthesis_weak_normalize]:
‹ 𝗉𝗋𝗈𝖼 f ⦃ X ⟼ λret. push_bit n x ⦂ Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 f ⦃ X ⟼ λret. x * 2 ^ n ⦂ Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag synthesis›
for x :: nat
unfolding push_bit_nat_def .
lemma [φreason %φsynthesis_weak_normalize]:
‹ 𝗉𝗋𝗈𝖼 f ⦃ X ⟼ λret. push_bit n x ⦂ Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag synthesis
⟹ 𝗉𝗋𝗈𝖼 f ⦃ X ⟼ λret. x * 2 ^ n ⦂ Y ret 𝗋𝖾𝗆𝖺𝗂𝗇𝗌 R ⦄ 𝗍𝗁𝗋𝗈𝗐𝗌 E @tag synthesis›
for x :: int
unfolding push_bit_int_def .
φtypeclass φOrder (T)
fixes leq[φoverload ≤]: ‹𝗉𝗋𝗈𝖼 leq(v⇩a,v⇩b) ⦃ x ⦂ 𝗏𝖺𝗅[v⇩a] T❟ y ⦂ 𝗏𝖺𝗅[v⇩b] T ⟼ x ≤ y ⦂ 𝗏𝖺𝗅 𝔹 ⦄ ›
thm φOrder_def
thm φOrder.leq
end