Início / coding / Perguntas / 79551444
Accepted
Squirtle
Asked: 2025-04-03 03:45:38 +0800 CST

Usando continuous_on_diff com subst (Isabelle)

  • 772

POSTAGEM ORIGINAL:

Estou tentando mostrar o seguinte:

have "continuous_on {x. 0 < x} (λx. 12 * x⇧2 - 1)"

E eu gostaria de usar o seguinte lema:

thm continuous_on_diff
----------------------------------------------------------------------------------------------------------
Output:
⟦continuous_on ?s ?f; continuous_on ?s ?g⟧ ⟹ continuous_on ?s (λx. ?f x - ?g x)

Mas talvez essa não seja a forma correta, então tento isso:

 have "continuous_on {x. 0 < x} (λx. (λw . 12 * w⇧2) x  - (λw . 1)x)"
                      apply(subst continuous_on_diff)

Mas isso não funcionou, então deixei ainda mais explícito:

have "continuous_on {x. 0 < x} (λx. (λw . 12 * w⇧2) x  - (λw . 1)x)"
      apply(subst continuous_on_diff[where f = "(λw . 12 * w⇧2)" and g= "(λw . 1)" and s = "{x. 0 < x}"])

Mas mesmo isso não funcionou, entretanto quando verifiquei o teorema:

thm continuous_on_diff[where f = "(λw . 12 * w⇧2)" and g = "(λw . 1)" and s = "{x. 0 < x}"]
-------------------------------------------------------------------------------------------
Output:
⟦continuous_on {x. 0 < x} (λw. 12 * w⇧2); continuous_on {x. 0 < x} (λw. 1)⟧ ⟹ continuous_on {x. 0 < x} (λx. 12 * x⇧2 - 1)

Parece ser exatamente o que eu quero. A única coisa que consigo pensar é que "subst" não é adequado para lidar com argumentos de estilo não equacional, e também não consigo fazer "rule" funcionar.

Qualquer ajuda é muito apreciada!

De forma semelhante, também estou lutando para provar:

"have continuous_on {x. 0 < x} ((*) 6)"

EDIT: Quando tornei as informações de digitação mais explícitas, como em:

have "continuous_on {x :: real. 0 < x} (λx. (λw . 12 * w⇧2) x  - (λw . 1)x)"
                      apply(rule continuous_on_diff[where f = "(λw . 12 * w⇧2)" and g = "(λw . 1)" and s = "{x. 0 < x}"])

Isso tornou isso provável. Mas qual é a diferença?

isabelle

1 respostas

  1. Best Answer

    Não entendo por que você está tentando usar subst. O substmétodo é para substituição; ele só funciona quando você dá a ele uma equação. Você quis dizer usar rule? Isso faria mais sentido.

    Em qualquer caso, a abordagem usual para provar continuidade é apenas fazer algo como apply (auto intro!: continuous_intros). A lista de teoremas continuous_introsé projetada especificamente para fazer com que obrigações óbvias de prova de continuidade simplesmente desapareçam. Claro que só funciona se todas as funções que você tem em seu objetivo tiverem uma regra correspondente em continuous_intros, e você pode obter condições secundárias que surgem. Mas geralmente funciona extremamente bem.

    Existem também conjuntos semelhantes de regras para coisas como analiticidade, holomorficidade e, mais importante, derivadas ( analytic_intros, holomorphic_intros, derivative_eq_intros).

    Observe também que você provavelmente terá que anotar tipos. Se você apenas escrever, continuous_on {x. 0 < x} ((*) 6)então Isabelle derivará um tipo muito genérico para essa função, e você provavelmente não será capaz de provar isso. Coloque uma anotação de tipo ali ( real, complex, o que você pretendeu), por exemplo, em uma das seguintes formas:

    continuous_on {x::real. 0 < x} ((*) 6)
continuous_on {x. 0 < x} ((*) (6::real))
continuous_on {x. 0 < x} ((*) 6 :: real ⇒ real)

    As seguintes obras:

    lemma "continuous_on {x. 0 < x} ((*) 6 :: real ⇒ real)"
  by (auto intro!: continuous_intros)
    • 1

relate perguntas