author  haftmann 
Fri, 25 Jul 2008 12:03:32 +0200  
changeset 27681  8cedebf55539 
parent 26958  ed3a58a9eae1 
child 28699  32b6a8f12c1c 
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 

26435  5 
section {* Further content for the Pure theory *} 
20627  6 

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

7 
subsection {* Metalevel connectives in assumptions *} 
15803  8 

9 
lemma meta_mp: 

18019  10 
assumes "PROP P ==> PROP Q" and "PROP P" 
15803  11 
shows "PROP Q" 
18019  12 
by (rule `PROP P ==> PROP Q` [OF `PROP P`]) 
15803  13 

23432  14 
lemmas meta_impE = meta_mp [elim_format] 
15 

15803  16 
lemma meta_spec: 
26958  17 
assumes "!!x. PROP P x" 
18 
shows "PROP P x" 

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

15803  20 

21 
lemmas meta_allE = meta_spec [elim_format] 

22 

26570  23 
lemma swap_params: 
26958  24 
"(!!x y. PROP P x y) == (!!y x. PROP P x y)" .. 
26570  25 

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

26 

21625  27 
subsection {* Embedded terms *} 
28 

27681  29 
locale meta_term_syntax = 
21625  30 
fixes meta_term :: "'a => prop" ("TERM _") 
31 

32 
lemmas [intro?] = termI 

33 

34 

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

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

36 

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

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

39 

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

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

41 
includes meta_conjunction_syntax 
26958  42 
shows "(!!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

43 
proof 
26958  44 
assume conj: "!!x. PROP A x && PROP B x" 
45 
show "(!!x. PROP A x) && (!!x. PROP B x)" 

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

47 
fix x 
26958  48 
from conj show "PROP A x" by (rule conjunctionD1) 
49 
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

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

51 
next 
26958  52 
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

53 
fix x 
26958  54 
show "PROP A x && PROP B x" 
19121  55 
proof  
26958  56 
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) 
57 
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

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

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

60 

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

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

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

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

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

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

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

73 
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

74 
assume "PROP A" 
19121  75 
show "PROP B && PROP C" 
76 
proof  

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

78 
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

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

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

81 

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

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

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

84 
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

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

86 
assume r: "PROP A && PROP B ==> PROP C" 
22933  87 
assume ab: "PROP A" "PROP B" 
88 
show "PROP C" 

89 
proof (rule r) 

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

91 
qed 

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

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

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

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

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

96 
proof (rule r) 
19121  97 
from conj show "PROP A" by (rule conjunctionD1) 
98 
from conj show "PROP B" by (rule conjunctionD2) 

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

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

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

101 