95 *} |
95 *} |
96 |
96 |
97 (*lemma equality_twice: |
97 (*lemma equality_twice: |
98 "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)" |
98 "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)" |
99 by auto*) |
99 by auto*) |
|
100 |
|
101 |
|
102 (*interpretation code *) |
|
103 (*val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
|
104 val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4; |
|
105 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
|
106 val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5; |
|
107 val eqn2i = Thm.prop_of (symmetric eqn2pre) |
|
108 |
|
109 val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6)); |
|
110 val exp_term = Morphism.term exp_morphism; |
|
111 val exp = Morphism.thm exp_morphism; |
|
112 |
|
113 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
|
114 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) |
|
115 val mthdt = Method.Basic (fn _ => mthd) |
|
116 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
|
117 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
|
118 Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]*) |
|
119 |
|
120 (*||> Local_Theory.theory (fn thy => |
|
121 let |
|
122 val global_eqns = map exp_term [eqn2i, eqn1i]; |
|
123 (* Not sure if the following context should not be used *) |
|
124 val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6; |
|
125 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
|
126 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)*) |