author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 23824  8ad7131dbfcf 
child 26426  ddac7ef1e991 
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 

20627  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 

23432  21 
lemmas meta_impE = meta_mp [elim_format] 
22 

15803  23 
lemma meta_spec: 
18019  24 
assumes "!!x. PROP P(x)" 
15803  25 
shows "PROP P(x)" 
18019  26 
by (rule `!!x. PROP P(x)`) 
15803  27 

28 
lemmas meta_allE = meta_spec [elim_format] 

29 

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

30 

21625  31 
subsection {* Embedded terms *} 
32 

33 
locale (open) meta_term_syntax = 

34 
fixes meta_term :: "'a => prop" ("TERM _") 

35 

36 
lemmas [intro?] = termI 

37 

38 

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

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

40 

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

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

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

43 

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

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

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

46 
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

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

48 
assume conj: "!!x. PROP A(x) && PROP B(x)" 
19121  49 
show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))" 
50 
proof  

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

51 
fix x 
19121  52 
from conj show "PROP A(x)" by (rule conjunctionD1) 
53 
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

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

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

56 
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

57 
fix x 
19121  58 
show "PROP A(x) && PROP B(x)" 
59 
proof  

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

61 
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

62 
qed 
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 

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

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

69 
assume conj: "PROP A ==> PROP B && PROP C" 
19121  70 
show "(PROP A ==> PROP B) && (PROP A ==> PROP C)" 
71 
proof  

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

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

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

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

77 
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

78 
assume "PROP A" 
19121  79 
show "PROP B && PROP C" 
80 
proof  

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

82 
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

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

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

85 

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

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

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

88 
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

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

90 
assume r: "PROP A && PROP B ==> PROP C" 
22933  91 
assume ab: "PROP A" "PROP B" 
92 
show "PROP C" 

93 
proof (rule r) 

94 
from ab show "PROP A && PROP B" . 

95 
qed 

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

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

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

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

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

100 
proof (rule r) 
19121  101 
from conj show "PROP A" by (rule conjunctionD1) 
102 
from conj show "PROP B" by (rule conjunctionD2) 

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

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

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

105 

15803  106 
end 