author  nipkow 
Wed, 20 Jun 2007 08:09:56 +0200  
changeset 23432  cec811764a38 
parent 22933  338c7890c96f 
child 23824  8ad7131dbfcf 
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 
parse_translation {* 

21627
b822c7e61701
meta_term_syntax: proper operation on untyped preterms;
wenzelm
parents:
21625
diff
changeset

37 
[("\<^fixed>meta_term", fn [t] => Const ("ProtoPure.term", dummyT > propT) $ t)] 
21625  38 
*} 
39 

40 
lemmas [intro?] = termI 

41 

42 

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

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

44 

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

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

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

47 

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

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

49 
[("\<^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

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

51 

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

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

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

54 
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

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

56 
assume conj: "!!x. PROP A(x) && PROP B(x)" 
19121  57 
show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))" 
58 
proof  

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

59 
fix x 
19121  60 
from conj show "PROP A(x)" by (rule conjunctionD1) 
61 
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

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

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

64 
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

65 
fix x 
19121  66 
show "PROP A(x) && PROP B(x)" 
67 
proof  

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

69 
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

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

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

72 

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

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

77 
assume conj: "PROP A ==> PROP B && PROP C" 
19121  78 
show "(PROP A ==> PROP B) && (PROP A ==> PROP C)" 
79 
proof  

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

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

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

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

85 
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

86 
assume "PROP A" 
19121  87 
show "PROP B && PROP C" 
88 
proof  

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

90 
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

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

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

93 

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

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

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

96 
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

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

98 
assume r: "PROP A && PROP B ==> PROP C" 
22933  99 
assume ab: "PROP A" "PROP B" 
100 
show "PROP C" 

101 
proof (rule r) 

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

103 
qed 

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

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

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

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

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

108 
proof (rule r) 
19121  109 
from conj show "PROP A" by (rule conjunctionD1) 
110 
from conj show "PROP B" by (rule conjunctionD2) 

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

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

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

113 

15803  114 
end 