22 |
22 |
23 lemma swap_params: |
23 lemma swap_params: |
24 "(!!x y. PROP P x y) == (!!y x. PROP P x y)" .. |
24 "(!!x y. PROP P x y) == (!!y x. PROP P x y)" .. |
25 |
25 |
26 |
26 |
27 subsection {* Embedded terms *} |
|
28 |
|
29 locale meta_term_syntax = |
|
30 fixes meta_term :: "'a => prop" ("TERM _") |
|
31 |
|
32 lemmas [intro?] = termI |
|
33 |
|
34 |
|
35 subsection {* Meta-level conjunction *} |
27 subsection {* Meta-level conjunction *} |
36 |
28 |
37 locale meta_conjunction_syntax = |
|
38 fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) |
|
39 |
|
40 lemma all_conjunction: |
29 lemma all_conjunction: |
41 fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) |
30 "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))" |
42 shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))" |
|
43 proof |
31 proof |
44 assume conj: "!!x. PROP A x && PROP B x" |
32 assume conj: "!!x. PROP A x &&& PROP B x" |
45 show "(!!x. PROP A x) && (!!x. PROP B x)" |
33 show "(!!x. PROP A x) &&& (!!x. PROP B x)" |
46 proof - |
34 proof - |
47 fix x |
35 fix x |
48 from conj show "PROP A x" by (rule conjunctionD1) |
36 from conj show "PROP A x" by (rule conjunctionD1) |
49 from conj show "PROP B x" by (rule conjunctionD2) |
37 from conj show "PROP B x" by (rule conjunctionD2) |
50 qed |
38 qed |
51 next |
39 next |
52 assume conj: "(!!x. PROP A x) && (!!x. PROP B x)" |
40 assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)" |
53 fix x |
41 fix x |
54 show "PROP A x && PROP B x" |
42 show "PROP A x &&& PROP B x" |
55 proof - |
43 proof - |
56 show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) |
44 show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) |
57 show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format]) |
45 show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format]) |
58 qed |
46 qed |
59 qed |
47 qed |
60 |
48 |
61 lemma imp_conjunction: |
49 lemma imp_conjunction: |
62 fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) |
50 "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
63 shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)" |
|
64 proof |
51 proof |
65 assume conj: "PROP A ==> PROP B && PROP C" |
52 assume conj: "PROP A ==> PROP B &&& PROP C" |
66 show "(PROP A ==> PROP B) && (PROP A ==> PROP C)" |
53 show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
67 proof - |
54 proof - |
68 assume "PROP A" |
55 assume "PROP A" |
69 from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1) |
56 from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1) |
70 from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2) |
57 from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2) |
71 qed |
58 qed |
72 next |
59 next |
73 assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)" |
60 assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" |
74 assume "PROP A" |
61 assume "PROP A" |
75 show "PROP B && PROP C" |
62 show "PROP B &&& PROP C" |
76 proof - |
63 proof - |
77 from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1]) |
64 from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1]) |
78 from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2]) |
65 from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2]) |
79 qed |
66 qed |
80 qed |
67 qed |
81 |
68 |
82 lemma conjunction_imp: |
69 lemma conjunction_imp: |
83 fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) |
70 "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)" |
84 shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)" |
|
85 proof |
71 proof |
86 assume r: "PROP A && PROP B ==> PROP C" |
72 assume r: "PROP A &&& PROP B ==> PROP C" |
87 assume ab: "PROP A" "PROP B" |
73 assume ab: "PROP A" "PROP B" |
88 show "PROP C" |
74 show "PROP C" |
89 proof (rule r) |
75 proof (rule r) |
90 from ab show "PROP A && PROP B" . |
76 from ab show "PROP A &&& PROP B" . |
91 qed |
77 qed |
92 next |
78 next |
93 assume r: "PROP A ==> PROP B ==> PROP C" |
79 assume r: "PROP A ==> PROP B ==> PROP C" |
94 assume conj: "PROP A && PROP B" |
80 assume conj: "PROP A &&& PROP B" |
95 show "PROP C" |
81 show "PROP C" |
96 proof (rule r) |
82 proof (rule r) |
97 from conj show "PROP A" by (rule conjunctionD1) |
83 from conj show "PROP A" by (rule conjunctionD1) |
98 from conj show "PROP B" by (rule conjunctionD2) |
84 from conj show "PROP B" by (rule conjunctionD2) |
99 qed |
85 qed |