examples/sigma/semanticsScript.sml

60 (* This defines TC in the logic as TC R is the transitive closure of R,  *)
63 (* induction tactis, cases theorems, etc.  It's theory "TC".             *)
74           val (TC,Ru'v') = boolSyntax.strip_comb ant
79           (*val (TC,[R,u',v']) = boolSyntax.strip_comb ant*)
80           (*val {Name = "TC",...} = dest_const TC*)
81           val _ = if #Name(dest_const TC) = "TC" then true else raise Match
100     ���!R (a:'a) b. TC R a b ==>
102                (?d. R b d /\ TC R c d)))���,
123     ���!R (a:'a) b. TC R a b ==>
124           (DIAMOND R ==> (!c. TC R a c ==>
125                (?d. TC R b d /\ TC R c d)))���,
145     ���!R:'a->'a->bool. DIAMOND R ==> DIAMOND (TC R)���,
1828 TC   R   =   R-arrow with "*" superscript after   =   transitive closure
2003     ���(!o1 o2. TC (RC (RED1_obj SIGMA_R)) o1 o2
2005         (!d1 d2. TC (RC (RED1_dict SIGMA_R)) d1 d2
2007         (!e1 e2. TC (RC (RED1_entry SIGMA_R)) e1 e2
2009         (!m1 m2. TC (RC (RED1_method SIGMA_R)) m1 m2
2022                    ==> TC (RC (RED1_obj R)) o1 o2) /\
2024                    ==> TC (RC (RED1_dict R)) d1 d2) /\
2026                    ==> TC (RC (RED1_entry R)) e1 e2) /\
2028                    ==> TC (RC (RED1_method R)) m1 m2)���,
2040     ���(!o1 o2. TC (RC (RED1_obj SIGMA_R)) o1 o2
2042         (!d1 d2. TC (RC (RED1_dict SIGMA_R)) d1 d2
2044         (!e1 e2. TC (RC (RED1_entry SIGMA_R)) e1 e2
2046         (!m1 m2. TC (RC (RED1_method SIGMA_R)) m1 m2
2062     ���(!o1 o2. TC REDL_obj o1 o2 ==> RED_obj SIGMA_R o1 o2) /\
2063         (!d1 d2. TC REDL_dict d1 d2 ==> RED_dict SIGMA_R d1 d2) /\
2064         (!e1 e2. TC REDL_entry e1 e2 ==> RED_entry SIGMA_R e1 e2) /\
2065         (!m1 m2. TC REDL_method m1 m2 ==> RED_method SIGMA_R m1 m2)���,
2076           TC R1 a b ==> (!x y. R1 x y ==> R2 x y) ==> TC R2 a b���,
2093                 (TC R1 a b ==> TC R2 a b)���,
2100     ���(!o1 o2. TC REDL_obj o1 o2 = RED_obj SIGMA_R o1 o2) /\
2101         (!d1 d2. TC REDL_dict d1 d2 = RED_dict SIGMA_R d1 d2) /\
2102         (!e1 e2. TC REDL_entry e1 e2 = RED_entry SIGMA_R e1 e2) /\
2103         (!m1 m2. TC REDL_method m1 m2 = RED_method SIGMA_R m1 m2)���,
2120     ���(TC REDL_obj = RED_obj SIGMA_R) /\
2121         (TC REDL_dict = RED_dict SIGMA_R) /\
2122         (TC REDL_entry = RED_entry SIGMA_R) /\
2123         (TC REDL_method = RED_method SIGMA_R)���,