author  paulson 
Mon, 18 Oct 1999 15:20:21 +0200  
changeset 7879  4547f0bd9454 
parent 5704  1ddf7e1e8b19 
child 9039  20ff649a0fd1 
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 

5704  32 
val surj_pair = Drule.unvarify (standard raw_surj_pair); 
5680
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 
val P = Free (variant used "P", pT > propT); 
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

38 

5704  39 
(*"!!a b. PROP (a, b)"*) 
40 
val all_a_b = all "a" aT (all "b" bT (P $ (con $ Bound 1 $ Bound 0))); 

41 
(*"!!x. PROP P x"*) 

42 
val all_x = all "x" pT (P $ Bound 0); 

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

43 

5704  44 
(*lemma "P p == P (fst p, snd p)"*) 
45 
val lem1 = Thm.combination (Thm.reflexive (ct P)) surj_pair; 

46 

7879  47 
(*lemma "(!!a b. PROP P (a,b)) ==> PROP P p"*) 
5704  48 
val lem2 = prove_goalw_cterm [lem1] (ct (all_a_b ==> P $ p)) 
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

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

50 

7879  51 
(*lemma "(!!a b. PROP P (a,b)) ==> !!x. PROP P x"*) 
5704  52 
val lem3 = prove_goalw_cterm [] (ct (all_a_b ==> all_x)) 
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

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

54 

7879  55 
(*lemma "(!!x. PROP P x) ==> !!a b. PROP P (a,b)"*) 
5704  56 
val lem4 = prove_goalw_cterm [] (ct (all_x ==> all_a_b)) 
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset

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

58 
in standard (Thm.equal_intr lem4 lem3) end; 
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 

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

61 
end; 