author  wenzelm 
Wed, 21 Jan 2009 23:21:44 +0100  
changeset 29606  fedb8be05f24 
parent 28856  5e009a80fe6d 
child 48638  22d65e375c01 
permissions  rwrr 
15803  1 

26435  2 
section {* Further content for the Pure theory *} 
20627  3 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

4 
subsection {* Metalevel connectives in assumptions *} 
15803  5 

6 
lemma meta_mp: 

18019  7 
assumes "PROP P ==> PROP Q" and "PROP P" 
15803  8 
shows "PROP Q" 
18019  9 
by (rule `PROP P ==> PROP Q` [OF `PROP P`]) 
15803  10 

23432  11 
lemmas meta_impE = meta_mp [elim_format] 
12 

15803  13 
lemma meta_spec: 
26958  14 
assumes "!!x. PROP P x" 
15 
shows "PROP P x" 

16 
by (rule `!!x. PROP P x`) 

15803  17 

18 
lemmas meta_allE = meta_spec [elim_format] 

19 

26570  20 
lemma swap_params: 
26958  21 
"(!!x y. PROP P x y) == (!!y x. PROP P x y)" .. 
26570  22 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

23 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

24 
subsection {* Metalevel conjunction *} 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

25 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

26 
lemma all_conjunction: 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

27 
"(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

28 
proof 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

29 
assume conj: "!!x. PROP A x &&& PROP B x" 
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

30 
show "(!!x. PROP A x) &&& (!!x. PROP B x)" 
19121  31 
proof  
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

32 
fix x 
26958  33 
from conj show "PROP A x" by (rule conjunctionD1) 
34 
from conj show "PROP B x" by (rule conjunctionD2) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

35 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

36 
next 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

37 
assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

38 
fix x 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

39 
show "PROP A x &&& PROP B x" 
19121  40 
proof  
26958  41 
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) 
42 
show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format]) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

43 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

44 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

45 

19121  46 
lemma imp_conjunction: 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

47 
"(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)" 
18836  48 
proof 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

49 
assume conj: "PROP A ==> PROP B &&& PROP C" 
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

50 
show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" 
19121  51 
proof  
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

52 
assume "PROP A" 
19121  53 
from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1) 
54 
from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

55 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

56 
next 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

57 
assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

58 
assume "PROP A" 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

59 
show "PROP B &&& PROP C" 
19121  60 
proof  
61 
from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1]) 

62 
from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2]) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

63 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

64 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

65 

389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

66 
lemma conjunction_imp: 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

67 
"(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

68 
proof 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

69 
assume r: "PROP A &&& PROP B ==> PROP C" 
22933  70 
assume ab: "PROP A" "PROP B" 
71 
show "PROP C" 

72 
proof (rule r) 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

73 
from ab show "PROP A &&& PROP B" . 
22933  74 
qed 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

75 
next 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

76 
assume r: "PROP A ==> PROP B ==> PROP C" 
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28699
diff
changeset

77 
assume conj: "PROP A &&& PROP B" 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

78 
show "PROP C" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

79 
proof (rule r) 
19121  80 
from conj show "PROP A" by (rule conjunctionD1) 
81 
from conj show "PROP B" by (rule conjunctionD2) 

18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

82 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

83 
qed 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

84 