45 tags: Properties.T, |
45 tags: Properties.T, |
46 maxidx: int, |
46 maxidx: int, |
47 shyps: sort OrdList.T, |
47 shyps: sort OrdList.T, |
48 hyps: term OrdList.T, |
48 hyps: term OrdList.T, |
49 tpairs: (term * term) list, |
49 tpairs: (term * term) list, |
|
50 prop: term} |
|
51 type deriv (*WN*) |
|
52 val rep_thm_G:(*WN*) thm -> |
|
53 deriv * |
|
54 {thy_ref: theory_ref, (*new since 2002*) |
|
55 tags: Properties.T, (*new since 2002*) |
|
56 maxidx: int, |
|
57 shyps: sort OrdList.T, |
|
58 hyps: term OrdList.T, |
|
59 tpairs: (term * term) list,(*new since 2002*) |
50 prop: term} |
60 prop: term} |
51 val crep_thm: thm -> |
61 val crep_thm: thm -> |
52 {thy_ref: theory_ref, |
62 {thy_ref: theory_ref, |
53 tags: Properties.T, |
63 tags: Properties.T, |
54 maxidx: int, |
64 maxidx: int, |
70 val weaken_sorts: sort list -> cterm -> cterm |
80 val weaken_sorts: sort list -> cterm -> cterm |
71 val extra_shyps: thm -> sort list |
81 val extra_shyps: thm -> sort list |
72 |
82 |
73 (*meta rules*) |
83 (*meta rules*) |
74 val assume: cterm -> thm |
84 val assume: cterm -> thm |
|
85 val make_thm:(*WN*) cterm -> thm |
|
86 val assbl_thm:(*WN*) deriv -> |
|
87 theory_ref -> |
|
88 Properties.T -> |
|
89 int -> |
|
90 sort OrdList.T -> |
|
91 term OrdList.T -> |
|
92 (term * term) list -> |
|
93 term -> |
|
94 thm |
75 val implies_intr: cterm -> thm -> thm |
95 val implies_intr: cterm -> thm -> thm |
76 val implies_elim: thm -> thm -> thm |
96 val implies_elim: thm -> thm -> thm |
77 val forall_intr: cterm -> thm -> thm |
97 val forall_intr: cterm -> thm -> thm |
78 val forall_elim: cterm -> thm -> thm |
98 val forall_elim: cterm -> thm -> thm |
79 val reflexive: cterm -> thm |
99 val reflexive: cterm -> thm |
356 |
376 |
357 (*errors involving theorems*) |
377 (*errors involving theorems*) |
358 exception THM of string * int * thm list; |
378 exception THM of string * int * thm list; |
359 |
379 |
360 fun rep_thm (Thm (_, args)) = args; |
380 fun rep_thm (Thm (_, args)) = args; |
|
381 fun rep_thm_G (Thm (deriv , args)) = (deriv, args); (*WN*) |
361 |
382 |
362 fun crep_thm (Thm (_, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = |
383 fun crep_thm (Thm (_, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = |
363 let fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps} in |
384 let fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps} in |
364 {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps, |
385 {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps, |
365 hyps = map (cterm ~1) hyps, |
386 hyps = map (cterm ~1) hyps, |
670 shyps = sorts, |
691 shyps = sorts, |
671 hyps = [prop], |
692 hyps = [prop], |
672 tpairs = [], |
693 tpairs = [], |
673 prop = prop}) |
694 prop = prop}) |
674 end; |
695 end; |
|
696 fun make_thm raw_ct = (*WN ---vvv *) |
|
697 let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in |
|
698 if T <> propT then |
|
699 raise THM ("assume: prop", 0, []) |
|
700 (*else if maxidx <> ~1 then (*WN true with matches (?b * v_ = 0)..*) |
|
701 raise THM ("assume: variables", maxidx, [])*) |
|
702 else Thm (deriv_rule0 (Proofterm.Hyp prop), |
|
703 {thy_ref = thy_ref, |
|
704 tags = [], |
|
705 maxidx = ~1, |
|
706 shyps = sorts, |
|
707 hyps = [prop], |
|
708 tpairs = [], |
|
709 prop = prop}) |
|
710 end; (*WN ---^^^ *) |
|
711 fun assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop = (*WN*) |
|
712 Thm (deriv, {thy_ref=thy_ref, tags=tags, maxidx=maxidx, |
|
713 shyps=shyps, hyps=hyps, tpairs=tpairs, prop=prop}); |
675 |
714 |
676 (*Implication introduction |
715 (*Implication introduction |
677 [A] |
716 [A] |
678 : |
717 : |
679 B |
718 B |