author  wenzelm 
Tue, 20 Oct 1998 16:18:18 +0200  
changeset 5680  4f526bcd3a68 
child 5704  1ddf7e1e8b19 
permissions  rwrr 
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

1 
(* Title: Provers/split_paired_all.ML 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

4 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

5 
Derived rule for turning metalevel surjective pairing into split rule: 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

6 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

7 
p == (fst p, snd p) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

8 
 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

9 
!!a b. PROP (a, b) == !! x. PROP P x 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

10 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

11 
*) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

12 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

13 
signature SPLIT_PAIRED_ALL = 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

14 
sig 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

15 
val rule: thm > thm 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

16 
end; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

17 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

18 
structure SplitPairedAll: SPLIT_PAIRED_ALL = 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

19 
struct 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

20 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

21 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

22 
fun all x T t = Term.all T $ Abs (x, T, t); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

23 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

24 
infixr ==>; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

25 
val op ==> = Logic.mk_implies; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

26 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

27 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

28 
fun rule raw_surj_pair = 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

29 
let 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

30 
val ct = Thm.cterm_of (Thm.sign_of_thm raw_surj_pair); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

31 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

32 
val surj_pair = Drule.unvarify raw_surj_pair; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

33 
val used = Term.add_term_names (#prop (Thm.rep_thm surj_pair), []); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

34 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

35 
val (p, con $ _ $ _) = Logic.dest_equals (#prop (rep_thm surj_pair)); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

36 
val pT as Type (_, [aT, bT]) = fastype_of p; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

37 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

38 
val P = Free (variant used "P", pT > propT); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

39 
val x_name = variant used "x"; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

40 
val x = Free (x_name, pT); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

41 
val a = variant used "a"; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

42 
val b = variant used "b"; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

43 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

44 
(*"P x == P (fst x, snd x)"*) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

45 
val lem1 = 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

46 
Thm.combination (Thm.reflexive (ct P)) surj_pair 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

47 
> Thm.forall_intr (ct p) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

48 
> Thm.forall_elim (ct x); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

49 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

50 
(*"!!a b. PROP (a, b) ==> PROP P x"*) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

51 
val lem2 = prove_goalw_cterm [lem1] 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

52 
(ct (all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0))) ==> P $ x)) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

53 
(fn prems => [resolve_tac prems 1]); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

54 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

55 
(*"!!a b. PROP (a, b) ==> !! x. PROP P x"*) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

56 
val lem3 = prove_goalw_cterm [] 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

57 
(ct (all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0))) ==> all x_name pT (P $ Bound 0))) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

58 
(fn prems => [rtac lem2 1, resolve_tac prems 1]); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

59 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

60 
(*"!! x. PROP P x ==> !!a b. PROP (a, b)"*) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

61 
val lem4 = prove_goalw_cterm [] 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

62 
(ct (all x_name pT (P $ Bound 0) ==> all a aT (all a bT (P $ (con $ Bound 1 $ Bound 0))))) 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

63 
(fn prems => [resolve_tac prems 1]); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

64 
in standard (Thm.equal_intr lem4 lem3) end; 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

65 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

66 

4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

67 
end; 