definition Valid :: "('w::world) form ==> bool" where"Valid A ≡∀w. A w"
definition const :: "'a ==> ('w::world, 'a) expr" where unl_con: "const c w ≡ c"
definition lift :: "['a ==> 'b, ('w::world, 'a) expr] ==> ('w,'b) expr" where unl_lift: "lift f x w ≡ f (x w)"
definition lift2 :: "['a ==> 'b ==> 'c, ('w::world,'a) expr, ('w,'b) expr] ==> ('w,'c) expr" where unl_lift2: "lift2 f x y w ≡ f (x w) (y w)"
definition lift3 :: "['a ==> 'b ==> 'c ==> 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] ==> ('w,'d) expr" where unl_lift3: "lift3 f x y z w ≡ f (x w) (y w) (z w)"
(* "Rigid" quantification (logic level) *) definition RAll :: "('a ==> ('w::world) form) ==> 'w form" (binder‹Rall › 10) where unl_Rall: "(Rall x. A x) w ≡∀x. A x w" definition REx :: "('a ==> ('w::world) form) ==> 'w form" (binder‹Rex › 10) where unl_Rex: "(Rex x. A x) w ≡∃x. A x w" definition REx1 :: "('a ==> ('w::world) form) ==> 'w form" (binder‹Rex! › 10) where unl_Rex1: "(Rex! x. A x) w ≡∃!x. A x w"
"_liftEqu" == "_lift2 (=)" "_liftNeq u v" == "_liftNot (_liftEqu u v)" "_liftNot" == "_lift (CONST Not)" "_liftAnd" == "_lift2 (∧)" "_liftOr" == "_lift2 (∨)" "_liftImp" == "_lift2 (⟶)" "_liftIf" == "_lift3 (CONST If)" "_liftPlus" == "_lift2 (+)" "_liftMinus" == "_lift2 (-)" "_liftTimes" == "_lift2 ((*))" "_liftDiv" == "_lift2 (div)" "_liftMod" == "_lift2 (mod)" "_liftLess" == "_lift2 (<)" "_liftLeq" == "_lift2 (≤)" "_liftMem" == "_lift2 (∈)" "_liftNotMem x xs" == "_liftNot (_liftMem x xs)" "_liftFinset (_liftargs x xs)" == "_lift2 (CONST insert) x (_liftFinset xs)" "_liftFinset x" == "_lift2 (CONST insert) x (_const {})" "_liftPair x (_liftargs y z)" == "_liftPair x (_liftPair y z)" "_liftPair" == "_lift2 (CONST Pair)" "_liftCons" == "CONST lift2 (CONST Cons)" "_liftApp" == "CONST lift2 (@)" "_liftList (_liftargs x xs)" == "_liftCons x (_liftList xs)" "_liftList x" == "_liftCons x (_const [])"
"w ⊨¬A" <= "_liftNot A w" "w ⊨ A ∧ B" <= "_liftAnd A B w" "w ⊨ A ∨ B" <= "_liftOr A B w" "w ⊨ A ⟶ B" <= "_liftImp A B w" "w ⊨ u = v" <= "_liftEqu u v w" "w ⊨∀x. A" <= "_RAll x A w" "w ⊨∃x. A" <= "_REx x A w" "w ⊨∃!x. A" <= "_REx1 x A w"
subsection‹Lemmas and tactics for "intensional" logics.›
(* Turn \<turnstile> F = G into meta-level rewrite rule F == G *) fun int_rewrite ctxt th =
zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection}))
(* flattening turns "\<longrightarrow>" into "\<Longrightarrow>" and eliminates conjunctions in the antecedent. For example, P & Q ⟶ (R | S ⟶ T) becomes [ P; Q; R | S ]==> T Flattening can be useful with "intensional" lemmas (after unlifting). Naive resolution with mp and conjI may run away because of higher-order unification, therefore the code is a little awkward. *) fun flatten t = let (* analogous to RS, but using matching instead of resolution *) fun matchres tha i thb = case Seq.chop 2 (Thm.biresolution NONE true [(false,tha)] i thb) of
([th],_) => th
| ([],_) => raise THM("matchres: no match", i, [tha,thb])
| _ => raise THM("matchres: multiple unifiers", i, [tha,thb])
(* match tha with some premise of thb *) fun matchsome tha thb = letfun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
| hmatch n = matchres tha n thb handle THM _ => hmatch (n-1) in hmatch (Thm.nprems_of thb) end
fun hflatten t = caseThm.concl_of t of
Const _ $ (Const (🍋‹HOL.implies›, _) $ _ $ _) => hflatten (t RS mp)
| _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t in
hflatten t end
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
