From 1ae4247014e2342b1455a378601acb7014a01224 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Thu, 5 Oct 2023 14:50:55 +0200 Subject: [PATCH] Minor updates to possible world theory. --- AOT_PossibleWorlds.thy | 184 +++++++++++++++++++++++++++++++++++++---- 1 file changed, 167 insertions(+), 17 deletions(-) diff --git a/AOT_PossibleWorlds.thy b/AOT_PossibleWorlds.thy index b01b747..3b3568b 100644 --- a/AOT_PossibleWorlds.thy +++ b/AOT_PossibleWorlds.thy @@ -7,7 +7,44 @@ begin section\Possible Worlds\ AOT_define Situation :: \\ \ \\ (\Situation'(_')\) - situations: \Situation(x) \\<^sub>d\<^sub>f A!x & \F (x[F] \ Propositional([F]))\ + "situations:1": \Situation(x) \\<^sub>d\<^sub>f A!x & \F (x[F] \ Propositional([F]))\ + +(* TODO: temporary alias to keep the old key used for the definition working *) +lemmas "situations" = "situations:1" + +AOT_theorem "situations:2": \\x Situation(x)\ +proof - + AOT_have \\x (A!x & \F (x[F] \ F = [\y [R]ab]))\ + using "A-objects" "vdash-properties:1[2]" by auto + then AOT_obtain c where c_prop: \A!c & \F (c[F] \ F = [\y [R]ab])\ + using "\E" by meson + AOT_have \Situation(c)\ + proof(safe intro!: "\\<^sub>d\<^sub>fI"[OF "situations:1"] "&I" GEN "\I") + AOT_show \A!c\ + using c_prop "&E" by blast + next + fix F + AOT_assume \c[F]\ + AOT_hence F_eq: \F = [\y [R]ab]\ + using "con-dis-i-e:2:b" "intro-elim:3:a" "rule-ui:3" c_prop by blast + AOT_find_theorems \Propositional([\])\ + AOT_show \Propositional([F])\ + proof(rule "prop-prop1"[THEN "\\<^sub>d\<^sub>fI"]) + AOT_show "\p F = [\y p]" + using F_eq "\I"(1) + using "log-prop-prop:2" by fastforce + qed + qed + AOT_thus \\x Situation(x)\ + using "\I" by blast +qed + +AOT_theorem "situations:3": \Situation(\) \ \\\ +proof (rule "\I") + AOT_assume \Situation(\)\ + AOT_hence \A!\\ by (metis "\\<^sub>d\<^sub>fE" "&E"(1) "situations:1") + AOT_thus \\\\ by (metis "russell-axiom[exe,1].\_denotes_asm") +qed AOT_theorem "T-sit": \TruthValue(x) \ Situation(x)\ proof(rule "\I") @@ -18,7 +55,7 @@ proof(rule "\I") AOT_hence \: \A!x & \F (x[F] \ \q((q \ p) & F = [\y q]))\ using "tv-p"[THEN "\\<^sub>d\<^sub>fE"] by blast AOT_show \Situation(x)\ - proof(rule situations[THEN "\\<^sub>d\<^sub>fI"]; safe intro!: "&I" GEN "\I" \[THEN "&E"(1)]) + proof(rule "situations:1"[THEN "\\<^sub>d\<^sub>fI"]; safe intro!: "&I" GEN "\I" \[THEN "&E"(1)]) fix F AOT_assume \x[F]\ AOT_hence \\q((q \ p) & F = [\y q])\ @@ -34,7 +71,7 @@ AOT_theorem "possit-sit:1": \Situation(x) \ \Situation(x)\I"; rule "\I") AOT_assume \Situation(x)\ AOT_hence 0: \A!x & \F (x[F] \ Propositional([F]))\ - using situations[THEN "\\<^sub>d\<^sub>fE"] by blast + using "situations:1"[THEN "\\<^sub>d\<^sub>fE"] by blast AOT_have 1: \\(A!x & \F (x[F] \ Propositional([F])))\ proof(rule "KBasic:3"[THEN "\E"(2)]; rule "&I") AOT_show \\A!x\ using 0[THEN "&E"(1)] by (metis "oa-facts:2"[THEN "\E"]) @@ -47,7 +84,7 @@ proof(rule "\I"; rule "\I") qed AOT_show \\Situation(x)\ by (AOT_subst \Situation(x)\ \A!x & \F (x[F] \ Propositional([F]))\) - (auto simp: 1 "\Df" situations) + (auto simp: 1 "\Df" "situations:1") next AOT_show \Situation(x)\ if \\Situation(x)\ using "qml:2"[axiom_inst, THEN "\E", OF that]. @@ -64,7 +101,7 @@ AOT_theorem "possit-sit:4": \\<^bold>\Situation(x) \ Situation(x by (meson "Act-Basic:5" "Act-Sub:2" "RA[2]" "\E"(1) "\E"(6) "possit-sit:2") AOT_theorem "possit-sit:5": \Situation(\p)\ -proof (safe intro!: situations[THEN "\\<^sub>d\<^sub>fI"] "&I" GEN "\I" "prop-prop1"[THEN "\\<^sub>d\<^sub>fI"]) +proof (safe intro!: "situations:1"[THEN "\\<^sub>d\<^sub>fI"] "&I" GEN "\I" "prop-prop1"[THEN "\\<^sub>d\<^sub>fI"]) AOT_have \\F \p[F]\ using "tv-id:2"[THEN "prop-enc"[THEN "\\<^sub>d\<^sub>fE"], THEN "&E"(2)] "existential:1" "prop-prop2:2" by blast @@ -128,22 +165,13 @@ AOT_register_rigid_restricted_type Situation: \Situation(\)\ proof AOT_modally_strict { - fix p - AOT_obtain x where \TruthValueOf(x,p)\ - by (metis "instantiation" "p-has-!tv:1") - AOT_hence \\p TruthValueOf(x,p)\ by (rule "\I") - AOT_hence \TruthValue(x)\ by (metis "\\<^sub>d\<^sub>fI" "T-value") - AOT_hence \Situation(x)\ using "T-sit"[THEN "\E"] by blast - AOT_thus \\x Situation(x)\ by (rule "\I") + AOT_show \\x Situation(x)\ + using "situations:2". } next AOT_modally_strict { AOT_show \Situation(\) \ \\\ for \ - proof (rule "\I") - AOT_assume \Situation(\)\ - AOT_hence \A!\\ by (metis "\\<^sub>d\<^sub>fE" "&E"(1) situations) - AOT_thus \\\\ by (metis "russell-axiom[exe,1].\_denotes_asm") - qed + using "situations:3". } next AOT_modally_strict { @@ -364,6 +392,7 @@ next THEN "\E"(2), THEN "\E", OF that(1)]. qed +(* TODO: removed in PLM *) AOT_define Persistent :: \\ \ \\ (\Persistent'(_')\) persistent: \Persistent(p) \\<^sub>d\<^sub>f \s (s \ p \ \s' (s \ s' \ s' \ p))\ @@ -371,6 +400,63 @@ AOT_theorem "pers-prop": \\p Persistent(p)\ by (safe intro!: GEN[where 'a=\] Situation.GEN persistent[THEN "\\<^sub>d\<^sub>fI"] "\I") (simp add: "sit-part-whole"[THEN "\\<^sub>d\<^sub>fE", THEN "&E"(2), THEN "\E"(2), THEN "\E"]) +(* TODO: put this at the correct place *) +AOT_theorem "sit-comp-simp": \\s\p(s \ p \ \{p})\ +proof - + AOT_have \\x (A!x & \F(x[F] \ \p (\{p} & F = [\y p])))\ + using "A-objects" "vdash-properties:1[2]" by force + then AOT_obtain c where c_prop: \A!c & \F(c[F] \ \p (\{p} & F = [\y p]))\ + using "\E" by meson + AOT_have sit_c: \Situation(c)\ + proof(safe intro!: "\\<^sub>d\<^sub>fI"[OF situations] "&I" GEN "\I") + AOT_show \A!c\ + using c_prop "&E" by blast + next + fix F + AOT_assume \c[F]\ + AOT_hence F_eq: \\p (\{p} & F = [\y p])\ + using "con-dis-i-e:2:b" "intro-elim:3:a" "rule-ui:3" c_prop by blast + then AOT_obtain q where q_prop: \\{q} & F = [\y q]\ + using "\E" by meson + AOT_show \Propositional([F])\ + proof(rule "prop-prop1"[THEN "\\<^sub>d\<^sub>fI"]) + AOT_show "\p F = [\y p]" + using q_prop[THEN "&E"(2)] "\I"(1) + by (metis "log-prop-prop:2") + qed + qed + moreover AOT_have \\p(c \ p \ \{p})\ + proof(safe intro!: GEN "\I" "\I") + fix p + AOT_assume \c \ p\ + AOT_hence 1: \c[\y p]\ + using "intro-elim:3:a" "vdash-properties:10" calculation lem1 by blast + AOT_have \\q (\{q} & [\y p] = [\y q])\ + by (safe intro!: c_prop[THEN "&E"(2), THEN "\E"(1)[where \="\[\y p]\"], THEN "\E"(1)] 1 "cqt:2") + then AOT_obtain q where 2: \\{q} & [\y p] = [\y q]\ + using "\E" by meson + AOT_hence \p = q\ + using "con-dis-i-e:2:b" "intro-elim:3:b" "p-identity-thm2:3" by blast + AOT_thus \\{p}\ + using 2 + using "con-dis-i-e:2:a" "rule=E" id_sym by blast + next + fix p + AOT_assume \\{p}\ + moreover AOT_have \[\y p] = [\y p]\ + by (simp add: "prop-prop2:2" "rule=I:1") + ultimately AOT_have \\{p} & [\y p] = [\y p]\ using "&I" by blast + AOT_hence \\q (\{q} & [\y p] = [\y q])\ + using "\I" by fast + AOT_hence \c[\y p]\ + by (safe intro!: c_prop[THEN "&E"(2), THEN "\E"(1)[where \="\[\y p]\"], THEN "\E"(2)] "cqt:2") + AOT_thus \c \ p\ + by (metis "intro-elim:3:b" "vdash-properties:10" sit_c lem1) + qed + ultimately AOT_show \\s\p(s \ p \ \{p})\ + by (meson "con-dis-i-e:1" "existential:2[const_var]") +qed + AOT_define NullSituation :: \\ \ \\ (\NullSituation'(_')\) "df-null-trivial:1": \NullSituation(s) \\<^sub>d\<^sub>f \\p s \ p\ @@ -3190,6 +3276,70 @@ AOT_theorem "rigid-rel-thms:3": \Rigid(F) \ \x\<^sub>1...\< AOT_subst_thm "rigid-rel-thms:2") (simp add: "oth-class-taut:3:a") +AOT_theorem \Possible(s) \ \w(s \ w)\ +proof(safe intro!: "\I" "\I") + AOT_assume \Possible(s)\ + AOT_hence \\Actual(s)\ + using "\\<^sub>d\<^sub>fE" "con-dis-i-e:2:b" pos by blast + AOT_hence \\\p (s \ p \ p)\ + apply (AOT_subst (reverse) \\p (s \ p \ p)\ \Actual(s)\) + using "df-simplify:1" "rule-eq-df:1" Situation.restricted_var_condition actual apply blast + by auto + AOT_hence \\w w \ \p (s \ p \ p)\ + by (safe intro!: "fund:1"[unvarify p, THEN "\E"(1)] "log-prop-prop:2") + then AOT_obtain w where \w \ \p (s \ p \ p)\ + using PossibleWorld.instantiation by meson + AOT_hence 1: \\p w \ (s \ p \ p)\ + using "conj-dist-w:5" + using "intro-elim:3:a" by blast + AOT_have \s \ w\ + proof(safe intro!: "sit-part-whole"[THEN "\\<^sub>d\<^sub>fI"] "&I" "Situation.\" GEN "\I") + AOT_show \Situation(w)\ + using "\\<^sub>d\<^sub>fE" "con-dis-i-e:2:a" "world-pos" pos by blast + next + fix p + AOT_assume \s \ p\ + AOT_hence \\s \ p\ + using "intro-elim:3:a" "lem2:1" by blast + AOT_hence \\w w \ s \ p\ + by (safe intro!: "fund:2"[unvarify p, THEN "\E"(1)] "log-prop-prop:2") + AOT_hence \w \ s \ p\ + using "rule-ui:3" "vdash-properties:10" PossibleWorld.restricted_var_condition by blast + moreover AOT_have \w \ (s \ p \ p)\ + using 1 "\E" by blast + ultimately AOT_show \w \ p\ + using "conj-dist-w:2"[unvarify p, THEN "\E"(1)] "log-prop-prop:2" "\E" by blast + qed + AOT_thus \\w(s \ w)\ + using "PossibleWorld.\I" by blast +next + AOT_assume \\w(s \ w)\ + then AOT_obtain w where \s \ w\ + using "PossibleWorld.\E" by meson + AOT_hence 1: \\p (s \ p \ w \ p)\ + using "sit-part-whole"[THEN "\\<^sub>d\<^sub>fE"] "&E" by blast + AOT_have \\p (w \ (s \ p \ p))\ + proof (safe intro!: GEN "conj-dist-w:2"[unvarify p, THEN "\E"(2)] "log-prop-prop:2" "\I") + fix p + AOT_assume \w \ s \ p\ + AOT_hence \\s \ p\ + by (auto intro!: "fund:1"[unvarify p, THEN "\E"(2)] "log-prop-prop:2" "PossibleWorld.\I") + AOT_hence \s \ p\ + using "intro-elim:3:a" "lem2:2" by blast + AOT_thus \w \ p\ + using 1 "log-prop-prop:2" "rule-ui:1" "vdash-properties:10" by blast + qed + AOT_hence \w \ \p (s \ p \ p)\ + by (metis "\E"(2) "conj-dist-w:5") + AOT_hence \\\p (s \ p \ p)\ + by (safe intro!: "fund:1"[unvarify p, THEN "\E"(2)] "log-prop-prop:2" PossibleWorld.existential) + AOT_hence \\Actual(s)\ + by (AOT_subst_def actual) + (metis "KBasic:16" "&I" "\E" RN "Situation.\") + AOT_thus \Possible(s)\ + by(safe intro!: "pos"[THEN "\\<^sub>d\<^sub>fI"] "&I" "Situation.\") +qed + (*<*) end (*>*)