author  wenzelm 
Tue, 06 Jun 2006 20:47:12 +0200  
changeset 19800  5f764272183e 
parent 19783  82f365a14960 
child 20596  3950e65f48f8 
permissions  rwrr 
15803  1 
(* Title: Pure/Pure.thy 
2 
ID: $Id$ 

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

3 
*) 
15803  4 

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

5 
header {* The Pure theory *} 
15803  6 

7 
theory Pure 

8 
imports ProtoPure 

9 
begin 

19800  10 

19048  11 
setup  {* Common setup of internal components *} 
15803  12 

18710  13 

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

14 
subsection {* Metalevel connectives in assumptions *} 
15803  15 

16 
lemma meta_mp: 

18019  17 
assumes "PROP P ==> PROP Q" and "PROP P" 
15803  18 
shows "PROP Q" 
18019  19 
by (rule `PROP P ==> PROP Q` [OF `PROP P`]) 
15803  20 

21 
lemma meta_spec: 

18019  22 
assumes "!!x. PROP P(x)" 
15803  23 
shows "PROP P(x)" 
18019  24 
by (rule `!!x. PROP P(x)`) 
15803  25 

26 
lemmas meta_allE = meta_spec [elim_format] 

27 

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

28 

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

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

30 

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

31 
locale (open) meta_conjunction_syntax = 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

32 
fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2) 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

33 

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

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

35 
[("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))] 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

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

37 

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

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

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

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

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

42 
assume conj: "!!x. PROP A(x) && PROP B(x)" 
19121  43 
show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))" 
44 
proof  

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

45 
fix x 
19121  46 
from conj show "PROP A(x)" by (rule conjunctionD1) 
47 
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

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

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

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

51 
fix x 
19121  52 
show "PROP A(x) && PROP B(x)" 
53 
proof  

54 
show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format]) 

55 
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

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

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

58 

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

60 
includes meta_conjunction_syntax 
19121  61 
shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)" 
18836  62 
proof 
18466
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

63 
assume conj: "PROP A ==> PROP B && PROP C" 
19121  64 
show "(PROP A ==> PROP B) && (PROP A ==> PROP C)" 
65 
proof  

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

66 
assume "PROP A" 
19121  67 
from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1) 
68 
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

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

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

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

72 
assume "PROP A" 
19121  73 
show "PROP B && PROP C" 
74 
proof  

75 
from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1]) 

76 
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

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

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

79 

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

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

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

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

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

84 
assume r: "PROP A && PROP B ==> PROP C" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

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

86 
show "PROP C" by (rule r)  
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

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

88 
assume r: "PROP A ==> PROP B ==> PROP C" 
389a6f9c31f4
added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents:
18019
diff
changeset

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

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

91 
proof (rule r) 
19121  92 
from conj show "PROP A" by (rule conjunctionD1) 
93 
from conj show "PROP B" by (rule conjunctionD2) 

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

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

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

96 

15803  97 
end 